Conditional Expectation API for Exchangeability Proofs

This file provides a reusable API for conditional expectations, conditional independence, and distributional equality, designed to eliminate repeated boilerplate in the de Finetti theorem proofs (ViaMartingale, ViaL2, ViaKoopman).

Purpose

The exchangeability proofs repeatedly need to:

1. Show bounded indicator compositions are integrable
2. Establish conditional independence via projection properties
3. Transfer conditional expectation equalities from distributional assumptions
4. Manage typeclass instances for sub-σ-algebras

This file centralizes these patterns to keep the main proofs clean and maintainable.

Main Components

1. Integrability Infrastructure

• integrable_indicator_comp: Bounded indicator composition (1_B ∘ X) is integrable
  • Used in: ViaMartingale (lines 2897, 2904), CommonEnding, multiple locations
  • Eliminates: Repeated (integrable_const 1).indicator boilerplate
  • Key insight: Bounded measurable functions on finite measures are always integrable

2. Conditional Independence (Doob's Characterization)

• condIndep_of_indicator_condexp_eq: Projection property ⇒ conditional independence

  • Used in: ViaMartingale conditional independence arguments
  • Key insight: Uses mathlib's ProbabilityTheory.CondIndep product formula

• condexp_indicator_inter_bridge: Indicator/set form of ProbabilityTheory.condIndep_iff, with the typeclass plumbing absorbed for ViaMartingale.lean

3. Distributional Equality ⇒ Conditional Expectation Equality

• condexp_indicator_eq_of_pair_law_eq: If (Y,Z) and (Y',Z) have the same law, then for measurable B:

  𝔼[1_{Y ∈ B} | σ(Z)] = 𝔼[1_{Y' ∈ B} | σ(Z)]  a.e.
  

  • Used in: ViaMartingale.CondExpConvergence (Y=X_m, Y'=X_k, Z=shiftRV X (m+1))
  • Key technique: Uniqueness of conditional expectation via integral identity

4. Sub-σ-algebra Infrastructure

• condExpWith: Explicit instance management wrapper
  • Purpose: Avoids typeclass metavariable issues in μ[f | m]
  • Used in: ViaMartingale finite-future sigma algebras

Design Philosophy

Extract patterns that:

1. Appear 3+ times across proof files
2. Have 5+ lines of boilerplate
3. Require careful typeclass management
4. Encode reusable probabilistic insights

Keep in main proofs:

• Domain-specific constructions (tailSigma, etc.)
• Proof-specific calculations
• High-level proof architecture

References

• Kallenberg, Probabilistic Symmetries and Invariance Principles (2005)
• Mathlib's conditional expectation infrastructure (MeasureTheory.Function.ConditionalExpectation)
• Mathlib's conditional independence (ProbabilityTheory.CondIndep)

Integrability lemmas for indicators

theorem Exchangeability.Probability.integrable_indicator_comp {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → α} (hX : Measurable X) {B : Set α} (hB : MeasurableSet B) : MeasureTheory.Integrable ((B.indicator fun (x : α) => 1) ∘ X) μ

Integrability of bounded indicator compositions.

Given a measurable function X : Ω → α, a measurable set B : Set α, the indicator composition (Set.indicator B (fun _ => (1 : ℝ))) ∘ X is integrable on any finite measure space. This is immediate since the function is bounded by 1 and measurable.

This lemma is used repeatedly in de Finetti proofs when showing conditional expectations of indicators are integrable.

Conditional Independence (Doob's Characterization)

theorem Exchangeability.Probability.condIndep_of_indicator_condexp_eq {Ω : Type u_3} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {mF mG mH : MeasurableSpace Ω} (hmF : mF ≤ mΩ) (hmG : mG ≤ mΩ) (hmH : mH ≤ mΩ) (h : ∀ (H : Set Ω), MeasurableSet H → μ[H.indicator fun (x : Ω) => 1 | mF ⊔ mG] =ᵐ[μ] μ[H.indicator fun (x : Ω) => 1 | mG]) : ProbabilityTheory.CondIndep mG mF mH hmG μ

Doob's characterization of conditional independence (FMP 6.6).

For σ-algebras 𝒻, 𝒢, ℋ, we have 𝒻 ⊥⊥_𝒢 ℋ if and only if

P[H | 𝒻 ∨ 𝒢] = P[H | 𝒢] a.s. for all H ∈ ℋ

This characterization follows from the product formula in condIndep_iff:

• Forward direction: From the product formula, taking F = univ gives the projection property
• Reverse direction: The projection property implies the product formula via uniqueness of CE

Note: Requires StandardBorelSpace assumption from mathlib's CondIndep definition.

Helper API for Sub-σ-algebras

These wrappers provide explicit instance management for conditional expectations with sub-σ-algebras, working around Lean 4 typeclass inference issues.

Stable conditional expectation wrapper

This wrapper manages typeclass instances to avoid metavariable issues when calling condexp with sub-σ-algebras.

noncomputable def Exchangeability.Probability.condExpWith {Ω : Type u_3} {m₀ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (m : MeasurableSpace Ω) (_hm : m ≤ m₀) (f : Ω → ℝ) : Ω → ℝ

Conditional expectation with explicit sub-σ-algebra and automatic instance management.

This wrapper "freezes" the conditioning σ-algebra and installs the necessary sigma-finite instances before calling μ[f | m], avoiding typeclass metavariable issues.

Equations

• Exchangeability.Probability.condExpWith μ m _hm f = μ[f | m]

Bridge lemma for indicator factorization

This adapter allows ViaMartingale.lean to use mathlib's product-formula characterisation of CondIndep while managing typeclass instances correctly.

theorem Exchangeability.Probability.condexp_indicator_inter_bridge {Ω : Type u_3} {m₀ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {m mF mH : MeasurableSpace Ω} (hm : m ≤ m₀) (hmF : mF ≤ m₀) (hmH : mH ≤ m₀) (hCI : ProbabilityTheory.CondIndep m mF mH hm μ) {A B : Set Ω} (hA : MeasurableSet A) (hB : MeasurableSet B) : μ[(A ∩ B).indicator fun (x : Ω) => 1 | m] =ᵐ[μ] μ[A.indicator fun (x : Ω) => 1 | m] * μ[B.indicator fun (x : Ω) => 1 | m]

Product formula for conditional expectations of indicators under conditional independence.

If mF and mH are conditionally independent given m, then for A ∈ mF and B ∈ mH we have

μ[1_{A∩B} | m] = μ[1_A | m] · μ[1_B | m]   a.e.

This is the indicator/set-valued half of ProbabilityTheory.condIndep_iff, wrapped here to relieve ViaMartingale.lean of the surrounding instance plumbing.

Conditional expectation equality from distributional equality

If (Y, Z) and (Y', Z) have the same joint distribution, then their conditional expectations given σ(Z) are equal. The consumer is ViaMartingale.CondExpConvergence.

theorem Exchangeability.Probability.condexp_indicator_eq_of_pair_law_eq {Ω : Type u_3} {α : Type u_4} {β : Type u_5} [mΩ : MeasurableSpace Ω] [MeasurableSpace α] [mβ : MeasurableSpace β] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (Y Y' : Ω → α) (Z : Ω → β) (hY : Measurable Y) (hY' : Measurable Y') (hZ : Measurable Z) (hpair : MeasureTheory.Measure.map (fun (ω : Ω) => (Y ω, Z ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (Y' ω, Z ω)) μ) {B : Set α} (hB : MeasurableSet B) : μ[(B.indicator fun (x : α) => 1) ∘ Y | MeasurableSpace.comap Z mβ] =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ Y' | MeasurableSpace.comap Z mβ]

CE bridge lemma: If (Y, Z) and (Y', Z) have the same law, then for every measurable B,

E[1_{Y ∈ B} | σ(Z)] = E[1_{Y' ∈ B} | σ(Z)]  a.e.

Proof strategy:

1. For any bounded h measurable w.r.t. σ(Z), we have

   ∫ 1_{Y ∈ B} · h ∘ Z dμ = ∫ 1_{Y' ∈ B} · h ∘ Z dμ
   

   by the equality of joint push-forward measures on rectangles B × E.

2. This equality holds for all σ(Z)-measurable test functions h.

3. By uniqueness of conditional expectation (ae_eq_condExp_of_forall_setIntegral_eq),

   E[1_{Y ∈ B} | σ(Z)] = E[1_{Y' ∈ B} | σ(Z)]  a.e.
   

Used with Y = X_m, Y' = X_k, Z = shiftRV X (m+1), where the law equality comes from contractability via contractable_dist_eq.

Operator-Theoretic Conditional Expectation Utilities

theorem Exchangeability.Probability.integrable_of_bounded {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → ℝ} (hf : Measurable f) (hbd : ∃ (C : ℝ), ∀ (ω : Ω), |f ω| ≤ C) : MeasureTheory.Integrable f μ

Bounded measurable functions are integrable on finite measures.

Wraps Integrable.of_bound so callers can pass ⟨C, hC⟩ directly instead of destructuring the bound first.

theorem Exchangeability.Probability.condExp_L1_lipschitz {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace Ω} {f g : Ω → ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) : ∫ (ω : Ω), |μ[f | m] ω - μ[g | m] ω| ∂μ ≤ ∫ (ω : Ω), |f ω - g ω| ∂μ

Conditional expectation is L¹-nonexpansive (load-bearing lemma).

For integrable functions f, g, the conditional expectation is contractive in L¹: ‖E[f|m] - E[g|m]‖₁ ≤ ‖f - g‖₁

This is the key operator-theoretic property that makes CE well-behaved.

theorem Exchangeability.Probability.condExp_mul_pullout {Ω : Type u_4} {m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ m₀) {f g : Ω → ℝ} (hf : MeasureTheory.Integrable f μ) (hg_meas : Measurable g) (hg_bd : ∃ (C : ℝ), ∀ (ω : Ω), |g ω| ≤ C) : μ[f * g | m] =ᵐ[μ] fun (ω : Ω) => μ[f | m] ω * g ω

Conditional expectation pull-out property for bounded measurable functions.

If g is m-measurable and bounded, then E[f·g|m] = E[f|m]·g a.e.