BlockAverages — Covariance structure for contractable L² sequences

contractable_covariance_structure: the uniform mean/variance/correlation package for a contractable real-valued sequence in L². The two L² Cauchy bounds (l2_bound_two_windows_uniform in BlockAverages/TwoWindows.lean and l2_bound_long_vs_tail in BlockAverages/LongVsTail.lean) consume this package.

Step 1: L² bound is the key tool

Covariance and Lp utility lemmas are now in L2Helpers.lean.

Covariance structure lemma

This auxiliary result characterizes the complete second-moment structure of contractable sequences. It's included here for use in applying l2_contractability_bound.

theorem Exchangeability.DeFinetti.ViaL2.contractable_covariance_structure {Ω : 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 μ) : ∃ (m : ℝ) (σSq : ℝ) (ρ : ℝ), (∀ (k : ℕ), ∫ (ω : Ω), X k ω ∂μ = m) ∧ (∀ (k : ℕ), ∫ (ω : Ω), (X k ω - m) ^ 2 ∂μ = σSq) ∧ (∀ (i j : ℕ), i ≠ j → ∫ (ω : Ω), (X i ω - m) * (X j ω - m) ∂μ = σSq * ρ) ∧ 0 ≤ σSq ∧ -1 ≤ ρ ∧ ρ ≤ 1

Uniform covariance structure for contractable L² sequences.

A contractable sequence X in L²(μ) has uniform second-moment structure:

• All X_i have the same mean m
• All X_i have the same variance σ²
• All distinct pairs (X_i, X_j) have the same covariance σ²·ρ
• The correlation coefficient satisfies |ρ| ≤ 1

This is proved using the Cauchy-Schwarz inequality and the fact that contractability forces all marginals of the same dimension to have identical distributions.