Directing Measure Integrals: Bridge Lemma and Conditional Expectation

This file establishes the key "bridge lemma" connecting the directing measure to conditional expectation: for bounded measurable f,

∫ f dν(ω) = Ef(X₀) | tail a.e.

This is the final piece connecting the Cesàro convergence theory to the directing measure construction.

Main results

• directing_measure_integral_Iic_ae_eq_alphaIicCE: Base case for Iic indicators
• integral_indicator_borel_tailAEStronglyMeasurable: Tail measurability of integrals
• setIntegral_directing_measure_indicator_eq: Set integral equality for indicators
• setIntegral_directing_measure_bounded_measurable_eq: General set integral equality
• directing_measure_integral_eq_condExp: Main bridge lemma

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1, "Second proof of Theorem 1.1"

Bridge Lemma: Integral against directing measure equals conditional expectation

This is the key Kallenberg insight: the directing measure ν(ω) is the conditional distribution of X₀ given the tail σ-algebra. Therefore:

∫ f dν(ω) = Ef(X₀) | tail a.e.

Proof Strategy:

1. Base case (Iic indicators): By Stieltjes construction, ∫ 1_{Iic t} dν(ω) = alphaIic t ω = alphaIicCE t ω = E[1_{Iic t}(X₀)|tail](ω) a.e.

2. Extension: Iic sets form a π-system generating the Borel σ-algebra. By measure extensionality, two probability measures agreeing on Iic agree everywhere. The same linearity/continuity argument extends to all bounded measurable f.

This lemma is the bridge that allows us to go from:

• cesaro_to_condexp_L2: α = E[f(X₀)|tail] to:
• directing_measure_integral: α = ∫f dν

by transitivity.

theorem Exchangeability.DeFinetti.ViaL2.directing_measure_integral_Iic_ae_eq_alphaIicCE {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (t : ℝ) : (fun (ω : Ω) => ∫ (x : ℝ), (Set.Iic t).indicator (fun (x : ℝ) => 1) x ∂directing_measure X hX_contract hX_meas hX_L2 ω) =ᵐ[μ] alphaIicCE X hX_contract hX_meas hX_L2 t

Base case: For Iic indicators, the directing measure integral equals alphaIicCE.

This follows from:

1. Stieltjes construction: ∫ 1_{Iic t} dν(ω) = (ν(Iic t)).toReal
2. Measure value: (ν(Iic t)).toReal = stieltjesOfMeasurableRat t
3. Stieltjes extension: stieltjesOfMeasurableRat t = alphaIic t a.e.
4. Identification: alphaIic t =ᵐ alphaIicCE t

Helper Lemmas for Monotone Class Extension

The following lemmas build up the π-λ argument needed for directing_measure_integral_eq_condExp. Each phase is factored out as a separate lemma with its own sorry to be filled.

Phase A: Indicators of Borel sets → tail-AEStronglyMeasurable Phase B: Simple functions → tail-AEStronglyMeasurable (via linearity) Phase C: Bounded measurable functions → tail-AEStronglyMeasurable (via DCT + limits)

theorem Exchangeability.DeFinetti.ViaL2.integral_indicator_borel_tailAEStronglyMeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (s : Set ℝ) (hs : MeasurableSet s) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ∫ (x : ℝ), s.indicator (fun (x : ℝ) => 1) x ∂directing_measure X hX_contract hX_meas hX_L2 ω) μ

Phase A: For all Borel sets s, ω ↦ ∫ 1_s dν(ω) is tail-AEStronglyMeasurable.

The π-λ argument:

1. Base case: {Iic t | t ∈ ℝ} is a π-system generating Borel ℝ
2. For Iic t: uses directing_measure_integral_Iic_ae_eq_alphaIicCE + stronglyMeasurable_condExp
3. For ∅: integral is 0 (constant)
4. For complement: ∫ 1_{sᶜ} dν = 1 - ∫ 1_s dν (probability measure)
5. For disjoint unions: ∫ 1_{⋃ fn} dν = ∑' ∫ 1_{fn n} dν (σ-additivity)
6. Apply MeasurableSpace.induction_on_inter with borel_eq_generateFrom_Iic

theorem Exchangeability.DeFinetti.ViaL2.integral_simpleFunc_tailAEStronglyMeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (φ : MeasureTheory.SimpleFunc ℝ ℝ) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ∫ (x : ℝ), φ x ∂directing_measure X hX_contract hX_meas hX_L2 ω) μ

Phase B: For simple functions, the integral is tail-AEStronglyMeasurable.

Simple functions are finite linear combinations of indicator functions. Uses Finset.aestronglyMeasurable_sum and scalar multiplication.

theorem Exchangeability.DeFinetti.ViaL2.integral_bounded_measurable_tailAEStronglyMeasurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ∫ (x : ℝ), f x ∂directing_measure X hX_contract hX_meas hX_L2 ω) μ

Phase C: For bounded measurable f, the integral is tail-AEStronglyMeasurable.

Uses SimpleFunc.approxOn to approximate f by simple functions. Takes limit via aestronglyMeasurable_of_tendsto_ae + DCT.

theorem Exchangeability.DeFinetti.ViaL2.setIntegral_directing_measure_indicator_Iic_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (t : ℝ) (A : Set Ω) (hA : MeasurableSet A) (hμA : μ A < ⊤) : ∫ (ω : Ω) in A, ∫ (x : ℝ), (Set.Iic t).indicator (fun (x : ℝ) => 1) x ∂directing_measure X hX_contract hX_meas hX_L2 ω ∂μ = ∫ (ω : Ω) in A, (Set.Iic t).indicator (fun (x : ℝ) => 1) (X 0 ω) ∂μ

Set integral equality for Iic indicators.

Base case: For Iic indicators, set integral equality follows from directing_measure_integral_Iic_ae_eq_alphaIicCE + setIntegral_condExp.

theorem Exchangeability.DeFinetti.ViaL2.setIntegral_directing_measure_indicator_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (s : Set ℝ) (hs : MeasurableSet s) (A : Set Ω) (hA : MeasurableSet A) (hμA : μ A < ⊤) : ∫ (ω : Ω) in A, ∫ (x : ℝ), s.indicator (fun (x : ℝ) => 1) x ∂directing_measure X hX_contract hX_meas hX_L2 ω ∂μ = ∫ (ω : Ω) in A, s.indicator (fun (x : ℝ) => 1) (X 0 ω) ∂μ

Set integral equality for Borel indicator functions.

Extended from Iic indicators via π-λ argument.

theorem Exchangeability.DeFinetti.ViaL2.setIntegral_directing_measure_bounded_measurable_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M) (A : Set Ω) (hA : MeasurableSet A) (hμA : μ A < ⊤) : ∫ (ω : Ω) in A, ∫ (x : ℝ), f x ∂directing_measure X hX_contract hX_meas hX_L2 ω ∂μ = ∫ (ω : Ω) in A, f (X 0 ω) ∂μ

Set integral equality for bounded measurable functions.

This is the key equality needed for ae_eq_condExp_of_forall_setIntegral_eq.

theorem Exchangeability.DeFinetti.ViaL2.directing_measure_integral_eq_condExp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M) : (fun (ω : Ω) => ∫ (x : ℝ), f x ∂directing_measure X hX_contract hX_meas hX_L2 ω) =ᵐ[μ] μ[fun (ω : Ω) => f (X 0 ω)|TailSigma.tailSigma X]

Main bridge lemma: For any bounded measurable f, the integral against directing_measure equals the conditional expectation E[f(X₀)|tail].

This is the Kallenberg identification: ν(ω) is the conditional distribution of X₀ given tail.

theorem Exchangeability.DeFinetti.ViaL2.directing_measure_integral_via_chain {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M) : ∃ (alpha : Ω → ℝ), Measurable alpha ∧ MeasureTheory.MemLp alpha 1 μ ∧ (∀ (n : ℕ), ∀ ε > 0, ∃ (M : ℕ), ∀ m ≥ M, ∫ (ω : Ω), |1 / ↑m * ∑ k : Fin m, f (X (n + ↑k + 1) ω) - alpha ω| ∂μ < ε) ∧ ∀ᵐ (ω : Ω) ∂μ, alpha ω = ∫ (x : ℝ), f x ∂directing_measure X hX_contract hX_meas hX_L2 ω

Simplified directing measure integral via identification chain.

This lemma proves that the L¹ limit α equals ∫f dν a.e. using the Kallenberg identification chain:

1. α = E[f(X₀)|tail] (from cesaro_to_condexp_L2)
2. E[f(X₀)|tail] = ∫f dν (from directing_measure_integral_eq_condExp)
3. Therefore α = ∫f dν by transitivity

This approach bypasses the Ioc/step function decomposition entirely, giving a much simpler proof.

Key insight: By uniqueness of L¹ limits, the L¹ limit from weighted_sums_converge_L1 equals the L² limit from cesaro_to_condexp_L2 (since L² convergence implies L¹ on prob spaces).