moment_def

Mathlib.Probability.Moments.Basic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.moment_def

English

The moment of X of order p with respect to μ is the integral of X^p: moment(X,p,μ) = ∫ X^p dμ.

Русский

Момент порядка p случайной величины X по отношению к μ равен интегралу X^p: moment(X,p,μ)=∫ X^p dμ.

LaTeX

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

Lean4

theorem moment_def (X : Ω → ℝ) (p : ℕ) (μ : Measure Ω) : moment X p μ = μ[X ^ p] :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru