condVar_ae_le_condExp_sq — Mathlib

English

The conditional variance is almost surely bounded above by the conditional second moment.

Русский

Условная дисперсия почти наверняка не превосходит условного второго момента.

LaTeX

$$$\\ Var[X; \\mu | m] \\;\\le\\;ᵃᵉ_\\mu\\;\\mu[X^2|m]$$$

Lean4

theorem condVar_ae_le_condExp_sq (hm : m ≤ m₀) [IsFiniteMeasure μ] (hX : MemLp X 2 μ) :
    Var[X; μ | m] ≤ᵐ[μ] μ[X ^ 2|m] :=
  by
  filter_upwards [condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX] with ω hω
  dsimp at hω
  nlinarith

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