Full exchangeability and path-law bridges

The Layer 0 bridges between finite exchangeability, full exchangeability, and path-law endomorphisms:

• exchangeable_iff_fullyExchangeable — finite exchangeability (invariance under permutations of each Fin n) is equivalent to full exchangeability (invariance under all permutations of ℕ) for a process with a.e. measurable coordinates under a finite measure.
• FullyExchangeable.measurePreserving_shift — a fully exchangeable process has a shift-invariant path law, the bridge from symmetry to the Koopman/ergodic lane.
• fullyExchangeable_iff_forall_map_permReindex_pathLaw and fullyExchangeable_iff_forall_measurePreserving_permReindex — full exchangeability is equivalently invariance, or measure preservation, of the path law under every time-permutation reindexing map.

These bridges live together because they all identify the process-level symmetry FullyExchangeable μ X with corresponding path-law invariance statements. They are thin: they reuse the Layer 0 API and Mathlib — finite-marginal uniqueness (FiniteMarginals), the contractability bridge (Contractability), generic path-law reindexing, and Mathlib's finite permutation extension theorem — rather than new measure theory.

These declarations are adapted from the cameronfreer/exchangeability Layer 0 sources pinned at e0532e59ceff23edab44dda9ab0655debbc9cc22, with Tau Ceti API names and hypotheses.

theorem TauCeti.Probability.FullyExchangeable.exchangeableAt {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : FullyExchangeable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (n : ℕ) : ExchangeableAt μ X n

Full exchangeability implies finite exchangeability at each dimension n.

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

Full exchangeability implies finite exchangeability.

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

Finite exchangeability implies full exchangeability for a finite law with a.e. measurable coordinates: the path law is invariant under every permutation of ℕ.

theorem TauCeti.Probability.exchangeable_iff_fullyExchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : Exchangeable μ X ↔ FullyExchangeable μ X

Finite exchangeability ↔ full exchangeability for a process with a.e. measurable coordinates under a finite measure.

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

A fully exchangeable process has a shift-invariant path law — the Layer 0 shift-preservation bridge.

Path-law permutation reindexing

theorem TauCeti.Probability.map_permReindex_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (π : Equiv.Perm ℕ) : MeasureTheory.Measure.map (permReindex π) (pathLaw μ X) = pathLaw μ fun (k : ℕ) (ω : Ω) => X (π k) ω

Reindexing a path law by a time permutation gives the path law of the permuted process.

theorem TauCeti.Probability.fullyExchangeable_iff_forall_map_permReindex_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : FullyExchangeable μ X ↔ ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (permReindex π) (pathLaw μ X) = pathLaw μ X

Full exchangeability is exactly invariance of the path law under every time permutation.

theorem TauCeti.Probability.FullyExchangeable.map_permReindex_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : FullyExchangeable μ X) (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (π : Equiv.Perm ℕ) : MeasureTheory.Measure.map (permReindex π) (pathLaw μ X) = pathLaw μ X

A fully exchangeable process has path law invariant under any time permutation.

theorem TauCeti.Probability.FullyExchangeable.measurePreserving_permReindex {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : FullyExchangeable μ X) (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (π : Equiv.Perm ℕ) : MeasureTheory.MeasurePreserving (permReindex π) (pathLaw μ X) (pathLaw μ X)

Reindexing path space by any time permutation preserves the path law of a fully exchangeable process.

theorem TauCeti.Probability.fullyExchangeable_iff_forall_measurePreserving_permReindex {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : FullyExchangeable μ X ↔ ∀ (π : Equiv.Perm ℕ), MeasureTheory.MeasurePreserving (permReindex π) (pathLaw μ X) (pathLaw μ X)

Full exchangeability is exactly preservation of the path law by every time-permutation reindexing map.

theorem TauCeti.Probability.fullyExchangeable_of_forall_map_permReindex_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (h : ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (permReindex π) (pathLaw μ X) = pathLaw μ X) : FullyExchangeable μ X

If every time permutation preserves the path law, then the process is fully exchangeable.

theorem TauCeti.Probability.fullyExchangeable_of_forall_measurePreserving_permReindex {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (h : ∀ (π : Equiv.Perm ℕ), MeasureTheory.MeasurePreserving (permReindex π) (pathLaw μ X) (pathLaw μ X)) : FullyExchangeable μ X

A measure-preserving form of the path-law bridge: if every time permutation preserves the path law, then the process is fully exchangeable.