Asymptotic frequency of digit blocks

champM b n is the digit length of the number straddling position n. The natural-number prefix bounds give an error that is little-o of n, and therefore the frequency of each nonempty length-k word tends to b⁻ᵏ.

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

Digit length of the straddling number champIndex b n + 1.

Equations

• Champernowne.champM b n = Nat.log b (Champernowne.champIndex b n + 1) + 1

theorem Champernowne.champM_pos (b n : ℕ) : 0 < champM b n

theorem Champernowne.pow_champM_le (b n : ℕ) : b ^ (champM b n - 1) ≤ champIndex b n + 1

theorem Champernowne.le_pow_champM {b : ℕ} (hb : 1 < b) (n : ℕ) : champIndex b n + 1 ≤ b ^ champM b n

theorem Champernowne.cohort_le_n {b : ℕ} (hb : 1 < b) (n : ℕ) : (b - 1) * b ^ (champM b n - 2) * (champM b n - 1) ≤ n

Length lower bound: n dominates the second-to-top cohort.

theorem Champernowne.tendsto_champIndex_atTop (b : ℕ) : Filter.Tendsto (champIndex b) Filter.atTop Filter.atTop

theorem Champernowne.tendsto_champM_atTop {b : ℕ} (hb : 1 < b) : Filter.Tendsto (champM b) Filter.atTop Filter.atTop

General-w packaging

Instantiates the Positions.lean straddle transfer at M := champM b n. w.length ≤ champM b n holds only eventually, since champM b n → ∞ (tendsto_champM_atTop), so the transfer itself is wrapped in ∀ᶠ.

theorem Champernowne.base_pow_count_le {b : ℕ} (hb : 1 < b) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) : ∀ᶠ (n : ℕ) in Filter.atTop, b ^ w.length * countOccurrences w (champPrefix b n) ≤ n + 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n

theorem Champernowne.le_base_pow_count {b : ℕ} (hb : 1 < b) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) : ∀ᶠ (n : ℕ) in Filter.atTop, n ≤ b ^ w.length * countOccurrences w (champPrefix b n) + 7 * (w.length + 1) * b ^ w.length * b ^ champM b n

theorem Champernowne.err_mul_le_pow {b : ℕ} (hb : 1 < b) (n : ℕ) (w : List ℕ) : 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n * ((b - 1) * (champM b n - 1)) ≤ 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ 2 * n

The error dominates its own budget: E(n)·(b-1)(M−1) ≤ E'·n.

theorem Champernowne.err_mul_le_pow' {b : ℕ} (hb : 1 < b) (n : ℕ) (w : List ℕ) (h2 : 2 ≤ champM b n) : 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n * ((b - 1) * champM b n) ≤ 2 * (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ 2) * n

Subtraction-free form for M ≥ 2.

theorem Champernowne.tendsto_err_div_pow {b : ℕ} (hb : 1 < b) (w : List ℕ) : Filter.Tendsto (fun (n : ℕ) => 7 * (↑w.length + 1) * ↑b ^ (2 * w.length) * ↑b ^ champM b n / ↑n) Filter.atTop (nhds 0)

The error sequence is negligible relative to n.

theorem Champernowne.countOccurrences_champPrefix_sub_isLittleO {b : ℕ} (hb : 1 < b) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) : (fun (n : ℕ) => ↑(countOccurrences w (champPrefix b n)) - ↑n / ↑b ^ w.length) =o[Filter.atTop] fun (n : ℕ) => ↑n

countOccurrences w (champPrefix b n) − n/b^k = o(n).

theorem Champernowne.tendsto_countOccurrences_champPrefix_div {b : ℕ} (hb : 1 < b) {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) : Filter.Tendsto (fun (n : ℕ) => ↑(countOccurrences w (champPrefix b n)) / ↑n) Filter.atTop (nhds (↑b ^ w.length)⁻¹)

Every nonempty block w (digits < b) occurs in the base-b Champernowne stream with asymptotic frequency b⁻ᵏ.