Contractability and Exchangeability

This file establishes the relationship between exchangeability and contractability for infinite sequences of random variables, following Kallenberg's "Probabilistic Symmetries and Invariance Principles" (2005).

Main definitions

• Exchangeable μ X: The sequence X is exchangeable under measure μ if its finite-dimensional distributions are invariant under finite permutations.
• FullyExchangeable μ X: The sequence is fully exchangeable if invariant under all permutations of ℕ (not just finite ones).
• Contractable μ X: The sequence is contractable if all strictly increasing subsequences of equal length have the same distribution.

Main results

• FullyExchangeable.exchangeable: Full exchangeability implies (finite) exchangeability.
• contractable_of_exchangeable: Exchangeable ⇒ contractable (via permutation extension).
• exists_perm_extending_strictMono: Key combinatorial lemma showing that any strictly monotone function k : Fin m → ℕ can be extended to a permutation of Fin n.

The de Finetti-Ryll-Nardzewski equivalence

The full theorem establishes the equivalence for infinite sequences: contractable ↔ exchangeable ↔ conditionally i.i.d.

This file proves the implication exchangeable → contractable using a permutation extension argument.

The complete picture

• Exchangeable → contractable (this file): Any strictly increasing subsequence can be realized as the image of the first m coordinates under some permutation.
• Contractable → exchangeable (Exchangeability/DeFinetti/Theorem.lean): Uses ergodic theory and the martingale convergence approach.
• Exchangeable ↔ fully exchangeable (Exchangeability/Exchangeability.lean): Uses π-system uniqueness and finite approximation of infinite permutations.
• Conditionally i.i.d. → exchangeable (Exchangeability/ConditionallyIID.lean): Directly from the definition.

Implementation notes

The key technical challenge is constructing permutations that extend strictly monotone selections. Given k : Fin m → ℕ with k(0) < k(1) < ... < k(m-1), we construct a permutation σ : Perm (Fin n) such that σ(i) = k(i) for i < m. This uses Equiv.extendSubtype to extend a bijection between subtypes to a full permutation.

References

• Kallenberg, "Probabilistic Symmetries and Invariance Principles" (2005), Theorem 1.1
• Kallenberg, "Foundations of Modern Probability" (2002), Theorem 11.10

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

A sequence of random variables is exchangeable if permuting finitely many indices preserves the joint distribution.

Formally, for every n and every permutation σ of Fin n, the distribution of (X_{σ(0)}, ..., X_{σ(n-1)}) equals the distribution of (X_0, ..., X_{n-1}).

This is the central notion in de Finetti's theorem.

Equations

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

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

A sequence is fully exchangeable if permuting any indices preserves the distribution.

This is stronger than Exchangeable because it requires invariance under all permutations of ℕ, not just finite ones. However, Exchangeability.lean proves that these notions are equivalent for probability measures.

Formally, for every permutation π : Perm ℕ, the distribution of the reindexed sequence (X_{π(0)}, X_{π(1)}, ...) equals the distribution of (X_0, X_1, ...).

Equations

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

def Exchangeability.extendFinPerm {n : ℕ} (σ : Equiv.Perm (Fin n)) : Equiv.Perm ℕ

Extend a finite permutation to a permutation of ℕ by fixing points ≥ n.

Given a permutation σ of Fin n, this produces a permutation of ℕ that acts as σ on {0, ..., n-1} and fixes all i ≥ n.

This is used to connect full exchangeability with finite exchangeability.

Equations

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

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

Exchangeability at a specific dimension n.

Equations

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

theorem Exchangeability.exchangeable_iff_forall_exchangeableAt {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} : Exchangeable μ X ↔ ∀ (n : ℕ), ExchangeableAt μ X n

Exchangeability is equivalent to being exchangeable at every dimension.

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

Full exchangeability implies exchangeability.

If a sequence is invariant under all permutations of ℕ, it is certainly invariant under finite permutations. The proof uses extendFinPerm to view a finite permutation as an infinite one.

theorem Exchangeability.Exchangeable.comp {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {n : ℕ} (hX : Exchangeable μ X) (σ τ : Equiv.Perm (Fin n)) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => X (↑((Equiv.trans σ τ) i)) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => X (↑i) ω) μ

Exchangeability is preserved under composition of permutations.

theorem Exchangeability.Exchangeable.refl {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (n : ℕ) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => X (↑((Equiv.refl (Fin n)) i)) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => X (↑i) ω) μ

The identity permutation preserves the distribution (trivially).

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

A sequence is contractable if all strictly increasing subsequences of equal length have the same distribution.

Definition: For any m and any strictly increasing function k : Fin m → ℕ, the distribution of (X_{k(0)}, ..., X_{k(m-1)}) equals the distribution of (X_0, ..., X_{m-1}).

Intuition: Contractability is weaker than exchangeability. While exchangeability requires invariance under all permutations, contractability only requires invariance under "order-preserving selections" - we can choose any m indices as long as they are in increasing order.

Example: For i.i.d. sequences, any increasing subsequence has the same distribution as the initial segment, so contractability holds.

This is a key property in de Finetti's theorem, equivalent to both exchangeability and conditional independence.

Equations

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

theorem Exchangeability.contractable_same_range {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {m : ℕ} (k₁ k₂ : Fin m → ℕ) (h_range : ∀ (i : Fin m), k₁ i = k₂ i) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k₁ i) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k₂ i) ω) μ

Helper lemma: If two index sequences are pointwise equal, then the corresponding subsequences have the same distribution.

theorem Exchangeability.Contractable.prefix {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (n m : ℕ) (k : Fin m → Fin n) : StrictMono k → MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (↑(k i)) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (↑i) ω) μ

Contractability is preserved under prefix: if X is contractable, so is any finite prefix.

theorem Exchangeability.ExchangeableAt.apply {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {n : ℕ} (hX : ExchangeableAt μ X n) (σ : Equiv.Perm (Fin n)) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => X (↑(σ i)) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => X (↑i) ω) μ

Exchangeable at dimension n means permuting the first n indices preserves distribution.

theorem Exchangeability.Contractable.subsequence_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (m : ℕ) (k : Fin m → ℕ) (hk : StrictMono k) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k i) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (↑i) ω) μ

Contractability implies any strictly increasing subsequence matches the initial segment.

This is just a restatement of the definition for clarity.

theorem Exchangeability.Contractable.allStrictMono_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (m : ℕ) (k₁ k₂ : Fin m → ℕ) (hk₁ : StrictMono k₁) (hk₂ : StrictMono k₂) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k₁ i) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k₂ i) ω) μ

Any two strictly increasing subsequences of the same length have equal distributions.

For a contractable sequence, (X_{k₁(0)}, ..., X_{k₁(m-1)}) and (X_{k₂(0)}, ..., X_{k₂(m-1)}) have the same distribution whenever both k₁ and k₂ are strictly increasing, regardless of which specific indices are chosen.

This is the key property that makes contractability useful: the distribution depends only on the length of the subsequence, not on which increasing subsequence is selected.

theorem Exchangeability.Contractable.determined_by_increasing {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (m : ℕ) : ∃! ν : MeasureTheory.Measure (Fin m → α), ∀ (k : Fin m → ℕ), StrictMono k → MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k i) ω) μ = ν

Contractability implies that the distribution is determined by the marginal distributions of increasing selections.

theorem Exchangeability.Contractable.symm {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (m : ℕ) (k : Fin m → ℕ) (hk : StrictMono k) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (↑i) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k i) ω) μ

Contractability is symmetric: if (X_{k(0)}, ..., X_{k(m-1)}) has the same distribution as the initial segment, then the converse also holds.

theorem Exchangeability.iidProduct_exists {α : Type u_2} [MeasurableSpace α] {ν₀ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure ν₀] : ∃ (μ : MeasureTheory.Measure (ℕ → α)), MeasureTheory.IsProbabilityMeasure μ

The infinite i.i.d. product measure exists for any probability measure. Constructed via Ionescu-Tulcea in Exchangeability.Probability.InfiniteProduct.

theorem Exchangeability.iidProduct_perm_invariant {α : Type u_2} [MeasurableSpace α] {ν₀ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure ν₀] (σ : Equiv.Perm ℕ) : MeasureTheory.Measure.map (fun (f : ℕ → α) => f ∘ ⇑σ) (Probability.iidProduct ν₀) = Probability.iidProduct ν₀

The i.i.d. product of identical measures is permutation-invariant. This is a consequence of the construction via Ionescu-Tulcea.

theorem Exchangeability.exists_perm_extending_strictMono {m n : ℕ} (k : Fin m → ℕ) (hk_mono : StrictMono k) (hk_bound : ∀ (i : Fin m), k i < n) (hmn : m ≤ n) : ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin m), ↑(σ ⟨↑i, ⋯⟩) = k i

Any strictly increasing function can be extended to a permutation.

Statement: Given a strictly increasing k : Fin m → ℕ with all values < n and m ≤ n, there exists a permutation σ : Perm (Fin n) such that σ(i) = k(i) for all i < m.

Intuition: We want to build a permutation that "realizes" the selection k as the image of the first m positions. Since k is strictly increasing, it's injective, so its image has cardinality m. We can extend this to a full permutation by arbitrarily pairing up the remaining elements.

Construction outline:

1. Domain partition: {0,...,m-1} ∪ {m,...,n-1} = Fin n
2. Codomain partition: {k(0),...,k(m-1)} ∪ complement = Fin n
3. Map first m positions to k-values: σ(i) = k(i) for i < m
4. Extend arbitrarily to remaining positions using Equiv.extendSubtype

This is the key combinatorial lemma enabling contractable_of_exchangeable: any strictly increasing subsequence can be realized via a permutation.

theorem Exchangeability.measurable_perm_map {α : Type u_2} [MeasurableSpace α] {n : ℕ} (σ : Equiv.Perm (Fin n)) : Measurable fun (h : Fin n → α) (i : Fin n) => h (σ i)

theorem Exchangeability.measure_map_comp_perm {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {n : ℕ} (f g : Ω → Fin n → α) (σ : Equiv.Perm (Fin n)) (h : MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g μ) (hf : Measurable f) (hg : Measurable g) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => f ω (σ i)) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin n) => g ω (σ i)) μ

Helper lemma: Permuting the output coordinates doesn't change the measure. If f and g produce the same measure, then f ∘ σ and g ∘ σ produce the same measure.

theorem Exchangeability.Contractable.shift_segment_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (m k : ℕ) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k + ↑i) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (↑i) ω) μ

Contractability implies the first m variables have the same joint distribution regardless of which m consecutive variables we pick (starting from position k).

theorem Exchangeability.Contractable.shift_and_select {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (m : ℕ) (k : Fin m → ℕ) (offset : ℕ) (hk : StrictMono k) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (offset + k i) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (↑i) ω) μ

Contractable sequences are invariant under taking strictly increasing subsequences with offsets.

theorem Exchangeability.perm_range_eq {n : ℕ} (σ : Equiv.Perm (Fin n)) : Finset.image (fun (i : Fin n) => σ i) Finset.univ = Finset.univ

For a permutation σ on Fin n, the range {σ(0), ..., σ(n-1)} equals {0, ..., n-1}.

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

Main theorem: Every exchangeable sequence is contractable.

Statement: If X is exchangeable, then any strictly increasing subsequence has the same distribution as the initial segment.

Proof strategy:

1. Given a strictly increasing k : Fin m → ℕ, choose n large enough to contain all k(i) values.
2. Use exists_perm_extending_strictMono to construct a permutation σ : Perm (Fin n) such that σ(i) = k(i) for i < m.
3. Apply exchangeability: the distributions under σ and the identity are equal.
4. Project both sides to the first m coordinates to conclude that (X_{k(0)}, ..., X_{k(m-1)}) has the same distribution as (X_0, ..., X_{m-1}).

Mathematical significance: This shows that exchangeability (invariance under all finite permutations) implies contractability (invariance under increasing selections). The converse requires ergodic theory and is much deeper.

This is one direction of de Finetti's theorem.