Efron–Stein inequality on finite probability products

Abstract

The variance of a bounded measurable observable on a finite dependent product is bounded by half its total coordinate resampling energy.

Theorem 1.1 (Finite-product variance tensorization).

$$\begin{array}{r}\forall I:\mathrm{Type}\left(\right),[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)]\forall Omega:I\to \mathrm{Type}\left(\right),[\forall i:I,\mathrm{MeasurableSpace}\left(Omega\left(i\right)\right)]\\ \forall mu:\forall i:I,\mathrm{Measure}\left(Omega\left(i\right)\right),[\forall i:I,\mathrm{IsProbabilityMeasure}\left(mu\left(i\right)\right)]\forall F:(\forall i:I,Omega\left(i\right))\to \mathbb{R},\mathrm{Measurable}\left(F\right)\Rightarrow \\ \forall M:\mathbb{R},(\forall x:(\forall i:I,Omega\left(i\right)),\left|F\left(x\right)\right|\le M)\Rightarrow \\ \mathrm{Var}\left(F,\mathrm{MeasurePi}\left(mu\right)\right)\le \frac{1}{2}\cdot \sum _{i:I}{\int }_x{\int }_y(F\left(\mathrm{update}\left(x,i,y\right)\right)-F\left(x\right){)}^{2}d\left(mu\left(i\right)\right)(y)d\left(\mathrm{MeasurePi}\left(mu\right)\right)(x)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Probability/EfronStein.efronStein_pi (✓ std3). ∎

Citation. Scott N. Armstrong (2026). CoarseGraining Efron-Stein source proof. URL: https://github.com/scottnarmstrong/CoarseGraining/tree/310d1a6bab3ba2d398cdaffec32f3c9d4b5a24be/Homogenization/Probability/EfronStein.

Commentary.

The index type is any finite type, including the empty type. Each coordinate has its own arbitrary measurable space and probability measure. The observable is a measurable real function on their dependent product with a single pointwise absolute bound M. The outer sample x follows the full product law, and the replacement y follows the probability measure of coordinate i. The coefficient is one half.

Splitting off one coordinate gives the two-factor variance decomposition. The two-point variance identity supplies that coordinate’s resampling term; Jensen’s inequality bounds each resampling term of the conditional mean by the corresponding term of the original observable. Induction on the number of coordinates and a measure-preserving reindexing give the stated finite-product inequality. The empty product has zero variance and an empty energy sum.

This is a credited port of Scott N. Armstrong’s CoarseGraining sources TwoPoint.lean, ProdDecomp.lean and Fin.lean at revision 310d1a6bab3ba2d398cdaffec32f3c9d4b5a24be. The original Apache-2.0 copyright and full license are retained, with source correspondence in the literature note. The source proof is consolidated and adapted to the receiving Mathlib API.

Coordinates may differ and their measures need not be identical. No topology, Borel-space condition, symmetry or nondegeneracy is required. The conclusion concerns bounded observables and finite products; it supplies variance control from coordinate sensitivities.

References

• Truth anchor: D5/S3/Analytic/Probability/EfronStein.efronStein_pi