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]