Block averages of a real-valued process

The empirical mean of a process over a finite selection of coordinates, with its elementary algebra. Nothing here involves a measure: blockAverage X k is a function of ω, and the three lemmas below are the pointwise formula, the scaled-sum normal form, and the value on a constant block. average_sub_sq_eq_sum_sum records the one further piece of average algebra used downstream: the square of a deviation from an average, expanded as a double sum. birkhoffAverage_eq_prefixAverage identifies a Birkhoff average of an arbitrary self-map with a prefix average of the iterated observable, which is how Mathlib's mean-ergodic theory reaches this API; it is stated for an arbitrary self-map because no dynamical content enters — both sides are the same normalised sum.

It also carries the standard selections, all measure-free. prefixAverage X n averages the first n coordinates and followingAverage X n the n after them, with their pointwise formulas.

fixedStart r is the same fixed-start window in moving-selection form — a family ∀ n, Fin (n + 1) → ℕ rather than a single block — which is the shape the L² convergence theorems quantify over. It belongs here because it is a generic block selection with no disjointness content; the disjoint windows those theorems also accept are disjointWindow in Process/DisjointWindow.lean. fixedStart_injective gives injectivity at each length and fixedStart_eventually_injective the eventual form the limit theorems take.

Measure-theoretic facts about all three — square-integrability, conditional expectations, variances and covariances under contractability — live with the L² averaging library in Exchangeability/L2/BlockAverages.lean and Exchangeability/L2/LongTailAverages.lean, which import this module. Keeping the definitions here means a route that only needs the algebra does not import the L² machinery to get them: the Koopman route needs prefixAverage to state its Birkhoff bridge, and has no L² content of its own.

noncomputable def TauCeti.Probability.blockAverage {Ω : Type u_1} (X : ℕ → Ω → ℝ) {n : ℕ} (k : Fin n → ℕ) : Ω → ℝ

The block average of a real-valued process X over a finite selection k : Fin n → ℕ: the empirical mean n⁻¹ • ∑ i, X (k i) of the block (X (k i))ᵢ.

Equations

• TauCeti.Probability.blockAverage X k = Finset.univ.expect fun (i : Fin n) => X (k i)

@[simp]

theorem TauCeti.Probability.blockAverage_apply {Ω : Type u_1} {X : ℕ → Ω → ℝ} {n : ℕ} (k : Fin n → ℕ) (ω : Ω) : blockAverage X k ω = (↑n)⁻¹ * ∑ i : Fin n, X (k i) ω

The pointwise formula for a block average: at each ω it is the normalised finite sum n⁻¹ * ∑ i, X (k i) ω.

theorem TauCeti.Probability.blockAverage_eq_sum {Ω : Type u_1} {X : ℕ → Ω → ℝ} {n : ℕ} (k : Fin n → ℕ) : blockAverage X k = (↑n)⁻¹ • ∑ i : Fin n, X (k i)

A block average as a real-scaled finite sum.

theorem TauCeti.Probability.blockAverage_apply_of_forall_eq {Ω : Type u_1} {X : ℕ → Ω → ℝ} {n : ℕ} (hn : 0 < n) {k : Fin n → ℕ} {ω : Ω} {c : ℝ} (h : ∀ (i : Fin n), X (k i) ω = c) : blockAverage X k ω = c

A block average of a constant block. If every coordinate of a nonempty block takes the value c at ω, then so does the block average: the normalisation n⁻¹ cancels the n terms.

noncomputable def TauCeti.Probability.prefixAverage {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) : Ω → ℝ

The average of the first n coordinates of a real-valued process.

Equations

• TauCeti.Probability.prefixAverage X n = TauCeti.Probability.blockAverage X fun (i : Fin n) => ↑i

noncomputable def TauCeti.Probability.followingAverage {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) : Ω → ℝ

The average of the n coordinates immediately following the first n coordinates.

Equations

• TauCeti.Probability.followingAverage X n = TauCeti.Probability.blockAverage X fun (i : Fin n) => n + ↑i

theorem TauCeti.Probability.prefixAverage_def {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) : prefixAverage X n = blockAverage X fun (i : Fin n) => ↑i

A prefix average is the block average over the selection i ↦ i.

theorem TauCeti.Probability.followingAverage_def {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) : followingAverage X n = blockAverage X fun (i : Fin n) => n + ↑i

A following-block average is the block average over the selection i ↦ n + i.

@[simp]

theorem TauCeti.Probability.prefixAverage_apply {Ω : Type u_1} {X : ℕ → Ω → ℝ} (n : ℕ) (ω : Ω) : prefixAverage X n ω = (↑n)⁻¹ * ∑ i : Fin n, X (↑i) ω

The pointwise formula for a prefix average.

@[simp]

theorem TauCeti.Probability.followingAverage_apply {Ω : Type u_1} {X : ℕ → Ω → ℝ} (n : ℕ) (ω : Ω) : followingAverage X n ω = (↑n)⁻¹ * ∑ i : Fin n, X (n + ↑i) ω

The pointwise formula for a following-block average.

theorem TauCeti.Probability.prod_blockAverage_eq_expect {Ω : Type u_1} {m N : ℕ} (Y : Fin m → ℕ → Ω → ℝ) (k : Fin m → Fin N → ℕ) (ω : Ω) : ∏ i : Fin m, blockAverage (Y i) (k i) ω = Finset.univ.expect fun (js : Fin m → Fin N) => ∏ i : Fin m, Y i (k i (js i)) ω

A product of block averages is an average of products. Purely algebraic: the product of sums distributes by Fintype.prod_sum, and the normalisations multiply. Disjointness of the selections plays no role here — it matters only for what the individual terms mean.

def TauCeti.Probability.fixedStart (r n : ℕ) : Fin (n + 1) → ℕ

The fixed-start selection: the window of length n + 1 beginning at r.

Equations

• TauCeti.Probability.fixedStart r x✝ j = r + ↑j

@[simp]

theorem TauCeti.Probability.fixedStart_apply (r n : ℕ) (j : Fin (n + 1)) : fixedStart r n j = r + ↑j

theorem TauCeti.Probability.fixedStart_injective (r n : ℕ) : Function.Injective (fixedStart r n)

The fixed-start selection is injective at each length.

theorem TauCeti.Probability.fixedStart_eventually_injective (r : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, Function.Injective (fixedStart r n)

The eventual form, as the moving-selection theorems take it.

theorem TauCeti.Probability.average_sub_sq_eq_sum_sum {ι : Type u_2} {R : Type u_3} [Field R] [CharZero R] {s : Finset ι} (hs : s.Nonempty) (a : ι → R) (b : R) : ((↑s.card)⁻¹ * ∑ i ∈ s, a i - b) ^ 2 = (↑s.card)⁻¹ ^ 2 * ∑ i ∈ s, ∑ j ∈ s, (a i - b) * (a j - b)

The squared deviation of an average, as a double sum. For a nonempty finite index set s, the square of (#s)⁻¹ * ∑ i ∈ s, a i - b is (#s)⁻¹ ^ 2 times the double sum of (a i - b) * (a j - b) over s × s.

theorem TauCeti.Probability.birkhoffAverage_eq_prefixAverage {β : Type u_2} (T : β → β) (F : β → ℝ) (n : ℕ) : birkhoffAverage ℝ T F n = prefixAverage (fun (i : ℕ) (x : β) => F (T^[i] x)) n

A Birkhoff average is a prefix average of the iterated observable. For any self-map T and any real observable F, birkhoffAverage ℝ T F n is the prefix average of i ↦ F ∘ T^[i].

Nothing about any particular dynamical system enters: both sides are the same normalised sum. This is the bridge from Mathlib's mean-ergodic theory, which speaks of Birkhoff averages, to the block-average API, which speaks of averages of a process over a selection of coordinates.

The unit interval

A block average of [0,1]-valued coordinates stays in [0,1]. This is the bound the product convergence lemmas need, and it is pure order algebra — no measure and no norm is involved, so the ‖·‖ ≤ 1 form is left to the consumer that has a normed structure in scope.

theorem TauCeti.Probability.blockAverage_nonneg {Ω : Type u_1} {Y : ℕ → Ω → ℝ} {n : ℕ} {k : Fin n → ℕ} {ω : Ω} (hY : ∀ (i : Fin n), 0 ≤ Y (k i) ω) : 0 ≤ blockAverage Y k ω

A block average of nonnegative coordinates is nonnegative. Only the sampled coordinates at the one point ω are constrained.

theorem TauCeti.Probability.blockAverage_le_one {Ω : Type u_1} {Y : ℕ → Ω → ℝ} {n : ℕ} {k : Fin n → ℕ} {ω : Ω} (hY : ∀ (i : Fin n), Y (k i) ω ≤ 1) : blockAverage Y k ω ≤ 1

A block average of coordinates bounded by 1 is bounded by 1. Only the sampled coordinates at the one point ω are constrained.