variance_eq_sub — Mathlib

English

If μ is a probability measure and X has finite second moment, then Var[X; μ] = μ[X^2] − μ[X]^2.

Русский

При мере μ, являющейся вероятностной, и X с конечным вторым моментом, Var[X; μ] = μ[X^2] − (μ[X])^2.

LaTeX

$$$$ \mathrm{variance}(X, \mu) = \mu[X^2] - (\mu[X])^2. $$$$

Lean4

theorem variance_eq_sub [IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : MemLp X 2 μ) : variance X μ = μ[X ^ 2] - μ[X] ^ 2 :=
  by rw [← covariance_self hX.aemeasurable, covariance_eq_sub hX hX, pow_two, pow_two]

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