4 Main Implication: Contractable implies Conditionally i.i.d.
This is the deep direction of de Finetti’s theorem. We formalize three independent proofs.
4.1 Via Martingale (Aldous’ proof)
The martingale approach uses reverse martingale convergence to the tail \(\sigma \)-algebra.
4.1.1 Pair Law Equality
For a contractable sequence and \(k \le m\), the joint distribution of \((X_k, X_{m+1}, X_{m+2}, \ldots )\) equals that of \((X_m, X_{m+1}, X_{m+2}, \ldots )\).
For a contractable sequence, the joint distribution of \((X_k, \theta _{m+1} X)\) equals that of \((X_m, \theta _{m+1} X)\) for all \(k \le m\), where \(\theta _n\) is the shift operator.
For contractable sequences and \(k \le m\): \(\mathbb {E}[\mathbf{1}_{X_k \in B} \mid \mathcal{F}_m] = \mathbb {E}[\mathbf{1}_{X_m \in B} \mid \mathcal{F}_m]\) a.s.
4.1.2 Kallenberg Chain and Convergence
Conditional expectations of indicators given the reverse filtration converge to conditional expectations given the tail \(\sigma \)-algebra.
For \(k \le m\) and measurable \(B\): \(\mathbb {E}[\mathbf{1}_{X_m \in B} \mid \mathcal{F}_m] = \mathbb {E}[\mathbf{1}_{X_k \in B} \mid \mathcal{F}_m]\) a.s.
For any measurable \(B\): \(\mathbb {E}[\mathbf{1}_{X_m \in B} \mid \mathcal{T}] = \mathbb {E}[\mathbf{1}_{X_0 \in B} \mid \mathcal{T}]\) a.s.
4.1.3 Factorization and Directing Measure
For finite products of indicators, the conditional expectation given \(\mathcal{F}_m\) factors as a product of individual conditional expectations.
The tail \(\sigma \)-algebra factorization follows from the finite-level factorization via reverse martingale convergence.
Coordinates are conditionally independent given the tail \(\sigma \)-algebra.
The directing measure \(\nu (\omega )(B) = \mathbb {E}[\mathbf{1}_{X_0 \in B} \mid \mathcal{T}](\omega )\) is a probability measure for every \(\omega \) (the bound is pointwise, not merely a.e., via mathlib’s isProbability_condExpKernel).
The directing measure \(\omega \mapsto \nu (\omega )(B)\) is measurable for each Borel \(B\).
Per-coordinate identification: for every \(n\) and every Borel \(B\), \((\omega \mapsto \nu (\omega )(B).\mathrm{toReal}) \, =^{\mu \text{-a.e.}} \, \mathbb {E}[\mathbf{1}_B \circ X_n \mid \mathcal{T}]\). This is the bridge condition consumed by 24 below.
Under contractability, for every strictly monotone selection \(k : \mathrm{Fin}\, m \to \mathbb {N}\) and any kernel \(\nu \) satisfying the per-coordinate bridge 23:
This is the martingale route’s analogue of the L²/Koopman 49: it bundles the rectangle \(\pi \)-system extension and the \(\mathrm{Measure.map} = \mathrm{bind}\) identification into one step driven by per-coordinate conditional expectations.
If \((X_n)\) is contractable, then it is conditionally i.i.d. The directing kernel \(\nu (\omega )(B) = \mathbb {E}[\mathbf{1}_{X_0 \in B} \mid \mathcal{T}](\omega )\) is constructed from the tail \(\sigma \)-algebra, identified per-coordinate by 23, and lifted to the joint law by 24 — bypassing the L²/Koopman common-ending step.
4.2 Via L\(^2\) (Elementary proof)
The L\(^2\) approach uses elementary contractability bounds on block averages. This is Kallenberg’s “second proof” and has the lightest dependencies.
Note: This proof applies to real-valued sequences (\(X : \mathbb {N} \to \Omega \to \mathbb {R}\)) with \(L^2\) integrability (i.e., \(\mathbb {E}[X_i^2] {\lt} \infty \) for all \(i\)).
4.2.1 Block Averages and Covariance Structure
The block average \(A_n = \frac{1}{n}\sum _{i=0}^{n-1} f(X_i)\) for bounded measurable \(f\).
For contractable sequences, the covariance \(\mathrm{Cov}(f(X_i), f(X_j))\) is constant for \(i \ne j\).
For contractable sequences, certain L\(^2\) norms of block averages are bounded.
4.2.2 Cesaro Convergence
Recorded Kallenberg L\(^2\) bound.
Kallenberg’s Lemma 1.2 gives an L\(^2\) distance bound for weighted averages of an exchangeable sequence. It is recorded in the Lean library as Exchangeability.DeFinetti.ViaL2.kallenberg_L2_bound for completeness, but it is not on the active proof path — the route below uses the contractability-only variant 28 so that the proof of Contractable \(\Rightarrow \) Conditionally i.i.d. does not assume exchangeability.
For contractable \(X\) and bounded \(f\), the block Cesaro averages \(\mathrm{blockAvg}\, f\, X\, 0\, n\) form a Cauchy sequence in L\(^2\).
Block averages converge in L\(^2\) to the conditional expectation given the tail.
Block averages converge in L\(^1\) to the conditional expectation given the tail.
4.2.3 Directing Measure Construction
The L\(^2\) route now goes through mathlib’s condExpKernel machinery: the Stieltjes construction supplies the candidate directing measure \(\omega \mapsto \nu (\omega )\), and a pair of bridge lemmas identifies its push-forward and integral with the kernel coming from mathlib’s condExpKernel on the tail \(\sigma \)-algebra. The shared common-ending theorem then lifts the indicator-level identity to the full product \(\sigma \)-algebra.
The Stieltjes measure constructed from the limiting CDF is a probability measure for every \(\omega \) (pointwise, not merely a.e.). Monotonicity, bounds, and right-continuity of the underlying CDF are inherited directly from mathlib’s stieltjesOfMeasurableRat construction.
Almost everywhere in \(\omega \), the Stieltjes-built directing measure coincides with the push-forward of mathlib’s condExpKernel \(\mu \) \(\mathcal{T}\) \(\omega \) by \(X_0\). This is the kernel-level bridge from the analytic L\(^2\) construction to mathlib’s conditional-expectation kernel API.
For a bounded measurable function \(f\), the integral \(\int f \, d\nu (\omega )\) against the directing measure equals \(\mathbb {E}[f \circ X_0 \mid \mathcal{T}](\omega )\) almost everywhere. This is the shape consumed by the shared common-ending step.
The weighted sums of indicators converge in L\(^1\).
If \((X_n)\) is contractable (and real-valued), then it is conditionally i.i.d. Scope note: the L\(^2\) route is currently stated for real-valued sequences via the Stieltjes-based directing-measure construction; extending it to general standard Borel targets would require a measure-disintegration replacement for the Stieltjes step.
4.3 Via Koopman (Mean Ergodic Theorem)
The Koopman approach uses the Mean Ergodic Theorem via the shift operator on L\(^2\). This is Kallenberg’s “first proof” and uses disjoint-block averaging.
Scope note: the Koopman route is currently stated for real-valued sequences (the Mean Ergodic Theorem is invoked through L\(^2(\mu ; \mathbb {R})\) on path space). Generalising to standard Borel targets would require an L\(^2\)-valued ergodic infrastructure beyond what is presently formalised. The default project export (50) handles general standard Borel spaces via the martingale route.
4.3.1 Block Averages and Ergodic Theory
The block average \(A_{m,n,k}(f)(\omega ) = \frac{1}{n} \sum _{j=0}^{n-1} f(\omega _{k \cdot n + j})\) averages \(f\) over the \(k\)-th block of size \(n\) (indices \([kn, kn+n)\)). For \(n = 0\), the block average is defined as \(0\).
The conditional expectation operator onto the shift-invariant subspace commutes with the Koopman operator.
Birkhoff averages converge in L\(^2\) to the conditional expectation given the shift-invariant \(\sigma \)-algebra.
For a shift-invariant measure, block averages converge in \(L^1\) to the conditional expectation given the shift-invariant \(\sigma \)-algebra: \(\int |A_{m,n,k}(f) - \mathbb {E}[f \circ \pi _0 \mid \mathcal{I}]| \, d\mu \to 0\) as \(n \to \infty \).
4.3.2 Contractability and Factorization
For exchangeable sequences, the conditional expectation of a product does not depend on the lag between coordinates.
For contractable sequences, integrals of products factor through block averages.
Products of block averages converge in L\(^1\).
For contractable sequences, the conditional expectation of a product of indicators factors as a product of conditional expectations.
For contractable sequences, indicator products satisfy the bridge condition.
If \((X_n)\) is contractable, then it is conditionally i.i.d. This proof uses the Mean Ergodic Theorem via the Koopman operator on L\(^2\).