centralMoment — Mathlib

English

The central moment of X of order p is μ[(X − μ[X])^p], i.e., the p-th moment of X around its mean μ[X].

Русский

Центральный момент X порядка p равен μ[(X − μ[X])^p], т.е. момент порядка p вокруг среднего μ[X].

LaTeX

$$centralMoment(X,p,μ) = \int_{\Omega} (X(\omega) - μ[X])^{p} \, dμ(\omega)$$

Lean4

/-- Central moment of a real random variable, `μ[(X - μ[X]) ^ p]`. -/
def centralMoment (X : Ω → ℝ) (p : ℕ) (μ : Measure Ω) : ℝ :=
  μ[(X - fun (_ : Ω) => μ[X]) ^ p]

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