Sum over 1/p diverges

Stream: Is there code for X?

[Michael Stoll]

Is the fact that the sum over $1/p$ for $p$ prime diverges somewhere in Mathlib?
Asking loogle for |- Not (Summable _) gives five results, the first three of which are not relevant, and the other two are docs#Real.not_summable_nat_cast_inv and docs#Real.not_summable_one_div_nat_cast , which are about the harmonic series.

If this is not there, I guess including it would be welcome? For fun (and also because I will need it) I have spent the last couple of days formalizing Erdös's elementary proof (as given in the BOOK), so it would be easy to PR the result now.

[Yury G. Kudryashov]

It would be nice to have something like Summable (∑' p : Nat.Primes, (p : Real) ^ r) <-> r < -1

[Michael Stoll]

That's an easy consequence.

[Michael Stoll]

What would be the idiomatic way to spell it? I currently have ¬ Summable (indicator {p | p.Prime} (fun n : ℕ ↦ (1 : ℝ) / n)), but one could also use Nat.Primes.

[Yury G. Kudryashov]

AFAIK, we don't have a convention here yet.

[Joachim Breitner]

Could it be expresses as = infty in EReal?

[Michael Stoll]

There should be lemmas in Mathlib that translate between the various versions. (But I didn't check yet.)

[Yury G. Kudryashov]

@Joachim Breitner We definitely have lemmas about = infty in ENNReal, not sure about EReal.

[Michael Stoll]

My code is here. I'll start PRing it tomorrow.

[Michael Stoll]

#9240 provides the necessary results on bounds for the cardinalities of the sets of k-smooth and k-rough numbers up to some bound N.

[Michael Stoll]

I think the statements on the divergence of the series should go into a separate file.
Would it make sense to set up a sub-folder Analytic below Number_Theory and put it there (and then also move ZetaFunction and ZetaValues and maybe some other filesthere), or is it better (for the time being, at least) to just have a new file SumPrimeReciprocals (say) in NumberTheory? @David Loeffler @Kevin Buzzard

[Kevin Buzzard]

I like the idea of an Analytic directory! We've seen evidence in 2023 that chunks of modern combinatorics are formalisable "in real time" and I'm wondering whether we might be able to push analytic number theory in that direction in 2024.

[Terence Tao]

@Michael Stoll would your code easily give the identities $\sum_{n=1}^\infty \frac{\Lambda(n)}{n^s} = -\frac{\zeta'(s)}{\zeta(s)}$ and $\sum_{n=2}^\infty \frac{\Lambda(n)}{n^s \log n} = \log \zeta(s)$ for $\mathrm{Re} s > 1$? This would not only give the divergence of $\sum_p 1/p$ (send $s \to 1^+$ in the second identity) but also start the road towards the prime number theorem.

[Michael Stoll]

Erdős's proof of the divergence will not give that, but it should not be too hard to get it from what I did so far w.r.t. Euler products (I'm preparing a logarithmic version). Then we only need the Wiener-Ikehara Tauberian theorem...

[Terence Tao]

I'd be willing to contribute to (but not take the lead on) a PFR-type collaborative project to develop the analytic number theory library, for instance by making blueprints of various basic analytic number theory facts (prime number theorem, Dirichlet's theorem, Mertens' theorem, etc.).

[Michael Stoll]

Dirichlet's Theorem (on primes in AP) is what I am aiming at with Euler products and related stuff. So I'd be happy to contribute. But I am not an analytic number theorist, so I'm not really qualified to lead a wider project to develop analytic number theory in Mathlib.

[Alex Kontorovich]

I think one of the issues is that there's not yet enough complex analysis to do analytic number theory the way some (myself included) would like... One can go around this in lots of ways for particular applications (e.g. the elementary approach), but ideally we would do something that applies to all Langlands L-functions, once the complex analysis is there...

[Michael Stoll]

#9270 is a prerequisite for applying log to Euler products.

[Thomas Bloom]

For the unit-fractions project, @Bhavik Mehta did formalise quite a bit of 'basic' ANT, including things like Chebyshev estimates, divergence of 1/p (in fact the asymptotic), basic sieves, and so on.

I believe he was in the middle of some sort of mathlib port. In any case I'd advise anyone against going ahead with this until Bhavik appears here with an update about the current state of the art.

[Alex Kontorovich]

In fact, thanks to @Vincent Beffara, the Rutgers group is quite close to showing that holomorphic functions on discs have primitives, and from there that holomorphic functions on simply connected domains have primitives. Then we should be able to do a lot more of the contour-pulling type argument that one would like... (We would also get complex logs on arbitrary branch cuts, and then combined with Vincent's work, the Riemann Mapping Theorem, which is a nice target of independent interest...)

[Thomas Bloom]

Indeed, I'd argue that unit-fractions is already a demonstration of analytic number theory being formalised 'in real time'.

[Eric Rodriguez]

Thomas Bloom said:

For the unit-fractions project, Bhavik Mehta did formalise quite a bit of 'basic' ANT, including things like Chebyshev estimates, divergence of 1/p (in fact the asymptotic), basic sieves, and so on.

I believe he was in the middle of some sort of mathlib port. In any case I'd advise anyone against going ahead with this until Bhavik appears here with an update about the current state of the art.

Oh yeah, I believe he even has the growth rate of it

[Thomas Bloom]

From memory, in unit-fractions we have: Chebyshev estimates for number of primes, asymptotic for sum of 1/p, related Mertens theorems like asymptotic for product of 1-1/p, divisor function upper bound, Eratosthenes-Legendre sieve, general partial summation lemmas.

[Thomas Bloom]

But all of the above just use elementary methods, nothing with complex analysis, which as Alex says is more problematic. In particular for PNT probably should set up enough complex analysis to.force the usual (Newman?) Proof through, rather than brute forcing an elementary proof through

[Thomas Bloom]

Although perhaps Florian Richter's recent elementary proof would be a good.project

[Alex Kontorovich]

I would suggest not doing one of the elementary approaches, but rather to go for a Riemann/Hadamard-de la Vallee Poussin - type proof of PNT (that is, using complex analysis), with some modern twists on smoothing/unsmoothing with Mellin convolutions and Hoffstein-Lockhart (+Goldfeld-Hoffstein) for the zero repulsion argument. (As in, e.g.: https://youtu.be/U11HOX8GZ3c) The reason is: this is very robust and will open up a world of possibilities, e.g., Hecke L-functions attached to modular forms, Rankin-Selberg, then Tate's thesis, etc etc...

[Thomas Bloom]

I agree, this way would be much better from a long term point of view, only question is whether there is enough complex analysis in place to make it feasible?

[Michael Stoll]

If there isn't, it should be provided.

[Terence Tao]

Perhaps a stretch goal would be to get as far as the Chebotarev density theorem?

[Michael Stoll]

That would be very good to have, as it is used frequently in applications.

[Terence Tao]

It would also be a good test of whether one can split up a complex project into more atomic pieces, where people only need to know one subfield of mathematics (e.g., complex analysis, analytic number theory, or algebraic number theory) to contribute to a single piece.

[Terence Tao]

@Kevin Buzzard Would Chebotarev density be useful at all for FLT?

[Alex Kontorovich]

I don't think Chebotarev is useful for FLT, but if we develop enough complex analysis to do PNT via contours, that will be important progress towards getting a trace formula, and Jacquet-Langlands is needed for FLT...

[Kevin Buzzard]

Cebotarev is surely needed for FLT. An R=T theorem is just a more precise way of giving a bijection between certain Galois representations and certain modular eigenforms. Given a modular eigenform, the Galois representation attached to it is characterised by the traces of Frobenius elements at a cofinite set of prime numbers. Without some form of Cebotarev you wouldn't know that the representation is uniquely determined by this data.

[Alex Kontorovich]

I stand corrected! So even better, PNT via complex analysis would open a path to Cheboratev as well...

[Terence Tao]

So perhaps we could open a Chebotarev subproject of FLT, and a PNT subproject of Chebotarev?

[Kevin Buzzard]

I have an FLT blueprint which is hugely incomplete and am slightly scared to open it because I have a heavy teaching load Jan to March and am worried that if I open it then suddenly everyone will be expecting me to run it, which I don't have the capacity to do right now (the grant starts in October but realistically I'll be able to run it from April)

[Terence Tao]

OK then maybe it makes more sense to focus for now on developing enough complex analysis and Dirichlet series theory to do PNT for now by the sort of complex analytic methods that extend to other L-functions, and just blackbox Chebatorev for FLT until someone manages to formalize it.

[Michael Stoll]

I would also think that it makes sense to aim at getting PNT and Dirichlet into Mathlib first:

• the results are important and useful (e.g., Hasse-Minkowski for quadratic forms depends on Dirichlet)
• the experience will help with more ambitious targets
• proofs can always be refactored later when more general results become available.

[David Loeffler]

I'm sorry to be dropping in late to this interesting discussion. One possibly relevant piece of info: the prime number theorem was recently formalised in Isabelle, by @Meow. I am not familiar with the details of the proof, but it certainly uses a lot of complex analysis, and gives the classical exp(sqrt log x) error term.

[Michael Stoll]

#9313 adds the fact in the title of this thread.

I think it makes sense to have that now, even though stronger results are very likely to be added soon from the unit fractions project:

• we want this specific result in any case, and it is better to have it earlier
• if desired, the proof can be refactored later

Reviews are welcome!

[Jz Pan]

I've heard that the elementary proof of PNT leads to large sieve method, which is also very important in analytic number theory. Is it correct?

[Terence Tao]

Jz Pan said:

I've heard that the elementary proof of PNT leads to large sieve method, which is also very important in analytic number theory. Is it correct?

The large sieve inequality is indeed important in ANT, though I don't know exactly how it is connected to the elementary proof of PNT other than that Selberg was heavily involved in both. The elementary proof usually requires the Brun-Titchmarsh inequality but this can be proven by a number of sieve methods (large sieve will work, but for instance the Selberg sieve will work just fine also).

If one is to do any serious analytic number theory in Lean (beyond "classical" multiplicative number theory, such as that required in the complex analytic proof of PNT, Dirichlet, Chebotarev, etc.) then sieve theory would definitely need to be implemented at some point, but that could be a bit messy (I'm hoping that a putative PNT project will give us experience in how to use asymptotic notation "in the style of analytic number theory", as this will be used a lot in sieve theory.)

[Junyan Xu]

Selberg sieve is here

[Michael Stoll]

I have now managed to produce a proof of the following.

import Mathlib
open Complex BigOperators EulerProduct

open scoped Nat.ArithmeticFunction in
lemma dirichletSeries_vonMangoldt_eq_neg_deriv_zeta_div_zeta {s : ℂ} (hs : 1 < s.re) :
    ∑' n : ℕ, Λ n * (n : ℂ) ^ (-s) = -deriv riemannZeta s / riemannZeta s :=  sorry

I'll generalize this to Dirichlet L-series and clean up my code in the next days, before starting PRing it to Mathlib.

To get from here to PNT, we need some version of the Wiener-Ikehara theorem and a proof that the zeta function does not vanish on Re = 1 (and the residue of the logarithmic derivative of zeta at 1).

[Alex Kontorovich]

May I ask a technical question: Why do you coerce n to ℂ here before raising to the -s? In "math" (as opposed to "mathlib"), this causes issues with complex powers of complex numbers, requiring branch cuts, etc. I would naively think that it would be better to coerce into, say, NNReal, where the power of a^b : NNReal^Complex can be defined as Real.exp(b Real.log a), with no need for branch cuts...?

[Alex Kontorovich]

And if we're going to be pulling contours, we'll need a residue theorem (for rectangles). I'm working on such now...

[David Loeffler]

Why do you coerce n to ℂ here before raising to the -s? [...] I would naively think that it would be better to coerce into, say, NNReal, where the power of a^b : NNReal^Complex can be defined as Real.exp(b Real.log a), with no need for branch cuts...?

Why use two coercions, if using one works? (I thought it was considered "good mathlib style" to avoid proliferation of subtypes as much as possible.)

[Kevin Buzzard]

If complex^complex is defined in lean then all the branch cut work must be done already.

[Michael Stoll]

One could set up HPow instances for Nat, Int, Rat, Real wth complex exponents (etc.), I suppose, but I suspect that this would lead to problems somewhere. There are some experts around who may be able to say more about that.

[Michael Stoll]

One pain point I encountered is that there are lemmas like docs#Complex.ofReal_log that apply to real numbers coerced to complex ones, but don't trigger (in a rewrite) when you have, say, a natural number coerced to a complex one. So I'm doing things like rw [..., show (n : Complex) = (n : Real) from rfl, <do something>, show ((n : Real) : Complex) = n from rfl, ...] a number of times. I have some idea how to improve on that; I'll try that out some time later today.

[Yaël Dillies]

In those cases you should have specific lemmas for coercions of naturals, integers...

[Michael Stoll]

But this would multiply the number of lemmas by n = #{Nat, Int, Rat, ....}.

[Michael Stoll]

I'll let you know if my idea works. But this will have to wait a bit.

[Yaël Dillies]

Michael Stoll said:

But this would multiply the number of lemmas by n = #{Nat, Int, Rat, ....}.

Yes, but that's fine because there are not so many such lemmas.

[Yaël Dillies]

This is what the rest of mathlib already does.

[Michael Stoll]

@loogle "Complex.", "ofReal"

[loogle]

:search: Complex.ofReal'.delaborator, Complex.ofReal', and 108 more

[Michael Stoll]

OK, not all of them are relevant, but I suspect it is still quite a lot...

[Michael Stoll]

I've started a new thread here to discuss this.

[Michael Stoll]

Michael Stoll said:

I have now managed to produce a proof of the following.

import Mathlib
open Complex BigOperators EulerProduct

open scoped Nat.ArithmeticFunction in
lemma dirichletSeries_vonMangoldt_eq_neg_deriv_zeta_div_zeta {s : ℂ} (hs : 1 < s.re) :
    ∑' n : ℕ, Λ n * (n : ℂ) ^ (-s) = -deriv riemannZeta s / riemannZeta s :=  sorry

I'll generalize this to Dirichlet L-series and clean up my code in the next days, before starting PRing it to Mathlib.

To get from here to PNT, we need some version of the Wiener-Ikehara theorem and a proof that the zeta function does not vanish on Re = 1 (and the residue of the logarithmic derivative of zeta at 1).

A status report:
I realized that it would make sense to build on the existing code for L-series and add more API (derivatives, products, convergence ...) and then deduce the result above from the existing relation between the von Mangoldt function and other arithmetic functions docs#Nat.ArithmeticFunction.vonMangoldt_mul_zeta rather than from the Euler product. So I've been working on L-series for a bit, and my code is slowly converging, but will need some more time.

Another question in this context (as L-series tend to converge conditionally in some vertical strip): Does Mathlib have a notion corresponding to the usual convergence of Nat-indexed series? I.e.

import Mathlib.Topology.Algebra.InfiniteSum.Basic

def HasSum_nat {M} [AddCommMonoid M] [TopologicalSpace M] (f : ℕ → M) (a : M) : Prop :=
  Filter.Tendsto (fun n ↦ (Finset.range n).sum f) Filter.atTop (nhds a)

(plus relevant API lemmas, of course...)

[Kevin Buzzard]

I don't think we have this and furthermore I don't think we've ever needed it. Will tsum not work for your application?

[Michael Stoll]

HasSum, Summable, tsum and friends are about absolute convergence (at least when the target is finite-dimensional over the reals). So when the sum converges conditionally, but not absolutely, then the tsum will be zero.

[Kevin Buzzard]

I see -- you're thinking about sums such as $1/1^s-1/3^s+1/5^s-1/7^s+\cdots$ and want to evaluate them at places like $s=1/2$?

[Yury G. Kudryashov]

no, we don't have separate definition for Tendsto (∑ i in range ⋅, f i) atTop (nhds a).

[Michael Stoll]

What I would like to have in particular is the conclusion that the limit function is holomorphic on the domain of conditional convergence. Do we have theorems about holomorphicity of limits of holomorphic functions?

[Chris Birkbeck]

We have that uniform limits of holomorphic functions are holomorphic docs#TendstoLocallyUniformlyOn.differentiableOn

[Michael Stoll]

What I have done so far on L-series is here. (This is not on the newest Mathlib as of now, but I will update when cache is working again.)
@Alex Kontorovich @Terence Tao @Kevin Buzzard

[Kevin Buzzard]

Presumably the idea is to PR everything to mathlib?

[Michael Stoll]

I have now managed to obtain a sorry-free proof of the following.

import Mathlib

open Filter Nat ArithmeticFunction

/-- A version of the *Wiener-Ikehara Tauberian Theorem*: If `f` is a nonnegative arithmetic
function whose L-series has a simple pole at `s = 1` with residue `A` and otherwise extends
continuously to the closed half-plane `re s ≥ 1`, then `∑ n < N, f n` is asymptotic to `A*N`. -/
def WienerIkeharaTheorem : Prop :=
  ∀ {f : ArithmeticFunction ℝ} {A : ℝ} {F : ℂ → ℂ}, (∀ n, 0 ≤ f n) →
    Set.EqOn F (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re} →
    ContinuousOn F {s | 1 ≤ s.re} →
    Tendsto (fun N : ℕ ↦ ((Finset.range N).sum f) / N) atTop (nhds A)

theorem PNT_vonMangoldt (WIT : WienerIkeharaTheorem) :
    Tendsto (fun N : ℕ ↦ ((Finset.range N).sum Λ) / N) atTop (nhds 1) := sorry

My current proofs of the analytic continuation of $\zeta'(s)/\zeta(s) + 1/(s-1)$ and of the non-vanishing of $\zeta$ on the line $\operatorname{Re}(s) = 1$ are a bit clunky, so I will try to polish them a bit before uploading then to my Euler Products repo.

[Michael Stoll]

So now somebody has to formalize a proof of Wiener-Ikehara :smile:

[Alex Kontorovich]

Yep! That'll be part of my forthcoming blueprint...

[Michael Stoll]

The code for the PNT reduction is now available here.

[Michael Stoll]

I have now refactored the proof of the non-vanishing of $\zeta$ on $\operatorname{Re} s = 1$ to use computations with big-O statements instead of working with explicit bounds. (The code is updated here.)

[Gareth Ma]

@Michael Stoll Hey, is your $\sum_n \Lambda(n)n^{-s}=-\zeta'(s)/\zeta(s)$ anywhere I can use for PNT?

[Gareth Ma]

I will also need $\sum_n \mu(n) n^{-s} = 1/\zeta(s)$, if you have that. From that the rest of my lemma should be easy c.f. other thread

[Gareth Ma]

Oh sorry, I should've checked EulerProduct.

[Michael Stoll]

The plan is to get this into Mathlib soon-ish.

[Gareth Ma]

I'm trying to use your EulerProducts to do the proofs. Does $\sum_n a_n n^{-s} = \sum_n b_n n^{-s}$ (as L-series, so L a = L b) imply $a_n = b_n$?
Lean:

example (a b : ℕ → ℂ) (h : L a = L b) : a = b := by sorry

[Gareth Ma]

I want to prove $(\Lambda * \mu)(n) = \mu(n)\log n$, which should follow straightaway from LSeries.deriv, LSeries_vonMangoldt_eq_deriv_riemannZeta_div, and some product rule stuff, but in the end I have to compare coefficients, and I'm wondering if that's easy.

[Terence Tao]

Gareth Ma said:

I want to prove $(\Lambda * \mu)(n) = \mu(n)\log n$, which should follow straightaway from LSeries.deriv, LSeries_vonMangoldt_eq_deriv_riemannZeta_div, and some product rule stuff, but in the end I have to compare coefficients, and I'm wondering if that's easy.

I can't speak for EulerProducts, but as long as both series have a non-trivial domain of convergence then the claim is true. (Proof: if the claim fails, then find the first natural number m where a m ≠ b m. Then show that m^s * (L a s - L b s) converges to the non-zero quantity a m - b m as s goes to infinity, a contradiction.)

In any event, uniqueness of Dirichlet series is fundamental enough that it ought to go into Mathlib, in my opinion.

[Kevin Buzzard]

I guess you can use mellin transforms and reduce to a claim about holomorphic functions having only one power series

[Michael Stoll]

That f ↦ L f is injective on f with abscissaOfAbsConv f < ⊤ should certainly be included in the LSeries part of Mathlib (but it currently isn't, also not in EulerProducts).

[Terence Tao]

It's possible that some of the Perron formula machinery developed at the PNT project may be able to get this injectivity cheaply, though aesthetically this would be a weird way to proceed. @Alex Kontorovich, what do you think?

[Gareth Ma]

I didn’t know LSeries is already in Mathlib, that’s amazing

[Michael Stoll]

Some things are there; more is on the way.

[Alex Kontorovich]

Terence Tao said:

It's possible that some of the Perron formula machinery developed at the PNT project may be able to get this injectivity cheaply, though aesthetically this would be a weird way to proceed. Alex Kontorovich, what do you think?

Oh, sure! If the L-series $L(f,s)=\sum a_n /n^s$ converges absolutely for some half-plane $\Re(s)>\sigma$, then we can already evaluate the Perron-type integral: $1/(2\pi i) \int_{(\sigma+1)}L(s) \frac{X^s}{s (s+1)} ds = \sum_{n<X} a_n (1 - n / X)$. So if $m$ is the first index for which $a_n \ne b_n$, take $X=m+1/2$. Then the sums $\sum_{n<X} a_n (1 - n / X)$ and $\sum_{n<X} b_n (1 - n / X)$ differ only on the last term; this is incompatible with $L(f,s)=L(g,s)$... Should be pretty easy to formalize that, I think?...