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.

def Exchangeability.DeFinetti.CommonEnding.invariantSigmaField (α : Type u_3) [MeasurableSpace α] : MeasurableSpace (ℕ → α)

The invariant σ-field ℐ consists of all measurable shift-invariant sets. Following FMP 10.2, this forms a σ-field.

Equations

• Exchangeability.DeFinetti.CommonEnding.invariantSigmaField α = MeasurableSpace.comap Exchangeability.PathSpace.shift inferInstance

def Exchangeability.DeFinetti.CommonEnding.IsAlmostShiftInvariant {α : Type u_3} [MeasurableSpace α] (μ : MeasureTheory.Measure (ℕ → α)) (S : Set (ℕ → α)) : Prop

A measure on the path space is almost shift-invariant on a set S if μ(S ∆ shift⁻¹(S)) = 0 (symmetric difference). This is the analogue of FMP 10.2's almost invariance.

Equations

• Exchangeability.DeFinetti.CommonEnding.IsAlmostShiftInvariant μ S = (μ (S \ Exchangeability.PathSpace.shift ⁻¹' S ∪ Exchangeability.PathSpace.shift ⁻¹' S \ S) = 0)

def Exchangeability.DeFinetti.CommonEnding.tailSigmaAlgebra (α : Type u_3) [MeasurableSpace α] : MeasurableSpace (ℕ → α)

The tail σ-algebra for infinite sequences consists of events that are "asymptotically independent" of the first n coordinates for all n.

Now using the canonical definition from Exchangeability.Tail.tailShift, defined as ⨅ n, comap (shift^n) inferInstance.

For exchangeable sequences, this equals the shift-invariant σ-field (to be proven using FMP 10.3-10.4).

Equations

• Exchangeability.DeFinetti.CommonEnding.tailSigmaAlgebra α = Exchangeability.Tail.tailShift α

def Exchangeability.DeFinetti.CommonEnding.IsTailMeasurable {α : Type u_3} {β : Type u_4} [MeasurableSpace α] [MeasurableSpace β] (f : (ℕ → α) → β) : Prop

A function on the path space is tail-measurable if it's measurable with respect to the tail σ-algebra. By FMP 10.3, this is equivalent to being (almost) shift-invariant.

Equations

• Exchangeability.DeFinetti.CommonEnding.IsTailMeasurable f = Measurable f

def Exchangeability.DeFinetti.CommonEnding.IsAlmostTailMeasurable {α : Type u_3} {β : Type u_4} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure (ℕ → α)) (f : (ℕ → α) → β) : Prop

For a probability measure μ on path space, a function is almost tail-measurable if it differs from a tail-measurable function on a μ-null set. By FMP 10.4, this is equivalent to measurability w.r.t. the μ-completion of the invariant σ-field.

Note: A more complete formalization would use measure completion.

Equations

• Exchangeability.DeFinetti.CommonEnding.IsAlmostTailMeasurable μ f = ∃ (g : (ℕ → α) → β), Exchangeability.DeFinetti.CommonEnding.IsTailMeasurable g ∧ f =ᵐ[μ] g

Helper lemmas for product measures

These lemmas establish the connection between bounded functions and indicator functions, which is essential for the monotone class argument.

theorem Exchangeability.DeFinetti.CommonEnding.indicator_bounded {α : Type u_3} {s : Set α} : ∃ (M : ℝ), ∀ (x : α), |s.indicator (fun (x : α) => 1) x| ≤ M

Indicator functions are bounded. This is a trivial but useful fact for the monotone class extension.

theorem Exchangeability.DeFinetti.CommonEnding.indicator_mem_zero_one {α : Type u_3} {s : Set α} {x : α} : ENNReal.ofReal (s.indicator (fun (x : α) => 1) x) ∈ {0, 1}

The ENNReal value of an indicator function is either 0 or 1.

theorem Exchangeability.DeFinetti.CommonEnding.indicator_le_one {α : Type u_3} {s : Set α} {x : α} : ENNReal.ofReal (s.indicator (fun (x : α) => 1) x) ≤ 1

The ENNReal value of an indicator function is at most 1.

theorem Exchangeability.DeFinetti.CommonEnding.prod_eq_zero_iff {ι : Type u_3} [Fintype ι] {f : ι → ENNReal} : ∏ i : ι, f i = 0 ↔ ∃ (i : ι), f i = 0

A product of ENNReal values equals 0 iff at least one factor is 0.

theorem Exchangeability.DeFinetti.CommonEnding.prod_eq_one_iff_of_zero_one {ι : Type u_3} [Fintype ι] {f : ι → ENNReal} (hf : ∀ (i : ι), f i ∈ {0, 1}) : ∏ i : ι, f i = 1 ↔ ∀ (i : ι), f i = 1

For values in {0, 1}, the product equals 1 iff all factors equal 1.

theorem Exchangeability.DeFinetti.CommonEnding.prod_le_one_of_le_one {ι : Type u_3} [Fintype ι] {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≤ 1) : ∏ i : ι, f i ≤ 1

The product of finitely many terms, each bounded by 1, is bounded by 1. This is useful for products of indicator functions.

theorem Exchangeability.DeFinetti.CommonEnding.measurable_indicator_comp {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] (f : Ω → α) (hf : Measurable f) (s : Set α) (hs : MeasurableSet s) : Measurable fun (ω : Ω) => ENNReal.ofReal (s.indicator (fun (x : α) => 1) (f ω))

The ENNReal indicator function composed with a measurable function is measurable.

theorem Exchangeability.DeFinetti.CommonEnding.product_bounded {ι : Type u_3} [Fintype ι] {α : Type u_4} (f : ι → α → ℝ) (hf : ∀ (i : ι), ∃ (M : ℝ), ∀ (x : α), |f i x| ≤ M) : ∃ (M : ℝ), ∀ (x : α), |∏ i : ι, f i x| ≤ M

The product of bounded functions is bounded.

Uses mathlib's Finset.prod_le_prod to bound product by product of bounds.

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.map_coords_apply {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} (X : ℕ → Ω → α) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (m : ℕ) (k : Fin m → ℕ) (B : Set (Fin m → α)) (hB : MeasurableSet B) : (MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k i) ω) μ) B = μ {ω : Ω | (fun (i : Fin m) => X (k i) ω) ∈ B}

Pushforward of a measure through coordinate selection equals the marginal distribution. This connects the map in the ConditionallyIID definition to the probability of events.

This is a direct application of Measure.map_apply from mathlib.

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

theorem Exchangeability.DeFinetti.CommonEnding.monotone_class_theorem {Ω' : Type u_3} {m : MeasurableSpace Ω'} {C : (s : Set Ω') → MeasurableSet s → Prop} {s : Set (Set Ω')} (h_eq : m = MeasurableSpace.generateFrom s) (h_inter : IsPiSystem s) (empty : C ∅ ⋯) (basic : ∀ (t : Set Ω') (ht : t ∈ s), C t ⋯) (compl : ∀ (t : Set Ω') (htm : MeasurableSet t), C t htm → C tᶜ ⋯) (iUnion : ∀ (f : ℕ → Set Ω'), (Pairwise fun (i j : ℕ) => Disjoint (f i) (f j)) → ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ (i : ℕ), f i) ⋯) {t : Set Ω'} (htm : MeasurableSet t) : C t htm

FMP 1.1: Monotone Class Theorem (Sierpiński) = Dynkin's π-λ theorem.

Let 𝒞 be a π-system and 𝒟 a λ-system in some space Ω such that 𝒞 ⊆ 𝒟. Then σ(𝒞) ⊆ 𝒟.

Proof outline (Kallenberg):

1. Assume 𝒟 = λ(𝒞) (smallest λ-system containing 𝒞)
2. Show 𝒟 is a π-system (then it's a σ-field)
3. Two-step extension:
   • Fix B ∈ 𝒞, define 𝒜_B = {A : A ∩ B ∈ 𝒟}, show 𝒜_B is λ-system ⊇ 𝒞
   • Fix A ∈ 𝒟, define ℬ_A = {B : A ∩ B ∈ 𝒟}, show ℬ_A is λ-system ⊇ 𝒞

Mathlib version: MeasurableSpace.induction_on_inter

Mathlib's version is stated as an induction principle: if a predicate C holds on:

• The empty set
• All sets in the π-system 𝒞
• Is closed under complements
• Is closed under countable disjoint unions

Then C holds on all measurable sets in σ(𝒞).

Definitions in mathlib:

• IsPiSystem: A collection closed under binary non-empty intersections (Mathlib/MeasureTheory/PiSystem.lean)
• DynkinSystem: A structure containing ∅, closed under complements and countable disjoint unions (Mathlib/MeasureTheory/PiSystem.lean)
• induction_on_inter: The π-λ theorem as an induction principle (Mathlib/MeasureTheory/PiSystem.lean)

This theorem is now a direct wrapper around mathlib's induction_on_inter.

theorem Exchangeability.DeFinetti.CommonEnding.complete_from_directing_measure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (_hX_contract : Contractable μ X) (ν : Ω → 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

Package the common ending as a reusable theorem.

Given a contractable sequence and a directing measure ν constructed via either approach (Mean Ergodic Theorem or L² bound), this completes the proof to conditional i.i.d.

This encapsulates the "completed as before" step.