Prerequisites for PNT and Dirichlet's Thm

Stream: PR reviews

[Michael Stoll]

I am now starting a series of PRs that provide the ingredients for the proof of the Prime Number Theorem and Dirichlet's Theorem on primes in AP. Essentially, one has to show that a certain linear combination of logarithmic derivatives of Dirichlet L-series has certain properties. This will at some point build on the earlier PRs discussed here.

The series stats with #18923, which adds "logarithmic" versions of Euler products of completely multiplicative (complex-valued) functions.

[Michael Stoll]

The next one is #18924; it adds two easy IsBigO lemmas that help going from complex functions to their restrictions to the real line.

[Michael Stoll]

#18927 is the third; it adds two further IsBigO lemmas for shifted functions.

[Michael Stoll]

It continues with #18928; it adds API showing that LSeries commutes with Finset.sum.

[Michael Stoll]

The next one will be a bit larger (~270 loc); it will show that L(χ, s) does not vanish for s.re ≥ 1 when χ is a Dirichlet character (and either χ is nontrivial or s ≠ 1). But this depends on the four preparatory PRs mentioned above.

[David Loeffler]

Are they literally a series with each PR depending on the previous one, or can they be reviewed in any order?

[Ruben Van de Velde]

Does the series converge? (Sorry)

[Michael Stoll]

David Loeffler said:

Are they literally a series with each PR depending on the previous one, or can they be reviewed in any order?

These four are independent. Thanks for the reviews!

[Michael Stoll]

Michael Stoll said:

#18927 is the third; it adds two further IsBigO lemmas for shifted functions.

After some discussion, whose result was that it is better to inline these two lemmas where they are used (once each, in the next PR), I have closed this now.

[Michael Stoll]

#18923 (Euler products) could do with a review...

[Michael Stoll]

Another small preparatory PR: #18973. It just adds one lemma (the derivatives of the L-function and the L-series of a Dirichlet character agree on the half-plane of convergence of the latter).

[Michael Stoll]

#19034 uses the previously merged PR to establish an exp-log Euler product formula for Dirichlet L-series.

[Michael Stoll]

Now the first substantial step: #19043 proves that $L(\chi, s) \ne 0$ for $\operatorname{Re} s \ge 1$ (unless $\chi$ is trivial and $s = 1$). (About 240 loc.)

[Kevin Buzzard]

This is so cool! These results are important!

[Michael Stoll]

#19254 adds some results on logarithmic derivatives of L-functions of Dirichlet characters.

[Michael Stoll]

#19334 and #19335 are two further (small and indpendent) preparatory PRs.

[Michael Stoll]

Next up are the following lemmas.

lemma tsum_eq_tsum_primes_of_support_subset_prime_powers {α : Type*} [AddCommGroup α]
     [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T0Space α] {f : ℕ → α}
     (hfs : Summable f) (hf : Function.support f ⊆ {n | IsPrimePow n}) :
    ∑' n : ℕ, f n = ∑' (p : Nat.Primes) (k : ℕ), f (p ^ (k + 1)) := by
  sorry

lemma tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers {α : Type*}
    [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] [T0Space α]
    {f : ℕ → α} (hfs : Summable f) (hf : Function.support f ⊆ {n | IsPrimePow n}) :
    ∑' n : ℕ, f n = (∑' p : Nat.Primes, f p) +  ∑' (p : Nat.Primes) (k : ℕ), f (p ^ (k + 2)) := by
  sorry

Should these go somewhere under Mathlib.Topology.Algebra.InfiniteSum, or are they too special, so that they should go close to their application?

[Michael Stoll]

#19344 creates a new file Mathlib.NumberTheory.LSeries.PrimesInAP that will eventually contain a proof of Dirichlet's Theorem. The first step is to add the lemmas mentioned above. (If desired, they can be moved elsewhere at some point, but there does not appear to be a canonical place.)

[Michael Stoll]

#19368 is the next step: properties of the von Mangoldt function restricted to a residue class.

[Michael Stoll]

#19418 adds two further relevant statements on docs#ArithmeticFunction.vonMangoldt.residueClass.

[Johan Commelin]

Btw, how far are we from Dirichlet's theorem? 10 PRs? Or twice that? Can you already estimate this?

[Michael Stoll]

About 200 loc. Probably two further PRs.

[Johan Commelin]

Ooh, wow!

[Johan Commelin]

Would you mind opening a PR already?

[Michael Stoll]

You can see what remains here. (Minus the last part, which needs the Wiener-Ikehara Theorem; this is done in PNT+.)

[Michael Stoll]

I prefer tinkering in my own repo rather than pushing everything to a Mathlib branch while I'm working on it. Though I think that the proof in its current shape looks quite good.

[Michael Stoll]

I've decided to end the suspense: #19421 contains everything that is still missing including Dirichlet's Theorem itself (in two versions).
Note that this is "just" the infinity statement; more precise asymptotic versions are and will be obtained in the PNT+ project.

[Johan Commelin]

I left two comments. But I think people with more expertise in analytic number theory should also take a look.

[David Loeffler]

I am travelling at the moment but can take a look on Wednesday, unless someone else gets there first.

[Johan Commelin]

Enjoy your travels. If you need some distraction: do you know a nice name for

/-- The auxiliary function used, e.g., with the Wiener-Ikehara Theorem to prove
Dirichlet's Theorem. On `re s > 1`, it agrees with the L-series of the von Mangoldt
function restricted to the residue class `a : ZMod q` minus the principal part
`(q.totient)⁻¹/(s-1)` of the pole at `s = 1`; see `DirichletsThm.auxFun_prop`. -/
noncomputable
abbrev auxFun (s : ℂ) : ℂ :=
  (q.totient : ℂ)⁻¹ * (-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s -
    ∑ χ ∈ ({1}ᶜ : Finset (DirichletCharacter ℂ q)), χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s)

[Michael Stoll]

LfunctionResidueClassSubInvTotientDiv is descriptive in a way, but I'm not sure it is actually better. auxFunForDirichletsThm? :smile:

[Damiano Testa]

Maybe LfunctionResidueClassAux is a little more explicit, but also maintains an aux status.

[Johan Commelin]

It's mostly that when a module docstring starts talking about auxFun, then this decl seems important enough to get a different name...

[Michael Stoll]

I'll go with @Damiano Testa's suggestion for now. If somebody comes up with a better idea, we can change it again.

[David Loeffler]

Elsewhere in the L-functions library there is a convention of using subscript "0" to mean "L-series modified by adding a multiple of 1 / (s -1) to kill the pole". So perhaps this could be "ZMod.LFunctionVonMangoldt0"?

[Michael Stoll]

The function it's related to the L-series of is not periodic, so ZMod is not the right namespace. Perhaps ArithmeticFunction.vonMangoldt.LFunctionResidueClass₀?

[David Loeffler]

Using vonMangoldt as a namespace seems a bit unorthodox. I would also be happy with Damiano's suggestion, and (as Johan observes) it would be very easy to change the name later anyway so it's probably not worth worrying too much about it now.

[Michael Stoll]

I've put the modified von Mangoldt function in the ArithmeticFunction.vonMangoldt namespace because I think this makes sense. Then using this namespace also for the associated L-function follows in a way the precedent of DirichletCharacter.LFunction.

[Michael Stoll]

The alternative would probably be to use ArithmeticFunction.vonMangoldtResidueClass, but then one has to write out the "vonMangoldt" part every single time...

[Johan Commelin]

Besides this name... does anybody have any other comments?

[Johan Commelin]

LGTM, and I'm happy to get this merged today :grinning:

[Riccardo Brasca]

Having a look

[David Loeffler]

I gave it a quick once-over (while sitting in a hotel room in Amsterdam). All looks reasonable to me, and I think it is important enough that we should merge it ASAP and sort out any rough edges later.

[Riccardo Brasca]

It looks (very) good also to me, I've left two minor comments and I think it is ready to go.

[Riccardo Brasca]

A related question, do we want to remove Mathlib.NumberTheory.PrimesCongruentOne?

[Johan Commelin]

[Johan Commelin]

Mathlib.NumberTheory.PrimesCongruentOne is used in an IMO problem. It seems a bit extravagant to use Dirichlet for that... but ey, it typechecks :rofl:

[Riccardo Brasca]

Well, we can always move everything in the same IMO file, it is a short proof. Anyway I think we will have more and more situation like this, when easy results become a special case of big ones

[Yaël Dillies]

Johan Commelin said:

Mathlib.NumberTheory.PrimesCongruentOne is used in an IMO problem. It seems a bit extravagant to use Dirichlet for that... but ey, it typechecks :rofl:

Makes sense to me. Dirichlet's theorem is one of the first things I learned when preparing for the IMO, along with Hensel's lemma

[Johan Commelin]

It's landed! Massive milestone! Congrats @Michael Stoll

[Michael Stoll]

Just noticed that it should be LFunctionResidueClassAux instead of LfunctionResidueClassAux...

[Michael Stoll]

#19474 fixes the names.

[Antoine Chambert-Loir]

Riccardo Brasca said:

A related question, do we want to remove Mathlib.NumberTheory.PrimesCongruentOne?

I'd suggest that the proof of that file should be transferred to another part of mathlib, so that it isn't lost (it's a Proof from the Book!), but the theorem should be refactored using Dirichlet's theorem.

[Michael Stoll]

Maybe move it to Archive?

[Michael Stoll]

It seems that this result is only used in Imo2008Q3 (and there is a comment in file#Mathlib/NumberTheory/FermatPsp referring to docs#Nat.frequently_atTop_modEq_one).

[Antoine Chambert-Loir]

You see, I'm not sure the full Dirichlet's theorem will have many applications in mathlib before some time!
The congruent to one case has a nice proof that can serve as an interesting example to people, and I would even suggest that mathlib documents it.

[Michael Stoll]

I hope to get the Hasse-Minkowski Theorem (over $\mathbb Q$ at least) into Mathlib eventually, and this will need Dirichlet's Theorem at some point. But this will certainly take a while...

[Antoine Chambert-Loir]

And that will be a wonderful application!

[Joseph Myers]

Some people have a notion that IMO problems shouldn't depend for their solution on non-elementary cases of Dirichlet's theorem (but that such dependence would be considered fine at some other competitions such as the Romanian Master of Mathematics): that while it's OK to use non-elementary results in solving a problem (indeed, people might occasionally quote FLT or Catalan-Mihăilescu in olympiad solutions), a problem ought to have a solution that doesn't use such results.

[Joseph Myers]

That's not relevant for what goes in mathlib; heavy dependencies are fine in the mathlib archive without needing to be concerned with whether the particular case of Dirichlet used is or is not an elementary one. Rather, the key question for whether to keep an elementary special case of Dirichlet in mathlib would be whether there is likely to be anything added to mathlib itself that (a) depends on such a case and (b) ought to have limited dependencies.

[Joseph Myers]

Moving to a particular IMO file in the mathlib archive doesn't seem such a good idea, though, since quite likely other IMO problems might also want to use that special case. (Though IMO 2003 P6 is more a matter of "solution uses similar ideas" than "solution quotes the result" - albeit that there is said to be a solution to 2003 P6 by quoting Chebotarev. Maybe once we have Chebotarev formalized we can see if that ends up much shorter than the elementary solution in compfiles.)

[Alex Kontorovich]

Antoine Chambert-Loir said:

You see, I'm not sure the full Dirichlet's theorem will have many applications in mathlib before some time!
The congruent to one case has a nice proof that can serve as an interesting example to people, and I would even suggest that mathlib documents it.

How about bounded generation of higher rank groups like $SL_n(\Z)$, $n\ge3$...?

[Violeta Hernández]

Johan Commelin said:

Mathlib.NumberTheory.PrimesCongruentOne is used in an IMO problem. It seems a bit extravagant to use Dirichlet for that... but ey, it typechecks :rofl:

Which one? There's always the possibility that there's some alternate solution without it that isn't much harder.

[Johan Commelin]

Archive/Imo/Imo2008Q3.lean

[Thomas Browning]

Seems like it just needs infinitely many primes congruent to 1 mod 4

[Kevin Buzzard]

And there's an elementary proof of this (given finitely many such primes, multiply them all together, double, square, add one and take a factor, using the fact that -1 is a square mod the factor)

[Antoine Chambert-Loir]

And having primes congruent to -1 mod 4 is easy as well. Even easier.

[Thomas Browning]

Kevin Buzzard said:

And there's an elementary proof of this (given finitely many such primes, multiply them all together, double, square, add one and take a factor, using the fact that -1 is a square mod the factor)

Although technically this proof follows the same route as the general 1 mod n proof, since you're using the fourth cyclotomic polynomial.

[Joseph Myers]

I think the general version of the elementary argument for primes -1 mod 4 results in: given a subgroup of (ZMod n)ˣ that's not the whole group, there are infinitely many primes whose values mod n are not in that subgroup.

[Riccardo Brasca]

The general result is (I think) that there infinitely many primes not congruent to 1 mod n, but this gives -1 only mod 4.

[Michael Stoll]

That's the special case of what @Joseph Myers says when the subgroup is trivial. But the more general result also includes the statement that there are infinitely many primes that are quadratic nonresidues mod a fixed prime, for example. (And the complementary statement that there are infinitely many primes that are quadratic residues follows from an argument like the one @Kevin Buzzard has sketched.)