Directing measure: Iic base case

For each t : ℝ, the integral of the indicator of Iic t against the directing measure agrees, almost everywhere in ω, with alphaIicCE X t ω. This is the Stieltjes-level identification that the kernel bridge and the bounded-measurable extension both consume.

Main result

• directing_measure_integral_Iic_ae_eq_alphaIicCE: base case for Iic indicators.

References

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

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.

Proof outline:

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

Both the kernel bridge (directing_measure_ae_eq_condExpKernel_map) and the bounded- measurable extension in DirectingMeasureIntegral consume this Iic identification.