Prefix-coherence API

Supporting lemmas relating champBlocks to champPrefix/champDigit: champBlocks is prefix-monotone in N, so champBlocks_getElem shows any sufficiently long block computes the same digit as champDigit, and champPrefix (the first n digits) agrees with mapping champDigit over List.range n. Used by Positions.lean, Asymptotics.lean, and Main.lean's proof; not needed to state champernowne_normal itself (see Defs.lean).

theorem Champernowne.champBlocks_prefix {b N M : ℕ} (h : N ≤ M) : champBlocks b N <+: champBlocks b M

theorem Champernowne.champBlocks_getElem (b N i : ℕ) (h : i < (champBlocks b N).length) : (champBlocks b N)[i] = champDigit b i

Coherence: any sufficiently long prefix computes champDigit.

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

The first n digits of the base-b Champernowne sequence.

Equations

• Champernowne.champPrefix b n = List.take n (Champernowne.champBlocks b n)

theorem Champernowne.length_champPrefix (b n : ℕ) : (champPrefix b n).length = n

theorem Champernowne.champPrefix_eq_map (b n : ℕ) : champPrefix b n = List.map (champDigit b) (List.range n)