Zulip Chat Archive

Stream: maths

Topic: Arithmetic Functions


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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+?

view this post on Zulip Adam Topaz (Sep 13 2020 at 21:58):

What's φ(0)\varphi(0)?

view this post on Zulip Aaron Anderson (Sep 13 2020 at 21:59):

0

view this post on Zulip Adam Topaz (Sep 13 2020 at 21:59):

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

view this post on Zulip Aaron Anderson (Sep 13 2020 at 21:59):

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

view this post on Zulip Adam Topaz (Sep 13 2020 at 22:00):

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

view this post on Zulip Adam Topaz (Sep 13 2020 at 22:02):

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

view this post on Zulip Aaron Anderson (Sep 13 2020 at 22:06):

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

view this post on Zulip Adam Topaz (Sep 13 2020 at 22:10):

Maybe?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Sep 13 2020 at 22:13):

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

view this post on Zulip Adam Topaz (Sep 13 2020 at 22:14):

My vote is to use pnat, fwiw

view this post on Zulip Adam Topaz (Sep 13 2020 at 22:14):

I think the pnat api could use some attention anyway

view this post on Zulip 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

view this post on Zulip Aaron Anderson (Sep 13 2020 at 22:16):

and then gcd

view this post on Zulip Aaron Anderson (Sep 13 2020 at 22:16):

But it probably won’t have a good solution

view this post on Zulip 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

view this post on Zulip Adam Topaz (Sep 13 2020 at 22:25):

@Kevin Buzzard might have a different opinion.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 22:50):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kyle Miller (Sep 13 2020 at 22:59):

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

view this post on Zulip 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

view this post on Zulip Aaron Anderson (Sep 13 2020 at 23:08):

My experience was that this was annoying for proving API lemmas

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Adam Topaz (Sep 13 2020 at 23:21):

Is there something like finitely supported functions for has_one?

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 23:51):

Not as far as I know

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 23:51):

I have run into this issue before

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 23:52):

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

view this post on Zulip Adam Topaz (Sep 13 2020 at 23:53):

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

view this post on Zulip Adam Topaz (Sep 13 2020 at 23:53):

I guess after taking finsupp will work too

view this post on Zulip Adam Topaz (Sep 13 2020 at 23:59):

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

view this post on Zulip Adam Topaz (Sep 14 2020 at 00:01):

Or is there a to_multiplicative?

view this post on Zulip Johan Commelin (Sep 14 2020 at 06:12):

Adam Topaz said:

Or is there a to_multiplicative?

Nope :sad:

view this post on Zulip Johan Commelin (Sep 14 2020 at 06:12):

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.

view this post on Zulip Johan Commelin (Sep 14 2020 at 06:13):

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.

view this post on Zulip Aaron Anderson (Sep 18 2020 at 08:09):

I'm working on it at branch#arithmetic_functions

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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