condVar_bot' — Mathlib

English

When conditioning on the bottom (trivial) sigma-algebra, the conditional variance is given by a function of ω that is the integral over the space of (X(ω) − E[X])^2 with respect to μ.

Русский

Условная дисперсия при условии минимальной информации есть функция от ω, равная ∫ (X(ω) − E[X])^2 dμ(ω').

LaTeX

$$$\\mathrm{Var}[X; \\mu | \\perp](\\omega) = \\displaystyle \\int (X(\\omega) - \\int X(\\omega')\,d\\mu(\\omega'))^2 \\, d\\mu(\\omega')$$$

Lean4

theorem condVar_bot' [NeZero μ] (X : Ω → ℝ) : Var[X; μ | ⊥] = fun _ => ⨍ ω, (X ω - ⨍ ω', X ω' ∂μ) ^ 2 ∂μ := by
  simp [condVar, condExp_bot', average, measureReal_def]

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