Prove2Me

expected_condVar_le_variance

Proved

by allychan327 · Jun 24, 2026 · Mathlib c5ea003 (Lean v4.30.0)

concentration-inequalitiesefron-steinprobabilityvariance

Expected conditional variance is at most the total variance. Let XX be a square-integrable real random variable on a probability space (Ω,m0,μ)(\Omega, m_0, \mu) and let m≤m0m \le m_0 be a sub-σ\sigma-algebra. Then

E[Var⁡(X∣m)]≤Var⁡(X).\mathbb{E}\big[\operatorname{Var}(X \mid m)\big] \le \operatorname{Var}(X).

This is the conditional-variance half of the law of total variance E[Var⁡(X∣m)]+Var⁡(E[X∣m])=Var⁡(X)\mathbb{E}[\operatorname{Var}(X\mid m)] + \operatorname{Var}(\mathbb{E}[X\mid m]) = \operatorname{Var}(X), obtained by discarding the nonnegative term Var⁡(E[X∣m])≥0\operatorname{Var}(\mathbb{E}[X\mid m]) \ge 0. It is the per-step contraction that the Efron–Stein coordinate induction iterates: each conditioning step can only shrink the expected residual variance.

Preamble
import Mathlib.Probability.CondVar
import Mathlib.Probability.Moments.Variance
open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal BigOperators
Formal statement
theorem expected_condVar_le_variance
    {Ω : Type*} {m₀ m : MeasurableSpace Ω} {μ : Measure[m₀] Ω}
    (hm : m ≤ m₀) [IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : MemLp X 2 μ) :
    μ[Var[X; μ | m]] ≤ Var[X; μ] := by sorry
Source
R. van Handel, Probability in High Dimension (APC 550 lecture notes, Princeton), §2.1 Tensorization and bounded differences (law of total variance / martingale decomposition); Boucheron-Lugosi-Massart, Concentration Inequalities (OUP 2013), Ch. 3.

View graph