Window Machinery for Cesàro Averages

This file defines finite windows of consecutive indices used to express Cesàro averages in the ViaL2 proof of de Finetti's theorem.

Main definitions

• window n k: The finset {n+1, n+2, ..., n+k} of k consecutive indices starting from n+1

Main results

• window_card: The window contains exactly k elements
• mem_window_iff: Characterization of window membership
• sum_window_eq_sum_fin: Sums over windows can be reindexed as sums over Fin k

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1

def Exchangeability.DeFinetti.ViaL2.window (n k : ℕ) : Finset ℕ

Finite window of consecutive indices.

The window {n+1, n+2, ..., n+k} represented as a Finset ℕ. Used to express Cesàro averages: (1/k) * ∑_{i ∈ window n k} f(X_i).

Equations

• Exchangeability.DeFinetti.ViaL2.window n k = Finset.image (fun (i : ℕ) => n + i + 1) (Finset.range k)

theorem Exchangeability.DeFinetti.ViaL2.window_card (n k : ℕ) : (window n k).card = k

The window contains exactly k elements.

theorem Exchangeability.DeFinetti.ViaL2.mem_window_iff {n k t : ℕ} : t ∈ window n k ↔ ∃ i < k, t = n + i + 1

Characterization of window membership.

theorem Exchangeability.DeFinetti.ViaL2.sum_window_eq_sum_fin {β : Type u_1} [AddCommMonoid β] (n k : ℕ) (g : ℕ → β) : ∑ t ∈ window n k, g t = ∑ i : Fin k, g (n + ↑i + 1)

Sum over a window of length k can be reindexed as a sum over Fin k.