Connecting with EulerProducts/PNT.lean

Stream: PrimeNumberTheorem+

[Vincent Beffara]

I had a quick look at the very last statement in our Wiener.lean file (i.e. the PNT itself), and how to obtaining by connecting what we have for now and the proof in EulerProduct. There is a mismatch between WienerIkeharaTheorem in EulerProducts/PNT.lean and WienerIkeharaTheorem' in Wiener.lean, in two places:

• We use ArithmeticFunction while EulerProducts uses plain maps from N to C. This does not really matter, a few of our lemmas do use the face that f 0 = 0 but the asymptotics are not affected, and it is easy to adapt
• We carry around the hcheby bound everywhere, and it is not present in the EulerProducts version, so it might look that our version of Wiener-Ikehara is weaker than needed. I am hoping that this bound can be obtained from the asymptotics of the function F at the pole and positivity of the coefficients (without having had much time to think about how), otherwise we will need it for \Lambda but that will make the direct use of EulerProducts as it is written now impossible.

Am I missing something obvious?

[Michael Stoll]

As far as I can see, WienerIkeharaTheorem' is identical (modulo the ArithmeticFunction ℝ vs. ℕ → ℝ issue) with WienerIkeharaTheorem. Am I missing something?

[Terence Tao]

You're right, strictly speaking the blueprint is establishing a slightly weaker version of the Wiener-Ikehara theorem in which a Chebyshev-type bound is assumed. It can be eliminated with a little bit more work, but I had thought to avoid this since the Chebyshev bound is relatively easy to establish in practice (I believe for instance that the unit fractions project already has a proof of it, and I think someone has even proven a stronger bound of Brun-Titchmarsh type using the Selberg sieve). However, if one really wanted to get the "full" Wiener-Ikehara, one can argue as follows.

(1) Establish a variant of Limiting Fourier identity in which the Chebyshev bound is not assumed, but instead f and the Fourier transform of psi assumed to be non-negative. This is the same proof, but uses monotone convergence instead of dominated convergence.

(2) By choosing a suitable psi that is both nonnegative and has nonnegative Fourier transform , use this variant to establish a bound of the form $\sum_{x \leq n \leq 2x} f(n) \ll x.$

(3) Perform a dyadic decomposition to conclude the Chebyshev bound.

I guess the question is whether the extra effort to establish steps (1)-(3) is worth it.

[Terence Tao]

Michael Stoll said:

As far as I can see, WienerIkeharaTheorem' is identical (modulo the ArithmeticFunction ℝ vs. ℕ → ℝ issue) with WienerIkeharaTheorem. Am I missing something?

There used to be an hcheby hypothesis (assuming a Chebyshev type bound $\sum_{n \leq x} f(n) \ll x$ on the Dirichlet series coefficients) as an ambient variable before WienerIkeharaTheorem' (and many other precursor results), but it is in the process of being moved to the individual lemmas. We haven't yet got to doing so for the Wiener Ikehara theorem itself though.

[Michael Stoll]

Ah OK; I would have expected the ambient variable mentioned in what the doc file shows, and I didn't see it there.

Of course, it would be nice to have the stronger version of Wiener-Ikehara available, but if we have the necessary estimate for $\Lambda$ anyway, it will be easy to modify the current proof of PNT using WienerIkeharaTheroem to use the weaker variant.

[Vincent Beffara]

I think that using positivity and evaluating the L function at 1+epsilon/n we can use the behavior of the function F to obtain the Chebychev condition directly, with C equal to constant times the residue at 1.

[Alex Kontorovich]

Terence Tao said:

You're right, strictly speaking the blueprint is establishing a slightly weaker version of the Wiener-Ikehara theorem in which a Chebyshev-type bound is assumed. It can be eliminated with a little bit more work, but I had thought to avoid this since the Chebyshev bound is relatively easy to establish in practice (I believe for instance that the unit fractions project already has a proof of it, and I think someone has even proven a stronger bound of Brun-Titchmarsh type using the Selberg sieve).

Indeed, there was a discussion of the Selberg sieve here. In the "MediumPNT" approach, it's no longer needed, now that we're aiming for an error that beats any power of log (so we can afford to lose a log here).

[Arend Mellendijk]

Given this is the second time it's come up, I'd be very happy to just PR the sieve estimate.

[Terence Tao]

Vincent Beffara said:

I think that using positivity and evaluating the L function at 1+epsilon/n we can use the behavior of the function F to obtain the Chebychev condition directly, with C equal to constant times the residue at 1.

I think this sort of Rankin trick argument gives a weak Mertens bound $\sum_{n \leq x} \Lambda(n)/n \ll \log x$, but doesn't easily give a Chebyshev bound $\sum_{n \leq x} \Lambda(n) \ll x$.

[Vincent Beffara]

Ah, you are right of course, my plan was overly optimistic :-(

[Vincent Beffara]

Here is the easy part of the gluing, just taking care of the discrepancy between \N \to \R and ArithmeticFunction (and assuming WienerIkeharaTheorem' without the hcheby assumption). Just to remove the number of sorries, but mathematically empty.

[Vincent Beffara]

theorem WeakPNT : Tendsto (fun N : ℕ ↦ ((Finset.range N).sum Λ) / N) atTop (nhds 1) := by

  apply PNT_vonMangoldt ; intro f A F f_nonneg hF hF'

  let ff : ArithmeticFunction ℝ := ⟨fun n => if n = 0 then 0 else f n, rfl⟩
  have ff_nonneg n : 0 ≤ ff n := by by_cases hn : n = 0 <;> simp [ff, hn, f_nonneg n]
  have l2 s i : term (fun n ↦ ↑(ff n)) s i =  term (fun n ↦ ↑(f n)) s i := by
    by_cases hi : i = 0 <;> simp [term, hi, ff]
  have l1 : LSeries (fun n ↦ ff n) = LSeries (fun n => f n) := by
    ext s ; simp [LSeries, l2]
  have l3 n (hn : 0 < n) : Finset.sum (Finset.range n) ff = (Finset.sum (Finset.range n) f) - f 0 := by
    have : 0 ∈ Finset.range n := by simp [hn]
    simp [Finset.sum_eq_sum_diff_singleton_add this, ff]
    apply Finset.sum_congr rfl
    intro i hi ; simp at hi ; simp [hi]
  have l4 : ∀ᶠ n in atTop, Finset.sum (Finset.range n) ff / n = (Finset.sum (Finset.range n) f) / n - f 0 / n := by
    filter_upwards [eventually_gt_atTop 0] with n hn
    simp [l3 n hn, sub_div]
  have l5 := @WienerIkeharaTheorem' ff A F ff_nonneg (by simpa [l1] using hF) hF'
  simpa using l5.congr' l4 |>.add (tendsto_const_div_atTop_nhds_zero_nat (f 0))

[Vincent Beffara]

The glue should rather go right after one of the limit theorems, so that the contents of the actual proof of WeakPNT can be more serious.

[Terence Tao]

OK... so in conjunction with Arend's PR of the Brun-Titchmarsh inequality primesBetween_le, we should have a relatively cheap way to get from WienerIkeharaTheorem to WeakPNT since hcheby is now available. It still might be nice to deduce the full Wiener-Ikehara Theorem from the weak one in the blueprint, but I still don't know whether it is worth the effort (one annoying thing is that one needs to produce some relatively smooth compactly supported function which non-negative and (is positive on some given interval such as [-1,1]), and whose Fourier transform is non-negative; it's not hard to show such functions exist on general principles (e.g., convolve a suitable non-negative even bump function with itself), but could be a bit fiddly to formalize).

[Arend Mellendijk]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/135 establishes $\pi(x+y) - \pi(x) \le 2y / \log z + 6z (1+\log z)^3$.

I can work on showing cheby (fun n ↦ Λ n) next.

[Notification Bot]

A message was moved here from #PrimeNumberTheorem+ > Outstanding Tasks, V5 by Arend Mellendijk.

[Arend Mellendijk]

Arend Mellendijk said:

I can work on showing cheby (fun n ↦ Λ n) next.

This is now done: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/141

[Vincent Beffara]

Is ∀ (σ' : ℝ), 1 < σ' → Summable (nterm Λ σ') proved somewhere explicitly?

[Vincent Beffara]

It follows directly from vonMangoldt_le_log in any case but it is probably already done.

[Alex Kontorovich]

Something like docs#LSeriesSummable_of_le_const_mul_rpow should help...?

[Michael Stoll]

docs#ArithmeticFunction.LSeriesSummable_vonMangoldt (very fresh in Mathlib!).

[Vincent Beffara]

I took the proof of WeakPNT from EulerProducts to put it in Wiener.lean so that I could adjust it, it now looks like this:

theorem WeakPNT : Tendsto (fun N ↦ cumsum Λ N / N) atTop (nhds 1) := by
  have hnv := riemannZeta_ne_zero_of_one_le_re
  have l1 (n : ℕ) : 0 ≤ Λ n := vonMangoldt_nonneg
  have l2 s (hs : 1 < s.re) : (-deriv ζ₁ / ζ₁) s = LSeries Λ s - 1 / (s - 1) := by
    have hs₁ : s ≠ 1 := by contrapose! hs ; simp [hs]
    simp [LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs, neg_logDeriv_ζ₁_eq hs₁ (hnv hs₁ hs.le)]
  have l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re} := continuousOn_neg_logDeriv_ζ₁.mono (by tauto)
  have l4 : cheby Λ := vonMangoldt_cheby
  have l5 (σ' : ℝ) (hσ' : 1 < σ') : Summable (nterm Λ σ') := by sorry
  apply WienerIkeharaTheorem' l1 l5 l4 l3 l2

with just one sorry left (plus of course WienerIkeharaTheorem', which is on the way, and Fourier inversion, which also is but a bit further away).

[Michael Stoll]

Wasn't the sorry discussed above?

[Alex Kontorovich]

I think it's there because we'll need a mathlib bump to access the theorem...

[Vincent Beffara]

No need for the bump, it is just a matter of massaging the result from mathlib into the right form (we need it with a norm). I just did the Ico transition first.

[Vincent Beffara]

  have l5 (σ' : ℝ) (hσ' : 1 < σ') : Summable (nterm Λ σ') := by
    simpa only [← nterm_eq_norm_term] using (@ArithmeticFunction.LSeriesSummable_vonMangoldt σ' hσ').norm

[Vincent Beffara]

WienerIkeharaTheorem' is done, meaning that

'WeakPNT' depends on axioms: [Quot.sound, propext, Classical.choice, fourier_surjection_on_schwartz]

and the only remaining piece of the puzzle is that the Fourier transform is bijective on the Schwartz class.

[Vincent Beffara]

I am very tempted to rush a proof of the Fourier stuff in the special case of R \to C just so that the whole proof is complete ...

[Sébastien Gouëzel]

You may definitely rush it (although #11776 will probably spare you a little bit of the work). It's hiring committees time in France, so I won't have a lot of Lean time in the next future, so the completion of the general case in mathlib might take a little bit longer than expected...

[Sébastien Gouëzel]

(deleted)

[Sébastien Gouëzel]

If you want to rush it, you might find useful some things that I've already proved in the branch SG_deriv_fourier3, notably the two following theorems (proved in arbitrary dimension, but then specialized to one dimension):

theorem iteratedDeriv_fourierIntegral {f : ℝ → E} {N : ℕ∞} {n : ℕ}
    (hf : ∀ (n : ℕ), n ≤ N → Integrable (fun x ↦ x^n • f x)) (hn : n ≤ N) :
    iteratedDeriv n (𝓕 f) = 𝓕 (fun x : ℝ ↦ (-2 * π * I * x) ^ n • f x) := by

theorem fourierIntegral_iteratedDeriv {f : ℝ → E} {N : ℕ∞} (hf : ContDiff ℝ N f)
    (h'f : ∀ (n : ℕ), n ≤ N → Integrable (iteratedDeriv n f)) {n : ℕ} (hn : n ≤ N) :
    𝓕 (iteratedDeriv n f) = fun (x : ℝ) ↦ (2 * π * I * x) ^ n • (𝓕 f x) := by

[Terence Tao]

Vincent Beffara said:

WienerIkeharaTheorem' is done, meaning that

'WeakPNT' depends on axioms: [Quot.sound, propext, Classical.choice, fourier_surjection_on_schwartz]

and the only remaining piece of the puzzle is that the Fourier transform is bijective on the Schwartz class.

Were there any steps in the blueprint that were unexpectedly hard to formalize? Just curious of there are any types of informal arguments that one should avoid in the blueprint because they are challenging to write in Lean.

[Patrick Massot]

Hopefully we can think about how to make them less challenging to write in Lean instead of avoiding them.

[Vincent Beffara]

So based on Sébastien's work I just defined this

noncomputable def FS (f : 𝓢(ℝ, ℂ)) : 𝓢(ℝ, ℂ) where
  toFun := 𝓕 f

(with proved regularity and decay). Between this and Fourier inversion, I think than not much is missing.

[Vincent Beffara]

'WeakPNT' depends on axioms: [Quot.sound, propext, Classical.choice]

[Vincent Beffara]

PR at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/150

[Vincent Beffara]

The Fourier approach is done :grinning:

[Johan Commelin]

Awesome! Congrats!!!

[Alex Kontorovich]

Merged!!! Congrats to all, and thanks for the hard work!!!

[Alex Kontorovich]

At some point we'll want to organize trying to get what's been done into Mathlib. But maybe not just yet, we can keep pushing to the stronger form of PNT (which, as far as I know, will be the first time that's formalized).

[Ruben Van de Velde]

Are there any parts that you consider ready to move to mathlib already? The sooner the better, I'd say

[Michael Stoll]

I will continue PRing material from EulerProducts, at least up to the proof that $\zeta$ (and Dirichlet L-series, as soon as we have the analytic continuation) does not vanish on the line $\operatorname{Re} s = 1$. The next step will be refactoring Euler products to use the new infinite products and extending the API a bit.

[Vincent Beffara]

Terence Tao said:

Vincent Beffara said:

WienerIkeharaTheorem' is done, meaning that

'WeakPNT' depends on axioms: [Quot.sound, propext, Classical.choice, fourier_surjection_on_schwartz]

and the only remaining piece of the puzzle is that the Fourier transform is bijective on the Schwartz class.

Were there any steps in the blueprint that were unexpectedly hard to formalize? Just curious of there are any types of informal arguments that one should avoid in the blueprint because they are challenging to write in Lean.

That is a very good question, but I have no good answer to give except that in my experience, high-level arguments are actually easier to formalize than routine details. Typically "now let epsilon go to zero in the previous lemma to conclude" can easily turn into a few hundred lines of intermediate lemmas ... but I'm only speaking for myself here, and the issue might very well be that I was doing it wrong

[Terence Tao]

Vincent Beffara said:

The Fourier approach is done :grinning:

This is great news! I wonder now what would be the logical next steps. I see three possible future directions to build off of this:

1. Remove the Chebyshev hypothesis from WienerIkehara(there is a blueprint on how to do this)
2. Start work on the elementary consequences of the PNT
3. Prove the prime number theorem in arithmetic progressions using the Wiener Ikehara theorem and some facts about non-vanishing of $L(s,\chi)$ for ${\mathrm Re} s = 1$

We had discussed #3 some weeks ago and my understanding is that it was waiting on some other project to define holomorphic continuation of L-functions? I think that if we do have the nonvanishing results about L-functions then it should not be too hard to use Dirichlet character expansion and Wiener Ikehara to get the PNT in AP, but I don't know how close we are to those results yet. If there is interest, and if I have some idea of what results on L-functions we can import, I can try to write a blueprint of how to get to PNT in AP from all these preliminaries.

Of course, we could pursue two or more directions simultaneously, but it might make more sense to focus initially on what people are most interested in working on; thoughts welcomed.

[Michael Stoll]

Once we have the analytic continuation of Dirichlet L-functions, the non-vanishing of $L(\chi, s)$ on $\operatorname{Re} s = 1$ should be fairly quick. I am planning to make the necessary preparations soon.

[Terence Tao]

Michael Stoll said:

Once we have the analytic continuation of Dirichlet L-functions, the non-vanishing of $L(\chi, s)$ on $\operatorname{Re} s = 1$ should be fairly quick. I am planning to make the necessary preparations soon.

OK, great. In the meantime I just quickly PR'ed a sketch proof of how the PNT in APs follows from Wiener-Ikehara and the non-vanishing of L-functions on $\mathrm{Re} s = 1$. It should be quite straightforward once one has the Fourier expansion $\sum_{n=a\ (q)} \frac{\Lambda(n)}{n^s} = - \frac{1}{\phi(q)} \sum_{\chi\ (q)} \bar{\chi}(a) \frac{L'(s,\chi)}{L(s,\chi)}$ into Dirichlet characters and also the identity $\frac{L'(s,\chi_0)}{L(s,\chi_0)} = \frac{\zeta'(s)}{\zeta(s)} + \sum_{p|q} \frac{\log p}{p^s-1},$ which I presume can be obtained without too much pain from the Euler products API.

[Johan Commelin]

Vincent Beffara said:

'WeakPNT' depends on axioms: [Quot.sound, propext, Classical.choice]

Btw, this also deserves an entry in 100.yaml, I guess

[David Loeffler]

Terence Tao said:

Vincent Beffara said:

The Fourier approach is done :grinning:

We had discussed #3 some weeks ago and my understanding is that it was waiting on some other project to define holomorphic continuation of L-functions?

Yes, that's my project.

I have (rough, but fully working) code for this at PR #10011, where I show that for any N : ℕ+ and any Φ : ZMod N → ℂ, the function ∑ n : ℕ, Φ n / n ^ s extends analytically to ℂ - {1}, and to all of ℂ if ∑ j : ZMod N, Φ j = 0 (see differentiable_congruenceLFunction_of_sum_zero in file ResidueClassZeta.lean). I also prove the expected functional equation in terms of the Fourier transform of Φ.

I am slowly drip-feeding this into mathlib (many thanks to @Michael Stoll for his very patient reviewing) – it was originally 4000 lines, now down to about 2500 still to merge.

[Kevin Buzzard]

For Fermat I will need automorphic induction from a character of a degree 2 extension of F to GL(2)/F (with F a (totally real) number field), and one way of proving that would be by converse theorems, which would need analytic continuation of grossencharacters (for CM fields with H-T weights 0,1, but I am not really sure that's any easier than characters for general number fields, basically it's Tate's thesis). I'll also need Cebotarev density for finite Galois extensions of number fields which I think one can reduce to the abelian case and then it's again some statement about the behaviour of Hecke L-functions but again with base field not $\mathbf{Q}$.

[David Loeffler]

Kevin Buzzard said:

For Fermat I will need automorphic induction from a character of a degree 2 extension of F to GL(2)/F (with F a (totally real) number field), and one way of proving that would be by converse theorems, which would need analytic continuation of grossencharacters (for CM fields with H-T weights 0,1, but I am not really sure that's any easier than characters for general number fields, basically it's Tate's thesis).

For this, going via converse theorems seems a bit of a roundabout approach (to me). In the imaginary quadratic case, it's pretty easy to show that the theta-series associated to a grossencharacter is a modular form (it's basically just Poisson summation in R ^ 2) and we already have the machinery to prove modular form L-functions are entire. I'm not sure how much harder this becomes with CM fields and Hilbert mod forms, but my instinct is that going via theta-series would still be easier than Tate's thesis + converse theorems.

(I think this is pretty much how Hecke originally proved analytic continuation of Groessencharacter L-series back in the 1930s or whatever it was.)

[Kevin Buzzard]

Oh interesting. I have put literally 0 thought into how to get to the analytic results I'll need, but I have finally got around to at least starting to collect my thoughts and write down the statements! They'll be public in a couple of weeks.