Proof of Euler's product formula for totient

Stream: new members

[Stuart Presnell]

I've formalised a proof of Euler's product formula for the totient function φ

↑(φ n) = ↑n * ∏ p in (prime_divisors n), (1 - p⁻¹:ℚ)

I've separately defined prime_divisors and proved a few basic lemmas that are used in the above proof

def prime_divisors (n:ℕ) := (divisors n).filter prime

which I guess best belongs in number_theory/divisors.

I'm guessing it would be best to submit the latter material as a PR first, and then if that's accepted I'll submit the product formula proof as another PR separately.

[Johan Commelin]

Is divisors available in data.nat.prime? If so, I would add prime_divisors there.

[Ruben Van de Velde]

Hmm, I'm surprised we don't have anything like prime_divisors yet - I was looking at docs#nat.factors, but that's with multiplicity

[Ruben Van de Velde]

Would it be equal to n.factors.to_finset?

[Stuart Presnell]

Johan Commelin said:

Is divisors available in data.nat.prime? If so, I would add prime_divisors there.

Looks like divisors isn't available in data.nat.prime.

[Stuart Presnell]

I've seen one or two Zulip threads on the lack of a finset-valued prime divisors function, which no-one seemed to have acted on since the topic came up.

[Stuart Presnell]

I briefly had a go at proving that it's equal to list.to_finset (factors n) but didn't finish it, mostly because I didn't need that for what I was doing.

[Stuart Presnell]

Ok, I've just added the proof that n.prime_divisors = n.factors.to_finset.

[Stuart Presnell]

Would it be better for some reason to define prime_divisors as n.factors.to_finset (and then prove the equality with (divisors n).filter prime as a lemma)?
[Of course, one answer to that question is "Try it and see if it makes anything easier"! But I'm hoping the voice of experience can swoop in to save me from having to try that experiment. :) ]

[Stuart Presnell]

Submitted the material on prime_divisors as PR #10318

[Kevin Buzzard]

@Chris Birkbeck the product formula should make the "classify roots of unity in cyclotomic fields" question from #FLT regular much easier

[Chris Birkbeck]

Yes, this should hopefully help with one of the totient proofs I've been stuck on :)

[Stuart Presnell]

Is it easy/reasonable to submit the proof as a PR that depends on the one that's currently under submission (#10318)? Or should I wait until that's accepted and merged?

[Stuart Presnell]

While I'm waiting to decide what to do, maybe I can ask for some help in improving the proof. At one point I end up needing to prove the following equality. My first draft was quite messy so I took it out as a lemma to work on it separately. Here's what I ended up with:

lemma euler_lemma1 {p m : ℕ} (hm : 0 < m) (hp: 0 < p) :
  ↑p ^ (m - 1) * ↑(p - 1) = ↑p ^ m - ↑p ^ m * (↑p:ℚ)⁻¹  :=
begin
  have hp' : 1 ≤ p := by linarith,
  rw [(nat.cast_sub hp'), mul_sub],

  have hm' : 1 ≤ m := by linarith,
  have := pow_sub_mul_pow ↑p hm',
  simp at this, rw this, simp,
  rw [←this, mul_assoc],

  have hp' : (↑p:ℚ) ≠ 0, by {intro H, finish},
  rw mul_inv_cancel hp', simp,
end

Is there a nicer way to prove this — some clever tactics for working in ℚ that I've missed?

[Alex J. Best]

Yes its possible to submit PRs that build on each other, and we have tools to help organise this, see e.g. https://github.com/leanprover-community/mathlib/pull/10255 you just have to put

- [ ] depends on: #10318

below the

---

line in the PR message, and the bots will automatically tag it with appropriate labels and let you know when its ready

[Alex J. Best]

In this case you should make the second branch based off of the branch for the first PR so that it all builds sucessfully in both PRs, then when the first is merged you can do git pull master and git push in the second branch to make the new diff against master now

[Alex J. Best]

I haven't tried to play with the code, bu I see some casts, so the tactic#norm_cast family (tactic#exact_mod_cast tactic#push_cast tactic#rw_mod_cast etc) might be useful to you. Maybe tactic#field_simps too, which is good for putting things over a common denominator.

[Stuart Presnell]

Great, thanks very much

[Alex J. Best]

There is also tactic#assoc_rw, which might shave a line off your proof, but it becomes very useful when you have to do a lot of manual mul_assocs

[Alex J. Best]

I'd try to avoid using finish in a PR to mathlib if I could, it can be quite slow unfortunately

[Alex J. Best]

Also it looks like you have a glossary#non-terminal-simp, which can be quite brittle so we avoid that pattern in mathlib

[Stuart Presnell]

Thanks so much for your help!

[Kevin Buzzard]

import tactic
import data.rat.basic

lemma euler_lemma1 {p m : ℕ} (hm : 0 < m) (hp: 0 < p) :
  ↑p ^ (m - 1) * ↑(p - 1) = ↑p ^ m - ↑p ^ m * (↑p:ℚ)⁻¹  :=
begin
  have : (p : ℚ) ≠ 0 := by simp [(ne_of_lt hp).symm],
  field_simp,
  cases m, cases hm,
  cases p, cases hp,
  simp [nat.succ_eq_add_one],
  ring_exp,
end

[Stuart Presnell]

Wow, that's so much nicer! Thanks!

[Kevin Buzzard]

It's a lazy proof -- I want to solve this by ring so I just keep trying ring until it works. The first problem is that I need to clear denominators so I do this with field_simp but that tactic isn't smart enough to construct the proof that (p : Q) isn't zero so I have to do it myself (I feed in the proof that it's non-zero as a natural because I knew simp could take it from there). The next issue is that you have used natural subtraction twice. For me, this is unidiomatic, because natural subtraction is not a sensible function; lots of things aren't true for it and it screws up automation. For me, hm : 0 < m and m-1 together tell me that you've stated this lemma suboptimally: m should be n+1 and there should be no inequality or natural subtraction, if you can possibly help it; that would save the cases m line and the succ_eq_add_one line; I was proving what was put in front of me, not what I would have formalised myself. Having eliminated both nat subtractions with this cases hack I then have to deal with the fact that my hack introduced succs, which I removed and then finally it worked.

[Stuart Presnell]

Ok, I'll see what I can do to reformulate it. I think I can see what I need to change.

[Stuart Presnell]

@Ruben Van de Velde suggested a couple of days ago that my definition of prime_divisors should be equal to factors.to_finset, which it turned out was correct, and I might have saved myself some work if I'd paid more attention to that point.

With that in mind I'd like to check whether another definition would be worth having:

def prime_factorization (n:ℕ) := (n.factors.to_finset).image (λ p, (p, n.factors.count p))
#eval (prime_factorization 1200)     -- {(2, 4), (3, 1), (5, 2)}   since 1200 = 2^4 * 3^1 * 5^2

Is something like this already defined in mathlib? Is there a nicer way to express it?

[Eric Rodriguez]

just don't to_finset it ;b factors is an ordered list of the prime factors, including multiplicity

[Eric Rodriguez]

oh, sorry, I read it wrong. anyways, I'm sure there must be a list/multiset function that counts and places them in a pair like that

[Alex J. Best]

Is it docs#prime_multiset or something like that?

[Stuart Presnell]

In data/pnat/factors we have

factor_multiset (n : ℕ+) : prime_multiset

where prime_multiset := multiset nat.primes. So this gives the multiset of prime factors but not explicitly the counts.

Similarly, in data/nat/prime we have

factors : ℕ → list ℕ

which is the list of all the prime factors but again not the counts.

[Stuart Presnell]

So I suppose whatever purpose might be served by prime_factorization could just as well be served by using factors.to_finset to get the set of prime factors and then extracting the count information by list.count p (factors n).

[Eric Rodriguez]

prime_multiset should be burnt to the ground, IMO. and I think if this should exist, this should exist in the form of a function that maps a multiset to a finset of the original thing and its multiplicity

[Stuart Presnell]

Ha! It certainly seemed a bit unwieldy when I tried using it, and the fact that factor_multiset takes a pnat rather than a nat added an extra little inconvenience.

Is there not already a function that takes a list L to a list (or finset) of pairs (x, count L x)? (I don't know how I would go about searching for such a function.)

[Alex J. Best]

Yes for multiset you still need to take counts, it just seems a more reasonable data type for a prime factorisation than a list

[Yaël Dillies]

Eric Rodriguez said:

prime_multiset should be burnt to the ground.

Yes please

[Eric Wieser]

Are you looking for docs#multiset.to_finsupp?

[Yakov Pechersky]

There's no reason it should be noncomputable.

[Alex J. Best]

Finsupp isn't a particularly computable representation of this data though right?

[Alex J. Best]

Like if you really wanted to compute something a list of pairs seems much more efficient

[Alex J. Best]

That said, I agree a better def than finsupp.to_multiset.symm wouldn't go amiss

[Yakov Pechersky]

I agree that finsupp isn't a useful computable notion. But going from multiset X to finset (X x pnat), which is isomorphic to a subset of finsupp, is what was originally asked for.

[Stuart Presnell]

So on the one hand we have factors : ℕ → list ℕ with list.count to extract the multiplicities. And on the other hand we have factor_multiset : nat → prime_multiset with multiset.to_finsupp to extract the multiplicities. Given the choice, it seems like factors and count is nicer all round. Are there any advantages to going the multiset route that I'm missing?

[Yakov Pechersky]

Did you look at the implementation of multiset.to_finsupp? It also goes through count. What will you be using the counts for? The multiset is more "basic" since there's no inherent order to the prime factorization. The list, iirc, is the result of sorting the prime factors.

[Yakov Pechersky]

So I think your proposed implementation above via image is the appropriate one.

[Alex J. Best]

Yeah you gain some API by using multiset is all, like a notion of less than or equal (which corresponds to the original numbers being divisible by each other), or being able to take unions and sums of multisets, whats better depends on your use case

[Stuart Presnell]

Thanks everyone. I think for now I'll stick with the list-based implementation and see how that goes.

[Eric Wieser]

@Yakov Pechersky, its noncomputable because docs#finsupp.has_add is noncomputable and that's one of the arguments to add_equiv.mk

[Yakov Pechersky]

Yes, that makes sense. I'm just saying the inv_fun of the equiv, which is the forward direction desired here, is computable.

[Stuart Presnell]

After building lots of infrastructure (mostly around prime_factorization) and filling in lots of sorrys I finally have a working sorry-free first draft of the proof. :D

[Stuart Presnell]

Now I have a bunch of refactoring and tidying up to do, then I'll be ready to submit it as a PR.