Contractable laws on path space

This file adds the path-law formulation of contractability, also called spreadability: a measure on ℕ → α is invariant under every strictly increasing reindexing of time. The process-level predicate Contractable μ X remains the main stochastic-process API; ContractableLaw names the equivalent path-space viewpoint needed by the de Finetti factorization and path-space dynamics.

This is the contractability analogue of ExchangeableLaw. It realizes the Exchangeability roadmap's Layer 0 request for the characterization of contractability by strictly increasing maps ℕ → ℕ, with finite-dimensional marginal consequences. The process-level ↔ path-law bridges live in TauCeti.Probability.Exchangeability.PathSpace.Law.Bridge, which imports this file and Contractability; no Mathlib infrastructure is vendored.

def TauCeti.Probability.ContractableLaw {α : Type u_2} [MeasurableSpace α] (ρ : MeasureTheory.Measure (ℕ → α)) : Prop

A measure on one-sided path space is contractable, or spreadable, if it is invariant under every strictly increasing reindexing of the time coordinate.

Equations

• TauCeti.Probability.ContractableLaw ρ = ∀ (φ : ℕ → ℕ), StrictMono φ → MeasureTheory.Measure.map (fun (x : ℕ → α) (k : ℕ) => x (φ k)) ρ = ρ

theorem TauCeti.Probability.ContractableLaw.intro {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (h : ∀ (φ : ℕ → ℕ), StrictMono φ → MeasureTheory.Measure.map (fun (x : ℕ → α) (k : ℕ) => x (φ k)) ρ = ρ) : ContractableLaw ρ

Constructor for ContractableLaw from the defining map invariance.

@[simp]

theorem TauCeti.Probability.contractableLaw_iff {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} : ContractableLaw ρ ↔ ∀ (φ : ℕ → ℕ), StrictMono φ → MeasureTheory.Measure.map (fun (x : ℕ → α) (k : ℕ) => x (φ k)) ρ = ρ

Simp normal form for ContractableLaw.

theorem TauCeti.Probability.ContractableLaw.map_reindex {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) {φ : ℕ → ℕ} (hφ : StrictMono φ) : MeasureTheory.Measure.map (fun (x : ℕ → α) (k : ℕ) => x (φ k)) ρ = ρ

The defining invariance of a contractable path law.

theorem TauCeti.Probability.ContractableLaw.measurePreserving_reindex {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) {φ : ℕ → ℕ} (hφ : StrictMono φ) : MeasureTheory.MeasurePreserving (fun (x : ℕ → α) (k : ℕ) => x (φ k)) ρ ρ

A strictly increasing time reindexing preserves a contractable path law.

theorem TauCeti.Probability.contractableLaw_iff_forall_measurePreserving_reindex {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} : ContractableLaw ρ ↔ ∀ (φ : ℕ → ℕ), StrictMono φ → MeasureTheory.MeasurePreserving (fun (x : ℕ → α) (k : ℕ) => x (φ k)) ρ ρ

Path-law contractability is equivalently measure preservation by every strictly increasing time reindexing.

theorem TauCeti.Probability.ContractableLaw.map_prefixProj_of_strictMono {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) {n : ℕ} {k : Fin n → ℕ} (hk : StrictMono k) : MeasureTheory.Measure.map (fun (x : ℕ → α) (i : Fin n) => x (k i)) ρ = MeasureTheory.Measure.map (prefixProj α n) ρ

The finite marginal of a contractable path law along any strictly increasing selection k : Fin n → ℕ equals its first-n prefix marginal.

theorem TauCeti.Probability.contractableLaw_iff_forall_map_prefixProj_of_strictMono {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] : ContractableLaw ρ ↔ ∀ (n : ℕ) (k : Fin n → ℕ), StrictMono k → MeasureTheory.Measure.map (fun (x : ℕ → α) (i : Fin n) => x (k i)) ρ = MeasureTheory.Measure.map (prefixProj α n) ρ

For finite path laws, contractability is equivalently invariance of every finite-dimensional marginal under strictly increasing finite selections.

theorem TauCeti.Probability.ContractableLaw.measurePreserving_shift {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) : MeasureTheory.MeasurePreserving (shift α) ρ ρ

A contractable path law is preserved by the one-sided shift.

theorem TauCeti.Probability.ContractableLaw.measurePreserving_shift_iterate {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) (n : ℕ) : MeasureTheory.MeasurePreserving (shift α)^[n] ρ ρ

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

theorem TauCeti.Probability.ContractableLaw.map_shift {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) : MeasureTheory.Measure.map (shift α) ρ = ρ

The one-sided shift leaves a contractable path law unchanged.

theorem TauCeti.Probability.ContractableLaw.map_shift_iterate {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ContractableLaw ρ) (n : ℕ) : MeasureTheory.Measure.map (shift α)^[n] ρ = ρ

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