From a row exchangeable successor array back to a mixture of Markov chains

Diaconis and Freedman represent a recurrent Markov exchangeable process as a mixture of Markov chains by passing to its successor array: the array whose (a, k)-entry is the state the process moves to right after its k-th visit to a. Their argument has two halves. One half shows that the successor array of such a process is row exchangeable — its law is unchanged when the entries of each row are permuted, with a permutation chosen separately for each row. The other half is the change of variables that turns a description of the successor array's law back into a description of the path law. This file is the second half.

The input is TauCeti.Probability.RowExchangeable for an array that almost surely records the successors of the process at the cells it consumes — the successor array itself (TauCeti.Probability.successorProcess), or the visited successor array (TauCeti.Probability.visitedSuccessorProcess) whose unvisited rows are constant — and the output is TauCeti.Probability.MixedMarkovChainWith, with the row marginals of the array's directing measure as the random transition matrix. The mechanism is that the finite path event {X i = w i, i ≤ n} is an event of the array: by TauCeti.eqOn_iff_visitCell_of_apply_visitCell_eq_succ it says exactly that the array takes the prescribed values at the n cells the reference path w designates, which are cells the process consumes, and by TauCeti.visitCell_injective those cells are pairwise distinct. Distinct cells of a row exchangeable array are conditionally independent given the directing measure of its columns (TauCeti.Probability.RowExchangeable.measure_setOf_forall_mem_eq_lintegral_prod), each governed by its row's marginal, so the mass of that event is the mixture of a product of transition probabilities — which is the defining identity of a mixture of Markov chains.

The process is assumed to start almost surely at a fixed state a₀, so the initial-law witness is the Dirac measure at a₀. That is the form in which Diaconis and Freedman state their theorem, and it is what the change of variables gives on its own: the array's mixture identity constrains the array law alone, so carrying a genuinely random initial state through it would need the joint law of the initial state and the array, not just the array's law.

This is the last step of the Diaconis–Freedman representation theorem that does not mention recurrence. Its other half, the row exchangeability of the visited successor array of a recurrent Markov exchangeable process, is TauCeti.Probability.MarkovExchangeable.rowExchangeable_visitedSuccessorProcess.

Main results

• TauCeti.Probability.mixedMarkovChainWith_of_rowExchangeable: at a named mixing representative for the columns of a row exchangeable array recording the successors at consumed cells, a process starting almost surely at a₀ is a mixture of Markov chains with the Dirac initial law at a₀ and the array's row marginals as transition matrix.
• TauCeti.Probability.mixedMarkovChain_of_rowExchangeable: the existential form, with de Finetti supplying the witness.

References

• P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115–130.
• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 8, "Markov exchangeability".

No material is adapted from cameronfreer/exchangeability, which treats exchangeable rather than Markov exchangeable sequences.

theorem TauCeti.Probability.mixedMarkovChainWith_of_rowExchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {Y : α × ℕ → Ω → α} {a₀ : α} {lam : Ω → MeasureTheory.ProbabilityMeasure (α → α)} [Countable α] [MeasurableSingletonClass α] [MeasureTheory.IsProbabilityMeasure μ] (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (h0 : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = a₀) (hY : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), Y (visitCell (fun (j : ℕ) => X j ω) n) ω = X (n + 1) ω) (hrow : RowExchangeable μ Y) (hlam : MixedIIDWith μ (arrayColumn Y) lam) : MixedMarkovChainWith μ X (fun (x : Ω) => MeasureTheory.diracProba a₀) fun (ω : Ω) (a : α) => (lam ω).map fun (x : α → α) => x a

The change of variables from a row exchangeable successor array back to the path law. Let Y be an array that almost surely records, at each cell the process consumes, the state the process moves to next — as TauCeti.Probability.successorProcess X and TauCeti.Probability.visitedSuccessorProcess X both do, whatever their entries elsewhere. A process that starts almost surely at a₀ and for which such an array is row exchangeable is a mixture of Markov chains: the Dirac measure at a₀ is its initial-law witness, and the row marginals of the mixing representative of the array's columns form its transition-matrix witness.

theorem TauCeti.Probability.mixedMarkovChain_of_rowExchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {Y : α × ℕ → Ω → α} {a₀ : α} [Countable α] [MeasurableSingletonClass α] [MeasureTheory.IsProbabilityMeasure μ] (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (h0 : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = a₀) (hYm : ∀ (p : α × ℕ), AEMeasurable (Y p) μ) (hY : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), Y (visitCell (fun (j : ℕ) => X j ω) n) ω = X (n + 1) ω) (hrow : RowExchangeable μ Y) : MixedMarkovChain μ X

The change of variables, with de Finetti supplying the mixing representative. A process that starts almost surely at a fixed state, and for which some almost everywhere measurable array recording its successors at the cells it consumes is row exchangeable, is a mixture of Markov chains.