Occurrence-counting inequalities

This file gives the lower append bound, a characterization by starting positions, and the allWords enumeration of length-k digit strings. Summing occurrences over allWords bounds the number of windows, allowing upper frequency estimates to be derived from lower ones by complement.

The window convention is documented at countOccurrences. Statements assume w ≠ [] when the empty word needs to be excluded. Further append, take, drop, and exact digit-counting results are in LeanPool.Champernowne.CountExtras.

theorem Champernowne.countOccurrences_cons (w l : List ℕ) (x : ℕ) : countOccurrences w (x :: l) = countOccurrences w l + if w.isPrefixOf (x :: l) = true then 1 else 0

theorem Champernowne.countOccurrences_nil' (w : List ℕ) : countOccurrences w [] = if w.isPrefixOf [] = true then 1 else 0

theorem Champernowne.countOccurrences_nil {w : List ℕ} (hw : w ≠ []) : countOccurrences w [] = 0

theorem Champernowne.isPrefixOf_append_of_isPrefixOf {w a : List ℕ} (b : List ℕ) (h : w.isPrefixOf a = true) : w.isPrefixOf (a ++ b) = true

Extending the list to the right preserves window hits.

The append lower bound

theorem Champernowne.add_countOccurrences_le_append {w : List ℕ} (hw : w ≠ []) (a b : List ℕ) : countOccurrences w a + countOccurrences w b ≤ countOccurrences w (a ++ b)

Lower bound: occurrences inside a and inside b survive in a ++ b. Fails for w = [] (window counts overlap at the seam).

Occurrences in champBlocks

theorem Champernowne.sum_le_countOccurrences_champBlocks {b : ℕ} {w : List ℕ} (hw : w ≠ []) (N : ℕ) : ∑ n ∈ Finset.Ico 1 (N + 1), countOccurrences w (bigDigits b n) ≤ countOccurrences w (champBlocks b N)

Per-number occurrences survive in the stream.

Position characterization

theorem Champernowne.countOccurrences_eq_card_filter_range (w l : List ℕ) : countOccurrences w l = {j ∈ Finset.range (l.length + 1) | w.isPrefixOf (List.drop j l) = true}.card

countOccurrences counts window start positions.

Word enumeration and the window pigeonhole

allWords b k enumerates all length-k digit strings over {0, …, b−1} (leading zeros allowed) — the complement machinery that lets the upper occurrence bound be derived from the lower one: a window matching no v ≠ w must match w.

def Champernowne.allWords (b : ℕ) : ℕ → Finset (List ℕ)

All length-k digit strings over {0, …, b−1}, leading zeros allowed.

Equations

• Champernowne.allWords b 0 = {[]}
• Champernowne.allWords b k.succ = (Finset.range b).biUnion fun (d : ℕ) => Finset.image (fun (x : List ℕ) => d :: x) (Champernowne.allWords b k)

theorem Champernowne.mem_allWords {b k : ℕ} {l : List ℕ} : l ∈ allWords b k ↔ l.length = k ∧ ∀ d ∈ l, d < b

theorem Champernowne.card_allWords (b k : ℕ) : (allWords b k).card = b ^ k

theorem Champernowne.sum_countOccurrences_allWords_le (b k : ℕ) (l : List ℕ) : ∑ v ∈ allWords b k, countOccurrences v l ≤ l.length + 1

Window pigeonhole: a window position matches at most one length-k word, so over ALL length-k words the occurrence counts total at most the number of window start positions. This single inequality replaces the entire upper-bound counting chain.