Recurrence and successor arrays

For a recurrent path, the visit times of a visited state are genuine, strictly increasing visits, and the visit counts along them run through every natural number; so the successor-array row of such a state is an infinite list of genuine transitions, read off at those times. Rows indexed by unvisited states remain unconstrained and may contain Nat.nth's junk values.

Combined with successorArray_def, which reads a row entry off the visit time, these are the facts that make every entry of a visited-state row a genuine transition of the path. Recovering the path from its successor array needs none of this — pathOfSuccessors_successorArray inverts the decomposition of an arbitrary sequence — but the later probabilistic argument, which permutes the entries within a row, does need them to be real transitions rather than junk.

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.Recurrent.ae_apply_visitTime {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Recurrent μ X) : ∀ᵐ (ω : Ω) ∂μ, ∀ (k j : ℕ), X (visitTime (fun (n : ℕ) => X n ω) (X k ω) j) ω = X k ω

The visit times of a visited state are genuine visits. Off a recurrent path the later entries of visitTime are Nat.nth's junk value; on one they are the times at which the process really is at that state.

theorem TauCeti.Probability.Recurrent.ae_strictMono_visitTime {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Recurrent μ X) : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), StrictMono (visitTime (fun (n : ℕ) => X n ω) (X k ω))

The visit times of a visited state of a recurrent process are strictly increasing, so the successor-array row of that state is read off at distinct times, in order.

theorem TauCeti.Probability.Recurrent.ae_visitCount_visitTime {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Recurrent μ X) : ∀ᵐ (ω : Ω) ∂μ, ∀ (k j : ℕ), visitCount (fun (n : ℕ) => X n ω) (X k ω) (visitTime (fun (n : ℕ) => X n ω) (X k ω) j) = j

The j-th visit of a recurrent process to one of its states really is preceded by exactly j earlier visits.

theorem TauCeti.Probability.Recurrent.ae_tendsto_visitCount_atTop {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Recurrent μ X) : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Filter.Tendsto (visitCount (fun (n : ℕ) => X n ω) (X k ω)) Filter.atTop Filter.atTop

Each visited row of the successor array is infinite. A recurrent process accumulates unboundedly many visits to every state it attains.