Stream: maths

Topic: Arithmetic Functions

Aaron Anderson (Sep 13 2020 at 21:43):

I've shelved my PR on perfect numbers for now, but I'm going to try to PR at least some easy parts of it soon.

Aaron Anderson (Sep 13 2020 at 21:44):

It seems like it should be simple enough to define and prove some basic facts about some arithmetic functions, like the number-of-divisors or sum-of-divisors functions, but I'm fretting once again over what type to define them in.

Aaron Anderson (Sep 13 2020 at 21:45):

Standardly arithmetic functions are defined with domain pnat, but the only important nontrivial one we have in mathlib is nat.totient, which is defined on nats.

Aaron Anderson (Sep 13 2020 at 21:47):

I'd also like to define the Dirichlet ring structure, and that's probably going to have to require a type synonym somewhere.

Aaron Anderson (Sep 13 2020 at 21:48):

Is the sensible thing to just define arithmetic_function := N+ -> ?, and then put a ring structure on that where multiplication is Dirichlet convolution, and make an API for coercion of functions with domain N or N+?

Adam Topaz (Sep 13 2020 at 21:58):

What's $\varphi(0)$?

0

Adam Topaz (Sep 13 2020 at 21:59):

But $(\mathbb{Z}/(0))^\times$ has two elements ;)

Aaron Anderson (Sep 13 2020 at 21:59):

Yeah, but it's defined as counting a subset of finset.range n

Adam Topaz (Sep 13 2020 at 22:00):

All jokes aside, having aruthmetic_function (with the ring structure) would be great!

Adam Topaz (Sep 13 2020 at 22:02):

Isn't there also a ring structure on multiplicative functions where convolution becomes addition?

Aaron Anderson (Sep 13 2020 at 22:06):

What's multiplication in that case, pointwise multiplication? does that work?

Maybe?

Adam Topaz (Sep 13 2020 at 22:10):

I was thinking of the Big Witt vectors, but that's not quite the multiplicative functions in the sense of elementary NT

Aaron Anderson (Sep 13 2020 at 22:11):

Anyway, I should probably clarify that the stumbling block here will be the fact that defining these functions at 0 doesn't really make any sense, and then the map to Dirichlet series isn't injective, etc., but if I don't define them at 0, then the entire API for gcd and factorization breaks, because the standard versions have "except 0" baked into everything

Adam Topaz (Sep 13 2020 at 22:13):

I found this paper: https://www.sciencedirect.com/science/article/pii/S0022314X07001886

Adam Topaz (Sep 13 2020 at 22:14):

My vote is to use pnat, fwiw

Adam Topaz (Sep 13 2020 at 22:14):

I think the pnat api could use some attention anyway

Aaron Anderson (Sep 13 2020 at 22:15):

Yeah, I think after my next PR on unique factorization (with 0, sigh) I'll have to go back to normalization_monoid and de-0-ify that

Aaron Anderson (Sep 13 2020 at 22:16):

and then gcd

Aaron Anderson (Sep 13 2020 at 22:16):

But it probably won’t have a good solution

Adam Topaz (Sep 13 2020 at 22:19):

At some point I tried starting to formalize the big Witt vector ring, and I quit early on because I got frustrated with the missing pnat api

Adam Topaz (Sep 13 2020 at 22:25):

@Kevin Buzzard might have a different opinion.

Kevin Buzzard (Sep 13 2020 at 22:41):

In pari, phi(0)=2, for exactly the reason Adam suggests. But who cares what phi(0) is in Lean. I would define it on nat and just not worry too much about the junk values. If you start using pnat then you might have trouble later on because e.g. ring probably won't work

Aaron Anderson (Sep 13 2020 at 22:44):

I guess one advantage of using a type synonym arithmetic_function is that we can change the exact implementation later on

Kevin Buzzard (Sep 13 2020 at 22:44):

This is just like the argument about whether 1/0 should be defined. Just define it but never use it. Or alternatively try using pnat and let's find out how painful it really it. When I started using lean there was no square root function on the reals and I defined it on the nonnegative reals and it drove me nuts. Does 3 : pnat work?

Adam Topaz (Sep 13 2020 at 22:46):

The problem with big Witt vectors is that gcd is used when you define the ring operations, and it gets really annoying if you have to insert a million proofs that something is nonzero

Kevin Buzzard (Sep 13 2020 at 22:48):

In the theory of modular forms, the L-function of the normalised eigenform sum_{n>=0} a_n q^n is sum_{n>=1} a_n n^s. Here the constant term a_0 can be nonzero, however it is determined uniquely by the a_n for n>=1 in positive weight.

Aaron Anderson (Sep 13 2020 at 22:48):

Kevin Buzzard said:

This is just like the argument about whether 1/0 should be defined. Just define it but never use it. Or alternatively try using pnat and let's find out how painful it really it. When I started using lean there was no square root function on the reals and I defined it on the nonnegative reals and it drove me nuts. Does 3 : pnat work?

Yeah, 3 : pnat is fine. It's just that putting a gcd_monoid or unique_factorization_monoid instance on pnats is a pain, and IIRC there's not even a class for commutative monoids with cancellation (and no zero)

Kevin Buzzard (Sep 13 2020 at 22:50):

Just prove that pnat is a free monoid on the primes, everything follows from that, right?

Kevin Buzzard (Sep 13 2020 at 22:52):

Why is it a pain to put a UFM structure on pnat? If you're going to use pnat despite essentially no API then you're going to have to make the API and indeed doing a project like this will actually be a good way of finding out what API we need.

Aaron Anderson (Sep 13 2020 at 22:52):

Just the fact that if you come up with a definition of UFM that doesn't mention 0, then it stops working for monoids that do have 0.

Aaron Anderson (Sep 13 2020 at 22:56):

Kevin Buzzard said:

Just prove that pnat is a free monoid on the primes, everything follows from that, right?

I know what you mean mathematically, but what do you mean in Lean? Prove that pnat is isomorphic to a free_comm_monoid? If so, we don't have that definition.

Kyle Miller (Sep 13 2020 at 22:59):

Could you do something like define all the $\operatorname{ord}_p : \mathrm{pnat} \to \mathrm{nat}$ functions, show they're homomorphisms, then use these to define a homomorphism to the $p$-indexed coproduct of copies of $\mathrm{nat}$? (and if this latter doesn't exist, define it?) Then, finally, show this is an isomorphism?

Aaron Anderson (Sep 13 2020 at 23:08):

There's already a function that sends a pnat to a multiset of prime factors, which is basically what you're talking about. It's just that everything that gets proven about this notion of factorization is totally parallel from other notions of factorization

Aaron Anderson (Sep 13 2020 at 23:08):

My experience was that this was annoying for proving API lemmas

Kyle Miller (Sep 13 2020 at 23:13):

I guess that's basically the same thing, and multisets form a free commutative monoid under unions. I haven't spent any time with any of this, so I don't know about practice, but in principle it seems nice pulling this structure back.

Kyle Miller (Sep 13 2020 at 23:16):

I'm mostly thinking about how things seemed sleek in Ireland and Rosen's "A classical introduction to modern number theory" by implicitly using the free monoid structure that the ords give you. (These do go backwards from the correct universal property, though, and it relies on the fact that only finitely many of the ords are non-zero.)

Adam Topaz (Sep 13 2020 at 23:21):

Is there something like finitely supported functions for has_one?

Kevin Buzzard (Sep 13 2020 at 23:51):

Not as far as I know

Kevin Buzzard (Sep 13 2020 at 23:51):

I have run into this issue before

Kevin Buzzard (Sep 13 2020 at 23:52):

But the free abelian monoid on S is just finitely supported functions to nat, right?

Adam Topaz (Sep 13 2020 at 23:53):

Yeah but you would need to make it multiplicative at some point

Adam Topaz (Sep 13 2020 at 23:53):

I guess after taking finsupp will work too

Adam Topaz (Sep 13 2020 at 23:59):

Can to_additive be used to redefine finsupp with has_zero from finsupp with has_one?

Adam Topaz (Sep 14 2020 at 00:01):

Or is there a to_multiplicative?

Johan Commelin (Sep 14 2020 at 06:12):

Or is there a to_multiplicative?

Johan Commelin (Sep 14 2020 at 06:12):

Can to_additive be used to redefine finsupp with has_zero from finsupp with has_one?

Maybe, but it would be a massive refactor of the library.

Johan Commelin (Sep 14 2020 at 06:13):

The problem with big Witt vectors is that gcd is used when you define the ring operations, and it gets really annoying if you have to insert a million proofs that something is nonzero

I guess there is also the approach via symmetric functions... but we don't have anything on symmetric polynomials atm.

Aaron Anderson (Sep 18 2020 at 08:09):

I'm working on it at branch#arithmetic_functions

Aaron Anderson (Sep 18 2020 at 17:47):

(in short, arithmetic functions are a structure consisting of a function from N, where 0 is fixed to go to 0.)

Aaron Anderson (Sep 20 2020 at 06:13):

I've now gotten up to using Dirichlet convolution to show that the sum of (kth powers of) divisors function is multiplicative

Aaron Anderson (Sep 20 2020 at 06:14):

So probably time to spend a day or two cleaning it up before starting to PR some things

Aaron Anderson (Sep 20 2020 at 06:14):

So I'm open to any suggestions people have

Last updated: May 11 2021 at 16:22 UTC