Exchangeability and Full Exchangeability

This file proves that exchangeability (invariance under finite permutations) and full exchangeability (invariance under all permutations of ℕ) are equivalent for probability measures on sequence spaces.

Main results

• exchangeable_iff_fullyExchangeable: For a probability measure and a measurable stochastic process, exchangeability is equivalent to full exchangeability.
• measure_eq_of_fin_marginals_eq: Two finite measures on ℕ → α that agree on all finite-dimensional marginals are equal.

Technical approach

The proof uses the π-system uniqueness theorem for finite measures rather than directly invoking Kolmogorov extension or Ionescu-Tulcea. While mathlib provides these powerful tools (Measure.infinitePi for Kolmogorov extension and ProbabilityTheory.Kernel.traj for Ionescu-Tulcea), applying them here would require first constructing the measure from exchangeability data, which is circular when proving that finite exchangeability implies full exchangeability.

Instead, we use a uniqueness-based approach:

1. Cylinder sets determined by initial segments form a π-system that generates the product σ-algebra on ℕ → α.
2. Two measures with matching finite marginals must be equal (by π-system uniqueness, Measure.ext_of_generate_finite).
3. Any infinite permutation can be approximated by a finite permutation on a sufficiently large initial segment, allowing us to transfer exchangeability to full exchangeability via the uniqueness result.

This approach directly proves the equivalence without requiring measure construction machinery.

π-system of prefix cylinders

A prefix cylinder is a measurable subset of ℕ → α determined by the first n coordinates. Formally, it is the preimage of a measurable set under the projection to Fin n → α.

Key properties:

• Prefix cylinders form a π-system (closed under finite intersections).
• They generate the product σ-algebra on ℕ → α.
• This allows us to apply the π-system uniqueness theorem: two finite measures that agree on all prefix cylinders must be equal.

def Exchangeability.prefixProj (α : Type u_3) (n : ℕ) (x : ℕ → α) : Fin n → α

Projection to the first n coordinates.

Equations

• Exchangeability.prefixProj α n x i = x ↑i

@[simp]

theorem Exchangeability.prefixProj_apply {α : Type u_2} {n : ℕ} (x : ℕ → α) (i : Fin n) : prefixProj α n x i = x ↑i

theorem Exchangeability.measurable_prefixProj {α : Type u_2} [MeasurableSpace α] {n : ℕ} : Measurable (prefixProj α n)

theorem Exchangeability.measure_eq_of_fin_marginals_eq {α : Type u_2} [MeasurableSpace α] {μ ν : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (n : ℕ) (S : Set (Fin n → α)), MeasurableSet S → (MeasureTheory.Measure.map (prefixProj α n) μ) S = (MeasureTheory.Measure.map (prefixProj α n) ν) S) : μ = ν

Finite measures with matching finite-dimensional marginals are equal.

If two finite measures on ℕ → α induce the same distribution on each finite-dimensional projection Fin n → α, then they are equal. This is a consequence of the π-system uniqueness theorem applied to prefix cylinders.

Mathematical content: This is a Kolmogorov extension-type result showing that infinite-dimensional measures are determined by their finite marginals.

Proof structure: The proof decomposes into three steps:

1. Measures agree on total mass (via 1-dimensional marginal)
2. Measures agree on all prefix cylinders (direct from marginals)
3. Apply π-system uniqueness to extend agreement to all measurable sets

theorem Exchangeability.measure_eq_of_fin_marginals_eq_prob {α : Type u_2} [MeasurableSpace α] {μ ν : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (h : ∀ (n : ℕ) (S : Set (Fin n → α)), MeasurableSet S → (MeasureTheory.Measure.map (prefixProj α n) μ) S = (MeasureTheory.Measure.map (prefixProj α n) ν) S) : μ = ν

Convenience wrapper of measure_eq_of_fin_marginals_eq for probability measures.

Exchangeability versus full exchangeability

This section proves that exchangeability (invariance under finite permutations) implies full exchangeability (invariance under all permutations of ℕ) for probability measures.

Strategy: Given an arbitrary permutation π of ℕ and a finite index n, we construct a finite permutation that agrees with π on the first n coordinates. Exchangeability ensures the finite marginals match, and by the previous uniqueness result, the full measures are equal.

def Exchangeability.reindex {α : Type u_2} (π : Equiv.Perm ℕ) (x : ℕ → α) : ℕ → α

Reindex a sequence by applying a permutation to the indices.

Given a permutation π of ℕ and a sequence x : ℕ → α, returns the sequence i ↦ x (π i).

Equations

• Exchangeability.reindex π x i = x (π i)

@[simp]

theorem Exchangeability.reindex_apply {α : Type u_2} {π : Equiv.Perm ℕ} (x : ℕ → α) (i : ℕ) : reindex π x i = x (π i)

theorem Exchangeability.measurable_reindex {α : Type u_2} [MeasurableSpace α] {π : Equiv.Perm ℕ} : Measurable (reindex π)

noncomputable def Exchangeability.pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) : MeasureTheory.Measure (ℕ → α)

The path law (or joint distribution) of a stochastic process.

Given a measure μ on Ω and a process X : ℕ → Ω → α, the path law is the pushforward measure on ℕ → α obtained by mapping each ω to its sample path i ↦ X i ω.

Equations

• Exchangeability.pathLaw μ X = MeasureTheory.Measure.map (fun (ω : Ω) (i : ℕ) => X i ω) μ

theorem Exchangeability.fullyExchangeable_iff_pathLaw_invariant {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), Measurable (X i)) : FullyExchangeable μ X ↔ ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (reindex π) (pathLaw μ X) = pathLaw μ X

Full exchangeability is equivalent to invariance of the path law.

A process is fully exchangeable if and only if its path law is invariant under all permutations of the index set ℕ. This provides a measure-theoretic characterization of full exchangeability.

Auxiliary combinatorics: approximating infinite permutations

To prove that exchangeability implies full exchangeability, we need to show that any infinite permutation π of ℕ can be approximated by a finite permutation on a sufficiently large initial segment.

The key construction: given π and n, we find a bound m = permBound π n such that both {0,...,n-1} and {π(0),...,π(n-1)} lie in {0,...,m-1}. Then we extend π to a permutation of Fin m by choosing an arbitrary permutation on the remaining indices.

theorem Exchangeability.exchangeable_iff_fullyExchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), Measurable (X i)) : Exchangeable μ X ↔ FullyExchangeable μ X