-- Mathlib/Probability/Variance.lean
theorem evariance_def' [IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : AEStronglyMeasurable X μ) :
    evariance X μ = (∫⁻ ω, ‖X ω‖ₑ ^ 2 ∂μ) - ENNReal.ofReal (μ[X] ^ 2)

Proof state:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ⊤ ∧ ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2) ≠ ⊤

Tactic:
refine ⟨?_, ENNReal.ofReal_ne_top⟩

Result:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ⊤

Proof state:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬eLpNorm X 2 μ < ⊤
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ⊤

Tactic:
simp only [eLpNorm_eq_lintegral_rpow_enorm two_ne_zero ENNReal.ofNat_ne_top, not_lt, top_le_iff,
  ENNReal.toReal_ofNat, one_div, ENNReal.rpow_eq_top_iff, inv_lt_zero, inv_pos, and_true,
  or_iff_not_imp_left, not_and_or, zero_lt_two] at hℒ

Result:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : (¬¬∫⁻ (x : Ω), ‖X x‖ₑ ^ 2 ∂μ = 0 → 0 ≤ 2) → ∫⁻ (x : Ω), ‖X x‖ₑ ^ 2 ∂μ = ⊤
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ⊤

Proof state:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ⊤

Tactic:
rw [MemLp, not_and] at hℒ

Result:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : AEStronglyMeasurable X μ → ¬eLpNorm X 2 μ < ⊤
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ⊤

Proof state:
case pos.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ

Tactic:
simp_rw [← enorm_pow, enorm]

Result:
case pos.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) = ∫⁻ (ω : Ω), ↑‖X ω ^ 2‖₊ ∂μ

Proof state:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2) = eVar[X; μ]

Tactic:
rw [evariance_eq_top hX hℒ, ENNReal.sub_eq_top_iff]

Result:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ⊤ ∧ ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2) ≠ ⊤

Proof state:
case pos.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) = ∫⁻ (ω : Ω), ↑‖X ω ^ 2‖₊ ∂μ

Tactic:
rw [lintegral_coe_eq_integral]

Result:
case pos.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) = ENNReal.ofReal (∫ (a : Ω), ↑‖X a ^ 2‖₊ ∂μ)

case pos.e_a.hfi
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ Integrable (fun x => ↑‖X x ^ 2‖₊) μ

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
rw [← ofReal_variance hℒ, variance_def' hℒ, ENNReal.ofReal_sub _ (sq_nonneg _)]

Result:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2) =
    ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

Proof state:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : (¬¬∫⁻ (x : Ω), ‖X x‖ₑ ^ 2 ∂μ = 0 → 0 ≤ 2) → ∫⁻ (x : Ω), ‖X x‖ₑ ^ 2 ∂μ = ⊤
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ⊤

Tactic:
exact mod_cast hℒ fun _ => zero_le_two

Result:
no goals

Proof state:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : AEStronglyMeasurable X μ → ¬eLpNorm X 2 μ < ⊤
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ⊤

Tactic:
specialize hℒ hX

Result:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬eLpNorm X 2 μ < ⊤
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ = ⊤

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
by_cases hℒ : MemLp X 2 μ

Result:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

Proof state:
case pos.e_a.hfi
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ Integrable (fun x => ↑‖X x ^ 2‖₊) μ

Tactic:
simpa using hℒ.abs.integrable_sq

Result:
no goals

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2) =
    ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
congr

Result:
case pos.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ

Proof state:
case pos.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) = ENNReal.ofReal (∫ (a : Ω), ↑‖X a ^ 2‖₊ ∂μ)

Tactic:
simp

Result:
no goals

Proof state:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
symm

Result:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2) = eVar[X; μ]