Prime factorizations

Stream: new members

[Stuart Presnell]

I have the beginnings of a formalisation of prime factorisations (as discussed in this thread: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Proof.20of.20Euler's.20product.20formula.20for.20totient),
defined as

def prime_factorization (n:ℕ) := (n.factors.to_finset).image (λ p, (p, n.factors.count p))

where for example (prime_factorization 1200) is {(2, 4), (3, 1), (5, 2)} since 1200 = 2^4 * 3^1 * 5^2.

It's not the last word on the subject and there's plenty more work to be done at some point — for example, on divisibility. But it covers everything I need for the proof of Euler's product formula for the totient function. The main result, used in that proof, is that for any multiplicative function f and any n > 0 we have

f n = ∏ pk in prime_factorization n, f(pk.1 ^ pk.2)

Where does this material best belong? Should I add this to data/nat/prime, which is already over 1000 lines? Or perhaps in number_theory/divisors? Or would it be better to start a new file?

[Eric Rodriguez]

Can you post your file on a branch somewhere quickly? What imports does it require upon?

Also, I still think that it's better to have some form of function that turns a list/multiset (nat.factors) into a finset with value/m,ultiplicity, with your statement being φ n = pk in (new_function_name n.factors), φ pk.1 ^ pk.2 as this is definitely a useful function.

[Eric Wieser]

Another way of spelling that would be:

def prime_factorization (n:ℕ) : ℕ →₀ ℕ := (n.factors : multiset ℕ).to_finsupp

and then

f n = prime_factorization.sum (λ n r, f(n ^ r))

[Eric Rodriguez]

ahh, yes we did have this discussion before and I forgot

[Eric Wieser]

The nice thing about the ℕ →₀ ℕ approach is that you can do a lookup of a factor in a way that is awkward for the list of pairs

[Eric Wieser]

The downside is that docs#multiset.to_finsupp : multiset α ≃+ (α →₀ ℕ) is noncomputable, but we could easily add a computable version if the type is instead multiset α ≃ (α →₀ ℕ) (it's the + that poisons it)

[Eric Rodriguez]

why is the + noncomputable?

[Eric Wieser]

because docs#finsupp.has_add is noncomputable

[Eric Wieser]

Because it uses classical.dec_eq instead of taking a decidable argument (which I think was a deliberate choice to appease mathematicians)

[Stuart Presnell]

As in the previous discussion, doing this via multiset has a number of disadvantages (amongst others, the involvement of prime_multiset which "should be burnt to the ground").

You're right that there should be a general function list α → finset (α × ℕ), and then I can replace the terminology prime_factorization with the application of this function to n.factors.

[Eric Rodriguez]

I think the finsupp idea is probably best though, still; it's got a huge api, too, as polynomials are built using finsupps

[Eric Wieser]

My comment above doesn't mention prime_multiset, only the coercion of factors to a multiset

[Stuart Presnell]

I've made a small start on refactoring via a new function

def census (l : list α) := (l.to_finset).image (λ a, (a, l.count a))

and posted what I have so far on branch#SP_factorizations_draft_v1.

But as you've suggested, I'll probably end up re-writing this in terms of finsupp instead.

[Stuart Presnell]

Eric Wieser said:

My comment above doesn't mention prime_multiset, only the coercion of factors to a multiset

Ah, sorry, I'd conflated the general use of multiset with the specific approach of using factor_multiset (n : ℕ+) : prime_multiset.

[Yakov Pechersky]

Your census function can, of course, be written to have better general performance, instead of the n ^ 2 (?) performance it is now. But might be more difficult to prove things about it in more performant definitions

[Stuart Presnell]

Ok, I've re-written this all in terms of finsupp (using the definition of prime_factorization proposed earlier in this thread by @Eric Wieser) and posted it at branch#SP_factorizations_draft_v3. I have a few basic utility lemmas, a couple of lemmas about the prime factorizations of coprime a and b, and the main result that for a multiplicative function f we have f n = n.prime_factorization.prod (λ p k, f(p ^ k)).