Champernowne sequence: core definitions

The digits of each positive integer are written in big-endian order in base b. champBlocks b N concatenates the first N blocks, and champDigit b is the resulting infinite digit stream. countOccurrences counts overlapping finite words, and IsNormalSequence states their limiting frequencies.

Definitions allow every base; hypotheses 1 < b appear on the results that need them. The prefix-coherence API is in LeanPool.Champernowne.Prefix.

def Champernowne.bigDigits (b n : ℕ) : List ℕ

Big-endian digits of n in base b.

Equations

• Champernowne.bigDigits b n = (b.digits n).reverse

def Champernowne.champBlocks (b N : ℕ) : List ℕ

First N blocks of the base-b Champernowne sequence: digits of 1..N.

Equations

• Champernowne.champBlocks b N = (List.map (fun (n : ℕ) => Champernowne.bigDigits b (n + 1)) (List.range N)).flatten

theorem Champernowne.champBlocks_succ (b N : ℕ) : champBlocks b (N + 1) = champBlocks b N ++ bigDigits b (N + 1)

theorem Champernowne.le_length_champBlocks (b N : ℕ) : N ≤ (champBlocks b N).length

def Champernowne.champDigit (b i : ℕ) : ℕ

The i-th digit (0-indexed) of the base-b Champernowne sequence.

Equations

• Champernowne.champDigit b i = (Champernowne.champBlocks b (i + 1))[i]

def Champernowne.countOccurrences (w l : List ℕ) : ℕ

Number of (overlapping) occurrences of w as a contiguous block of l.

Window convention: l.tails yields the suffixes starting at positions 0, 1, …, l.length (the last being []). A tail shorter than w can never satisfy w.isPrefixOf, so the windows that can count are exactly the start positions 0 … l.length - w.length; there are no partial windows at the end of the list. In particular countOccurrences w l = 0 whenever w.length > l.length, and countOccurrences [] l = l.length + 1 (the empty word is a prefix of every tail) — callers always pass w ≠ [].

Equations

• Champernowne.countOccurrences w l = List.countP (fun (x : List ℕ) => w.isPrefixOf x) l.tails

def Champernowne.IsNormalSequence (b : ℕ) (s : ℕ → ℕ) : Prop

Normality of a digit sequence in base b: every block of length k (entries < b, leading zeros allowed) has asymptotic frequency b⁻ᵏ.

Equations

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