Nat.ArithmeticFunction --> ArithmeticFunction

Stream: mathlib4

[Michael Stoll]

It seems to me that the Nat. part in the namespace Nat.ArithmeticFunction is unnecessary, as I would not expect the need for "arithmetic functions" defined on something else than Nat to arise.
Would there be any objections to removing it?

[Kevin Buzzard]

You should change it to PNat ;-)

[Yaël Dillies]

I agree you can remove it

[Michael Stoll]

I'll do that once #10385 is merged (and I had some sleep...).

[Michael Stoll]

#10399

[Michael Stoll]

As a next step here. I would like to put the various notations introduced in NumberTheory.AithmeticFunction into separate scopes (like ArithmeticFunction.vonMangoldt for Λ), so that it will be possible to make them available more selectively. For example, in some context I would like to use Λ for the von Mangoldt function but at the same time ζ as a (local) notation for the Riemann zeta function.
Objections?

[Yaël Dillies]

Objection: Make it possible to get all notations by opening a single locale

[Michael Stoll]

How does one do that?

[Yaël Dillies]

Can locales be hierarchised?

[Michael Stoll]

No idea.

[Michael Stoll]

Is there documentation on locales somewhere?

[Yaël Dillies]

At worse you can define the notations in two locales

[Michael Stoll]

So just add separate locales for the various definitions in addition to what exists, I guess?

[Yaël Dillies]

I think that's good, yes

[Michael Stoll]

OK; I'll try that.

[Michael Stoll]

This approach seems to work in a simple test file, so it looks good.

[Michael Stoll]

#10403

[Antoine Chambert-Loir]

I wonder whether the locale shouldn't be named RiemannZeta and RiemannSigma, for example if one wishes to have DedekindZeta or WeierstrassSigma …

[Michael Stoll]

Note that this zeta is not the Riemann zeta function, but the arithmetic function giving its coefficients (i.e., it is the constant function 1 except that zero is mapped to zero). So I don't think RiemannZeta is a good name here.
(We can of course introduce notation ζ for the Riemann zeta function in a locale RiemannZeta in addition.)

[Antoine Chambert-Loir]

Well, then zeta is a rather confusing name, is it?
(Stupid remark that shows I must have missed some episodes: the ring of arithmetic functions is just the large monoid algebra of the strictly positive integers. Thinking of it in this way would have a lot of the lemmas be general instances of what exists, say, for power series, etc.)

[Junyan Xu]

HahnSeries (Additive ℕ+) R probably works :)
(Edit: maybe only Additive (Associates ℕ+) has the correct order + algebra structure.)

[Michael Stoll]

It would, I think, but is perhaps a bit overkill and likely painful to use in concrete cases.

[Michael Stoll]

(Historically, arithmetic functions in Mathlib seem to predate Hahn series.)

[Michael Stoll]

Antoine Chambert-Loir said:

Well, then zeta is a rather confusing name, is it?

I assume it is fairly standard in the context of arithmetic functions. The goal of #10403 is to mitigate the confusion by enabling you to just import notation for the Möbius and von Mangoldt functions (say).

[Antoine Chambert-Loir]

(It is called z in the book where I learnt this, D. P. Parent, Exercises in Number Theory, and I have to admit that z is not really better than ζ.)

[Antoine Chambert-Loir]

Serious question : can you define the Riemann zeta function using the notation, and have the notation ζ for both of them?

[Michael Stoll]

I think yes:

import Mathlib.NumberTheory.LSeries.Basic
import Mathlib.NumberTheory.ZetaFunction

open ArithmeticFunction
open scoped ArithmeticFunction -- defines `ζ` as an arith. function
notation "ζ" => riemannZeta

#check (ζ : ℂ → ℂ) = LSeries ζ  -- error without type ascription
variable (s : ℂ)
#check ζ s = LSeries ζ s