variance_eq_integral — Mathlib

English

If X is AEMeasurable, the variance equals the integral of (X − μ[X])^2 with respect to μ.

Русский

Если X измеримо по AE, дисперсия равна интегралу от (X − E[X])^2 по μ.

LaTeX

$$Var[X; μ] = ∫ ω (X(ω) - μ[X])^2 ∂μ$$

Lean4

theorem variance_eq_integral (hX : AEMeasurable X μ) : Var[X; μ] = ∫ ω, (X ω - μ[X]) ^ 2 ∂μ := by
  simp [variance, evariance, toReal_enorm,
    ← integral_toReal ((hX.sub_const _).enorm.pow_const _) <| .of_forall fun _ ↦ ENNReal.pow_lt_top enorm_lt_top]

Похожие утверждения