Arithmetic Functions

Stream: maths

[Aaron Anderson]

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]

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]

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]

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]

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]

What's $\varphi(0)$?

[Aaron Anderson]

0

[Adam Topaz]

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

[Aaron Anderson]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Aaron Anderson]

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

[Adam Topaz]

Maybe?

[Adam Topaz]

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

[Aaron Anderson]

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]

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

[Adam Topaz]

My vote is to use pnat, fwiw

[Adam Topaz]

I think the pnat api could use some attention anyway

[Aaron Anderson]

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]

and then gcd

[Aaron Anderson]

But it probably won’t have a good solution

[Adam Topaz]

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]

@Kevin Buzzard might have a different opinion.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

My experience was that this was annoying for proving API lemmas

[Kyle Miller]

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]

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]

Is there something like finitely supported functions for has_one?

[Kevin Buzzard]

Not as far as I know

[Kevin Buzzard]

I have run into this issue before

[Kevin Buzzard]

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

[Adam Topaz]

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

[Adam Topaz]

I guess after taking finsupp will work too

[Adam Topaz]

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

[Adam Topaz]

Or is there a to_multiplicative?

[Johan Commelin]

Adam Topaz said:

Or is there a to_multiplicative?

Nope :sad:

[Johan Commelin]

Adam Topaz said:

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]

Adam Topaz said:

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]

I'm working on it at branch#arithmetic_functions

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

So I'm open to any suggestions people have