Exchangeable laws are stationary

This file records the Layer 0 stationarity bridge from the Exchangeability roadmap: a finitely exchangeable process has a shift-invariant path law. The existing implication Exchangeable.contractable gives the exchangeability-to-contractability bridge. The lemmas here first expose the shift-stationarity consequences at the natural Contractable level, then provide thin Exchangeable-named wrappers for downstream code that starts from exchangeability.

The bridge is stated for the one-sided shift and its iterates. The final processShift form packages the same invariance at the process-law level.

theorem TauCeti.Probability.Contractable.measurePreserving_shift_iterate {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (n : ℕ) : MeasureTheory.MeasurePreserving (shift α)^[n] (pathLaw μ X) (pathLaw μ X)

Every iterate of the one-sided shift preserves the path law of a contractable process.

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

Iterating the one-sided shift leaves the path law of a contractable process unchanged.

theorem TauCeti.Probability.Contractable.pathLaw_preimage_shift_iterate {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (n : ℕ) {s : Set (ℕ → α)} (hs : MeasureTheory.NullMeasurableSet s (pathLaw μ X)) : (pathLaw μ X) ((shift α)^[n] ⁻¹' s) = (pathLaw μ X) s

Setwise stationarity for every shift iterate of a contractable process.

theorem TauCeti.Probability.Contractable.map_processShift_eq_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (n : ℕ) : MeasureTheory.Measure.map (processShift X n) μ = pathLaw μ X

The law of the n-step shifted process of a contractable process is the original path law.

theorem TauCeti.Probability.Contractable.map_prefixProj_shift_iterate_pathLaw_eq_prefixLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (n m : ℕ) : MeasureTheory.Measure.map (prefixProj α m) (MeasureTheory.Measure.map (shift α)^[n] (pathLaw μ X)) = prefixLaw μ X m

Prefix laws are unchanged after shifting a contractable process by any finite amount.

theorem TauCeti.Probability.Exchangeable.measurePreserving_shift {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Exchangeable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : MeasureTheory.MeasurePreserving (shift α) (pathLaw μ X) (pathLaw μ X)

An exchangeable process has a shift-invariant path law.

theorem TauCeti.Probability.Exchangeable.measurePreserving_shift_iterate {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Exchangeable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (n : ℕ) : MeasureTheory.MeasurePreserving (shift α)^[n] (pathLaw μ X) (pathLaw μ X)

Every iterate of the one-sided shift preserves the path law of an exchangeable process.

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

Iterating the one-sided shift leaves the path law of an exchangeable process unchanged.

theorem TauCeti.Probability.Exchangeable.pathLaw_preimage_shift_iterate {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Exchangeable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (n : ℕ) {s : Set (ℕ → α)} (hs : MeasureTheory.NullMeasurableSet s (pathLaw μ X)) : (pathLaw μ X) ((shift α)^[n] ⁻¹' s) = (pathLaw μ X) s

Setwise stationarity for every shift iterate.

theorem TauCeti.Probability.Exchangeable.map_processShift_eq_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Exchangeable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (n : ℕ) : MeasureTheory.Measure.map (processShift X n) μ = pathLaw μ X

The law of the n-step shifted process of an exchangeable process is the original path law.

theorem TauCeti.Probability.Exchangeable.map_prefixProj_shift_iterate_pathLaw_eq_prefixLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Exchangeable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (n m : ℕ) : MeasureTheory.Measure.map (prefixProj α m) (MeasureTheory.Measure.map (shift α)^[n] (pathLaw μ X)) = prefixLaw μ X m

Prefix laws are unchanged after shifting an exchangeable process by any finite amount.