The excursion process of a sequence

Fix a state a of a sequence x : ℕ → α. Its k-th excursion from a is the finite list of values strictly between the k-th and (k + 1)-st visits to a. This file defines that list as TauCeti.excursion x a k and packages the first m excursions as TauCeti.excursionPrefix x a m.

When the m-th visit exists, the visit times through m are genuine and strictly increasing. The main reconstruction theorem then says that spelling out the first m excursions with TauCeti.loopPath recovers exactly the segment of x between its zeroth and m-th visits:

loopPath a (excursionPrefix x a m)
  = (List.Ico (visitTime x a 0) (visitTime x a m + 1)).map x.

In particular this applies whenever x visits a infinitely often, and if x 0 = a, the result is the initial path segment through its m-th return to a. Read as an equivalence (TauCeti.eqOn_loopPathAt_iff_excursionPrefix_eq), this is the combinatorial bridge from the finite excursion-reordering theorem in TauCeti.Probability.Exchangeability.Excursion to the exchangeability of the excursion process of a recurrent Markov exchangeable path, which is proved in TauCeti.Probability.Exchangeability.Recurrence.Excursion: a prescribed list of first excursions is nothing but a prescribed finite path.

Main definitions

• TauCeti.excursion: the finite word strictly between two consecutive visits to a state.
• TauCeti.excursionPrefix: the list of the first m excursions.
• TauCeti.pathOfExcursions: the sequence spelled out by a base state and an infinite sequence of excursions.

Main results

• TauCeti.not_mem_excursion: an excursion does not visit its base state.
• TauCeti.loopPath_excursionPrefix: the first excursions reconstruct the corresponding segment of the original sequence.
• TauCeti.loopSteps_excursionPrefix: the number of reconstructed transitions is the difference of the endpoint visit times.
• TauCeti.visitCount_loopPathAt: a loop visits its base state once per excursion.
• TauCeti.eqOn_loopPathAt_iff_excursionPrefix_eq: for a path whose relevant return exists, having prescribed first excursions is the same as spelling out their loop word.
• TauCeti.pathOfExcursions_excursion: a sequence that starts at a state and returns to it infinitely often is rebuilt from its own excursions.
• TauCeti.excursion_pathOfExcursions: conversely, a sequence spelled out by excursions avoiding the base state has exactly those excursions.

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".

No material is adapted from cameronfreer/exchangeability, which treats exchangeable rather than Markov exchangeable sequences.

Excursions and finite prefixes

noncomputable def TauCeti.excursion {α : Type u_1} (x : ℕ → α) (a : α) (k : ℕ) : List α

The k-th excursion of x from a: the finite list of values at the times strictly between the k-th and (k + 1)-st visits to a.

If either visit does not exist, visitTime uses its documented junk value and this interval may be empty.

Equations

• TauCeti.excursion x a k = List.map x (List.Ico (TauCeti.visitTime x a k + 1) (TauCeti.visitTime x a (k + 1)))

theorem TauCeti.excursion_def {α : Type u_1} (x : ℕ → α) (a : α) (k : ℕ) : excursion x a k = List.map x (List.Ico (visitTime x a k + 1) (visitTime x a (k + 1)))

The defining equation of an excursion.

noncomputable def TauCeti.excursionPrefix {α : Type u_1} (x : ℕ → α) (a : α) (m : ℕ) : List (List α)

The list of the first m excursions of x from a.

Equations

• TauCeti.excursionPrefix x a m = List.map (TauCeti.excursion x a) (List.range m)

theorem TauCeti.excursionPrefix_def {α : Type u_1} (x : ℕ → α) (a : α) (m : ℕ) : excursionPrefix x a m = List.map (excursion x a) (List.range m)

The defining equation of a finite excursion prefix.

@[simp]

theorem TauCeti.excursionPrefix_zero {α : Type u_1} (x : ℕ → α) (a : α) : excursionPrefix x a 0 = []

@[simp]

theorem TauCeti.excursionPrefix_succ {α : Type u_1} (x : ℕ → α) (a : α) (m : ℕ) : excursionPrefix x a (m + 1) = excursionPrefix x a m ++ [excursion x a m]

@[simp]

theorem TauCeti.length_excursionPrefix {α : Type u_1} (x : ℕ → α) (a : α) (m : ℕ) : (excursionPrefix x a m).length = m

theorem TauCeti.mem_excursion_iff {α : Type u_1} {x : ℕ → α} {a : α} {k : ℕ} {b : α} : b ∈ excursion x a k ↔ ∃ (n : ℕ), visitTime x a k < n ∧ n < visitTime x a (k + 1) ∧ x n = b

Membership in an excursion is membership in the corresponding open interval of times.

Deliberately not @[simp]: it would rewrite the left-hand side of the @[simp] lemma TauCeti.not_mem_excursion into an existential that simp cannot close, so simp would stop proving that an excursion avoids its base state.

@[simp]

theorem TauCeti.getElem_excursionPrefix {α : Type u_1} {x : ℕ → α} {a : α} {k m : ℕ} (hk : k < m) : (excursionPrefix x a m)[k] = excursion x a k

The k-th entry of a finite excursion prefix is the k-th excursion.

Elementary properties

@[simp]

theorem TauCeti.length_excursion {α : Type u_1} (x : ℕ → α) (a : α) (k : ℕ) : (excursion x a k).length = visitTime x a (k + 1) - visitTime x a k - 1

The length of an excursion is the gap between its endpoint visit times, less one.

@[simp]

theorem TauCeti.not_mem_excursion {α : Type u_1} (x : ℕ → α) (a : α) (k : ℕ) : a ∉ excursion x a k

An excursion never contains its base state. This remains true in the finite-visit case, where visitTime may make the interval empty.

theorem TauCeti.forall_not_mem_excursionPrefix {α : Type u_1} (x : ℕ → α) (a : α) (m : ℕ) (e : List α) : e ∈ excursionPrefix x a m → a ∉ e

No excursion of a finite excursion prefix visits the base state, so such a prefix is a legitimate argument for TauCeti.loopPath_injOn.

theorem TauCeti.visitCount_loopPathAt {α : Type u_1} (a : α) {bs : List (List α)} (havoid : ∀ e ∈ bs, a ∉ e) : visitCount (loopPathAt a bs) a (loopSteps bs) = bs.length

A loop visits its base state once per excursion. Counting the visits a loop makes to its base letter over its whole span counts its excursions, because an excursion never returns there.

Reconstruction

theorem TauCeti.loopPath_singleton_excursion {α : Type u_1} {x : ℕ → α} {a : α} {k : ℕ} (h : ∃ (n : ℕ), x n = a ∧ visitCount x a n = k + 1) : loopPath a [excursion x a k] = List.map x (List.Ico (visitTime x a k) (visitTime x a (k + 1) + 1))

A single excursion whose next endpoint exists spells out exactly the segment between its two endpoint visits.

theorem TauCeti.loopPath_singleton_excursion_of_infinite {α : Type u_1} {x : ℕ → α} {a : α} (h : {n : ℕ | x n = a}.Infinite) (k : ℕ) : loopPath a [excursion x a k] = List.map x (List.Ico (visitTime x a k) (visitTime x a (k + 1) + 1))

The infinite-visit form of loopPath_singleton_excursion.

theorem TauCeti.loopPath_excursionPrefix {α : Type u_1} {x : ℕ → α} {a : α} {m : ℕ} (h : ∃ (n : ℕ), x n = a ∧ visitCount x a n = m) : loopPath a (excursionPrefix x a m) = List.map x (List.Ico (visitTime x a 0) (visitTime x a m + 1))

If the m-th visit exists, the loop path of the first m excursions is the original sequence segment from the zeroth through the m-th visit to the base state.

theorem TauCeti.loopPath_excursionPrefix_of_infinite {α : Type u_1} {x : ℕ → α} {a : α} (h : {n : ℕ | x n = a}.Infinite) (m : ℕ) : loopPath a (excursionPrefix x a m) = List.map x (List.Ico (visitTime x a 0) (visitTime x a m + 1))

The infinite-visit form of loopPath_excursionPrefix.

theorem TauCeti.loopSteps_excursionPrefix {α : Type u_1} {x : ℕ → α} {a : α} {m : ℕ} (h : ∃ (n : ℕ), x n = a ∧ visitCount x a n = m) : loopSteps (excursionPrefix x a m) = visitTime x a m - visitTime x a 0

If the m-th visit exists, the first m excursions contain exactly the transitions between the zeroth and m-th visits to the base state.

theorem TauCeti.loopSteps_excursionPrefix_of_infinite {α : Type u_1} {x : ℕ → α} {a : α} (h : {n : ℕ | x n = a}.Infinite) (m : ℕ) : loopSteps (excursionPrefix x a m) = visitTime x a m - visitTime x a 0

The infinite-visit form of loopSteps_excursionPrefix.

theorem TauCeti.loopPath_excursionPrefix_of_zero {α : Type u_1} {x : ℕ → α} {a : α} {m : ℕ} (h : ∃ (n : ℕ), x n = a ∧ visitCount x a n = m) (h0 : x 0 = a) : loopPath a (excursionPrefix x a m) = List.map x (List.range (visitTime x a m + 1))

If the m-th visit exists for a sequence starting at a, its first m excursions reconstruct the initial segment through the m-th return.

theorem TauCeti.loopPath_excursionPrefix_of_infinite_of_zero {α : Type u_1} {x : ℕ → α} {a : α} (h : {n : ℕ | x n = a}.Infinite) (h0 : x 0 = a) (m : ℕ) : loopPath a (excursionPrefix x a m) = List.map x (List.range (visitTime x a m + 1))

The infinite-visit form of loopPath_excursionPrefix_of_zero.

theorem TauCeti.loopSteps_excursionPrefix_of_zero {α : Type u_1} {x : ℕ → α} {a : α} {m : ℕ} (h : ∃ (n : ℕ), x n = a ∧ visitCount x a n = m) (h0 : x 0 = a) : loopSteps (excursionPrefix x a m) = visitTime x a m

If the m-th visit exists for a sequence starting at a, its first m excursions have total duration equal to the m-th return time.

theorem TauCeti.loopSteps_excursionPrefix_of_infinite_of_zero {α : Type u_1} {x : ℕ → α} {a : α} (h : {n : ℕ | x n = a}.Infinite) (h0 : x 0 = a) (m : ℕ) : loopSteps (excursionPrefix x a m) = visitTime x a m

The infinite-visit form of loopSteps_excursionPrefix_of_zero.

Excursion prefixes as finite-path events

theorem TauCeti.eqOn_loopPathAt_iff_excursionPrefix_eq {α : Type u_1} {x : ℕ → α} {a : α} {bs : List (List α)} (havoid : ∀ e ∈ bs, a ∉ e) (h : ∃ (n : ℕ), x n = a ∧ visitCount x a n = bs.length) (h0 : x 0 = a) : (∀ i ≤ loopSteps bs, x i = loopPathAt a bs i) ↔ excursionPrefix x a bs.length = bs

A returning path has prescribed first excursions exactly when it spells out their loop. For a sequence starting at a whose bs.length-th return to a exists, and a list bs of excursions avoiding a, the following are the same condition:

• over the span loopSteps bs of the loop, the sequence agrees with the loop word of bs;
• the first bs.length excursions of the sequence are bs.

This is what turns a finite-dimensional event of the excursion process into a finite-path event of the sequence itself, which is the form Markov exchangeability constrains.

The sequence spelled out by an infinite sequence of excursions

def TauCeti.pathOfExcursions {α : Type u_1} (a : α) (b : ℕ → List α) (i : ℕ) : α

The sequence spelled out by a base state a and an infinite sequence b of excursions:

a, b 0, a, b 1, a, …

Index i is read off the loop word of the first i + 1 excursions, which already runs for at least i + 1 steps, so the reading never falls off its end.

Equations

• TauCeti.pathOfExcursions a b i = TauCeti.loopPathAt a (List.map b (List.range (i + 1))) i

theorem TauCeti.pathOfExcursions_eq_loopPathAt {α : Type u_1} (a : α) (b : ℕ → List α) {i n : ℕ} (hi : i ≤ loopSteps (List.map b (List.range n))) : pathOfExcursions a b i = loopPathAt a (List.map b (List.range n)) i

A sequence spelled out by excursions is read off any long enough loop word. The definition uses the shortest such word; this is the form the reconstruction theorems below need.

@[simp]

theorem TauCeti.pathOfExcursions_zero {α : Type u_1} (a : α) (b : ℕ → List α) : pathOfExcursions a b 0 = a

theorem TauCeti.loopSteps_map_range_succ {α : Type u_1} (b : ℕ → List α) (n : ℕ) : loopSteps (List.map b (List.range (n + 1))) = loopSteps (List.map b (List.range n)) + ((b n).length + 1)

Appending one more excursion lengthens the loop by that excursion and the step back to the base state.

@[simp]

theorem TauCeti.pathOfExcursions_loopSteps {α : Type u_1} (a : α) (b : ℕ → List α) (n : ℕ) : pathOfExcursions a b (loopSteps (List.map b (List.range n))) = a

A sequence spelled out by excursions is back at its base state at the end of every excursion.

theorem TauCeti.infinite_setOf_pathOfExcursions_eq {α : Type u_1} (a : α) (b : ℕ → List α) : {n : ℕ | pathOfExcursions a b n = a}.Infinite

A sequence spelled out by excursions returns to its base state infinitely often, whatever the excursions are.

The two reconstructions

theorem TauCeti.pathOfExcursions_excursion {α : Type u_1} {x : ℕ → α} {a : α} (h : {n : ℕ | x n = a}.Infinite) (h0 : x 0 = a) : pathOfExcursions a (excursion x a) = x

Excursions rebuild the sequence they came from. A sequence that starts at a and returns to it infinitely often is spelled out by its own excursions.

@[simp]

theorem TauCeti.excursionPrefix_pathOfExcursions {α : Type u_1} {a : α} {b : ℕ → List α} (n : ℕ) (havoid : ∀ j < n, a ∉ b j) : excursionPrefix (pathOfExcursions a b) a n = List.map b (List.range n)

A sequence spelled out by excursions has the prescribed excursion prefix, provided the excursions in that prefix avoid the base state.

@[simp]

theorem TauCeti.excursion_pathOfExcursions {α : Type u_1} {a : α} {b : ℕ → List α} (j : ℕ) (havoid : ∀ k ≤ j, a ∉ b k) : excursion (pathOfExcursions a b) a j = b j

Each excursion of a sequence spelled out by excursions is the corresponding one, provided that excursion and its predecessors avoid the base state.