The visited successor array of a recurrent Markov exchangeable process is row exchangeable #
Diaconis and Freedman represent a recurrent Markov exchangeable process as a mixture of Markov
chains by passing to its successor array, whose (a, k)-entry is the state reached right after
the k-th visit to a. TauCeti/Probability/Exchangeability/DiaconisFreedman.lean supplies the
change of variables that turns a row exchangeable array recording those successors back into a
mixture of Markov chains. This file supplies the missing hypothesis of that change of variables:
for a recurrent Markov exchangeable process, the visited successor array
TauCeti.Probability.visitedSuccessorProcess, whose rows at unvisited states are constant, is row
exchangeable, and the Diaconis--Freedman representation of such a process started at a fixed state
follows.
The argument #
Permuting the entries of each row and following the reordered rows rebuilds a finite path with the
same initial state and the same transition counts, provided the permutations obey the last-exit
condition — that is what TauCeti.pathOfReindexedSuccessors and the finite reconstruction lemmas
of TauCeti/Combinatorics/Enumerative/LastExit.lean establish. Markov exchangeability equates the
masses of two such words, so a prefix law is invariant under a last-exit-admissible reindexing
(TauCeti.Probability.MarkovExchangeable.measure_setOf_eqOn_pathOfReindexedSuccessors).
Row exchangeability is the limit of that finite statement. Fix a finitely supported family of row permutations and a finite family of cells. Over a horizon at which every relevant row the prefix visits has consumed its relevant cells, a last-exit reindexing is legitimate, and the reconstruction pairs the prefixes realizing the reindexed cell values with those realizing the original ones. Along a recurrent path each relevant row is either never visited or visited infinitely often, so every long enough prefix is such a horizon and reads the visited successor array at those cells correctly; the masses of the prefix events therefore converge to the mass of the array event.
Why the unvisited rows are reset #
TauCeti/Probability/Exchangeability/Recurrence/UnvisitedRow.lean exhibits a recurrent Markov
exchangeable process whose plain successor array is not row exchangeable: an unattained state
has junk visit times, so its whole row is tied to the cell (x 0, 0), and permuting the row of
x 0 breaks the tie. Recurrence constrains only the states a process does attain, so for the plain
array one needs every state to be attained
(TauCeti.Probability.MarkovExchangeable.rowExchangeable_successorProcess). The visited successor
array agrees with the successor array on every visited row, which is all the change of variables
reads, and carries no such tie.
Main results #
TauCeti.Probability.MarkovExchangeable.measure_setOf_eqOn_pathOfReindexedSuccessors— a finite path and its last-exit reconstruction are equally likely.TauCeti.Probability.MarkovExchangeable.rowExchangeable_visitedSuccessorProcess— the visited successor array of a recurrent Markov exchangeable process is row exchangeable.TauCeti.Probability.MarkovExchangeable.rowExchangeable_successorProcess— the plain successor array is row exchangeable when every state is almost surely attained.TauCeti.Probability.MarkovExchangeable.mixedMarkovChain_of_ae_initial_eq— the Diaconis--Freedman representation at a fixed start: a recurrent Markov exchangeable process started at a fixed state is a mixture of Markov chains. Conditioning on the initial state removes the fixed start (TauCeti.Probability.MarkovExchangeable.mixedMarkovChain).
References #
- P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115--130.
- S. Fortini, L. Ladelli, G. Petris, and E. Regazzini, "On mixtures of distributions of Markov chains", Stochastic Processes and their Applications 100 (2002), 147--165, Lemma 1(b).
A finite path and its last-exit reconstruction are equally likely under a Markov exchangeable process. Rebuilding a prefix from row-permuted successor entries preserves the initial state and every transition count, so Markov exchangeability equates the two masses.
This is the probabilistic half of the successor-array argument; the finite reconstruction itself
is TauCeti.pathOfReindexedSuccessors.
The visited successor array of a recurrent Markov exchangeable process is row exchangeable. Its law is unchanged when the entries of each row are permuted, with a permutation chosen separately for each row.
Together with TauCeti.Probability.mixedMarkovChain_of_rowExchangeable this is the
Diaconis--Freedman representation. No state needs to be attained: the rows of the states the
process never visits are constant, so the obstruction exhibited by
TauCeti.Probability.spareStateProcess_not_rowExchangeable_successorProcess for the plain
successor array does not arise.
The successor array of a recurrent Markov exchangeable process that almost surely attains every state is row exchangeable. Almost surely it coincides with the visited successor array.
The hypothesis that every state is almost surely attained is not decorative:
TauCeti.Probability.spareStateProcess_not_rowExchangeable_successorProcess is a recurrent Markov
exchangeable process without it whose successor array is not row exchangeable.
The Diaconis--Freedman representation theorem at a fixed start. A recurrent Markov
exchangeable process that starts almost surely at a fixed state is a mixture of Markov chains.
TauCeti.Probability.MarkovExchangeable.mixedMarkovChain removes the fixed start.