Exchangeable and contractable processes are recurrent #
A contractable process has a shift-invariant path law, so on a countable state space the
Poincaré recurrence theorem of TauCeti.Probability.Recurrent applies to it. Exchangeable
processes are contractable, so they are recurrent too.
Main results #
TauCeti.Probability.Contractable.recurrentandTauCeti.Probability.Exchangeable.recurrent— contractable and exchangeable processes on a countable state space are recurrent.
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".
theorem
TauCeti.Probability.Contractable.recurrent
{Ω : Type u_1}
{α : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace α]
[Countable α]
[MeasurableSingletonClass α]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{X : ℕ → Ω → α}
(hX : Contractable μ X)
(hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ)
:
Recurrent μ X
A contractable process on a countable state space is recurrent.
theorem
TauCeti.Probability.Exchangeable.recurrent
{Ω : Type u_1}
{α : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace α]
[Countable α]
[MeasurableSingletonClass α]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{X : ℕ → Ω → α}
(hX : Exchangeable μ X)
(hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ)
:
Recurrent μ X
An exchangeable process on a countable state space is recurrent. Together with
Exchangeable.markovExchangeable this says that the Diaconis–Freedman hypotheses hold for every
exchangeable process on a countable state space.