First Contribution - Simple Lemma about sums of digits

Stream: mathlib4

[Hugh]

Hello, I'm interested in contributing (for my first time) a few simple lemmas about digits and digits sums, starting with the following:

theorem sum_digits_succ_eq_sum_pair_digits {n b}
  (pos_b : 0 < b) :
  ∑ i ∈ Finset.range (b^(n+1)), (b.digits i).sum =
  ∑ p ∈ Finset.range (b^n) ×ˢ Finset.range b,
    (b.digits (b * p.fst + p.snd)).sum

would this be a useful contribution? I'm pretty sure it doesn't exist yet.

[Kenny Lau]

@Hugh welcome to mathlib! I have a few comments about this proposal (and I hope they don't deter you, I only want to make your proposals better):

1. The ×ˢ doesn't seem necessary, it seems like you can just use a double sum there.
2. And then on further inspection, I suspect this has nothing to do with digits! I think this would follow from a more general fact of partitioning $[0, b^{n+1})$ as a cartesian product exactly as you described.
3. In addition to the 1st point, a Loogle search on SProd reveals that there are not many lemmas about SProd (the ×ˢ), which would usually mean that it's not really the idiomatic way to express what you want to express in this scenario.
4. And a minor addition, in your future posts, please add import Mathlib (and other relevant details) so that your code block can just compile as-is, which is called a #mwe.

Happy Lean-ing!

[Weiyi Wang]

This doesn't look like it should be specific to .digits.sum, right? T

Kenny Lau said:

1. In addition to the 1st point, a Loogle search on SProd reveals that there are not many lemmas about SProd (the ×ˢ), which would usually mean that it's not really the idiomatic way to express what you want to express in this scenario.

It is weird that loogle didn't find Finset.sum_product

[Kenny Lau]

I would like to retract my 3rd point above. The correct Loogle search is SProd.sprod, which reveals a lot of lemmas.

So ×ˢ is indeed the preferred way to express cartesian product (and as noted, Finset.sum_product and Finset.sum_product' are also the canonical ways to rewrite into double sum).

[Kenny Lau]

@Hugh So while the exact lemma you proposed might not be suitable for Mathlib, I think the lemmas that this would use would be very welcome!

1. I think you can construct an equivalence (i.e. Equiv) of Fin(b^(i+j)) with Fin(b^i) × Fin(b^j). Let me know if you want me to clarify what this means.
2. And then you can specialise to j=1 easily too.
3. And then you can prove that your formula holds, but with (b.digits ·).sum replaced with any function

[Kenny Lau]

(preferably 3 would also come in 2 versions, one that takes a function on N and one that takes a function on Fin (b^(i+j)))

[Kenny Lau]

if you complete on any of the 3 points above and decide to turn it into a PR, feel free to ping me to review your PR!

[Hugh]

Kenny Lau said:

if you complete on any of the 3 points above and decide to turn it into a PR, feel free to ping me to review your PR!

ok thanks! I'll look into it

[Hugh]

@Kenny Lau Is this what you had in mind?

import Mathlib
theorem sum_digits_pow_add_eq_sum_pair {i j b}
  (pos_b : 0 < b) (f : ℕ → ℕ) :
  ∑ x ∈ Finset.range (b^(i+j)), f x =
  ∑ p ∈ Finset.range (b^i) ×ˢ Finset.range (b^j),
    f (b^j * p.fst + p.snd)

[Kenny Lau]

@Hugh that is indeed closer; that's closer to 3 than to 1, and I would advise you to clear my goals in the stated order; and another thing is that I think I would prefer to see a double sum here.

[Kenny Lau]

and also note that the codomain of f can be generalised to any commutative additive monoid :slight_smile:

[Kenny Lau]

oh and of course everything should work out so that you wouldn't need b>0

[Hugh]

Kenny Lau said:

Hugh So while the exact lemma you proposed might not be suitable for Mathlib, I think the lemmas that this would use would be very welcome!

1. I think you can construct an equivalence (i.e. Equiv) of Fin(b^(i+j)) with Fin(b^i) × Fin(b^j). Let me know if you want me to clarify what this means.
2. And then you can specialise to j=1 easily too.
3. And then you can prove that your formula holds, but with (b.digits ·).sum replaced with any function

I should try to prove this first then?

import Mathlib
instance fin_add_equiv_pair {b i j} : Fin (b^(i+j)) ≃ (Fin (b^i) × Fin (b^j)) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

[Aaron Liu]

my solution

import Mathlib

def fin_add_equiv_pair {b i j} : Fin (b ^ (i + j)) ≃ (Fin (b ^ i) × Fin (b ^ j)) :=
  (finCongr (Nat.pow_add b i j)).trans finProdFinEquiv.symm

[Aaron Liu]

also it shouldn't be an instance

[Kenny Lau]

aha, completely missed that generalisation

[Kenny Lau]

it has nothing to do with b^i and b^j anymore

[Kenny Lau]

but i think this might still be worth adding because b^(i+j) is not defeq to b^i * b^j?

[Hugh]

Ok I have:

import Mathlib

theorem sum_add_eq_sum_parts {α : Type*}
  [AddCommMonoidWithOne α] {f : α → α} {i j b : ℕ} :
  ∑ x ∈ Finset.range (b^(i+j)), f x =
  ∑ x ∈ Finset.range (b^i), ∑ y ∈ Finset.range (b^j),
    f (b^j * x + y : ℕ)

should I make a PR for it? (I didn't understand if the fintype equiv makes this redundant)

[Hugh]

oh and its an AddCommMonoidWithOne because I didn't see how to make the definition compile without it, but maybe AddCommMonoid is enough?

[Aaron Liu]

you need AddCommMonoidWithOne for the NatCast

[Aaron Liu]

you should make f : ℕ → α and then it will work with just AddCommMonoid α

[Kenny Lau]

Hugh said:

Ok I have:

import Mathlib

theorem sum_add_eq_sum_parts {α : Type*}
  [AddCommMonoidWithOne α] {f : α → α} {i j b : ℕ} :
  ∑ x ∈ Finset.range (b^(i+j)), f x =
  ∑ x ∈ Finset.range (b^i), ∑ y ∈ Finset.range (b^j),
    f (b^j * x + y : ℕ)

should I make a PR for it? (I didn't understand if the fintype equiv makes this redundant)

yes, but did you also do the generalisations we suggested?

[Antoine Chambert-Loir]

My impression is that b ^i and b ^j can be replaced by arbitrary natural numbers a and b, and then b ^ (i +j) becomes a * b, so that this is all about an equiv of Finset.range (a * b) with the product of Finset.range a and Finset.range b.

[Aaron Liu]

this is starting to look like docs#Equiv.sum_comp with docs#finProdFinEquiv followed by docs#Finset.sum_product but using Finset.range instead of Fintype.univ over Fin

[Hugh]

Kenny Lau said:

Hugh said:

Ok I have:

import Mathlib

theorem sum_add_eq_sum_parts {α : Type*}
  [AddCommMonoidWithOne α] {f : α → α} {i j b : ℕ} :
  ∑ x ∈ Finset.range (b^(i+j)), f x =
  ∑ x ∈ Finset.range (b^i), ∑ y ∈ Finset.range (b^j),
    f (b^j * x + y : ℕ)

should I make a PR for it? (I didn't understand if the fintype equiv makes this redundant)

yes, but did you also do the generalisations we suggested?

I have this working (exponents generalized):

import Mathlib
theorem sum_add_eq_sum_pair {α : Type*}
  [AddCommMonoid α] {f : ℕ → α} {i j : ℕ} :
  ∑ x ∈ Finset.range (i*j), f x =
  ∑ p ∈ Finset.range (i) ×ˢ Finset.range (j),
    f (j * p.fst + p.snd)

I have been trying to do what @Aaron Liu suggested:

import Mathlib
theorem sum_add_eq_sum_pair' {α : Type*}
  [AddCommMonoid α] {i j : ℕ} {f : ℕ → ℕ} :
  ∑ x : Fin (i*j), f x =
  ∑ p : Finset.range i ×ˢ Finset.range j,
    f (j * p.1.fst + p.1.snd) := by
  have := @Equiv.sum_comp ℕ _ _ _ (ι := Fin i × Fin j) (κ := Fin (i*j))
    (e := finProdFinEquiv) (g := λ x => f x)
  simp at this
  rw [<- Finset.sum_range] at this

but I have no idea what I'm doing when it comes to casting between Fin and Finset.range. If the second one is best, any advice on how to finish it is much appreciated.

[Aaron Liu]

docs#Finset.sum_range

[Hugh]

Aaron Liu said:

docs#Finset.sum_range

That works to rewrite the equivalence but after having to change f to Nat -> Nat I'm having trouble finishing the equality. It seems like the expressions are equal, its just the types that aren't.

[Aaron Liu]

that's not possible

[Aaron Liu]

what does congr give you?

[Hugh]

Three goals: Fin (i * j) = { x // x ∈ Finset.range i ×ˢ Finset.range j }
HEq (Fin.fintype (i * j)) (Finset.Subtype.fintype (Finset.range i ×ˢ Finset.range j))
HEq (fun x ↦ f ↑x) fun p ↦ f (j * (↑p).1 + (↑p).2)
It seems like the last one isn't possible to prove

[Aaron Liu]

so clearly you have different expressions

[Hugh]

Which probably means I'm using the wrong g in the sum equiv?

[Aaron Liu]

by the way none of these are possible to prove

[Aaron Liu]

Hugh said:

Which probably means I'm using the wrong g in the sum equiv?

you should use docs#Equiv.sum_congr along with docs#finProdFinEquiv

[Aaron Liu]

and it looks like you got { x // x ∈ Finset.range i ×ˢ Finset.range j } somehow so undo that by using docs#Finset.sum_coe_sort along with docs#Finset.sum_product and docs#Finset.sum_range and docs#Fintype.sum_prod_type' to go back to Fin i × Fin j

[Hugh]

Thank you, you helped me notice I was using Finset.range as a type. I now have:

import Mathlib
theorem sum_add_eq_sum_pair {α : Type*}
  [AddCommMonoid α] {i j : ℕ} {f : ℕ → α} :
  ∑ x : Fin (i*j), f x =
  ∑ p : Fin i × Fin j,
    f (j * p.fst + p.snd : ℕ) := by
  have := @Equiv.sum_comp α _ _ _ (ι := Fin i × Fin j) (κ := Fin (i*j))
    (e := finProdFinEquiv) (g := λ x => f x)
  simp [<- this, add_comm]

proven, and I'm going to try to use it to prove the rest.

[Hugh]

Alright, I have

import Mathlib
theorem sum_range_mul_eq_sum_pair {α : Type*}
  [AddCommMonoid α] {f : ℕ → α} {i j : ℕ} :
  ∑ x ∈ Finset.range (i*j), f x =
  ∑ p ∈ Finset.range i ×ˢ Finset.range j,
    f (j * p.fst + p.snd) := by
  simp [sum_add_eq_sum_pair, Finset.sum_range, Fintype.sum_prod_type,
    Finset.sum_product
  ]

I tried to put them in Algebra/BigOperators/Group/Finset/Sigma.lean but its missing the Fintype import. It feels like they should really go in separate files anyways, but I'm not sure where?

[Hugh]

Maybe this one would be more useful?

import Mathlib
theorem sum_digit_sum_base_pow_eq {k b : ℕ} (pos_k : 0 < k) (hb : 1 < b) :
    2 * ∑ n ∈ Finset.range (b^k), (b.digits n).sum = (b-1) * k * b^k

[Kenny Lau]

@Hugh neither assumptions are necessary

[Kenny Lau]

and i would prefer /2

[Aaron Liu]

If it's in Nat then the /2 statement is strictly weaker

[Kenny Lau]

is it?

[Aaron Liu]

You need to prove the rhs is even in order to cancel the 2

[Kenny Lau]

import Mathlib.Data.ZMod.Basic

theorem two_dvd_pred_mul_self (n : ℕ) : 2 ∣ (n - 1) * n := by
  obtain _ | n := n
  · decide
  rw [Nat.add_sub_cancel, ← ZMod.natCast_eq_zero_iff]
  simp only [Nat.cast_mul, Nat.cast_add, Nat.cast_one]
  generalize (n : ZMod 2) = a; decide +revert

theorem two_dvd_pred_mul_mul_pow (b k : ℕ) : 2 ∣ (b - 1) * k * b^k := by
  obtain _ | k := k
  · simp
  rw [mul_right_comm, pow_succ', ← mul_assoc, mul_assoc (_ * _)]
  exact (two_dvd_pred_mul_self b).trans (dvd_mul_right _ _)

[Aaron Liu]

See? 10 extra lines.

[Hugh]

Kenny Lau said:

Hugh neither assumptions are necessary

PR is up for a version without the assumptions. Personally I prefer without division, but I'm happy to change it and/or add two versions, like for the original Gauss sum.

[Kenny Lau]

link?

[Hugh]

Kenny Lau said:

link?

https://github.com/leanprover-community/mathlib4/pull/27242

[Hugh]

How can I generalize these lemmas to an f : Fin (a * b) -> M?

@[to_additive]
theorem prod_mul_eq_prod_product {a b : ℕ} {f : ℕ → M} :
    ∏ x : Fin (a * b), f x = ∏ i : Fin a, ∏ j : Fin b, f (b * i + j) := by
  have := @Equiv.prod_comp M _ _ _ (ι := Fin a × Fin b) (κ := Fin (a * b))
    (e := finProdFinEquiv) (g := fun x => f x)
  simp [<- this, add_comm, <- Finset.prod_product']

@[to_additive]
theorem prod_range_mul_eq_prod_product {a b : ℕ} {f : ℕ → M} :
    ∏ x ∈ Finset.range (a * b), f x = ∏ i : Fin a, ∏ j : Fin b, f (b * i + j) := by
  simp [prod_mul_eq_prod_product, Finset.prod_range]