Occurrence and transition counts of a finite word

A word w : Fin N → α over an arbitrary alphabet α has two elementary statistics: the occurrence count occCount w a, the number of positions carrying the letter a, and — for a word of length n + 1 — the transition count transitionCount w a b, the number of positions at which the letter a is immediately followed by the letter b.

The main result is that a word of positive length is determined up to rearrangement by its first letter together with its transition counts:

exists_perm_comp_of_transitionCount_eq.

The mechanism is a conservation law. Summing transitionCount w a · recovers the number of positions other than the last carrying a, and summing transitionCount w · a recovers the number of positions other than the first carrying a; comparing the two expressions for occCount w a pins the last letter once the first letter is known, and then pins every occurrence count. Equal occurrence counts glue the fibrewise bijections into a permutation of the positions.

This is the combinatorial heart of Markov exchangeability (Diaconis–Freedman), where the transition counts of a path are the sufficient statistic: see TauCeti/Probability/Exchangeability/MarkovExchangeable.lean.

Main definitions

• TauCeti.transitionCount: the number of positions of a word at which a given ordered pair of letters occurs consecutively.

Main results

• TauCeti.occCount_eq_of_transitionCount_eq: equal first letters and equal transition counts force equal occurrence counts.
• TauCeti.exists_perm_comp_of_transitionCount_eq: two such words are rearrangements of each other.
• TauCeti.consecutivePairs_append_cons: splitting a word at a letter splits its consecutive pairs.
• TauCeti.transitionCount_getD: the transition counts of a list, read as a Fin-indexed word, count its consecutive pairs.
• TauCeti.prod_consecutivePairs_getD: a product of transition weights along a list, read as a Fin-indexed word, is the product over its consecutive pairs.
• TauCeti.prod_transitionCount: a product of transition weights along a word depends on the word only through its transition counts.
• TauCeti.prod_eq_of_transitionCount_eq: the resulting comparison of two words with equal transition counts.

References

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

noncomputable def TauCeti.transitionCount {α : Type u_1} {n : ℕ} (w : Fin (n + 1) → α) (a b : α) : ℕ

The number of positions i of the word w at which the letter a is immediately followed by the letter b.

Equations

• TauCeti.transitionCount w a b = Function.occCount (fun (i : Fin n) => (w i.castSucc, w i.succ)) (a, b)

theorem TauCeti.transitionCount_def {α : Type u_1} {n : ℕ} (w : Fin (n + 1) → α) (a b : α) : transitionCount w a b = Function.occCount (fun (i : Fin n) => (w i.castSucc, w i.succ)) (a, b)

Transition counts are occurrence counts of consecutive pairs.

theorem TauCeti.transitionCount_eq_card_filter {α : Type u_1} [DecidableEq α] {n : ℕ} (w : Fin (n + 1) → α) (a b : α) : transitionCount w a b = {i : Fin n | w i.castSucc = a ∧ w i.succ = b}.card

The transition count as the cardinality of a Finset of positions.

theorem TauCeti.transitionCount_comp_castSucc_add_last {α : Type u_1} [DecidableEq α] {n : ℕ} (w : Fin (n + 2) → α) (a b : α) : (transitionCount (w ∘ Fin.castSucc) a b + if w (Fin.last n).castSucc = a ∧ w (Fin.last (n + 1)) = b then 1 else 0) = transitionCount w a b

Splitting off the last transition: the transitions in a word are those in its initial segment together with a possible transition at the final position.

theorem TauCeti.transitionCount_comp_succ_add_zero {α : Type u_1} [DecidableEq α] {n : ℕ} (w : Fin (n + 2) → α) (a b : α) : (transitionCount (w ∘ Fin.succ) a b + if w 0 = a ∧ w 1 = b then 1 else 0) = transitionCount w a b

Splitting off the first transition: the transitions in a word are those in its final segment together with a possible transition at the first position.

Words presented as lists

A word can equally be presented as a list, read through List.getD; its transitions are then the occurrences among the list List.consecutivePairs of consecutive pairs supplied by Mathlib.

theorem TauCeti.consecutivePairs_cons_cons {α : Type u_1} (a b : α) (l : List α) : (a :: b :: l).consecutivePairs = (a, b) :: (b :: l).consecutivePairs

theorem TauCeti.consecutivePairs_append_cons {α : Type u_1} (l : List α) (y : α) (m : List α) : (l ++ y :: m).consecutivePairs = (l ++ [y]).consecutivePairs ++ (y :: m).consecutivePairs

Splitting a word at a letter y splits its consecutive pairs: those of the part up to and including y, followed by those of the part from y on.

theorem TauCeti.transitionCount_getD {α : Type u_1} [DecidableEq α] (d a b : α) (n : ℕ) (l : List α) : l.length = n + 1 → transitionCount (fun (i : Fin (n + 1)) => l.getD (↑i) d) a b = List.count (a, b) l.consecutivePairs

Transition counts count consecutive pairs. Reading a list of length n + 1 as a word indexed by Fin (n + 1), its transition count from a to b is the number of occurrences of (a, b) among its consecutive pairs.

theorem TauCeti.prod_consecutivePairs_getD {α : Type u_1} {M : Type u_2} [CommMonoid M] (p : α → α → M) (d : α) (n : ℕ) (l : List α) : l.length = n + 1 → ∏ i : Fin n, p (l.getD (↑i) d) (l.getD (↑i + 1) d) = (List.map (fun (q : α × α) => p q.1 q.2) l.consecutivePairs).prod

A product of transition weights along a word is a product over its consecutive pairs. Reading a list of length n + 1 as a word indexed by Fin (n + 1), the product of a weight over the n transitions of the word is the product of that weight over the list of its consecutive pairs. This is the multiplicative counterpart of transitionCount_getD.

theorem TauCeti.sum_transitionCount_right {α : Type u_1} {n : ℕ} (w : Fin (n + 1) → α) {S : Finset α} (hS : ∀ (i : Fin n), w i.succ ∈ S) (a : α) : ∑ b ∈ S, transitionCount w a b = Function.occCount (w ∘ Fin.castSucc) a

Summing the transitions out of a counts the positions carrying a other than the last one. The index set S only has to contain the successors of transitions in w.

theorem TauCeti.sum_transitionCount_left {α : Type u_1} {n : ℕ} (w : Fin (n + 1) → α) {S : Finset α} (hS : ∀ (i : Fin n), w i.castSucc ∈ S) (b : α) : ∑ a ∈ S, transitionCount w a b = Function.occCount (w ∘ Fin.succ) b

Summing the transitions into a counts the positions carrying a other than the first one. The index set S only has to contain the predecessors of transitions in w.

theorem TauCeti.occCount_eq_of_transitionCount_eq {α : Type u_1} {n : ℕ} {u v : Fin (n + 1) → α} (h0 : u 0 = v 0) (h : ∀ (a b : α), transitionCount u a b = transitionCount v a b) (a : α) : Function.occCount u a = Function.occCount v a

The transition counts and the first letter determine the occurrence counts.

theorem TauCeti.exists_perm_comp_of_transitionCount_eq {α : Type u_1} {n : ℕ} {u v : Fin (n + 1) → α} (h0 : u 0 = v 0) (h : ∀ (a b : α), transitionCount u a b = transitionCount v a b) : ∃ (σ : Equiv.Perm (Fin (n + 1))), v ∘ ⇑σ = u

Words with the same first letter and the same transition counts are rearrangements of each other. This is the elementary fact underlying Markov exchangeability: the transition counts of a path, together with its starting point, are a sufficient statistic finer than the occurrence counts, so any symmetry expressed through them is implied by exchangeability.

theorem TauCeti.prod_transitionCount {α : Type u_1} {M : Type u_2} [CommMonoid M] {n : ℕ} (w : Fin (n + 1) → α) {S : Finset α} (hS : ∀ (i : Fin n), w i.castSucc ∈ S ∧ w i.succ ∈ S) (p : α → α → M) : ∏ i : Fin n, p (w i.castSucc) (w i.succ) = ∏ ab ∈ S ×ˢ S, p ab.1 ab.2 ^ transitionCount w ab.1 ab.2

A product of transition weights along a word is a function of its transition counts. The index set S only has to contain both endpoints of every transition in w.

theorem TauCeti.prod_eq_of_transitionCount_eq {α : Type u_1} {M : Type u_2} [CommMonoid M] {n : ℕ} {u v : Fin (n + 1) → α} (h : ∀ (a b : α), transitionCount u a b = transitionCount v a b) (p : α → α → M) : ∏ i : Fin n, p (u i.castSucc) (u i.succ) = ∏ i : Fin n, p (v i.castSucc) (v i.succ)

Words with the same transition counts have the same product of transition weights. This is prod_transitionCount with the index set eliminated: the two words are compared through the common Finset of letters they use.