Identification of alphaIic with alphaIicCE

alphaIic (the raw existential L¹ limit) and alphaIicCE (the canonical condExp-based form) are almost everywhere equal. Both are L¹ limits of the same Cesàro averages, so uniqueness of L¹ limits gives a.e. equality.

Main result

• alphaIic_ae_eq_alphaIicCE: alphaIic =ᵐ[μ] alphaIicCE.

References

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

theorem Exchangeability.DeFinetti.ViaL2.alphaIic_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 : ℝ) : alphaIic X hX_contract hX_meas hX_L2 t =ᵐ[μ] alphaIicCE X hX_contract hX_meas hX_L2 t

Identification lemma: alphaIic equals alphaIicCE almost everywhere.

Proof strategy: Both are L¹ limits of the same Cesàro averages (1/m) ∑ᵢ (indIic t) ∘ X_{n+i}:

• alphaIic is defined as the L¹ limit from weighted_sums_converge_L1
• alphaIicCE is the conditional expectation μ[(indIic t) ∘ X_0 | tailSigma X]

By the reverse martingale convergence theorem (or direct L² analysis), the Cesàro averages converge in L² (hence L¹) to the conditional expectation. Since L¹ limits are unique up to a.e. equality, we get alphaIic =ᵐ alphaIicCE.

Note: Uses reverse martingale convergence or L² projection argument.