evariance

Mathlib.Probability.Moments.Variance

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

← MathLib Explorer

English

If X =ᵐ[μ] Y, then evariance(X; μ) = evariance(Y; μ).

Русский

Если X =ᵐ[μ] Y, то evariance(X; μ) = evariance(Y; μ).

LaTeX

$$$evariance[X; \\mu] = evariance[Y; \\mu]$ when $X =_{ae}^{\\mu} Y$$$

Lean4

/-- The `ℝ≥0∞`-valued variance of a real-valued random variable defined as the Lebesgue integral of
`‖X - 𝔼[X]‖^2`. -/
def evariance : ℝ≥0∞ :=
  ∫⁻ ω, ‖X ω - μ[X]‖ₑ ^ 2 ∂μ

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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