condVar_bot_ae_eq — Mathlib

English

Provided X is integrable, the bottom conditional variance equals the unconditional variance almost everywhere.

Русский

При условии интегрируемости X нижняя условная дисперсия равна безусловной дисперсии почти наверняка.

LaTeX

$$$\\mathrm{Var}[X; \\mu | \\perp] \\;=ᵃᵉ_μ\\; \\mathrm{Var}[X; \\mu]$$$

Lean4

theorem condVar_bot_ae_eq (X : Ω → ℝ) : Var[X; μ | ⊥] =ᵐ[μ] fun _ ↦ ⨍ ω, (X ω - ⨍ ω', X ω' ∂μ) ^ 2 ∂μ :=
  by
  obtain rfl | hμ := eq_zero_or_neZero μ
  · rw [ae_zero]
    exact eventually_bot
  · exact .of_forall <| congr_fun (condVar_bot' X)

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