Infinite Products of Identically Distributed Measures

This file constructs the infinite i.i.d. product measure ν^ℕ on the space ℕ → α for a given probability measure ν : Measure α. This is the fundamental measure-theoretic construction underlying i.i.d. sequences.

Main definitions

• iidProjectiveFamily ν: The projective family of finite product measures indexed by Finset ℕ. For each finite subset I, gives the product measure ν^I on ∀ i : I, α.
• iidProduct ν: The probability measure on ℕ → α representing an i.i.d. sequence with marginal distribution ν. Defined as Measure.infinitePi (fun _ : ℕ => ν).

Main results

• iidProjectiveFamily_projective: The finite products form a projective family (projections preserve the measure).
• iidProduct_isProjectiveLimit: iidProduct ν is the projective limit of the finite products, making it unique with this property.
• cylinder_finset: For any finite subset I, the marginal distribution on I equals the finite product ν^I.
• cylinder_fintype: The distribution on the first n coordinates equals ν^n.
• perm_eq: The measure is invariant under all permutations of ℕ, proving that i.i.d. sequences are fully exchangeable.

Mathematical background

Kolmogorov extension theorem: Given a consistent family of finite-dimensional distributions (a projective family), there exists a unique probability measure on the infinite product space with these marginals.

For the i.i.d. case, consistency is automatic: if we want each coordinate to be distributed as ν independently, then for any finite subset I, the joint distribution is just ν^I. Mathlib's Measure.infinitePi implements this construction via Carathéodory's extension theorem.

Implementation approach

We use mathlib's Kolmogorov extension machinery rather than implementing it from scratch:

1. Finite products (Measure.pi): For finite index sets (requires Fintype)
2. Projectivity (isProjectiveMeasureFamily_pi): Finite products are consistent
3. Infinite extension (Measure.infinitePi): Extends to infinite product via Carathéodory's theorem
4. Marginal characterization (infinitePi_map_restrict): The extended measure has the correct finite-dimensional marginals

This construction uses mathlib's standard measure theory infrastructure.

Relation to other files

This construction is used in Contractability.lean and ConditionallyIID.lean to build exchangeable sequences. The permutation invariance (perm_eq) shows that i.i.d. sequences are the canonical example of exchangeable sequences.

References

• Kallenberg, "Foundations of Modern Probability" (2002), Theorem 6.10 (Kolmogorov extension)
• Billingsley, "Probability and Measure" (1995), Section 36 (Product measures)

def Exchangeability.Probability.iidProjectiveFamily {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure ν] (I : Finset ℕ) : MeasureTheory.Measure (↥I → α)

The projective family of finite product measures for the i.i.d. construction.

Definition: For each finite subset I : Finset ℕ, this returns the product measure ν^I on ∀ i : I, α, where each coordinate is independently distributed according to ν.

Purpose: This family of finite-dimensional distributions serves as the input to Kolmogorov's extension theorem. We will show that this family is projective (consistent under marginalization) and then extend it to an infinite product.

Equations

• Exchangeability.Probability.iidProjectiveFamily I = MeasureTheory.Measure.pi fun (x : ↥I) => ν

theorem Exchangeability.Probability.iidProjectiveFamily_projective {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsProjectiveMeasureFamily iidProjectiveFamily

The finite product measures form a projective family (consistency condition).

Statement: The family iidProjectiveFamily ν satisfies the projectivity condition: if J ⊆ I, then marginalizing ν^I onto coordinates in J gives ν^J.

Mathematical content: This is the consistency requirement for Kolmogorov's extension theorem. For i.i.d. sequences, consistency is automatic because each coordinate is independently distributed.

Proof: This is a special case of mathlib's isProjectiveMeasureFamily_pi, which proves projectivity for any family of probability measures. For constant families (same measure on each coordinate), the result is immediate.

def Exchangeability.Probability.iidProduct {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.Measure (ℕ → α)

The infinite i.i.d. product measure ν^ℕ on ℕ → α.

Definition: This is the unique probability measure on ℕ → α such that:

• Each coordinate X_i is distributed according to ν
• The coordinates are mutually independent

Construction: Uses mathlib's Measure.infinitePi, which implements Kolmogorov's extension theorem:

1. Start with finite product measures ν^I for each finite I ⊆ ℕ
2. Verify they form a projective family (consistency under marginalization)
3. Apply Carathéodory's extension theorem to extend to the infinite product σ-algebra
4. The result is the unique probability measure with the specified finite marginals

Uniqueness: This measure is uniquely determined by the requirement that finite- dimensional marginals are i.i.d. products. This follows from the π-system uniqueness theorem (used in Exchangeability.lean).

Mathematical significance: This is the fundamental construction underlying the theory of i.i.d. sequences, forming the basis for the law of large numbers, central limit theorem, and de Finetti's theorem.

Equations

• Exchangeability.Probability.iidProduct ν = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ν

theorem Exchangeability.Probability.iidProduct_isProjectiveLimit {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsProjectiveLimit (iidProduct ν) iidProjectiveFamily

The infinite product is the projective limit of the finite products.

Statement: iidProduct ν is the unique measure whose marginals on all finite subsets I match the finite products ν^I.

Mathematical content: This characterizes iidProduct ν as a projective limit, meaning that for every finite I ⊆ ℕ, if we marginalize the infinite product onto coordinates in I, we recover the finite product measure ν^I.

This is the defining property from Kolmogorov's extension theorem.

instance Exchangeability.Probability.iidProduct.instIsProbabilityMeasureForallNat {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsProbabilityMeasure (iidProduct ν)

The measure iidProduct ν is a probability measure.

This follows from the projective limit characterization: each finite product is a probability measure, so the projective limit is too.

theorem Exchangeability.Probability.iidProduct.cylinder_finset {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure ν] {I : Finset ℕ} : MeasureTheory.Measure.map I.restrict (iidProduct ν) = MeasureTheory.Measure.pi fun (x : ↥I) => ν

Marginal distributions on arbitrary finite subsets match the finite products.

Statement: For any finite subset I ⊆ ℕ, the marginal distribution of iidProduct ν on the coordinates indexed by I equals the product measure ν^I.

Intuition: If we project an i.i.d. sequence onto a finite set of coordinates, we get a finite i.i.d. sample with the same marginal distribution.

This is a direct consequence of the projective limit characterization.

theorem Exchangeability.Probability.iidProduct.cylinder_fintype {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure ν] {n : ℕ} : MeasureTheory.Measure.map (fun (f : ℕ → α) (i : Fin n) => f ↑i) (iidProduct ν) = MeasureTheory.Measure.pi fun (x : Fin n) => ν

The distribution on the first n coordinates is the n-fold product ν^n.

Statement: The marginal distribution of iidProduct ν on {0, 1, ..., n-1} equals the n-fold product measure on Fin n → α.

Intuition: The first n coordinates of an i.i.d. sequence form a finite i.i.d. sample of size n.

Proof strategy: Show that both measures agree on all measurable rectangles (sets of the form ∏ᵢ Sᵢ). This uses Measure.pi_eq and the characterization of iidProduct via infinitePi_pi.

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

Key result: i.i.d. sequences are invariant under all permutations of the indices.

Statement: For any permutation σ : Perm ℕ, reindexing an i.i.d. sequence by σ gives the same distribution. Formally, the pushforward of iidProduct ν under the map f ↦ f ∘ σ equals iidProduct ν.

Mathematical significance: This proves that i.i.d. sequences are fully exchangeable. In fact, i.i.d. is the canonical example of exchangeability, and de Finetti's theorem shows that all exchangeable sequences are conditionally i.i.d.

Intuition: If we randomly permute the indices of an i.i.d. sequence, we still get an i.i.d. sequence with the same distribution, because:

1. Each coordinate is still distributed as ν (permuting doesn't change marginals)
2. Independence is preserved (permuting independent coordinates gives independent coordinates)

Proof strategy: Use Measure.eq_infinitePi to show both measures agree on all measurable rectangles. For a rectangle indexed by finite set s, the preimage under f ↦ f ∘ σ is a rectangle indexed by σ(s), and the product over σ(s) equals the product over s by permutation of the product.

Connection to other results: Combined with Exchangeability.lean, this shows that i.i.d. ⇒ fully exchangeable ⇒ exchangeable, completing one direction of de Finetti's equivalence.