Exchangeable laws on path space

This file adds the path-law formulation of full exchangeability for measures on ℕ → α. The process-level definitions in TauCeti.Probability.Exchangeability.Basic remain the main user-facing API for stochastic processes; ExchangeableLaw names the equivalent path-space viewpoint needed by π-system, invariant-σ-algebra, and shift arguments.

Everything here is pure path space: it depends only on the coordinate-reindexing and prefix machinery of Basic and Mathlib's finite permutation extension Equiv.Perm.exists_extending_pair. The process-level ↔ path-law bridges live in TauCeti.Probability.Exchangeability.PathSpace.Law.Bridge, which imports both this file and FullyExchangeable. No measure-theoretic infrastructure is vendored.

The closure theorem exchangeableLaw_map_prod_coding records that applying one jointly measurable coding function coordinatewise to independent parameter and exchangeable-noise laws preserves exchangeability.

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

A measure on one-sided path space is exchangeable if it is invariant under every permutation of the time coordinate.

Equations

• TauCeti.Probability.ExchangeableLaw ρ = ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (TauCeti.Probability.permReindex π) ρ = ρ

theorem TauCeti.Probability.ExchangeableLaw.intro {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (h : ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (permReindex π) ρ = ρ) : ExchangeableLaw ρ

Constructor for ExchangeableLaw from the defining map invariance.

@[simp]

theorem TauCeti.Probability.exchangeableLaw_iff {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} : ExchangeableLaw ρ ↔ ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (permReindex π) ρ = ρ

Simp normal form for ExchangeableLaw.

theorem TauCeti.Probability.ExchangeableLaw.map_permReindex {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ExchangeableLaw ρ) (π : Equiv.Perm ℕ) : MeasureTheory.Measure.map (permReindex π) ρ = ρ

The defining invariance of an exchangeable path law.

theorem TauCeti.Probability.ExchangeableLaw.measurePreserving_permReindex {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ExchangeableLaw ρ) (π : Equiv.Perm ℕ) : MeasureTheory.MeasurePreserving (permReindex π) ρ ρ

Reindexing by a time permutation preserves an exchangeable path law.

theorem TauCeti.Probability.exchangeableLaw_infinitePi_const {α : Type u_1} [MeasurableSpace α] (P : MeasureTheory.ProbabilityMeasure α) : ExchangeableLaw (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P)

An i.i.d. product law is exchangeable. Reindexing a constant product law by a permutation leaves every factor unchanged.

theorem TauCeti.Probability.exchangeableLaw_map_prod_coding {α : Type u_1} [MeasurableSpace α] {T : Type u_2} {β : Type u_3} [MeasurableSpace T] [MeasurableSpace β] (π : MeasureTheory.Measure T) [MeasureTheory.SFinite π] {ρ : MeasureTheory.Measure (ℕ → β)} [MeasureTheory.SFinite ρ] (hρ : ExchangeableLaw ρ) {f : T → β → α} (hf : Measurable (Function.uncurry f)) : ExchangeableLaw (MeasureTheory.Measure.map (fun (p : T × (ℕ → β)) (i : ℕ) => f p.1 (p.2 i)) (π.prod ρ))

Coordinatewise coding preserves exchangeability. Applying a jointly measurable f coordinatewise to a parameter and an independent exchangeable noise sequence gives an exchangeable law.

theorem TauCeti.Probability.exchangeableLaw_iff_forall_measurePreserving_permReindex {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} : ExchangeableLaw ρ ↔ ∀ (π : Equiv.Perm ℕ), MeasureTheory.MeasurePreserving (permReindex π) ρ ρ

Path-law exchangeability is equivalently measure preservation by every time permutation.

theorem TauCeti.Probability.map_reindex_prefixProj {α : Type u_1} [MeasurableSpace α] (ρ : MeasureTheory.Measure (ℕ → α)) (φ : ℕ → ℕ) (n : ℕ) : MeasureTheory.Measure.map (prefixProj α n) (MeasureTheory.Measure.map (fun (x : ℕ → α) (k : ℕ) => x (φ k)) ρ) = MeasureTheory.Measure.map (fun (x : ℕ → α) (i : Fin n) => x (φ ↑i)) ρ

The first-n prefix marginal of a path-space measure reindexed by φ : ℕ → ℕ is its finite coordinate marginal along i ↦ φ i. This only uses coordinate reindexing, so it holds for an arbitrary function φ, not just a permutation.

theorem TauCeti.Probability.ExchangeableLaw.map_prefixProj_of_injective {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ExchangeableLaw ρ) {n : ℕ} (k : Fin n → ℕ) (hk : Function.Injective k) : MeasureTheory.Measure.map (fun (x : ℕ → α) (i : Fin n) => x (k i)) ρ = MeasureTheory.Measure.map (prefixProj α n) ρ

The finite marginal of an exchangeable path law along any injective selection k : Fin n → ℕ equals its first-n prefix marginal: an exchangeable law has the same finite-dimensional distribution along every injective finite selection of coordinates.

theorem TauCeti.Probability.ExchangeableLaw.map_prefixProj_perm {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} (hρ : ExchangeableLaw ρ) (n : ℕ) (σ : Equiv.Perm (Fin n)) : MeasureTheory.Measure.map (fun (x : ℕ → α) (i : Fin n) => x ↑(σ i)) ρ = MeasureTheory.Measure.map (prefixProj α n) ρ

The prefix marginal of an exchangeable path law is invariant under permutations of the finite prefix, the special case of ExchangeableLaw.map_prefixProj_of_injective along the injective selection i ↦ (σ i).val.