The successor array of a sequence

For a sequence x : ℕ → α, its successor array records, for each value a, the values that follow successive visits to a. Together with x 0, this array determines the original sequence. The reconstruction is total: entries after the last genuine visit use the junk value supplied by Nat.nth, but the round-trip theorem never reads them.

Main definitions

• TauCeti.visitCount: the number of visits to a value before a given index.
• TauCeti.visitTime: the index of a given visit to a value.
• TauCeti.successorArray: the values following successive visits to each value.
• TauCeti.visitedSuccessorArray: the successor array with the rows of unvisited values reset to constants.
• TauCeti.visitCell: the cell of the successor array a sequence uses at a given time.
• TauCeti.pathOfSuccessors: reconstruction from an initial value and successor array.

Main results

• TauCeti.visitCount_monotone: visit counts are monotone in the horizon.
• TauCeti.visitCount_add: a visit count splits at any intermediate index.
• TauCeti.visitTime_eq_of_eqOn: a visit time is read off any sequence agreeing with the original up to that time.
• TauCeti.successorArray_visitCount: the defining step relation of the successor array.
• TauCeti.visitTime_eq_iff: the fibres of the visit times, including the junk-value branch.
• TauCeti.successorArray_eq_successorArray_zero_of_forall_ne: the successor row of a value the sequence never visits is constant, and repeats the cell the starting value indexes.
• TauCeti.apply_visitTime_of_infinite and TauCeti.visitTime_strictMono_of_infinite: visit times are genuine and strictly increasing when the value occurs infinitely often.
• TauCeti.apply_visitTime_of_le and TauCeti.visitTime_lt_visitTime_of_le: the same two facts below a visit that is known to exist.
• TauCeti.visitTime_lt_of_lt_visitCount: a visit indexed below a visit count is realised before the horizon.
• TauCeti.apply_visitTime_of_lt_visitCount: such an index names a genuine visit.
• TauCeti.visitCount_visitTime_of_lt_visitCount: exactly the indexed number of visits precede that visit.
• TauCeti.occCount_succ_add_zero_eq_visitCount_add_last: the arrival/departure balance of a finite prefix.
• TauCeti.successorArray_pathOfSuccessors_of_lt_visitCount: a reconstruction consumes exactly the successor entries it was prescribed.
• TauCeti.eq_pathOfSuccessors: the uniqueness principle for the reconstruction.
• TauCeti.pathOfSuccessors_successorArray: reconstruction inverts the successor decomposition.
• TauCeti.visitCell_injective: distinct times use distinct cells.
• TauCeti.eqOn_iff_successorArray_visitCell: a finite initial segment of a sequence is pinned down by its initial value together with the successor-array entries at the cells that segment designates. This is the finite-horizon form of TauCeti.eq_pathOfSuccessors, and the form a finite-path event needs: the cells are read off a reference sequence, so they do not move with the sequence being described. TauCeti.eqOn_iff_visitCell_of_apply_visitCell_eq_succ is the same criterion for any array agreeing with the successor array at the cells the sequence consumes, such as TauCeti.visitedSuccessorArray.

References

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

noncomputable def TauCeti.visitCount {α : Type u_1} (x : ℕ → α) (a : α) (n : ℕ) : ℕ

The number of times the sequence x visits a strictly before n.

Equations

• TauCeti.visitCount x a n = Function.occCount (fun (i : Fin n) => x ↑i) a

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

The index of the k-th visit of x to a, or the junk value 0 if there is no such visit.

Equations

• TauCeti.visitTime x a k = Nat.nth (fun (i : ℕ) => x i = a) k

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

The value immediately following the k-th visit of x to a. It is junk if that visit does not exist.

Equations

• TauCeti.successorArray x a k = x (TauCeti.visitTime x a k + 1)

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

The successor array with the rows of the values the sequence never visits reset to a constant: the (a, k)-entry is successorArray x a k if x visits a, and a itself otherwise. Unlike TauCeti.successorArray, whose unvisited rows repeat a genuine successor entry, the unvisited rows of this array carry no information about the sequence beyond the fact that it avoids them.

Equations

• TauCeti.visitedSuccessorArray x a k = if ∃ (n : ℕ), x n = a then TauCeti.successorArray x a k else a

noncomputable def TauCeti.pathOfSuccessors {α : Type u_1} (a₀ : α) (s : α → ℕ → α) (n : ℕ) : α

The sequence rebuilt from an initial value and a successor array.

Equations

• TauCeti.pathOfSuccessors a₀ s n = TauCeti.pathOfSuccessorsUpTo✝ a₀ s n n

theorem TauCeti.visitCount_def {α : Type u_1} (x : ℕ → α) (a : α) (n : ℕ) : visitCount x a n = Function.occCount (fun (i : Fin n) => x ↑i) a

The defining equation for visit counts.

theorem TauCeti.visitTime_def {α : Type u_1} (x : ℕ → α) (a : α) (k : ℕ) : visitTime x a k = Nat.nth (fun (i : ℕ) => x i = a) k

The defining equation for visit times.

theorem TauCeti.successorArray_def {α : Type u_1} (x : ℕ → α) (a : α) (k : ℕ) : successorArray x a k = x (visitTime x a k + 1)

The defining equation for an entry of the successor array.

theorem TauCeti.visitedSuccessorArray_def {α : Type u_1} (x : ℕ → α) (a : α) (k : ℕ) : visitedSuccessorArray x a k = if ∃ (n : ℕ), x n = a then successorArray x a k else a

The defining equation for an entry of the visited successor array.

theorem TauCeti.visitCount_eq_count {α : Type u_1} [DecidableEq α] (x : ℕ → α) (a : α) (n : ℕ) : visitCount x a n = Nat.count (fun (i : ℕ) => x i = a) n

Visit counts are Nat.count of the visiting predicate.

@[simp]

theorem TauCeti.visitCount_zero {α : Type u_1} (x : ℕ → α) (a : α) : visitCount x a 0 = 0

theorem TauCeti.visitCount_monotone {α : Type u_1} (x : ℕ → α) (a : α) : Monotone (visitCount x a)

Visit counts are monotone in the horizon.

theorem TauCeti.visitCount_congr {α : Type u_1} {x y : ℕ → α} {a : α} {n : ℕ} (h : ∀ i < n, x i = y i) : visitCount x a n = visitCount y a n

Visit counts before n depend only on sequence values before n.

theorem TauCeti.visitCount_succ {α : Type u_1} [DecidableEq α] (x : ℕ → α) (a : α) (n : ℕ) : visitCount x a (n + 1) = if x n = a then visitCount x a n + 1 else visitCount x a n

Splitting a visit count at the final index.

@[simp]

theorem TauCeti.visitCount_succ_of_eq {α : Type u_1} {x : ℕ → α} {a : α} {n : ℕ} (h : x n = a) : visitCount x a (n + 1) = visitCount x a n + 1

One more visit is counted when the sequence has the specified value.

@[simp]

theorem TauCeti.visitCount_succ_of_ne {α : Type u_1} {x : ℕ → α} {a : α} {n : ℕ} (h : x n ≠ a) : visitCount x a (n + 1) = visitCount x a n

No visit is added when the sequence has a different value.

theorem TauCeti.visitCount_add {α : Type u_1} (x : ℕ → α) (a : α) (m n : ℕ) : visitCount x a (m + n) = visitCount x a m + visitCount (fun (i : ℕ) => x (m + i)) a n

Splitting a visit count at an intermediate index. The visits before m + n are the visits before m together with the visits the sequence shifted by m makes before n.

theorem TauCeti.occCount_succ_add_zero_eq_visitCount_add_last {α : Type u_1} (z : ℕ → α) (b : α) (t : ℕ) : (Function.occCount (fun (i : Fin t) => z (↑i + 1)) b + if z 0 = b then 1 else 0) = visitCount z b t + if z t = b then 1 else 0

The arrival/departure balance of a finite prefix. Reading the first t successors of z as a word, its occurrences of b together with a possible occurrence of b at time 0 match the visits of z to b before t together with a possible visit at time t.

theorem TauCeti.visitCount_eq_zero_of_forall_ne {α : Type u_1} {x : ℕ → α} {a : α} {n : ℕ} (h : ∀ i < n, x i ≠ a) : visitCount x a n = 0

A stretch of a sequence that avoids a contributes nothing to its visit count.

theorem TauCeti.visitCount_pos_iff {α : Type u_1} {x : ℕ → α} {a : α} {n : ℕ} : 0 < visitCount x a n ↔ ∃ i < n, x i = a

A visit count is positive exactly when the sequence visits the value before the horizon.

theorem TauCeti.visitCount_eq_succ_of_forall_ne {α : Type u_1} (x : ℕ → α) {r m : ℕ} (hr : r < m) (hne : ∀ (j : ℕ), r < j → j < m → x j ≠ x r) : visitCount x (x r) m = visitCount x (x r) r + 1

If time r is a visit and the sequence does not return to x r before m, its visit count at m is its visit count at r plus that final visit.

@[simp]

theorem TauCeti.visitTime_visitCount {α : Type u_1} {x : ℕ → α} {a : α} {n : ℕ} (h : x n = a) : visitTime x a (visitCount x a n) = n

A time at which x has value a is the visit indexed by the number of earlier visits.

theorem TauCeti.visitTime_eq_of_eqOn {α : Type u_1} {x y : ℕ → α} {a : α} {k n : ℕ} (hxy : ∀ i ≤ n, x i = y i) (hy : y n = a) (hcount : visitCount y a n = k) : visitTime x a k = n

A visit time is read off any sequence agreeing with the original up to that time. If x and y agree through index n, and n is a visit of y to a preceded by exactly k earlier visits, then n is the k-th visit of x as well.

This is what transfers the visit structure of a reference path to a process known only to spell that path out over a finite horizon.

theorem TauCeti.visitTime_eq_iff {α : Type u_1} {x : ℕ → α} {a : α} {k m : ℕ} : visitTime x a k = m ↔ x m = a ∧ visitCount x a m = k ∨ m = 0 ∧ ∀ (n : ℕ), ¬(x n = a ∧ visitCount x a n = k)

The fibres of visitTime, including the junk-value branch.

theorem TauCeti.apply_visitTime_of_infinite {α : Type u_1} {x : ℕ → α} {a : α} (h : {n : ℕ | x n = a}.Infinite) (k : ℕ) : x (visitTime x a k) = a

If x visits a infinitely often, every visit time is a genuine visit.

theorem TauCeti.visitTime_strictMono_of_infinite {α : Type u_1} {x : ℕ → α} {a : α} (h : {n : ℕ | x n = a}.Infinite) : StrictMono (visitTime x a)

The visit times of an infinitely often visited value are strictly increasing.

@[simp]

theorem TauCeti.visitTime_zero_of_eq {α : Type u_1} {x : ℕ → α} {a : α} (h : x 0 = a) : visitTime x a 0 = 0

If a sequence starts at a, its zeroth visit to a occurs at time zero.

@[simp]

theorem TauCeti.visitTime_eq_zero_of_forall_ne {α : Type u_1} {x : ℕ → α} {a : α} {k : ℕ} (h : ∀ (n : ℕ), x n ≠ a) : visitTime x a k = 0

A value the sequence never takes has junk visit times. Every one of them is Nat.nth's junk value 0, so the whole successor row of such a value is read off at time zero.

@[simp]

theorem TauCeti.successorArray_eq_of_forall_ne {α : Type u_1} {x : ℕ → α} {a : α} {k : ℕ} (h : ∀ (n : ℕ), x n ≠ a) : successorArray x a k = x 1

The successor row of a value the sequence never visits is constant, equal to the sequence's entry at time one.

@[simp]

theorem TauCeti.successorArray_zero_of_eq {α : Type u_1} {x : ℕ → α} {a : α} (h : x 0 = a) : successorArray x a 0 = x 1

The zeroth successor of a value the sequence starts at is its entry at time one.

theorem TauCeti.successorArray_eq_successorArray_zero_of_forall_ne {α : Type u_1} {x : ℕ → α} {a : α} {k : ℕ} (h : ∀ (n : ℕ), x n ≠ a) : successorArray x a k = successorArray x (x 0) 0

An unvisited row of the successor array duplicates the cell (x 0, 0). The row of a value the sequence never takes carries no information of its own: each of its entries repeats the first successor of the value the sequence starts at.

This ties two cells of the successor array of any sequence that leaves a value unvisited, so a reindexing that moves the second of them can break the tie, and with it the array. Whether it does depends on the sequence; TauCeti.Probability.spareStateProcess_not_rowExchangeable_successorProcess exhibits one where it does.

theorem TauCeti.visitCount_lt_card {α : Type u_1} {x : ℕ → α} {a : α} {n : ℕ} (hf : {n : ℕ | x n = a}.Finite) (hn : x n = a) : visitCount x a n < hf.toFinset.card

If x visits a only finitely often, the number of visits before a genuine visit is smaller than the total number of visits.

theorem TauCeti.visitTime_lt_of_lt_visitCount {α : Type u_1} {x : ℕ → α} {a : α} {k n : ℕ} (h : k < visitCount x a n) : visitTime x a k < n

A visit index below the visit count at time n is realised strictly before n.

theorem TauCeti.apply_visitTime_of_lt_visitCount {α : Type u_1} {x : ℕ → α} {a : α} {k n : ℕ} (h : k < visitCount x a n) : x (visitTime x a k) = a

A visit index below the visit count at time n names a genuine visit.

theorem TauCeti.visitCount_visitTime_of_lt_visitCount {α : Type u_1} {x : ℕ → α} {a : α} {k n : ℕ} (h : k < visitCount x a n) : visitCount x a (visitTime x a k) = k

Before a realised visit indexed by k, there are exactly k earlier visits.

theorem TauCeti.successorArray_congr {α : Type u_1} {x y : ℕ → α} {a : α} {k m : ℕ} (hxy : ∀ i ≤ m, x i = y i) (hk : k < visitCount x a m) : successorArray x a k = successorArray y a k

A consumed successor entry is read off any sequence agreeing with the original over the horizon that consumes it. Below the visit count at time m, the entry successorArray x a k is realised at a visit before m, so it only sees the values of x up to m.

theorem TauCeti.exists_visitCount_of_le {α : Type u_1} {x : ℕ → α} {a : α} {k m : ℕ} (h : ∃ (n : ℕ), x n = a ∧ visitCount x a n = m) (hk : k ≤ m) : ∃ (n : ℕ), x n = a ∧ visitCount x a n = k

If some time is the m-th visit of x to a, then every earlier visit is realised too: for k ≤ m some time is the k-th visit.

theorem TauCeti.apply_visitTime_of_le {α : Type u_1} {x : ℕ → α} {a : α} {k m : ℕ} (h : ∃ (n : ℕ), x n = a ∧ visitCount x a n = m) (hk : k ≤ m) : x (visitTime x a k) = a

If some time is the m-th visit of x to a, then the k-th visit time is a genuine visit for every k ≤ m.

theorem TauCeti.visitTime_lt_visitTime_of_le {α : Type u_1} {x : ℕ → α} {a : α} {j k m : ℕ} (h : ∃ (n : ℕ), x n = a ∧ visitCount x a n = m) (hkj : k < j) (hj : j ≤ m) : visitTime x a k < visitTime x a j

If some time is the m-th visit of x to a, the visit times up to m are strictly increasing.

theorem TauCeti.exists_visitCount_of_infinite {α : Type u_1} {x : ℕ → α} {a : α} (h : {n : ℕ | x n = a}.Infinite) (m : ℕ) : ∃ (n : ℕ), x n = a ∧ visitCount x a n = m

If x visits a infinitely often, every visit count is realised.

@[simp]

theorem TauCeti.successorArray_visitCount_of_eq {α : Type u_1} {x : ℕ → α} {a : α} {n : ℕ} (h : x n = a) : successorArray x a (visitCount x a n) = x (n + 1)

At a visit to a, the sequence moves to the corresponding entry of its successor array.

theorem TauCeti.successorArray_visitCount {α : Type u_1} (x : ℕ → α) (n : ℕ) : successorArray x (x n) (visitCount x (x n) n) = x (n + 1)

The step relation of the successor array.

@[simp]

theorem TauCeti.pathOfSuccessors_zero {α : Type u_1} (a₀ : α) (s : α → ℕ → α) : pathOfSuccessors a₀ s 0 = a₀

The rebuilt sequence starts at the given initial value.

@[simp]

theorem TauCeti.pathOfSuccessors_succ {α : Type u_1} (a₀ : α) (s : α → ℕ → α) (n : ℕ) : pathOfSuccessors a₀ s (n + 1) = s (pathOfSuccessors a₀ s n) (visitCount (pathOfSuccessors a₀ s) (pathOfSuccessors a₀ s n) n)

The recursion equation for the rebuilt sequence.

theorem TauCeti.eq_pathOfSuccessors {α : Type u_1} {y : ℕ → α} {a₀ : α} {s : α → ℕ → α} (h₀ : y 0 = a₀) (hstep : ∀ (n : ℕ), y (n + 1) = s (y n) (visitCount y (y n) n)) : y = pathOfSuccessors a₀ s

A sequence satisfying the reconstruction equations is the rebuilt sequence.

theorem TauCeti.successorArray_pathOfSuccessors_of_lt_visitCount {α : Type u_1} {a a₀ : α} {s : α → ℕ → α} {n k : ℕ} (hk : k < visitCount (pathOfSuccessors a₀ s) a n) : successorArray (pathOfSuccessors a₀ s) a k = s a k

Every entry a rebuilt sequence has already consumed is the prescribed one. Below the visit count of a at any horizon, the successor array of the reconstruction agrees with the successor array it was built from, even though the two may differ on unused entries.

@[simp]

theorem TauCeti.pathOfSuccessors_successorArray {α : Type u_1} (x : ℕ → α) : pathOfSuccessors (x 0) (successorArray x) = x

Rebuilding from a sequence's initial value and successor array recovers the sequence.

noncomputable def TauCeti.visitCell {α : Type u_1} (x : ℕ → α) (n : ℕ) : α × ℕ

The cell of the successor array that x uses at time n: the value it takes there, paired with the number of earlier visits to that value.

Equations

• TauCeti.visitCell x n = (x n, TauCeti.visitCount x (x n) n)

@[simp]

theorem TauCeti.visitCell_def {α : Type u_1} (x : ℕ → α) (n : ℕ) : visitCell x n = (x n, visitCount x (x n) n)

theorem TauCeti.visitCell_injective {α : Type u_1} (x : ℕ → α) : Function.Injective (visitCell x)

Distinct times use distinct cells. Two times carrying the same value are separated by that value's visit counts, which strictly increase across the earlier of the two.

theorem TauCeti.successorArray_visitCell_eq_of_eqOn {α : Type u_1} {w x : ℕ → α} {i n : ℕ} (h : ∀ i ≤ n, x i = w i) (hi : i < n) : successorArray x (visitCell w i).1 (visitCell w i).2 = w (i + 1)

Along a sequence agreeing with w up to n, the successor-array entries at the cells w designates are the successors w prescribes.

theorem TauCeti.eqOn_of_successorArray_visitCell_eq {α : Type u_1} {w x : ℕ → α} {n : ℕ} (h₀ : x 0 = w 0) (h : ∀ i < n, successorArray x (visitCell w i).1 (visitCell w i).2 = w (i + 1)) (i : ℕ) : i ≤ n → x i = w i

Conversely, a sequence with the same initial value as w whose successor-array entries at the cells w designates are the ones w prescribes agrees with w up to n.

theorem TauCeti.eqOn_iff_visitCell_of_apply_visitCell_eq_succ {α : Type u_1} {x : ℕ → α} {s : α → ℕ → α} (hs : ∀ (i : ℕ), s (visitCell x i).1 (visitCell x i).2 = x (i + 1)) (w : ℕ → α) (n : ℕ) : (∀ i ≤ n, x i = w i) ↔ x 0 = w 0 ∧ ∀ i < n, s (visitCell w i).1 (visitCell w i).2 = w (i + 1)

The criterion of TauCeti.eqOn_iff_successorArray_visitCell for any array that records the successors at the cells the sequence consumes. Only the entries of s at the cells visitCell x i are constrained: the remaining entries, including the unconsumed cells of a visited row, are arbitrary. The cells a reference sequence designates are consumed by any sequence agreeing with it, so such an s pins the initial segment down just as well as the successor array.

theorem TauCeti.eqOn_iff_successorArray_visitCell {α : Type u_1} (w x : ℕ → α) (n : ℕ) : (∀ i ≤ n, x i = w i) ↔ x 0 = w 0 ∧ ∀ i < n, successorArray x (visitCell w i).1 (visitCell w i).2 = w (i + 1)

A finite initial segment is pinned down by its initial value and the successor-array entries at the cells it designates. Both the cells and the prescribed successors are read off the reference sequence w, so the right-hand side is a condition on x through finitely many entries of its successor array at cells that do not depend on x.

@[simp]

theorem TauCeti.visitedSuccessorArray_eq_successorArray_of_mem_range {α : Type u_1} {x : ℕ → α} {a : α} {k : ℕ} (h : a ∈ Set.range x) : visitedSuccessorArray x a k = successorArray x a k

On a row the sequence visits, the visited successor array is the successor array.

@[simp]

theorem TauCeti.visitedSuccessorArray_eq_self_of_not_mem_range {α : Type u_1} {x : ℕ → α} {a : α} {k : ℕ} (h : a ∉ Set.range x) : visitedSuccessorArray x a k = a

On a row the sequence never visits, the visited successor array is constant, equal to the row's own value.

theorem TauCeti.visitedSuccessorArray_visitCell {α : Type u_1} (x : ℕ → α) (n : ℕ) : visitedSuccessorArray x (visitCell x n).1 (visitCell x n).2 = x (n + 1)

At every cell consumed by a sequence, its visited successor array records the next value.

@[simp]

theorem TauCeti.pathOfSuccessors_visitedSuccessorArray {α : Type u_1} (x : ℕ → α) : pathOfSuccessors (x 0) (visitedSuccessorArray x) = x

Rebuilding from a sequence's initial value and visited successor array recovers the sequence.

theorem TauCeti.visitedSuccessorArray_congr {α : Type u_1} {x y : ℕ → α} {a : α} {k m : ℕ} (hxy : ∀ i ≤ m, x i = y i) (hk : k < visitCount x a m) : visitedSuccessorArray x a k = visitedSuccessorArray y a k

A consumed entry of the visited successor array is read off any sequence agreeing with the original over the horizon that consumes it. A row with a visit before m is visited by both sequences, so this is TauCeti.successorArray_congr.