Helper Lemmas for L² de Finetti Proof

This file contains auxiliary lemmas used in the L² approach to de Finetti's theorem. All lemmas here are complete (no sorries) and compile cleanly.

Contents

1. Lp Utility Lemmas: Standard Lp space and ENNReal conversion helpers
2. FinIndexHelpers: Fin reindexing lemmas for two-window bounds

Key Results

• dist_toLp_eq_eLpNorm_sub: Distance in L^p equals norm of difference
• Various arithmetic bounds for convergence rates (e.g. sqrt_div_lt_half_eps_of_nat)
• Fin index reindexing lemmas for filtered sums

The contractability/covariance helpers that previously lived here have moved to the canonical Exchangeability.Contractable.{map_single, map_pair, comp} API in Exchangeability/Contractability.lean.

Lp utility lemmas

Standard lemmas for working with Lp spaces and ENNReal conversions.

theorem Exchangeability.DeFinetti.L2Helpers.dist_toLp_eq_eLpNorm_sub {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {p : ENNReal} {f g : Ω → ℝ} (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g p μ) : dist (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp g hg) = (MeasureTheory.eLpNorm (fun (ω : Ω) => f ω - g ω) p μ).toReal

Distance in L^p space equals the L^p norm of the difference.

For functions in L^p, the metric distance between their toLp representatives equals the eLpNorm of their pointwise difference (after converting from ENNReal).

This bridges the abstract metric structure of L^p spaces with concrete norm calculations.

theorem Exchangeability.DeFinetti.L2Helpers.toReal_lt_of_lt_ofReal {x : ENNReal} {ε : ℝ} (_hx : x ≠ ⊤) (hε : 0 ≤ ε) : x < ENNReal.ofReal ε → x.toReal < ε

Converting ENNReal inequalities to real inequalities.

If x < ofReal ε in ENNReal (with x finite), then toReal x < ε in ℝ. Bridges extended and real arithmetic in L^p norm bounds.

theorem Exchangeability.DeFinetti.L2Helpers.sqrt_div_lt_half_eps_of_nat {Cf ε : ℝ} (hCf : 0 ≤ Cf) (hε : 0 < ε) ⦃m : ℕ⦄ : m ≥ ⌈4 * Cf / ε ^ 2⌉₊ + 1 → √(Cf / ↑m) < ε / 2

Arithmetic bound for convergence rates: √(Cf/m) < ε/2 when m is large.

Given a constant Cf and target precision ε, provides an explicit threshold for m such that √(Cf/m) < ε/2. Used to establish L² Cauchy sequences converge in L¹.

theorem Exchangeability.DeFinetti.L2Helpers.eLpNorm_two_from_integral_sq_le {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {g : Ω → ℝ} (hg : MeasureTheory.MemLp g 2 μ) {C : ℝ} (hC : 0 ≤ C) (h : ∫ (ω : Ω), g ω ^ 2 ∂μ ≤ C) : MeasureTheory.eLpNorm g 2 μ ≤ ENNReal.ofReal √C

Convert an L² integral bound to an eLpNorm bound.

L² Contractability Bound

This section contains Kallenberg's L² contractability bound (Lemma 1.2), which provides an elementary proof of de Finetti's theorem using L² estimates without requiring the full Mean Ergodic Theorem machinery.

For detailed mathematical background, see the module docstring in the original L2Approach.lean.

theorem Exchangeability.DeFinetti.L2Approach.double_sum_covariance_formula {n : ℕ} {c : Fin n → ℝ} (σSq ρ cov_diag cov_offdiag : ℝ) (h_diag : cov_diag = σSq) (h_offdiag : cov_offdiag = σSq * ρ) : (∑ i : Fin n, ∑ j : Fin n, c i * c j * if i = j then cov_diag else cov_offdiag) = σSq * ρ * (∑ i : Fin n, c i) ^ 2 + σSq * (1 - ρ) * ∑ i : Fin n, c i ^ 2

Step 3: Separate diagonal from off-diagonal terms in covariance expansion.

theorem Exchangeability.DeFinetti.L2Approach.covariance_formula_zero_sum {n : ℕ} {c : Fin n → ℝ} (σSq ρ : ℝ) (hc_sum : ∑ i : Fin n, c i = 0) : σSq * ρ * (∑ i : Fin n, c i) ^ 2 + σSq * (1 - ρ) * ∑ i : Fin n, c i ^ 2 = σSq * (1 - ρ) * ∑ i : Fin n, c i ^ 2

Step 4: When coefficients sum to zero, the correlation term vanishes.

theorem Exchangeability.DeFinetti.L2Approach.sum_sq_le_sum_abs_mul_sup {n : ℕ} {c : Fin n → ℝ} : ∑ i : Fin n, c i ^ 2 ≤ ∑ i : Fin n, |c i| * ⨆ (j : Fin n), |c j|

Step 5: Sum of squares bounded by L¹ norm times supremum.

theorem Exchangeability.DeFinetti.L2Approach.l2_bound_from_steps {n : ℕ} {c p q : Fin n → ℝ} (σSq ρ : ℝ) (hσSq_nonneg : 0 ≤ σSq) (hρ_bd : ρ ≤ 1) (hc_def : c = fun (i : Fin n) => p i - q i) (hc_abs_sum : ∑ i : Fin n, |c i| ≤ 2) (step5 : ∑ i : Fin n, c i ^ 2 ≤ ∑ i : Fin n, |c i| * ⨆ (j : Fin n), |c j|) : σSq * (1 - ρ) * ∑ i : Fin n, c i ^ 2 ≤ 2 * σSq * (1 - ρ) * ⨆ (i : Fin n), |p i - q i|

Step 6: Combine all steps into final bound. Takes the chain of equalities and inequalities from the previous steps and produces the final L² contractability bound.

theorem Exchangeability.DeFinetti.L2Approach.l2_contractability_bound {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (ξ : Fin n → Ω → ℝ) (m σ ρ : ℝ) (_hρ_bd : -1 ≤ ρ ∧ ρ ≤ 1) (_hmean : ∀ (k : Fin n), ∫ (ω : Ω), ξ k ω ∂μ = m) (_hL2 : ∀ (k : Fin n), MeasureTheory.MemLp (fun (ω : Ω) => ξ k ω - m) 2 μ) (_hvar : ∀ (k : Fin n), ∫ (ω : Ω), (ξ k ω - m) ^ 2 ∂μ = σ ^ 2) (_hcov : ∀ (i j : Fin n), i ≠ j → ∫ (ω : Ω), (ξ i ω - m) * (ξ j ω - m) ∂μ = σ ^ 2 * ρ) (p q : Fin n → ℝ) (_hp_prob : ∑ i : Fin n, p i = 1 ∧ ∀ (i : Fin n), 0 ≤ p i) (_hq_prob : ∑ i : Fin n, q i = 1 ∧ ∀ (i : Fin n), 0 ≤ q i) : ∫ (ω : Ω), (∑ i : Fin n, p i * ξ i ω - ∑ i : Fin n, q i * ξ i ω) ^ 2 ∂μ ≤ 2 * σ ^ 2 * (1 - ρ) * ⨆ (i : Fin n), |p i - q i|