divisibilty of powers

Stream: Is there code for X?

[Niels Voss]

In my PR, I also proved the following statements

lemma odd_pow_lem (a : ℤ) (n k : ℕ) (h₁ : k ∣ n) (h₂ : odd (n / k)) : a^k + 1 ∣ a^n + 1
lemma sub_one_dvd_pow_sub_one (a n : ℕ) (h : 1 ≤ a) : a - 1 ∣ a^n - 1

I wasn't able to find these in mathlib. Technically I only need the case when k = 1 for odd_pow_lem. If they aren't already in mathlib, do they belong?
I also have proofs of the more general lemma ab_lem (a b n : ℕ) : (a - b) ∣ (a^n - b^n) and Kevin Buzzard suggested that I reformalize odd_pow_lem as lemma odd_pow_lem (a : ℤ) (q k : ℕ) (h₂ : odd q) : a^k + 1 ∣ a^(q * k) + 1 to avoid natural number division.

[Yaël Dillies]

@Mantas Baksys, thoughts?

[Martin Dvořák]

I think that lemma ab_lem (a b n : ℕ) : (a - b) ∣ (a^n - b^n) is extremely useful.

[Martin Dvořák]

This one is not in your PR, is it?

[Niels Voss]

It used to be, but I removed it because I only ever used the b = 1 case.
It has a (ungolfed) proof here

[Kevin Buzzard]

I would say that odd_pow_lem is better stated off as odd q -> a + 1 | a^q + 1 avoiding natural division and the divisibility hypothesis, and then you can apply with a = a^k if you want your version. As for sub_one_dvd_pow_sub_one I think it's probably better stated for a : int, and deduced for naturals afterwards (note that it looks true for a=0 so h should be removed in the final version, but you can do cases on a when proving the natural version)

[Martin Dvořák]

Niels Voss said:

It used to be, but I removed it because I only ever used the b = 1 case.
It has a (ungolfed) proof here

Nice!

Just one comment... for me, the terms with "triangle" are hard to read.
Instead of:

exact (eq.symm h₈) ▸ h₇

I'd write:

rwa ←h₈ at  h₇

[Michael Stoll]

docs#geom_sum₂_mul and friends might be useful.

[Michael Stoll]

(This came up in my seminar a while ago. I was certain I had seen this somewhere in mathlib, but could not find it when I was looking for it. The name is not what I had expected...)

[Niels Voss]

I would say that odd_pow_lem is better stated off as odd q -> a + 1 | a^q + 1 avoiding natural division and the divisibility hypothesis, and then you can apply with a = a^k if you want your version.

I agree, for some reason it never occurred to me that the two forms are actually equivalent

[Niels Voss]

Here are some short proofs of ab_lem for ℤ and ℕ using the lemma Michael Stoll suggested

private lemma ab_lem (a b : ℤ) (n : ℕ) : a - b ∣ a^n - b^n :=
dvd.intro_left _ (geom_sum₂_mul a b n)

private lemma ab_lem' (a b n : ℕ) : a - b ∣ a^n - b^n :=
begin
  by_cases h : b ≤ a,
  { have : b^n ≤ a^n := nat.pow_le_pow_of_le_left h _,
    exact_mod_cast ab_lem ↑a ↑b n },
  { have : a^n ≤ b^n := nat.pow_le_pow_of_le_left (show a ≤ b, by linarith) _,
    exact (nat.sub_eq_zero_iff_le.mpr this).symm ▸ dvd_zero (a - b) }
end

[Junyan Xu]

You can cases le_total b a

[Kevin Buzzard]

Or split on le_or_lt.

[Niels Voss]

This link suggests that for all a, b, n where n is odd then a + b ∣ a^n + b^n, which is basically a more general version of what I proved. Since geom_sum₂_mul is in the library, is there something similar for sums of odd powers?

[Eric Rodriguez]

docs#geom_sum₂_mul

[Eric Rodriguez]

oh great the linkifier is broken

[Eric Rodriguez]

geom_sum2_mul seems to pretty much be that lemma with x = a, y = -b, no?

[Niels Voss]

Yeah it does, I was just wondering if there was a more convenient form to use

[Eric Rodriguez]

I don't think so, I also don't think a PR that makes it would be unwelcome though! not sure how far away geom_sum is from a port but some lemma called odd.pow_add_X or something of the sort would be nice

[Niels Voss]

I tried proving that (finset.range n).sum (λ (i : ℕ), (-1)^i * a ^ i * b ^ (n - 1 - i)) * (a + b) = a^n + b^n. Proving that (finset.range n).sum (λ (i : ℕ), (a ^ i * (-b) ^ (n - 1 - i)) * (a + b) = a^n + b^n is basically a direct result of geom_sum₂_mul. Proving that the two finset sums are equal is harder, as it requires showing that (-1 : ℤ) ^ i = (-1) ^ (n - 1 - i), for odd n, which is not true in general due to how natural number subtraction works.

I don't actually care about what is inside the finset sum for my PR because it only depends on divisibility, but I could try finishing the proof if it would be helpful to have in the library.

[Eric Rodriguez]

I'd say just upload the divisibility proof and if people want the "proper" proof, they'll ask. Mention these details in the PR description!

[Niels Voss]

Which file and namespace would these go into? I'm planning on doing a - b | a^n - b^n and odd n -> a + b | a^n + b^n for both a b : nat and a b : int (maybe it works for any comm ring in general)?

[Eric Rodriguez]

I'd try to stick to comm_rings if you can, I find it unlikely it'd be accepted for a b : int only. I'd put the second one in the odd namespace (not sure about the name) and the first one, I'd call sub_dvd_pow_sub_pow maybe?

[Niels Voss]

I don't know how far down the import chain algebra.geom_sum is, but I'd imagine it would be after data.nat.parity. Should these just go in algebra.geom_sum?

[Junyan Xu]

It may be easier to plug in x = -a, y = b into geom_sum2_mul to get

(finset.range n).sum (λ (i : ℕ), (-a) ^ i * b ^ (n - 1 - i)) * (-a - b) = (-a) ^ n - b ^ n

and cancel a minus sign from both sides (when n is odd).

[Niels Voss]

That definitely would help if I was trying to provide a version of geom_sum₂_mul for subtraction. I don't think it matters for just divisibility though.
It would avoid all problems with natural number subtraction in my attempted proof above though.

[Kevin Buzzard]

@Niels Voss I don't understand why docs#geom_sum₂_mul doesn't solve all your problems? What are you trying to prove?

[Kevin Buzzard]

To get a + b ∣ a^n + b^n for n odd and a, b naturals, just prove it for integers and then observe that a natural divides another one iff the corresponding integer divides the other one.

[Niels Voss]

It does, I just thought that it would be nice if the lemmas were in a more convenient and library_search friendly form for the rest of the library. If this isn't necessary, my PR could just use geom_sum₂_mul directly.

[Kevin Buzzard]

I was just referring to the fact that you seemed to be re-proving results about (finset.range n).sum (λ (i : ℕ), (-1)^i * a ^ i * b ^ (n - 1 - i)), which should not be necessary. You don't want to go there.

[Niels Voss]

Yeah, I don't really know why I was trying to do that (I guess I thought it would add something to algebra.geom_sum?) but you are right that it isn't necessary for divisibility.

[Niels Voss]

Here's what I have so far:

theorem sub_dvd_pow_sub_pow [comm_ring α] (x y : α) (n : ℕ) : x - y ∣ x^n - y^n :=
  dvd.intro_left _ (geom_sum₂_mul x y n)

theorem nat.sub_dvd_pow_sub_pow (x y n : ℕ) : x - y ∣ x^n - y^n :=
begin
  cases le_or_lt y x with h,
  { have : y^n ≤ x^n := nat.pow_le_pow_of_le_left h _,
    exact_mod_cast sub_dvd_pow_sub_pow (x : ℤ) ↑y n },
  { have : x^n ≤ y^n := nat.pow_le_pow_of_le_left h.le _,
    exact (nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y) }
end

theorem odd.add_dvd_pow_add_pow [comm_ring α] (x y : α) {n : ℕ} (h : odd n) : x + y ∣ x^n + y^n :=
begin
  have h₁ := geom_sum₂_mul x (-y) n,
  rw [odd.neg_pow h y, sub_neg_eq_add, sub_neg_eq_add] at h₁,
  exact dvd.intro_left _ h₁,
end

theorem nat.add_dvd_pow_add_pow_of_odd (x y : ℕ) {n : ℕ} (h : odd n) : x + y ∣ x^n + y^n :=
by exact_mod_cast odd.add_dvd_pow_add_pow (x : ℤ) ↑y h

I don't really know if I should change any of the names.

[Kevin Buzzard]

Nice!

import tactic
import algebra.geom_sum

variable {α : Type*}

for the #mwe

[Niels Voss]

Oh yeah, sorry I forgot to mention that this is in algebra/geom_sum.lean (outside of any namespace though). It can be moved if needed.

[Niels Voss]

As a general guideline, is there always a space between x and ^ in x ^ y? Because I haven't always been adding them.

[Kevin Buzzard]

I always put them in, others often don't; it's a bit weird because usually there are concrete conventions for everything.

[Martin Dvořák]

I put them too.

[Yaël Dillies]

It is an infix operator. As such, it should get spaces around it. But this rule is loosely enforced.