5 Common Ending
The L\(^2\) and Koopman routes share a common final step: a directing kernel built from the tail (or shift-invariant) \(\sigma \)-algebra is fed to a \(\pi \)-system / monotone-class extension argument that lifts the indicator-level identity to the full product \(\sigma \)-algebra. The martingale route reaches conditional independence through its own parallel finite_product_formula pipeline (built on condExpKernel) rather than the lemmas in this chapter.
5.1 Comparing the two endings
The L²/Koopman ending (49, in CommonEnding.lean) and the martingale ending (24, in ViaMartingale/FiniteProduct.lean) are similar in total length and both finish with a rectangle \(\pi \)-system extension via MeasureTheory.ext_of_generate_finite. The substantive difference is the shape of the bridge condition each accepts about the directing kernel \(\nu \).
|
Route |
Bridge shape |
How the route produces it |
|
Martingale |
Per-coordinate conditional-expectation equality: \((\omega \mapsto \nu (\omega )(B).\mathrm{toReal}) \, =^{\mathrm{a.e.}} \, \mathbb {E}[\mathbf{1}_B \circ X_n \mid \mathcal{T}]\) for every \(n\), \(B\) (see 23). |
Falls out directly from mathlib’s condExpKernel applied to the tail \(\sigma \)-algebra. |
|
L²/Koopman |
Joint integral equality on the whole \(m\)-tuple: for every injective \(k : \mathrm{Fin}\, m \to \mathbb {N}\) and rectangle \(B\), \(\int ^- \prod _i \mathbf{1}_{X_{k\, i} \in B_i}\, d\mu = \int ^- \prod _i \nu (\omega )(B_i)\, d\mu .\) |
Falls out of Cesàro / ergodic averaging — both sides are limits of the same averaged sequence. |
Why this matters.
Each route’s directing-measure construction naturally produces the bridge shape its own ending expects, so the routes pick the ending that matches what they already have. The martingale route’s per-coordinate bridge is “smaller” (one σ-algebra-relative equality per index) and is what condExpKernel delivers without extra work; the common ending’s joint integral bridge is what limit-of-averages arguments deliver without extra work, but would be wasteful if you already had per-coordinate CE equalities. At the stitching level both routes compress to a short top-level theorem that hands a 4-tuple \((\nu , h_{\nu \text{-prob}}, h_{\nu \text{-meas}}, h_{\text{bridge}})\) to the chosen ending — the choice of ending is what differs, not the amount of stitching.
Measures on product spaces are determined by their finite-dimensional marginals.
The monotone class theorem allows extending from indicators to measurable functions.
Conditional independence on indicators extends to the full product \(\sigma \)-algebra.