de Finetti's Theorem via Contractability (Kallenberg's First Proof)

This file provides de Finetti's theorem using contractability directly, following Kallenberg's "first proof" which uses disjoint-block averaging rather than permutations.

Main results

• deFinetti_viaKoopman_path: de Finetti's theorem from contractability (path-space version). For a contractable sequence on a standard Borel space, there exists a kernel ν such that the coordinates are conditionally i.i.d. given ν.

Mathematical overview

The key insight of Kallenberg's first proof is that contractability (invariance under strictly monotone subsequences) directly implies conditional i.i.d., without going through exchangeability.

The proof proceeds as follows:

1. Block injection: For m blocks of size n, define strictly monotone maps ρⱼ : ℕ → ℕ that select one element from each block.

2. Contractability application: For each choice function j : Fin m → Fin n, the block injection ρⱼ is strictly monotone, so contractability gives: ∫ ∏ fᵢ(ωᵢ) dμ = ∫ ∏ fᵢ(ω(ρⱼ(i))) dμ

3. Averaging: Sum over all n^m choice functions to get: ∫ ∏ fᵢ(ωᵢ) dμ = ∫ ∏ blockAvg_i dμ

4. L¹ convergence: As n → ∞, block averages converge in L¹ to conditional expectations (using Cesàro convergence).

5. Factorization: Taking limits yields: CE[∏ fᵢ(ωᵢ) | mSI] = ∏ CE[fᵢ(ω₀) | mSI] a.e.

6. Kernel construction: The product factorization gives kernel independence, from which we construct the directing measure ν.

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1

Transfer to General Spaces

The path-space result conditionallyIID_of_contractable_path can be transferred to general random sequences X : ℕ → Ω → α via the pushforward measure.

Key insight: For X : ℕ → Ω → α, the pushforward measure μ.map (fun ω i => X i ω) on path space satisfies the contractability hypothesis if X is contractable.

theorem Exchangeability.DeFinetti.pathSpace_contractable_of_contractable {α : Type u_1} [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hContract : Contractable μ X) (m : ℕ) (k : Fin m → ℕ) : StrictMono k → MeasureTheory.Measure.map (fun (ω : ℕ → α) (i : Fin m) => ω (k i)) (MeasureTheory.Measure.map (fun (ω' : Ω) (i : ℕ) => X i ω') μ) = MeasureTheory.Measure.map (fun (ω : ℕ → α) (i : Fin m) => ω ↑i) (MeasureTheory.Measure.map (fun (ω' : Ω) (i : ℕ) => X i ω') μ)

Transfer path-space contractability to the pushforward of a general sequence.

Given X : ℕ → Ω → α that is contractable, the pushforward measure on Ω[α] = ℕ → α satisfies the path-space contractability hypothesis.

theorem Exchangeability.DeFinetti.measure_map_shift_eq_of_contractable {α : Type u_1} [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hContract : Contractable μ X) : MeasureTheory.Measure.map (fun (ω' : Ω) (i : ℕ) => X (i + 1) ω') μ = MeasureTheory.Measure.map (fun (ω' : Ω) (i : ℕ) => X i ω') μ

Shifting coordinates by +1 preserves the pushforward measure for contractable sequences.

This is the key measure-theoretic step for shift-preservation: if X is contractable, then μ.map(i ↦ X(i+1)) = μ.map(i ↦ X i).

Proof outline:

1. Contractability gives finite-dimensional marginal equality
2. For each n, the marginal on {0,...,n-1} of μ.map(i ↦ X(i+1)) equals the marginal of μ.map(i ↦ X i) (by contractability with k(i) = i+1)
3. Apply measure_eq_of_fin_marginals_eq_prob to conclude measure equality

theorem Exchangeability.DeFinetti.pathSpace_shift_preserving_of_contractable {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hContract : Contractable μ X) : MeasureTheory.MeasurePreserving PathSpace.shift (MeasureTheory.Measure.map (fun (ω' : Ω) (i : ℕ) => X i ω') μ) (MeasureTheory.Measure.map (fun (ω' : Ω) (i : ℕ) => X i ω') μ)

Shift-preservation transfers to the pushforward measure.

If X is contractable, the pushforward measure is shift-preserving.

theorem Exchangeability.DeFinetti.conditionallyIID_transfer {α : Type u_1} [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hCIID_path : ConditionallyIID (MeasureTheory.Measure.map (fun (ω' : Ω) (i : ℕ) => X i ω') μ) fun (i : ℕ) (ω : Ω[α]) => ω i) : ConditionallyIID μ X

ConditionallyIID transfers between path space and original space.

If μ_path = μ.map φ where φ ω = (fun i => X i ω), then ConditionallyIID μ_path id ↔ ConditionallyIID μ X where id on path space is fun i ω => ω i.

Bridge from Contractability to ConditionallyIID

The bridge from contractability to the bind-based Exchangeability.ConditionallyIID requires extending from StrictMono indices (which contractability gives) to arbitrary Injective indices (which CommonEnding.conditional_iid_from_directing_measure needs).

The key insight is that any injective function can be sorted to a StrictMono one, and products are commutative. So for injective k : Fin m → ℕ:

1. Sort k to get sorted : Fin m → ℕ which is StrictMono
2. k = sorted ∘ σ for some permutation σ of Fin m
3. Use contractability with sorted to reduce to consecutive indices
4. Use product commutativity to handle the σ reordering

theorem Exchangeability.DeFinetti.indicator_product_bridge_contractable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (hContract : ∀ (m : ℕ) (k : Fin m → ℕ), StrictMono k → MeasureTheory.Measure.map (fun (ω : Ω[α]) (i : Fin m) => ω (k i)) μ = MeasureTheory.Measure.map (fun (ω : Ω[α]) (i : Fin m) => ω ↑i) μ) (m : ℕ) (k : Fin m → ℕ) (hk : Function.Injective k) (B : Fin m → Set α) (hB_meas : ∀ (i : Fin m), MeasurableSet (B i)) : ∫⁻ (ω : Ω[α]), ∏ i : Fin m, ENNReal.ofReal ((B i).indicator (fun (x : α) => 1) (ω (k i))) ∂μ = ∫⁻ (ω : Ω[α]), ∏ i : Fin m, (ViaKoopman.ν ω) (B i) ∂μ

Bridge condition for contractable measures: extends from StrictMono to Injective.

This is the key technical step connecting contractability to conditional_iid_from_directing_measure. The proof uses that any injective function on Fin m can be sorted to a StrictMono one. Then contractability reduces to consecutive indices, and product commutativity handles reordering.

Proof sketch:

1. Sort k to get ρ : Fin m → ℕ (StrictMono) and σ : Fin m ≃ Fin m with k = ρ ∘ σ
2. ∏ i, indicator(B i)(ω(k i)) = ∏ j, indicator(B(σ⁻¹ j))(ω(ρ j)) (reorder)
3. By contractability: ∫ ... dμ at ρ-indices = ∫ ... dμ at consecutive indices
4. By condexp_product_factorization_contractable: = ∫ ∏ j, (∫ indicator(B(σ⁻¹ j)) dν) dμ
5. = ∫ ∏ i, ν(B i) dμ (by product commutativity)

theorem Exchangeability.DeFinetti.conditionallyIID_bind_of_contractable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (hContract : ∀ (m : ℕ) (k : Fin m → ℕ), StrictMono k → MeasureTheory.Measure.map (fun (ω : Ω[α]) (i : Fin m) => ω (k i)) μ = MeasureTheory.Measure.map (fun (ω : Ω[α]) (i : Fin m) => ω ↑i) μ) : ConditionallyIID μ fun (i : ℕ) (ω : Ω[α]) => ω i

Bridge from contractable to bind-based ConditionallyIID on path space.

This is the key lemma connecting contractability to Exchangeability.ConditionallyIID. It uses CommonEnding.conditional_iid_from_directing_measure with the bridge condition proved by indicator_product_bridge_contractable.