-- Mathlib/Probability/CondVar.lean
/-- **Law of total variance** -/
lemma integral_condVar_add_variance_condExp (hm : m ≤ m₀) [IsProbabilityMeasure μ]
    (hX : MemLp X 2 μ) : μ[Var[X; μ | m]] + Var[μ[X | m]; μ] = Var[X; μ]

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ + (∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2) =
    Var[X; μ]

Tactic:
rw [variance_def' hX]

Result:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ + (∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Proof state:
case e_a
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Var[μ[X|m]; μ] = ∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ - (∫ (x : Ω), (μ[X|m]) x ∂μ) ^ 2

Tactic:
exact variance_def' hX.condExp

Result:
no goals

Proof state:
case e_a
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ = ∫ (x : Ω), (μ[X ^ 2|m] - μ[X|m] ^ 2) x ∂μ

Tactic:
exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX

Result:
no goals

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (μ[X ^ 2|m] - μ[X|m] ^ 2) x ∂μ + (∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ - (∫ (x : Ω), (μ[X|m]) x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ + (∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]

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

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

Tactic:
exact hX.condExp.integrable_sq

Result:
no goals

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X|m]; μ] =
    ∫ (x : Ω), (μ[X ^ 2|m] - μ[X|m] ^ 2) x ∂μ + (∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ - (∫ (x : Ω), (μ[X|m]) x ∂μ) ^ 2)

Tactic:
congr 1

Result:
case e_a
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ = ∫ (x : Ω), (μ[X ^ 2|m] - μ[X|m] ^ 2) x ∂μ

case e_a
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Var[μ[X|m]; μ] = ∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ - (∫ (x : Ω), (μ[X|m]) x ∂μ) ^ 2

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ + (∫ (x : Ω), (μ[X|m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
ring

Result:
no goals