Common Ending for de Finetti Proofs

This file contains the common final step shared by Kallenberg's First and Second proofs of de Finetti's theorem. Both proofs construct a directing measure ν and then use the same argument to establish the conditional i.i.d. property.

The common structure

Given:

• A contractable/exchangeable sequence ξ
• A directing measure ν (constructed differently in each proof)
• The property that E[f(ξ_i) | ℱ] = ν^f for bounded measurable f

Show:

• ξ is conditionally i.i.d. given the tail σ-algebra

Integration with Mathlib

This file uses several key mathlib components:

• Measure.pi: Finite product measures from Mathlib.MeasureTheory.Constructions.Pi
• Kernel: Probability kernels from Mathlib.Probability.Kernel.Basic
• MeasureSpace.induction_on_inter: π-λ theorem from Mathlib.MeasureTheory.PiSystem
• Ergodic, MeasurePreserving: From Mathlib.Dynamics.Ergodic.Ergodic
• condExp: Conditional expectation from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

See also Exchangeability.ConditionallyIID for the definition of conditionally i.i.d. sequences using mathlib's measure theory infrastructure.

References

• Kallenberg (2005), page 26-27: "The proof can now be completed as before"
• Kallenberg (2005), Chapter 10: Stationary Processes and Ergodic Theory (FMP 10.2-10.4)

Tail σ-algebras and Invariant σ-fields

For an exchangeable or contractable sequence X : ℕ → Ω → α, the tail σ-algebra consists of events that depend only on the "tail" of the sequence, i.e., events invariant under modifications of finitely many coordinates.

Following Kallenberg (FMP 10.2-10.4):

• A set I is invariant under a transformation T if T⁻¹I = I
• A set I is almost invariant if μ(I Δ T⁻¹I) = 0
• The collection of invariant sets forms the invariant σ-field ℐ
• The collection of almost invariant sets forms the almost invariant σ-field ℐ'
• Key result (FMP 10.4): ℐ' = ℐ^μ (the μ-completion of ℐ)

For exchangeable sequences:

• The shift operator T: (ℕ → α) → (ℕ → α) by (Tξ)(n) = ξ(n+1) is the natural transformation
• The tail σ-algebra is related to the shift-invariant σ-field
• A function f is tail-measurable iff it's measurable w.r.t. the tail σ-algebra
• FMP 10.3: f is invariant/almost invariant iff f is ℐ-measurable/ℐ^μ-measurable

The directing measure ν constructed in de Finetti proofs is tail-measurable (almost invariant). This is essential for showing that ν defines a proper conditional kernel.

Note: Formalizing tail σ-algebra equality with shift-invariant σ-field is future work.

theorem Exchangeability.DeFinetti.CommonEnding.fidi_eq_avg_product {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (ν : Ω → MeasureTheory.Measure α) (hν_prob : ∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)) (_hν_meas : ∀ (s : Set α), MeasurableSet s → Measurable fun (ω : Ω) => (ν ω) s) (m : ℕ) (k : Fin m → ℕ) (B : Fin m → Set α) (hB : ∀ (i : Fin m), MeasurableSet (B i)) (h_bridge : ∫⁻ (ω : Ω), ∏ i : Fin m, ENNReal.ofReal ((B i).indicator (fun (x : α) => 1) (X (k i) ω)) ∂μ = ∫⁻ (ω : Ω), ∏ i : Fin m, (ν ω) (B i) ∂μ) : μ {ω : Ω | ∀ (i : Fin m), X (k i) ω ∈ B i} = ∫⁻ (ω : Ω), (MeasureTheory.Measure.pi fun (x : Fin m) => ν ω) {x : Fin m → α | ∀ (i : Fin m), x i ∈ B i} ∂μ

theorem Exchangeability.DeFinetti.CommonEnding.bind_pi_apply {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (ν : Ω → MeasureTheory.Measure α) (hν_prob : ∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)) (hν_meas : ∀ (s : Set α), MeasurableSet s → Measurable fun (ω : Ω) => (ν ω) s) (m : ℕ) (B : Set (Fin m → α)) (hB : MeasurableSet B) : (μ.bind fun (ω : Ω) => MeasureTheory.Measure.pi fun (x : Fin m) => ν ω) B = ∫⁻ (ω : Ω), (MeasureTheory.Measure.pi fun (x : Fin m) => ν ω) B ∂μ

The bind of a probability measure with the product measure kernel equals the integral of the product measure. This is the other side of the ConditionallyIID equation.

Note: We use lintegral (∫⁻) for measure-valued integrals since measures are ENNReal-valued.

This is a direct application of Measure.bind_apply from mathlib's Giry monad.

theorem Exchangeability.DeFinetti.CommonEnding.measure_eq_of_agree_on_pi_system {Ω : Type u_3} [MeasurableSpace Ω] (μ ν : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (C : Set (Set Ω)) (hC_pi : IsPiSystem C) (hC_gen : inst✝ = MeasurableSpace.generateFrom C) (h_agree : ∀ s ∈ C, μ s = ν s) : μ = ν

Two finite measures are equal if they agree on a π-system that generates the σ-algebra. This is the key uniqueness result from Dynkin's π-λ theorem.

This is mathlib's Measure.ext_of_generate_finite from Mathlib.MeasureTheory.Measure.Typeclasses.Finite.

The common completion argument

Kallenberg's text says: "The proof can now be completed as before."

This refers to the final step of the first proof, which goes:

1. Have directing measure ν with E[f(ξ_i) | ℱ] = ν^f
2. Use monotone class argument to extend to product sets
3. Show P[∩ Bᵢ | ℱ] = ν^k B for B ∈ 𝒮^k

Proof Strategy Overview

The key insight is to connect three equivalent characterizations of conditional i.i.d.:

A. Bounded Functions (what we have from ergodic theory): For all bounded measurable f and all i: E[f(Xᵢ) | tail] = ∫ f d(ν ω) almost everywhere

B. Indicator Functions (intermediate step): For all measurable sets B and all i: E[𝟙_B(Xᵢ) | tail] = ν(B) almost everywhere

C. Product Sets (what we need for ConditionallyIID): For all m, k, and measurable rectangles B₀ × ... × Bₘ₋₁: μ{ω : ∀ i < m, X_{kᵢ}(ω) ∈ Bᵢ} = ∫ ∏ᵢ ν(Bᵢ) dμ

The progression:

• A → B: Apply A to indicator functions (they're bounded)
• B → C: Use product structure and independence
  • ∏ᵢ 𝟙_{Bᵢ}(Xᵢ) = 𝟙_{B₀×...×Bₘ₋₁}(X₀,...,Xₘ₋₁)
  • E[∏ᵢ 𝟙_{Bᵢ}(Xᵢ)] = ∏ᵢ E[𝟙_{Bᵢ}(Xᵢ)] = ∏ᵢ ν(Bᵢ) (conditional independence!)
• C → ConditionallyIID: π-λ theorem
  • Rectangles form a π-system generating the product σ-algebra
  • Both Measure.map and μ.bind (Measure.pi ν) agree on rectangles
  • By uniqueness of measure extension, they're equal everywhere

This modular structure makes each step verifiable and connects to standard measure theory results.

theorem Exchangeability.DeFinetti.CommonEnding.conditional_iid_from_directing_measure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (ν : Ω → MeasureTheory.Measure α) (hν_prob : ∀ (ω : Ω), MeasureTheory.IsProbabilityMeasure (ν ω)) (hν_meas : ∀ (s : Set α), MeasurableSet s → Measurable fun (ω : Ω) => (ν ω) s) (h_bridge : ∀ {m : ℕ} (k : Fin m → ℕ), Function.Injective k → ∀ (B : Fin m → Set α), (∀ (i : Fin m), MeasurableSet (B i)) → ∫⁻ (ω : Ω), ∏ i : Fin m, ENNReal.ofReal ((B i).indicator (fun (x : α) => 1) (X (k i) ω)) ∂μ = ∫⁻ (ω : Ω), ∏ i : Fin m, (ν ω) (B i) ∂μ) : ConditionallyIID μ X