English
For a probability measure μ and an AEStronglyMeasurable X, the extended variance evariance equals the second moment minus the square of the mean, when finite; otherwise it is top (infinite).
Русский
Для вероятностной меры μ и AEV-измеримой X eVariance равна \int|X|^2 dμ минус (E[X])^2, если это конечно; иначе бесконечность.
LaTeX
$$$\mathrm{evariance}[X;\, \mu] = \int |X|^{2} \, d\mu - \mathrm{ofReal}(\mu[X]^{2})$ (при принадлежности X к L^2; в противном случае верхняя граница)$$
Lean4
theorem evariance_def' [IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : AEStronglyMeasurable X μ) :
evariance X μ = (∫⁻ ω, ‖X ω‖ₑ ^ 2 ∂μ) - ENNReal.ofReal (μ[X] ^ 2) :=
by
by_cases hℒ : MemLp X 2 μ
· rw [← ofReal_variance hℒ, variance_eq_sub hℒ, ENNReal.ofReal_sub _ (sq_nonneg _)]
congr
simp_rw [← enorm_pow, enorm]
rw [lintegral_coe_eq_integral]
· simp
· simpa using hℒ.abs.integrable_sq
· symm
rw [evariance_eq_top hX hℒ, ENNReal.sub_eq_top_iff]
refine ⟨?_, ENNReal.ofReal_ne_top⟩
rw [MemLp, not_and] at hℒ
specialize hℒ hX
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ℒ
exact mod_cast hℒ fun _ => zero_le_two
