Directing Measure Integrals: Bridge Lemma and Conditional Expectation

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

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

The proof routes through the kernel-level identification directing_measure_ae_eq_condExpKernel_map plus mathlib's condExp_ae_eq_integral_condExpKernel.

Main result

• directing_measure_integral_eq_condExp: bridge lemma (routes through DirectingMeasureBridge).

References

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

theorem Exchangeability.DeFinetti.ViaL2.directing_measure_integral_eq_condExp {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : 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 ω) | Tail.tailProcess X]

Bridge lemma: For bounded measurable f,

fun ω => ∫ x, f x ∂(directing_measure X … ω) agrees a.e. with the conditional expectation μ[fun ω => f (X 0 ω) | tailSigma X].

The proof routes through the kernel-level bridge directing_measure_ae_eq_condExpKernel_map and mathlib's condExp_ae_eq_integral_condExpKernel, replacing what was previously a hand-built monotone-class extension from Iic indicators.

The [StandardBorelSpace Ω] assumption comes from condExpKernel.