Exchangeable path laws are contractable #
This file records the path-space form of the Layer 0 bridge from exchangeability to
contractability: an exchangeable finite measure on one-sided path space is invariant under
every strictly increasing reindexing of time. The process-level theorem remains available in
TauCeti.Probability.Exchangeability.Contractability; this file is the corresponding
ExchangeableLaw to ContractableLaw adapter.
theorem
TauCeti.Probability.ExchangeableLaw.contractableLaw
{α : Type u_1}
[MeasurableSpace α]
{ρ : MeasureTheory.Measure (ℕ → α)}
[MeasureTheory.IsFiniteMeasure ρ]
(hρ : ExchangeableLaw ρ)
:
An exchangeable finite path law is contractable: invariance under all permutations implies invariance under every strictly increasing time reindexing.