condExp_piFinset_eq_marginal

Proved

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

conditional-expectationefron-steinmeasure-theoryprobabilityproduct-measure

Let $(\mu_i)_{i\in\iota}$ be probability measures on measurable spaces $\alpha_i$ over a finite index type $\iota$ , and let $Z$ be integrable on the product cube $\bigotimes_i \mu_i$ (Measure.pi μ). Fix a coordinate subset $s \subseteq \iota$ and consider the prefix sub- $\sigma$ -algebra generated by the restriction-to- $s$ map (MeasurableSpace.comap (Finset.restrict s)). Then the conditional expectation of $Z$ given this prefix $\sigma$ -algebra equals, $\bigotimes_i\mu_i$ -almost everywhere, the result of integrating $Z$ out over the complement coordinates $\{i : i\notin s\}$ , with the prefix values held fixed:

\mathbb{E}\big[Z \mid \sigma(\text{coords in } s)\big](\omega) \;=\; \int Z\big(\text{merge of } \omega|_s \text{ with } z\big)\, d\!\!\bigotimes_{i\notin s}\!\mu_i(z),

where the merge of the prefix-values $\omega|_s$ with complement-values $z$ is performed by the measurable equivalence MeasurableEquiv.piEquivPiSubtypeProd. This is the multi-coordinate generalization of the two-factor brick condExp_comap_fst_eq_partial_integral: conditioning on a block of coordinates equals marginalizing out the complementary block. It is the step-(c) ingredient (prefix-filtration conditional expectation as marginalization) of 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
import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.Probability.Process.Filtration

open MeasureTheory Filter
open scoped ENNReal NNReal BigOperators

Formal statement

theorem condExp_piFinset_eq_marginal
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    {α : ι → Type*} [∀ i, MeasurableSpace (α i)]
    (μ : ∀ i, Measure (α i)) [∀ i, IsProbabilityMeasure (μ i)]
    (s : Finset ι) {Z : (∀ i, α i) → ℝ}
    (hZ : Integrable Z (Measure.pi μ)) :
    (Measure.pi μ)[Z | MeasurableSpace.comap (Finset.restrict s) inferInstance]
      =ᵐ[Measure.pi μ]
      fun ω => ∫ z : (∀ i : {i // ¬ i ∈ s}, α i),
          Z ((MeasurableEquiv.piEquivPiSubtypeProd α (· ∈ s)).symm
              ((MeasurableEquiv.piEquivPiSubtypeProd α (· ∈ s) ω).1, z))
          ∂(Measure.pi fun i : {i // ¬ i ∈ s} => μ i) := 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; prefix-filtration conditional expectation as marginalization).

View graph