Digits of a natural number

This provides lemma about the digits of natural numbers.

theorem Nat.ofDigits_eq_sum_mapIdx_aux (b : ℕ) (l : List ℕ) : (List.zipWith (fun (a i : ℕ) => a * b ^ (i + 1)) l (List.range l.length)).sum = b * (List.zipWith (fun (a i : ℕ) => a * b ^ i) l (List.range l.length)).sum

theorem Nat.ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) : ofDigits b L = (List.mapIdx (fun (i a : ℕ) => a * b ^ i) L).sum

Properties

This section contains various lemmas of properties relating to digits and ofDigits.

theorem Nat.digits_len (b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) : (b.digits n).length = log b n + 1

theorem Nat.digits_length_le_iff {b k : ℕ} (hb : 1 < b) (n : ℕ) : (b.digits n).length ≤ k ↔ n < b ^ k

theorem Nat.lt_digits_length_iff {b k : ℕ} (hb : 1 < b) (n : ℕ) : k < (b.digits n).length ↔ b ^ k ≤ n

theorem Nat.getLast_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) : (b.digits m).getLast ⋯ ≠ 0

theorem Nat.digits_append_digits {b m n : ℕ} (hb : 0 < b) : b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)

theorem Nat.digits_append_zeroes_append_digits {b k m n : ℕ} (hb : 1 < b) (hm : 0 < m) : b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ ((b.digits n).length + k) * m)

theorem Nat.digits_len_le_digits_len_succ (b n : ℕ) : (b.digits n).length ≤ (b.digits (n + 1)).length

theorem Nat.le_digits_len_le (b n m : ℕ) (h : n ≤ m) : (b.digits n).length ≤ (b.digits m).length

theorem Nat.pow_length_le_mul_ofDigits {b : ℕ} {l : List ℕ} (hl : l ≠ []) (hl2 : l.getLast hl ≠ 0) : (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l

theorem Nat.base_pow_length_digits_le' (b m : ℕ) (hm : m ≠ 0) : (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m

Any non-zero natural number m is greater than (b+2)^((number of digits in the base (b+2) representation of m) - 1)

theorem Nat.base_pow_length_digits_le (b m : ℕ) (hb : 1 < b) : m ≠ 0 → b ^ (b.digits m).length ≤ b * m

Any non-zero natural number m is greater than b^((number of digits in the base b representation of m) - 1)

theorem Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digits {p : ℕ} (L : List ℕ) {h_nonempty : L ≠ []} (h_ne_zero : L.getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ L, l < p) : (p - 1) * ∑ i ∈ Finset.range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

theorem Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : ℕ} (n : ℕ) : (p - 1) * ∑ i ∈ Finset.range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Binary

theorem Nat.digits_two_eq_bits (n : ℕ) : digits 2 n = List.map (fun (b : Bool) => bif b then 1 else 0) n.bits

Modular Arithmetic

theorem Nat.dvd_ofDigits_sub_ofDigits {α : Type u_1} [CommRing α] {a b k : α} (h : k ∣ a - b) (L : List ℕ) : k ∣ ofDigits a L - ofDigits b L

theorem Nat.ofDigits_modEq' (b b' k : ℕ) (h : b ≡ b' [MOD k]) (L : List ℕ) : ofDigits b L ≡ ofDigits b' L [MOD k]

theorem Nat.ofDigits_modEq (b k : ℕ) (L : List ℕ) : ofDigits b L ≡ ofDigits (b % k) L [MOD k]

theorem Nat.ofDigits_mod (b k : ℕ) (L : List ℕ) : ofDigits b L % k = ofDigits (b % k) L % k

theorem Nat.ofDigits_mod_eq_head! (b : ℕ) (l : List ℕ) : ofDigits b l % b = l.head! % b

theorem Nat.head!_digits {b n : ℕ} (h : b ≠ 1) : (b.digits n).head! = n % b

theorem Nat.ofDigits_zmodeq' (b b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD ↑k]) (L : List ℕ) : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]

theorem Nat.ofDigits_zmodeq (b : ℤ) (k : ℕ) (L : List ℕ) : ofDigits b L ≡ ofDigits (b % ↑k) L [ZMOD ↑k]

theorem Nat.ofDigits_zmod (b : ℤ) (k : ℕ) (L : List ℕ) : ofDigits b L % ↑k = ofDigits (b % ↑k) L % ↑k

theorem Nat.modEq_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) : n ≡ (b'.digits n).sum [MOD b]

theorem Nat.zmodeq_ofDigits_digits (b b' : ℕ) (c : ℤ) (h : ↑b' ≡ c [ZMOD ↑b]) (n : ℕ) : ↑n ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

theorem Nat.ofDigits_neg_one (L : List ℕ) : ofDigits (-1) L = (List.map (fun (n : ℕ) => ↑n) L).alternatingSum

theorem Nat.getD_digits (n i : ℕ) {b : ℕ} (h : 2 ≤ b) : (b.digits n).getD i 0 = n / b ^ i % b

Explicit computation of the i-th digit of n in base b.

Bijection

def Nat.digitsAppend (b l n : ℕ) : List ℕ

The list of digits of n in base b with some 0's appended so that its length is equal to l if it is < l. This is an inverse function of Nat.ofDigits for n < b ^ l, see Nat.setInvOn_digitsAppend_ofDigits. If n ≥ b ^ l, then the list of digits of n in base b is of length at least l and this function just return b.digits n.

Equations

• b.digitsAppend l n = b.digits n ++ List.replicate (l - (b.digits n).length) 0

theorem Nat.length_digitsAppend {n b : ℕ} (hb : 1 < b) (l : ℕ) (hn : n < b ^ l) : (b.digitsAppend l n).length = l

theorem Nat.lt_of_mem_digitsAppend {n b : ℕ} (hb : 1 < b) (l i : ℕ) (hi : i ∈ b.digitsAppend l n) : i < b

theorem Nat.mapsTo_ofDigits {b : ℕ} (hb : 1 < b) (l : ℕ) : Set.MapsTo (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} {n : ℕ | n < b ^ l}

theorem Nat.mapsTo_digitsAppend {b : ℕ} (hb : 1 < b) (l : ℕ) : Set.MapsTo (b.digitsAppend l) {n : ℕ | n < b ^ l} {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}

theorem Nat.injOn_ofDigits {b : ℕ} (hb : 1 < b) (l : ℕ) : Set.InjOn (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}

theorem Nat.setInvOn_digitsAppend_ofDigits {b : ℕ} (hb : 1 < b) (l : ℕ) : Set.InvOn (b.digitsAppend l) (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} {n : ℕ | n < b ^ l}

theorem Nat.bijOn_ofDigits {b : ℕ} (hb : 1 < b) (l : ℕ) : Set.BijOn (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} {n : ℕ | n < b ^ l}

The map L ↦ Nat.ofDigits b L is bijection between the set of lists of natural integers of length l with coefficients < b to the set of natural integers < b ^ l.

theorem Nat.bijOn_digitsAppend {b : ℕ} (hb : 1 < b) (l : ℕ) : Set.BijOn (b.digitsAppend l) {n : ℕ | n < b ^ l} {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}

The map n ↦ Nat.digitsAppend b L is bijection between the set of natural integers < b ^ l to the set of lists of natural integers of length l with coefficients < b to .

theorem Nat.sum_digits_ofDigits_eq_sum {b : ℕ} (hb : 1 < b) {l : ℕ} {L : List ℕ} (hL : L ∈ {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}) : (b.digits (ofDigits b L)).sum = L.sum

noncomputable def List.fixedLengthDigits {b : ℕ} (hb : 1 < b) (l : ℕ) : Finset (List ℕ)

The set of lists of natural integers of length l with coefficients < b as a Finset. This can be seen as the set of lists of length l of the digits in base b of the integers < b ^ l. Having this set as a Finset can be helpful for some proofs.

Equations

• List.fixedLengthDigits hb l = {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}.toFinset

theorem List.mem_fixedLengthDigits_iff {b : ℕ} (hb : 1 < b) {l : ℕ} {L : List ℕ} : L ∈ fixedLengthDigits hb l ↔ L.length = l ∧ ∀ x ∈ L, x < b

theorem Nat.bijOn_ofDigits' {b : ℕ} (hb : 1 < b) (l : ℕ) : Set.BijOn (ofDigits b) ↑(List.fixedLengthDigits hb l) ↑(Finset.range (b ^ l))

The bijection Nat.bijOn_ofDigits stated as a bijection between Finset. This spelling can be helpful for some proofs.

theorem Nat.bijOn_digitsAppend' {b : ℕ} (hb : 1 < b) (l : ℕ) : Set.BijOn (b.digitsAppend l) ↑(Finset.range (b ^ l)) ↑(List.fixedLengthDigits hb l)

The bijection Nat.bijOn_digitsAppend stated as a bijection between Finset. This spelling can be helpful for some proofs.

@[simp]

theorem List.fixedLengthDigits_zero {b : ℕ} (hb : 1 < b) : fixedLengthDigits hb 0 = {[]}

@[simp]

theorem List.fixedLengthDigits_one {b : ℕ} (hb : 1 < b) : fixedLengthDigits hb 1 = Finset.image (fun (x : ℕ) => [x]) (Finset.range b)

theorem List.card_fixedLengthDigits {b : ℕ} (hb : 1 < b) (l : ℕ) : (fixedLengthDigits hb l).card = b ^ l

noncomputable def List.consFixedLengthDigits {b : ℕ} (hb : 1 < b) (l d : ℕ) : Finset (List ℕ)

The Finset of lists whose head is a fixed integer d and tail is a list in List.fixedLengthDigits b l.

Equations

• List.consFixedLengthDigits hb l d = Finset.image (fun (L : List ℕ) => d :: L) (List.fixedLengthDigits hb l)

theorem List.ne_empty_of_mem_consFixedLengthDigits {b : ℕ} (hb : 1 < b) {l d : ℕ} {L : List ℕ} (hL : L ∈ consFixedLengthDigits hb l d) : L ≠ []

theorem List.consFixedLengthDigits_head {b : ℕ} (hb : 1 < b) {l d : ℕ} {L : List ℕ} (hL : L ∈ consFixedLengthDigits hb l d) : L.head ⋯ = d

theorem List.cons_mem_fixedLengthDigits_succ {b : ℕ} (hb : 1 < b) (l d : ℕ) (hd : d < b) {L : List ℕ} (hL : L ∈ fixedLengthDigits hb l) : d :: L ∈ fixedLengthDigits hb (l + 1)

If L is a list in List.fixedLengthDigits b l and d is an integer < b, then d :: L is a list in List.fixedLengthDigits b (l + 1).

theorem List.pairwiseDisjoint_consFixedLengthDigits {b : ℕ} (hb : 1 < b) (l : ℕ) : (↑(Finset.range b)).PairwiseDisjoint fun (d : ℕ) => consFixedLengthDigits hb l d

theorem List.fixedLengthDigits_succ_eq_disjiUnion {b : ℕ} (hb : 1 < b) (l : ℕ) : fixedLengthDigits hb (l + 1) = (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯

The set List.fixedLengthDigits b (l + 1) is the disjoint union of the sets List.consFixedLengthDigits b l d where d ranges through the natural integers < d.

theorem List.sum_fixedLengthDigits_sum {b : ℕ} (hb : 1 < b) (l : ℕ) : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2

theorem Nat.sum_sum_digits_eq {b : ℕ} (hb : 1 < b) (l : ℕ) : ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2

The formula for the sum of the sum of the digits in base b over the natural integers < b ^ l.