English
Equality between evariance and a lintegral form; the exact formula expresses evariance as integral of squared centered variable.
Русский
Эквивалентность evariance и линтеграла: evariance X μ = ∫⁻ (X−E[X])^2 dμ.
LaTeX
$$evariance X μ = ∫⁻ ω, ENNReal.ofReal ((X(ω) - μ[X])^2) ∂μ$$
Lean4
theorem evariance_eq_top [IsFiniteMeasure μ] (hXm : AEStronglyMeasurable X μ) (hX : ¬MemLp X 2 μ) : evariance X μ = ∞ :=
by
by_contra h
rw [← Ne, ← lt_top_iff_ne_top] at h
have : MemLp (fun ω => X ω - μ[X]) 2 μ := by
refine ⟨by fun_prop, ?_⟩
rw [eLpNorm_eq_lintegral_rpow_enorm two_ne_zero ENNReal.ofNat_ne_top]
simp only [ENNReal.toReal_ofNat, ENNReal.rpow_two]
exact ENNReal.rpow_lt_top_of_nonneg (by linarith) h.ne
refine hX ?_
convert this.add (memLp_const μ[X])
ext ω
rw [Pi.add_apply, sub_add_cancel]
