Helper Lemmas for L² de Finetti Proof

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

Contents

1. CovarianceHelpers: Lemmas about contractable sequences and covariance structure
2. Lp Utility Lemmas: Standard Lp space and ENNReal conversion helpers
3. FinIndexHelpers: Fin reindexing lemmas for two-window bounds

Key Results

• contractable_map_single: All marginals have the same distribution
• contractable_map_pair: All bivariate marginals have the same joint distribution
• contractable_comp: Contractability preserved under measurable postcomposition
• dist_toLp_eq_eLpNorm_sub: Distance in L^p equals norm of difference
• Various arithmetic bounds for convergence rates
• Fin index reindexing lemmas for filtered sums

theorem Exchangeability.DeFinetti.L2Helpers.contractable_map_single {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) {i : ℕ} : MeasureTheory.Measure.map (fun (ω : Ω) => X i ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) => X 0 ω) μ

All marginals have the same distribution in a contractable sequence.

For a contractable sequence, the law of each coordinate agrees with the law of X 0. This follows from contractability by taking the singleton subsequence {i}.

This is used to establish uniform covariance structure across all pairs of coordinates.

theorem Exchangeability.DeFinetti.L2Helpers.contractable_map_pair {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) {i j : ℕ} (hij : i < j) : MeasureTheory.Measure.map (fun (ω : Ω) => (X i ω, X j ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X 0 ω, X 1 ω)) μ

All bivariate marginals have the same distribution in a contractable sequence.

For a contractable sequence, every increasing pair (i,j) with i < j has the same joint law as (X 0, X 1). This follows from contractability by taking the two-point subsequence {i, j}.

Combined with contractable_map_single, this establishes that covariances are uniform: Cov(X_i, X_j) depends only on whether i = j, giving the covariance structure needed for the L² contractability bound.

theorem Exchangeability.DeFinetti.L2Helpers.contractable_comp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (f : ℝ → ℝ) (hf_meas : Measurable f) : Contractable μ fun (n : ℕ) (ω : Ω) => f (X n ω)

Contractability is preserved under measurable postcomposition.

If X is a contractable sequence and f is measurable, then f ∘ X is also contractable. This allows transferring contractability from one sequence to another via measurable transformations, which is useful for studying bounded functions of contractable sequences.

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.sqrt_div_lt_third_eps_of_nat {Cf ε : ℝ} (hCf : 0 ≤ Cf) (hε : 0 < ε) ⦃m : ℕ⦄ : m ≥ ⌈9 * Cf / ε ^ 2⌉₊ + 1 → 3 * √(Cf / ↑m) < ε

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

Similar to sqrt_div_lt_half_eps_of_nat but with factor 3 instead of 1/2. Used in the Cauchy argument where we sum three L² bounds via triangle inequality.

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.

theorem Exchangeability.DeFinetti.L2Helpers.contractable_single_marginal_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (k : ℕ) : MeasureTheory.Measure.map (X k) μ = MeasureTheory.Measure.map (X 0) μ

Single marginals have identical distribution in contractable sequences.

For contractable sequences, all variables X_k have the same distribution as X_0. This is a direct application of contractable_map_single.

Note: This wrapper is kept for compatibility, but contractable_map_single can be used directly when measurability hypotheses are available.

theorem Exchangeability.DeFinetti.L2Helpers.FinIndexHelpers.card_filter_fin_val_lt_two_mul (k : ℕ) : {i : Fin (2 * k) | ↑i < k}.card = k

Cardinality of {i : Fin(2k) | i.val < k} is k.

theorem Exchangeability.DeFinetti.L2Helpers.FinIndexHelpers.card_filter_fin_val_ge_two_mul (k : ℕ) : {i : Fin (2 * k) | ¬↑i < k}.card = k

Cardinality of {i : Fin(2k) | i.val ≥ k} is k.

theorem Exchangeability.DeFinetti.L2Helpers.FinIndexHelpers.sum_filter_fin_val_lt_eq_sum_fin {β : Type u_3} [AddCommMonoid β] (n k : ℕ) (hk : k ≤ n) (g : ℕ → β) : ∑ i : Fin n with ↑i < k, g ↑i = ∑ j : Fin k, g ↑j

Sum over {i : Fin n | i.val < k} equals sum over Fin k when k ≤ n.

theorem Exchangeability.DeFinetti.L2Helpers.FinIndexHelpers.sum_filter_fin_val_ge_eq_sum_fin {β : Type u_3} [AddCommMonoid β] (n k : ℕ) (hk : k ≤ n) (g : ℕ → β) : ∑ i : Fin n with ¬↑i < k, g ↑i = ∑ j : Fin (n - k), g (k + ↑j)

Sum over {i : Fin n | i.val ≥ k} equals sum over Fin (n-k) with offset, when k ≤ n.

theorem Exchangeability.DeFinetti.L2Helpers.FinIndexHelpers.sum_last_block_eq_sum_fin {β : Type u_3} [AddCommMonoid β] (n k : ℕ) (g : ℕ → β) : ∑ i : Fin (n + k) with n ≤ ↑i, g ↑i = ∑ j : Fin k, g (n + ↑j)

Sum over last k elements of Fin(n+k) equals sum over Fin k with offset.

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.integral_sq_weighted_sum_eq_centered {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (ξ : Fin n → Ω → ℝ) (c : Fin n → ℝ) (m : ℝ) (hc_sum : ∑ i : Fin n, c i = 0) : ∫ (ω : Ω), (∑ i : Fin n, c i * ξ i ω) ^ 2 ∂μ = ∫ (ω : Ω), (∑ i : Fin n, c i * (ξ i ω - m)) ^ 2 ∂μ

Step 1: Centering reduction - when coefficients sum to zero, we can replace variables with centered variables in weighted sums.

theorem Exchangeability.DeFinetti.L2Approach.integral_sq_weighted_sum_eq_double_sum {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {n : ℕ} (η : Fin n → Ω → ℝ) (c : Fin n → ℝ) (h_integrable : ∀ (i j : Fin n), MeasureTheory.Integrable (fun (ω : Ω) => η i ω * η j ω) μ) : ∫ (ω : Ω), (∑ i : Fin n, c i * η i ω) ^ 2 ∂μ = ∑ i : Fin n, ∑ j : Fin n, c i * c j * ∫ (ω : Ω), η i ω * η j ω ∂μ

Step 2: Expand L² norm as bilinear form - converts integral of square to double sum of covariances.

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|