Reconstructing a recurrent path from its excursions

A recurrent process that starts at a₀ returns to it infinitely often, so concatenating its excursions recovers the path: pathOfExcursions_excursion is the identity used here, and it needs exactly that recurrence. This file turns it into an identity of laws,

pathLaw μ X = (pathLaw of the excursion process).map (pathOfExcursions a₀)

and nothing more.

Only that direction is established. Concatenation is not injective on arbitrary excursion sequences — a word containing a₀ is split further when the excursions are read back — so the converse excursion_pathOfExcursions carries the hypothesis that the words avoid a₀, and is not used here. What the identity above needs is a pushforward along a measurable map that is a.e. left inverse to reading the excursions off, not a bijection.

This change of variables does not require any symmetry or mixture representation of the process. The specialization to a recurrent process is in TauCeti.Probability.Recurrent.Excursion.

Main results

• TauCeti.Probability.measurable_pathOfExcursions — concatenation is measurable;
• TauCeti.Probability.pathLaw_eq_map_pathOfExcursions — the path law is the pushforward of the excursion path law along concatenation.

References

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

theorem TauCeti.Probability.measurable_loopPathAt_ofFn {α : Type u_2} [MeasurableSpace α] (a₀ : α) (n i : ℕ) : Measurable fun (v : Fin n → List α) => loopPathAt a₀ (List.ofFn v) i

Finite concatenations of excursions are measurable coordinatewise. For every fixed coordinate i, the map sending n list-valued inputs to the i-th point of the path obtained by concatenating them from a₀ is measurable, with no discreteness assumption on α.

theorem TauCeti.Probability.measurable_pathOfExcursions {α : Type u_2} [MeasurableSpace α] (a₀ : α) : Measurable (pathOfExcursions a₀)

Concatenating a sequence of excursions is measurable. Each coordinate of the concatenated sequence depends on finitely many excursions. Their measurable lengths determine which word and coordinate to read, so no discreteness assumption on the state space is needed.

Reconstructing the path law

theorem TauCeti.Probability.pathLaw_eq_map_pathOfExcursions {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {a₀ : α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (ha₀ : MeasurableSet {a₀}) (hreturns : ∀ᵐ (ω : Ω) ∂μ, {n : ℕ | X n ω = a₀}.Infinite) (h0 : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = a₀) : pathLaw μ X = MeasureTheory.Measure.map (pathOfExcursions a₀) (pathLaw μ (excursionProcess X a₀))

The path law of a process returning infinitely often to a₀ is the image of its excursion law. Almost every sample path starts at and returns infinitely often to a₀, so concatenating its excursions recovers it. Only the base state's singleton needs to be measurable.