Alpha Convergence: Endpoint Limits for alphaIicCE

This file proves the endpoint limit properties for alphaIicCE:

• Identification of alphaIic and alphaIicCE a.e.
• L¹ convergence to 0 at -∞ and to 1 at +∞
• A.e. pointwise convergence to 0 at -∞ and to 1 at +∞

Main results

• alphaIic_ae_eq_alphaIicCE: Raw and canonical versions are equal a.e.
• alphaIicCE_L1_tendsto_zero_atBot: L¹ convergence to 0 as t → -∞
• alphaIicCE_L1_tendsto_one_atTop: L¹ convergence to 1 as t → +∞
• alphaIicCE_ae_tendsto_zero_atBot: A.e. pointwise limit 0 at -∞
• alphaIicCE_ae_tendsto_one_atTop: A.e. pointwise limit 1 at +∞

References

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

Identification lemma and endpoint limits for alphaIicCE

The key results that solve the endpoint limit problem:

1. Identification: The existential alphaIic equals the canonical alphaIicCE a.e.
2. L¹ endpoint limits: Using L¹ contraction of condExp, we get integral convergence
3. A.e. endpoint limits: Monotonicity + boundedness + L¹ limits ⇒ a.e. pointwise limits

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.

theorem Exchangeability.DeFinetti.ViaL2.alphaIicCE_L1_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)

L¹ endpoint limit at -∞: As t → -∞, alphaIicCE → 0 in L¹.

Proof strategy:

• For t → -∞, the indicator 1_{(-∞,t]}(X_0 ω) → 0 for each fixed ω
• By dominated convergence (bounded by 1), ‖1_{(-∞,t]} ∘ X_0‖₁ → 0
• By L¹ contraction of conditional expectation:

  ‖alphaIicCE t - 0‖₁ = ‖μ[1_{(-∞,t]} ∘ X_0 | tailSigma] - μ[0 | tailSigma]‖₁
                      ≤ ‖1_{(-∞,t]} ∘ X_0 - 0‖₁ → 0
  

theorem Exchangeability.DeFinetti.ViaL2.alphaIicCE_L1_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) ω - 1| ∂μ) Filter.atTop (nhds 0)

L¹ endpoint limit at +∞: As t → +∞, alphaIicCE → 1 in L¹.

Proof strategy: Similar to the -∞ case, but 1_{(-∞,t]}(X_0 ω) → 1 as t → +∞.

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.

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.