dlp_sigma_randomization_condexp_eq_sigma_integral

σ-conditional-expectation substrate (de la Peña–Montgomery-Smith 1995 forward bound, eqs (4)–(6)). On a product probability space $\mu \otimes \nu$ — the sample block $\Omega$ (playing the role of $G_2 = \sigma(X^{(1)},X^{(2)})$) times the sign block $B$ (the independent symmetric Rademacher signs $\{\sigma_i\}$) — the conditional expectation, given the sample block, of any Banach-valued function $g$ that depends only on the sign block equals its sign-average:

Formally: for a strongly measurable, $\nu$-integrable $g : B \to E$ (with $E$ a complete real normed space, e.g. a matrix or real statistic), the conditional expectation of $(\omega,\sigma)\mapsto g(\sigma)$ with respect to the $\sigma$-algebra $\mathrm{comap}\,\mathrm{Prod.fst}$ generated by the sample block, under $\mu.\mathrm{prod}\,\nu$, is almost everywhere the constant $\int g\,d\nu$. This is the measure-theoretic core of the de la Peña–Montgomery-Smith σ-randomization step (arXiv:math/9309211, §4 eqs (4)→(6)): the signs are independent of the X's, so conditioning on $G_2$ integrates them to the uniform average that defines $T_{n,k} = 2^k\,\mathbb{E}(\sum f(Z)\mid G_2)$. It packages Mathlib's condExp_indep_eq with product-measure coordinate independence (indepFun_prod).