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)

def Exchangeability.prefixCylinder {α : Type u_2} {n : ℕ} (S : Set (Fin n → α)) : Set (ℕ → α)

Cylinder set determined by the first n coordinates.

Given a set S ⊆ Fin n → α, the prefix cylinder prefixCylinder n S is the set of all sequences x : ℕ → α whose first n coordinates lie in S.

Equations

• Exchangeability.prefixCylinder S = Exchangeability.prefixProj α n ⁻¹' S

@[simp]

theorem Exchangeability.mem_prefixCylinder {α : Type u_2} {n : ℕ} {S : Set (Fin n → α)} {x : ℕ → α} : x ∈ prefixCylinder S ↔ prefixProj α n x ∈ S

@[simp]

theorem Exchangeability.prefixCylinder_univ {α : Type u_2} {n : ℕ} : prefixCylinder Set.univ = Set.univ

@[simp]

theorem Exchangeability.prefixCylinder_empty {α : Type u_2} {n : ℕ} : prefixCylinder ∅ = ∅

def Exchangeability.prefixCylinders {α : Type u_2} [MeasurableSpace α] : Set (Set (ℕ → α))

The collection of all prefix cylinders.

A set A ⊆ ℕ → α belongs to prefixCylinders if it is the preimage of some measurable set S ⊆ Fin n → α under projection to the first n coordinates, for some n.

Key property: This forms a π-system that generates the product σ-algebra.

Equations

• Exchangeability.prefixCylinders = {A : Set (ℕ → α) | ∃ (n : ℕ) (S : Set (Fin n → α)), MeasurableSet S ∧ A = Exchangeability.prefixCylinder S}

theorem Exchangeability.prefixCylinder_mem_prefixCylinders {α : Type u_2} [MeasurableSpace α] {n : ℕ} {S : Set (Fin n → α)} (hS : MeasurableSet S) : prefixCylinder S ∈ prefixCylinders

theorem Exchangeability.measurable_of_mem_prefixCylinders {α : Type u_2} [MeasurableSpace α] {A : Set (ℕ → α)} (hA : A ∈ prefixCylinders) : MeasurableSet A

def Exchangeability.takePrefix {α : Type u_2} {m n : ℕ} (hmn : m ≤ n) (x : Fin n → α) : Fin m → α

Restrict a finite tuple to its first m coordinates.

Given a function x : Fin n → α and a proof that m ≤ n, returns the restriction to Fin m → α.

Equations

• Exchangeability.takePrefix hmn x i = x (Fin.castLE hmn i)

@[simp]

theorem Exchangeability.takePrefix_apply {α : Type u_2} {m n : ℕ} {hmn : m ≤ n} (x : Fin n → α) (i : Fin m) : takePrefix hmn x i = x (Fin.castLE hmn i)

@[simp]

theorem Exchangeability.takePrefix_prefixProj {α : Type u_2} {m n : ℕ} {hmn : m ≤ n} (x : ℕ → α) : takePrefix hmn (prefixProj α n x) = prefixProj α m x

@[simp]

theorem Exchangeability.castLE_coe_nat {m n : ℕ} {hmn : m ≤ n} (i : Fin m) : ↑(Fin.castLE hmn i) = ↑i

def Exchangeability.extendSet {α : Type u_2} {m n : ℕ} (hmn : m ≤ n) (S : Set (Fin m → α)) : Set (Fin n → α)

Extend a set from Fin m → α to Fin n → α by ignoring extra coordinates.

Given a set S ⊆ Fin m → α and m ≤ n, the extended set consists of all x : Fin n → α whose first m coordinates lie in S.

Equations

• Exchangeability.extendSet hmn S = {x : Fin n → α | Exchangeability.takePrefix hmn x ∈ S}

theorem Exchangeability.prefixCylinder_inter {α : Type u_2} {m n : ℕ} {S : Set (Fin m → α)} {T : Set (Fin n → α)} : prefixCylinder S ∩ prefixCylinder T = prefixCylinder (extendSet ⋯ S ∩ extendSet ⋯ T)

theorem Exchangeability.takePrefix_measurable {α : Type u_2} [MeasurableSpace α] [MeasurableSpace α] {m n : ℕ} (hmn : m ≤ n) : Measurable (takePrefix hmn)

theorem Exchangeability.extendSet_measurable {α : Type u_2} [MeasurableSpace α] [MeasurableSpace α] {m n : ℕ} {S : Set (Fin m → α)} {hmn : m ≤ n} (hS : MeasurableSet S) : MeasurableSet (extendSet hmn S)

theorem Exchangeability.isPiSystem_prefixCylinders {α : Type u_2} [MeasurableSpace α] [MeasurableSpace α] : IsPiSystem prefixCylinders

The prefix cylinders form a π-system.

A π-system is a collection of sets closed under finite intersections. This property is crucial for applying the uniqueness theorem for finite measures.

theorem Exchangeability.cylinder_subset_prefixCylinders {α : Type u_2} [MeasurableSpace α] [MeasurableSpace α] {s : Finset ℕ} {S : Set (↥s → α)} (hS : MeasurableSet S) : MeasureTheory.cylinder s S ∈ prefixCylinders

Helper: any cylinder determined by a finite set of coordinates belongs to the σ-algebra generated by prefix cylinders.

theorem Exchangeability.generateFrom_prefixCylinders {α : Type u_2} [MeasurableSpace α] [MeasurableSpace α] : MeasurableSpace.generateFrom prefixCylinders = inferInstance

The σ-algebra generated by prefix cylinders is the product σ-algebra.

This shows that prefix cylinders generate the full product σ-algebra on ℕ → α, which means any measurable set can be approximated by prefix cylinders.

theorem Exchangeability.measure_eq_of_fin_marginals_eq {α : Type u_2} [MeasurableSpace α] [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 α] [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} [MeasurableSpace α] [MeasurableSpace α] {π : Equiv.Perm ℕ} (x : ℕ → α) (i : ℕ) : reindex π x i = x (π i)

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

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.pathLaw_map_prefix {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) (hX : ∀ (i : ℕ), Measurable (X i)) (n : ℕ) : MeasureTheory.Measure.map (prefixProj α n) (pathLaw μ X) = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => X (↑i) ω) μ

theorem Exchangeability.pathLaw_map_prefix_perm {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) (hX : ∀ (i : ℕ), Measurable (X i)) (π : Equiv.Perm ℕ) (n : ℕ) : MeasureTheory.Measure.map (prefixProj α n) (MeasureTheory.Measure.map (reindex π) (pathLaw μ X)) = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => X (π ↑i) ω) μ

theorem Exchangeability.fullyExchangeable_iff_pathLaw_invariant {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [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.

def Exchangeability.permBound (π : Equiv.Perm ℕ) (n : ℕ) : ℕ

A finite bound containing both {0,...,n-1} and {π(0),...,π(n-1)}.

This is the maximum of n and the supremum of π(i) + 1 for i < n.

Equations

• Exchangeability.permBound π n = max n ((Finset.range n).sup fun (i : ℕ) => π i + 1)

theorem Exchangeability.le_permBound (π : Equiv.Perm ℕ) (n : ℕ) : n ≤ permBound π n

theorem Exchangeability.lt_permBound_of_lt (π : Equiv.Perm ℕ) (n : ℕ) {i : ℕ} (hi : i < n) : π i < permBound π n

theorem Exchangeability.lt_permBound_fin (π : Equiv.Perm ℕ) (n : ℕ) {i : Fin n} : π ↑i < permBound π n

def Exchangeability.approxEquiv (π : Equiv.Perm ℕ) (n : ℕ) : { x : Fin (permBound π n) // ↑x < n } ≃ { x : Fin (permBound π n) // ∃ (j : Fin n), ↑x = π ↑j }

Equivalence between indices below n and indices in the image of a permutation. Used in the proof of exchangeability via permutation extension.

Equations

• One or more equations did not get rendered due to their size.

def Exchangeability.approxPerm (π : Equiv.Perm ℕ) (n : ℕ) : Equiv.Perm (Fin (permBound π n))

A finite permutation of Fin (permBound π n) that agrees with π on {0,...,n-1}.

This extends the restriction of π to an equivalence on the finite type Fin (permBound π n) by choosing an arbitrary permutation on the indices outside the range of π restricted to {0,...,n-1}.

Equations

• Exchangeability.approxPerm π n = (Exchangeability.approxEquiv π n).extendSubtype

theorem Exchangeability.approxPerm_apply_cast (π : Equiv.Perm ℕ) (n : ℕ) {i : Fin n} : (approxPerm π n) (Fin.castLE ⋯ i) = ⟨π ↑i, ⋯⟩

@[simp]

theorem Exchangeability.approxPerm_apply_cast_coe (π : Equiv.Perm ℕ) (n : ℕ) {i : Fin n} : ↑((approxPerm π n) (Fin.castLE ⋯ i)) = π ↑i

theorem Exchangeability.marginals_perm_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} (X : ℕ → Ω → α) (hX : ∀ (i : ℕ), Measurable (X i)) (hμ : Exchangeable μ X) (π : Equiv.Perm ℕ) (n : ℕ) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => X (π ↑i) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => X (↑i) ω) μ

Exchangeability implies invariance of all finite marginals under arbitrary permutations.

If a process X is exchangeable (invariant under finite permutations), then each finite marginal is invariant under any permutation of ℕ, not just finite ones. This is the key step in proving exchangeability implies full exchangeability.

Proof idea: Given an arbitrary permutation π and dimension n, construct a finite permutation that agrees with π on the first n coordinates using approxPerm. Exchangeability ensures this finite permutation preserves the n-dimensional marginal, hence so does π.

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