Endpoint limit at +∞ for alphaIicCE

L¹ and almost-everywhere pointwise convergence of alphaIicCE to 1 as t → +∞.

Main result

• alphaIicCE_ae_tendsto_one_atTop: For a.e. ω, alphaIicCE X _ t ω → 1 as t → +∞.

The L¹ stepping stone alphaIicCE_L1_tendsto_one_atTop is private to this file.

References

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

theorem Exchangeability.DeFinetti.ViaL2.alphaIicCE_ae_tendsto_one_atTop {Ω : 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 μ) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => alphaIicCE X hX_contract hX_meas hX_L2 (↑n) ω) Filter.atTop (nhds 1)

A.e. pointwise endpoint limit at +∞.

Proof strategy: Similar to the -∞ case, using monotonicity + boundedness + L¹ → 1.