-- Mathlib/Probability/Variance.lean
theorem variance_def' [IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : MemLp X 2 μ) :
    variance X μ = μ[X ^ 2] - μ[X] ^ 2

Proof state:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun ω => 2 * X ω * ∫ (x : Ω), X x ∂μ) μ

Tactic:
exact ((hX.integrable one_le_two).const_mul 2).mul_const' _

Result:
no goals

Proof state:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun ω => (∫ (x : Ω), X x ∂μ) ^ 2) μ

Tactic:
apply integrable_const

Result:
no goals

Proof state:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun ω => X ω ^ 2 + (∫ (x : Ω), X x ∂μ) ^ 2) μ

Tactic:
apply hX.integrable_sq.add

Result:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun ω => (∫ (x : Ω), X x ∂μ) ^ 2) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ ∫ (a : Ω), X a ^ 2 ∂μ + ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) ^ 2 ∂μ - ∫ (a : Ω), 2 * X a * ∫ (x : Ω), X x ∂μ ∂μ =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
simp only [Pi.pow_apply, integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul,
  Pi.mul_apply, Pi.ofNat_apply, Nat.cast_ofNat, integral_mul_right, integral_mul_left]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ ∫ (a : Ω), X a ^ 2 ∂μ + (∫ (x : Ω), X x ∂μ) ^ 2 - (2 * ∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), X x ∂μ =
    ∫ (x : Ω), X x ^ 2 ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ ∫ (ω : Ω), X ω ^ 2 + (∫ (x : Ω), X x ∂μ) ^ 2 - 2 * X ω * ∫ (x : Ω), X x ∂μ ∂μ =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
rw [integral_sub, integral_add]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ ∫ (a : Ω), X a ^ 2 ∂μ + ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) ^ 2 ∂μ - ∫ (a : Ω), 2 * X a * ∫ (x : Ω), X x ∂μ ∂μ =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun a => X a ^ 2) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun a => (∫ (x : Ω), X x ∂μ) ^ 2) μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun ω => X ω ^ 2 + (∫ (x : Ω), X x ∂μ) ^ 2) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun ω => 2 * X ω * ∫ (x : Ω), X x ∂μ) μ

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

Tactic:
simp only [variance_eq_integral hX.aestronglyMeasurable.aemeasurable, sub_sq']

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ ∫ (ω : Ω), X ω ^ 2 + (∫ (x : Ω), X x ∂μ) ^ 2 - 2 * X ω * ∫ (x : Ω), X x ∂μ ∂μ =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ ∫ (a : Ω), X a ^ 2 ∂μ + (∫ (x : Ω), X x ∂μ) ^ 2 - (2 * ∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), X x ∂μ =
    ∫ (x : Ω), X x ^ 2 ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun a => (∫ (x : Ω), X x ∂μ) ^ 2) μ

Tactic:
apply integrable_const

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ ∫ (a : Ω), X a ^ 2 ∂μ + ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) ^ 2 ∂μ - ∫ (a : Ω), 2 * X a * ∫ (x : Ω), X x ∂μ ∂μ =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun a => X a ^ 2) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun a => (∫ (x : Ω), X x ∂μ) ^ 2) μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun ω => X ω ^ 2 + (∫ (x : Ω), X x ∂μ) ^ 2) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun ω => 2 * X ω * ∫ (x : Ω), X x ∂μ) μ

Tactic:
rotate_left

Result:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun a => X a ^ 2) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun a => (∫ (x : Ω), X x ∂μ) ^ 2) μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun ω => X ω ^ 2 + (∫ (x : Ω), X x ∂μ) ^ 2) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun ω => 2 * X ω * ∫ (x : Ω), X x ∂μ) μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ ∫ (a : Ω), X a ^ 2 ∂μ + ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) ^ 2 ∂μ - ∫ (a : Ω), 2 * X a * ∫ (x : Ω), X x ∂μ ∂μ =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Proof state:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Integrable (fun a => X a ^ 2) μ

Tactic:
exact hX.integrable_sq

Result:
no goals