Basic exchangeability definitions

This file defines the symmetry notions of a process X : ℕ → Ω → α in terms of its finite-dimensional and path laws (blockLaw, prefixLaw, pathLaw, from TauCeti.Probability.Process.PathLaw.Basic):

• ExchangeableAt μ X n — the law of the first n coordinates is invariant under every permutation of Fin n;
• Exchangeable μ X — finite exchangeability at every length;
• FullyExchangeable μ X — the path law is invariant under every permutation of ℕ;
• Contractable μ X — finite-dimensional laws are invariant under strictly increasing finite subsequences (spreadability).

The definitions are intentionally hypothesis-light; measurability hypotheses enter only in lemmas that compose Measure.maps. They are adapted from the cameronfreer/exchangeability sources pinned at e0532e59ceff23edab44dda9ab0655debbc9cc22, with Tau Ceti API names and hypotheses.

def TauCeti.Probability.ExchangeableAt {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) (n : ℕ) : Prop

Finite exchangeability at n: the first n coordinates have permutation-invariant law.

Equations

• TauCeti.Probability.ExchangeableAt μ X n = ∀ (σ : Equiv.Perm (Fin n)), (TauCeti.Probability.blockLaw μ X fun (i : Fin n) => ↑(σ i)) = TauCeti.Probability.prefixLaw μ X n

def TauCeti.Probability.Exchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) : Prop

Finite exchangeability at every length.

Equations

• TauCeti.Probability.Exchangeable μ X = ∀ (n : ℕ), TauCeti.Probability.ExchangeableAt μ X n

def TauCeti.Probability.FullyExchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) : Prop

Full exchangeability: the path law is invariant under every permutation of ℕ.

Equations

• TauCeti.Probability.FullyExchangeable μ X = ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (fun (ω : Ω) (i : ℕ) => X (π i) ω) μ = TauCeti.Probability.pathLaw μ X

def TauCeti.Probability.Contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) : Prop

Contractability, or spreadability: finite-dimensional laws are invariant under strictly increasing finite subsequences.

Equations

• TauCeti.Probability.Contractable μ X = ∀ (m : ℕ) (k : Fin m → ℕ), StrictMono k → TauCeti.Probability.blockLaw μ X k = TauCeti.Probability.prefixLaw μ X m

theorem TauCeti.Probability.Exchangeable.exchangeableAt {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Exchangeable μ X) (n : ℕ) : ExchangeableAt μ X n

theorem TauCeti.Probability.ExchangeableAt.permute {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {n : ℕ} (h : ExchangeableAt μ X n) (σ : Equiv.Perm (Fin n)) : (blockLaw μ X fun (i : Fin n) => ↑(σ i)) = prefixLaw μ X n

theorem TauCeti.Probability.ExchangeableAt.prefixLaw_singleton_comp {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {n : ℕ} (h : ExchangeableAt μ X n) (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) (w : Fin n → α) (σ : Equiv.Perm (Fin n)) : (prefixLaw μ X n) {w ∘ ⇑σ} = (prefixLaw μ X n) {w}

Under finite exchangeability at n, rearranging a path leaves its probability unchanged.

theorem TauCeti.Probability.FullyExchangeable.permute {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : FullyExchangeable μ X) (π : Equiv.Perm ℕ) : MeasureTheory.Measure.map (fun (ω : Ω) (i : ℕ) => X (π i) ω) μ = pathLaw μ X