The shift-invariant σ-algebra: its place below the path tail, and its stability under reindexing

For the one-sided shift on path space ℕ → α, an ambient-measurable event fixed by the shift is fixed by every iterate of the shift, and therefore depends only on the coordinates from an arbitrarily late time onward. This file proves that comparison,

MeasurableSpace.invariants (shift α) ≤ pathTail α,

and shows that the inclusion is strict: for Bool-valued paths, the tail event "the value true occurs at infinitely many even times" is not shift-invariant, because the shift exchanges even and odd times.

It also records how shift-invariant events behave under time reindexing: a reindexing that is eventually a translation leaves every exactly shift-invariant event unchanged (preimage_reindex_eq_of_preimage_shift_eq_of_eventually_add, with preimage_reindex_eq_of_measurableSet_invariants_of_eventually_add the invariant-measurable form). That is one of the two independent inputs a Koopman-style block argument needs — the other, measure preservation, comes from contractability and needs strict monotonicity, which this one does not. The function-level form lives beside its set-level counterpart in PathSpace/Shift.lean: a shift-invariant function is unchanged by such a reindexing, pointwise. The invariants-measurable corollary here is Mathlib's MeasurableSpace.comp_eq_of_measurable_invariants composed with it.

The Layer 2 exchangeability roadmap warns against silently identifying the tail σ-algebra with the shift-invariant σ-algebra for one-sided sequences; these two results are the exact form of that comparison. Combining with pathTail_le_exchangeableSigma from TauCeti.Probability.Exchangeability.PathSpace.Exchangeable.Sigma gives the chain

invariants (shift α) ≤ pathTail α ≤ exchangeableSigma α,

with the first inclusion strict already over Bool.

The engine of the positive direction is tailFamily_coord_eq_comap_shift_iterate: the future path σ-algebra from time n onward is the σ-algebra generated by the n-fold shift. That identity also gives the shift description pathTail_eq_iInf_comap_shift_iterate of the path tail σ-algebra.

Main results

Reindexing under an eventual translation:

• preimage_reindex_eq_of_measurableSet_invariants_of_eventually_add — such a reindexing fixes every invariants-measurable event;

• comp_reindex_apply_eq_of_measurable_invariants_of_eventually_add — and leaves every invariants-measurable function unchanged, pointwise. The raw form, comp_reindex_apply_eq_of_comp_shift_eq_of_eventually_add, is in PathSpace/Shift.lean.

• tailFamily_coord_eq_comap_shift_iterate

• pathTail_eq_iInf_comap_shift_iterate

• invariants_shift_le_pathTail

• invariants_shift_le_exchangeableSigma

• not_pathTail_le_invariants_shift

• invariants_shift_lt_pathTail

Future σ-algebras as shift preimages

theorem TauCeti.Probability.tailFamily_coord_eq_comap_shift_iterate {α : Type u_1} [MeasurableSpace α] (n : ℕ) : tailFamily (fun (k : ℕ) (x : ℕ → α) => x k) n = MeasurableSpace.comap (shift α)^[n] inferInstance

The future path σ-algebra from time n onward is the σ-algebra generated by the n-fold shift: an event depends only on the coordinates n, n + 1, … exactly when it is the preimage of an ambient-measurable event under (shift α)^[n].

theorem TauCeti.Probability.pathTail_eq_iInf_comap_shift_iterate {α : Type u_1} [MeasurableSpace α] : pathTail α = ⨅ (n : ℕ), MeasurableSpace.comap (shift α)^[n] inferInstance

The path tail σ-algebra is the intersection of the σ-algebras generated by the iterated shifts.

Shift-invariant events are tail events

theorem TauCeti.Probability.invariants_shift_le_pathTail {α : Type u_1} [MeasurableSpace α] : MeasurableSpace.invariants (shift α) ≤ pathTail α

A shift-invariant event is a tail event. A shift-invariant event is fixed by every iterate of the one-sided shift, hence for each n it is the preimage under (shift α)^[n] of an ambient-measurable event, so it depends only on the coordinates from time n onward.

theorem TauCeti.Probability.invariants_shift_le_exchangeableSigma {α : Type u_1} [MeasurableSpace α] : MeasurableSpace.invariants (shift α) ≤ exchangeableSigma α

A shift-invariant event is an exchangeable event: it is a tail event, and tail events are fixed by every finitely supported permutation of the time coordinate.

The inclusion is strict

The one-sided shift moves even times to odd times, so a tail event that refers to the even times only need not be shift-invariant. The witness below is the Bool-valued event "the value true occurs at infinitely many even times".

theorem TauCeti.Probability.not_pathTail_le_invariants_shift : ¬pathTail Bool ≤ MeasurableSpace.invariants (shift Bool)

The path tail σ-algebra is not contained in the shift-invariant σ-algebra: for Bool-valued paths, the tail event "the value true occurs at infinitely many even times" is not fixed by the one-sided shift, which carries the even times onto the odd ones.

theorem TauCeti.Probability.invariants_shift_lt_pathTail : MeasurableSpace.invariants (shift Bool) < pathTail Bool

For Bool-valued paths the inclusion invariants_shift_le_pathTail is strict: the shift-invariant σ-algebra is a proper sub-σ-algebra of the path tail σ-algebra.

theorem TauCeti.Probability.invariants_shift_lt_exchangeableSigma : MeasurableSpace.invariants (shift Bool) < exchangeableSigma Bool

For Bool-valued paths the shift-invariant σ-algebra is a proper sub-σ-algebra of the exchangeable σ-algebra.

theorem TauCeti.Probability.preimage_reindex_eq_of_measurableSet_invariants_of_eventually_add {α : Type u_1} [MeasurableSpace α] {m C : ℕ} {φ : ℕ → ℕ} {A : Set (ℕ → α)} (hA : MeasurableSet A) (hφ : ∀ (n : ℕ), m ≤ n → φ n = n + C) : (fun (x : ℕ → α) (k : ℕ) => x (φ k)) ⁻¹' A = A

Invariant events are fixed by an eventually-translating reindexing, in the MeasurableSpace.invariants-measurable form.

Deliberately not @[simp]: m and C occur only in the hypothesis hφ, never in the left-hand side, so simp cannot infer them and the rule would never fire.

theorem TauCeti.Probability.comp_reindex_apply_eq_of_measurable_invariants_of_eventually_add {α : Type u_1} [MeasurableSpace α] {m C : ℕ} {φ : ℕ → ℕ} {β : Type u_2} [MeasurableSpace β] [MeasurableSingletonClass β] {w : (ℕ → α) → β} (hw : Measurable w) (hφ : ∀ (n : ℕ), m ≤ n → φ n = n + C) (x : ℕ → α) : (w fun (k : ℕ) => x (φ k)) = w x

An invariants-measurable function is unchanged by such a reindexing, pointwise.

The invariants-measurable form of the above. Measurable singletons are needed only to pass from invariants-measurability to w ∘ shift α = w, which is Mathlib's MeasurableSpace.comp_eq_of_measurable_invariants; the displacement itself needs neither.

Compare the permutation analogue comp_permReindex_eq_of_measurable_exchangeableSigma.