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 an argument that permutes the entries within a row does need them to be real transitions rather than junk.

The same recurrence makes row permutations that move finitely many cells on attained rows eventually last-exit admissible (Recurrent.ae_eventually_lastExitAdmissible), the hypothesis under which TauCeti.Combinatorics.Enumerative.LastExit rebuilds a finite prefix from reindexed successor rows with the same endpoint and transition counts.

Main results

• TauCeti.Probability.Recurrent.ae_apply_visitTime and TauCeti.Probability.Recurrent.ae_strictMono_visitTime — the visit times of a visited state are genuine, strictly increasing visits;
• TauCeti.Probability.Recurrent.ae_visitCount_visitTime and TauCeti.Probability.Recurrent.ae_tendsto_visitCount_atTop — the visit counts along them run through every natural number, so every visited row is infinite;
• TauCeti.Probability.Recurrent.ae_eventually_lastExitAdmissible — a family of row permutations moving almost surely finitely many cells on attained rows is almost surely last-exit admissible for every long enough prefix.

References

• P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115–130.
• S. Fortini, L. Ladelli, G. Petris, and E. Regazzini, "On mixtures of distributions of Markov chains", Stochastic Processes and their Applications 100 (2002), 147–165, Lemma 1(b).

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.

theorem TauCeti.Probability.Recurrent.ae_eventually_lastExitAdmissible {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Recurrent μ X) (π : α → Equiv.Perm ℕ) (hπ : ∀ᵐ (ω : Ω) ∂μ, {p : α × ℕ | (π p.1) p.2 ≠ p.2 ∧ ∃ (t : ℕ), X t ω = p.1}.Finite) : ∀ᵐ (ω : Ω) ∂μ, ∀ᶠ (m : ℕ) in Filter.atTop, LastExitAdmissible π (fun (n : ℕ) => X n ω) m

A family of successor-row permutations moving almost surely finitely many cells on attained rows is almost surely eventually last-exit admissible for a recurrent process. This is the almost-sure form of TauCeti.eventually_lastExitAdmissible_of_recurrent; only the cells on rows the sampled path attains need be finitely many, so a finitely supported π is a special case.