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_mul_indicator_of_condIndep: Product formula for indicators

  • Direct application of ProbabilityTheory.condIndep_iff

• condexp_indicator_inter_bridge: Typeclass-safe wrapper for ViaMartingale.lean

  • Manages IsFiniteMeasure and SigmaFinite instances automatically

3. Distributional Equality ⇒ Conditional Expectation Equality

• condexp_indicator_eq_of_pair_law_eq: Core lemma for Axiom 1 (condexp_convergence)

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

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

  • Used in: ViaMartingale contractability arguments (with Y=X_m, Y'=X_k, Z=shift)
  • Key technique: Uniqueness of conditional expectation via integral identity

• condexp_indicator_eq_of_agree_on_future_rectangles: Application to sequences

  • Wrapper for exchangeable sequence contexts

4. Sub-σ-algebra Infrastructure

• condExpWith: Explicit instance management wrapper

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

• sigmaFinite_trim: Trimmed measure is sigma-finite (when base is finite)

  • Used in: ViaMartingale, multiple sub-σ-algebra constructions
  • Note: isFiniteMeasure_trim is now in mathlib as an instance

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 (finFutureSigma, tailSigma, etc.)
• Proof-specific calculations
• High-level proof architecture

Related Files

• CondExpBasic.lean: Basic conditional expectation utilities
• CondProb.lean: Conditional probability definitions
• ViaMartingale.lean: Main consumer of this API
• ViaL2.lean: Uses integrability lemmas
• ViaKoopman.lean: Uses integrability and independence lemmas

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.

Pair-law ⇒ conditional indicator equality (stub)

def Exchangeability.Probability.cylinder (α : Type u_3) (r : ℕ) (C : Fin r → Set α) : Set (ℕ → α)

Standard cylinder on the first r coordinates starting at index 0.

NOTE: This is intentionally duplicated from PathSpace.CylinderHelpers.cylinder to avoid a circular import. CondExp is a low-level module that cannot import PathSpace, but needs this definition for working with product measures on sequence spaces.

Equations

• Exchangeability.Probability.cylinder α r C = {f : ℕ → α | ∀ (i : Fin r), f ↑i ∈ C i}

Conditional Independence (Doob's Characterization)

Mathlib Integration

Conditional independence is now available in mathlib as ProbabilityTheory.CondIndep from Mathlib.Probability.Independence.Conditional.

For two σ-algebras m₁ and m₂ to be conditionally independent given m' with respect to μ, we require that for any sets t₁ ∈ m₁ and t₂ ∈ m₂: μ⟦t₁ ∩ t₂ | m'⟧ =ᵐ[μ] μ⟦t₁ | m'⟧ * μ⟦t₂ | m'⟧

To use: open ProbabilityTheory to access CondIndep, or use ProbabilityTheory.CondIndep directly.

Related definitions also available in mathlib:

• ProbabilityTheory.CondIndepSet: conditional independence of sets
• ProbabilityTheory.CondIndepFun: conditional independence of functions
• ProbabilityTheory.iCondIndep: conditional independence of families

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.

Bounded Martingales and L² Inequalities

Axioms for Conditional Independence Factorization

theorem Exchangeability.Probability.condExp_indicator_mul_indicator_of_condIndep {Ω : Type u_3} {m₀ : MeasurableSpace Ω} [StandardBorelSpace Ω] {m mF mH : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (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 a direct consequence of ProbabilityTheory.condIndep_iff (set version).

Helper API for Sub-σ-algebras

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

SigmaFinite instances for trimmed measures

When working with conditional expectations on sub-σ-algebras, we need SigmaFinite (μ.trim hm). For probability measures (or finite measures), this follows from showing the trimmed measure is still finite.

These lemmas are now in ForMathlib.MeasureTheory.Measure.TrimInstances and re-exported here for backward compatibility.

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 the proven factorization lemma 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]

Bridge lemma: Product formula for conditional expectations of indicators under conditional independence.

This is an adapter that manages typeclass instances and forwards to condExp_indicator_mul_indicator_of_condIndep. Use this in ViaMartingale.lean to avoid typeclass resolution issues.

Conditional expectation equality from distributional equality

This is the key bridge lemma for Axiom 1 (condexp_convergence): if (Y, Z) and (Y', Z) have the same joint distribution, then their conditional expectations given σ(Z) are equal.

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.
   

This is the key step for condexp_convergence in ViaMartingale.lean! Use with Y = X_m, Y' = X_k, Z = shiftRV X (m+1), and the equality comes from contractability via contractable_dist_eq.

theorem Exchangeability.Probability.condexp_indicator_eq_of_agree_on_future_rectangles {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X₁ X₂ : Ω → α} {Y : Ω → ℕ → α} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hY : Measurable Y) (heq : MeasureTheory.Measure.map (fun (ω : Ω) => (X₁ ω, Y ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X₂ ω, Y ω)) μ) (B : Set α) (hB : MeasurableSet B) : μ[(B.indicator fun (x : α) => 1) ∘ X₁|MeasurableSpace.comap Y inferInstance] =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X₂|MeasurableSpace.comap Y inferInstance]

Proof of condexp_indicator_eq_of_agree_on_future_rectangles.

This is a direct application of condexp_indicator_eq_of_pair_law_eq with the sequence type.

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.

NOTE: Check if this exists in mathlib! This is a standard result.

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

Product of integrable and bounded measurable functions is integrable.

theorem Exchangeability.Probability.condExp_abs_le_of_abs_le {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace Ω} (_hm : m ≤ m) {f g : Ω → ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (h : ∀ (ω : Ω), |f ω| ≤ |g ω|) : ∀ᵐ (ω : Ω) ∂μ, |μ[f|m] ω| ≤ μ[fun (ω' : Ω) => |g ω'| |m] ω

Conditional expectation preserves monotonicity (in absolute value).

If |f| ≤ |g| everywhere, then |E[f|m]| ≤ E[|g||m].

theorem Exchangeability.Probability.condExp_L1_lipschitz {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace Ω} (_hm : m ≤ m) {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.