moment — Mathlib

English

For a real-valued random variable X and a natural p, the p-th moment is the integral of X^p with respect to μ, i.e., μ[X^p].

Русский

Для действительной случайной величины X и натурального p момент порядка p равен интегралу X^p по μ, т.е. μ[X^p].

LaTeX

$$moment\left(X,p,\mu\right) = \int_{\Omega} X(\omega)^{p} \, d\mu(\omega)$$

Lean4

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

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