Main Convergence Theorems via L² Approach

This file contains the main convergence theorems for the L² proof of de Finetti's theorem, including weighted sums convergence and reverse martingale results.

Main results

• weighted_sums_converge_L1: Weighted sums converge in L¹ for contractable sequences
• reverse_martingale_limit: Tail-measurable limit via reverse martingale
• directing_measure: Construction of the directing measure
• directing_measure_satisfies_requirements: Final packaging theorem

References

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

L¹ convergence via reverse martingale (main convergence theorem)

theorem Exchangeability.DeFinetti.ViaL2.weighted_sums_converge_L1 {Ω : 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 μ) (f : ℝ → ℝ) (hf_meas : Measurable f) (hf_bdd : ∃ (M : ℝ), ∀ (x : ℝ), |f x| ≤ M) : ∃ (alpha : Ω → ℝ), Measurable alpha ∧ MeasureTheory.MemLp alpha 1 μ ∧ ∀ (n : ℕ), ∀ ε > 0, ∃ (M : ℕ), ∀ m ≥ M, ∫ (ω : Ω), |1 / ↑m * ∑ k : Fin m, f (X (n + ↑k + 1) ω) - alpha ω| ∂μ < ε

Weighted sums converge in L¹ for contractable sequences.

For a contractable sequence X and bounded measurable f, the Cesàro averages (1/m) * ∑_{i<m} f(X_{n+i+1}) converge in L¹ to a limit α : Ω → ℝ that does not depend on n.

This is the key convergence result needed for de Finetti's theorem via the L² approach. The proof uses L² contractability bounds to show the averages form a Cauchy sequence in L¹.

Step 3: Reverse martingale convergence

theorem Exchangeability.DeFinetti.ViaL2.subsequence_criterion_convergence_in_probability {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (ξ : ℕ → Ω → ℝ) (ξ_limit : Ω → ℝ) (hξ_meas : ∀ (n : ℕ), Measurable (ξ n)) (hξ_limit_meas : Measurable ξ_limit) (h_prob_conv : ∀ ε > 0, Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | ε ≤ |ξ n ω - ξ_limit ω|}) Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (k : ℕ) => ξ (φ k) ω) Filter.atTop (nhds (ξ_limit ω))

FMP 4.2: Subsequence criterion.

Let ξ, ξ₁, ξ₂,... be random elements in a metric space (S, ρ). Then ξₙ →ᵖ ξ iff every subsequence N' ⊆ ℕ has a further subsequence N'' ⊆ N' such that ξₙ → ξ a.s. along N''. In particular, ξₙ → ξ a.s. implies ξₙ →ᵖ ξ.

Proof outline (Kallenberg): Forward direction (→ᵖ implies a.s. along subsequence):

1. Assume ξₙ →ᵖ ξ, fix arbitrary subsequence N' ⊆ ℕ
2. Choose further subsequence N'' ⊆ N' with E ∑{n∈N''} {ρ(ξₙ,ξ) ∧ 1} = ∑{n∈N''} E[ρ(ξₙ,ξ) ∧ 1] < ∞ (equality by monotone convergence)
3. Series converges a.s., so ξₙ → ξ a.s. along N''

Reverse direction (a.s. subsequences imply →ᵖ):

1. Assume condition. If ξₙ ↛ᵖ ξ, then ∃ε > 0 with E[ρ(ξₙ,ξ) ∧ 1] > ε along N' ⊆ ℕ
2. By hypothesis, ξₙ → ξ a.s. along N'' ⊆ N'
3. By dominated convergence, E[ρ(ξₙ,ξ) ∧ 1] → 0 along N'', contradiction

Mathlib reference: Look for convergence in probability and a.s. convergence in Probability namespace. The subsequence extraction should follow from summability of expectations.

Note: Adapted to our L¹ convergence setting.

theorem Exchangeability.DeFinetti.ViaL2.reverse_martingale_subsequence_convergence {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (alpha : ℕ → Ω → ℝ) (alpha_inf : Ω → ℝ) (h_alpha_meas : ∀ (n : ℕ), Measurable (alpha n)) (h_alpha_inf_meas : Measurable alpha_inf) (h_integrable : ∀ (n : ℕ), MeasureTheory.Integrable (fun (ω : Ω) => alpha n ω - alpha_inf ω) μ) (h_L1_conv : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, ∫ (ω : Ω), |alpha n ω - alpha_inf ω| ∂μ < ε) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (k : ℕ) => alpha (φ k) ω) Filter.atTop (nhds (alpha_inf ω))

OBSOLETE with refactored approach: This theorem is no longer needed.

With the refactored weighted_sums_converge_L1, we get a single alpha : Ω → ℝ that is independent of the starting index. There is no sequence alpha_n to take a subsequence of.

The original Kallenberg approach had alpha_n → alpha_∞, but our refactored proof shows alpha_n = alpha for all n directly.

Step 4: Contractability + dominated convergence gives conditional expectation formula

Note: Step 5 theorem alpha_is_conditional_expectation_packaged has a complete proof in MoreL2Helpers.lean (at the ViaL2 namespace level). It was removed from here since it wasn't used in the critical path. The critical path uses directing_measure_satisfies_requirements from MoreL2Helpers instead.