centralMoment_one' — Mathlib

English

If X is integrable with respect to μ and μ is finite, then the second central moment equals the variance of X with respect to μ: centralMoment X 2 μ = variance X μ.

Русский

Если X интегрируема по μ и μ конечна, то второй центральный момент равен дисперсии: centralMoment X 2 μ = variance X μ.

LaTeX

$$centralMoment(X,2,μ) = variance(X,μ)$$

Lean4

theorem centralMoment_one' [IsFiniteMeasure μ] (h_int : Integrable X μ) :
    centralMoment X 1 μ = (1 - μ.real Set.univ) * μ[X] :=
  by
  simp only [centralMoment, Pi.sub_apply, pow_one]
  rw [integral_sub h_int (integrable_const _)]
  simp only [sub_mul, integral_const, smul_eq_mul, one_mul]

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