Contractable Factorization: Product Convergence and Kernel Independence

This file completes the disjoint-block averaging argument from Kallenberg's "first proof" of de Finetti's theorem. Building on BlockAverage.lean (which defines block averages and establishes their L¹ convergence), this file proves:

Main results

• product_blockAvg_L1_convergence: Product of block averages converges L¹ to product of CEs.
• measure_map_reindexBlock_eq_of_contractable: Contractability implies path-space measure invariance under block reindexing (via π-λ theorem).
• condexp_product_factorization_contractable: For contractable measures, CE[∏ fᵢ(ωᵢ) | mSI] = ∏ CE[fᵢ(ω₀) | mSI] a.e.

Mathematical context

The proof proceeds as follows:

1. L¹ convergence of products: Using the telescoping bound and individual L¹ convergence of block averages (from BlockAverage.lean), we show that products of block averages converge to products of conditional expectations.

2. Measure invariance from contractability: The π-λ theorem upgrades finite-dimensional contractability to full path-space measure invariance under block reindexing.

3. CE product factorization: Combining L¹ convergence with measure invariance and uniqueness of conditional expectation yields the key factorization result.

References

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

Product L¹ Convergence via Telescoping

theorem Exchangeability.DeFinetti.ViaKoopman.product_blockAvg_L1_convergence {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) {m : ℕ} (fs : Fin m → α → ℝ) (hfs_meas : ∀ (i : Fin m), Measurable (fs i)) (hfs_bd : ∀ (i : Fin m), ∃ (C : ℝ), ∀ (x : α), |fs i x| ≤ C) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω[α]), |∏ i : Fin m, blockAvg m (n + 1) i (fs i) ω - ∏ i : Fin m, μ[fun (ω : Ω[α]) => fs i (ω 0) | shiftInvariantSigma] ω| ∂μ) Filter.atTop (nhds 0)

Product of block averages converges L¹ to product of conditional expectations.

∫ |∏ blockAvg_i - ∏ CE[fᵢ(ω₀) | mSI]| dμ → 0 as n → ∞

Proof uses telescoping bound and individual L¹ convergence of each blockAvg_i.

Path-Space Measure Invariance from Contractability

The key insight (Kallenberg's first proof): finite-dimensional contractability upgrades to full path-space measure invariance via the π-λ theorem. This avoids the need for "conditional contractability" or disintegration.

Kernel Independence from Contractability

The main result: for contractable measures, the product factorization of conditional expectations holds almost surely, giving kernel independence.

theorem Exchangeability.DeFinetti.ViaKoopman.condexp_product_factorization_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 : ℕ} (fs : Fin m → α → ℝ) (hfs_meas : ∀ (i : Fin m), Measurable (fs i)) (hfs_bd : ∀ (i : Fin m), ∃ (C : ℝ), ∀ (x : α), |fs i x| ≤ C) : μ[fun (ω : Ω[α]) => ∏ i : Fin m, fs i (ω ↑i) | shiftInvariantSigma] =ᵐ[μ] fun (ω : Ω[α]) => ∏ i : Fin m, μ[fun (ω' : Ω[α]) => fs i (ω' 0) | shiftInvariantSigma] ω

For contractable measures, product of CEs equals CE of product.

CE[∏ fᵢ(ωᵢ) | mSI] = ∏ CE[fᵢ(ω₀) | mSI] a.e.

This is the key factorization that yields conditional i.i.d.

Bridge to CommonEnding

The CE-based factorization above feeds indicator_product_bridge_contractable (in Exchangeability/DeFinetti/BridgeProperty.lean), which converts it into the shape consumed by CommonEnding.conditional_iid_from_directing_measure. The construction is: for injective k, sort to obtain a strictly-monotone ρ with permutation σ such that k = ρ ∘ σ, apply contractability to get integral equality, and combine with the CE factorization via the ν ↔ conditional expectation identification.