-- Mathlib/Probability/Variance.lean
theorem evariance_eq_top [IsFiniteMeasure μ] (hXm : AEStronglyMeasurable X μ) (hX : ¬MemLp X 2 μ) :
    evariance X μ = ∞

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
⊢ False

Tactic:
have : MemLp (fun ω => X ω - μ[X]) 2 μ := by
  refine ⟨hXm.sub aestronglyMeasurable_const, ?_⟩
  rw [eLpNorm_eq_lintegral_rpow_enorm two_ne_zero ENNReal.ofNat_ne_top]
  simp only [ENNReal.toReal_ofNat, ENNReal.one_toReal, ENNReal.rpow_two, Ne]
  exact ENNReal.rpow_lt_top_of_nonneg (by linarith) h.ne

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
this : MemLp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ False

Proof state:
case h.e'_6.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
this : MemLp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ
ω : Ω
⊢ X ω = ((fun ω => X ω - ∫ (x : Ω), X x ∂μ) + fun x => ∫ (x : Ω), X x ∂μ) ω

Tactic:
rw [Pi.add_apply, sub_add_cancel]

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
⊢ (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2) < ⊤

Tactic:
simp only [ENNReal.toReal_ofNat, ENNReal.one_toReal, ENNReal.rpow_two, Ne]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
⊢ (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ (1 / 2) < ⊤

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
this : MemLp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ MemLp X 2 μ

Tactic:
convert this.add (memLp_const μ[X])

Result:
case h.e'_6
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
this : MemLp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ X = (fun ω => X ω - ∫ (x : Ω), X x ∂μ) + fun x => ∫ (x : Ω), X x ∂μ

Proof state:
case h.e'_6
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
this : MemLp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ X = (fun ω => X ω - ∫ (x : Ω), X x ∂μ) + fun x => ∫ (x : Ω), X x ∂μ

Tactic:
ext ω

Result:
case h.e'_6.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
this : MemLp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ
ω : Ω
⊢ X ω = ((fun ω => X ω - ∫ (x : Ω), X x ∂μ) + fun x => ∫ (x : Ω), X x ∂μ) ω

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
⊢ (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ (1 / 2) < ⊤

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg (by linarith) h.ne

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
⊢ eLpNorm (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ < ⊤

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm two_ne_zero ENNReal.ofNat_ne_top]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
⊢ (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2) < ⊤

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
⊢ 0 ≤ 1 / 2

Tactic:
linarith

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ eVar[X; μ] = ⊤

Tactic:
by_contra h

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : ¬eVar[X; μ] = ⊤
⊢ False

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
this : MemLp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ False

Tactic:
refine hX ?_

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
this : MemLp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ MemLp X 2 μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
⊢ MemLp (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ

Tactic:
refine ⟨hXm.sub aestronglyMeasurable_const, ?_⟩

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
⊢ eLpNorm (fun ω => X ω - ∫ (x : Ω), X x ∂μ) 2 μ < ⊤

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : ¬eVar[X; μ] = ⊤
⊢ False

Tactic:
rw [← Ne, ← lt_top_iff_ne_top] at h

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ⊤
⊢ False