I am working on understanding a theorem related to the coupling-from-the-past protocol in Markov chain theory. The theorem is as follows:
Theorem 1: With probability 1 the coupling-from-the-past protocol returns a value, and this value is distributed according to the stationary distribution of the Markov chain.
Proof: Since the chain is ergodic, there is an $L$ such that for all states $i$ and $j$, there is a positive chance of going from $i$ to $j$ in $L$ steps. Hence for each $t$, $F_{t-L}^{t}(\cdot)$ has a positive chance of being constant, and since these events are independent, it will happen with probability $1$ that one of these maps is constant, in which case $F_{-M}^{0}$ is constant for all sufficiently large M. When the algorithm reaches back $M$ steps into the past, it will terminate and return a value that we will call $\overline{F}_{- \infty }^{0}$. Note that $\overline{F}_{- \infty }^{0}$ is obtained from $\overline{F}_{-\infty}^{1}$ by running the Markov chain one step, and that $\overline{F}_{-\infty}^{0}$ and $\overline{F}_{-\infty}^{1}$ have the same probability distribution. Together these last two assertions imply that the output $\overline{F}_{-\infty}^{0}$ is distributed according to the unique stationary distribution $\pi$.
Before diving into the proof I'd like to note that we can view Markov chains from the point of view of random functions. That is instead of considering a sequence of random variable $X_{n}$ we can also think of functions on the state space. F.e. consider a Markov chain with state space $S=\{1, 2\}$ and transition matrix $P=\left(\begin{array}[cc].1 & .9 \\ .4 & .6 \end{array} \right)$. Then in the random function view we would consider the set $\mathcal{F}:=\{f: f:S \mapsto S\}$ with cardinality $|\mathcal{F}|=|S|^{|S|}=4$ and assume that at each step one of these functions is drawn such that $x_{t+1}=f_{t}(x_{t})$. Furthermore the transition over multiple steps is given by the composition $X_{t+1}=f_{t}(x_{t})=(f_{t}\circ f_{0})(x_{0})=F_{0}^{t}(x_{0})$.
I've attempted to break down the proof as follows:
Since the chain is ergodic, there is an $L$ such that for all states $i$ and $j$, there is a positive chance of going from $i$ to $j$ in $L$ steps.
This is simply by definition of an ergodic Markov chain.
Hence for each $t$, $F_{i-L}^{t}(\cdot)$ has a positive chance of being constant
This follows after observing that if all values of a columns of the transition matrix $P^{L}$ are $>0$ then the constant function has a positive probability.
and since these events are independent,
Independent by construction.
it will happen with probability $1$ that one of these maps is constant,
Lemma of Borel-Cantelli.
in which case $F_{-M}^{0}$ is constant for all sufficiently large M.
Simply choose $M$ larger enought.
When the algorithm reaches back $M$ steps into the past, it will terminate and return a value that we will call $\overline{F}_{-\infty}^{0}$.
It holds that $F_{-t_{2}}^{0}=F_{-t_{1}}^{0}\circ F_{-t_{2}}^{-t_{1}-1}$ for $0< t_{1}<t_{2}$. Since $F_{-M}^{0}$ is a constant it holds that $F_{-N}^{0}=F_{-M}^{0}\circ F_{-N}^{-M-1}$ for all $N>M$.
Note that $\overline{F}_{-\infty}^{0}$ obtained from $\overline{F}_{-\infty}^{1}$ by running the Markov chain one step, and that $\overline{F}_{-\infty}^{0}$ and $\overline{F}_{-\infty}^{1}$ have the same probability distribution.
Since the chain has run for long enough to be in the stationary distribution $\overline{F}_{-\infty}^{1}$ returns a value from the stationary distribution.
Together these last two assertions imply that the output $\overline{F}_{-\infty}^{0}$ is distributed according to the unique stationary distribution $\pi$.
Is my understanding of the proof correct?