Given the past, the chain from time $k+n$ on is started from $P^n(u_k,\cdot)$

Let $P$ be a Markov kernel and let $\mathrm{traj}_k$ be the kernel giving the law of the trajectory continuing from an initial segment $u = (u_0,\dots,u_k)$. Then for every $n$,

where $\sigma^{k+n}\omega = (\omega_{k+n+l})_l$.

What it says. Conditionally on the first $k+1$ states of the chain, the process observed from time $k+n$ onwards is a chain started from $P^n(u_k,\cdot)$ — and it depends on the conditioning only through $u_k$. This single statement packages both halves of the Markov property that a mixing estimate needs: forgetting (the past enters only via its last state) and restarting after $n$ steps (the distribution of that state is $P^n$).

Why it is the last probabilistic step. In the definition of the mixing coefficients $\alpha(n)$, $\rho(n)$, $\phi(n)$ one fixes a split point $k$, a past event in $\sigma(X_0,\dots,X_k)$ and a future event in $\sigma(X_{k+n},X_{k+n+1},\dots)$. Under the identification of the future $\sigma$-algebra as a single pullback along $\sigma^{k+n}$, the conditional probability of the future event given the past is precisely the left-hand side evaluated at a fixed measurable set. This theorem computes it: it equals $\int \mathbb{P}_y(B_0)\,P^n(u_k,\mathrm{d}y)$. Comparing with the stationary value $\int \mathbb{P}_y(B_0)\,\pi(\mathrm{d}y)$ and applying the total-variation bound for $[0,1]$-valued integrands turns any rate $\|P^n(x,\cdot)-\pi\| \le C$ into the bound $\phi(n) \le C$, uniformly in the split point $k$. After this, no probabilistic input remains — only the arithmetic of averages.

Proof. Factor $\sigma^{k+n}$ as $\sigma^{n}\circ\sigma^{k}$, which requires the associativity $k+n+l = k+(n+l)$. The inner shift is handled by the strong restart property, $\sigma^k_*[\mathrm{traj}_k(u)] = \mathbb{P}_{u_k}$; the outer one by the unconditional $n$-step restart, $\sigma^n_*\mathbb{P}_x = \int \mathbb{P}_y P^n(x,\mathrm{d}y)$, after commuting $n+l$ into $l+n$ to match its indexing convention. Composing the two pushforwards with Measure.map_map gives the claim.