From 1ab4ffb1a4798beb01d7b6f3325af343df660ca2 Mon Sep 17 00:00:00 2001 From: Vilin97 automation Date: Sat, 19 Sep 2026 03:13:57 -0700 Subject: [PATCH 1/2] feat: import Champernowne normality in every base --- LeanPool.lean | 9 + LeanPool/Champernowne.lean | 20 + LeanPool/Champernowne/Asymptotics.lean | 268 +++++++++++ LeanPool/Champernowne/Count.lean | 198 +++++++++ LeanPool/Champernowne/CountExtras.lean | 591 +++++++++++++++++++++++++ LeanPool/Champernowne/Defs.lean | 75 ++++ LeanPool/Champernowne/DigitCount.lean | 523 ++++++++++++++++++++++ LeanPool/Champernowne/Main.lean | 30 ++ LeanPool/Champernowne/Positions.lean | 212 +++++++++ LeanPool/Champernowne/Prefix.lean | 61 +++ LeanPool/projects.yml | 57 +++ 11 files changed, 2044 insertions(+) create mode 100644 LeanPool/Champernowne.lean create mode 100644 LeanPool/Champernowne/Asymptotics.lean create mode 100644 LeanPool/Champernowne/Count.lean create mode 100644 LeanPool/Champernowne/CountExtras.lean create mode 100644 LeanPool/Champernowne/Defs.lean create mode 100644 LeanPool/Champernowne/DigitCount.lean create mode 100644 LeanPool/Champernowne/Main.lean create mode 100644 LeanPool/Champernowne/Positions.lean create mode 100644 LeanPool/Champernowne/Prefix.lean diff --git a/LeanPool.lean b/LeanPool.lean index fb8c49ac85..1cd32419d8 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -358,6 +358,15 @@ import LeanPool.CencovPetz.Uniform import LeanPool.CencovPetz.UniformScalarConstant import LeanPool.CencovPetz.UniformScalarMultiple import LeanPool.CencovPetz.UniformSimplex +import LeanPool.Champernowne +import LeanPool.Champernowne.Asymptotics +import LeanPool.Champernowne.Count +import LeanPool.Champernowne.CountExtras +import LeanPool.Champernowne.Defs +import LeanPool.Champernowne.DigitCount +import LeanPool.Champernowne.Main +import LeanPool.Champernowne.Positions +import LeanPool.Champernowne.Prefix import LeanPool.ChannelCapacity import LeanPool.ChannelCapacity.Basic import LeanPool.ChannelCapacity.Capacity diff --git a/LeanPool/Champernowne.lean b/LeanPool/Champernowne.lean new file mode 100644 index 0000000000..675c8e3bc6 --- /dev/null +++ b/LeanPool/Champernowne.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2026 Arthur Champernowne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Champernowne +-/ +module + +public import LeanPool.Champernowne.Main +public import LeanPool.Champernowne.CountExtras + +/-! +# Champernowne normality in every base + +Source: url:https://github.com/OldMathematician/ChampernowneNormality +Authors: Arthur Champernowne +Status: verified +Main declarations: `Champernowne.champernowne_normal` +Tags: normal-numbers, digit-expansions, combinatorics-on-words, asymptotic-frequency +MSC: 11K16, 68R15 +-/ diff --git a/LeanPool/Champernowne/Asymptotics.lean b/LeanPool/Champernowne/Asymptotics.lean new file mode 100644 index 0000000000..47988a1111 --- /dev/null +++ b/LeanPool/Champernowne/Asymptotics.lean @@ -0,0 +1,268 @@ +/- +Copyright (c) 2026 Arthur Champernowne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Champernowne +-/ +module + +public import LeanPool.Champernowne.Positions +public import Mathlib.Analysis.Asymptotics.Lemmas +public import Mathlib.Analysis.SpecificLimits.Basic + +/-! +# 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⁻ᵏ`. +-/ + +@[expose] public section + +namespace Champernowne + +open Filter Asymptotics Topology + +/-- Digit length of the straddling number `champIndex b n + 1`. -/ +def champM (b n : ℕ) : ℕ := Nat.log b (champIndex b n + 1) + 1 + +theorem champM_pos (b n : ℕ) : 0 < champM b n := Nat.succ_pos _ + +theorem pow_champM_le (b n : ℕ) : + b ^ (champM b n - 1) ≤ champIndex b n + 1 := by + rw [champM, Nat.add_sub_cancel] + exact Nat.pow_log_le_self b (Nat.succ_ne_zero _) + +theorem le_pow_champM {b : ℕ} (hb : 1 < b) (n : ℕ) : + champIndex b n + 1 ≤ b ^ champM b n := + le_of_lt (Nat.lt_pow_succ_log_self hb _) + +/-- Length lower bound: `n` dominates the second-to-top cohort. -/ +theorem cohort_le_n {b : ℕ} (hb : 1 < b) (n : ℕ) : + (b - 1) * b ^ (champM b n - 2) * (champM b n - 1) ≤ n := by + rcases Nat.lt_or_ge (champM b n) 2 with h2 | h2 + · rw [show champM b n - 1 = 0 by omega, Nat.mul_zero] + exact Nat.zero_le n + · have hN1 := pow_champM_le b n + have hlen := length_champBlocks_champIndex_le b n + rw [length_champBlocks] at hlen + have hsub : Finset.Ico 1 (b ^ (champM b n - 1)) + ⊆ Finset.Ico 1 (champIndex b n + 1) := + Finset.Ico_subset_Ico_right hN1 + have hmono := Finset.sum_le_sum_of_subset + (f := fun k => (bigDigits b k).length) hsub + rw [sum_Ico_one_pow hb] at hmono + have hsingle : (∑ k ∈ Finset.Ico (b ^ (champM b n - 1 - 1)) + (b ^ (champM b n - 1)), (bigDigits b k).length) + ≤ ∑ m ∈ Finset.Icc 1 (champM b n - 1), + ∑ k ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), + (bigDigits b k).length := + Finset.single_le_sum + (f := fun m => ∑ k ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), + (bigDigits b k).length) + (fun _ _ => Nat.zero_le _) + (Finset.mem_Icc.mpr ⟨by omega, le_rfl⟩) + rw [sum_length_cohort hb (champM b n - 1) (by omega), + show champM b n - 1 - 1 = champM b n - 2 by omega] at hsingle + omega + +theorem tendsto_champIndex_atTop (b : ℕ) : + Tendsto (champIndex b) atTop atTop := by + rw [Filter.tendsto_atTop] + intro K + filter_upwards [Filter.eventually_ge_atTop ((champBlocks b K).length)] + with n hn + exact Nat.le_findGreatest (le_trans (le_length_champBlocks b K) hn) hn + +theorem tendsto_champM_atTop {b : ℕ} (hb : 1 < b) : + Tendsto (champM b) atTop atTop := by + rw [Filter.tendsto_atTop] + intro K + have h10 : Tendsto (fun n => champIndex b n + 1) atTop atTop := + tendsto_atTop_mono (fun n => Nat.le_succ (champIndex b n)) + (tendsto_champIndex_atTop b) + filter_upwards [h10.eventually_ge_atTop (b ^ K)] with n hn + have hn' : b ^ K ≤ champIndex b n + 1 := hn + have hlog := (Nat.le_log_iff_pow_le hb + (show champIndex b n + 1 ≠ 0 by omega)).mpr hn' + change K ≤ Nat.log b (champIndex b n + 1) + 1 + omega + +/-! ### 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 base_pow_count_le {b : ℕ} (hb : 1 < b) {w : List ℕ} + (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) : + ∀ᶠ n in atTop, b ^ w.length * countOccurrences w (champPrefix b n) + ≤ n + 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n := by + filter_upwards [(tendsto_champM_atTop hb).eventually_ge_atTop w.length] with n hn + exact base_pow_countOccurrences_champPrefix_le hb n (champM b n) hw hwne + (champM_pos b n) hn (pow_champM_le b n) (le_pow_champM hb n) + +theorem le_base_pow_count {b : ℕ} (hb : 1 < b) {w : List ℕ} + (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) : + ∀ᶠ n in atTop, n ≤ b ^ w.length * countOccurrences w (champPrefix b n) + + 7 * (w.length + 1) * b ^ w.length * b ^ champM b n := by + filter_upwards [(tendsto_champM_atTop hb).eventually_ge_atTop w.length] with n hn + exact le_base_pow_countOccurrences_champPrefix hb n (champM b n) hw hwne + (champM_pos b n) hn (pow_champM_le b n) (le_pow_champM hb n) + +/-- The error dominates its own budget: `E(n)·(b-1)(M−1) ≤ E'·n`. -/ +theorem 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 := by + rcases Nat.lt_or_ge (champM b n) 2 with h2 | h2 + · rw [show champM b n - 1 = 0 by omega] + simp + · have hD := cohort_le_n hb n + have hpow : b ^ champM b n = b ^ 2 * b ^ (champM b n - 2) := by + rw [← pow_add]; congr 1; omega + calc 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) + * ((b - 1) * b ^ (champM b n - 2) * (champM b n - 1)) := by + rw [hpow]; ring + _ ≤ (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ 2) * n := Nat.mul_le_mul_left _ hD + +/-- Subtraction-free form for `M ≥ 2`. -/ +theorem 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 := by + have hF := err_mul_le_pow hb n w + have h9 : (b - 1) * champM b n ≤ 2 * ((b - 1) * (champM b n - 1)) := by + calc (b - 1) * champM b n ≤ (b - 1) * (2 * (champM b n - 1)) := + Nat.mul_le_mul_left _ (by omega) + _ = 2 * ((b - 1) * (champM b n - 1)) := by ring + calc 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n * ((b - 1) * champM b n) + ≤ 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n + * (2 * ((b - 1) * (champM b n - 1))) := Nat.mul_le_mul_left _ h9 + _ = 2 * (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n + * ((b - 1) * (champM b n - 1))) := by ring + _ ≤ 2 * ((7 * (w.length + 1) * b ^ (2 * w.length) * b ^ 2) * n) := + Nat.mul_le_mul_left _ hF + _ = 2 * (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ 2) * n := by ring + +/-- The error sequence is negligible relative to `n`. -/ +theorem tendsto_err_div_pow {b : ℕ} (hb : 1 < b) (w : List ℕ) : + Tendsto (fun n => (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n : ℝ) / n) + atTop (𝓝 0) := by + have hbR : (1 : ℝ) ≤ (b : ℝ) - 1 := by + have : (2 : ℝ) ≤ b := by exact_mod_cast hb + linarith + have hden : Tendsto (fun n => ((b : ℝ) - 1) * (champM b n : ℝ)) + atTop atTop := + (tendsto_const_mul_atTop_of_pos (by linarith)).mpr + (tendsto_natCast_atTop_atTop.comp (tendsto_champM_atTop hb)) + have hg : Tendsto (fun n => + (2 * (7 * ((w.length : ℝ) + 1) * (b : ℝ) ^ (2 * w.length) * (b : ℝ) ^ 2)) + / (((b : ℝ) - 1) * (champM b n : ℝ))) atTop (𝓝 0) := + Filter.Tendsto.div_atTop tendsto_const_nhds hden + refine squeeze_zero' ?_ ?_ hg + · filter_upwards [Filter.eventually_ge_atTop 1] with n hn + have h0 : (0 : ℝ) < n := by exact_mod_cast hn + positivity + · filter_upwards [(tendsto_champM_atTop hb).eventually_ge_atTop 2, + Filter.eventually_ge_atTop 1] with n hM2 hn1 + have h0 : (0 : ℝ) < n := by exact_mod_cast hn1 + have hM0 : (0 : ℝ) < ((b : ℝ) - 1) * (champM b n : ℝ) := by + have hMpos : (0 : ℝ) < (champM b n : ℝ) := by + exact_mod_cast champM_pos b n + nlinarith + rw [div_le_div_iff₀ h0 hM0] + have := err_mul_le_pow' hb n w hM2 + have hcast2 : ((7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n + * ((b - 1) * champM b n) : ℕ) : ℝ) + = (7 * ((w.length : ℝ) + 1) * (b : ℝ) ^ (2 * w.length) * (b : ℝ) ^ champM b n) + * (((b : ℝ) - 1) * (champM b n : ℝ)) := by + have hb1 : ((b - 1 : ℕ) : ℝ) = (b : ℝ) - 1 := by + rw [Nat.cast_sub (by omega : 1 ≤ b), Nat.cast_one] + push_cast [hb1] + ring + have hcast3 : ((2 * (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ 2) * n : ℕ) : ℝ) + = 2 * (7 * ((w.length : ℝ) + 1) * (b : ℝ) ^ (2 * w.length) * (b : ℝ) ^ 2) * n := by + push_cast; ring + rw [← hcast2, ← hcast3] + exact_mod_cast this + +/-- `countOccurrences w (champPrefix b n) − +n/b^k = o(n)`. -/ +theorem 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[atTop] (fun n => (n : ℝ)) := by + have hbR : (0 : ℝ) < (b : ℝ) ^ w.length := by positivity + have hb1R : (1 : ℝ) ≤ (b : ℝ) ^ w.length := by + have : (1 : ℝ) ≤ (b : ℝ) := by exact_mod_cast le_of_lt hb + exact one_le_pow₀ this + have hEo : (fun n => (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n : ℝ)) + =o[atTop] (fun n => (n : ℝ)) := by + rw [Asymptotics.isLittleO_iff_tendsto'] + · exact tendsto_err_div_pow hb w + · filter_upwards [Filter.eventually_ge_atTop 1] with n hn h0 + have : (0 : ℝ) < n := by exact_mod_cast hn + exact absurd h0 (ne_of_gt this) + refine Asymptotics.IsBigO.trans_isLittleO ?_ hEo + rw [Asymptotics.isBigO_iff] + refine ⟨1, ?_⟩ + filter_upwards [base_pow_count_le hb hw hwne, le_base_pow_count hb hw hwne] + with n h1 h2 + -- Widen the lower transfer's error b^k·… to the upper's b^(2k)·… (ℕ level). + have h2' : n ≤ b ^ w.length * countOccurrences w (champPrefix b n) + + 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n := by + have hpow : b ^ w.length ≤ b ^ (2 * w.length) := + Nat.pow_le_pow_right (by omega) (by omega) + have hmul := Nat.mul_le_mul_right (b ^ champM b n) + (Nat.mul_le_mul_left (7 * (w.length + 1)) hpow) + omega + have e1 : (b : ℝ) ^ w.length * countOccurrences w (champPrefix b n) + ≤ n + 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n := by exact_mod_cast h1 + have e2 : (n : ℝ) ≤ (b : ℝ) ^ w.length * countOccurrences w (champPrefix b n) + + 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n := by exact_mod_cast h2' + have hEpos : (0 : ℝ) ≤ (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n : ℝ) := + by positivity + have key : |(b : ℝ) ^ w.length * countOccurrences w (champPrefix b n) - n| + ≤ (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n : ℝ) := by + rw [abs_le] + constructor + · linarith + · linarith + rw [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_of_nonneg hEpos, + show (countOccurrences w (champPrefix b n) : ℝ) - n / (b : ℝ) ^ w.length + = ((b : ℝ) ^ w.length * countOccurrences w (champPrefix b n) - n) / (b : ℝ) ^ w.length by + field_simp, + abs_div, abs_of_pos hbR] + calc |(b : ℝ) ^ w.length * countOccurrences w (champPrefix b n) - n| / (b : ℝ) ^ w.length + ≤ (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n : ℝ) / (b : ℝ) ^ w.length := by + exact div_le_div_of_nonneg_right key hbR.le + _ ≤ (7 * (w.length + 1) * b ^ (2 * w.length) * b ^ champM b n : ℝ) := by + rw [div_le_iff₀ hbR] + exact le_mul_of_one_le_right hEpos hb1R + +/-- Every nonempty block `w` (digits `< b`) +occurs in the base-`b` Champernowne stream with asymptotic frequency +`b⁻ᵏ`. -/ +theorem tendsto_countOccurrences_champPrefix_div {b : ℕ} (hb : 1 < b) {w : List ℕ} + (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) : + Tendsto (fun n => (countOccurrences w (champPrefix b n) : ℝ) / n) + atTop (𝓝 (((b : ℝ) ^ w.length)⁻¹)) := by + have hb0 : ((b : ℝ) ^ w.length) ≠ 0 := by positivity + have ho := countOccurrences_champPrefix_sub_isLittleO hb hw hwne + rw [Asymptotics.isLittleO_iff_tendsto' + (by + filter_upwards [Filter.eventually_ge_atTop 1] with n hn h0 + have : (0 : ℝ) < n := by exact_mod_cast hn + exact absurd h0 (ne_of_gt this))] at ho + have hsum := ho.add_const ((1 : ℝ) / (b : ℝ) ^ w.length) + rw [zero_add] at hsum + rw [← one_div] + refine Tendsto.congr' ?_ hsum + filter_upwards [Filter.eventually_ge_atTop 1] with n hn + have h0 : (0 : ℝ) < n := by exact_mod_cast hn + rw [one_div] + field_simp + ring + +end Champernowne diff --git a/LeanPool/Champernowne/Count.lean b/LeanPool/Champernowne/Count.lean new file mode 100644 index 0000000000..35c1c770be --- /dev/null +++ b/LeanPool/Champernowne/Count.lean @@ -0,0 +1,198 @@ +/- +Copyright (c) 2026 Arthur Champernowne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Champernowne +-/ +module + +public import LeanPool.Champernowne.Defs +public import Mathlib.Algebra.BigOperators.Intervals +public import Mathlib.Data.Finset.Powerset + +/-! +# Occurrence-counting inequalities + +This file gives the lower append bound, a characterization by starting positions, +and the `allWords` enumeration of length-`k` digit strings. Summing occurrences +over `allWords` bounds the number of windows, allowing upper frequency estimates +to be derived from lower ones by complement. + +The window convention is documented at `countOccurrences`. Statements assume +`w ≠ []` when the empty word needs to be excluded. Further append, take, drop, +and exact digit-counting results are in `LeanPool.Champernowne.CountExtras`. +-/ + +@[expose] public section + +namespace Champernowne + +theorem countOccurrences_cons (w l : List ℕ) (x : ℕ) : + countOccurrences w (x :: l) + = countOccurrences w l + (if w.isPrefixOf (x :: l) then 1 else 0) := by + simp [countOccurrences, List.countP_cons] + +theorem countOccurrences_nil' (w : List ℕ) : + countOccurrences w [] = if w.isPrefixOf [] then 1 else 0 := by + simp [countOccurrences] + +theorem countOccurrences_nil {w : List ℕ} (hw : w ≠ []) : + countOccurrences w [] = 0 := by + obtain ⟨y, ys, rfl⟩ := List.exists_cons_of_ne_nil hw + simp [countOccurrences, List.isPrefixOf] + +/-- Extending the list to the right preserves window hits. -/ +theorem isPrefixOf_append_of_isPrefixOf {w a : List ℕ} (b : List ℕ) + (h : w.isPrefixOf a) : w.isPrefixOf (a ++ b) := by + rw [List.isPrefixOf_iff_prefix] at h ⊢ + exact h.trans (List.prefix_append a b) + +/-! ### The append lower bound -/ + +/-- Lower bound: occurrences inside `a` and inside `b` survive in `a ++ b`. +Fails for `w = []` (window counts overlap at the seam). -/ +theorem add_countOccurrences_le_append {w : List ℕ} (hw : w ≠ []) + (a b : List ℕ) : + countOccurrences w a + countOccurrences w b + ≤ countOccurrences w (a ++ b) := by + induction a with + | nil => simp [countOccurrences_nil hw] + | cons x a' ih => + rw [List.cons_append, countOccurrences_cons, countOccurrences_cons] + have hmono : (if w.isPrefixOf (x :: a') then 1 else 0) + ≤ if w.isPrefixOf (x :: (a' ++ b)) then 1 else 0 := by + by_cases h : w.isPrefixOf (x :: a') + · have h2 : w.isPrefixOf (x :: (a' ++ b)) := by + rw [← List.cons_append] + exact isPrefixOf_append_of_isPrefixOf b h + simp [h, h2] + · simp [h] + omega + +/-! ### Occurrences in `champBlocks` -/ + +/-- Per-number occurrences survive in the stream. -/ +theorem sum_le_countOccurrences_champBlocks {b : ℕ} {w : List ℕ} + (hw : w ≠ []) (N : ℕ) : + ∑ n ∈ Finset.Ico 1 (N + 1), countOccurrences w (bigDigits b n) + ≤ countOccurrences w (champBlocks b N) := by + induction N with + | zero => simp [champBlocks, countOccurrences_nil hw] + | succ n ih => + rw [champBlocks_succ, Finset.sum_Ico_succ_top (by omega)] + calc (∑ k ∈ Finset.Ico 1 (n + 1), countOccurrences w (bigDigits b k)) + + countOccurrences w (bigDigits b (n + 1)) + ≤ countOccurrences w (champBlocks b n) + + countOccurrences w (bigDigits b (n + 1)) := + Nat.add_le_add_right ih _ + _ ≤ _ := add_countOccurrences_le_append hw _ _ + +/-! ### Position characterization -/ + +/-- `countOccurrences` counts window start positions. -/ +theorem countOccurrences_eq_card_filter_range (w l : List ℕ) : + countOccurrences w l + = ((Finset.range (l.length + 1)).filter + (fun j => w.isPrefixOf (l.drop j))).card := by + induction l with + | nil => + by_cases h : w.isPrefixOf [] + · simp [countOccurrences_nil', h] + · simp [countOccurrences_nil', h] + | cons x xs ih => + rw [List.length_cons, Finset.card_filter, Finset.sum_range_succ', + countOccurrences_cons, ih, Finset.card_filter] + simp only [List.drop_succ_cons, List.drop_zero] + +/-! ### Word enumeration and the window pigeonhole + +`allWords b k` enumerates all length-`k` digit strings over `{0, …, b−1}` +(leading zeros allowed) — the complement machinery that lets the upper +occurrence bound be *derived* from the lower one: a window matching no +`v ≠ w` must match `w`. -/ + +/-- All length-`k` digit strings over `{0, …, b−1}`, leading zeros allowed. -/ +def allWords (b : ℕ) : ℕ → Finset (List ℕ) + | 0 => {[]} + | k + 1 => (Finset.range b).biUnion fun d => (allWords b k).image (d :: ·) + +theorem mem_allWords {b k : ℕ} {l : List ℕ} : + l ∈ allWords b k ↔ l.length = k ∧ ∀ d ∈ l, d < b := by + induction k generalizing l with + | zero => cases l <;> simp [allWords] + | succ k ih => + simp only [allWords, Finset.mem_biUnion, Finset.mem_range, Finset.mem_image] + constructor + · rintro ⟨d, hd, v, hv, rfl⟩ + obtain ⟨hlen, hlt⟩ := ih.mp hv + refine ⟨by simp [hlen], ?_⟩ + intro e he + rcases List.mem_cons.mp he with rfl | he' + · exact hd + · exact hlt e he' + · rintro ⟨hlen, hlt⟩ + cases l with + | nil => simp at hlen + | cons d v => + exact ⟨d, hlt d (List.mem_cons_self ..), v, + ih.mpr ⟨by simpa using hlen, fun e he => hlt e (List.mem_cons_of_mem d he)⟩, + rfl⟩ + +theorem card_allWords (b k : ℕ) : (allWords b k).card = b ^ k := by + induction k with + | zero => simp [allWords] + | succ k ih => + have hdisj : ∀ d₁ ∈ Finset.range b, ∀ d₂ ∈ Finset.range b, d₁ ≠ d₂ → + Disjoint ((allWords b k).image (d₁ :: ·)) + ((allWords b k).image (d₂ :: ·)) := by + intro d₁ _ d₂ _ hne + rw [Finset.disjoint_left] + rintro l hl₁ hl₂ + obtain ⟨v₁, -, rfl⟩ := Finset.mem_image.mp hl₁ + obtain ⟨v₂, -, heq⟩ := Finset.mem_image.mp hl₂ + injection heq with h1 _ + exact hne h1.symm + calc (allWords b (k + 1)).card + = ∑ d ∈ Finset.range b, ((allWords b k).image (d :: ·)).card := + Finset.card_biUnion hdisj + _ = ∑ _d ∈ Finset.range b, (allWords b k).card := + Finset.sum_congr rfl fun d _ => + Finset.card_image_of_injective _ fun v₁ v₂ h => by injection h + _ = b ^ (k + 1) := by + rw [Finset.sum_const, Finset.card_range, smul_eq_mul, ih, pow_succ'] + +/-- Window pigeonhole: a window position matches at most one length-`k` +word, so over ALL length-`k` words the occurrence counts total at most the +number of window start positions. This single inequality replaces the +entire upper-bound counting chain. -/ +theorem sum_countOccurrences_allWords_le (b k : ℕ) (l : List ℕ) : + ∑ v ∈ allWords b k, countOccurrences v l ≤ l.length + 1 := by + have hdisj : ∀ v₁ ∈ allWords b k, ∀ v₂ ∈ allWords b k, v₁ ≠ v₂ → + Disjoint + ((Finset.range (l.length + 1)).filter (fun j => v₁.isPrefixOf (l.drop j))) + ((Finset.range (l.length + 1)).filter (fun j => v₂.isPrefixOf (l.drop j))) := by + intro v₁ h₁ v₂ h₂ hne + rw [Finset.disjoint_left] + rintro j hj₁ hj₂ + have hp₁ := List.isPrefixOf_iff_prefix.mp (Finset.mem_filter.mp hj₁).2 + have hp₂ := List.isPrefixOf_iff_prefix.mp (Finset.mem_filter.mp hj₂).2 + have hlen₁ := (mem_allWords.mp h₁).1 + have hlen₂ := (mem_allWords.mp h₂).1 + apply hne + calc v₁ = (l.drop j).take v₁.length := List.prefix_iff_eq_take.mp hp₁ + _ = (l.drop j).take v₂.length := by rw [hlen₁, hlen₂] + _ = v₂ := (List.prefix_iff_eq_take.mp hp₂).symm + calc ∑ v ∈ allWords b k, countOccurrences v l + = ∑ v ∈ allWords b k, + ((Finset.range (l.length + 1)).filter + (fun j => v.isPrefixOf (l.drop j))).card := + Finset.sum_congr rfl fun v _ => countOccurrences_eq_card_filter_range v l + _ = ((allWords b k).biUnion fun v => + (Finset.range (l.length + 1)).filter + (fun j => v.isPrefixOf (l.drop j))).card := + (Finset.card_biUnion hdisj).symm + _ ≤ (Finset.range (l.length + 1)).card := + Finset.card_le_card + (Finset.biUnion_subset.mpr fun v _ => Finset.filter_subset _ _) + _ = l.length + 1 := Finset.card_range _ + +end Champernowne diff --git a/LeanPool/Champernowne/CountExtras.lean b/LeanPool/Champernowne/CountExtras.lean new file mode 100644 index 0000000000..2b745beb75 --- /dev/null +++ b/LeanPool/Champernowne/CountExtras.lean @@ -0,0 +1,591 @@ +/- +Copyright (c) 2026 Arthur Champernowne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Champernowne +-/ +module + +public import LeanPool.Champernowne.DigitCount +public import Mathlib.Data.List.GetD + +/-! +# Exact digit counts and further occurrence-counting inequalities + +The append, take, drop, and flatten bounds extend the occurrence-counting API. +The exact periodic count and `digitEquiv` relate integer intervals to digit +strings. Exact counts distinguish the head position, where a positive integer +cannot start with zero, from interior positions; their sum gives a closed +formula for occurrences inside a complete cohort of equal-length numbers. + +These results are exported by the project entry module as reusable infrastructure. +The normality proof itself needs only the lower bounds in `DigitCount`. +-/ + +@[expose] public section + +namespace Champernowne + +/-- Sanity bridge to `List.count`: single-letter blocks are `List.count`. -/ +theorem countOccurrences_singleton (d : ℕ) (l : List ℕ) : + countOccurrences [d] l = l.count d := by + induction l with + | nil => simp [countOccurrences, List.isPrefixOf] + | cons x xs ih => + rw [countOccurrences_cons, ih, List.count_cons] + by_cases h : x = d + · subst h + simp [List.isPrefixOf] + · have h' : ¬d = x := fun hdx => h hdx.symm + simp [h, h', List.isPrefixOf] + +/-- A prefix short enough to fit inside `a` is a prefix of `a`. -/ +theorem prefix_of_prefix_append {α : Type*} {w a c : List α} + (h : w <+: a ++ c) (hl : w.length ≤ a.length) : w <+: a := by + obtain ⟨t, ht⟩ := h + have h1 : (a ++ c).take w.length = w := by + rw [← ht] + exact List.take_left .. + have h2 : w = a.take w.length := + h1.symm.trans (List.take_append_of_le_length hl) + rw [h2] + exact List.take_prefix _ _ + +theorem countOccurrences_le_cons (w l : List ℕ) (x : ℕ) : + countOccurrences w l ≤ countOccurrences w (x :: l) := by + rw [countOccurrences_cons] + omega + +/-- Append sandwich, upper bound: at most `min w.length a.length` +occurrences straddle the seam (they must start within `w.length − 1` +slots of the end of `a`, and there are only `a.length` interior start +slots). -/ +theorem countOccurrences_append_le_min (w a b : List ℕ) : + countOccurrences w (a ++ b) + ≤ countOccurrences w a + countOccurrences w b + + min w.length a.length := by + induction a with + | nil => + simp only [List.nil_append, List.length_nil, Nat.min_zero, Nat.add_zero] + exact Nat.le_add_left _ _ + | cons x a' ih => + rw [List.cons_append, countOccurrences_cons, countOccurrences_cons] + have hlc : (x :: a').length = a'.length + 1 := by simp + by_cases h : w.isPrefixOf (x :: (a' ++ b)) + · by_cases h' : w.isPrefixOf (x :: a') + · simp only [h, h'] + omega + · -- straddling window: `w` overhangs the end of `x :: a'` + have hlen : (x :: a').length < w.length := by + rcases Nat.lt_or_ge (x :: a').length w.length with hlt | hge + · exact hlt + · refine absurd ?_ h' + rw [List.isPrefixOf_iff_prefix] at h ⊢ + exact prefix_of_prefix_append + (by rwa [← List.cons_append] at h) hge + simp only [h, h', ite_true] + omega + · have h' : ¬ w.isPrefixOf (x :: a') := by + intro hc + apply h + rw [← List.cons_append] + exact isPrefixOf_append_of_isPrefixOf b hc + simp only [h, h'] + omega + +/-- The seam bound with the word length as an upper bound. -/ +theorem countOccurrences_append_le (w a b : List ℕ) : + countOccurrences w (a ++ b) + ≤ countOccurrences w a + countOccurrences w b + w.length := + (countOccurrences_append_le_min w a b).trans + (Nat.add_le_add_left (Nat.min_le_left _ _) _) + +theorem countOccurrences_le_append_left (w a b : List ℕ) : + countOccurrences w b ≤ countOccurrences w (a ++ b) := by + induction a with + | nil => simp + | cons x a' ih => + rw [List.cons_append] + exact ih.trans (countOccurrences_le_cons w _ x) + +/-- The whole-list window contributes to the count. -/ +theorem if_isPrefixOf_le_countOccurrences (w l : List ℕ) : + (if w.isPrefixOf l then 1 else 0) ≤ countOccurrences w l := by + rcases l with _ | ⟨x, xs⟩ + · rw [countOccurrences_nil'] + · rw [countOccurrences_cons] + omega + +theorem countOccurrences_le_append_right (w a b : List ℕ) : + countOccurrences w a ≤ countOccurrences w (a ++ b) := by + induction a with + | nil => + simp only [List.nil_append] + rw [countOccurrences_nil'] + by_cases hw0 : w.isPrefixOf [] + · have hwnil : w = [] := by + simpa [List.isPrefixOf_iff_prefix, List.prefix_nil] using hw0 + subst hwnil + have h := if_isPrefixOf_le_countOccurrences [] b + simpa [List.isPrefixOf_iff_prefix, List.nil_prefix, hw0] using h + · simp [hw0] + | cons x a' ih => + rw [List.cons_append, countOccurrences_cons, countOccurrences_cons] + have hmono : (if w.isPrefixOf (x :: a') then 1 else 0) + ≤ if w.isPrefixOf (x :: (a' ++ b)) then 1 else 0 := by + by_cases h : w.isPrefixOf (x :: a') + · have h2 : w.isPrefixOf (x :: (a' ++ b)) := by + rw [← List.cons_append] + exact isPrefixOf_append_of_isPrefixOf b h + simp [h, h2] + · simp [h] + omega + +theorem countOccurrences_take_le (w l : List ℕ) (n : ℕ) : + countOccurrences w (l.take n) ≤ countOccurrences w l := by + conv_rhs => rw [← List.take_append_drop n l] + exact countOccurrences_le_append_right .. + +theorem countOccurrences_drop_le (w l : List ℕ) (n : ℕ) : + countOccurrences w (l.drop n) ≤ countOccurrences w l := by + conv_rhs => rw [← List.take_append_drop n l] + exact countOccurrences_le_append_left .. + +/-- Cutting at `n` loses at most `w.length` (seam) occurrences. -/ +theorem countOccurrences_le_take_add_drop (w l : List ℕ) (n : ℕ) : + countOccurrences w l + ≤ countOccurrences w (l.take n) + countOccurrences w (l.drop n) + + w.length := by + conv_lhs => rw [← List.take_append_drop n l] + exact countOccurrences_append_le .. + +/-- Cutting at `n` never gains occurrences (for `w ≠ []`). -/ +theorem take_add_drop_countOccurrences_le {w : List ℕ} (hw : w ≠ []) + (l : List ℕ) (n : ℕ) : + countOccurrences w (l.take n) + countOccurrences w (l.drop n) + ≤ countOccurrences w l := by + conv_rhs => rw [← List.take_append_drop n l] + exact add_countOccurrences_le_append hw .. + +/-- Per-block occurrences survive flattening. -/ +theorem sum_countOccurrences_le_flatten {w : List ℕ} (hw : w ≠ []) + (L : List (List ℕ)) : + (L.map (countOccurrences w)).sum ≤ countOccurrences w L.flatten := by + induction L with + | nil => simp [countOccurrences_nil hw] + | cons l L' ih => + rw [List.flatten_cons, List.map_cons, List.sum_cons] + calc countOccurrences w l + (L'.map (countOccurrences w)).sum + ≤ countOccurrences w l + countOccurrences w L'.flatten := + Nat.add_le_add_left ih _ + _ ≤ countOccurrences w (l ++ L'.flatten) := + add_countOccurrences_le_append hw _ _ + +/-- No occurrences of `w` in a list shorter than `w`. -/ +theorem countOccurrences_eq_zero_of_length_lt {w l : List ℕ} + (h : l.length < w.length) : countOccurrences w l = 0 := by + rw [countOccurrences_eq_card_filter_range, Finset.card_eq_zero, + Finset.filter_eq_empty_iff] + intro j hj + rw [Finset.mem_range] at hj + intro hpre + have hle := (List.isPrefixOf_iff_prefix.mp hpre).length_le + rw [List.length_drop] at hle + omega + +/-! ### Exact interval ↔ digit-string counting + +Superseded on the main path by the lower-bound-only layer in +`DigitCount.lean`; see the module docstring above. -/ + +/-- Exact periodic counting: over an interval whose endpoints are multiples +of `p * q`, the value `n / p % q` hits a fixed `d < q` exactly `p` times +per period `p * q`. Only the lower bound `le_card_Ico_filter_div_mod` +(proved directly in `DigitCount.lean`) feeds `champernowne_normal`. -/ +theorem card_Ico_filter_div_mod {A B p q d : ℕ} (hp : 0 < p) (hq : 0 < q) + (hd : d < q) (hA : p * q ∣ A) (hB : p * q ∣ B) : + ((Finset.Ico A B).filter (fun n => n / p % q = d)).card + = (B / (p * q) - A / (p * q)) * p := by + have hpq : 0 < p * q := Nat.mul_pos hp hq + have hdpr : ∀ r < p, d * p + r < p * q := by + intro r hr + calc d * p + r < (d + 1) * p := by rw [Nat.succ_mul]; omega + _ ≤ q * p := Nat.mul_le_mul_right p (by omega) + _ = p * q := Nat.mul_comm q p + rw [show (B / (p * q) - A / (p * q)) * p + = ((Finset.Ico (A / (p * q)) (B / (p * q))) ×ˢ Finset.range p).card by + rw [Finset.card_product, Nat.card_Ico, Finset.card_range]] + apply Finset.card_nbij' (i := fun n => (n / (p * q), n % p)) + (j := fun x => x.1 * (p * q) + d * p + x.2) + · -- forward map lands in the box + intro n hn + simp only [Finset.coe_filter, Set.mem_ofPred_eq, Finset.mem_Ico] at hn + obtain ⟨⟨h1, h2⟩, _⟩ := hn + simp only [Finset.coe_product, Set.mem_prod, Finset.mem_coe, Finset.mem_Ico, + Finset.mem_range] + refine ⟨⟨Nat.div_le_div_right h1, ?_⟩, Nat.mod_lt n hp⟩ + rw [Nat.div_lt_iff_lt_mul hpq, Nat.div_mul_cancel hB] + exact h2 + · -- inverse map lands in the filtered interval + rintro ⟨h, r⟩ hx + simp only [Finset.coe_product, Set.mem_prod, Finset.mem_coe, Finset.mem_Ico, + Finset.mem_range] at hx + obtain ⟨⟨hh1, hh2⟩, hr⟩ := hx + simp only [Finset.coe_filter, Set.mem_ofPred_eq, Finset.mem_Ico] + refine ⟨⟨?_, ?_⟩, ?_⟩ + · calc A = A / (p * q) * (p * q) := (Nat.div_mul_cancel hA).symm + _ ≤ h * (p * q) := Nat.mul_le_mul_right _ hh1 + _ ≤ h * (p * q) + d * p + r := by + exact le_add_right (le_add_right le_rfl) + · calc h * (p * q) + d * p + r + = h * (p * q) + (d * p + r) := by rw [Nat.add_assoc] + _ < h * (p * q) + p * q := Nat.add_lt_add_left (hdpr r hr) _ + _ = (h + 1) * (p * q) := by rw [Nat.succ_mul] + _ ≤ B / (p * q) * (p * q) := Nat.mul_le_mul_right _ (by omega) + _ = B := Nat.div_mul_cancel hB + · have hrew : h * (p * q) + d * p + r = r + p * (q * h + d) := by ring + rw [hrew, Nat.add_mul_div_left _ _ hp, Nat.div_eq_of_lt hr, Nat.zero_add, + Nat.mul_add_mod, Nat.mod_eq_of_lt hd] + · -- left inverse on the filtered interval + intro n hn + simp only [Finset.coe_filter, Set.mem_ofPred_eq, Finset.mem_Ico] at hn + obtain ⟨-, hd'⟩ := hn + change n / (p * q) * (p * q) + d * p + n % p = n + rw [← hd'] + calc n / (p * q) * (p * q) + n / p % q * p + n % p + = (q * (n / p / q) + n / p % q) * p + n % p := by + rw [← Nat.div_div_eq_div_mul]; ring + _ = n / p * p + n % p := by rw [Nat.div_add_mod] + _ = n := by rw [Nat.mul_comm]; exact Nat.div_add_mod n p + · -- right inverse on the box + rintro ⟨h, r⟩ hx + simp only [Finset.coe_product, Set.mem_prod, Finset.mem_coe, Finset.mem_Ico, + Finset.mem_range] at hx + obtain ⟨-, hr⟩ := hx + have h1 : (h * (p * q) + d * p + r) / (p * q) = h := by + have hrew : h * (p * q) + d * p + r = d * p + r + (p * q) * h := by ring + rw [hrew, Nat.add_mul_div_left _ _ hpq, Nat.div_eq_of_lt (hdpr r hr), + Nat.zero_add] + have h2 : (h * (p * q) + d * p + r) % p = r := by + have hrew : h * (p * q) + d * p + r = p * (h * q + d) + r := by ring + rw [hrew, Nat.mul_add_mod, Nat.mod_eq_of_lt hr] + exact Prod.ext h1 h2 + +/-- Every digit of a base-`b` expansion is `< b`. -/ +theorem lt_of_mem_bigDigits {b n d : ℕ} (hb : 1 < b) + (hd : d ∈ bigDigits b n) : d < b := + Nat.digits_lt_base hb (List.mem_reverse.mp hd) + +/-- The leading digit of a nonzero number is nonzero. -/ +theorem head_bigDigits_ne_zero {b n : ℕ} (hn : n ≠ 0) : + (bigDigits b n).head? ≠ some 0 := by + have hnil : Nat.digits b n ≠ [] := Nat.digits_ne_nil_iff_ne_zero.mpr hn + change (Nat.digits b n).reverse.head? ≠ some 0 + rw [← List.getLast?_eq_head?_reverse, List.getLast?_eq_getLast_of_ne_nil hnil] + simpa using Nat.getLast_digit_ne_zero b hn + +/-- Round-trip 1: reading the digits of `n` back yields `n`. +Together with the converse, this gives `digitEquiv`. -/ +theorem ofDigits_reverse_bigDigits (b n : ℕ) : + Nat.ofDigits b (bigDigits b n).reverse = n := by + simp [bigDigits, Nat.ofDigits_digits] + +/-- Little-endian form of round-trip 2. -/ +theorem digits_ofDigits_reverse {b : ℕ} (hb : 1 < b) {l : List ℕ} + (hlt : ∀ d ∈ l, d < b) (hhead : l.head? ≠ some 0) : + Nat.digits b (Nat.ofDigits b l.reverse) = l.reverse := by + refine Nat.digits_ofDigits b hb l.reverse + (fun d hd => hlt d (List.mem_reverse.mp hd)) ?_ + intro h hgl0 + apply hhead + have h? : l.reverse.getLast? = l.head? := by + rw [List.getLast?_eq_head?_reverse, List.reverse_reverse] + rw [← h?, List.getLast?_eq_getLast_of_ne_nil h, hgl0] + +/-- Round-trip 2: a digit string with nonzero head is the digit expansion of +the number it denotes. (Also holds for `l = []`.) -/ +theorem bigDigits_ofDigits_reverse {b : ℕ} (hb : 1 < b) {l : List ℕ} + (hlt : ∀ d ∈ l, d < b) (hhead : l.head? ≠ some 0) : + bigDigits b (Nat.ofDigits b l.reverse) = l := by + simp only [bigDigits, digits_ofDigits_reverse hb hlt hhead, + List.reverse_reverse] + +/-- A length-`m` digit string with nonzero head denotes an `m`-digit number. -/ +theorem ofDigits_reverse_mem_Ico {b m : ℕ} (hb : 1 < b) (hm : 0 < m) + {l : List ℕ} (hlen : l.length = m) (hlt : ∀ d ∈ l, d < b) + (hhead : l.head? ≠ some 0) : + Nat.ofDigits b l.reverse ∈ Finset.Ico (b ^ (m - 1)) (b ^ m) := by + have hlength : (Nat.digits b (Nat.ofDigits b l.reverse)).length = m := by + rw [digits_ofDigits_reverse hb hlt hhead, List.length_reverse, hlen] + rw [Finset.mem_Ico] + exact ⟨(Nat.lt_digits_length_iff hb _).mp (by omega), + (Nat.digits_length_le_iff hb _).mp (by omega)⟩ + +/-- Big-endian digit extraction: position `j` of an `m`-digit number `n` is +`n / b^(m-1-j) % b`. -/ +theorem getElemOption_bigDigits {b m n : ℕ} (hb : 1 < b) + (hlen : (bigDigits b n).length = m) {j : ℕ} (hj : j < m) : + (bigDigits b n)[j]? = some (n / b ^ (m - 1 - j) % b) := by + have hlen' : (Nat.digits b n).length = m := by + simpa [bigDigits] using hlen + change (Nat.digits b n).reverse[j]? = _ + rw [List.getElem?_reverse (by omega), hlen', + List.getElem?_eq_getElem (by omega)] + have hgd := Nat.getD_digits n (m - 1 - j) (show 2 ≤ b from hb) + rw [List.getD_eq_getElem _ _ (by omega)] at hgd + exact congrArg some hgd + +/-- `m`-digit numbers ≃ length-`m` digit strings with nonzero head. +Forward map `bigDigits b`; inverse `Nat.ofDigits b ∘ List.reverse`. +The normality proof uses only lower-bound cardinality consequences. -/ +def digitEquiv {b : ℕ} (hb : 1 < b) (m : ℕ) (hm : 0 < m) : + Finset.Ico (b ^ (m - 1)) (b ^ m) ≃ + {l : List ℕ // l.length = m ∧ (∀ d ∈ l, d < b) ∧ l.head? ≠ some 0} where + toFun n := + have hn := Finset.mem_Ico.mp n.2 + ⟨bigDigits b n, length_bigDigits_eq hb hn.1 hn.2, + fun _ hd => lt_of_mem_bigDigits hb hd, + head_bigDigits_ne_zero (by + have hP : 0 < b ^ (m - 1) := pow_pos (by omega) _ + have h1 := hn.1 + omega)⟩ + invFun l := ⟨Nat.ofDigits b l.1.reverse, + ofDigits_reverse_mem_Ico hb hm l.2.1 l.2.2.1 l.2.2.2⟩ + left_inv n := Subtype.ext (ofDigits_reverse_bigDigits b n) + right_inv l := Subtype.ext (bigDigits_ofDigits_reverse hb l.2.2.1 l.2.2.2) + +/-- Interior positions: block `w` occurs at position `0 < j` in exactly +`(b-1)·b^(m - w.length - 1)` of the `m`-digit numbers, independently of +`j` and of `w` itself. -/ +theorem card_blockAt {b : ℕ} (hb : 1 < b) (m j : ℕ) {w : List ℕ} + (hw : ∀ d ∈ w, d < b) (hj : 0 < j) (hjk : j + w.length ≤ m) : + ((Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => ((bigDigits b n).drop j).take w.length = w)).card + = (b - 1) * b ^ (m - w.length - 1) := by + have hD : Nat.ofDigits b w.reverse < b ^ w.length := by + have h := Nat.ofDigits_lt_base_pow_length hb + (fun d hd => hw d (List.mem_reverse.mp hd)) + rwa [List.length_reverse] at h + have hcongr : (Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => ((bigDigits b n).drop j).take w.length = w) + = (Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => n / b ^ (m - j - w.length) % b ^ w.length + = Nat.ofDigits b w.reverse) := by + apply Finset.filter_congr + intro n hn + rw [Finset.mem_Ico] at hn + exact block_eq_iff hb (length_bigDigits_eq hb hn.1 hn.2) hw hjk + have hpq : b ^ (m - j - w.length) * b ^ w.length = b ^ (m - j) := by + rw [← pow_add]; congr 1; omega + rw [hcongr, card_Ico_filter_div_mod (pow_pos (by omega) _) + (pow_pos (by omega) _) hD (hpq ▸ pow_dvd_pow b (by omega)) + (hpq ▸ pow_dvd_pow b (by omega)), hpq, + Nat.pow_div (by omega) (by omega), Nat.pow_div (by omega) (by omega)] + have h1 : b ^ (m - (m - j)) = b * b ^ (m - 1 - (m - j)) := by + rw [← pow_succ']; congr 1; omega + have h2 : b ^ (m - 1 - (m - j)) * b ^ (m - j - w.length) + = b ^ (m - w.length - 1) := by + rw [← pow_add]; congr 1; omega + have hbr : (b - 1) * b ^ (m - 1 - (m - j)) + b ^ (m - 1 - (m - j)) + = b * b ^ (m - 1 - (m - j)) := by + have hb1 : b - 1 + 1 = b := by omega + calc (b - 1) * b ^ (m - 1 - (m - j)) + b ^ (m - 1 - (m - j)) + = (b - 1 + 1) * b ^ (m - 1 - (m - j)) := by ring + _ = b * b ^ (m - 1 - (m - j)) := by rw [hb1] + rw [h1, show b * b ^ (m - 1 - (m - j)) - b ^ (m - 1 - (m - j)) + = (b - 1) * b ^ (m - 1 - (m - j)) by omega, + Nat.mul_assoc, h2] + +/-- Head position: a block with nonzero head occurs at position `0` in +exactly `b^(m - w.length)` of the `m`-digit numbers. -/ +theorem card_blockAt_head {b : ℕ} (hb : 1 < b) (m : ℕ) {w : List ℕ} + (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) (hw0 : w.head? ≠ some 0) + (hk : w.length ≤ m) : + ((Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => ((bigDigits b n).drop 0).take w.length = w)).card + = b ^ (m - w.length) := by + have hkpos : 0 < w.length := List.length_pos_of_ne_nil hwne + have hmem := ofDigits_reverse_mem_Ico hb hkpos rfl hw hw0 + rw [Finset.mem_Ico] at hmem + have hP : 0 < b ^ (m - w.length) := pow_pos (by omega) _ + have hbm : b ^ w.length * b ^ (m - w.length) = b ^ m := by + rw [← pow_add]; congr 1; omega + have hbm1 : b ^ (w.length - 1) * b ^ (m - w.length) = b ^ (m - 1) := by + rw [← pow_add]; congr 1; omega + have hset : (Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => ((bigDigits b n).drop 0).take w.length = w) + = Finset.Ico (Nat.ofDigits b w.reverse * b ^ (m - w.length)) + ((Nat.ofDigits b w.reverse + 1) * b ^ (m - w.length)) := by + ext n + rw [Finset.mem_filter, Finset.mem_Ico, Finset.mem_Ico] + constructor + · rintro ⟨⟨h1, h2⟩, hblk⟩ + rw [block_eq_iff hb (length_bigDigits_eq hb h1 h2) hw (by omega), + show m - 0 - w.length = m - w.length from rfl] at hblk + have hdiv : n / b ^ (m - w.length) < b ^ w.length := by + rw [Nat.div_lt_iff_lt_mul hP] + omega + rw [Nat.mod_eq_of_lt hdiv] at hblk + constructor + · rw [← hblk] + exact (Nat.le_div_iff_mul_le hP).mp le_rfl + · rw [← hblk] + exact (Nat.div_lt_iff_lt_mul hP).mp (by omega) + · rintro ⟨hlo, hhi⟩ + have hmem1 : b ^ (m - 1) ≤ n := by + calc b ^ (m - 1) = b ^ (w.length - 1) * b ^ (m - w.length) := + hbm1.symm + _ ≤ Nat.ofDigits b w.reverse * b ^ (m - w.length) := + Nat.mul_le_mul_right _ hmem.1 + _ ≤ n := hlo + have hmem2 : n < b ^ m := by + calc n < (Nat.ofDigits b w.reverse + 1) * b ^ (m - w.length) := hhi + _ ≤ b ^ w.length * b ^ (m - w.length) := + Nat.mul_le_mul_right _ (by omega) + _ = b ^ m := hbm + have hdiv : n / b ^ (m - w.length) = Nat.ofDigits b w.reverse := by + have hlow := (Nat.le_div_iff_mul_le hP).mpr hlo + have hhigh := (Nat.div_lt_iff_lt_mul hP).mpr hhi + omega + refine ⟨⟨hmem1, hmem2⟩, ?_⟩ + rw [block_eq_iff hb (length_bigDigits_eq hb hmem1 hmem2) hw (by omega), + show m - 0 - w.length = m - w.length from rfl, hdiv, + Nat.mod_eq_of_lt (by omega)] + rw [hset, Nat.card_Ico, Nat.succ_mul] + omega + +/-- Past the end: no window of length `w.length` starts after `m - w.length`. -/ +theorem card_blockAt_past_end {b : ℕ} (hb : 1 < b) (m j : ℕ) {w : List ℕ} + (hwne : w ≠ []) (hj : m < j + w.length) : + ((Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => ((bigDigits b n).drop j).take w.length = w)).card = 0 := by + rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff] + intro n hn + rw [Finset.mem_Ico] at hn + have hlen := length_bigDigits_eq hb hn.1 hn.2 + intro heq + have hlw := congrArg List.length heq + rw [List.length_take, List.length_drop, hlen] at hlw + have hkpos := List.length_pos_of_ne_nil hwne + omega + +/-- Head position, leading zero: a block with head `0` never occurs at +position `0` of an `m`-digit number. -/ +theorem card_blockAt_head_zero {b : ℕ} (hb : 1 < b) (m : ℕ) {w : List ℕ} + (hw : ∀ d ∈ w, d < b) (hw0 : w.head? = some 0) (hk : w.length ≤ m) : + ((Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => ((bigDigits b n).drop 0).take w.length = w)).card = 0 := by + rcases w with _ | ⟨d, w'⟩ + · simp at hw0 + · simp only [List.head?_cons, Option.some_inj] at hw0 + subst hw0 + have hlc : (0 :: w').length = w'.length + 1 := rfl + have hD : Nat.ofDigits b (0 :: w').reverse < b ^ w'.length := by + rw [List.reverse_cons, Nat.ofDigits_append] + have h := Nat.ofDigits_lt_base_pow_length hb + (fun d hd => hw d (List.mem_cons_of_mem _ (List.mem_reverse.mp hd))) + rw [List.length_reverse] at h + simpa [Nat.ofDigits] using h + rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff] + intro n hn + rw [Finset.mem_Ico] at hn + rw [block_eq_iff hb (length_bigDigits_eq hb hn.1 hn.2) hw (by omega)] + intro hcontra + have hP : 0 < b ^ (m - 0 - (0 :: w').length) := pow_pos (by omega) _ + have hup : b ^ (0 :: w').length * b ^ (m - 0 - (0 :: w').length) + = b ^ m := by + rw [← pow_add]; congr 1 + simp only [List.length_cons] + omega + have hdiv : n / b ^ (m - 0 - (0 :: w').length) + < b ^ (0 :: w').length := by + rw [Nat.div_lt_iff_lt_mul hP] + omega + have hlo1 : b ^ ((0 :: w').length - 1) * b ^ (m - 0 - (0 :: w').length) + = b ^ (m - 1) := by + rw [← pow_add]; congr 1 + simp only [List.length_cons] + omega + have hdivlo : b ^ ((0 :: w').length - 1) + ≤ n / b ^ (m - 0 - (0 :: w').length) := by + rw [Nat.le_div_iff_mul_le hP] + omega + rw [Nat.mod_eq_of_lt hdiv] at hcontra + have hlen1 : (0 :: w').length - 1 = w'.length := by + omega + rw [hlen1] at hdivlo + omega + +/-- Split a cohort occurrence count into its head contribution and interior windows. -/ +theorem sum_countOccurrences_cohort_eq_head {b : ℕ} (hb : 1 < b) (m : ℕ) + {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) (hk : w.length ≤ m) : + ∑ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), countOccurrences w (bigDigits b n) + = ((Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => ((bigDigits b n).drop 0).take w.length = w)).card + + (m - w.length) * ((b - 1) * b ^ (m - w.length - 1)) := by + have hstep : ∀ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), + countOccurrences w (bigDigits b n) + = ∑ j ∈ Finset.range (m + 1), + if ((bigDigits b n).drop j).take w.length = w then 1 else 0 := by + intro n hn + rw [Finset.mem_Ico] at hn + have hpred : ∀ j ∈ Finset.range (m + 1), + (w.isPrefixOf ((bigDigits b n).drop j) = true) + ↔ ((bigDigits b n).drop j).take w.length = w := fun j _ => by + rw [List.isPrefixOf_iff_prefix, List.prefix_iff_eq_take, eq_comm] + rw [countOccurrences_eq_card_filter_range, + length_bigDigits_eq hb hn.1 hn.2, Finset.filter_congr hpred, + Finset.card_filter] + rw [Finset.sum_congr rfl hstep, Finset.sum_comm] + have hswap : ∀ j ∈ Finset.range (m + 1), + (∑ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), + if ((bigDigits b n).drop j).take w.length = w then 1 else 0) + = ((Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => ((bigDigits b n).drop j).take w.length = w)).card := by + intro j _ + rw [Finset.card_filter] + rw [Finset.sum_congr rfl hswap, Finset.range_eq_Ico, + ← Finset.sum_Ico_consecutive _ (Nat.zero_le (m - w.length + 1)) + (by omega : m - w.length + 1 ≤ m + 1)] + have htail : ∑ j ∈ Finset.Ico (m - w.length + 1) (m + 1), + ((Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => ((bigDigits b n).drop j).take w.length = w)).card = 0 := by + refine Finset.sum_eq_zero fun j hj => ?_ + rw [Finset.mem_Ico] at hj + exact card_blockAt_past_end hb m j hwne (by omega) + rw [htail, Nat.add_zero, ← Finset.range_eq_Ico, Finset.sum_range_succ'] + have hint : ∀ i ∈ Finset.range (m - w.length), + ((Finset.Ico (b ^ (m - 1)) (b ^ m)).filter + (fun n => ((bigDigits b n).drop (i + 1)).take w.length = w)).card + = (b - 1) * b ^ (m - w.length - 1) := by + intro i hi + rw [Finset.mem_range] at hi + exact card_blockAt hb m (i + 1) hw (Nat.succ_pos i) (by omega) + rw [Finset.sum_congr rfl hint, Finset.sum_const, Finset.card_range, + smul_eq_mul] + exact Nat.add_comm _ _ + +/-- Block `w` with nonzero head occurs +`b^(m-k) + (m-k)·(b-1)·b^(m-k-1)` times inside the digit strings of all +`m`-digit numbers (`k := w.length`). -/ +theorem sum_countOccurrences_cohort {b : ℕ} (hb : 1 < b) (m : ℕ) + {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) + (hw0 : w.head? ≠ some 0) (hk : w.length ≤ m) : + ∑ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), + countOccurrences w (bigDigits b n) + = b ^ (m - w.length) + + (m - w.length) * ((b - 1) * b ^ (m - w.length - 1)) := by + rw [sum_countOccurrences_cohort_eq_head hb m hw hwne hk, + card_blockAt_head hb m hw hwne hw0 hk] + +/-- Block `w` with head `0` occurs `(m-k)·(b-1)·b^(m-k-1)` times inside the +digit strings of all `m`-digit numbers. -/ +theorem sum_countOccurrences_cohort_zero {b : ℕ} (hb : 1 < b) (m : ℕ) + {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hwne : w ≠ []) + (hw0 : w.head? = some 0) (hk : w.length ≤ m) : + ∑ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), + countOccurrences w (bigDigits b n) + = (m - w.length) * ((b - 1) * b ^ (m - w.length - 1)) := by + rw [sum_countOccurrences_cohort_eq_head hb m hw hwne hk, + card_blockAt_head_zero hb m hw hw0 hk, Nat.zero_add] + +end Champernowne diff --git a/LeanPool/Champernowne/Defs.lean b/LeanPool/Champernowne/Defs.lean new file mode 100644 index 0000000000..a1487606e6 --- /dev/null +++ b/LeanPool/Champernowne/Defs.lean @@ -0,0 +1,75 @@ +/- +Copyright (c) 2026 Arthur Champernowne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Champernowne +-/ +module + +public import Mathlib.Data.Nat.Digits.Defs +public import Mathlib.Data.List.Basic +public import Mathlib.Topology.MetricSpace.Pseudo.Defs + +/-! +# 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`. +-/ + +@[expose] public section + +namespace Champernowne + +/-- Big-endian digits of `n` in base `b`. -/ +def bigDigits (b n : ℕ) : List ℕ := (Nat.digits b n).reverse + +/-- First `N` blocks of the base-`b` Champernowne sequence: digits of 1..N. -/ +def champBlocks (b N : ℕ) : List ℕ := + ((List.range N).map fun n => bigDigits b (n + 1)).flatten + +theorem champBlocks_succ (b N : ℕ) : + champBlocks b (N + 1) = champBlocks b N ++ bigDigits b (N + 1) := by + simp [champBlocks, List.range_succ] + +theorem le_length_champBlocks (b N : ℕ) : N ≤ (champBlocks b N).length := by + induction N with + | zero => simp [champBlocks] + | succ n ih => + rw [champBlocks_succ, List.length_append] + have hpos : 0 < (bigDigits b (n + 1)).length := by + rw [bigDigits, List.length_reverse] + exact List.length_pos_of_ne_nil + (Nat.digits_ne_nil_iff_ne_zero.mpr (Nat.succ_ne_zero n)) + omega + +/-- The `i`-th digit (0-indexed) of the base-`b` Champernowne sequence. -/ +def champDigit (b i : ℕ) : ℕ := + (champBlocks b (i + 1))[i]'(lt_of_lt_of_le (Nat.lt_succ_self i) + (le_length_champBlocks b (i + 1))) + +/-- 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 ≠ []`. -/ +def countOccurrences (w l : List ℕ) : ℕ := + l.tails.countP (w.isPrefixOf ·) + +/-- Normality of a digit sequence in base `b`: every block of length `k` +(entries `< b`, leading zeros allowed) has asymptotic frequency `b⁻ᵏ`. -/ +def IsNormalSequence (b : ℕ) (s : ℕ → ℕ) : Prop := + ∀ w : List ℕ, w ≠ [] → (∀ d ∈ w, d < b) → + Filter.Tendsto + (fun n => (countOccurrences w ((List.range n).map s) : ℝ) / n) + Filter.atTop (nhds ((b : ℝ) ^ w.length)⁻¹) + +end Champernowne diff --git a/LeanPool/Champernowne/DigitCount.lean b/LeanPool/Champernowne/DigitCount.lean new file mode 100644 index 0000000000..3bf5c2c9e2 --- /dev/null +++ b/LeanPool/Champernowne/DigitCount.lean @@ -0,0 +1,523 @@ +/- +Copyright (c) 2026 Arthur Champernowne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Champernowne +-/ +module + +public import LeanPool.Champernowne.Count +public import Mathlib.Data.Nat.Digits.Lemmas +public import Mathlib.Algebra.Order.BigOperators.Group.Finset + +/-! +# 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`. +-/ + +@[expose] public section + +namespace Champernowne + +/-! ### Generic counting and rounding lemmas (no base) -/ + +/-- 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 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 + ≤ ((Finset.Ico A (A + t)).filter (fun n => n / p % q = d)).card := by + have hpq : 0 < p * q := Nat.mul_pos hp hq + have hdpr : ∀ r < p, d * p + r < p * q := by + intro r hr + calc d * p + r < (d + 1) * p := by rw [Nat.succ_mul]; omega + _ ≤ q * p := Nat.mul_le_mul_right p (by omega) + _ = p * q := Nat.mul_comm q p + rw [show t / (p * q) * p + = (Finset.range (t / (p * q)) ×ˢ Finset.range p).card by + rw [Finset.card_product, Finset.card_range, Finset.card_range]] + apply Finset.card_le_card_of_injOn + (fun x => A + (x.1 * (p * q) + d * p + x.2)) + · -- the map lands in the filtered interval + rintro ⟨h, r⟩ hx + simp only [Finset.coe_product, Set.mem_prod, Finset.mem_coe, + Finset.mem_range] at hx + obtain ⟨hh, hr⟩ := hx + have hlt : h * (p * q) + d * p + r < t := + calc h * (p * q) + d * p + r + < h * (p * q) + p * q := by have := hdpr r hr; omega + _ = (h + 1) * (p * q) := by ring + _ ≤ t / (p * q) * (p * q) := Nat.mul_le_mul_right _ (by omega) + _ ≤ t := Nat.div_mul_le_self t (p * q) + simp only [Finset.coe_filter, Set.mem_ofPred_eq, Finset.mem_Ico] + refine ⟨⟨Nat.le_add_right _ _, by omega⟩, ?_⟩ + obtain ⟨a, rfl⟩ := hA + have hrew : p * q * a + (h * (p * q) + d * p + r) + = r + p * (d + q * (a + h)) := by ring + rw [hrew, Nat.add_mul_div_left _ _ hp, Nat.div_eq_of_lt hr, Nat.zero_add, + Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hd] + · -- injectivity: extract `h` and `r` back out by div/mod + have hext : ∀ h r, r < p → + (h * (p * q) + d * p + r) / (p * q) = h + ∧ (h * (p * q) + d * p + r) % p = r := by + intro h r hr + constructor + · have hrew : h * (p * q) + d * p + r = d * p + r + (p * q) * h := by + ring + rw [hrew, Nat.add_mul_div_left _ _ hpq, Nat.div_eq_of_lt (hdpr r hr), + Nat.zero_add] + · have hrew : h * (p * q) + d * p + r = p * (h * q + d) + r := by ring + rw [hrew, Nat.mul_add_mod, Nat.mod_eq_of_lt hr] + rintro ⟨h₁, r₁⟩ hx₁ ⟨h₂, r₂⟩ hx₂ heq + simp only [Finset.coe_product, Set.mem_prod, Finset.mem_coe, + Finset.mem_range] at hx₁ hx₂ + have hcancel : h₁ * (p * q) + d * p + r₁ = h₂ * (p * q) + d * p + r₂ := + Nat.add_left_cancel heq + have hh : h₁ = h₂ := by + rw [← (hext h₁ r₁ hx₁.2).1, ← (hext h₂ r₂ hx₂.2).1, hcancel] + have hr : r₁ = r₂ := by + rw [← (hext h₁ r₁ hx₁.2).2, ← (hext h₂ r₂ hx₂.2).2, hcancel] + exact Prod.ext hh hr + +/-- Rounding compatibility: `t/q ≤ t/(p·q)·p + p`. -/ +theorem div_le_div_mul_add (t p q : ℕ) (hp : 0 < p) (hq : 0 < q) : + t / q ≤ t / (p * q) * p + p := by + have hpq : 0 < p * q := Nat.mul_pos hp hq + have e := Nat.div_add_mod t (p * q) + have hm : t % (p * q) < p * q := Nat.mod_lt t hpq + have key : t < (t / (p * q) * p + p) * q := by + have h1 : t < p * q * (t / (p * q)) + p * q := by omega + calc t < p * q * (t / (p * q)) + p * q := h1 + _ = (t / (p * q) * p + p) * q := by ring + exact Nat.le_of_lt_succ (Nat.lt_succ_of_lt + ((Nat.div_lt_iff_lt_mul hq).mpr key)) + +/-- `∑_{i simp + | succ K ih => + rw [Finset.sum_range_succ, pow_succ] + have h2 : b ^ K * 2 ≤ b ^ K * b := Nat.mul_le_mul_left _ hb + omega + +/-! ### `bigDigits` API -/ + +/-- A number in `[b^(m-1), b^m)` has exactly `m` digits. -/ +theorem length_bigDigits_eq {b m n : ℕ} (hb : 1 < b) + (h1 : b ^ (m - 1) ≤ n) (h2 : n < b ^ m) : + (bigDigits b n).length = m := by + have hle : (Nat.digits b n).length ≤ m := + (Nat.digits_length_le_iff hb n).mpr h2 + have hlt : m - 1 < (Nat.digits b n).length := + (Nat.lt_digits_length_iff hb n).mpr h1 + simp only [bigDigits, List.length_reverse] + omega + +/-! ### Cardinalities -/ + +/-- There are `(b-1) * b^(m-1)` numbers with exactly `m` digits. -/ +theorem card_mDigit {b : ℕ} (hb : 1 < b) (m : ℕ) (hm : 0 < m) : + (Finset.Ico (b ^ (m - 1)) (b ^ m)).card = (b - 1) * b ^ (m - 1) := by + rw [Nat.card_Ico] + have h : b ^ m = b * b ^ (m - 1) := by + conv_lhs => rw [show m = (m - 1) + 1 by omega] + rw [pow_succ'] + have hd : (b - 1) * b ^ (m - 1) + b ^ (m - 1) = b * b ^ (m - 1) := by + have hb1 : b - 1 + 1 = b := by omega + calc (b - 1) * b ^ (m - 1) + b ^ (m - 1) + = (b - 1 + 1) * b ^ (m - 1) := by ring + _ = b * b ^ (m - 1) := by rw [hb1] + omega + +/-! ### Cohort decomposition -/ + +/-- Cohort decomposition of a sum over `[1, b^M)`. -/ +theorem sum_Ico_one_pow {β : Type*} [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 := by + induction M with + | zero => simp + | succ M ih => + rw [← Finset.sum_Ico_consecutive g + (Nat.one_le_pow M b (by omega)) + (Nat.pow_le_pow_right (by omega) (Nat.le_add_right M 1)), + ih, Finset.sum_Icc_succ_top (by omega), Nat.add_sub_cancel] + +/-! ### Stream and cohort length sums -/ + +/-- The stream-prefix length as a sum over the numbers `1..N`. -/ +theorem length_champBlocks (b N : ℕ) : + (champBlocks b N).length + = ∑ n ∈ Finset.Ico 1 (N + 1), (bigDigits b n).length := by + induction N with + | zero => simp [champBlocks] + | succ n ih => + rw [champBlocks_succ, List.length_append, ih] + exact (Finset.sum_Ico_succ_top (show 1 ≤ n + 1 by omega) _).symm + +/-- Total digit length of the `m`-digit cohort. -/ +theorem 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 := by + have hc : ∀ n ∈ Finset.Ico (b ^ (m - 1)) (b ^ m), + (bigDigits b n).length = m := by + intro n hn + rw [Finset.mem_Ico] at hn + exact length_bigDigits_eq hb hn.1 hn.2 + rw [Finset.sum_congr rfl hc, Finset.sum_const, card_mDigit hb m hm, + smul_eq_mul] + +/-- Total digit length of a partial cohort. -/ +theorem 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) := by + have hc : ∀ n ∈ Finset.Ico (b ^ K) (b ^ K + t), + (bigDigits b n).length = K + 1 := by + intro n hn + rw [Finset.mem_Ico] at hn + exact length_bigDigits_eq hb (by simpa using hn.1) (by omega) + rw [Finset.sum_congr rfl hc, Finset.sum_const, Nat.card_Ico, + Nat.add_sub_cancel_left, smul_eq_mul] + +/-! ### Blocks at positions -/ + +/-- 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`. -/ +theorem 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) : + ((bigDigits b n).drop j).take w.length = w + ↔ n / b ^ (m - j - w.length) % b ^ w.length + = Nat.ofDigits b w.reverse := by + have hml : (Nat.digits b n).length = m := by simpa [bigDigits] using hlen + have hsub : ((bigDigits b n).drop j).take w.length + = (((Nat.digits b n).drop (m - j - w.length)).take w.length).reverse := by + change (((Nat.digits b n).reverse.drop j).take w.length) = _ + rw [List.drop_reverse, hml, List.take_reverse, List.length_take, hml, + Nat.min_eq_left (by omega)] + congr 1 + rw [List.take_drop, + show m - j - w.length + w.length = m - j by omega] + have hA_lt : ∀ d ∈ ((Nat.digits b n).drop (m - j - w.length)).take w.length, + d < b := fun d hd => + Nat.digits_lt_base hb (List.mem_of_mem_drop (List.mem_of_mem_take hd)) + have hA_len : + ((((Nat.digits b n).drop (m - j - w.length)).take w.length)).length + = w.length := by + rw [List.length_take, List.length_drop, hml] + omega + have hofA : Nat.ofDigits b + (((Nat.digits b n).drop (m - j - w.length)).take w.length) + = n / b ^ (m - j - w.length) % b ^ w.length := by + rw [← Nat.ofDigits_mod_pow_eq_ofDigits_take w.length (by omega) _ + (fun d hd => Nat.digits_lt_base hb (List.mem_of_mem_drop hd)), + ← Nat.self_div_pow_eq_ofDigits_drop _ _ hb] + rw [hsub, List.reverse_eq_iff] + constructor + · intro h + rw [← hofA, h] + · intro h + refine Nat.ofDigits_inj_of_len_eq hb ?_ hA_lt + (fun d hd => hw d (List.mem_reverse.mp hd)) ?_ + · rw [hA_len, List.length_reverse] + · rw [hofA, h] + +/-! ### 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). -/ + +/-- Convert the block predicate at interior position `j` to the arithmetic +predicate, on a partial cohort of `(K+1)`-digit numbers. -/ +theorem filter_blockAt_partial_congr {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)) : + (Finset.Ico (b ^ K) (b ^ K + t)).filter + (fun n => ((bigDigits b n).drop j).take w.length = w) + = (Finset.Ico (b ^ K) (b ^ K + t)).filter + (fun n => n / b ^ (K + 1 - j - w.length) % b ^ w.length + = Nat.ofDigits b w.reverse) := by + apply Finset.filter_congr + intro n hn + rw [Finset.mem_Ico] at hn + exact block_eq_iff hb (length_bigDigits_eq (m := K + 1) hb hn.1 (by omega)) hw + (by omega) + +/-- Lower bound for one interior position over a partial cohort. -/ +theorem 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 ≤ ((Finset.Ico (b ^ K) (b ^ K + t)).filter + (fun n => ((bigDigits b n).drop j).take w.length = w)).card + + b ^ (K + 1 - j - w.length) := by + rw [filter_blockAt_partial_congr hb K t j hw hj hjk hAt] + have hD : Nat.ofDigits b w.reverse < b ^ w.length := by + have h := Nat.ofDigits_lt_base_pow_length hb + (fun d hd => hw d (List.mem_reverse.mp hd)) + rwa [List.length_reverse] at h + have hp : 0 < b ^ (K + 1 - j - w.length) := pow_pos (by omega) _ + have hq : 0 < b ^ w.length := pow_pos (by omega) _ + have hpq : b ^ (K + 1 - j - w.length) * b ^ w.length = b ^ (K + 1 - j) := by + rw [← pow_add]; congr 1; omega + have hdvd : b ^ (K + 1 - j - w.length) * b ^ w.length ∣ b ^ K := + hpq ▸ pow_dvd_pow b (by omega) + calc t / b ^ w.length + ≤ t / (b ^ (K + 1 - j - w.length) * b ^ w.length) + * b ^ (K + 1 - j - w.length) + b ^ (K + 1 - j - w.length) := + div_le_div_mul_add t _ (b ^ w.length) hp hq + _ ≤ _ := Nat.add_le_add_right + (le_card_Ico_filter_div_mod hp hq hD hdvd) _ + +/-- Partial-cohort occurrence sum as a sum of per-position cards. -/ +theorem 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), + ((Finset.Ico (b ^ K) (b ^ K + t)).filter + (fun n => ((bigDigits b n).drop j).take w.length = w)).card := by + have hstep : ∀ n ∈ Finset.Ico (b ^ K) (b ^ K + t), + countOccurrences w (bigDigits b n) + = ∑ j ∈ Finset.range (K + 2), + if ((bigDigits b n).drop j).take w.length = w then 1 else 0 := by + intro n hn + rw [Finset.mem_Ico] at hn + have hpred : ∀ j ∈ Finset.range (K + 2), + (w.isPrefixOf ((bigDigits b n).drop j) = true) + ↔ ((bigDigits b n).drop j).take w.length = w := fun j _ => by + rw [List.isPrefixOf_iff_prefix, List.prefix_iff_eq_take, eq_comm] + rw [countOccurrences_eq_card_filter_range, + length_bigDigits_eq (m := K + 1) hb hn.1 (by omega), Finset.filter_congr hpred, + Finset.card_filter] + rw [Finset.sum_congr rfl hstep, Finset.sum_comm] + exact Finset.sum_congr rfl fun j _ => (Finset.card_filter _ _).symm + +/-- Partial-cohort occurrence sum, lower bound (stated additively; drops the +head position, which is only ever a nonnegative contribution). -/ +theorem 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) := by + rw [sum_countOccurrences_Ico_eq hb K t w hAt, Finset.range_eq_Ico, + ← Finset.sum_Ico_consecutive _ (Nat.zero_le (K + 1 - w.length + 1)) + (by omega : K + 1 - w.length + 1 ≤ K + 2), + ← Finset.range_eq_Ico, Finset.sum_range_succ'] + have hint : (K + 1 - w.length) * (t / b ^ w.length) + ≤ (∑ i ∈ Finset.range (K + 1 - w.length), + ((Finset.Ico (b ^ K) (b ^ K + t)).filter + (fun n => ((bigDigits b n).drop (i + 1)).take w.length = w)).card) + + ∑ i ∈ Finset.range (K + 1 - w.length), b ^ (K - w.length - i) := by + have h1 : ∑ _i ∈ Finset.range (K + 1 - w.length), t / b ^ w.length + = (K + 1 - w.length) * (t / b ^ w.length) := by + rw [Finset.sum_const, Finset.card_range, smul_eq_mul] + have h2 : (∑ _i ∈ Finset.range (K + 1 - w.length), t / b ^ w.length) + ≤ ∑ i ∈ Finset.range (K + 1 - w.length), + (((Finset.Ico (b ^ K) (b ^ K + t)).filter + (fun n => ((bigDigits b n).drop (i + 1)).take w.length = w)).card + + b ^ (K + 1 - (i + 1) - w.length)) := + Finset.sum_le_sum fun i hi => + le_card_blockAt_partial hb K t (i + 1) hw (Nat.succ_pos i) + (by rw [Finset.mem_range] at hi; omega) hAt + rw [Finset.sum_add_distrib] at h2 + rw [h1] at h2 + refine le_trans h2 (Nat.add_le_add_left (le_of_eq ?_) _) + exact Finset.sum_congr rfl fun i _ => by congr 1; omega + have hgl := geomsum_lt hb (K + 1 - w.length) + have hrefl : ∑ i ∈ Finset.range (K + 1 - w.length), b ^ (K - w.length - i) + = ∑ i ∈ Finset.range (K + 1 - w.length), b ^ i := by + rw [← Finset.sum_range_reflect (fun i => b ^ i) (K + 1 - w.length)] + exact Finset.sum_congr rfl fun i hi => by + rw [Finset.mem_range] at hi; congr 1; omega + rw [hrefl] at hint + omega + +/-! ### Partial-cohort comparison, boundary induction, and general `N` -/ + +/-- `c + j + 1 ≤ (c+1) * b^j` for `b ≥ 2` -- linear growth is dominated by +any base's exponential, uniformly from `j = 0`. -/ +theorem linear_le_const_mul_pow {b : ℕ} (hb : 1 < b) (c j : ℕ) : + c + j + 1 ≤ (c + 1) * b ^ j := by + induction j with + | zero => simp + | succ j ih => + have hpow : b ^ (j + 1) = b * b ^ j := by rw [pow_succ'] + rw [hpow] + have h2 : (c + 1) * b ^ j * 2 ≤ (c + 1) * b ^ j * b := Nat.mul_le_mul_left _ hb + nlinarith [ih] + +/-- Partial-cohort comparison, lower. -/ +theorem 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) := by + have hwlen : 0 < w.length := List.length_pos_of_ne_nil hwne + have hsum := le_sum_countOccurrences_partial_cohort hb K t hw hk hAt + have hmul := Nat.mul_le_mul_left (b ^ w.length) hsum + rw [Nat.mul_add] at hmul + have hbpow : b ^ w.length * (2 * b ^ (K + 1 - w.length)) = 2 * b ^ (K + 1) := by + rw [show b ^ w.length * (2 * b ^ (K + 1 - w.length)) + = 2 * (b ^ w.length * b ^ (K + 1 - w.length)) from by ring, ← pow_add] + congr 2; omega + have hlen := sum_length_partial hb K t hAt + have hdm : b ^ w.length * (t / b ^ w.length) + t % b ^ w.length = t := + Nat.div_add_mod t (b ^ w.length) + have hmod : t % b ^ w.length ≤ b ^ w.length := le_of_lt (Nat.mod_lt t (by positivity)) + have hlin := linear_le_const_mul_pow hb w.length (K + 1 - w.length) + have hj : w.length + (K + 1 - w.length) + 1 = K + 2 := by omega + rw [hj] at hlin + have hpoweq : b ^ (K + 1 - w.length) * b ^ w.length = b ^ (K + 1) := by + rw [← pow_add]; congr 1; omega + have hrbound : (K + 1 - w.length) * (t % b ^ w.length) ≤ (w.length + 1) * b ^ (K + 1) := by + calc (K + 1 - w.length) * (t % b ^ w.length) + ≤ (K + 2) * b ^ w.length := Nat.mul_le_mul (by omega) hmod + _ ≤ (w.length + 1) * b ^ (K + 1 - w.length) * b ^ w.length := + Nat.mul_le_mul_right _ hlin + _ = (w.length + 1) * (b ^ (K + 1 - w.length) * b ^ w.length) := by ring + _ = (w.length + 1) * b ^ (K + 1) := by rw [hpoweq] + have htw : t * w.length ≤ (w.length + 1) * b ^ (K + 1) := by + have ht1 : t ≤ b ^ (K + 1) := by omega + calc t * w.length ≤ b ^ (K + 1) * w.length := Nat.mul_le_mul_right _ ht1 + _ ≤ b ^ (K + 1) * (w.length + 1) := Nat.mul_le_mul_left _ (by omega) + _ = (w.length + 1) * b ^ (K + 1) := by ring + have hkey : t * (K + 1) = (K + 1 - w.length) * (b ^ w.length * (t / b ^ w.length)) + + (K + 1 - w.length) * (t % b ^ w.length) + t * w.length := by + have h2 : (K + 1 - w.length) * (b ^ w.length * (t / b ^ w.length)) + + (K + 1 - w.length) * (t % b ^ w.length) = (K + 1 - w.length) * t := by + rw [← Nat.mul_add, hdm] + have h3 : (K + 1 - w.length) * t + t * w.length = t * (K + 1) := by + have hKw : (K + 1 - w.length) + w.length = K + 1 := by omega + calc (K + 1 - w.length) * t + t * w.length + = t * ((K + 1 - w.length) + w.length) := by ring + _ = t * (K + 1) := by rw [hKw] + omega + have hcomm : b ^ w.length * ((K + 1 - w.length) * (t / b ^ w.length)) + = (K + 1 - w.length) * (b ^ w.length * (t / b ^ w.length)) := by ring + have e1 : (K + 1 - w.length) * (b ^ w.length * (t / b ^ w.length)) + ≤ b ^ w.length * (∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), countOccurrences w (bigDigits b n)) + + b ^ w.length * (2 * b ^ (K + 1 - w.length)) := by + rw [← hcomm]; exact hmul + have hscale3 : 2 * b ^ (K + 1) ≤ (w.length + 1) * b ^ (K + 1) := + Nat.mul_le_mul_right _ (by omega) + calc (∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), (bigDigits b n).length) + = t * (K + 1) := hlen + _ = (K + 1 - w.length) * (b ^ w.length * (t / b ^ w.length)) + + (K + 1 - w.length) * (t % b ^ w.length) + t * w.length := hkey + _ ≤ (b ^ w.length * (∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), countOccurrences w (bigDigits b n)) + + b ^ w.length * (2 * b ^ (K + 1 - w.length))) + + (w.length + 1) * b ^ (K + 1) + (w.length + 1) * b ^ (K + 1) := + Nat.add_le_add (Nat.add_le_add e1 hrbound) htw + _ = b ^ w.length * (∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), countOccurrences w (bigDigits b n)) + + (b ^ w.length * (2 * b ^ (K + 1 - w.length)) + + (w.length + 1) * b ^ (K + 1) + (w.length + 1) * b ^ (K + 1)) := by ring + _ = b ^ w.length * (∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), countOccurrences w (bigDigits b n)) + + (2 * b ^ (K + 1) + (w.length + 1) * b ^ (K + 1) + (w.length + 1) * b ^ (K + 1)) := by + rw [hbpow] + _ ≤ b ^ w.length * (∑ n ∈ Finset.Ico (b ^ K) (b ^ K + t), countOccurrences w (bigDigits b n)) + + 3 * (w.length + 1) * b ^ (K + 1) := by + have hseq : 3 * (w.length + 1) * b ^ (K + 1) + = (w.length + 1) * b ^ (K + 1) + (w.length + 1) * b ^ (K + 1) + + (w.length + 1) * b ^ (K + 1) := by ring + omega + +/-- The accumulated cohort error is absorbed by the next power of the base. -/ +theorem cohort_error_add_le {b : ℕ} (hb : 1 < b) (c K : ℕ) : + 6 * c * b ^ K + 3 * c * b ^ (K + 1) ≤ 6 * c * b ^ (K + 1) := by + rw [pow_succ'] + have hstep : c * b ^ K * 2 ≤ c * b ^ K * b := Nat.mul_le_mul_left _ hb + nlinarith only [hstep] + +/-- 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 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 := by + have hwlen : 0 < w.length := List.length_pos_of_ne_nil hwne + induction K with + | zero => simp + | succ K ih => + have h1 : b ^ K ≤ b ^ (K + 1) := + Nat.pow_le_pow_right (by omega) (Nat.le_add_right K 1) + have hcov : b ^ K + (b ^ (K + 1) - b ^ K) = b ^ (K + 1) := by omega + rw [← Finset.sum_Ico_consecutive (fun n => countOccurrences w (bigDigits b n)) + (Nat.one_le_pow K b (by omega)) h1, + ← Finset.sum_Ico_consecutive (fun n => (bigDigits b n).length) + (Nat.one_le_pow K b (by omega)) h1, + Nat.mul_add] + rcases Nat.lt_or_ge (K + 1) w.length with hshort | hlong + · -- cohort shorter than `w`: drop the count, bound the length crudely + have hlen := sum_length_partial hb K (b ^ (K + 1) - b ^ K) (by omega) + rw [hcov] at hlen + have hbnd : (b ^ (K + 1) - b ^ K) * (K + 1) ≤ (w.length + 1) * b ^ (K + 1) := by + calc (b ^ (K + 1) - b ^ K) * (K + 1) + ≤ b ^ (K + 1) * (K + 1) := Nat.mul_le_mul_right _ (by omega) + _ ≤ b ^ (K + 1) * (w.length + 1) := Nat.mul_le_mul_left _ (by omega) + _ = (w.length + 1) * b ^ (K + 1) := Nat.mul_comm _ _ + have hscale : 6 * (w.length + 1) * b ^ K + (w.length + 1) * b ^ (K + 1) + ≤ 6 * (w.length + 1) * b ^ (K + 1) := by + have h := cohort_error_add_le hb (w.length + 1) K + nlinarith only [h, Nat.zero_le ((w.length + 1) * b ^ (K + 1))] + omega + · have hpart := le_base_pow_countOccurrences_partial hb K (b ^ (K + 1) - b ^ K) + hw hwne (by omega) (by omega) + rw [hcov] at hpart + have hscale := cohort_error_add_le hb (w.length + 1) K + omega + +/-- General-`N` comparison, lower. -/ +theorem 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 := by + obtain ⟨K, rfl⟩ : ∃ K, M = K + 1 := ⟨M - 1, by omega⟩ + rw [show K + 1 - 1 = K from rfl] at h1 + obtain ⟨t, ht⟩ : ∃ t, N + 1 = b ^ K + t := ⟨N + 1 - b ^ K, by omega⟩ + have hAt : b ^ K + t ≤ b ^ (K + 1) := by omega + rw [ht, ← Finset.sum_Ico_consecutive (fun n => countOccurrences w (bigDigits b n)) + (Nat.one_le_pow K b (by omega)) (Nat.le_add_right _ _), + ← Finset.sum_Ico_consecutive (fun n => (bigDigits b n).length) + (Nat.one_le_pow K b (by omega)) (Nat.le_add_right _ _), + Nat.mul_add] + have hbd := le_base_pow_count_boundary hb K hw hwne + have hpart := le_base_pow_countOccurrences_partial hb K t hw hwne (by omega) hAt + have hscale := cohort_error_add_le hb (w.length + 1) K + omega + +end Champernowne diff --git a/LeanPool/Champernowne/Main.lean b/LeanPool/Champernowne/Main.lean new file mode 100644 index 0000000000..90737bd0d0 --- /dev/null +++ b/LeanPool/Champernowne/Main.lean @@ -0,0 +1,30 @@ +/- +Copyright (c) 2026 Arthur Champernowne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Champernowne +-/ +module + +public import LeanPool.Champernowne.Asymptotics + +/-! +# Champernowne's theorem (1933) + +The base-`b` Champernowne sequence is normal in base `b`. +-/ + +@[expose] public section + +namespace Champernowne + +theorem champernowne_normal (b : ℕ) (hb : 2 ≤ b) : + IsNormalSequence b (champDigit b) := by + intro w hwne hw + have h := tendsto_countOccurrences_champPrefix_div (b := b) (w := w) (by omega) hw hwne + simpa only [champPrefix_eq_map] using h + +/-- The classical base-10 statement. -/ +theorem champernowne_normal_ten : IsNormalSequence 10 (champDigit 10) := + champernowne_normal 10 (by norm_num) + +end Champernowne diff --git a/LeanPool/Champernowne/Positions.lean b/LeanPool/Champernowne/Positions.lean new file mode 100644 index 0000000000..fc305876ea --- /dev/null +++ b/LeanPool/Champernowne/Positions.lean @@ -0,0 +1,212 @@ +/- +Copyright (c) 2026 Arthur Champernowne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Champernowne +-/ +module + +public import LeanPool.Champernowne.DigitCount +public import LeanPool.Champernowne.Prefix +public import Mathlib.Algebra.BigOperators.Ring.Finset + +/-! +# 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`. +-/ + +@[expose] public section + +namespace Champernowne + +/-- Greatest `N` with `(champBlocks b N).length ≤ n`. -/ +def champIndex (b n : ℕ) : ℕ := + Nat.findGreatest (fun N => (champBlocks b N).length ≤ n) n + +theorem length_champBlocks_champIndex_le (b n : ℕ) : + (champBlocks b (champIndex b n)).length ≤ n := by + have h0 : (champBlocks b 0).length ≤ n := by simp [champBlocks] + exact Nat.findGreatest_spec (P := fun N => (champBlocks b N).length ≤ n) + (Nat.zero_le n) h0 + +theorem lt_length_champBlocks_champIndex_succ (b n : ℕ) : + n < (champBlocks b (champIndex b n + 1)).length := by + rcases Nat.lt_or_ge n (champIndex b n + 1) with h | h + · exact lt_of_lt_of_le h (le_length_champBlocks b _) + · have hng := Nat.findGreatest_is_greatest + (P := fun N => (champBlocks b N).length ≤ n) + (k := champIndex b n + 1) (Nat.lt_succ_self _) h + exact Nat.lt_of_not_le hng + +/-- `champPrefix b n` is a prefix of the blocks it is carved from. -/ +theorem champPrefix_prefix (b n : ℕ) : champPrefix b n <+: champBlocks b n := + List.take_prefix n _ + +/-- Complete blocks below position `n` form a prefix of `champPrefix b n`. -/ +theorem champBlocks_prefix_champPrefix {b N n : ℕ} + (h : (champBlocks b N).length ≤ n) : + champBlocks b N <+: champPrefix b n := by + have hNn : N ≤ n := le_trans (le_length_champBlocks b N) h + exact List.prefix_of_prefix_length_le (champBlocks_prefix hNn) + (champPrefix_prefix b n) (by rw [length_champPrefix]; exact h) + +/-- Position `n` lies within one number's digits of the complete blocks. -/ +theorem n_lt_length_champIndex_add (b n : ℕ) : + n < (champBlocks b (champIndex b n)).length + + (bigDigits b (champIndex b n + 1)).length := by + have h := lt_length_champBlocks_champIndex_succ b n + rwa [champBlocks_succ, List.length_append] at h + +/-- The straddling number has at most `M + 1` digits. -/ +theorem 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 := by + rw [bigDigits, List.length_reverse] + refine (Nat.digits_length_le_iff hb _).mpr ?_ + calc champIndex b n + 1 ≤ b ^ M := h2 + _ < b ^ (M + 1) := Nat.pow_lt_pow_right hb (Nat.lt_succ_self M) + +/-! ### 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. -/ + +/-- `champBlocks (champIndex n)` is a genuine prefix of `champPrefix n`, so +its occurrence count only ever undercounts. -/ +theorem le_countOccurrences_champPrefix (b n : ℕ) {w : List ℕ} (hwne : w ≠ []) : + countOccurrences w (champBlocks b (champIndex b n)) + ≤ countOccurrences w (champPrefix b n) := by + obtain ⟨l, hl⟩ := champBlocks_prefix_champPrefix (length_champBlocks_champIndex_le b n) + rw [← hl] + have h := add_countOccurrences_le_append hwne (champBlocks b (champIndex b n)) l + omega + +/-- 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 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 := by + have hS := sum_le_countOccurrences_champBlocks (b := b) hwne (champIndex b n) + have hDig := le_base_pow_countOccurrences_champBlocks hb (champIndex b n) M hw hwne hM hwM h1 h2 + have hlen := n_lt_length_champIndex_add b n + have hstraddle := length_bigDigits_champIndex_succ_le hb h2 + have hle := le_countOccurrences_champPrefix b n hwne (w := w) + have hMpow : M + 1 ≤ b ^ M := by + have h0 := linear_le_const_mul_pow hb 0 M; simpa using h0 + rw [length_champBlocks] at hlen + have hSmul : b ^ w.length + * (∑ n ∈ Finset.Ico 1 (champIndex b n + 1), countOccurrences w (bigDigits b n)) + ≤ b ^ w.length * countOccurrences w (champBlocks b (champIndex b n)) := + Nat.mul_le_mul_left _ hS + have hlemul : b ^ w.length * countOccurrences w (champBlocks b (champIndex b n)) + ≤ b ^ w.length * countOccurrences w (champPrefix b n) := + Nat.mul_le_mul_left _ hle + have hp : 1 ≤ b ^ w.length := Nat.one_le_iff_ne_zero.mpr (by positivity) + have hMscale : M + 1 ≤ b ^ w.length * b ^ M := by + calc M + 1 ≤ b ^ M := hMpow + _ = 1 * b ^ M := by ring + _ ≤ b ^ w.length * b ^ M := Nat.mul_le_mul_right _ hp + have hbudget : 6 * (w.length + 1) * b ^ M + b ^ w.length * b ^ M + ≤ 7 * (w.length + 1) * b ^ w.length * b ^ M := by + have e0 : 6 * (w.length + 1) * b ^ M ≤ 6 * (w.length + 1) * b ^ w.length * b ^ M := by + calc 6 * (w.length + 1) * b ^ M = 6 * (w.length + 1) * 1 * b ^ M := by ring + _ ≤ 6 * (w.length + 1) * b ^ w.length * b ^ M := + Nat.mul_le_mul_right _ (Nat.mul_le_mul_left _ hp) + have e1 : b ^ w.length * b ^ M ≤ (w.length + 1) * b ^ w.length * b ^ M := by + have hh : b ^ w.length ≤ (w.length + 1) * b ^ w.length := + Nat.le_mul_of_pos_left _ (by omega) + exact Nat.mul_le_mul_right _ hh + have e2 : 6 * (w.length + 1) * b ^ w.length * b ^ M + (w.length + 1) * b ^ w.length * b ^ M + = 7 * (w.length + 1) * b ^ w.length * b ^ M := by ring + omega + omega + +/-- 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`. -/ +theorem 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 := by + have hk : 0 < w.length := List.length_pos_of_ne_nil hwne + have hwW : w ∈ allWords b w.length := mem_allWords.mpr ⟨rfl, hw⟩ + -- Pigeonhole over all length-k words, with the w term split off. + have hpig := sum_countOccurrences_allWords_le b w.length (champPrefix b n) + rw [length_champPrefix, ← Finset.add_sum_erase _ _ hwW] at hpig + have hpig' := Nat.mul_le_mul_left (b ^ w.length) hpig + rw [Nat.mul_add, Nat.mul_add, Nat.mul_one] at hpig' + -- The lower transfer at each of the other words. + have hlow : ∀ v ∈ (allWords b w.length).erase w, + n ≤ b ^ w.length * countOccurrences v (champPrefix b n) + + 7 * (w.length + 1) * b ^ w.length * b ^ M := by + intro v hv + obtain ⟨hvlen, hvlt⟩ := mem_allWords.mp (Finset.mem_of_mem_erase hv) + have hvne : v ≠ [] := by + intro hnil + rw [hnil] at hvlen + simp only [List.length_nil] at hvlen + omega + have hvM : v.length ≤ M := by rw [hvlen]; exact hwM + have h := le_base_pow_countOccurrences_champPrefix hb n M hvlt hvne hM hvM h1 h2 + rwa [hvlen] at h + have hsum := Finset.sum_le_sum hlow + simp only [Finset.sum_const, smul_eq_mul, Finset.sum_add_distrib, + ← Finset.mul_sum] at hsum + -- Count of the other words: card + 1 = b^k. + have hcard : ((allWords b w.length).erase w).card + 1 = b ^ w.length := by + rw [Finset.card_erase_of_mem hwW, card_allWords] + have hp : 0 < b ^ w.length := pow_pos (by omega) _ + omega + -- Rewrite the goal's error as b^k · (lower-bound error), then abstract. + rw [show 7 * (w.length + 1) * b ^ (2 * w.length) * b ^ M + = b ^ w.length * (7 * (w.length + 1) * b ^ w.length * b ^ M) by + rw [two_mul, pow_add]; ring] + set P := b ^ w.length with hPdef + set E := 7 * (w.length + 1) * P * b ^ M with hEdef + set C := countOccurrences w (champPrefix b n) with hCdef + set S := ∑ v ∈ (allWords b w.length).erase w, + countOccurrences v (champPrefix b n) with hSdef + set c := ((allWords b w.length).erase w).card with hcdef + -- Bridges between the omega atoms. + have g1 : c * n + n = P * n := by rw [← hcard]; ring + have g2 : c * E + E = P * E := by rw [← hcard]; ring + have g3 : P ≤ E := by + have hbM : 1 ≤ b ^ M := Nat.one_le_pow _ _ (by omega) + calc P = 1 * P * 1 := by ring + _ ≤ 7 * (w.length + 1) * P * b ^ M := + Nat.mul_le_mul (Nat.mul_le_mul_right _ (by omega)) hbM + -- hpig' : P*C + P*S ≤ P*n + P; hsum : c*n ≤ P*S + c*E; goal : P*C ≤ n + P*E. + omega + +/-! ### Prefix chain -/ + +/-- `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)`. -/ +theorem champPrefix_prefix_champBlocks {b n N : ℕ} + (h : n ≤ (champBlocks b N).length) : + champPrefix b n <+: champBlocks b N := by + rcases le_total n N with hnN | hNn + · exact (champPrefix_prefix b n).trans (champBlocks_prefix hnN) + · exact List.prefix_of_prefix_length_le (champPrefix_prefix b n) + (champBlocks_prefix hNn) (by rw [length_champPrefix]; exact h) + +end Champernowne diff --git a/LeanPool/Champernowne/Prefix.lean b/LeanPool/Champernowne/Prefix.lean new file mode 100644 index 0000000000..b5f9f49acc --- /dev/null +++ b/LeanPool/Champernowne/Prefix.lean @@ -0,0 +1,61 @@ +/- +Copyright (c) 2026 Arthur Champernowne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arthur Champernowne +-/ +module + +public import LeanPool.Champernowne.Defs + +/-! +# 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`). +-/ + +@[expose] public section + +namespace Champernowne + +theorem champBlocks_prefix {b N M : ℕ} (h : N ≤ M) : + champBlocks b N <+: champBlocks b M := by + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h + simp only [champBlocks, List.range_add, List.map_append, List.flatten_append] + exact List.prefix_append _ _ + +/-- Coherence: any sufficiently long prefix computes `champDigit`. -/ +theorem champBlocks_getElem (b N i : ℕ) (h : i < (champBlocks b N).length) : + (champBlocks b N)[i] = champDigit b i := by + simp only [champDigit] + rcases le_total N (i + 1) with hN | hN + · exact (champBlocks_prefix hN).getElem h + · exact ((champBlocks_prefix hN).getElem (lt_of_lt_of_le (Nat.lt_succ_self i) + (le_length_champBlocks b (i + 1)))).symm + +/-- The first `n` digits of the base-`b` Champernowne sequence. -/ +def champPrefix (b n : ℕ) : List ℕ := (champBlocks b n).take n + +theorem length_champPrefix (b n : ℕ) : (champPrefix b n).length = n := by + rw [champPrefix, List.length_take] + exact Nat.min_eq_left (le_length_champBlocks b n) + +theorem champPrefix_eq_map (b n : ℕ) : + champPrefix b n = (List.range n).map (champDigit b) := by + have hlen := length_champPrefix b n + apply List.ext_getElem + · rw [hlen, List.length_map, List.length_range] + · intro i h1 h2 + have hi : i < (champBlocks b n).length := by + rw [hlen] at h1 + exact lt_of_lt_of_le h1 (le_length_champBlocks b n) + simp only [champPrefix, List.getElem_take, List.getElem_map, List.getElem_range] + exact champBlocks_getElem b n i hi + +end Champernowne diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 4b297d329a..95610cc732 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -1,4 +1,61 @@ projects: + - slug: champernowne-normality + title: Champernowne normality in every base + summary: >- + Proves that concatenating the base-b digits of the positive integers + gives a normal digit sequence for every integer base b at least 2: + every nonempty length-k word of digits below b has limiting frequency + b^(-k). This is a discrete, all-base generalization of D. G. + Champernowne's 1933 base-ten result, without a real-number expansion + bridge. Includes reusable substring-counting inequalities, a + digit-string equivalence, exact cohort counts, and quantitative prefix + bounds used to establish the frequency limit. + branch: number theory and asymptotic analysis + entry_module: LeanPool.Champernowne + authors: + - Arthur Champernowne + source: + title: Champernowne Sequence Normality Proof + authors: + - Arthur Champernowne + url: https://github.com/OldMathematician/ChampernowneNormality + github_repo: OldMathematician/ChampernowneNormality + commit: 31a76dbde2727745beb6fb81af4cab1ce6a15fda + license: Apache-2.0 + status: verified + provenance: AI + main_declarations: + - Champernowne.champernowne_normal + main_results: + - declaration: Champernowne.champernowne_normal + informal: >- + For every integer base b at least 2, the sequence formed by + concatenating the base-b digits of 1, 2, 3, and so on is normal: + each nonempty word w of digits below b has limiting occurrence + frequency 1 / b^(length w), counting overlapping occurrences. + - declaration: Champernowne.champernowne_normal_ten + informal: >- + The decimal digit sequence 123456789101112... is normal in base ten. + - declaration: Champernowne.sum_countOccurrences_cohort + informal: >- + For a nonempty length-k word of base-b digits with nonzero first + digit and k at most m, its total occurrences inside all m-digit + positive integers equal b^(m-k) + (m-k)(b-1)b^(m-k-1), with natural + subtraction in the exponents. + - declaration: Champernowne.sum_countOccurrences_cohort_zero + informal: >- + For a nonempty length-k word of base-b digits starting with zero + and k at most m, its total occurrences inside all m-digit positive + integers equal (m-k)(b-1)b^(m-k-1), with natural subtraction in the + exponent. + tags: + - normal-numbers + - digit-expansions + - combinatorics-on-words + - asymptotic-frequency + msc: + - 11K16 + - 68R15 - slug: sum-difference-exponent title: The optimal exponent relating sumsets and difference sets summary: >- From 2cc87eed5829cc29be2361d5e41a6b5e29218407 Mon Sep 17 00:00:00 2001 From: Vilin97 automation Date: Mon, 21 Sep 2026 10:33:59 -0700 Subject: [PATCH 2/2] fix(champernowne): allow head positions in block conversion --- LeanPool/Champernowne/DigitCount.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/LeanPool/Champernowne/DigitCount.lean b/LeanPool/Champernowne/DigitCount.lean index 3bf5c2c9e2..85d9eaf189 100644 --- a/LeanPool/Champernowne/DigitCount.lean +++ b/LeanPool/Champernowne/DigitCount.lean @@ -253,10 +253,10 @@ 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). -/ -/-- Convert the block predicate at interior position `j` to the arithmetic +/-- Convert the block predicate at position `j` to the arithmetic predicate, on a partial cohort of `(K+1)`-digit numbers. -/ theorem filter_blockAt_partial_congr {b : ℕ} (hb : 1 < b) (K t j : ℕ) - {w : List ℕ} (hw : ∀ d ∈ w, d < b) (_hj : 0 < j) (hjk : j + w.length ≤ K + 1) + {w : List ℕ} (hw : ∀ d ∈ w, d < b) (hjk : j + w.length ≤ K + 1) (hAt : b ^ K + t ≤ b ^ (K + 1)) : (Finset.Ico (b ^ K) (b ^ K + t)).filter (fun n => ((bigDigits b n).drop j).take w.length = w) @@ -276,7 +276,7 @@ theorem le_card_blockAt_partial {b : ℕ} (hb : 1 < b) (K t j : ℕ) t / b ^ w.length ≤ ((Finset.Ico (b ^ K) (b ^ K + t)).filter (fun n => ((bigDigits b n).drop j).take w.length = w)).card + b ^ (K + 1 - j - w.length) := by - rw [filter_blockAt_partial_congr hb K t j hw hj hjk hAt] + rw [filter_blockAt_partial_congr hb K t j hw hjk hAt] have hD : Nat.ofDigits b w.reverse < b ^ w.length := by have h := Nat.ofDigits_lt_base_pow_length hb (fun d hd => hw d (List.mem_reverse.mp hd))