Documentation

Exchangeability.ConditionallyIID

Conditionally i.i.d. Sequences and de Finetti's Theorem #

This file defines conditionally i.i.d. sequences and proves that they are exchangeable. This establishes one direction of de Finetti's representation theorem: conditionally i.i.d. ⇒ exchangeable.

Main definitions #

Main results #

The de Finetti-Ryll-Nardzewski theorem #

The complete equivalence for infinite sequences is: contractable ↔ exchangeable ↔ conditionally i.i.d.

This file proves: conditionally i.i.d. ⇒ exchangeable

The complete picture #

Mathematical intuition #

Conditionally i.i.d. means: "There exists a random probability measure ν, and given the value of ν, the sequence is i.i.d. with distribution ν."

Why this is exchangeable: If we permute the indices, we're still sampling i.i.d. from the same random distribution ν, so the joint distribution is unchanged.

Example: Pólya's urn - drawing balls with replacement where the replacement probability depends on the urn composition. Conditionally on the limiting proportion, the draws are i.i.d. Bernoulli.

Implementation notes #

This file uses the Giry monad structure (Measure.bind) to express conditioning. The key technical ingredient is showing that permuting coordinates of a product measure gives the same measure, which follows from measurePreserving_piCongrLeft.

References #

source
instance MeasureTheory.Measure.pi_isProbabilityMeasure {ι : Type u_3} [Fintype ι] {α : ι → Type u_4} [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), IsProbabilityMeasure (μ i)] [∀ (i : ι), SigmaFinite (μ i)] :
IsProbabilityMeasure (Measure.pi μ)

The product of probability measures is a probability measure.

This is a basic fact about product measures: if each marginal μ i has total mass 1, then the product measure ∏ᵢ μ i also has total mass 1.

Proof: The measure of the whole space ∏ᵢ αᵢ equals the product of the measures of the marginal spaces, which is ∏ᵢ 1 = 1.

source
theorem MeasureTheory.Measure.pi_comp_perm {ι : Type u_3} [Fintype ι] {α : Type u_4} [MeasurableSpace α] {ν : Measure α} [SigmaFinite ν] (σ : Equiv.Perm ι) :
map (fun (f : ι → α) => f ∘ ⇑σ) (Measure.pi fun (x : ι) => ν) = Measure.pi fun (x : ι) => ν

Product measures with identical marginals are invariant under permutations.

Statement: If we have a product measure where each coordinate is distributed as ν, and we permute the coordinates by σ, we get the same measure back.

Mathematical content: For i.i.d. sequences, permuting the indices doesn't change the distribution because all coordinates have the same marginal and are independent.

Proof: Uses mathlib's measurePreserving_piCongrLeft, which shows that the permutation map is measure-preserving for product measures.

This is the key technical lemma enabling exchangeable_of_conditionallyIID.

source
theorem MeasureTheory.Measure.bind_map_comm {Ω : Type u_3} {α : Type u_4} {β : Type u_5} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : Measure Ω} {κ : Ω → Measure α} (hκ : Measurable κ) {f : α → β} (hf : Measurable f) :
map f (μ.bind κ) = μ.bind fun (ω : Ω) => map f (κ ω)

Giry monad functoriality: mapping commutes with binding.

Statement: Mapping a function f after binding a kernel κ is the same as binding the kernel obtained by mapping f through κ.

Category theory: This expresses functoriality of the Giry monad: the map operation interacts properly with the monadic bind operation. In categorical terms: fmap f ∘ join = join ∘ fmap (fmap f).

Probabilistic interpretation: If we first sample ω ~ μ, then sample x ~ κ(ω), then apply f, this is the same as first sampling ω ~ μ, then sampling from the mapped kernel f₊κ(ω).

Application: This is used to show that conditioning preserves exchangeability - we can push permutations through the conditional distribution.

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

A sequence is conditionally i.i.d. if there exists a random probability measure making the coordinates independent.

Definition: X is conditionally i.i.d. if there exists a probability kernel ν : Ω → Measure α such that for every finite selection of distinct indices k : Fin m → ℕ (i.e., strictly monotone), the joint law of (X_{k(0)}, ..., X_{k(m-1)}) equals 𝔼[ν^m], where ν^m is the m-fold product of ν.

Intuition: There exists a random distribution ν, and conditionally on ν, the sequence is i.i.d. with marginal distribution ν. Different sample paths may have different ν values, but for each fixed ν, the coordinates are independent with that distribution.

Example: Pólya's urn - drawing colored balls with replacement where we add a ball of the drawn color each time. The limiting proportion of colors is random, and conditionally on this proportion, the draws are i.i.d. Bernoulli.

Mathematical formulation: For each finite selection of distinct indices, we have: P{(X_{k(0)}, ..., X_{k(m-1)}) ∈ ·} = ∫ ν(ω)^m μ(dω)

Implementation: Uses mathlib's Measure.bind (Giry monad) and Measure.pi (product measure) to express the mixture of i.i.d. distributions.

Note on repeated indices: This definition only requires the product formula for strictly monotone index functions (distinct coordinates). For non-strictly-monotone functions (e.g., k = (0,0,1)), the correct law involves a duplication map, which follows trivially from the distinct-indices case. This matches Kallenberg (2005), Theorem 1.1.

Reference: Kallenberg (2005), "Probabilistic Symmetries and Invariance Principles", Theorem 1.1 (page 27-28).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Exchangeability.pi_perm_comm {ι : Type u_3} [Fintype ι] {α : Type u_4} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite ν] (σ : Equiv.Perm ι) :
    (MeasureTheory.Measure.pi fun (x : ι) => ν) = MeasureTheory.Measure.map (fun (f : ι → α) => f ∘ ⇑(Equiv.symm σ)) (MeasureTheory.Measure.pi fun (x : ι) => ν)

    Helper lemma: Permuting coordinates after taking a product is the same as taking the product and then permuting.

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

    Main theorem: Conditionally i.i.d. sequences are exchangeable.

    Statement: If X is conditionally i.i.d., then it is exchangeable (invariant under finite permutations).

    Proof strategy:

    1. By ConditionallyIID, the law of (X_0, ..., X_{n-1}) is μ.bind(λω. ν(ω)^n) (using the identity function, which is strictly monotone)
    2. Show that permuting coordinates after sampling from this mixture gives the same measure
    3. Use pi_comp_perm to show that permuting a product measure ν^n gives ν^n back
    4. Use bind_map_comm to push the permutation through the bind operation
    5. Therefore the law of (X_{σ(0)}, ..., X_{σ(n-1)}) equals the law of (X_0, ..., X_{n-1})

    Intuition: Permuting the indices doesn't change the distribution because:

    • We're still integrating over the same random measure ν
    • For each fixed ν, permuting i.i.d. samples gives the same distribution (by pi_comp_perm)

    Mathematical significance: This proves one direction of de Finetti's theorem. The converse (exchangeable ⇒ conditionally i.i.d.) is the deep content of de Finetti's representation theorem and requires constructing the de Finetti measure from the tail σ-algebra.

    This is the "easy" direction because we're given the mixing measure ν explicitly.