Chain law from an initial distribution, sample averages, and the CLT property

chainMeasure — For a measurable type $X$, a kernel $P$ from $X$ to $X$ assumed (typeclass) to be a Markov kernel (each $P(x,\cdot)$ a probability measure), and an arbitrary measure $\lambda$ on $X$ (not assumed to be a probability measure in this definition), $\mathrm{chainMeasure}\,P\,\lambda$ is the measure on the sequence space $\mathbb{N} \to X$ obtained by composing the kernel $\mathrm{markovChainKernel}\,P$ with $\lambda$: the measure $B \mapsto \int (\mathrm{markovChainKernel}\,P)(x)(B)\, d\lambda(x)$. Unfolding the imported declaration: $\mathrm{markovChainKernel}\,P$ is the Ionescu–Tulcea trajectory kernel built from the step kernels which map a finite history $(\omega_0,\dots,\omega_n)$ (a function on $\{0,\dots,n\}$) to the measure $P(\omega_n,\cdot)$ — the next state depends only on the last coordinate, through $P$ — precomposed with the map sending $x$ to the one-point time-$0$ history with value $x$; an accompanying lemma identifies $(\mathrm{markovChainKernel}\,P)(x)$ with the trajectory measure started from $\delta_x$. Concretely, $(\mathrm{markovChainKernel}\,P)(x)$ is the probability measure on $\mathbb{N} \to X$ under which coordinate $0$ equals $x$ almost surely and, for each $n$, the conditional law of coordinate $n+1$ given coordinates $0,\dots,n$ is $P(\omega_n,\cdot)$. So $\mathrm{chainMeasure}\,P\,\lambda$ is this path law with the initial state integrated against $\lambda$.

chainMeasure.instIsProbabilityMeasure — Under the same hypotheses ($X$ measurable, $P$ a Markov kernel), with the additional typeclass hypothesis that $\lambda$ is a probability measure, the declaration provides the fact that $\mathrm{chainMeasure}\,P\,\lambda$ (the composition of the trajectory kernel with $\lambda$, as unfolded above) is a probability measure on $\mathbb{N} \to X$.

sampleAvg — For an arbitrary type $X$ (no σ-algebra needed here), an arbitrary function $f : X \to \mathbb{R}$ (no measurability assumed), $n \in \mathbb{N}$, and a sequence $\omega : \mathbb{N} \to X$: $\mathrm{sampleAvg}\,f\,n\,\omega = n^{-1} \sum_{i=0}^{n-1} f(\omega(i+1))$, i.e., $\tfrac{1}{n}\bigl(f(\omega_1) + \dots + f(\omega_n)\bigr)$. Coordinate $\omega_0$ is never used — the average runs over coordinates $1$ through $n$. For $n = 0$ the sum is empty and the real inverse of $0$ is $0$ by convention, so the value is $0$.

SatisfiesCLT — For a measurable type $X$, a kernel $P$ on $X$ assumed (typeclass) to be a Markov kernel, a measure $\pi$ on $X$ (completely arbitrary: not assumed to be a probability measure, finite, or invariant for $P$), and a function $f : X \to \mathbb{R}$ (no measurability or integrability assumed): the proposition that there exists $v \in [0,\infty)$ (a nonnegative real; $v = 0$ is allowed) such that for every measure $\lambda$ on $X$ that is a probability measure, the sequence of functions on path space $Z_n(\omega) = \sqrt{n}\,\bigl(\mathrm{sampleAvg}\,f\,n\,\omega - \int f\,d\pi\bigr)$ — where $\mathrm{sampleAvg}\,f\,n\,\omega = n^{-1}\sum_{i=0}^{n-1} f(\omega(i+1))$ (value $0$ at $n=0$) and $\sqrt{\cdot}$ is the real square root — converges in distribution as $n \to \infty$, each $Z_n$ taken under the single fixed measure $\mathrm{chainMeasure}\,P\,\lambda$ (the path law of the chain with one-step kernel $P$ and initial law $\lambda$, as unfolded above), to the identity map on $\mathbb{R}$ under the real Gaussian measure with mean $0$ and variance $v$ — i.e., the image laws of the $Z_n$ converge weakly to that Gaussian measure ($v = 0$ gives the Dirac mass at $0$). Points to note: the quantifier order makes one single $v$ work uniformly for all initial probability laws $\lambda$; the centering constant is the Bochner integral $\int f\,d\pi$, which equals $0$ by convention when $f$ is not $\pi$-integrable; and since $f$ carries no measurability hypothesis, the $Z_n$ need not be almost-everywhere measurable, in which case their image laws are the zero measure by the pushforward convention.