Quantitative correlation decay forces time averages to the space average

Category: 1-Mathlib. Nothing here mentions CSD; this is elementary ergodic-theory-flavoured measure theory, and it is the engine the equilibration arc's E4 needs (specs/equilibration-arc-plan.md).

The statement, and why it is shaped this way

E4 wants: if the flow has decaying correlations, then time-averaged observables converge to the space average, at a rate controlled by that decay — explicitly conditional; mixing is never proved here or anywhere in the corpus.

The antecedent is deliberately quantitative correlation decay (HasCorrelationDecay), an explicit bound |⟨(f∘Φ^s)(f∘Φ^t)⟩ − ⟨f⟩²| ≤ ε (dist s t), rather than abstract mixing. That choice is the difference between a feasible brick and a blocked one:

• Mathlib has no mixing definition and no pointwise Birkhoff theorem (the standing row in MATHLIB-GAPS.md), so routing through abstract ergodic theory stops immediately.
• Mathlib does have the von Neumann mean ergodic theorem (ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection) — the arc plan's wall note claiming otherwise was stale and is corrected at source. But it is not what E4 needs: it gives no rate, and its limit is the orthogonal projection onto the invariant subspace, which equals the space average only under an ergodicity hypothesis. Correlation decay delivers both the rate and the identification of the limit, and needs no upstream ergodic theorem at all.

From the quantitative antecedent the Cesàro estimate is elementary: expand the square of the Birkhoff average, and the double sum is controlled by counting how often each distance occurs.

What is proved

• sum_sum_nat_dist_le — the counting bound: a nonnegative weight depending only on Nat.dist is counted at most twice per value across a T × T block;
• HasCorrelationDecay — the antecedent, and HasCorrelationDecay.nonneg;
• ★ integral_birkhoffAverage_sub_sq_le — the sharp L² estimate, in double-sum form;
• ★★ integral_birkhoffAverage_sub_sq_le_cesaro — the usable form, E[(A_T f − ⟨f⟩)²] ≤ (2/T) Σ_{u<T} ε u;
• ★★ tendsto_integral_birkhoffAverage_sub_sq — if ε is summable then the time averages converge to the space average in L², which is E4's consequent;
• integral_iterate_of_measurePreserving and HasCorrelationDecay.of_measurePreserving — the bridge supplying both hypotheses from a measure-preserving map plus a one-lag bound;
• ★★ HasCorrelationDecay.integral_mul_self_eq_of_recurrent — the sharpness direction: if the correlation returns near its lag-zero value at arbitrarily large lags, decay forces an a.e. constant observable. ★ …_of_periodic is the special case where it returns exactly.

⚠️ Honest scope

• Mixing is not proved, and no dynamics is exhibited. Everything is conditional on HasCorrelationDecay, which is a hypothesis about a particular Φ, f and ε. Whether any Σ-flow satisfies it is the separate question E5 asks; a non-vacuity witness is required before any of this may be described as equilibration of anything in particular.
• Discrete time. Φ^[t] iterates a single map. A continuous one-parameter flow enters by sampling at a fixed timestep; the continuous-time statement is not proved.
• The mean-stationarity hypothesis hmean is stated directly (⟨f∘Φ^t⟩ = ⟨f⟩) rather than derived from MeasurePreserving, so that the analytic core has no dynamics in it at all. HasCorrelationDecay.of_measurePreserving is the bridge for the measure-preserving case.
• Convergence is proved in L². On a probability space that implies convergence in measure by Chebyshev, but the in-measure form is not stated here — no theorem below mentions μ {x | δ ≤ |A_T f x − ⟨f⟩|}. Almost-everywhere convergence is a different matter: it is what pointwise Birkhoff would buy and is not available.
• The observable must be bounded (hfb), which is what keeps every integrability side condition trivial. Unbounded L² observables would need a genuine L² argument.

Reference: specs/equilibration-arc-plan.md (E4); MATHLIB-GAPS.md (the Birkhoff row); specs/future-work.md.

The pair-distance counting bound

theorem MeasureTheory.sum_sum_nat_dist_le {ε : ℕ → ℝ} {T : ℕ} (hε : ∀ u < T, 0 ≤ ε u) : ∑ s ∈ Finset.range T, ∑ t ∈ Finset.range T, ε (s.dist t) ≤ 2 * ↑T * ∑ u ∈ Finset.range T, ε u

Each distance is counted at most twice per row. For a nonnegative weight ε depending only on Nat.dist, the total over a T × T block is at most 2T Σ_{u<T} ε u.

This is the whole combinatorial content of the Cesàro estimate below: within a row s, the map t ↦ Nat.dist s t is injective on each side of the diagonal separately (not globally — the truncated subtraction t - s collapses the whole left half to 0), so the row splits into two injective pieces, each of which reindexes into range T.

The antecedent

def MeasureTheory.HasCorrelationDecay {X : Type u_1} [MeasurableSpace X] (μ : Measure X) (Φ : X → X) (f : X → ℝ) (ε : ℕ → ℝ) : Prop

Quantitative correlation decay — E4's antecedent, and the only hypothesis about the dynamics anywhere in this file. The pair correlation of f along the iterates of Φ sits within ε (Nat.dist s t) of the product of means.

Stated as an explicit bound rather than as abstract mixing, deliberately: see the module header. Any prose derived from the theorems below must carry this hypothesis with it — nothing here says that any particular dynamics satisfies it.

Equations

• MeasureTheory.HasCorrelationDecay μ Φ f ε = ∀ (s t : ℕ), |∫ (x : X), f (Φ^[s] x) * f (Φ^[t] x) ∂μ - (∫ (y : X), f y ∂μ) ^ 2| ≤ ε (s.dist t)

theorem MeasureTheory.HasCorrelationDecay.nonneg {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {Φ : X → X} {f : X → ℝ} {ε : ℕ → ℝ} (h : HasCorrelationDecay μ Φ f ε) (u : ℕ) : 0 ≤ ε u

A decay envelope is automatically nonnegative — it dominates an absolute value.

def MeasureTheory.HasCorrelationDecayUpTo {X : Type u_1} [MeasurableSpace X] (μ : Measure X) (Φ : X → X) (f : X → ℝ) (ε : ℕ → ℝ) (T : ℕ) : Prop

Finite-horizon correlation decay — the antecedent weakened to a bounded window of lags.

This is the escape route from the arc's own no-go. E6 (CSD.Thermo.not_hasCorrelationDecay_blockPop_of_unitary) shows that no unitary flow on a finite-dimensional space can satisfy HasCorrelationDecay with a summable envelope: its powers recur, so the correlations recur too. That argument needs the bound at arbitrarily large lags. Over a bounded window it says nothing, and a unitary flow on a large space can decorrelate for a very long time before recurring — which is what a physical environment actually does.

So the theorems below are the honest form for finite-dimensional dynamics: a statement at horizon T, with no asymptotics and no conflict with E6. See specs/q12-fibre-mechanism-scoping.md (W1, and Q12-d route 2).

Equations

• MeasureTheory.HasCorrelationDecayUpTo μ Φ f ε T = ∀ (s t : ℕ), s < T → t < T → |∫ (x : X), f (Φ^[s] x) * f (Φ^[t] x) ∂μ - (∫ (y : X), f y ∂μ) ^ 2| ≤ ε (s.dist t)

theorem MeasureTheory.HasCorrelationDecay.upTo {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {Φ : X → X} {f : X → ℝ} {ε : ℕ → ℝ} (h : HasCorrelationDecay μ Φ f ε) (T : ℕ) : HasCorrelationDecayUpTo μ Φ f ε T

Asymptotic decay is finite-horizon decay at every horizon.

theorem MeasureTheory.HasCorrelationDecayUpTo.nonneg {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {Φ : X → X} {f : X → ℝ} {ε : ℕ → ℝ} {T : ℕ} (h : HasCorrelationDecayUpTo μ Φ f ε T) {u : ℕ} (hu : u < T) : 0 ≤ ε u

★ The Cesàro estimate

theorem MeasureTheory.integral_birkhoffAverage_sub_sq_le {X : Type u_1} [MeasurableSpace X] {μ : Measure X} [IsProbabilityMeasure μ] {Φ : X → X} {f : X → ℝ} {ε : ℕ → ℝ} {C : ℝ} (hΦ : Measurable Φ) (hf : Measurable f) (hC : 0 ≤ C) (hfb : ∀ (x : X), |f x| ≤ C) (hmean : ∀ (t : ℕ), ∫ (x : X), f (Φ^[t] x) ∂μ = ∫ (y : X), f y ∂μ) {T : ℕ} (hdec : HasCorrelationDecayUpTo μ Φ f ε T) (hT : 0 < T) : ∫ (x : X), (birkhoffAverage ℝ Φ f T x - ∫ (y : X), f y ∂μ) ^ 2 ∂μ ≤ (↑T ^ 2)⁻¹ * ∑ s ∈ Finset.range T, ∑ t ∈ Finset.range T, ε (s.dist t)

★ The sharp L² Cesàro estimate. The mean square deviation of the Birkhoff average from the space average is controlled by the correlation envelope over the T × T block of time pairs.

Note what is not assumed: no ergodicity, no mixing, no measure-preservation. The only inputs are that f is bounded and measurable, that its mean is stationary (hmean), and the quantitative decay.

theorem MeasureTheory.integral_birkhoffAverage_sub_sq_le_cesaro {X : Type u_1} [MeasurableSpace X] {μ : Measure X} [IsProbabilityMeasure μ] {Φ : X → X} {f : X → ℝ} {ε : ℕ → ℝ} {C : ℝ} (hΦ : Measurable Φ) (hf : Measurable f) (hC : 0 ≤ C) (hfb : ∀ (x : X), |f x| ≤ C) (hmean : ∀ (t : ℕ), ∫ (x : X), f (Φ^[t] x) ∂μ = ∫ (y : X), f y ∂μ) {T : ℕ} (hdec : HasCorrelationDecayUpTo μ Φ f ε T) (hT : 0 < T) : ∫ (x : X), (birkhoffAverage ℝ Φ f T x - ∫ (y : X), f y ∂μ) ^ 2 ∂μ ≤ 2 * (↑T)⁻¹ * ∑ u ∈ Finset.range T, ε u

★★ The Cesàro estimate in usable form: the mean square deviation of the time average from the space average is at most (2/T) Σ_{u<T} ε u.

The factor two is the counting bound sum_sum_nat_dist_le: across the T × T block of time pairs each distance occurs at most twice per row.

theorem MeasureTheory.tendsto_integral_birkhoffAverage_sub_sq {X : Type u_1} [MeasurableSpace X] {μ : Measure X} [IsProbabilityMeasure μ] {Φ : X → X} {f : X → ℝ} {ε : ℕ → ℝ} {C : ℝ} (hΦ : Measurable Φ) (hf : Measurable f) (hC : 0 ≤ C) (hfb : ∀ (x : X), |f x| ≤ C) (hmean : ∀ (t : ℕ), ∫ (x : X), f (Φ^[t] x) ∂μ = ∫ (y : X), f y ∂μ) (hdec : HasCorrelationDecay μ Φ f ε) (hsum : Summable ε) : Filter.Tendsto (fun (T : ℕ) => ∫ (x : X), (birkhoffAverage ℝ Φ f T x - ∫ (y : X), f y ∂μ) ^ 2 ∂μ) Filter.atTop (nhds 0)

★★ E4's consequent. If the correlation envelope is summable, the time averages converge to the space average in L².

This is equilibration conditional on decay — the hypothesis hdec is doing all the work and must travel with any statement derived from this theorem. Nothing here exhibits a dynamics with decaying correlations.

★ The antecedent has teeth: periodic dynamics cannot satisfy it

theorem MeasureTheory.HasCorrelationDecay.integral_mul_self_eq_of_recurrent {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {Φ : X → X} {f : X → ℝ} {ε : ℕ → ℝ} (hrec : ∀ (δ : ℝ), 0 < δ → ∀ (M : ℕ), ∃ (u : ℕ), M ≤ u ∧ |∫ (x : X), f x * f (Φ^[u] x) ∂μ - ∫ (x : X), f x * f x ∂μ| < δ) (hdec : HasCorrelationDecay μ Φ f ε) (hsum : Summable ε) : ∫ (x : X), f x * f x ∂μ = (∫ (y : X), f y ∂μ) ^ 2

★★ Recurrence of the correlation function kills decay. If the correlation returns arbitrarily close to its lag-zero value ⟨f²⟩ at arbitrarily large lags, then a summable envelope forces ⟨f²⟩ = ⟨f⟩² — an a.e. constant observable.

This is the sharpness statement for HasCorrelationDecay, and hrec is exactly the property that almost periodic dynamics has: a system that keeps returning near its starting configuration cannot have correlations that fade. Two systems of interest satisfy hrec: periodic maps (below, exactly) and unitary flows on a finite-dimensional space (CSD.Thermo, via compactness of the unitary group).

The proof is a three-term triangle inequality: ⟨f²⟩ is near C u by recurrence, C u is near ⟨f⟩² by decay, and both gaps can be made smaller than half of |⟨f²⟩ − ⟨f⟩²|.

theorem MeasureTheory.HasCorrelationDecay.integral_mul_self_eq_of_periodic {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {Φ : X → X} {f : X → ℝ} {ε : ℕ → ℝ} {k : ℕ} (hk : 0 < k) (hper : Φ^[k] = id) (hdec : HasCorrelationDecay μ Φ f ε) (hsum : Summable ε) : ∫ (x : X), f x * f x ∂μ = (∫ (y : X), f y ∂μ) ^ 2

★ A periodic map forces zero variance — the special case of integral_mul_self_eq_of_recurrent in which the correlation does not merely return near ⟨f²⟩ but hits it exactly, at every multiple of the period.

Every measure-preserving map of a finite or countable probability space is periodic on its support, so no such space carries a non-trivial witness: a genuine one needs a non-atomic space, which is why CorrelationDecayWitness builds on the circle.

The measure-preserving bridge

The analytic core above deliberately takes hmean and the two-index decay as bare hypotheses, so that it contains no dynamics at all. These two lemmas supply both from the natural inputs: a measure-preserving map and a one-lag decay bound, which is what a physical estimate actually provides.

theorem MeasureTheory.integral_comp_of_measurePreserving {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {Ψ : X → X} (hΨ : MeasurePreserving Ψ μ μ) {f : X → ℝ} (hf : AEStronglyMeasurable f μ) : ∫ (x : X), f (Ψ x) ∂μ = ∫ (y : X), f y ∂μ

Precomposing with a measure-preserving self-map does not change an integral.

theorem MeasureTheory.integral_iterate_of_measurePreserving {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {Φ : X → X} (hΦ : MeasurePreserving Φ μ μ) {f : X → ℝ} (hf : AEStronglyMeasurable f μ) (t : ℕ) : ∫ (x : X), f (Φ^[t] x) ∂μ = ∫ (y : X), f y ∂μ

Along a measure-preserving map, the mean of an observable is stationary — this is hmean.

theorem MeasureTheory.integral_eq_zero_of_measurePreserving_neg {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {Ψ : X → X} (hΨ : MeasurePreserving Ψ μ μ) {g : X → ℝ} (hg : Integrable g μ) (hflip : ∀ (x : X), g (Ψ x) = -g x) : ∫ (x : X), g x ∂μ = 0

An odd symmetry kills an integral. If some measure-preserving involution-like translation negates the integrand, the integral vanishes — the sign-flip argument of Q24, in the form the circle witness uses.

theorem MeasureTheory.HasCorrelationDecay.of_measurePreserving {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {Φ : X → X} {f : X → ℝ} {ε : ℕ → ℝ} (hΦ : MeasurePreserving Φ μ μ) (hf : Measurable f) (hlag : ∀ (u : ℕ), |∫ (x : X), f x * f (Φ^[u] x) ∂μ - (∫ (y : X), f y ∂μ) ^ 2| ≤ ε u) : HasCorrelationDecay μ Φ f ε

From a one-lag bound to the two-index antecedent. For a measure-preserving map the pair correlation depends only on the lag, so a decay estimate at each lag u — the form a physical argument produces — gives HasCorrelationDecay.