[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
⊢ evariance X μ < ⊤
[PROOFSTEP]
have := ENNReal.pow_lt_top (hX.sub <| memℒp_const <| μ[X]).2 2
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
this : snorm (X - fun x => ∫ (x : Ω), X x ∂μ) 2 μ ^ 2 < ⊤
⊢ evariance X μ < ⊤
[PROOFSTEP]
rw [snorm_eq_lintegral_rpow_nnnorm two_ne_zero ENNReal.two_ne_top, ← ENNReal.rpow_two] at this
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
this : ((∫⁻ (x : Ω), ↑‖(X - fun x => ∫ (x : Ω), X x ∂μ) x‖₊ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2)) ^ 2 < ⊤
⊢ evariance X μ < ⊤
[PROOFSTEP]
simp only [coe_two, Pi.sub_apply, ENNReal.one_toReal, one_div] at this
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
this : ((∫⁻ (x : Ω), ↑‖X x - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 ∂μ) ^ 2⁻¹) ^ 2 < ⊤
⊢ evariance X μ < ⊤
[PROOFSTEP]
rw [← ENNReal.rpow_mul, inv_mul_cancel (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_one] at this
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
this : ∫⁻ (x : Ω), ↑‖X x - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 ∂μ < ⊤
⊢ evariance X μ < ⊤
[PROOFSTEP]
simp_rw [ENNReal.rpow_two] at this
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
this : ∫⁻ (x : Ω), ↑‖X x - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 ∂μ < ⊤
⊢ evariance X μ < ⊤
[PROOFSTEP]
exact this
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
⊢ evariance X μ = ⊤
[PROOFSTEP]
by_contra h
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : ¬evariance X μ = ⊤
⊢ False
[PROOFSTEP]
rw [← Ne.def, ← lt_top_iff_ne_top] at h
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : evariance X μ < ⊤
⊢ False
[PROOFSTEP]
have : Memℒp (fun ω => X ω - μ[X]) 2 μ :=
  by
  refine' ⟨hXm.sub aestronglyMeasurable_const, _⟩
  rw [snorm_eq_lintegral_rpow_nnnorm two_ne_zero ENNReal.two_ne_top]
  simp only [coe_two, ENNReal.one_toReal, ENNReal.rpow_two, Ne.def]
  exact ENNReal.rpow_lt_top_of_nonneg (by linarith) h.ne
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : evariance X μ < ⊤
⊢ Memℒp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2
[PROOFSTEP]
refine' ⟨hXm.sub aestronglyMeasurable_const, _⟩
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : evariance X μ < ⊤
⊢ snorm (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ < ⊤
[PROOFSTEP]
rw [snorm_eq_lintegral_rpow_nnnorm two_ne_zero ENNReal.two_ne_top]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : evariance X μ < ⊤
⊢ (∫⁻ (x : Ω), ↑‖X x - ∫ (x : Ω), X x ∂μ‖₊ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2) < ⊤
[PROOFSTEP]
simp only [coe_two, ENNReal.one_toReal, ENNReal.rpow_two, Ne.def]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : evariance X μ < ⊤
⊢ (∫⁻ (x : Ω), ↑‖X x - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 ∂μ) ^ (1 / 2) < ⊤
[PROOFSTEP]
exact ENNReal.rpow_lt_top_of_nonneg (by linarith) h.ne
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : evariance X μ < ⊤
⊢ 0 ≤ 1 / 2
[PROOFSTEP]
linarith
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : evariance X μ < ⊤
this : Memℒp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2
⊢ False
[PROOFSTEP]
refine'
  hX
    _
      -- Porting note: `μ[X]` without whitespace is ambiguous as it could be GetElem,
        -- and `convert` cannot disambiguate based on typeclass inference failure.
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : evariance X μ < ⊤
this : Memℒp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2
⊢ Memℒp X 2
[PROOFSTEP]
convert this.add (memℒp_const <| μ [X])
[GOAL]
case h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : evariance X μ < ⊤
this : Memℒp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2
⊢ X = (fun ω => X ω - ∫ (x : Ω), X x ∂μ) + fun x => ∫ (x : Ω), X x ∂μ
[PROOFSTEP]
ext ω
[GOAL]
case h.e'_5.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬Memℒp X 2
h : evariance X μ < ⊤
this : Memℒp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2
ω : Ω
⊢ X ω = ((fun ω => X ω - ∫ (x : Ω), X x ∂μ) + fun x => ∫ (x : Ω), X x ∂μ) ω
[PROOFSTEP]
rw [Pi.add_apply, sub_add_cancel]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ evariance X μ < ⊤ ↔ Memℒp X 2
[PROOFSTEP]
refine' ⟨_, MeasureTheory.Memℒp.evariance_lt_top⟩
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ evariance X μ < ⊤ → Memℒp X 2
[PROOFSTEP]
contrapose
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬Memℒp X 2 → ¬evariance X μ < ⊤
[PROOFSTEP]
rw [not_lt, top_le_iff]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬Memℒp X 2 → evariance X μ = ⊤
[PROOFSTEP]
exact evariance_eq_top hX
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
⊢ ENNReal.ofReal (variance X μ) = evariance X μ
[PROOFSTEP]
rw [variance, ENNReal.ofReal_toReal]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
⊢ evariance X μ ≠ ⊤
[PROOFSTEP]
exact hX.evariance_lt_top.ne
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
X : Ω → ℝ
μ : Measure Ω
⊢ evariance X μ = ∫⁻ (ω : Ω), ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2) ∂μ
[PROOFSTEP]
rw [evariance]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
X : Ω → ℝ
μ : Measure Ω
⊢ ∫⁻ (ω : Ω), ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 ∂μ = ∫⁻ (ω : Ω), ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2) ∂μ
[PROOFSTEP]
congr
[GOAL]
case e_f
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
X : Ω → ℝ
μ : Measure Ω
⊢ (fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) = fun ω => ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2)
[PROOFSTEP]
ext1 ω
[GOAL]
case e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 = ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2)
[PROOFSTEP]
rw [pow_two, ← ENNReal.coe_mul, ← nnnorm_mul, ← pow_two]
[GOAL]
case e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ↑‖(X ω - ∫ (x : Ω), X x ∂μ) ^ 2‖₊ = ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2)
[PROOFSTEP]
congr
[GOAL]
case e_f.h.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ‖(X ω - ∫ (x : Ω), X x ∂μ) ^ 2‖₊ = Real.toNNReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2)
[PROOFSTEP]
exact (Real.toNNReal_eq_nnnorm_of_nonneg <| sq_nonneg _).symm
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : Memℒp X 2
hXint : ∫ (x : Ω), X x ∂μ = 0
⊢ variance X μ = ∫ (x : Ω), (X ^ 2) x ∂μ
[PROOFSTEP]
rw [variance, evariance_eq_lintegral_ofReal, ← ofReal_integral_eq_lintegral_ofReal, ENNReal.toReal_ofReal]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : Memℒp X 2
hXint : ∫ (x : Ω), X x ∂μ = 0
⊢ ∫ (x : Ω), (X x - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ = ∫ (x : Ω), (X ^ 2) x ∂μ
[PROOFSTEP]
simp_rw [hXint, sub_zero]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : Memℒp X 2
hXint : ∫ (x : Ω), X x ∂μ = 0
⊢ 0 ≤ ∫ (x : Ω), (X x - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ
[PROOFSTEP]
simp_rw [hXint, sub_zero]
[GOAL]
case hfi
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : Memℒp X 2
hXint : ∫ (x : Ω), X x ∂μ = 0
⊢ Integrable fun ω => (X ω - ∫ (x : Ω), X x ∂μ) ^ 2
[PROOFSTEP]
simp_rw [hXint, sub_zero]
[GOAL]
case f_nn
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : Memℒp X 2
hXint : ∫ (x : Ω), X x ∂μ = 0
⊢ 0 ≤ᵐ[μ] fun ω => (X ω - ∫ (x : Ω), X x ∂μ) ^ 2
[PROOFSTEP]
simp_rw [hXint, sub_zero]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : Memℒp X 2
hXint : ∫ (x : Ω), X x ∂μ = 0
⊢ ∫ (x : Ω), X x ^ 2 ∂μ = ∫ (x : Ω), (X ^ 2) x ∂μ
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : Memℒp X 2
hXint : ∫ (x : Ω), X x ∂μ = 0
⊢ 0 ≤ ∫ (x : Ω), X x ^ 2 ∂μ
[PROOFSTEP]
exact integral_nonneg fun ω => pow_two_nonneg _
[GOAL]
case hfi
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : Memℒp X 2
hXint : ∫ (x : Ω), X x ∂μ = 0
⊢ Integrable fun ω => X ω ^ 2
[PROOFSTEP]
convert hX.integrable_norm_rpow two_ne_zero ENNReal.two_ne_top with ω
[GOAL]
case h.e'_5.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : Memℒp X 2
hXint : ∫ (x : Ω), X x ∂μ = 0
ω : Ω
⊢ X ω ^ 2 = ‖X ω‖ ^ ENNReal.toReal 2
[PROOFSTEP]
simp only [Pi.sub_apply, Real.norm_eq_abs, coe_two, ENNReal.one_toReal, Real.rpow_two, sq_abs, abs_pow]
[GOAL]
case f_nn
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : Memℒp X 2
hXint : ∫ (x : Ω), X x ∂μ = 0
⊢ 0 ≤ᵐ[μ] fun ω => X ω ^ 2
[PROOFSTEP]
exact ae_of_all _ fun ω => pow_two_nonneg _
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
⊢ variance X μ = ∫ (x : Ω), ((X - fun x => ∫ (x : Ω), X x ∂μ) ^ 2) x ∂μ
[PROOFSTEP]
rw [variance, evariance_eq_lintegral_ofReal, ← ofReal_integral_eq_lintegral_ofReal, ENNReal.toReal_ofReal]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
⊢ ∫ (x : Ω), (X x - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ = ∫ (x : Ω), ((X - fun x => ∫ (x : Ω), X x ∂μ) ^ 2) x ∂μ
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
⊢ 0 ≤ ∫ (x : Ω), (X x - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ
[PROOFSTEP]
exact integral_nonneg fun ω => pow_two_nonneg _
[GOAL]
case hfi
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
⊢ Integrable fun ω => (X ω - ∫ (x : Ω), X x ∂μ) ^ 2
[PROOFSTEP]
convert (hX.sub <| memℒp_const (μ [X])).integrable_norm_rpow two_ne_zero ENNReal.two_ne_top with ω
[GOAL]
case h.e'_5.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
ω : Ω
⊢ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 = ‖(X - fun x => ∫ (x : Ω), X x ∂μ) ω‖ ^ ENNReal.toReal 2
[PROOFSTEP]
simp only [Pi.sub_apply, Real.norm_eq_abs, coe_two, ENNReal.one_toReal, Real.rpow_two, sq_abs, abs_pow]
[GOAL]
case f_nn
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : Memℒp X 2
⊢ 0 ≤ᵐ[μ] fun ω => (X ω - ∫ (x : Ω), X x ∂μ) ^ 2
[PROOFSTEP]
exact ae_of_all _ fun ω => pow_two_nonneg _
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ evariance 0 μ = 0
[PROOFSTEP]
simp [evariance]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X
⊢ evariance X μ = 0 ↔ X =ᵐ[μ] fun x => ∫ (x : Ω), X x ∂μ
[PROOFSTEP]
rw [evariance, lintegral_eq_zero_iff']
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X
⊢ (fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) =ᵐ[μ] 0 ↔ X =ᵐ[μ] fun x => ∫ (x : Ω), X x ∂μ
[PROOFSTEP]
constructor
[GOAL]
case mp
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X
⊢ (fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) =ᵐ[μ] 0 → X =ᵐ[μ] fun x => ∫ (x : Ω), X x ∂μ
[PROOFSTEP]
intro hX
[GOAL]
case mpr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X
⊢ (X =ᵐ[μ] fun x => ∫ (x : Ω), X x ∂μ) → (fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) =ᵐ[μ] 0
[PROOFSTEP]
intro hX
[GOAL]
case mp
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX✝ : AEMeasurable X
hX : (fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) =ᵐ[μ] 0
⊢ X =ᵐ[μ] fun x => ∫ (x : Ω), X x ∂μ
[PROOFSTEP]
filter_upwards [hX] with ω hω
[GOAL]
case mpr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX✝ : AEMeasurable X
hX : X =ᵐ[μ] fun x => ∫ (x : Ω), X x ∂μ
⊢ (fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) =ᵐ[μ] 0
[PROOFSTEP]
filter_upwards [hX] with ω hω
[GOAL]
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX✝ : AEMeasurable X
hX : (fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) =ᵐ[μ] 0
ω : Ω
hω : ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 = OfNat.ofNat 0 ω
⊢ X ω = ∫ (x : Ω), X x ∂μ
[PROOFSTEP]
simp only [Pi.zero_apply, pow_eq_zero_iff, Nat.succ_pos', ENNReal.coe_eq_zero, nnnorm_eq_zero, sub_eq_zero] at hω
[GOAL]
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX✝ : AEMeasurable X
hX : (fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2) =ᵐ[μ] 0
ω : Ω
hω : X ω = ∫ (x : Ω), X x ∂μ
⊢ X ω = ∫ (x : Ω), X x ∂μ
[PROOFSTEP]
exact hω
[GOAL]
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX✝ : AEMeasurable X
hX : X =ᵐ[μ] fun x => ∫ (x : Ω), X x ∂μ
ω : Ω
hω : X ω = ∫ (x : Ω), X x ∂μ
⊢ ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 = OfNat.ofNat 0 ω
[PROOFSTEP]
rw [hω]
[GOAL]
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX✝ : AEMeasurable X
hX : X =ᵐ[μ] fun x => ∫ (x : Ω), X x ∂μ
ω : Ω
hω : X ω = ∫ (x : Ω), X x ∂μ
⊢ ↑‖∫ (x : Ω), X x ∂μ - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 = OfNat.ofNat 0 ω
[PROOFSTEP]
simp
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X
⊢ AEMeasurable fun ω => ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2
[PROOFSTEP]
measurability
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ evariance (fun ω => c * X ω) μ = ENNReal.ofReal (c ^ 2) * evariance X μ
[PROOFSTEP]
rw [evariance, evariance, ← lintegral_const_mul' _ _ ENNReal.ofReal_lt_top.ne]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ ∫⁻ (ω : Ω), ↑‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2 ∂μ =
    ∫⁻ (a : Ω), ENNReal.ofReal (c ^ 2) * ↑‖X a - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 ∂μ
[PROOFSTEP]
congr
[GOAL]
case e_f
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ (fun ω => ↑‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2) = fun a => ENNReal.ofReal (c ^ 2) * ↑‖X a - ∫ (x : Ω), X x ∂μ‖₊ ^ 2
[PROOFSTEP]
ext1 ω
[GOAL]
case e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ↑‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2 = ENNReal.ofReal (c ^ 2) * ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2
[PROOFSTEP]
rw [ENNReal.ofReal, ← ENNReal.coe_pow, ← ENNReal.coe_pow, ← ENNReal.coe_mul]
[GOAL]
case e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ↑(‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2) = ↑(Real.toNNReal (c ^ 2) * ‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2)
[PROOFSTEP]
congr
[GOAL]
case e_f.h.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2 = Real.toNNReal (c ^ 2) * ‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2
[PROOFSTEP]
rw [← sq_abs, ← Real.rpow_two, Real.toNNReal_rpow_of_nonneg (abs_nonneg _), NNReal.rpow_two, ← mul_pow,
  Real.toNNReal_mul_nnnorm _ (abs_nonneg _)]
[GOAL]
case e_f.h.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2 = ‖|c| * (X ω - ∫ (x : Ω), X x ∂μ)‖₊ ^ 2
[PROOFSTEP]
conv_rhs => rw [← nnnorm_norm, norm_mul, norm_abs_eq_norm, ← norm_mul, nnnorm_norm, mul_sub]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
| ‖|c| * (X ω - ∫ (x : Ω), X x ∂μ)‖₊ ^ 2
[PROOFSTEP]
rw [← nnnorm_norm, norm_mul, norm_abs_eq_norm, ← norm_mul, nnnorm_norm, mul_sub]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
| ‖|c| * (X ω - ∫ (x : Ω), X x ∂μ)‖₊ ^ 2
[PROOFSTEP]
rw [← nnnorm_norm, norm_mul, norm_abs_eq_norm, ← norm_mul, nnnorm_norm, mul_sub]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
| ‖|c| * (X ω - ∫ (x : Ω), X x ∂μ)‖₊ ^ 2
[PROOFSTEP]
rw [← nnnorm_norm, norm_mul, norm_abs_eq_norm, ← norm_mul, nnnorm_norm, mul_sub]
[GOAL]
case e_f.h.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2 = ‖c * X ω - c * ∫ (x : Ω), X x ∂μ‖₊ ^ 2
[PROOFSTEP]
congr
[GOAL]
case e_f.h.e_a.e_a.e_a.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ∫ (x : Ω), c * X x ∂μ = c * ∫ (x : Ω), X x ∂μ
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case e_f.h.e_a.e_a.e_a.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ ∫ (x : Ω), c * X x ∂μ = (∫ (x : Ω), X x ∂μ) * c
[PROOFSTEP]
simp_rw [← smul_eq_mul, ← integral_smul_const, smul_eq_mul, mul_comm]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ✝ μ : Measure Ω
⊢ variance 0 μ = 0
[PROOFSTEP]
simp only [variance, evariance_zero, ENNReal.zero_toReal]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ variance (fun ω => c * X ω) μ = c ^ 2 * variance X μ
[PROOFSTEP]
rw [variance, evariance_mul, ENNReal.toReal_mul, ENNReal.toReal_ofReal (sq_nonneg _)]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ c ^ 2 * ENNReal.toReal (evariance (fun ω => X ω) μ) = c ^ 2 * variance X μ
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ variance (c • X) μ = c ^ 2 • variance X μ
[PROOFSTEP]
convert variance_smul (algebraMap A ℝ c) X μ using 1
[GOAL]
case h.e'_2
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ variance (c • X) μ = variance (↑(algebraMap A ℝ) c • X) μ
[PROOFSTEP]
congr
[GOAL]
case h.e'_2.e_X
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ c • X = ↑(algebraMap A ℝ) c • X
[PROOFSTEP]
simp only [algebraMap_smul]
[GOAL]
case h.e'_3
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ✝ : Measure Ω
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ c ^ 2 • variance X μ = ↑(algebraMap A ℝ) c ^ 2 * variance X μ
[PROOFSTEP]
simp only [Algebra.smul_def, map_pow]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ variance X ℙ = (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2
[PROOFSTEP]
rw [hX.variance_eq, sub_sq', integral_sub', integral_add']
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ ((∫ (a : Ω), (X ^ 2) a) + ∫ (a : Ω), ((fun x => ∫ (x : Ω), X x) ^ 2) a) -
      ∫ (a : Ω), (2 * X * fun x => ∫ (x : Ω), X x) a =
    (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ Integrable (X ^ 2)
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ Integrable ((fun x => ∫ (x : Ω), X x) ^ 2)
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ Integrable (X ^ 2 + (fun x => ∫ (x : Ω), X x) ^ 2)
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ Integrable (2 * X * fun x => ∫ (x : Ω), X x)
[PROOFSTEP]
rotate_left
[GOAL]
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ Integrable (X ^ 2)
[PROOFSTEP]
exact hX.integrable_sq
[GOAL]
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ Integrable ((fun x => ∫ (x : Ω), X x) ^ 2)
[PROOFSTEP]
convert @integrable_const Ω ℝ (_) ℙ _ _ (𝔼[X] ^ 2)
[GOAL]
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ Integrable (X ^ 2 + (fun x => ∫ (x : Ω), X x) ^ 2)
[PROOFSTEP]
apply hX.integrable_sq.add
[GOAL]
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ Integrable ((fun x => ∫ (x : Ω), X x) ^ 2)
[PROOFSTEP]
convert @integrable_const Ω ℝ (_) ℙ _ _ (𝔼[X] ^ 2)
[GOAL]
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ Integrable (2 * X * fun x => ∫ (x : Ω), X x)
[PROOFSTEP]
exact ((hX.integrable one_le_two).const_mul 2).mul_const' _
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ ((∫ (a : Ω), (X ^ 2) a) + ∫ (a : Ω), ((fun x => ∫ (x : Ω), X x) ^ 2) a) -
      ∫ (a : Ω), (2 * X * fun x => ∫ (x : Ω), X x) a =
    (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2
[PROOFSTEP]
simp [integral_mul_right, integral_mul_left]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
⊢ (∫ (a : Ω), X a ^ 2) + (∫ (x : Ω), X x) ^ 2 - (2 * ∫ (x : Ω), X x) * ∫ (x : Ω), X x =
    (∫ (a : Ω), X a ^ 2) - (∫ (x : Ω), X x) ^ 2
[PROOFSTEP]
ring
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
⊢ variance X ℙ ≤ ∫ (a : Ω), (X ^ 2) a
[PROOFSTEP]
by_cases hX : Memℒp X 2
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : Memℒp X 2
⊢ variance X ℙ ≤ ∫ (a : Ω), (X ^ 2) a
[PROOFSTEP]
rw [variance_def' hX]
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : Memℒp X 2
⊢ (∫ (a : Ω), (X ^ 2) a) - (∫ (a : Ω), X a) ^ 2 ≤ ∫ (a : Ω), (X ^ 2) a
[PROOFSTEP]
simp only [sq_nonneg, sub_le_self_iff]
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
⊢ variance X ℙ ≤ ∫ (a : Ω), (X ^ 2) a
[PROOFSTEP]
rw [variance, evariance_eq_lintegral_ofReal, ← integral_eq_lintegral_of_nonneg_ae]
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x) ^ 2 ≤ ∫ (a : Ω), (X ^ 2) a
case neg.hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
⊢ 0 ≤ᵐ[ℙ] fun ω => (X ω - ∫ (x : Ω), X x) ^ 2
case neg.hfm
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
⊢ AEStronglyMeasurable (fun ω => (X ω - ∫ (x : Ω), X x) ^ 2) ℙ
[PROOFSTEP]
by_cases hint : Integrable X
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : Integrable X
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x) ^ 2 ≤ ∫ (a : Ω), (X ^ 2) a
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : ¬Integrable X
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x) ^ 2 ≤ ∫ (a : Ω), (X ^ 2) a
case neg.hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
⊢ 0 ≤ᵐ[ℙ] fun ω => (X ω - ∫ (x : Ω), X x) ^ 2
case neg.hfm
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
⊢ AEStronglyMeasurable (fun ω => (X ω - ∫ (x : Ω), X x) ^ 2) ℙ
[PROOFSTEP]
swap
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : ¬Integrable X
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x) ^ 2 ≤ ∫ (a : Ω), (X ^ 2) a
[PROOFSTEP]
simp only [integral_undef hint, Pi.pow_apply, Pi.sub_apply, sub_zero]
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : ¬Integrable X
⊢ ∫ (a : Ω), X a ^ 2 ≤ ∫ (a : Ω), X a ^ 2
[PROOFSTEP]
exact le_rfl
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : Integrable X
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x) ^ 2 ≤ ∫ (a : Ω), (X ^ 2) a
[PROOFSTEP]
rw [integral_undef]
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : Integrable X
⊢ 0 ≤ ∫ (a : Ω), (X ^ 2) a
[PROOFSTEP]
exact integral_nonneg fun a => sq_nonneg _
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : Integrable X
⊢ ¬Integrable fun a => (X a - ∫ (x : Ω), X x) ^ 2
[PROOFSTEP]
intro h
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : Integrable X
h : Integrable fun a => (X a - ∫ (x : Ω), X x) ^ 2
⊢ False
[PROOFSTEP]
have A : Memℒp (X - fun ω : Ω => 𝔼[X]) 2 ℙ :=
  (memℒp_two_iff_integrable_sq (hint.aestronglyMeasurable.sub aestronglyMeasurable_const)).2 h
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : Integrable X
h : Integrable fun a => (X a - ∫ (x : Ω), X x) ^ 2
A : Memℒp (X - fun ω => ∫ (a : Ω), X a) 2
⊢ False
[PROOFSTEP]
have B : Memℒp (fun _ : Ω => 𝔼[X]) 2 ℙ := memℒp_const _
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : Integrable X
h : Integrable fun a => (X a - ∫ (x : Ω), X x) ^ 2
A : Memℒp (X - fun ω => ∫ (a : Ω), X a) 2
B : Memℒp (fun x => ∫ (a : Ω), X a) 2
⊢ False
[PROOFSTEP]
apply hX
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : Integrable X
h : Integrable fun a => (X a - ∫ (x : Ω), X x) ^ 2
A : Memℒp (X - fun ω => ∫ (a : Ω), X a) 2
B : Memℒp (fun x => ∫ (a : Ω), X a) 2
⊢ Memℒp X 2
[PROOFSTEP]
convert A.add B
[GOAL]
case h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
hint : Integrable X
h : Integrable fun a => (X a - ∫ (x : Ω), X x) ^ 2
A : Memℒp (X - fun ω => ∫ (a : Ω), X a) 2
B : Memℒp (fun x => ∫ (a : Ω), X a) 2
⊢ X = (X - fun ω => ∫ (a : Ω), X a) + fun x => ∫ (a : Ω), X a
[PROOFSTEP]
simp
[GOAL]
case neg.hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
⊢ 0 ≤ᵐ[ℙ] fun ω => (X ω - ∫ (x : Ω), X x) ^ 2
[PROOFSTEP]
exact @ae_of_all _ (_) _ _ fun x => sq_nonneg _
[GOAL]
case neg.hfm
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hm : AEStronglyMeasurable X ℙ
hX : ¬Memℒp X 2
⊢ AEStronglyMeasurable (fun ω => (X ω - ∫ (x : Ω), X x) ^ 2) ℙ
[PROOFSTEP]
exact (AEMeasurable.pow_const (hm.aemeasurable.sub_const _) _).aestronglyMeasurable
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
⊢ evariance X ℙ = (∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2)) - ENNReal.ofReal ((∫ (a : Ω), X a) ^ 2)
[PROOFSTEP]
by_cases hℒ : Memℒp X 2
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : Memℒp X 2
⊢ evariance X ℙ = (∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2)) - ENNReal.ofReal ((∫ (a : Ω), X a) ^ 2)
[PROOFSTEP]
rw [← hℒ.ofReal_variance_eq, variance_def' hℒ, ENNReal.ofReal_sub _ (sq_nonneg _)]
[GOAL]
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : Memℒp X 2
⊢ ENNReal.ofReal (∫ (a : Ω), (X ^ 2) a) - ENNReal.ofReal ((∫ (a : Ω), X a) ^ 2) =
    (∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2)) - ENNReal.ofReal ((∫ (a : Ω), X a) ^ 2)
[PROOFSTEP]
congr
[GOAL]
case pos.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : Memℒp X 2
⊢ ENNReal.ofReal (∫ (a : Ω), (X ^ 2) a) = ∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2)
[PROOFSTEP]
rw [lintegral_coe_eq_integral]
[GOAL]
case pos.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : Memℒp X 2
⊢ ENNReal.ofReal (∫ (a : Ω), (X ^ 2) a) = ENNReal.ofReal (∫ (a : Ω), ↑(‖X a‖₊ ^ 2))
[PROOFSTEP]
congr 2 with ω
[GOAL]
case pos.e_a.e_r.e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : Memℒp X 2
ω : Ω
⊢ (X ^ 2) ω = ↑(‖X ω‖₊ ^ 2)
[PROOFSTEP]
simp only [Pi.pow_apply, NNReal.coe_pow, coe_nnnorm, Real.norm_eq_abs, Even.pow_abs even_two]
[GOAL]
case pos.e_a.hfi
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : Memℒp X 2
⊢ Integrable fun x => ↑(‖X x‖₊ ^ 2)
[PROOFSTEP]
exact hℒ.abs.integrable_sq
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : ¬Memℒp X 2
⊢ evariance X ℙ = (∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2)) - ENNReal.ofReal ((∫ (a : Ω), X a) ^ 2)
[PROOFSTEP]
symm
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : ¬Memℒp X 2
⊢ (∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2)) - ENNReal.ofReal ((∫ (a : Ω), X a) ^ 2) = evariance X ℙ
[PROOFSTEP]
rw [evariance_eq_top hX hℒ, ENNReal.sub_eq_top_iff]
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : ¬Memℒp X 2
⊢ ∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2) = ⊤ ∧ ENNReal.ofReal ((∫ (a : Ω), X a) ^ 2) ≠ ⊤
[PROOFSTEP]
refine' ⟨_, ENNReal.ofReal_ne_top⟩
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : ¬Memℒp X 2
⊢ ∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2) = ⊤
[PROOFSTEP]
rw [Memℒp, not_and] at hℒ
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : AEStronglyMeasurable X ℙ → ¬snorm X 2 ℙ < ⊤
⊢ ∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2) = ⊤
[PROOFSTEP]
specialize hℒ hX
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : ¬snorm X 2 ℙ < ⊤
⊢ ∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2) = ⊤
[PROOFSTEP]
simp only [snorm_eq_lintegral_rpow_nnnorm two_ne_zero ENNReal.two_ne_top, not_lt, top_le_iff, coe_two, one_div,
  ENNReal.rpow_eq_top_iff, inv_lt_zero, inv_pos, and_true_iff, or_iff_not_imp_left, not_and_or, zero_lt_two] at hℒ
[GOAL]
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
hℒ : (¬¬∫⁻ (x : Ω), ↑‖X x‖₊ ^ 2 = 0 → 0 ≤ 2) → ∫⁻ (x : Ω), ↑‖X x‖₊ ^ 2 = ⊤
⊢ ∫⁻ (ω : Ω), ↑(‖X ω‖₊ ^ 2) = ⊤
[PROOFSTEP]
exact_mod_cast hℒ fun _ => zero_le_two
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
⊢ ↑↑ℙ {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} ≤ evariance X ℙ / ↑(c ^ 2)
[PROOFSTEP]
have A : (c : ℝ≥0∞) ≠ 0 := by rwa [Ne.def, ENNReal.coe_eq_zero]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
⊢ ↑c ≠ 0
[PROOFSTEP]
rwa [Ne.def, ENNReal.coe_eq_zero]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
⊢ ↑↑ℙ {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} ≤ evariance X ℙ / ↑(c ^ 2)
[PROOFSTEP]
have B : AEStronglyMeasurable (fun _ : Ω => 𝔼[X]) ℙ := aestronglyMeasurable_const
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ
⊢ ↑↑ℙ {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} ≤ evariance X ℙ / ↑(c ^ 2)
[PROOFSTEP]
convert meas_ge_le_mul_pow_snorm ℙ two_ne_zero ENNReal.two_ne_top (hX.sub B) A using 1
[GOAL]
case h.e'_3
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ
⊢ ↑↑ℙ {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} = ↑↑ℙ {x | ↑c ≤ ↑‖(X - fun x => ∫ (a : Ω), X a) x‖₊}
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ
⊢ {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} = {x | ↑c ≤ ↑‖(X - fun x => ∫ (a : Ω), X a) x‖₊}
[PROOFSTEP]
simp only [Pi.sub_apply, ENNReal.coe_le_coe, ← Real.norm_eq_abs, ← coe_nnnorm, NNReal.coe_le_coe,
  ENNReal.ofReal_coe_nnreal]
[GOAL]
case h.e'_4
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ
⊢ evariance X ℙ / ↑(c ^ 2) = (↑c)⁻¹ ^ ENNReal.toReal 2 * snorm (X - fun x => ∫ (a : Ω), X a) 2 ℙ ^ ENNReal.toReal 2
[PROOFSTEP]
rw [snorm_eq_lintegral_rpow_nnnorm two_ne_zero ENNReal.two_ne_top]
[GOAL]
case h.e'_4
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ
⊢ evariance X ℙ / ↑(c ^ 2) =
    (↑c)⁻¹ ^ ENNReal.toReal 2 *
      ((∫⁻ (x : Ω), ↑‖(X - fun x => ∫ (a : Ω), X a) x‖₊ ^ ENNReal.toReal 2) ^ (1 / ENNReal.toReal 2)) ^ ENNReal.toReal 2
[PROOFSTEP]
simp only [show ENNReal.some (c ^ 2) = (ENNReal.some c) ^ 2 by norm_cast, coe_two, one_div, Pi.sub_apply]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ
⊢ ↑(c ^ 2) = ↑c ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_4
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ
⊢ evariance X ℙ / ↑c ^ 2 = (↑c)⁻¹ ^ 2 * ((∫⁻ (x : Ω), ↑‖X x - ∫ (a : Ω), X a‖₊ ^ 2) ^ 2⁻¹) ^ 2
[PROOFSTEP]
rw [div_eq_mul_inv, ENNReal.inv_pow, mul_comm, ENNReal.rpow_two]
[GOAL]
case h.e'_4
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ
⊢ (↑c)⁻¹ ^ 2 * evariance X ℙ = (↑c)⁻¹ ^ 2 * ((∫⁻ (x : Ω), ↑‖X x - ∫ (a : Ω), X a‖₊ ^ 2) ^ 2⁻¹) ^ 2
[PROOFSTEP]
congr
[GOAL]
case h.e'_4.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X ℙ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ
⊢ evariance X ℙ = ((∫⁻ (x : Ω), ↑‖X x - ∫ (a : Ω), X a‖₊ ^ 2) ^ 2⁻¹) ^ 2
[PROOFSTEP]
simp_rw [← ENNReal.rpow_mul, inv_mul_cancel (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_two, ENNReal.rpow_one, evariance]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
c : ℝ
hc : 0 < c
⊢ ↑↑ℙ {ω | c ≤ |X ω - ∫ (a : Ω), X a|} ≤ ENNReal.ofReal (variance X ℙ / c ^ 2)
[PROOFSTEP]
rw [ENNReal.ofReal_div_of_pos (sq_pos_of_ne_zero _ hc.ne.symm), hX.ofReal_variance_eq]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
c : ℝ
hc : 0 < c
⊢ ↑↑ℙ {ω | c ≤ |X ω - ∫ (a : Ω), X a|} ≤ evariance X ℙ / ENNReal.ofReal (c ^ 2)
[PROOFSTEP]
convert @meas_ge_le_evariance_div_sq _ _ _ hX.1 c.toNNReal (by simp [hc]) using 1
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
c : ℝ
hc : 0 < c
⊢ Real.toNNReal c ≠ 0
[PROOFSTEP]
simp [hc]
[GOAL]
case h.e'_3
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
c : ℝ
hc : 0 < c
⊢ ↑↑ℙ {ω | c ≤ |X ω - ∫ (a : Ω), X a|} = ↑↑ℙ {ω | ↑(Real.toNNReal c) ≤ |X ω - ∫ (a : Ω), X a|}
[PROOFSTEP]
simp only [Real.coe_toNNReal', max_le_iff, abs_nonneg, and_true_iff]
[GOAL]
case h.e'_4
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
c : ℝ
hc : 0 < c
⊢ evariance X ℙ / ENNReal.ofReal (c ^ 2) = evariance X ℙ / ↑(Real.toNNReal c ^ 2)
[PROOFSTEP]
rw [ENNReal.ofReal_pow hc.le, ENNReal.coe_pow]
[GOAL]
case h.e'_4
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Memℒp X 2
c : ℝ
hc : 0 < c
⊢ evariance X ℙ / ENNReal.ofReal c ^ 2 = evariance X ℙ / ↑(Real.toNNReal c) ^ 2
[PROOFSTEP]
rfl
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ variance (X + Y) ℙ = (∫ (a : Ω), (fun a => X a ^ 2 + Y a ^ 2 + 2 * X a * Y a) a) - (∫ (a : Ω), (X + Y) a) ^ 2
[PROOFSTEP]
simp [variance_def' (hX.add hY), add_sq']
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ (∫ (a : Ω), (fun a => X a ^ 2 + Y a ^ 2 + 2 * X a * Y a) a) - (∫ (a : Ω), (X + Y) a) ^ 2 =
    (((∫ (a : Ω), (X ^ 2) a) + ∫ (a : Ω), (Y ^ 2) a) + 2 * ∫ (a : Ω), (X * Y) a) -
      ((∫ (a : Ω), X a) + ∫ (a : Ω), Y a) ^ 2
[PROOFSTEP]
simp only [Pi.add_apply, Pi.pow_apply, Pi.mul_apply, mul_assoc]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ (∫ (a : Ω), X a ^ 2 + Y a ^ 2 + 2 * (X a * Y a)) - (∫ (a : Ω), X a + Y a) ^ 2 =
    (((∫ (a : Ω), X a ^ 2) + ∫ (a : Ω), Y a ^ 2) + 2 * ∫ (a : Ω), X a * Y a) - ((∫ (a : Ω), X a) + ∫ (a : Ω), Y a) ^ 2
[PROOFSTEP]
rw [integral_add, integral_add, integral_add, integral_mul_left]
[GOAL]
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ Integrable fun a => X a
[PROOFSTEP]
exact hX.integrable one_le_two
[GOAL]
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ Integrable fun a => Y a
[PROOFSTEP]
exact hY.integrable one_le_two
[GOAL]
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ Integrable fun a => X a ^ 2
[PROOFSTEP]
exact hX.integrable_sq
[GOAL]
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ Integrable fun a => Y a ^ 2
[PROOFSTEP]
exact hY.integrable_sq
[GOAL]
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ Integrable fun a => X a ^ 2 + Y a ^ 2
[PROOFSTEP]
exact hX.integrable_sq.add hY.integrable_sq
[GOAL]
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ Integrable fun a => 2 * (X a * Y a)
[PROOFSTEP]
apply Integrable.const_mul
[GOAL]
case hg.h
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ Integrable fun x => X x * Y x
[PROOFSTEP]
exact h.integrable_mul (hX.integrable one_le_two) (hY.integrable one_le_two)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ (((∫ (a : Ω), (X ^ 2) a) + ∫ (a : Ω), (Y ^ 2) a) + 2 * ∫ (a : Ω), (X * Y) a) -
      ((∫ (a : Ω), X a) + ∫ (a : Ω), Y a) ^ 2 =
    ((∫ (a : Ω), (X ^ 2) a) + ∫ (a : Ω), (Y ^ 2) a) + ↑2 * ((∫ (a : Ω), X a) * ∫ (a : Ω), Y a) -
      ((∫ (a : Ω), X a) + ∫ (a : Ω), Y a) ^ 2
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a.e_a
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ ∫ (a : Ω), (X * Y) a = (∫ (a : Ω), X a) * ∫ (a : Ω), Y a
[PROOFSTEP]
exact h.integral_mul_of_integrable (hX.integrable one_le_two) (hY.integrable one_le_two)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ ((∫ (a : Ω), (X ^ 2) a) + ∫ (a : Ω), (Y ^ 2) a) + ↑2 * ((∫ (a : Ω), X a) * ∫ (a : Ω), Y a) -
      ((∫ (a : Ω), X a) + ∫ (a : Ω), Y a) ^ 2 =
    variance X ℙ + variance Y ℙ
[PROOFSTEP]
simp only [variance_def', hX, hY, Pi.pow_apply]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X Y : Ω → ℝ
hX : Memℒp X 2
hY : Memℒp Y 2
h : IndepFun X Y
⊢ ((∫ (a : Ω), X a ^ 2) + ∫ (a : Ω), Y a ^ 2) + ↑2 * ((∫ (a : Ω), X a) * ∫ (a : Ω), Y a) -
      ((∫ (a : Ω), X a) + ∫ (a : Ω), Y a) ^ 2 =
    (∫ (a : Ω), X a ^ 2) - (∫ (a : Ω), X a) ^ 2 + ((∫ (a : Ω), Y a ^ 2) - (∫ (a : Ω), Y a) ^ 2)
[PROOFSTEP]
ring
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ (i : ι), i ∈ s → Memℒp (X i) 2
h : Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)
⊢ variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
[PROOFSTEP]
classical
induction' s using Finset.induction_on with k s ks IH
· simp only [Finset.sum_empty, variance_zero]
rw [variance_def' (memℒp_finset_sum' _ hs), sum_insert ks, sum_insert ks]
simp only [add_sq']
calc
  𝔼[X k ^ 2 + (∑ i in s, X i) ^ 2 + 2 * X k * ∑ i in s, X i] - 𝔼[X k + ∑ i in s, X i] ^ 2 =
      𝔼[X k ^ 2] + 𝔼[(∑ i in s, X i) ^ 2] + 𝔼[2 * X k * ∑ i in s, X i] - (𝔼[X k] + 𝔼[∑ i in s, X i]) ^ 2 :=
    by
    rw [integral_add', integral_add', integral_add']
    · exact Memℒp.integrable one_le_two (hs _ (mem_insert_self _ _))
    · apply integrable_finset_sum' _ fun i hi => ?_
      exact Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi))
    · exact Memℒp.integrable_sq (hs _ (mem_insert_self _ _))
    · apply Memℒp.integrable_sq
      exact memℒp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi)
    · apply Integrable.add
      · exact Memℒp.integrable_sq (hs _ (mem_insert_self _ _))
      · apply Memℒp.integrable_sq
        exact memℒp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi)
    · rw [mul_assoc]
      apply Integrable.const_mul _ (2 : ℝ)
      simp only [mul_sum, sum_apply, Pi.mul_apply]
      apply integrable_finset_sum _ fun i hi => ?_
      apply
        IndepFun.integrable_mul _ (Memℒp.integrable one_le_two (hs _ (mem_insert_self _ _)))
          (Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi)))
      apply h (mem_insert_self _ _) (mem_insert_of_mem hi)
      exact fun hki => ks (hki.symm ▸ hi)
  _ = Var[X k] + Var[∑ i in s, X i] + (𝔼[2 * X k * ∑ i in s, X i] - 2 * 𝔼[X k] * 𝔼[∑ i in s, X i]) :=
    by
    rw [variance_def' (hs _ (mem_insert_self _ _)),
      variance_def' (memℒp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi))]
    ring
  _ = Var[X k] + Var[∑ i in s, X i] :=
    by
    simp only [mul_assoc, integral_mul_left, Pi.mul_apply, Pi.one_apply, sum_apply, add_right_eq_self, mul_sum]
    rw [integral_finset_sum s fun i hi => ?_]; swap
    · apply Integrable.const_mul _ (2 : ℝ)
      apply
        IndepFun.integrable_mul _ (Memℒp.integrable one_le_two (hs _ (mem_insert_self _ _)))
          (Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi)))
      apply h (mem_insert_self _ _) (mem_insert_of_mem hi)
      exact fun hki => ks (hki.symm ▸ hi)
    rw [integral_finset_sum s fun i hi => Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi)), mul_sum, mul_sum, ←
      sum_sub_distrib]
    apply Finset.sum_eq_zero fun i hi => ?_
    have : ∀ (a : Ω), @OfNat.ofNat (Ω → ℝ) 2 instOfNat a = (2 : ℝ) := fun a => rfl
    conv_lhs => enter [1, 2, a]; rw [this]
    rw [integral_mul_left, IndepFun.integral_mul', sub_self]
    · apply h (mem_insert_self _ _) (mem_insert_of_mem hi)
      exact fun hki => ks (hki.symm ▸ hi)
    · exact Memℒp.aestronglyMeasurable (hs _ (mem_insert_self _ _))
    · exact Memℒp.aestronglyMeasurable (hs _ (mem_insert_of_mem hi))
  _ = Var[X k] + ∑ i in s, Var[X i] := by
    rw [IH (fun i hi => hs i (mem_insert_of_mem hi)) (h.mono (by simp only [coe_insert, Set.subset_insert]))]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ (i : ι), i ∈ s → Memℒp (X i) 2
h : Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)
⊢ variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
[PROOFSTEP]
induction' s using Finset.induction_on with k s ks IH
[GOAL]
case empty
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
hs✝ : ∀ (i : ι), i ∈ s → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)
hs : ∀ (i : ι), i ∈ ∅ → Memℒp (X i) 2
h : Set.Pairwise ↑∅ fun i j => IndepFun (X i) (X j)
⊢ variance (∑ i in ∅, X i) ℙ = ∑ i in ∅, variance (X i) ℙ
[PROOFSTEP]
simp only [Finset.sum_empty, variance_zero]
[GOAL]
case insert
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ variance (∑ i in insert k s, X i) ℙ = ∑ i in insert k s, variance (X i) ℙ
[PROOFSTEP]
rw [variance_def' (memℒp_finset_sum' _ hs), sum_insert ks, sum_insert ks]
[GOAL]
case insert
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ (∫ (a : Ω), ((X k + ∑ x in s, X x) ^ 2) a) - (∫ (a : Ω), (X k + ∑ x in s, X x) a) ^ 2 =
    variance (X k) ℙ + ∑ x in s, variance (X x) ℙ
[PROOFSTEP]
simp only [add_sq']
[GOAL]
case insert
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ (∫ (a : Ω), (X k ^ 2 + (∑ x in s, X x) ^ 2 + 2 * X k * ∑ x in s, X x) a) - (∫ (a : Ω), (X k + ∑ x in s, X x) a) ^ 2 =
    variance (X k) ℙ + ∑ x in s, variance (X x) ℙ
[PROOFSTEP]
calc
  𝔼[X k ^ 2 + (∑ i in s, X i) ^ 2 + 2 * X k * ∑ i in s, X i] - 𝔼[X k + ∑ i in s, X i] ^ 2 =
      𝔼[X k ^ 2] + 𝔼[(∑ i in s, X i) ^ 2] + 𝔼[2 * X k * ∑ i in s, X i] - (𝔼[X k] + 𝔼[∑ i in s, X i]) ^ 2 :=
    by
    rw [integral_add', integral_add', integral_add']
    · exact Memℒp.integrable one_le_two (hs _ (mem_insert_self _ _))
    · apply integrable_finset_sum' _ fun i hi => ?_
      exact Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi))
    · exact Memℒp.integrable_sq (hs _ (mem_insert_self _ _))
    · apply Memℒp.integrable_sq
      exact memℒp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi)
    · apply Integrable.add
      · exact Memℒp.integrable_sq (hs _ (mem_insert_self _ _))
      · apply Memℒp.integrable_sq
        exact memℒp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi)
    · rw [mul_assoc]
      apply Integrable.const_mul _ (2 : ℝ)
      simp only [mul_sum, sum_apply, Pi.mul_apply]
      apply integrable_finset_sum _ fun i hi => ?_
      apply
        IndepFun.integrable_mul _ (Memℒp.integrable one_le_two (hs _ (mem_insert_self _ _)))
          (Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi)))
      apply h (mem_insert_self _ _) (mem_insert_of_mem hi)
      exact fun hki => ks (hki.symm ▸ hi)
  _ = Var[X k] + Var[∑ i in s, X i] + (𝔼[2 * X k * ∑ i in s, X i] - 2 * 𝔼[X k] * 𝔼[∑ i in s, X i]) :=
    by
    rw [variance_def' (hs _ (mem_insert_self _ _)),
      variance_def' (memℒp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi))]
    ring
  _ = Var[X k] + Var[∑ i in s, X i] :=
    by
    simp only [mul_assoc, integral_mul_left, Pi.mul_apply, Pi.one_apply, sum_apply, add_right_eq_self, mul_sum]
    rw [integral_finset_sum s fun i hi => ?_]; swap
    · apply Integrable.const_mul _ (2 : ℝ)
      apply
        IndepFun.integrable_mul _ (Memℒp.integrable one_le_two (hs _ (mem_insert_self _ _)))
          (Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi)))
      apply h (mem_insert_self _ _) (mem_insert_of_mem hi)
      exact fun hki => ks (hki.symm ▸ hi)
    rw [integral_finset_sum s fun i hi => Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi)), mul_sum, mul_sum, ←
      sum_sub_distrib]
    apply Finset.sum_eq_zero fun i hi => ?_
    have : ∀ (a : Ω), @OfNat.ofNat (Ω → ℝ) 2 instOfNat a = (2 : ℝ) := fun a => rfl
    conv_lhs => enter [1, 2, a]; rw [this]
    rw [integral_mul_left, IndepFun.integral_mul', sub_self]
    · apply h (mem_insert_self _ _) (mem_insert_of_mem hi)
      exact fun hki => ks (hki.symm ▸ hi)
    · exact Memℒp.aestronglyMeasurable (hs _ (mem_insert_self _ _))
    · exact Memℒp.aestronglyMeasurable (hs _ (mem_insert_of_mem hi))
  _ = Var[X k] + ∑ i in s, Var[X i] := by
    rw [IH (fun i hi => hs i (mem_insert_of_mem hi)) (h.mono (by simp only [coe_insert, Set.subset_insert]))]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ (∫ (a : Ω), (X k ^ 2 + (∑ i in s, X i) ^ 2 + 2 * X k * ∑ i in s, X i) a) - (∫ (a : Ω), (X k + ∑ i in s, X i) a) ^ 2 =
    (((∫ (a : Ω), (X k ^ 2) a) + ∫ (a : Ω), ((∑ i in s, X i) ^ 2) a) + ∫ (a : Ω), (2 * X k * ∑ i in s, X i) a) -
      ((∫ (a : Ω), X k a) + ∫ (a : Ω), Finset.sum s (fun i => X i) a) ^ 2
[PROOFSTEP]
rw [integral_add', integral_add', integral_add']
[GOAL]
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable (X k)
[PROOFSTEP]
exact Memℒp.integrable one_le_two (hs _ (mem_insert_self _ _))
[GOAL]
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable (∑ i in s, X i)
[PROOFSTEP]
apply integrable_finset_sum' _ fun i hi => ?_
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
⊢ Integrable (X i)
[PROOFSTEP]
exact Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi))
[GOAL]
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable (X k ^ 2)
[PROOFSTEP]
exact Memℒp.integrable_sq (hs _ (mem_insert_self _ _))
[GOAL]
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable ((∑ i in s, X i) ^ 2)
[PROOFSTEP]
apply Memℒp.integrable_sq
[GOAL]
case hg.h
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Memℒp (fun x => Finset.sum s (fun i => X i) x) 2
[PROOFSTEP]
exact memℒp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi)
[GOAL]
case hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable (X k ^ 2 + (∑ i in s, X i) ^ 2)
[PROOFSTEP]
apply Integrable.add
[GOAL]
case hf.hf
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable (X k ^ 2)
[PROOFSTEP]
exact Memℒp.integrable_sq (hs _ (mem_insert_self _ _))
[GOAL]
case hf.hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable ((∑ i in s, X i) ^ 2)
[PROOFSTEP]
apply Memℒp.integrable_sq
[GOAL]
case hf.hg.h
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Memℒp (fun x => Finset.sum s (fun i => X i) x) 2
[PROOFSTEP]
exact memℒp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi)
[GOAL]
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable (2 * X k * ∑ i in s, X i)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case hg
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable (2 * (X k * ∑ i in s, X i))
[PROOFSTEP]
apply Integrable.const_mul _ (2 : ℝ)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable fun x => (X k * ∑ i in s, X i) x
[PROOFSTEP]
simp only [mul_sum, sum_apply, Pi.mul_apply]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ Integrable fun x => ∑ x_1 in s, X k x * X x_1 x
[PROOFSTEP]
apply integrable_finset_sum _ fun i hi => ?_
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
⊢ Integrable fun a => X k a * X i a
[PROOFSTEP]
apply
  IndepFun.integrable_mul _ (Memℒp.integrable one_le_two (hs _ (mem_insert_self _ _)))
    (Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi)))
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
⊢ IndepFun (X k) (X i)
[PROOFSTEP]
apply h (mem_insert_self _ _) (mem_insert_of_mem hi)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
⊢ k ≠ i
[PROOFSTEP]
exact fun hki => ks (hki.symm ▸ hi)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ (((∫ (a : Ω), (X k ^ 2) a) + ∫ (a : Ω), ((∑ i in s, X i) ^ 2) a) + ∫ (a : Ω), (2 * X k * ∑ i in s, X i) a) -
      ((∫ (a : Ω), X k a) + ∫ (a : Ω), Finset.sum s (fun i => X i) a) ^ 2 =
    variance (X k) ℙ + variance (∑ i in s, X i) ℙ +
      ((∫ (a : Ω), (2 * X k * ∑ i in s, X i) a) - (2 * ∫ (a : Ω), X k a) * ∫ (a : Ω), Finset.sum s (fun i => X i) a)
[PROOFSTEP]
rw [variance_def' (hs _ (mem_insert_self _ _)),
  variance_def' (memℒp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi))]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ (((∫ (a : Ω), (X k ^ 2) a) + ∫ (a : Ω), ((∑ i in s, X i) ^ 2) a) + ∫ (a : Ω), (2 * X k * ∑ i in s, X i) a) -
      ((∫ (a : Ω), X k a) + ∫ (a : Ω), Finset.sum s (fun i => X i) a) ^ 2 =
    (∫ (a : Ω), (X k ^ 2) a) - (∫ (a : Ω), X k a) ^ 2 +
        ((∫ (a : Ω), ((∑ i in s, X i) ^ 2) a) - (∫ (a : Ω), Finset.sum s (fun i => X i) a) ^ 2) +
      ((∫ (a : Ω), (2 * X k * ∑ i in s, X i) a) - (2 * ∫ (a : Ω), X k a) * ∫ (a : Ω), Finset.sum s (fun i => X i) a)
[PROOFSTEP]
ring
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ variance (X k) ℙ + variance (∑ i in s, X i) ℙ +
      ((∫ (a : Ω), (2 * X k * ∑ i in s, X i) a) - (2 * ∫ (a : Ω), X k a) * ∫ (a : Ω), Finset.sum s (fun i => X i) a) =
    variance (X k) ℙ + variance (∑ i in s, X i) ℙ
[PROOFSTEP]
simp only [mul_assoc, integral_mul_left, Pi.mul_apply, Pi.one_apply, sum_apply, add_right_eq_self, mul_sum]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ (∫ (a : Ω), ∑ x in s, OfNat.ofNat 2 a * (X k a * X x a)) - 2 * ((∫ (a : Ω), X k a) * ∫ (a : Ω), ∑ c in s, X c a) = 0
[PROOFSTEP]
rw [integral_finset_sum s fun i hi => ?_]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ (∑ i in s, ∫ (a : Ω), OfNat.ofNat 2 a * (X k a * X i a)) - 2 * ((∫ (a : Ω), X k a) * ∫ (a : Ω), ∑ c in s, X c a) = 0
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
⊢ Integrable fun a => OfNat.ofNat 2 a * (X k a * X i a)
[PROOFSTEP]
swap
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
⊢ Integrable fun a => OfNat.ofNat 2 a * (X k a * X i a)
[PROOFSTEP]
apply Integrable.const_mul _ (2 : ℝ)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
⊢ Integrable fun x => X k x * X i x
[PROOFSTEP]
apply
  IndepFun.integrable_mul _ (Memℒp.integrable one_le_two (hs _ (mem_insert_self _ _)))
    (Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi)))
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
⊢ IndepFun (X k) (X i)
[PROOFSTEP]
apply h (mem_insert_self _ _) (mem_insert_of_mem hi)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
⊢ k ≠ i
[PROOFSTEP]
exact fun hki => ks (hki.symm ▸ hi)
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ (∑ i in s, ∫ (a : Ω), OfNat.ofNat 2 a * (X k a * X i a)) - 2 * ((∫ (a : Ω), X k a) * ∫ (a : Ω), ∑ c in s, X c a) = 0
[PROOFSTEP]
rw [integral_finset_sum s fun i hi => Memℒp.integrable one_le_two (hs _ (mem_insert_of_mem hi)), mul_sum, mul_sum, ←
  sum_sub_distrib]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ ∑ x in s, ((∫ (a : Ω), OfNat.ofNat 2 a * (X k a * X x a)) - 2 * ((∫ (a : Ω), X k a) * ∫ (a : Ω), X x a)) = 0
[PROOFSTEP]
apply Finset.sum_eq_zero fun i hi => ?_
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
⊢ (∫ (a : Ω), OfNat.ofNat 2 a * (X k a * X i a)) - 2 * ((∫ (a : Ω), X k a) * ∫ (a : Ω), X i a) = 0
[PROOFSTEP]
have : ∀ (a : Ω), @OfNat.ofNat (Ω → ℝ) 2 instOfNat a = (2 : ℝ) := fun a => rfl
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
this : ∀ (a : Ω), OfNat.ofNat 2 a = 2
⊢ (∫ (a : Ω), OfNat.ofNat 2 a * (X k a * X i a)) - 2 * ((∫ (a : Ω), X k a) * ∫ (a : Ω), X i a) = 0
[PROOFSTEP]
conv_lhs => enter [1, 2, a]; rw [this]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
this : ∀ (a : Ω), OfNat.ofNat 2 a = 2
| (∫ (a : Ω), OfNat.ofNat 2 a * (X k a * X i a)) - 2 * ((∫ (a : Ω), X k a) * ∫ (a : Ω), X i a)
[PROOFSTEP]
enter [1, 2, a]; rw [this]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
this : ∀ (a : Ω), OfNat.ofNat 2 a = 2
| (∫ (a : Ω), OfNat.ofNat 2 a * (X k a * X i a)) - 2 * ((∫ (a : Ω), X k a) * ∫ (a : Ω), X i a)
[PROOFSTEP]
enter [1, 2, a]; rw [this]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
this : ∀ (a : Ω), OfNat.ofNat 2 a = 2
| (∫ (a : Ω), OfNat.ofNat 2 a * (X k a * X i a)) - 2 * ((∫ (a : Ω), X k a) * ∫ (a : Ω), X i a)
[PROOFSTEP]
enter [1, 2, a]
[GOAL]
case h
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
this : ∀ (a : Ω), OfNat.ofNat 2 a = 2
a : Ω
| OfNat.ofNat 2 a * (X k a * X i a)
[PROOFSTEP]
rw [this]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
this : ∀ (a : Ω), OfNat.ofNat 2 a = 2
⊢ (∫ (a : Ω), 2 * (X k a * X i a)) - 2 * ((∫ (a : Ω), X k a) * ∫ (a : Ω), X i a) = 0
[PROOFSTEP]
rw [integral_mul_left, IndepFun.integral_mul', sub_self]
[GOAL]
case hXY
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
this : ∀ (a : Ω), OfNat.ofNat 2 a = 2
⊢ IndepFun (fun a => X k a) fun a => X i a
[PROOFSTEP]
apply h (mem_insert_self _ _) (mem_insert_of_mem hi)
[GOAL]
case hXY
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
this : ∀ (a : Ω), OfNat.ofNat 2 a = 2
⊢ k ≠ i
[PROOFSTEP]
exact fun hki => ks (hki.symm ▸ hi)
[GOAL]
case hX
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
this : ∀ (a : Ω), OfNat.ofNat 2 a = 2
⊢ AEStronglyMeasurable (fun a => X k a) ℙ
[PROOFSTEP]
exact Memℒp.aestronglyMeasurable (hs _ (mem_insert_self _ _))
[GOAL]
case hY
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
i : ι
hi : i ∈ s
this : ∀ (a : Ω), OfNat.ofNat 2 a = 2
⊢ AEStronglyMeasurable (fun a => X i a) ℙ
[PROOFSTEP]
exact Memℒp.aestronglyMeasurable (hs _ (mem_insert_of_mem hi))
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ variance (X k) ℙ + variance (∑ i in s, X i) ℙ = variance (X k) ℙ + ∑ i in s, variance (X i) ℙ
[PROOFSTEP]
rw [IH (fun i hi => hs i (mem_insert_of_mem hi)) (h.mono (by simp only [coe_insert, Set.subset_insert]))]
[GOAL]
Ω : Type u_1
m : MeasurableSpace Ω
X✝ : Ω → ℝ
μ : Measure Ω
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
hs✝ : ∀ (i : ι), i ∈ s✝ → Memℒp (X i) 2
h✝ : Set.Pairwise ↑s✝ fun i j => IndepFun (X i) (X j)
k : ι
s : Finset ι
ks : ¬k ∈ s
IH :
  (∀ (i : ι), i ∈ s → Memℒp (X i) 2) →
    (Set.Pairwise ↑s fun i j => IndepFun (X i) (X j)) → variance (∑ i in s, X i) ℙ = ∑ i in s, variance (X i) ℙ
hs : ∀ (i : ι), i ∈ insert k s → Memℒp (X i) 2
h : Set.Pairwise ↑(insert k s) fun i j => IndepFun (X i) (X j)
⊢ ↑s ⊆ ↑(insert k s)
[PROOFSTEP]
simp only [coe_insert, Set.subset_insert]