Position arithmetic & prefix decomposition

champIndex b n locates digit position n in the base-b stream: the greatest N whose complete block champBlocks b N fits within the first n digits. The chain champBlocks b (champIndex b n) <+: champPrefix b n <+: champBlocks b (champIndex b n + 1) transfers occurrence counts from complete blocks to arbitrary prefixes with a one-number error, giving the two-sided comparison between b^k · countOccurrences w (champPrefix b n) and n with error O(k)·b^(2k)·b^M.

def Champernowne.champIndex (b n : ℕ) : ℕ

Greatest N with (champBlocks b N).length ≤ n.

Equations

• Champernowne.champIndex b n = Nat.findGreatest (fun (N : ℕ) => (Champernowne.champBlocks b N).length ≤ n) n

theorem Champernowne.length_champBlocks_champIndex_le (b n : ℕ) : (champBlocks b (champIndex b n)).length ≤ n

theorem Champernowne.lt_length_champBlocks_champIndex_succ (b n : ℕ) : n < (champBlocks b (champIndex b n + 1)).length

theorem Champernowne.champPrefix_prefix (b n : ℕ) : champPrefix b n <+: champBlocks b n

champPrefix b n is a prefix of the blocks it is carved from.

theorem Champernowne.champBlocks_prefix_champPrefix {b N n : ℕ} (h : (champBlocks b N).length ≤ n) : champBlocks b N <+: champPrefix b n

Complete blocks below position n form a prefix of champPrefix b n.

theorem Champernowne.n_lt_length_champIndex_add (b n : ℕ) : n < (champBlocks b (champIndex b n)).length + (bigDigits b (champIndex b n + 1)).length

Position n lies within one number's digits of the complete blocks.

theorem Champernowne.length_bigDigits_champIndex_succ_le {b n M : ℕ} (hb : 1 < b) (h2 : champIndex b n + 1 ≤ b ^ M) : (bigDigits b (champIndex b n + 1)).length ≤ M + 1

The straddling number has at most M + 1 digits.

General-w straddle transfer

Only the lower transfer is proved against the counting machinery (the stream sandwich sum_le_countOccurrences_champBlocks, the general-N result le_base_pow_countOccurrences_champBlocks from DigitCount.lean, and the champIndex straddle). The upper transfer is then derived from the lower one by a complement/pigeonhole argument over all b^k length-k words (allWords), at the price of one extra b^k factor in the error constant.

theorem Champernowne.le_countOccurrences_champPrefix (b n : ℕ) {w : List ℕ} (hwne : w ≠ []) : countOccurrences w (champBlocks b (champIndex b n)) ≤ countOccurrences w (champPrefix b n)

champBlocks (champIndex n) is a genuine prefix of champPrefix n, so its occurrence count only ever undercounts.

theorem Champernowne.le_base_pow_countOccurrences_champPrefix {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) ≤ champIndex b n + 1) (h2 : champIndex b n + 1 ≤ b ^ M) : n ≤ b ^ w.length * countOccurrences w (champPrefix b n) + 7 * (w.length + 1) * b ^ w.length * b ^ M

Main transfer, lower: for b^(M-1) ≤ champIndex b n + 1 ≤ b^M and w.length ≤ M, n ≤ b^k · countOccurrences w (champPrefix b n) + 7(k+1)·b^k·b^M.

theorem Champernowne.base_pow_countOccurrences_champPrefix_le {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) ≤ champIndex b n + 1) (h2 : champIndex b n + 1 ≤ b ^ M) : b ^ w.length * countOccurrences w (champPrefix b n) ≤ n + 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ M

Main transfer, upper — derived from the lower transfer by complement: a window position matches exactly one of the b^k length-k words, so b^k·(occ w + Σ_{v ≠ w} occ v) ≤ b^k·(n+1) (sum_countOccurrences_allWords_le), while the lower transfer applied to each of the b^k − 1 words v ≠ w bounds Σ_{v ≠ w} b^k·occ v from below. Costs one extra b^k factor in the error over the lower bound's 7(k+1)·b^k·b^M.

Prefix chain

theorem Champernowne.champPrefix_prefix_champBlocks {b n N : ℕ} (h : n ≤ (champBlocks b N).length) : champPrefix b n <+: champBlocks b N

champPrefix b n sits inside the complete blocks covering position n. This completes the prefix chain champBlocks (champIndex n) <+: champPrefix n <+: champBlocks (champIndex n + 1).