expected_condVar_coord_eq_half_resample

Let $\mu_i$ be probability measures on measurable spaces $\alpha_i$ over a finite index type $\iota$, and let $Z$ be square-integrable on the product cube with the independent-coordinate measure $\bigotimes_i \mu_i$ (Measure.pi μ). For a fixed coordinate $i$, the per-coordinate conditional variance is $\operatorname{Var}_i Z(\omega) = \operatorname{Var}_{x\sim\mu_i}\, Z(\omega \text{ with } i\text{-th coordinate replaced by } x)$ (variance (fun x => Z (Function.update ω i x)) (μ i)). Then its expectation over $\omega \sim \bigotimes_j \mu_j$ equals half the expected squared single-coordinate resampling difference on the doubled product cube:

This is the per-coordinate global resampling identity at the heart of the factor $\tfrac12$ in the Efron–Stein inequality: it identifies the expected conditional variance contributed by coordinate $i$ with the expected square of the difference produced by independently resampling that single coordinate. Combined over all coordinates with the variance tensorization spine it yields $\operatorname{Var}(Z) \le \tfrac12 \sum_i \mathbb{E}\,(Z - Z'_i)^2$. The proof applies the single-measure symmetrization $\operatorname{Var}(W)=\tfrac12\mathbb{E}(W-W')^2$ fiberwise in coordinate $i$, then collapses the resulting double integral via the measure-preservation of the single-coordinate resample map and Fubini. Source: R. van Handel, Probability in High Dimension (APC 550), §2.1; Boucheron–Lugosi–Massart, Concentration Inequalities (OUP 2013), Ch. 3, Thm 3.1.