Block Injection for Disjoint-Block Averaging

This file defines the block injection map used in the disjoint-block averaging argument for de Finetti's theorem via contractability. The block injection allows us to select one element from each of m disjoint blocks, while preserving strict monotonicity (required for contractability).

Main definitions

• blockInjection m n j: For j : Fin m → Fin n, maps:
  • i < m to i * n + j(i) (selects element j(i) from block i)
  • i ≥ m to i + (m * n - m) (shifts the tail)

Main results

• blockInjection_strictMono: The block injection is strictly monotone when n > 0.

Mathematical context

The disjoint-block averaging argument (Kallenberg's "first proof") works as follows:

1. Partition ℕ into m blocks of size n each: [0, n), [n, 2n), ..., [(m-1)n, mn)
2. For each choice function j : Fin m → Fin n, the block injection selects one element from each block while being strictly monotone
3. Average over all n^m such choices to get block averages
4. As n → ∞, block averages converge to conditional expectations

This approach avoids permutations entirely, using only strictly monotone injections, which is exactly what contractability requires.

References

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

Block Injection Definition

def Exchangeability.DeFinetti.blockInjection (m n : ℕ) (j : Fin m → Fin n) : ℕ → ℕ

Block injection: for i < m, select element j(i) from block i; for i ≥ m, shift by m * n - m to avoid collision.

The result is strictly monotone when n > 0, making it suitable for contractability arguments.

Equations

• Exchangeability.DeFinetti.blockInjection m n j i = if h : i < m then i * n + ↑(j ⟨i, h⟩) else i + (m * n - m)

@[simp]

theorem Exchangeability.DeFinetti.blockInjection_apply_lt {m n : ℕ} {j : Fin m → Fin n} {i : ℕ} (hi : i < m) : blockInjection m n j i = i * n + ↑(j ⟨i, hi⟩)

@[simp]

theorem Exchangeability.DeFinetti.blockInjection_apply_ge {m n : ℕ} {j : Fin m → Fin n} {i : ℕ} (hi : m ≤ i) : blockInjection m n j i = i + (m * n - m)

Strict Monotonicity

theorem Exchangeability.DeFinetti.blockInjection_strictMono (m n : ℕ) (hn : 0 < n) (j : Fin m → Fin n) : StrictMono (blockInjection m n j)

Block injection is strictly monotone when block size n > 0.

Reindexing by Block Injection

def Exchangeability.DeFinetti.reindexBlock {α : Type u_1} (m n : ℕ) (j : Fin m → Fin n) (ω : ℕ → α) : ℕ → α

Reindex a sequence by block injection.

Given ω : ℕ → α, j : Fin m → Fin n, produces the sequence where position i has value ω (blockInjection m n j i).

Equations

• Exchangeability.DeFinetti.reindexBlock m n j ω i = ω (Exchangeability.DeFinetti.blockInjection m n j i)

@[simp]

theorem Exchangeability.DeFinetti.reindexBlock_apply {α : Type u_1} (m n : ℕ) (j : Fin m → Fin n) (ω : ℕ → α) (i : ℕ) : reindexBlock m n j ω i = ω (blockInjection m n j i)

theorem Exchangeability.DeFinetti.measurable_reindexBlock {α : Type u_1} [MeasurableSpace α] (m n : ℕ) (j : Fin m → Fin n) : Measurable (reindexBlock m n j)

Reindexing by block injection is measurable.

Block Injection Properties for First m Coordinates

theorem Exchangeability.DeFinetti.blockInjection_val_lt (m n : ℕ) (j : Fin m → Fin n) (i : Fin m) : blockInjection m n j ↑i = ↑i * n + ↑(j i)

The first m values under block injection hit positions in disjoint blocks.

Shift-Invariance of Reindexing

For mSI-sets, reindexing by blockInjection preserves membership because:

1. For i ≥ m: blockInjection(i) = i + (m*n - m) (constant shift)
2. mSI-sets are determined by the tail (coordinates ≥ any M)
3. Therefore membership is preserved

theorem Exchangeability.DeFinetti.reindex_blockInjection_preimage_shiftInvariant {α : Type u_1} [MeasurableSpace α] {m n : ℕ} (_hn : 0 < n) (j : Fin m → Fin n) (s : Set Ω[α]) (hs : isShiftInvariant s) : (fun (ω : ℕ → α) => ω ∘ blockInjection m n j) ⁻¹' s = s

Reindexing by blockInjection preserves membership in shift-invariant sets.

The key insight is that blockInjection is eventually a constant shift: for i ≥ m, blockInjection(i) = i + (m*n - m).

For shift-invariant sets s (where shift⁻¹(s) = s), membership is determined by the eventual behavior of the sequence. Since blockInjection only permutes finitely many coordinates and then shifts, it preserves membership in s.

The _hn : 0 < n hypothesis is unused by the current proof but retained in the signature: callers (e.g. ContractableFactorization) already track it and the hypothesis is informative for readers.