efron_stein_condExp_comap_snd_eq_partial_integral

Proved

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

conditional-expectationefron-steinmeasure-theoryprobability

Let $\rho$ and $\sigma$ be probability measures on measurable spaces $\beta$ and $\gamma$ , and let $W : \beta \times \gamma \to \mathbb{R}$ be integrable for the product measure $\rho \otimes \sigma$ . Then the conditional expectation of $W$ given the sub- $\sigma$ -algebra generated by the second coordinate (MeasurableSpace.comap Prod.snd) is, almost everywhere, the function obtained by integrating out the first coordinate:

\mathbb{E}\big[W \mid \sigma(\mathrm{snd})\big](b,c) \;=\; \int_\beta W(x,c)\,d\rho(x) \qquad (\rho\otimes\sigma)\text{-a.e.}

In words: conditioning a product-measure integrand on the second factor equals taking the partial integral over the first factor. This is the standard product-space identification of a conditional expectation as a marginal (fiberwise) integral, proved here without any StandardBorelSpace / condDistrib hypotheses — directly from the defining set-integral characterization of conditional expectation (ae_eq_condExp_of_forall_setIntegral_eq) together with Fubini's theorem (integral_prod_symm), since every set in comap Prod.snd is of the form Set.univ ×ˢ t. It is the foundational measure-theoretic brick underlying the Efron–Stein variance tensorization (van Handel, Probability in High Dimension, APC 550, §2.1) and the general Han-type subadditivity, where conditioning on all-but-one coordinate of a product space must be identified with the within-coordinate fiber integral.

Preamble

import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
import Mathlib.MeasureTheory.Integral.Prod
import Mathlib.MeasureTheory.Measure.Prod

open MeasureTheory Filter
open scoped ENNReal NNReal BigOperators

Formal statement

theorem efron_stein_condExp_comap_snd_eq_partial_integral
    {β γ : Type*} [MeasurableSpace β] [MeasurableSpace γ]
    (ρ : Measure β) [IsProbabilityMeasure ρ] (σ : Measure γ) [IsProbabilityMeasure σ]
    {W : β × γ → ℝ} (hW : Integrable W (ρ.prod σ)) :
    (ρ.prod σ)[W | MeasurableSpace.comap Prod.snd inferInstance]
      =ᵐ[ρ.prod σ] fun p => ∫ x, W (x, p.2) ∂ρ := by sorry

Source

R. van Handel, Probability in High Dimension (APC 550), §2.1; Boucheron–Lugosi–Massart, Concentration Inequalities (OUP 2013), Ch. 3 (standard product-measure conditional expectation = partial integral).

View graph