integral_condVar_le_integral_sq_sub_of_strongly_measurable

Integrated conditional $L^2$-minimizer bound (resampling form of the Efron–Stein step). On a probability space $(\Omega, m_0, \mu)$ with $m \le m_0$, for square-integrable $X$ and any square-integrable, $m$-strongly-measurable $Y$,

Taking expectations of the pointwise conditional $L^2$-minimizer inequality gives the per-coordinate Efron–Stein bound in integrated form. Composed with the Doob-martingale decomposition $\operatorname{Var}(X) = \sum_k \mathbb{E}[\operatorname{Var}(\mathbb{E}[X\mid F_{k+1}]\mid F_k)]$ and choosing, at each step, $Y$ a resampled copy of the coordinate, this bounds each summand by a squared resampling difference and yields $\operatorname{Var}(X) \le \sum_i \mathbb{E}[(X - X'_i)^2]$ (the factor $\tfrac12$ appears in the symmetric form). This is the missing analytic ingredient that combines with the variance tensorization spine to close the general (nonlinear) Efron–Stein inequality $\operatorname{Var}(Z) \le \tfrac12 \sum_i \mathbb{E}[(Z - Z'_i)^2]$ for sup-type functionals.