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.abs_prod_sub_prod_le_general {m : ℕ} (A B : Fin m → ℝ) {C : ℝ} (hC : 0 < C) (hA : ∀ (i : Fin m), |A i| ≤ C) (hB : ∀ (i : Fin m), |B i| ≤ C) : |∏ i : Fin m, A i - ∏ i : Fin m, B i| ≤ C ^ (m - 1) * ∑ i : Fin m, |A i - B i|

Telescoping bound for product differences with general bound C.

Extends abs_prod_sub_prod_le (which requires bound 1) to general bounds via normalization. For functions bounded by C > 0: |∏ A - ∏ B| ≤ C^{m-1} * ∑ |A_i - B_i|

This is derived from abs_prod_sub_prod_le by dividing by C.

theorem Exchangeability.DeFinetti.ViaKoopman.prod_diff_bound {m : ℕ} {A B : Fin m → ℝ} {C : ℝ} (hC : 0 ≤ C) (hA : ∀ (i : Fin m), |A i| ≤ C) (hB : ∀ (i : Fin m), |B i| ≤ C) : |∏ i : Fin m, A i - ∏ i : Fin m, B i| ≤ if h : 0 < m then ↑m * C ^ (m - 1) * Finset.univ.sup' ⋯ fun (i : Fin m) => |A i - B i| else 0

Telescoping bound for product differences.

|∏ Aᵢ - ∏ Bᵢ| ≤ m * C^{m-1} * max |Aᵢ - Bᵢ|

when |Aᵢ|, |Bᵢ| ≤ C for all i.

Note: When m = 0, both products are 1, so the LHS is 0 and the RHS is 0. For m > 0, we use Finset.univ.sup' with nonemptiness.

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.

theorem Exchangeability.DeFinetti.ViaKoopman.measure_map_reindexBlock_eq_of_contractable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (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 n : ℕ} (hn : 0 < n) (j : Fin m → Fin n) : MeasureTheory.Measure.map (reindexBlock m n j) μ = μ

Finite-dimensional contractability upgrades to path-space measure invariance.

Given contractability (finite marginals on {k(0), ..., k(m-1)} equal marginals on {0, ..., m-1}), we show that the pushforward under reindexing by any strictly monotone ρ equals the original measure. This is the π-λ argument: finite marginal equality → full measure equality.

theorem Exchangeability.DeFinetti.ViaKoopman.setIntegral_comp_reindexBlock_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] {m n : ℕ} {j : Fin m → Fin n} (hμ : MeasureTheory.Measure.map (reindexBlock m n j) μ = μ) {s : Set Ω[α]} (hs_meas : MeasurableSet s) (hs_inv : reindexBlock m n j ⁻¹' s = s) {f : Ω[α] → ℝ} (hf_meas : AEMeasurable f μ) : ∫ (ω : Ω[α]) in s, f (reindexBlock m n j ω) ∂μ = ∫ (ω : Ω[α]) in s, f ω ∂μ

Set integral equality from measure invariance and set invariance.

If the measure is invariant under reindexing (μ = μ ∘ reindexBlock⁻¹) and the set is invariant under reindexing (s = reindexBlock⁻¹(s)), then ∫_s f ∘ reindexBlock = ∫_s f.

This is the key lemma that replaces "conditional contractability".

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 bridge lemma indicator_product_bridge_contractable would connect the CE-based factorization in this file to the ConditionallyIID definition required by CommonEnding.conditional_iid_from_directing_measure.

The key insight is:

• For injective k, sort to get StrictMono ρ with permutation σ such that k = ρ ∘ σ
• Apply contractability to get integral equality
• Use CE factorization and the ν ↔ CE relationship

This bridge is needed to complete the sorry at line 178 of TheoremViaKoopman.lean, which proves Contractable μ X → Exchangeable μ X ∧ ConditionallyIID μ X.

Status: Incomplete. The path-space proof in ViaKoopman.lean is complete; the original-space bridge requires additional work to match the ConditionallyIID definition's bind-based formula.