-- Mathlib/Probability/CondVar.lean
lemma condVar_ae_eq_condExp_sq_sub_sq_condExp (hm : m ≤ m₀) [IsFiniteMeasure μ] (hX : MemLp X 2 μ) :
    Var[X; μ | m] =ᵐ[μ] μ[X ^ 2 | m] - μ[X | m] ^ 2

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[X ^ 2|m] - μ[X|m] ^ 2

Tactic:
calc
  Var[X; μ | m]
  _ = μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] := by rw [condVar, sub_sq]
  _ =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2 := by
    have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq
    have aux₁ : Integrable (2 * X * μ[X | m]) μ := by
      rw [mul_assoc]
      exact (memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _
    have aux₂ : Integrable (μ[X | m] ^ 2) μ := hX.condExp.integrable_sq
    filter_upwards [condExp_add (m := m) (aux₀.sub aux₁) aux₂, condExp_sub (m := m) aux₀ aux₁,
      condExp_mul_of_stronglyMeasurable_right stronglyMeasurable_condExp aux₁
        ((hX.integrable one_le_two).const_mul _), condExp_ofNat (m := m) 2 X]
      with ω hω₀ hω₁ hω₂ hω₃
    simp [hω₀, hω₁, hω₂, hω₃, condExp_const,
      condExp_of_stronglyMeasurable hm (stronglyMeasurable_condExp.pow _) aux₂]
    simp [mul_assoc, sq]
  _ = μ[X ^ 2 | m] - μ[X | m] ^ 2 := by ring

Result:
no goals

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m] =ᶠ[ae μ] μ[X ^ 2|m] - 2 * μ[X|m] ^ 2 + μ[X|m] ^ 2

Tactic:
have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq

Result:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
⊢ μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m] =ᶠ[ae μ] μ[X ^ 2|m] - 2 * μ[X|m] ^ 2 + μ[X|m] ^ 2

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X|m]) μ
⊢ μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m] =ᶠ[ae μ] μ[X ^ 2|m] - 2 * μ[X|m] ^ 2 + μ[X|m] ^ 2

Tactic:
have aux₂ : Integrable (μ[X | m] ^ 2) μ := hX.condExp.integrable_sq

Result:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X|m]) μ
aux₂ : Integrable (μ[X|m] ^ 2) μ
⊢ μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m] =ᶠ[ae μ] μ[X ^ 2|m] - 2 * μ[X|m] ^ 2 + μ[X|m] ^ 2

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
⊢ Integrable (2 * (X * μ[X|m])) μ

Tactic:
exact (memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _

Result:
no goals

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X|m]) μ
aux₂ : Integrable (μ[X|m] ^ 2) μ
⊢ μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m] =ᶠ[ae μ] μ[X ^ 2|m] - 2 * μ[X|m] ^ 2 + μ[X|m] ^ 2

Tactic:
filter_upwards [condExp_add (m := m) (aux₀.sub aux₁) aux₂, condExp_sub (m := m) aux₀ aux₁,
  condExp_mul_of_stronglyMeasurable_right stronglyMeasurable_condExp aux₁
    ((hX.integrable one_le_two).const_mul _), condExp_ofNat (m := m) 2 X]
  with ω hω₀ hω₁ hω₂ hω₃

Result:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X|m]) μ
aux₂ : Integrable (μ[X|m] ^ 2) μ
ω : Ω
hω₀ : (μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m]) ω = (μ[X ^ 2 - 2 * X * μ[X|m]|m] + μ[μ[X|m] ^ 2|m]) ω
hω₁ : (μ[X ^ 2 - 2 * X * μ[X|m]|m]) ω = (μ[X ^ 2|m] - μ[2 * X * μ[X|m]|m]) ω
hω₂ : (μ[2 * X * μ[X|m]|m]) ω = (μ[2 * X|m] * μ[X|m]) ω
hω₃ : (μ[OfNat.ofNat 2 * X|m]) ω = (OfNat.ofNat 2 * μ[X|m]) ω
⊢ (μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m]) ω = (μ[X ^ 2|m] - 2 * μ[X|m] ^ 2 + μ[X|m] ^ 2) ω

Proof state:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X|m]) μ
aux₂ : Integrable (μ[X|m] ^ 2) μ
ω : Ω
hω₀ : (μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m]) ω = (μ[X ^ 2 - 2 * X * μ[X|m]|m] + μ[μ[X|m] ^ 2|m]) ω
hω₁ : (μ[X ^ 2 - 2 * X * μ[X|m]|m]) ω = (μ[X ^ 2|m] - μ[2 * X * μ[X|m]|m]) ω
hω₂ : (μ[2 * X * μ[X|m]|m]) ω = (μ[2 * X|m] * μ[X|m]) ω
hω₃ : (μ[OfNat.ofNat 2 * X|m]) ω = (OfNat.ofNat 2 * μ[X|m]) ω
⊢ 2 * (μ[X|m]) ω * (μ[X|m]) ω = 2 * (μ[X|m]) ω ^ 2

Tactic:
simp [mul_assoc, sq]

Result:
no goals

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
⊢ Integrable (2 * X * μ[X|m]) μ

Tactic:
rw [mul_assoc]

Result:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
⊢ Integrable (2 * (X * μ[X|m])) μ

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
⊢ μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m] =ᶠ[ae μ] μ[X ^ 2|m] - 2 * μ[X|m] ^ 2 + μ[X|m] ^ 2

Tactic:
have aux₁ : Integrable (2 * X * μ[X | m]) μ := by
  rw [mul_assoc]
  exact (memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _

Result:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X|m]) μ
⊢ μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m] =ᶠ[ae μ] μ[X ^ 2|m] - 2 * μ[X|m] ^ 2 + μ[X|m] ^ 2

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ μ[X ^ 2|m] - 2 * μ[X|m] ^ 2 + μ[X|m] ^ 2 = μ[X ^ 2|m] - μ[X|m] ^ 2

Tactic:
ring

Result:
no goals

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ Var[X; μ | m] = μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m]

Tactic:
rw [condVar, sub_sq]

Result:
no goals

Proof state:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X|m]) μ
aux₂ : Integrable (μ[X|m] ^ 2) μ
ω : Ω
hω₀ : (μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m]) ω = (μ[X ^ 2 - 2 * X * μ[X|m]|m] + μ[μ[X|m] ^ 2|m]) ω
hω₁ : (μ[X ^ 2 - 2 * X * μ[X|m]|m]) ω = (μ[X ^ 2|m] - μ[2 * X * μ[X|m]|m]) ω
hω₂ : (μ[2 * X * μ[X|m]|m]) ω = (μ[2 * X|m] * μ[X|m]) ω
hω₃ : (μ[OfNat.ofNat 2 * X|m]) ω = (OfNat.ofNat 2 * μ[X|m]) ω
⊢ (μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m]) ω = (μ[X ^ 2|m] - 2 * μ[X|m] ^ 2 + μ[X|m] ^ 2) ω

Tactic:
simp [hω₀, hω₁, hω₂, hω₃, condExp_const,
  condExp_of_stronglyMeasurable hm (stronglyMeasurable_condExp.pow _) aux₂]

Result:
case h
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X|m]) μ
aux₂ : Integrable (μ[X|m] ^ 2) μ
ω : Ω
hω₀ : (μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2|m]) ω = (μ[X ^ 2 - 2 * X * μ[X|m]|m] + μ[μ[X|m] ^ 2|m]) ω
hω₁ : (μ[X ^ 2 - 2 * X * μ[X|m]|m]) ω = (μ[X ^ 2|m] - μ[2 * X * μ[X|m]|m]) ω
hω₂ : (μ[2 * X * μ[X|m]|m]) ω = (μ[2 * X|m] * μ[X|m]) ω
hω₃ : (μ[OfNat.ofNat 2 * X|m]) ω = (OfNat.ofNat 2 * μ[X|m]) ω
⊢ 2 * (μ[X|m]) ω * (μ[X|m]) ω = 2 * (μ[X|m]) ω ^ 2