-- Mathlib/Probability/Variance.lean
theorem variance_le_expectation_sq [IsProbabilityMeasure μ] {X : Ω → ℝ}
    (hm : AEStronglyMeasurable X μ) : variance X μ ≤ μ[X ^ 2]

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (fun a => (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ
A : MemLp (X - fun ω => ∫ (x : Ω), X x ∂μ) 2 μ
B : MemLp (fun x => ∫ (x : Ω), X x ∂μ) 2 μ
⊢ MemLp X 2 μ

Tactic:
convert A.add B

Result:
case h.e'_6
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (fun a => (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ
A : MemLp (X - fun ω => ∫ (x : Ω), X x ∂μ) 2 μ
B : MemLp (fun x => ∫ (x : Ω), X x ∂μ) 2 μ
⊢ X = (X - fun ω => ∫ (x : Ω), X x ∂μ) + fun x => ∫ (x : Ω), X x ∂μ

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

Tactic:
by_cases hX : MemLp X 2 μ

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

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

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (fun a => (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ
A : MemLp (X - fun ω => ∫ (x : Ω), X x ∂μ) 2 μ
⊢ False

Tactic:
have B : MemLp (fun _ : Ω => μ[X]) 2 μ := memLp_const _

Result:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (fun a => (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ
A : MemLp (X - fun ω => ∫ (x : Ω), X x ∂μ) 2 μ
B : MemLp (fun x => ∫ (x : Ω), X x ∂μ) 2 μ
⊢ False

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

Tactic:
rw [integral_undef]

Result:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ 0 ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

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

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2 ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

Tactic:
simp only [sq_nonneg, sub_le_self_iff]

Result:
no goals