Two-window L² bounds for block averages of a contractable sequence

This file continues the Layer 3 (L²) lane of the Exchangeability roadmap (TauCetiRoadmap/Exchangeability/README.md, "Layer 3: L² averaging library and the standard-Borel de Finetti route"), building the "two-window L² bounds for block averages" milestone (l2_bound_two_windows_uniform) on top of the uniform covariance structure of a contractable L² sequence (contractable_covariance_structure).

For a real-valued process X : ℕ → Ω → ℝ and a finite selection k : Fin n → ℕ, the block average blockAverage X k = n⁻¹ • ∑ i, X (k i) is the empirical mean of the block (X (k i))ᵢ; it is defined, with its measure-free algebra, in TauCeti.Probability.Process.BlockAverage. When X is contractable with L² coordinates, its second-moment structure is uniform: all coordinate variances agree and all off-diagonal covariances agree (contractable_covariance_structure). Writing v = Var[X 0] and c = cov[X 0, X 1], this uniformity forces the block average to have the explicit variance

Var[blockAverage X k] = (v - c) / n + c,

and any two blocks over disjoint index sets to have covariance exactly c. Consequently two disjoint block averages of lengths n and m satisfy

Var[blockAverage X k - blockAverage X k'] = (v - c) / n + (v - c) / m,

and, since contractability makes the two averages share the common mean μ[X 0], this is the squared L² distance ∫ (blockAverage X k - blockAverage X k')² dμ itself. The squared distance vanishes like 1 / n + 1 / m (equivalently, the L² norm like n^(-1/2) for equal windows), which is the quantitative averaging input the L² route runs on: it is what drives the convergence of blockAverage X k toward the common conditional mean.

The elementary L² route to de Finetti's theorem formalised here is the one presented in Kallenberg, Probabilistic Symmetries and Invariance Principles (Springer, 2005), Chapter 1 (around Theorem 1.1); the Lean identities below were derived independently.

The covariance/variance bilinearity (ProbabilityTheory.covariance_sum_sum, variance_sum, covariance_smul_left, variance_const_mul) and the integral manipulations are Mathlib's; the contractability input is the Layer 0/3 API in TauCeti.Probability.Exchangeability.Contractability and TauCeti.Probability.Exchangeability.L2.Covariance. No material from cameronfreer/exchangeability is reused: the source carries the block-average bounds through a different, sequence-specific L² development, whereas this file records the closed-form second-moment identities directly.

theorem TauCeti.Probability.memLp_blockAverage {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} {n : ℕ} (k : Fin n → ℕ) (hX_L2 : ∀ (i : Fin n), MeasureTheory.MemLp (X (k i)) 2 μ) : MeasureTheory.MemLp (blockAverage X k) 2 μ

A block average of L² coordinates is itself L².

theorem TauCeti.Probability.condExp_blockAverage {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} {m : MeasurableSpace Ω} {n : ℕ} (k : Fin n → ℕ) (hX : ∀ (i : Fin n), MeasureTheory.Integrable (X (k i)) μ) : μ[blockAverage X k | m] =ᵐ[μ] blockAverage (fun (i : ℕ) => μ[X i | m]) k

Conditional expectation commutes with block averages. The conditional expectation of a block average of integrable coordinates is the block average of their conditional expectations.

theorem TauCeti.Probability.Contractable.variance_blockAverage {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_L2 : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 μ) {n : ℕ} (hn : 0 < n) {k : Fin n → ℕ} (hk : Function.Injective k) : ProbabilityTheory.variance (blockAverage X k) μ = (ProbabilityTheory.variance (X 0) μ - ProbabilityTheory.covariance (X 0) (X 1) μ) / ↑n + ProbabilityTheory.covariance (X 0) (X 1) μ

The variance of a block average of a contractable L² sequence. For a contractable real-valued process with L² coordinates and an injective selection k : Fin n → ℕ (0 < n), the block average has the closed-form variance (v - c) / n + c, where v = Var[X 0] is the common coordinate variance and c = cov[X 0, X 1] is the common off-diagonal covariance.

theorem TauCeti.Probability.Contractable.integral_blockAverage {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} (hX : Contractable μ X) (hint0 : MeasureTheory.Integrable (X 0) μ) {n : ℕ} (hn : 0 < n) {k : Fin n → ℕ} (hint : ∀ (i : Fin n), MeasureTheory.Integrable (X (k i)) μ) : ∫ (x : Ω), blockAverage X k x ∂μ = ∫ (x : Ω), X 0 x ∂μ

The mean of a block average of a contractable process. A block average over any selection of length 0 < n has the common coordinate mean μ[X 0].

theorem TauCeti.Probability.Contractable.covariance_blockAverage_of_disjoint {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_L2 : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 μ) {n m : ℕ} (hn : 0 < n) (hm : 0 < m) {k : Fin n → ℕ} {k' : Fin m → ℕ} (hdisj : ∀ (i : Fin n) (j : Fin m), k i ≠ k' j) : ProbabilityTheory.covariance (blockAverage X k) (blockAverage X k') μ = ProbabilityTheory.covariance (X 0) (X 1) μ

The covariance of two disjoint block averages of a contractable L² sequence. Two block averages over selections k : Fin n → ℕ and k' : Fin m → ℕ with disjoint ranges (0 < n, 0 < m) have covariance exactly the common off-diagonal covariance c = cov[X 0, X 1], regardless of the two block lengths.

theorem TauCeti.Probability.Contractable.variance_blockAverage_sub_of_disjoint {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_L2 : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 μ) {n m : ℕ} (hn : 0 < n) (hm : 0 < m) {k : Fin n → ℕ} {k' : Fin m → ℕ} (hk : Function.Injective k) (hk' : Function.Injective k') (hdisj : ∀ (i : Fin n) (j : Fin m), k i ≠ k' j) : ProbabilityTheory.variance (blockAverage X k - blockAverage X k') μ = (ProbabilityTheory.variance (X 0) μ - ProbabilityTheory.covariance (X 0) (X 1) μ) / ↑n + (ProbabilityTheory.variance (X 0) μ - ProbabilityTheory.covariance (X 0) (X 1) μ) / ↑m

The two-window L² bound for block averages. For a contractable real-valued process with L² coordinates, two block averages over injective selections k : Fin n → ℕ and k' : Fin m → ℕ with disjoint ranges (0 < n, 0 < m) satisfy

Var[blockAverage X k - blockAverage X k'] = (v - c) / n + (v - c) / m,

where v = Var[X 0] and c = cov[X 0, X 1]. The bound vanishes as the block lengths grow, which is the analytic core of the L² route to de Finetti's theorem.

theorem TauCeti.Probability.Contractable.integral_sq_blockAverage_sub_of_disjoint {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_L2 : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 μ) {n m : ℕ} (hn : 0 < n) (hm : 0 < m) {k : Fin n → ℕ} {k' : Fin m → ℕ} (hk : Function.Injective k) (hk' : Function.Injective k') (hdisj : ∀ (i : Fin n) (j : Fin m), k i ≠ k' j) : ∫ (ω : Ω), (blockAverage X k ω - blockAverage X k' ω) ^ 2 ∂μ = (ProbabilityTheory.variance (X 0) μ - ProbabilityTheory.covariance (X 0) (X 1) μ) / ↑n + (ProbabilityTheory.variance (X 0) μ - ProbabilityTheory.covariance (X 0) (X 1) μ) / ↑m

The two-window L² distance for block averages. Since two disjoint block averages of a contractable process share the common mean μ[X 0], the two-window variance bound is the squared L² distance between them:

∫ (blockAverage X k - blockAverage X k')² dμ = (v - c) / n + (v - c) / m.