Exact digit counts and further occurrence-counting inequalities

The append, take, drop, and flatten bounds extend the occurrence-counting API. The exact periodic count and digitEquiv relate integer intervals to digit strings. Exact counts distinguish the head position, where a positive integer cannot start with zero, from interior positions; their sum gives a closed formula for occurrences inside a complete cohort of equal-length numbers.

These results are exported by the project entry module as reusable infrastructure. The normality proof itself needs only the lower bounds in DigitCount.

theorem Champernowne.countOccurrences_singleton (d : ℕ) (l : List ℕ) : countOccurrences [d] l = List.count d l

Sanity bridge to List.count: single-letter blocks are List.count.

theorem Champernowne.prefix_of_prefix_append {α : Type u_1} {w a c : List α} (h : w <+: a ++ c) (hl : w.length ≤ a.length) : w <+: a

A prefix short enough to fit inside a is a prefix of a.

theorem Champernowne.countOccurrences_le_cons (w l : List ℕ) (x : ℕ) : countOccurrences w l ≤ countOccurrences w (x :: l)

theorem Champernowne.countOccurrences_append_le_min (w a b : List ℕ) : countOccurrences w (a ++ b) ≤ countOccurrences w a + countOccurrences w b + min w.length a.length

Append sandwich, upper bound: at most min w.length a.length occurrences straddle the seam (they must start within w.length − 1 slots of the end of a, and there are only a.length interior start slots).

theorem Champernowne.countOccurrences_append_le (w a b : List ℕ) : countOccurrences w (a ++ b) ≤ countOccurrences w a + countOccurrences w b + w.length

The seam bound with the word length as an upper bound.

theorem Champernowne.countOccurrences_le_append_left (w a b : List ℕ) : countOccurrences w b ≤ countOccurrences w (a ++ b)

theorem Champernowne.if_isPrefixOf_le_countOccurrences (w l : List ℕ) : (if w.isPrefixOf l = true then 1 else 0) ≤ countOccurrences w l

The whole-list window contributes to the count.

theorem Champernowne.countOccurrences_le_append_right (w a b : List ℕ) : countOccurrences w a ≤ countOccurrences w (a ++ b)

theorem Champernowne.countOccurrences_take_le (w l : List ℕ) (n : ℕ) : countOccurrences w (List.take n l) ≤ countOccurrences w l

theorem Champernowne.countOccurrences_drop_le (w l : List ℕ) (n : ℕ) : countOccurrences w (List.drop n l) ≤ countOccurrences w l

theorem Champernowne.countOccurrences_le_take_add_drop (w l : List ℕ) (n : ℕ) : countOccurrences w l ≤ countOccurrences w (List.take n l) + countOccurrences w (List.drop n l) + w.length

Cutting at n loses at most w.length (seam) occurrences.

theorem Champernowne.take_add_drop_countOccurrences_le {w : List ℕ} (hw : w ≠ []) (l : List ℕ) (n : ℕ) : countOccurrences w (List.take n l) + countOccurrences w (List.drop n l) ≤ countOccurrences w l

Cutting at n never gains occurrences (for w ≠ []).

theorem Champernowne.sum_countOccurrences_le_flatten {w : List ℕ} (hw : w ≠ []) (L : List (List ℕ)) : (List.map (countOccurrences w) L).sum ≤ countOccurrences w L.flatten

Per-block occurrences survive flattening.

theorem Champernowne.countOccurrences_eq_zero_of_length_lt {w l : List ℕ} (h : l.length < w.length) : countOccurrences w l = 0

No occurrences of w in a list shorter than w.

Exact interval ↔ digit-string counting

Superseded on the main path by the lower-bound-only layer in DigitCount.lean; see the module docstring above.

theorem Champernowne.card_Ico_filter_div_mod {A B p q d : ℕ} (hp : 0 < p) (hq : 0 < q) (hd : d < q) (hA : p * q ∣ A) (hB : p * q ∣ B) : {n ∈ Finset.Ico A B | n / p % q = d}.card = (B / (p * q) - A / (p * q)) * p

Exact periodic counting: over an interval whose endpoints are multiples of p * q, the value n / p % q hits a fixed d < q exactly p times per period p * q. Only the lower bound le_card_Ico_filter_div_mod (proved directly in DigitCount.lean) feeds champernowne_normal.

theorem Champernowne.lt_of_mem_bigDigits {b n d : ℕ} (hb : 1 < b) (hd : d ∈ bigDigits b n) : d < b

Every digit of a base-b expansion is < b.

theorem Champernowne.head_bigDigits_ne_zero {b n : ℕ} (hn : n ≠ 0) : (bigDigits b n).head? ≠ some 0

The leading digit of a nonzero number is nonzero.

theorem Champernowne.ofDigits_reverse_bigDigits (b n : ℕ) : Nat.ofDigits b (bigDigits b n).reverse = n

Round-trip 1: reading the digits of n back yields n. Together with the converse, this gives digitEquiv.

theorem Champernowne.digits_ofDigits_reverse {b : ℕ} (hb : 1 < b) {l : List ℕ} (hlt : ∀ d ∈ l, d < b) (hhead : l.head? ≠ some 0) : b.digits (Nat.ofDigits b l.reverse) = l.reverse

Little-endian form of round-trip 2.

theorem Champernowne.bigDigits_ofDigits_reverse {b : ℕ} (hb : 1 < b) {l : List ℕ} (hlt : ∀ d ∈ l, d < b) (hhead : l.head? ≠ some 0) : bigDigits b (Nat.ofDigits b l.reverse) = l

Round-trip 2: a digit string with nonzero head is the digit expansion of the number it denotes. (Also holds for l = [].)

theorem Champernowne.ofDigits_reverse_mem_Ico {b m : ℕ} (hb : 1 < b) (hm : 0 < m) {l : List ℕ} (hlen : l.length = m) (hlt : ∀ d ∈ l, d < b) (hhead : l.head? ≠ some 0) : Nat.ofDigits b l.reverse ∈ Finset.Ico (b ^ (m - 1)) (b ^ m)

A length-m digit string with nonzero head denotes an m-digit number.

theorem Champernowne.getElemOption_bigDigits {b m n : ℕ} (hb : 1 < b) (hlen : (bigDigits b n).length = m) {j : ℕ} (hj : j < m) : (bigDigits b n)[j]? = some (n / b ^ (m - 1 - j) % b)

Big-endian digit extraction: position j of an m-digit number n is n / b^(m-1-j) % b.

def Champernowne.digitEquiv {b : ℕ} (hb : 1 < b) (m : ℕ) (hm : 0 < m) : ↥(Finset.Ico (b ^ (m - 1)) (b ^ m)) ≃ { l : List ℕ // l.length = m ∧ (∀ d ∈ l, d < b) ∧ l.head? ≠ some 0 }

m-digit numbers ≃ length-m digit strings with nonzero head. Forward map bigDigits b; inverse Nat.ofDigits b ∘ List.reverse. The normality proof uses only lower-bound cardinality consequences.

Equations

• One or more equations did not get rendered due to their size.

theorem Champernowne.card_blockAt {b : ℕ} (hb : 1 < b) (m j : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hj : 0 < j) (hjk : j + w.length ≤ m) : {n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m) | List.take w.length (List.drop j (bigDigits b n)) = w}.card = (b - 1) * b ^ (m - w.length - 1)

Interior positions: block w occurs at position 0 < j in exactly (b-1)·b^(m - w.length - 1) of the m-digit numbers, independently of j and of w itself.

theorem Champernowne.card_blockAt_head {b : ℕ} (hb : 1 < b) (m : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) (hw0 : w.head? ≠ some 0) (hk : w.length ≤ m) : {n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m) | List.take w.length (List.drop 0 (bigDigits b n)) = w}.card = b ^ (m - w.length)

Head position: a block with nonzero head occurs at position 0 in exactly b^(m - w.length) of the m-digit numbers.

theorem Champernowne.card_blockAt_past_end {b : ℕ} (hb : 1 < b) (m j : ℕ) {w : List ℕ} (hwne : w ≠ []) (hj : m < j + w.length) : {n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m) | List.take w.length (List.drop j (bigDigits b n)) = w}.card = 0

Past the end: no window of length w.length starts after m - w.length.

theorem Champernowne.card_blockAt_head_zero {b : ℕ} (hb : 1 < b) (m : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hw0 : w.head? = some 0) (hk : w.length ≤ m) : {n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m) | List.take w.length (List.drop 0 (bigDigits b n)) = w}.card = 0

Head position, leading zero: a block with head 0 never occurs at position 0 of an m-digit number.

theorem Champernowne.sum_countOccurrences_cohort_eq_head {b : ℕ} (hb : 1 < b) (m : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) (hk : w.length ≤ m) : ∑ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), countOccurrences w (bigDigits b n) = {n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m) | List.take w.length (List.drop 0 (bigDigits b n)) = w}.card + (m - w.length) * ((b - 1) * b ^ (m - w.length - 1))

Split a cohort occurrence count into its head contribution and interior windows.

theorem Champernowne.sum_countOccurrences_cohort {b : ℕ} (hb : 1 < b) (m : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) (hw0 : w.head? ≠ some 0) (hk : w.length ≤ m) : ∑ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), countOccurrences w (bigDigits b n) = b ^ (m - w.length) + (m - w.length) * ((b - 1) * b ^ (m - w.length - 1))

Block w with nonzero head occurs b^(m-k) + (m-k)·(b-1)·b^(m-k-1) times inside the digit strings of all m-digit numbers (k := w.length).

theorem Champernowne.sum_countOccurrences_cohort_zero {b : ℕ} (hb : 1 < b) (m : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) (hw0 : w.head? = some 0) (hk : w.length ≤ m) : ∑ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), countOccurrences w (bigDigits b n) = (m - w.length) * ((b - 1) * b ^ (m - w.length - 1))

Block w with head 0 occurs (m-k)·(b-1)·b^(m-k-1) times inside the digit strings of all m-digit numbers.