L¹ convergence of Cesàro averages of a contractable process

This file proves the weighted_sums_converge_L1 milestone from Layer 3 of the Exchangeability roadmap. For a measurable real-valued observable f of a contractable process X with f ∘ X 0 square-integrable — in particular for any bounded f — the block averages

(m + 1)⁻¹ ∑_{i ≤ m} f(X_{k m i})

converge in L¹ to the same measurable limit, for every selection k that is injective for all sufficiently large lengths. The selection may move with the length: fixed-start windows k m i = r + i are one instance, and disjoint windows k m i = c * (m + 1) + i — which fixed starts cannot express — are another.

The proof first applies the two-window identity Contractable.integral_sq_blockAverage_sub_of_disjoint to compare two prefix averages through a third block disjoint from both. This makes the prefixes Cauchy in Mathlib's complete L² space. The same disjoint-block comparison shows that every such selection converges to the prefix limit: its bound depends on the block lengths and not on their positions, so a comparison block beyond the selection's range is available at every length. Finally, eLpNorm_le_eLpNorm_mul_rpow_measure_univ turns the L² convergence into L¹ convergence, at the cost of the fixed factor μ univ ^ (1 - 1/2).

The mathematical argument follows the elementary L² route around Theorem 1.1 in Kallenberg, Probabilistic Symmetries and Invariance Principles (2005). The theorem statement is adapted from weighted_sums_converge_L1 in cameronfreer/exchangeability at commit e0532e59ceff23edab44dda9ab0655debbc9cc22; the proof is rewritten around Tau Ceti's closed-form block-average covariance API.

theorem TauCeti.Probability.weighted_sums_converge_L1_of_memLp {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_ae : ∀ (i : ℕ), AEMeasurable (X i) μ) {f : α → ℝ} (hf : Measurable f) (hf_L2 : MeasureTheory.MemLp (fun (ω : Ω) => f (X 0 ω)) 2 μ) : ∃ (a : Ω → ℝ), Measurable a ∧ MeasureTheory.MemLp a 1 μ ∧ ∀ (k : (n : ℕ) → Fin (n + 1) → ℕ), (∀ᶠ (n : ℕ) in Filter.atTop, Function.Injective (k n)) → Filter.Tendsto (fun (m : ℕ) => ∫ (ω : Ω), |blockAverage (fun (i : ℕ) (ω : Ω) => f (X i ω)) (k m) ω - a ω| ∂μ) Filter.atTop (nhds 0)

A measurable observable of a contractable process whose composite with a single coordinate is square-integrable has moving injective block averages converging in L¹ to one common measurable limit.

The selection k m may move with the length m + 1, and need only be injective eventually — finitely many degenerate initial selections cannot affect a limit. This costs nothing because the underlying L² comparison is bounded in terms of the block lengths and not their positions. Fixed starts are the instance fixedStart r, with fixedStart_eventually_injective. Disjoint windows are the instance k m j = c * (m + 1) + j, which fixed starts cannot give: windows from distinct fixed starts overlap once the common length exceeds the gap between them.

The limit a does not depend on the selection: it is the prefix limit, so every moving selection converges to the same function. The successor in the length avoids assigning any special meaning to an empty average.

Contractability makes the mapped coordinates identically distributed, so square-integrability at coordinate 0 carries to all of them.

theorem TauCeti.Probability.weighted_sums_converge_L1 {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_ae : ∀ (i : ℕ), AEMeasurable (X i) μ) {f : α → ℝ} (hf : Measurable f) (hf_bdd : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C) : ∃ (a : Ω → ℝ), Measurable a ∧ MeasureTheory.MemLp a 1 μ ∧ ∀ (k : (n : ℕ) → Fin (n + 1) → ℕ), (∀ᶠ (n : ℕ) in Filter.atTop, Function.Injective (k n)) → Filter.Tendsto (fun (m : ℕ) => ∫ (ω : Ω), |blockAverage (fun (i : ℕ) (ω : Ω) => f (X i ω)) (k m) ω - a ω| ∂μ) Filter.atTop (nhds 0)

Bounded-observable form, the shape the Layer 3 roadmap names. A uniform bound on f gives square-integrability of the composite on a finite measure space, so this is the direct entry point for bounded observables.