Endpoint limit at -∞ for alphaIicCE

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

Main result

• alphaIicCE_ae_tendsto_zero_atBot: For a.e. ω, alphaIicCE X _ t ω → 0 as t → -∞.

The L¹ stepping stone alphaIicCE_L1_tendsto_zero_atBot 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_zero_atBot {Ω : 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 0)

A.e. pointwise endpoint limit at -∞.

Proof strategy: Combine monotonicity (from conditional expectation), boundedness (0 ≤ alphaIicCE ≤ 1), and L¹ → 0 to conclude a.e. pointwise → 0 along integers.