Digits of j + b * y, factorials of digits, cyclic shifts of digits and redundant words

For a digit j < b, the base-b digits of j + b * y are j followed by the digits of y. This gives the digit sum and the products over the digits of j + b * y in terms of those of y. The product of the factorials of the base-p digits of n is prime to p, since every digit is less than p. These facts index the digit induction in Stickelberger's congruence.

For 0 ≤ a < b ^ f - 1, multiplication by b modulo b ^ f - 1 cyclically shifts the f base-b digits of a. Summing the f shifts b ^ i * a % (b ^ f - 1), every digit of a occurs once in every position, so (b - 1) ∑_{i < f} (b ^ i * a % (b ^ f - 1)) = (b ^ f - 1) s(a) with s(a) the digit sum of a; equivalently s(a) = (b - 1) ∑_{i < f} {b ^ i a / (b ^ f - 1)}. For a = (b ^ f - 1) / m * t this reads m s(a) = (b - 1) ∑_{i < f} (b ^ i t % m). With b = p and b ^ f = q the size of a finite field, this identity turns the digit-sum valuation of Gauss sums into the exponents t of Stickelberger's element ∑ t σ_t⁻¹.

Allowing the digits 0, …, 2b, every z ≤ 2 b ^ n with n ≥ 1 is the base-b value of a word of length exactly n. Such redundant words of a fixed length let an automaton append the same suffix of length n to two prefixes and reach every offset in the doubled interval [0, 2 b ^ n], as in Krebs's proof of Cobham's theorem.

Main results

• Nat.exists_length_eq_ofDigits_eq_of_le_two_mul_pow: for n ≥ 1, every z ≤ 2 b ^ n is the value of a word of length n with digits at most 2b.
• Nat.sum_digits_add_mul: the digit sum of j + b * y is j plus the digit sum of y.
• Nat.prod_map_digits_add_mul: ∏ g(dᵢ) over the digits of j + b * y is g j times the product over the digits of y, whenever g 0 = 1.
• Nat.Prime.not_dvd_prod_factorial_digits: p does not divide the product of the factorials of the base-p digits of n.
• Nat.sub_one_mul_sum_div_pow_succ_eq_sub_sum_digits: Legendre's identity (b - 1) ∑_{i < f} ⌊a / b ^ (i + 1)⌋ = a - s(a) for a < b ^ f, summed over a fixed range.
• Nat.pow_mul_mod_pow_add_sub_one: b ^ i * a % (b ^ (i + k) - 1) is the cyclic shift a / b ^ k + b ^ i * (a % b ^ k) of the digits of a < b ^ (i + k) - 1.
• Nat.sub_one_mul_sum_pow_mul_mod_eq_mul_sum_digits: the sum of the cyclic shifts, (b - 1) ∑_{i < f} (b ^ i * a % (b ^ f - 1)) = (b ^ f - 1) s(a) for a < b ^ f - 1.
• Nat.sub_one_mul_sum_pow_mul_mod_eq_mul_sum_digits_div_mul: for m ∣ b ^ f - 1 and t < m, (b - 1) ∑_{i < f} (b ^ i * t % m) = m s((b ^ f - 1) / m * t).

References

• S. A. Katre, Gauss–Jacobi sums and Stickelberger's theorem, §3.
• L. C. Washington, Introduction to Cyclotomic Fields, 2nd ed., §6.2.
• Thijmen J. P. Krebs, A more reasonable proof of Cobham's theorem, 2018, arXiv:1801.06704, §3.

theorem Nat.map_val_map_ofNat_digits {b : ℕ} [NeZero b] (hb : 2 ≤ b) (n : ℕ) : List.map Fin.val (List.map (Fin.ofNat b) (b.digits n)) = b.digits n

Mapping canonical digits into Fin b and then taking their values recovers the digits.

theorem Nat.exists_length_eq_ofDigits_eq_of_le_two_mul_pow {b n z : ℕ} (hn : 0 < n) (hz : z ≤ 2 * b ^ n) : ∃ (w : List (Fin (2 * b + 1))), w.length = n ∧ ofDigits b (List.map Fin.val w) = z

Short redundant words cover a doubled radix interval. For n ≥ 1, every z ≤ 2 b ^ n is the base-b value, read least significant digit first, of a word of length exactly n with digits at most 2b. The upper endpoint 2 b ^ n is included; for n = 0 only z = 0 is the value of a word of length n.

theorem Nat.sum_digits_add_mul {b j : ℕ} (hj : j < b) (y : ℕ) : (b.digits (j + b * y)).sum = j + (b.digits y).sum

The digit sum of j + b * y, for a digit j < b, is j plus the digit sum of y.

theorem Nat.prod_map_digits_add_mul {M : Type u_1} [Monoid M] {g : ℕ → M} (hg : g 0 = 1) {b j : ℕ} (hj : j < b) (y : ℕ) : (List.map g (b.digits (j + b * y))).prod = g j * (List.map g (b.digits y)).prod

The product of g over the digits of j + b * y, for a digit j < b and g 0 = 1, is g j times the product of g over the digits of y.

theorem Nat.Prime.not_dvd_prod_factorial_digits {p : ℕ} (hp : Prime p) (n : ℕ) : ¬p ∣ (List.map factorial (p.digits n)).prod

A prime p does not divide the product of the factorials of the base-p digits of n.

theorem Nat.sub_one_mul_sum_div_pow_succ_eq_sub_sum_digits {b f a : ℕ} (ha : a < b ^ f) : (b - 1) * ∑ i ∈ Finset.range f, a / b ^ (i + 1) = a - (b.digits a).sum

Legendre's identity over a fixed range. For a < b ^ f, (b - 1) ∑_{i < f} ⌊a / b ^ (i + 1)⌋ = a - s(a), where s(a) is the base-b digit sum of a. This is Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits with the sum extended by zero terms from log b a + 1 to f.

theorem Nat.pow_mul_mod_pow_add_sub_one {b i k a : ℕ} (ha : a < b ^ (i + k) - 1) : b ^ i * a % (b ^ (i + k) - 1) = a / b ^ k + b ^ i * (a % b ^ k)

Multiplication by b ^ i shifts digits cyclically modulo b ^ (i + k) - 1. For a < b ^ (i + k) - 1, b ^ i * a % (b ^ (i + k) - 1) = a / b ^ k + b ^ i * (a % b ^ k): the top i digits of a move to the bottom.

theorem Nat.sub_one_mul_sum_pow_mul_mod_eq_mul_sum_digits {b f a : ℕ} (ha : a < b ^ f - 1) : (b - 1) * ∑ i ∈ Finset.range f, b ^ i * a % (b ^ f - 1) = (b ^ f - 1) * (b.digits a).sum

The sum of the cyclic shifts of the digits. For a < b ^ f - 1, (b - 1) ∑_{i < f} (b ^ i * a % (b ^ f - 1)) = (b ^ f - 1) s(a), where s(a) is the base-b digit sum of a. Equivalently s(a) = (b - 1) ∑_{i < f} {b ^ i a / (b ^ f - 1)}, with {·} the fractional part.

theorem Nat.sub_one_mul_sum_pow_mul_mod_eq_mul_sum_digits_div_mul {b f m t : ℕ} (hm : m ∣ b ^ f - 1) (ht : t < m) : (b - 1) * ∑ i ∈ Finset.range f, b ^ i * t % m = m * (b.digits ((b ^ f - 1) / m * t)).sum

The digit sum of (b ^ f - 1) / m * t. If m ∣ b ^ f - 1 and t < m, then (b - 1) ∑_{i < f} (b ^ i * t % m) = m s((b ^ f - 1) / m * t), where s is the base-b digit sum.