Interval ↔ digit-string counting

Base-general (1 < b). Everything here feeds the lower comparison le_base_pow_countOccurrences_champBlocks between the stream length and b^k · (occurrence count) over [1, N]; the upper direction is derived downstream (Positions.lean) from the lower one via the allWords pigeonhole. Two relaxations keep this file small:

• occurrences at the head position of a number are never counted — the interior positions already carry the main term, uniformly in w (so no w.head? = some 0 case split anywhere), and
• every cohort, full or not, is handled by the partial-cohort lower bound, so only lower periodic-count bounds are ever needed.

The exact counterparts (exact periodic count, per-position cards, exact cohort sums, digitEquiv and its round-trips) live in CountExtras.lean.

Generic counting and rounding lemmas (no base)

theorem Champernowne.le_card_Ico_filter_div_mod {A t p q d : ℕ} (hp : 0 < p) (hq : 0 < q) (hd : d < q) (hA : p * q ∣ A) : t / (p * q) * p ≤ {n ∈ Finset.Ico A (A + t) | n / p % q = d}.card

Lower bound for periodic counting: over [A, A + t) with a left endpoint divisible by p * q, the value n / p % q hits a fixed d < q at least t / (p·q) · p times — p hits in each complete period p·q. Proved directly by injecting range (t/(p·q)) ×ˢ range p; the main proof never needs the exact count (card_Ico_filter_div_mod, CountExtras.lean).

theorem Champernowne.div_le_div_mul_add (t p q : ℕ) (hp : 0 < p) (hq : 0 < q) : t / q ≤ t / (p * q) * p + p

Rounding compatibility: t/q ≤ t/(p·q)·p + p.

theorem Champernowne.geomsum_lt {b : ℕ} (hb : 1 < b) (K : ℕ) : ∑ i ∈ Finset.range K, b ^ i < b ^ K

∑_{i<K} b^i < b^K for 1 < b.

bigDigits API

theorem Champernowne.length_bigDigits_eq {b m n : ℕ} (hb : 1 < b) (h1 : b ^ (m - 1) ≤ n) (h2 : n < b ^ m) : (bigDigits b n).length = m

A number in [b^(m-1), b^m) has exactly m digits.

Cardinalities

theorem Champernowne.card_mDigit {b : ℕ} (hb : 1 < b) (m : ℕ) (hm : 0 < m) : (Finset.Ico (b ^ (m - 1)) (b ^ m)).card = (b - 1) * b ^ (m - 1)

There are (b-1) * b^(m-1) numbers with exactly m digits.

Cohort decomposition

theorem Champernowne.sum_Ico_one_pow {β : Type u_1} [AddCommMonoid β] {b : ℕ} (hb : 1 < b) (M : ℕ) (g : ℕ → β) : ∑ n ∈ Finset.Ico 1 (b ^ M), g n = ∑ m ∈ Finset.Icc 1 M, ∑ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), g n

Cohort decomposition of a sum over [1, b^M).

Stream and cohort length sums

theorem Champernowne.length_champBlocks (b N : ℕ) : (champBlocks b N).length = ∑ n ∈ Finset.Ico 1 (N + 1), (bigDigits b n).length

The stream-prefix length as a sum over the numbers 1..N.

theorem Champernowne.sum_length_cohort {b : ℕ} (hb : 1 < b) (m : ℕ) (hm : 0 < m) : ∑ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), (bigDigits b n).length = (b - 1) * b ^ (m - 1) * m

Total digit length of the m-digit cohort.

theorem Champernowne.sum_length_partial {b : ℕ} (hb : 1 < b) (K t : ℕ) (hAt : b ^ K + t ≤ b ^ (K + 1)) : ∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), (bigDigits b n).length = t * (K + 1)

Total digit length of a partial cohort.

Blocks at positions

theorem Champernowne.block_eq_iff {b m n : ℕ} (hb : 1 < b) (hlen : (bigDigits b n).length = m) {w : List ℕ} (hw : ∀ d ∈ w, d < b) {j : ℕ} (hjk : j + w.length ≤ m) : List.take w.length (List.drop j (bigDigits b n)) = w ↔ n / b ^ (m - j - w.length) % b ^ w.length = Nat.ofDigits b w.reverse

Substring ↔ arithmetic bridge: the block of w.length digits at big-endian position j of an m-digit n equals w iff the corresponding quotient-remainder is the value of w.

Partial-cohort block occurrence sums

Every cohort is treated as a partial cohort [b^K, b^K + t) (a full one has t = b^(K+1) - b^K), and only the interior positions j ≥ 1 are counted — occurrences at the head of a number are dropped, which is sound for a lower bound and uniform in w (a leading-zero w simply never occurs there).

theorem Champernowne.filter_blockAt_partial_congr {b : ℕ} (hb : 1 < b) (K t j : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hjk : j + w.length ≤ K + 1) (hAt : b ^ K + t ≤ b ^ (K + 1)) : {n ∈ Finset.Ico (b ^ K) (b ^ K + t) | List.take w.length (List.drop j (bigDigits b n)) = w} = {n ∈ Finset.Ico (b ^ K) (b ^ K + t) | n / b ^ (K + 1 - j - w.length) % b ^ w.length = Nat.ofDigits b w.reverse}

Convert the block predicate at position j to the arithmetic predicate, on a partial cohort of (K+1)-digit numbers.

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

Lower bound for one interior position over a partial cohort.

theorem Champernowne.sum_countOccurrences_Ico_eq {b : ℕ} (hb : 1 < b) (K t : ℕ) (w : List ℕ) (hAt : b ^ K + t ≤ b ^ (K + 1)) : ∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), countOccurrences w (bigDigits b n) = ∑ j ∈ Finset.range (K + 2), {n ∈ Finset.Ico (b ^ K) (b ^ K + t) | List.take w.length (List.drop j (bigDigits b n)) = w}.card

Partial-cohort occurrence sum as a sum of per-position cards.

theorem Champernowne.le_sum_countOccurrences_partial_cohort {b : ℕ} (hb : 1 < b) (K t : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hk : w.length ≤ K + 1) (hAt : b ^ K + t ≤ b ^ (K + 1)) : (K + 1 - w.length) * (t / b ^ w.length) ≤ ∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), countOccurrences w (bigDigits b n) + 2 * b ^ (K + 1 - w.length)

Partial-cohort occurrence sum, lower bound (stated additively; drops the head position, which is only ever a nonnegative contribution).

Partial-cohort comparison, boundary induction, and general N

theorem Champernowne.linear_le_const_mul_pow {b : ℕ} (hb : 1 < b) (c j : ℕ) : c + j + 1 ≤ (c + 1) * b ^ j

c + j + 1 ≤ (c+1) * b^j for b ≥ 2 -- linear growth is dominated by any base's exponential, uniformly from j = 0.

theorem Champernowne.le_base_pow_countOccurrences_partial {b : ℕ} (hb : 1 < b) (K t : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) (hk : w.length ≤ K + 1) (hAt : b ^ K + t ≤ b ^ (K + 1)) : ∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), (bigDigits b n).length ≤ b ^ w.length * ∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), countOccurrences w (bigDigits b n) + 3 * (w.length + 1) * b ^ (K + 1)

Partial-cohort comparison, lower.

theorem Champernowne.cohort_error_add_le {b : ℕ} (hb : 1 < b) (c K : ℕ) : 6 * c * b ^ K + 3 * c * b ^ (K + 1) ≤ 6 * c * b ^ (K + 1)

The accumulated cohort error is absorbed by the next power of the base.

theorem Champernowne.le_base_pow_count_boundary {b : ℕ} (hb : 1 < b) (K : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) : ∑ n ∈ Finset.Ico 1 (b ^ K), (bigDigits b n).length ≤ b ^ w.length * ∑ n ∈ Finset.Ico 1 (b ^ K), countOccurrences w (bigDigits b n) + 6 * (w.length + 1) * b ^ K

Boundary comparison, lower: over the complete cohorts [1, b^K), the stream length exceeds b^k times the occurrence count by at most 6·(k+1)·b^K. Each full cohort [b^K, b^(K+1)) is a partial cohort with t = b^(K+1) - b^K (le_base_pow_countOccurrences_partial); the geometric accumulation of the per-cohort errors 3(k+1)·b^(K+1) stays below 6(k+1)·b^K because 2 ≤ b. Cohorts too short to fit w only need their length bounded (the occurrence count is dropped at ≥ 0).

theorem Champernowne.le_base_pow_countOccurrences_champBlocks {b : ℕ} (hb : 1 < b) (N M : ℕ) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) (hM : 0 < M) (hwM : w.length ≤ M) (h1 : b ^ (M - 1) ≤ N + 1) (h2 : N + 1 ≤ b ^ M) : ∑ n ∈ Finset.Ico 1 (N + 1), (bigDigits b n).length ≤ b ^ w.length * ∑ n ∈ Finset.Ico 1 (N + 1), countOccurrences w (bigDigits b n) + 6 * (w.length + 1) * b ^ M

General-N comparison, lower.