variance_le_half_sum_resample_sq

Proved

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

concentrationefron-steinprobability

Efron–Stein resampling inequality: Var(Z) <= (1/2) * sum over coordinates i of E_{omega,omega'}[(Z(omega) - Z(update omega i (omega' i)))^2], with omega, omega' two independent product-measure draws and the i-th coordinate of omega resampled from omega'.

Preamble

import Mathlib.Probability.CondVar
import Mathlib.Probability.Moments.Variance
import Mathlib.Probability.Process.Filtration
import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.MeasureTheory.Integral.Prod

open MeasureTheory ProbabilityTheory Filter Set Function
open scoped ENNReal NNReal BigOperators

Formal statement

theorem variance_le_half_sum_resample_sq
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    {α : ι → Type*} [∀ i, MeasurableSpace (α i)]
    (μ : ∀ i, Measure (α i)) [∀ i, IsProbabilityMeasure (μ i)]
    {Z : (∀ j, α j) → ℝ} (hZ : MemLp Z 2 (Measure.pi μ)) :
    variance Z (Measure.pi μ)
      ≤ (∑ i, ∫ p, (Z p.1 - Z (Function.update p.1 i (p.2 i))) ^ 2
            ∂((Measure.pi μ).prod (Measure.pi μ))) / 2 := by
  sorry

Source

van Handel, Probability in High Dimension (APC 550), Section 2.1, Theorem 2.3; Boucheron–Lugosi–Massart, Concentration Inequalities (OUP 2013), Chapter 3, Theorem 3.1.

View graph