Prove2Me

condExp_comap_fst_eq_partial_integral

Proved

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

conditional-expectationefron-steinfubinimeasure-theoryprobability

Let ρ\rho and σ\sigma be probability measures on measurable spaces β\beta and γ\gamma, and let WW be integrable on the product measure ρ⊗σ\rho \otimes \sigma. Then the conditional expectation of WW given the sub-σ\sigma-algebra generated by the FIRST coordinate (MeasurableSpace.comap Prod.fst) equals, ρ⊗σ\rho\otimes\sigma-almost everywhere, the partial integral of WW over the second factor:

E[W∣σ(fst)](p)  =  ∫γW(p1,y) dσ(y)(ρ⊗σ)-a.e.\mathbb{E}\big[W \mid \sigma(\mathrm{fst})\big](p) \;=\; \int_\gamma W(p_1, y)\, d\sigma(y) \qquad (\rho\otimes\sigma)\text{-a.e.}

i.e. conditioning a product-measure integrand on the first factor amounts to integrating out the second factor. This is the mirror of the brick efron_stein_condExp_comap_snd_eq_partial_integral (which conditions on the second coordinate). It is a prerequisite for the multi-coordinate prefix-filtration conditional expectation used in the Doob-martingale proof of the Efron–Stein tensorization of variance. Source: R. van Handel, Probability in High Dimension (APC 550), §2.1; Boucheron–Lugosi–Massart, Concentration Inequalities (OUP 2013), Ch. 3.

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 condExp_comap_fst_eq_partial_integral
    {β γ : Type*} [MeasurableSpace β] [MeasurableSpace γ]
    (ρ : Measure β) [IsProbabilityMeasure ρ] (σ : Measure γ) [IsProbabilityMeasure σ]
    {W : β × γ → ℝ} (hW : Integrable W (ρ.prod σ)) :
    (ρ.prod σ)[W | MeasurableSpace.comap Prod.fst inferInstance]
      =ᵐ[ρ.prod σ] fun p => ∫ y, W (p.1, y) ∂σ := by sorry
Source
R. van Handel, Probability in High Dimension (APC 550), §2.1; Boucheron–Lugosi–Massart, Concentration Inequalities (OUP 2013), Ch. 3 (Efron–Stein; conditional expectation as partial integral, first-factor version).

View graph