Excursion processes

The excursions of a process away from a state form a process of finite words. Reading an excursion is measurable when the base state's singleton is measurable; no recurrence or symmetry assumption is needed. When a path starts at the base state and makes the visit closing its prescribed excursions, the excursion-prefix event agrees with a finite-path event.

These change-of-variables facts let excursion laws be studied independently of any symmetry of the original process. Concatenation and reconstruction of the path law are developed in TauCeti.Probability.Process.Excursion.Reconstruction.

References

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

noncomputable def TauCeti.Probability.excursionProcess {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (a₀ : α) : ℕ → Ω → List α

The excursion process of X away from a₀: its k-th value is the finite word the sample path traverses strictly between its k-th and (k + 1)-st visits to a₀.

@[simp]

theorem TauCeti.Probability.excursionProcess_apply {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (a₀ : α) (k : ℕ) (ω : Ω) : excursionProcess X a₀ k ω = excursion (fun (n : ℕ) => X n ω) a₀ k

theorem TauCeti.Probability.measurable_excursion {α : Type u_2} [MeasurableSpace α] (a₀ : α) (k : ℕ) (ha₀ : MeasurableSet {a₀}) : Measurable fun (x : ℕ → α) => excursion x a₀ k

An excursion is a measurable function of the path. The two endpoint visit times are measurable and range over a countable set, and on each of their fibres the excursion reads a fixed finite list of coordinates.

theorem TauCeti.Probability.aemeasurable_excursionProcess {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (a₀ : α) (ha₀ : MeasurableSet {a₀}) (k : ℕ) : AEMeasurable (excursionProcess X a₀ k) μ

Every excursion of a process with a.e. measurable coordinates is a.e. measurable when the base state's singleton is measurable.

theorem TauCeti.Probability.measure_setOf_excursionPrefix_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {a₀ : α} {bs : List (List α)} (hvisit : ∀ᵐ (ω : Ω) ∂μ, ∃ (n : ℕ), X n ω = a₀ ∧ visitCount (fun (n : ℕ) => X n ω) a₀ n = bs.length) (h0 : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = a₀) (havoid : ∀ e ∈ bs, a₀ ∉ e) : μ {ω : Ω | excursionPrefix (fun (n : ℕ) => X n ω) a₀ bs.length = bs} = μ {ω : Ω | ∀ i ≤ loopSteps bs, X i ω = loopPathAt a₀ bs i}

Prescribing the first excursions is a finite-path event. For a process almost surely starting at a₀ and almost surely making a bs.length-th visit to a₀, having bs as its first bs.length excursions is, up to a null set, spelling out the loop word of bs. Only the visit closing the last prescribed excursion is used, so this asks less than returning to a₀ infinitely often, let alone recurrence of the whole process; TauCeti.exists_visitCount_of_infinite supplies the hypothesis from infinitely many returns.