Dependencies

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 block average \(A_n = \frac{1}{n}\sum _{i=0}^{n-1} f(X_i)\) for bounded measurable \(f\).

A sequence \((X_n)_{n \in \mathbb {N}}\) is conditionally i.i.d. with respect to measure \(\mu \) if there exists a probability kernel \(\nu : \Omega \to \mathrm{Measure}(\alpha )\) such that for any strictly monotone \(k : \mathrm{Fin}(m) \to \mathbb {N}\), the joint distribution of \((X_{k(0)}, \ldots , X_{k(m-1)})\) equals the mixture \(\mu .\mathrm{bind}(\omega \mapsto \nu (\omega )^{\otimes m})\).

A sequence \((X_n)_{n \in \mathbb {N}}\) is contractable with respect to measure \(\mu \) if for all \(m \in \mathbb {N}\) and all strictly increasing functions \(k, k' : \mathrm{Fin}(m) \to \mathbb {N}\), the joint distribution of \((X_{k(0)}, \ldots , X_{k(m-1)})\) equals that of \((X_{k'(0)}, \ldots , X_{k'(m-1)})\).

A sequence \((X_n)_{n \in \mathbb {N}}\) of random variables is exchangeable with respect to measure \(\mu \) if for every \(n \in \mathbb {N}\) and every permutation \(\sigma \) of \(\{ 0, \ldots , n-1\} \), the joint distribution of \((X_{\sigma (0)}, \ldots , X_{\sigma (n-1)})\) equals that of \((X_0, \ldots , X_{n-1})\).

The future filtration at level \(m\) is \(\mathcal{F}_m = \sigma (X_{m+1}, X_{m+2}, \ldots )\).

The (one-sided) shift-invariant \(\sigma \)-algebra on path space \(\mathbb {N} \to \alpha \) consists of measurable sets \(S\) such that \(\theta ^{-1}(S) = S\), where \(\theta \) is the left shift. A two-sided counterpart on \(\mathbb {Z} \to \alpha \), ViaKoopman.shiftInvariantSigma\(\mathbb {Z}\), is introduced separately as scaffolding for the Koopman route’s lag-constancy lemmas.

The tail \(\sigma \)-algebra of a sequence \((X_n)\) is \(\mathcal{T} = \bigcap _{n=0}^{\infty } \sigma (X_n, X_{n+1}, \ldots )\).

Coordinates are conditionally independent given the tail \(\sigma \)-algebra.

For contractable \(X\) and bounded \(f\), the block Cesaro averages \(\mathrm{blockAvg}\, f\, X\, 0\, n\) form a Cauchy sequence in L\(^2\).

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 \).

Block averages converge in L\(^1\) to the conditional expectation given the tail.

Block averages converge in L\(^2\) to the conditional expectation given the tail.

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 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.

For exchangeable sequences, the conditional expectation of a product does not depend on the lag between coordinates.

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.

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, the covariance \(\mathrm{Cov}(f(X_i), f(X_j))\) is constant for \(i \ne j\).

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 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.

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\).

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.

For finite products of indicators, the conditional expectation given \(\mathcal{F}_m\) factors as a product of individual conditional expectations.

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.

The future filtration is antitone: \(m \le n\) implies \(\mathcal{F}_n \le \mathcal{F}_m\).

For contractable sequences, indicator products satisfy the bridge condition.

For contractable sequences, integrals of products factor through block averages.

Conditional expectations of indicators given the reverse filtration converge to conditional expectations given the tail \(\sigma \)-algebra.

The conditional expectation operator onto the shift-invariant subspace commutes with the Koopman operator.

For contractable sequences, certain L\(^2\) norms of block averages are bounded.

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 )\).

Any strictly increasing function \(k : \mathrm{Fin}(m) \to \mathbb {N}\) with range contained in \(\{ 0, \ldots , n-1\} \) extends to a permutation of \(\{ 0, \ldots , n-1\} \).

Measures on product spaces are determined by their finite-dimensional marginals.

Products of block averages converge in L\(^1\).

The tail \(\sigma \)-algebra factorization follows from the finite-level factorization via reverse martingale convergence.

For all \(m\): \(\mathcal{T} \le \mathcal{F}_m\).

Birkhoff averages converge in L\(^2\) to the conditional expectation given the shift-invariant \(\sigma \)-algebra.

For contractable sequences, the conditional expectation of a product of indicators factors as a product of conditional expectations.

Conditional independence on indicators extends to the full product \(\sigma \)-algebra.

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\).

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.

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.

If \((X_n)\) is exchangeable, then it is contractable.

For an infinite sequence \((X_n)_{n \in \mathbb {N}}\) of random variables taking values in a standard Borel space \(\alpha \) (with \(\alpha \) nonempty), the following are equivalent:

1. \((X_n)\) is contractable

2. \((X_n)\) is exchangeable

3. \((X_n)\) is conditionally i.i.d. (i.e., there exists a directing kernel \(\nu \))

This is the default project export. The proof constructs \(\nu \) from the tail \(\sigma \)-algebra \(\mathcal{T}\) via \(\nu (\omega )(B) = \mathbb {E}[\mathbf{1}_{X_0 \in B} \mid \mathcal{T}](\omega )\).

Same three-way equivalence, proved via the Mean Ergodic Theorem through the Koopman operator. This route is currently stated for real-valued sequences (see the Koopman section caveat).

Same three-way equivalence, proved via the elementary L\(^2\) approach. This route is currently stated for real-valued sequences (see the L\(^2\) section caveat).

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.

If \((X_n)\) is conditionally i.i.d., then it is exchangeable.

The monotone class theorem allows extending from indicators to measurable functions.

The weighted sums of indicators converge in L\(^1\).