Block Averages for Contractable Factorization

This file defines block averages and proves their L¹ convergence to conditional expectations. These are the foundational lemmas for the disjoint-block averaging argument in Kallenberg's "first proof" of de Finetti's theorem.

Main definitions

• blockAvg m n k f ω: Block average of f at position k with m blocks of size n. Computes (1/n) * ∑_{j=0}^{n-1} f(ω(k*n + j)).

Main results

• blockAvg_tendsto_condExp: Block averages converge L¹ to conditional expectation.
• integral_prod_reindex_of_contractable: Contractability gives integral equality under reindexing.
• integral_prod_eq_integral_blockAvg: Averaging over choice functions yields block averages.

References

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

Block Average Definition

def Exchangeability.DeFinetti.ViaKoopman.blockAvg {α : Type u_1} (m n : ℕ) (k : Fin m) (f : α → ℝ) (ω : ℕ → α) : ℝ

Block average of function f at position k with m blocks of size n.

For coordinate k < m, computes the average of f(ω(k*n + j)) over j ∈ {0, ..., n-1}. This is the Cesàro average of f starting at coordinate k*n.

Equations

• Exchangeability.DeFinetti.ViaKoopman.blockAvg m n k f ω = if hn : n = 0 then 0 else 1 / ↑n * ∑ j ∈ Finset.range n, f (ω (↑k * n + j))

@[simp]

theorem Exchangeability.DeFinetti.ViaKoopman.blockAvg_zero_n {α : Type u_1} [MeasurableSpace α] (m : ℕ) (k : Fin m) (f : α → ℝ) (ω : ℕ → α) : blockAvg m 0 k f ω = 0

theorem Exchangeability.DeFinetti.ViaKoopman.blockAvg_pos_n {α : Type u_1} [MeasurableSpace α] {m n : ℕ} (hn : 0 < n) (k : Fin m) (f : α → ℝ) (ω : ℕ → α) : blockAvg m n k f ω = 1 / ↑n * ∑ j ∈ Finset.range n, f (ω (↑k * n + j))

Block Average and Shifted Cesàro Averages

theorem Exchangeability.DeFinetti.ViaKoopman.blockAvg_eq_cesaro_shifted {α : Type u_1} [MeasurableSpace α] {m n : ℕ} (hn : 0 < n) (k : Fin m) (f : α → ℝ) (ω : ℕ → α) : blockAvg m n k f ω = 1 / ↑n * ∑ j ∈ Finset.range n, f (PathSpace.shift^[↑k * n] ω j)

Block average at position k equals Cesàro average starting at k*n.

This connects block averages to the existing Cesàro convergence machinery.

Measurability of Block Averages

theorem Exchangeability.DeFinetti.ViaKoopman.measurable_blockAvg {α : Type u_1} [MeasurableSpace α] {m n : ℕ} (k : Fin m) {f : α → ℝ} (hf : Measurable f) : Measurable (blockAvg m n k f)

theorem Exchangeability.DeFinetti.ViaKoopman.blockAvg_abs_le {α : Type u_1} [MeasurableSpace α] {m n : ℕ} (k : Fin m) {f : α → ℝ} {C : ℝ} (hC : 0 ≤ C) (hf_bd : ∀ (x : α), |f x| ≤ C) (ω : Ω[α]) : |blockAvg m n k f ω| ≤ C

Block averages of bounded functions are bounded.

If |f x| ≤ C for all x, then |blockAvg m n k f ω| ≤ C for all ω. This follows because blockAvg is a convex combination of values of f.

Block Average L¹ Convergence

The key observation is that block average at position k is a Cesàro average starting at k*n. By condexp_precomp_iterate_eq, the conditional expectation of f(ω(k*n)) equals CE[f(ω₀) | mSI]. The existing Cesàro convergence machinery then gives L¹ convergence.

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

Block averages converge in L¹ to conditional expectation.

For each fixed k, as n → ∞: ∫ |blockAvg m n k f ω - μ[f(ω₀) | mSI] ω| dμ → 0

This follows from the Cesàro convergence theorem since blockAvg at position k is a Cesàro average starting at coordinate k*n, and by condexp_precomp_iterate_eq, the target CE is the same regardless of the starting position.

Contractability and Block Average Factorization

The core of Kallenberg's first proof: contractability gives integral factorization via averaging over all choice functions.

theorem Exchangeability.DeFinetti.ViaKoopman.integral_prod_reindex_of_contractable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (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) {k : Fin m → ℕ} (hk : StrictMono k) : ∫ (ω : Ω[α]), ∏ i : Fin m, fs i (ω ↑i) ∂μ = ∫ (ω : Ω[α]), ∏ i : Fin m, fs i (ω (k i)) ∂μ

For contractable μ, integral of product equals integral of product with reindexed coordinates.

Given strict monotone k : Fin m → ℕ, contractability says: ∫ ∏ᵢ fᵢ(ωᵢ) dμ = ∫ ∏ᵢ fᵢ(ω(k(i))) dμ

This is the fundamental identity that lets us swap between original and reindexed coordinates.

theorem Exchangeability.DeFinetti.ViaKoopman.integral_prod_eq_integral_blockAvg {α : 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 n : ℕ} (hn : 0 < n) (fs : Fin m → α → ℝ) (hfs_meas : ∀ (i : Fin m), Measurable (fs i)) (hfs_bd : ∀ (i : Fin m), ∃ (C : ℝ), ∀ (x : α), |fs i x| ≤ C) : ∫ (ω : Ω[α]), ∏ i : Fin m, fs i (ω ↑i) ∂μ = ∫ (ω : Ω[α]), ∏ i : Fin m, blockAvg m n i (fs i) ω ∂μ

Averaging over all choice functions yields product of block averages.

For any bounded measurable fs : Fin m → α → ℝ: ∫ ∏ᵢ fᵢ(ωᵢ) dμ = ∫ ∏ᵢ blockAvg m n i fᵢ ω dμ

This is proved by:

1. For each j : Fin m → Fin n, contractability gives ∫ ∏ fᵢ(ωᵢ) = ∫ ∏ fᵢ(ω(ρⱼ(i)))
2. Sum over all j and divide by n^m to get block averages