Shift Operator on Path Space

This file defines the left shift operator on infinite sequences ℕ → α and establishes its basic properties.

Main definitions

• shift: The left shift operator that maps ξ : ℕ → α to fun n => ξ (n + 1).
• IsShiftInvariant: Predicate for sets that are invariant under the shift map.

Main results

• shift_measurable: The shift operator is measurable.
• shift_comp_shift: Composing shift with itself gives fun ξ n => ξ (n + 2).
• isShiftInvariant_iff: Characterization of shift-invariant sets.

Implementation notes

The shift operator is fundamental in ergodic theory and the study of stationary processes. It appears in:

• Ergodic theory (Koopman operator, measure-preserving transformations)
• de Finetti's theorem (tail σ-algebras, shift-invariant σ-algebras)
• Martingale theory (reverse martingales, backward filtrations)

This file provides a single canonical definition to avoid duplication across the codebase.

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles
• Fristedt-Gray (1997), A Modern Approach to Probability Theory

@[reducible, inline]

abbrev PathSpace (α : Type u_1) : Type u_1

Path space: sequences indexed by ℕ taking values in α.

Equations

• Ω[α] = (ℕ → α)

def «termΩ[_]» : Lean.ParserDescr

Notation Ω[α] for path space ℕ → α.

Equations

• One or more equations did not get rendered due to their size.

def Exchangeability.PathSpace.shift {α : Type u_1} : (ℕ → α) → ℕ → α

The left shift operator on path space: (shift ξ) n = ξ (n + 1).

This is the fundamental shift operation that "drops the first element" of a sequence.

Equations

• Exchangeability.PathSpace.shift ξ n = ξ (n + 1)

@[simp]

theorem Exchangeability.PathSpace.shift_apply {α : Type u_1} (ξ : ℕ → α) (n : ℕ) : shift ξ n = ξ (n + 1)

theorem Exchangeability.PathSpace.shift_comp_shift {α : Type u_1} : shift ∘ shift = fun (ξ : ℕ → α) (n : ℕ) => ξ (n + 2)

Composing shift with itself is shift by 2. More generally, shift^n shifts by n.

theorem Exchangeability.PathSpace.shift_measurable {α : Type u_1} [MeasurableSpace α] : Measurable shift

The shift operator is measurable.

Proof: shift is measurable iff for all i, the composition (shift ξ) i is measurable. Since (shift ξ) i = ξ (i + 1), this is the projection onto coordinate (i + 1), which is measurable by definition of the product σ-algebra.

theorem Exchangeability.PathSpace.measurable_shift {α : Type u_1} [MeasurableSpace α] : Measurable shift

def Exchangeability.PathSpace.IsShiftInvariant {α : Type u_1} (S : Set (ℕ → α)) : Prop

A set in the path space is shift-invariant if it equals its preimage under the shift.

This is the analogue of T⁻¹(S) = S from classical ergodic theory.

Equations

• Exchangeability.PathSpace.IsShiftInvariant S = (Exchangeability.PathSpace.shift ⁻¹' S = S)

theorem Exchangeability.PathSpace.isShiftInvariant_iff {α : Type u_1} (S : Set (ℕ → α)) : IsShiftInvariant S ↔ ∀ (ξ : ℕ → α), ξ ∈ S ↔ shift ξ ∈ S