The Diaconis--Freedman representation with a random initial state

The Diaconis--Freedman representation for a recurrent Markov exchangeable process is first available when its initial state is fixed (TauCeti.Probability.MarkovExchangeable.mixedMarkovChain_of_ae_initial_eq). Conditioning on an initial state of positive probability preserves recurrence and Markov exchangeability and gives that fixed-start hypothesis, so the process is a mixture of Markov chains under each such conditional law. The state space is countable, so these conditional mixtures glue along the partition by the initial state (TauCeti.Probability.mixedMarkovChain_of_forall_cond) into a single mixture of Markov chains under the original law.

Together with the easy direction TauCeti.Probability.MixedMarkovChain.markovExchangeable, this is the theorem of Diaconis and Freedman: a recurrent process is Markov exchangeable if and only if it is a mixture of Markov chains.

Main results

• TauCeti.Probability.MarkovExchangeable.mixedMarkovChain_cond_initial: the conditional representation at a positive-probability initial state.
• TauCeti.Probability.MarkovExchangeable.mixedMarkovChain: the Diaconis--Freedman representation theorem, a recurrent Markov exchangeable process is a mixture of Markov chains.
• TauCeti.Probability.markovExchangeable_iff_mixedMarkovChain: for a recurrent process, Markov exchangeability and being a mixture of Markov chains are equivalent.

References

• P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115--130.

theorem TauCeti.Probability.MarkovExchangeable.mixedMarkovChain_cond_initial {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {a : α} [MeasureTheory.IsFiniteMeasure μ] (h : MarkovExchangeable μ X) (hrec : Recurrent μ X) (ha : μ {ω : Ω | X 0 ω = a} ≠ 0) : MixedMarkovChain μ[|{ω : Ω | X 0 ω = a}] X

The conditional Diaconis--Freedman representation at an initial state. Each positive-probability initial state of a recurrent Markov exchangeable process yields a mixture of Markov chains under the conditional law.

theorem TauCeti.Probability.MarkovExchangeable.mixedMarkovChain {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (h : MarkovExchangeable μ X) (hrec : Recurrent μ X) : MixedMarkovChain μ X

The Diaconis--Freedman representation theorem. A recurrent Markov exchangeable process is a mixture of Markov chains. The initial state may be random: the representations conditional on the individual initial states are glued into a single pair of mixing witnesses. The measure is finite and nonzero, as in the gluing theorem TauCeti.Probability.mixedMarkovChain_of_forall_cond.

theorem TauCeti.Probability.markovExchangeable_iff_mixedMarkovChain {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (hrec : Recurrent μ X) : MarkovExchangeable μ X ↔ MixedMarkovChain μ X

The Diaconis--Freedman theorem. A recurrent process is Markov exchangeable if and only if it is a mixture of Markov chains.