Loops at a base point and their excursions

A finite word that starts at a letter a₀ and returns to it splits at its visits to a₀ into excursions: the (possibly empty) stretches of letters strictly between consecutive visits. Conversely a list bs : List (List α) of excursions spells out a word

a₀, bs[0], a₀, bs[1], a₀, …, bs[k-1], a₀

which this file calls TauCeti.loopPath a₀ bs.

The theorem of this file is that the transition counts of a loop are the sum of the transition counts of its individual excursion loops (TauCeti.transitionCount_loopPathAt), so they do not see the order in which the excursions are traversed (TauCeti.transitionCount_loopPathAt_eq_of_perm). Together with the first-letter equality TauCeti.loopPathAt_zero this is exactly the input of Diaconis and Freedman's Markov exchangeability, where the first letter and the transition counts of a finite path are its sufficient statistic: see TauCeti/Probability/Exchangeability/Excursion.lean.

The mechanism is a bookkeeping identity for the list List.consecutivePairs l of consecutive pairs of a word. Concatenating two words at a shared letter y splits that list as the pairs of the first word closed off with y, followed by the pairs of the second word (TauCeti.consecutivePairs_append_cons); every excursion of a loop is closed off with a₀, so iterating the split writes the pairs of loopPath a₀ bs as a List.flatMap over bs, which a permutation of bs rearranges.

Words are lists here, while TauCeti.transitionCount counts transitions of a Fin (n + 1)-indexed word; the bridge is TauCeti.transitionCount_getD, which reads a list of length n + 1 as such a word through List.getD. Both of those list lemmas live in TauCeti/Combinatorics/Enumerative/TransitionCount.lean.

Main definitions

• TauCeti.loopPath: the word spelled out by a base letter and a list of excursions.
• TauCeti.loopSteps: its number of transitions.
• TauCeti.loopPathAt: loopPath read as a function on ℕ, padded with the base letter.

Main results

• TauCeti.transitionCount_loopPathAt: the transition counts of a loop are the sum of those of its excursion loops.
• TauCeti.transitionCount_loopPathAt_eq_of_perm: reordering the excursions leaves them unchanged.
• TauCeti.exists_loopPath: every word that starts and ends at a₀ is a loop path, with excursions that avoid a₀.
• TauCeti.loopPath_injOn: those excursions are unique.
• TauCeti.loopPathAt_cons_add: past its first excursion a loop is the loop of the remaining ones.
• TauCeti.loopPathAt_append_of_le: over the span of its first excursions a loop is their loop.
• TauCeti.infinite_setOf_loopPathAt_eq: read as a function on ℕ, a loop returns to its base letter infinitely often.
• TauCeti.map_range_loopPathAt: reading that function over the loop's span spells the loop word out again.

References

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

Loops and their excursions

def TauCeti.loopPath {α : Type u_1} (a₀ : α) : List (List α) → List α

The word spelled out by a base letter a₀ and a list of excursions: a₀, the first excursion, a₀ again, the second excursion, and so on, ending with a final a₀.

Equations

• TauCeti.loopPath a₀ [] = [a₀]
• TauCeti.loopPath a₀ (e :: bs) = a₀ :: (e ++ TauCeti.loopPath a₀ bs)

@[simp]

theorem TauCeti.loopPath_nil {α : Type u_1} (a₀ : α) : loopPath a₀ [] = [a₀]

@[simp]

theorem TauCeti.loopPath_cons {α : Type u_1} (a₀ : α) (e : List α) (bs : List (List α)) : loopPath a₀ (e :: bs) = a₀ :: (e ++ loopPath a₀ bs)

theorem TauCeti.loopPath_append {α : Type u_1} (a₀ : α) (bs cs : List (List α)) : loopPath a₀ (bs ++ cs) = (loopPath a₀ bs).dropLast ++ loopPath a₀ cs

Concatenating two lists of excursions splices their loops at the shared base letter: the final letter of the first loop is the initial letter of the second.

def TauCeti.loopSteps {α : Type u_1} (bs : List (List α)) : ℕ

The number of transitions of a loop with the given excursions: each excursion contributes its own length, plus the one step that returns to the base letter.

Equations

• TauCeti.loopSteps bs = (List.map (fun (e : List α) => e.length + 1) bs).sum

@[simp]

theorem TauCeti.loopSteps_nil {α : Type u_1} : loopSteps [] = 0

@[simp]

theorem TauCeti.loopSteps_cons {α : Type u_1} (e : List α) (bs : List (List α)) : loopSteps (e :: bs) = e.length + 1 + loopSteps bs

@[simp]

theorem TauCeti.length_loopPath {α : Type u_1} (a₀ : α) (bs : List (List α)) : (loopPath a₀ bs).length = loopSteps bs + 1

theorem TauCeti.loopSteps_eq_of_perm {α : Type u_1} {bs bs' : List (List α)} (h : bs.Perm bs') : loopSteps bs = loopSteps bs'

Reordering the excursions does not change the length of the loop.

@[simp]

theorem TauCeti.loopSteps_append {α : Type u_1} (bs cs : List (List α)) : loopSteps (bs ++ cs) = loopSteps bs + loopSteps cs

theorem TauCeti.length_le_loopSteps {α : Type u_1} (bs : List (List α)) : bs.length ≤ loopSteps bs

A loop takes at least one step per excursion, since every excursion is followed by the step back to the base letter.

def TauCeti.loopPathAt {α : Type u_1} (a₀ : α) (bs : List (List α)) (i : ℕ) : α

A loop, read as a function on ℕ: past its last letter it is padded with the base letter.

Equations

• TauCeti.loopPathAt a₀ bs i = (TauCeti.loopPath a₀ bs).getD i a₀

theorem TauCeti.loopPathAt_def {α : Type u_1} (a₀ : α) (bs : List (List α)) (i : ℕ) : loopPathAt a₀ bs i = (loopPath a₀ bs).getD i a₀

@[simp]

theorem TauCeti.loopPathAt_zero {α : Type u_1} (a₀ : α) (bs : List (List α)) : loopPathAt a₀ bs 0 = a₀

theorem TauCeti.loopPathAt_loopSteps {α : Type u_1} (a₀ : α) (bs : List (List α)) : loopPathAt a₀ bs (loopSteps bs) = a₀

@[simp]

theorem TauCeti.loopPathAt_cons_of_lt {α : Type u_1} (a₀ : α) (e : List α) (bs : List (List α)) {i : ℕ} (hi : i < e.length) : loopPathAt a₀ (e :: bs) (i + 1) = e[i]

Inside its first excursion, a loop spells that excursion out.

@[simp]

theorem TauCeti.loopPathAt_cons_add {α : Type u_1} (a₀ : α) (e : List α) (bs : List (List α)) (i : ℕ) : loopPathAt a₀ (e :: bs) (e.length + 1 + i) = loopPathAt a₀ bs i

Past its first excursion, a loop is the loop of the remaining excursions. The shift is by the length of that excursion plus the one step returning to the base letter.

@[simp]

theorem TauCeti.loopPathAt_eq_of_loopSteps_le {α : Type u_1} (a₀ : α) (bs : List (List α)) {i : ℕ} (hi : loopSteps bs ≤ i) : loopPathAt a₀ bs i = a₀

A loop sits at its base letter from its final letter onwards: loopPathAt pads with the base letter past the end of the word.

theorem TauCeti.loopPathAt_append_of_le {α : Type u_1} (a₀ : α) (bs cs : List (List α)) {i : ℕ} (hi : i ≤ loopSteps bs) : loopPathAt a₀ (bs ++ cs) i = loopPathAt a₀ bs i

A loop extends its own initial stretches. Over the span of bs, the loop of bs ++ cs spells out the loop of bs: the two words share the prefix loopPath a₀ bs, and at the very end of that span both sit at the base letter, where the loop of cs starts.

theorem TauCeti.infinite_setOf_loopPathAt_eq {α : Type u_1} (a₀ : α) (bs : List (List α)) : {i : ℕ | loopPathAt a₀ bs i = a₀}.Infinite

A loop returns to its base letter infinitely often, since loopPathAt pads with that letter. This is what lets the excursion decomposition of a loop be read with no side condition.

theorem TauCeti.map_range_loopPathAt {α : Type u_1} (a₀ : α) (bs : List (List α)) : List.map (loopPathAt a₀ bs) (List.range (loopSteps bs + 1)) = loopPath a₀ bs

A loop read as a function on ℕ recovers the loop word. Reading loopPathAt over the whole span of the loop spells out loopPath again.

theorem TauCeti.loopPath_eq_cons_tail {α : Type u_1} (a₀ : α) (bs : List (List α)) : loopPath a₀ bs = a₀ :: (loopPath a₀ bs).tail

A loop always starts at its base letter.

theorem TauCeti.loopPath_injOn {α : Type u_1} (a₀ : α) : Set.InjOn (loopPath a₀) {bs : List (List α) | ∀ e ∈ bs, a₀ ∉ e}

The excursions of a loop are determined by the loop. Two lists of excursions that avoid the base letter and spell out the same word are equal, so together with TauCeti.exists_loopPath this makes TauCeti.loopPath a bijection between such lists and the words that start and end at the base letter.

theorem TauCeti.consecutivePairs_loopPath {α : Type u_1} (a₀ : α) (bs : List (List α)) : (loopPath a₀ bs).consecutivePairs = List.flatMap (fun (e : List α) => (loopPath a₀ [e]).consecutivePairs) bs

The consecutive pairs of a loop, gathered excursion by excursion.

theorem TauCeti.transitionCount_loopPathAt {α : Type u_1} (a₀ : α) (bs : List (List α)) {n : ℕ} (hn : loopSteps bs = n) (a b : α) : transitionCount (fun (i : Fin (n + 1)) => loopPathAt a₀ bs ↑i) a b = (List.map (fun (e : List α) => transitionCount (fun (i : Fin (e.length + 1 + 1)) => loopPathAt a₀ [e] ↑i) a b) bs).sum

The transition counts of a loop are the sum of those of its excursions. Each excursion is counted as the loop it forms on its own, from the base letter back to it.

theorem TauCeti.transitionCount_loopPathAt_eq_of_perm {α : Type u_1} (a₀ : α) {bs bs' : List (List α)} (h : bs.Perm bs') {n : ℕ} (hn : loopSteps bs = n) (a b : α) : transitionCount (fun (i : Fin (n + 1)) => loopPathAt a₀ bs ↑i) a b = transitionCount (fun (i : Fin (n + 1)) => loopPathAt a₀ bs' ↑i) a b

Reordering the excursions of a loop leaves its transition counts unchanged.

Every loop decomposes into excursions

theorem TauCeti.exists_loopPath {α : Type u_1} (a₀ : α) (n : ℕ) (x : ℕ → α) : x 0 = a₀ → x n = a₀ → ∃ (bs : List (List α)), loopSteps bs = n ∧ (∀ e ∈ bs, a₀ ∉ e) ∧ ∀ i ≤ n, loopPathAt a₀ bs i = x i

A word that starts and ends at a₀ is the loop of its excursions. The excursions are the stretches strictly between consecutive visits to a₀, so none of them visits a₀.

theorem TauCeti.exists_loopPathAt {α : Type u_1} {n : ℕ} (w : Fin (n + 1) → α) (hw : w (Fin.last n) = w 0) : ∃ (bs : List (List α)), loopSteps bs = n ∧ (∀ e ∈ bs, w 0 ∉ e) ∧ ∀ (i : Fin (n + 1)), loopPathAt (w 0) bs ↑i = w i

A word that ends where it starts is the loop of its excursions. The Fin-indexed form of TauCeti.exists_loopPath.