Excursion reconstruction for recurrent processes #
A recurrent process started at a₀ returns to that state infinitely often almost surely.
Its path law is therefore the image of its excursion law under concatenation. This
specializes the general reconstruction theorem without imposing any distributional symmetry.
References #
- P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115–130.
theorem
TauCeti.Probability.Recurrent.pathLaw_eq_map_pathOfExcursions
{Ω : Type u_1}
{α : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace α]
{μ : MeasureTheory.Measure Ω}
{X : ℕ → Ω → α}
{a₀ : α}
(hrec : Recurrent μ X)
(hX : ∀ (i : ℕ), AEMeasurable (X i) μ)
(ha₀ : MeasurableSet {a₀})
(h0 : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = a₀)
:
The path law of a recurrent process started at a₀ is the image of its excursion law.
Only the base state's singleton needs to be measurable.