Path-space reindexing and iterates of the one-sided shift

This file records the elementary path-space API for iterating the one-sided shift TauCeti.Probability.shift: the shift-invariant σ-algebra on path space is built on them, as are comparisons of finite-dimensional path laws after discarding an initial block.

It also records how shift-fixed sets behave under time reindexing: preimage_reindex_eq_of_preimage_shift_eq_of_eventually_add shows that a reindexing which is eventually a translation n ↦ n + C leaves every set with shift α ⁻¹' A = A unchanged, because beyond the altered prefix the reindexing agrees with a fixed shift iterate. That is a purely set-theoretic statement — it assumes no measurability — and it is what lets a block argument move an invariant event through a reindexing; the complementary fact, that a contractable law is preserved by such a reindexing, needs strict monotonicity and lives with ContractableLaw.

The shift-specialized statements reuse the general time-reindexing path-law lemmas (measurable_reindex, map_reindex_pathLaw, map_reindex_prefixProj_pathLaw) from TauCeti.Probability.Process.PathLaw.Basic.

@[simp]

theorem TauCeti.Probability.shift_iterate_apply {α : Type u_2} (n k : ℕ) (x : ℕ → α) : (shift α)^[n] x k = x (k + n)

Iterating the one-sided shift by n drops the first n coordinates.

theorem TauCeti.Probability.shift_iterate_eq_reindex {α : Type u_2} (n : ℕ) : (shift α)^[n] = fun (x : ℕ → α) (k : ℕ) => x (k + n)

The nth shift iterate is the coordinate reindexing k ↦ k + n.

theorem TauCeti.Probability.measurable_shift_iterate {α : Type u_2} [MeasurableSpace α] (n : ℕ) : Measurable (shift α)^[n]

Every iterate of the one-sided path-space shift is measurable.

theorem TauCeti.Probability.aemeasurable_shift_iterate {α : Type u_2} [MeasurableSpace α] (n : ℕ) (μ : MeasureTheory.Measure (ℕ → α)) : AEMeasurable (shift α)^[n] μ

Every iterate of the one-sided path-space shift is a.e.-measurable with respect to any measure on path space.

@[simp]

theorem TauCeti.Probability.prefixProj_shift_iterate {α : Type u_2} (n m : ℕ) (x : ℕ → α) : prefixProj α m ((shift α)^[n] x) = fun (i : Fin m) => x (↑i + n)

A finite prefix after n shifts is the block of coordinates n, …, n + m - 1.

theorem TauCeti.Probability.measurable_prefixProj_shift_iterate {α : Type u_2} [MeasurableSpace α] (n m : ℕ) : Measurable fun (x : ℕ → α) => prefixProj α m ((shift α)^[n] x)

The prefix projection after an n-fold shift is measurable.

theorem TauCeti.Probability.map_shift_iterate_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (n : ℕ) : MeasureTheory.Measure.map (shift α)^[n] (pathLaw μ X) = pathLaw μ fun (k : ℕ) (ω : Ω) => X (k + n) ω

Shifting the path law by n gives the path law of the reindexed process k ↦ X (k + n).

theorem TauCeti.Probability.map_prefixProj_shift_iterate_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (n m : ℕ) : MeasureTheory.Measure.map (prefixProj α m) (MeasureTheory.Measure.map (shift α)^[n] (pathLaw μ X)) = blockLaw μ X fun (i : Fin m) => ↑i + n

The first m coordinates of the path law after n shifts are the block law along i ↦ i + n.

theorem TauCeti.Probability.map_prefixProj_shift_iterate_pathLaw_apply {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (n m : ℕ) (s : Set (Fin m → α)) : (MeasureTheory.Measure.map (prefixProj α m) (MeasureTheory.Measure.map (shift α)^[n] (pathLaw μ X))) s = (blockLaw μ X fun (i : Fin m) => ↑i + n) s

The setwise form of map_prefixProj_shift_iterate_pathLaw.

theorem TauCeti.Probability.preimage_reindex_eq_of_preimage_shift_eq_of_eventually_add {α : Type u_2} {m C : ℕ} {φ : ℕ → ℕ} {A : Set (ℕ → α)} (hshift : shift α ⁻¹' A = A) (hφ : ∀ (n : ℕ), m ≤ n → φ n = n + C) : (fun (x : ℕ → α) (k : ℕ) => x (φ k)) ⁻¹' A = A

Shift-fixed sets are fixed by an eventually-translating reindexing. If φ is eventually n ↦ n + C, then reindexing by φ leaves unchanged every set A exactly fixed by the shift, shift α ⁻¹' A = A. No measurability is assumed — this is a set-theoretic identity, and the MeasurableSpace.invariants formulation is the corollary preimage_reindex_eq_of_measurableSet_invariants_of_eventually_add.

Beyond the first m coordinates the reindexing agrees with (shift α)^[C], so the identity (shift α)^[m] (reindex φ x) = (shift α)^[m + C] x holds, and exact shift invariance of A under both iterates transfers membership.

Strict monotonicity of φ is not needed for this set identity; it enters separately, when ContractableLaw.measurePreserving_reindex turns the reindexing into a measure-preserving map. The two facts are the pair of inputs the Koopman block factorization needs.

The eventual-translation hypothesis is exactly the conclusion recorded by StrictMono.exists_strictMono_nat_extending_fin_eventually_add; this theorem is the consumer of that clause.

theorem TauCeti.Probability.comp_reindex_apply_eq_of_comp_shift_eq_of_eventually_add {α : Type u_2} {m C : ℕ} {φ : ℕ → ℕ} {β : Type u_3} {w : (ℕ → α) → β} (hw : w ∘ shift α = w) (hφ : ∀ (n : ℕ), m ≤ n → φ n = n + C) (x : ℕ → α) : (w fun (k : ℕ) => x (φ k)) = w x

A shift-invariant function is unchanged by such a reindexing, pointwise.

Each level set w ⁻¹' {c} is shift-invariant, so preimage_reindex_eq_of_preimage_shift_eq_of_eventually_add sends the reindexed point into the same level set as the original. Taking c = w x gives the claim.

No measure and no measurable structure appears: this is the raw form. Its invariants-measurable counterpart, comp_reindex_apply_eq_of_measurable_invariants_of_eventually_add, is in PathSpace/Invariant/Tail.lean, mirroring how the set-level raw and invariants-measurable forms are split between the two files.