L-series

Stream: PrimeNumberTheorem+

[Michael Stoll]

I have started PRing material on L-series from EulerProducts to Mathlib: #10725, #10728. Reviews welcome!

[Terence Tao]

One thing we might start doing in parallel with the main contour integration stuff is to lay the groundwork for the PNT in arithmetic progressions by showing that $L(1,\chi) \neq 0$ and $L(1+it,\chi) \neq 0$ for Dirichlet characters $\chi$, and that $L(s,\chi)$ has a holomorphic continuation into the critical strip. Do you have material from EulerProducts that might be helpful for these purposes? For instance, we could use Euler products to prove the inequality
$\prod_{\chi\ (q)} L(\sigma, \chi) \geq 1$
for $\sigma > 1$, which already demonstrates nonvanishing of $L(1,\chi)$ in the complex case, and similarly
$L(\sigma,\chi_0)^3 |L(\sigma+it,\chi)|^4 |L(\sigma+2it,\chi^2)| \geq 1$
for $\sigma > 1$ and real $t$, which also demonstrates nonvanishing of $L(1+it,\chi)$ for non-zero $t$.

For the non-vanishing of $L(1,\chi)$ for real $\chi$ there are a number of options. There are some elementary proofs that don't look too challenging (other than having to do a bunch of asymptotic estimation), such as the one based on the divergence of $\sum_{n=1}^\infty \frac{1*\chi(n)}{\sqrt{n}}$, or one can be much more algebraic and shoot for the class number formula (which would be independently valuable for Mathlib I imagine). The latter is more complicated may be worth doing anyway as a warmup to Chebotarev.

[Terence Tao]

p.s. an intermediate proof is to argue by contradiction: if $L(1,\chi)=0$ then $\zeta(s) L(s,\chi)$ has an analytic continuation into the strip, hence by Perron's formula $\sum_{n=1}^\infty \frac{1*\chi(n)}{\sqrt{n}}$ will converge, contradiction. This proof is terrible for quantitative bounds, but may be relatively "cheap" given that we will likely have most of the Perron formula infrastructure in place already.

[Michael Stoll]

Some of this is in PNT.lean in the EulerProducts repository.

I was waiting for @David Loeffler to provide the analytic continuation of Dirichlet L-series in order to add a proof that $L(1, \chi) \neq 0$ (for quadratic $\chi$; for the other ones one can deduce it from the lower bound on the power product).

[Michael Stoll]

My idea for this proof was to use that $\zeta(s) L(s, \chi)$ is entire (if $L(1, \chi) = 0$) and then argue that its derivatives at a convenient real point (say $s = 2$) are alternating in sign, forcing the values on the real axis to the left of it to be positive, which contradicts $\zeta(-2) = 0$.

[Terence Tao]

OK, that works as well, though it requires analytic continuation well to the left of the critical strip, which I guess is worth doing but sounds like more work.

I see that you have indeed already demonstrated $L(\sigma,\chi_0)^3 |L(\sigma+it,\chi)|^4 |L(\sigma+2it,\chi^2)| \geq 1$ in PNT.lean, which is great! Actually on setting $t=0$ I see this also shows non-vanishing of $L(1,\chi)$ in the complex case, so there is no need to bring in the alternate inequality $\prod_{\chi\ (q)} L(\sigma, \chi) \geq 1$.

[David Loeffler]

I have a complete proof formalised of analytic continuation of Hurwitz zeta functions $\sum_{n \in \mathbb{N}} 1 / (n + a)^s$ for any $a \in [0, 1]$; I will begin PR'ing this later this week. Deducing analytic continuation of Dirichlet L-functions is an easy step from this (taking weighted sum over $a = r / n$ for $0 \le r < n$).

[David Loeffler]

By the way, I have a (totally content-free) question about conventions for zeta functions, and I'd like to run it past you guys to determine what is the preferred spelling. The issue is how to most simply formulate the naive sum definition of L-functions, given that in mathlib $0 \in \mathbb{N}$ (but $0^s = 0$ for $s \ne 0$).

[David Loeffler]

/poll How should the Riemann zeta function be written?
∑' n : ℕ, 1 / (n : ℂ) ^ s
∑' n : ℕ, 1 / (n + 1 : ℂ) ^ s
∑' n : ℕ, if n = 0 then 0 else 1 / (n : ℂ) ^ s
Something else

[Yaël Dillies]

(my vote is from past experience with similar issues, maybe I am missing zeta-specific subtleties)

[David Loeffler]

@Alex Kontorovich @Michael Stoll I'm particularly interested in which of these options will most easily link up with the code you have written / are writing.

[Vincent Beffara]

How about ∑' n : ℕ+, 1 / (n : ℂ) ^ s ?

[Yaël Dillies]

That's more annoying to work with in practice, I found

[Michael Stoll]

The first option is easiest to work with, I would think, and is used in docs#zeta_eq_tsum_one_div_nat_cpow. The second one is used in docs#zeta_eq_tsum_one_div_nat_add_one_cpow. The third one agrees with LSeries ζ(where ζ is the arithmetic function $\zeta$). They probably all have advantages and disadvantages. I would suggest to have both (1) and (2) (also for Dirichlet L-series perhaps) as is already the case, so that one can easily use whatever is more convenient (and also (3) in the form LSeries ArithmeticFunction.zeta s = riemannZeta s for 1 < s.re; see LSeries.zeta_eq_riemannZeta in DirichletLSeries.lean).

[Alex Kontorovich]

I wonder how useful ArithmeticFunction is for Dirichlet series... Precisely because Mathlib chose to define 1/0 = 0, we just might be able to get away with doing everything over $\N$, and indexing it the "natural" way... (Perhaps there's an issue with $s=0$ and $0^0=1$? But then the tsum should not converge, so the whole series should anyway be defined to be zero... There's a kind of magic here with junk values perfectly balancing each other...?)

[Michael Stoll]

It is actually pretty useful, since arithmetic functions are defined on ℕ, but with value zero at zero. So you can just take ∑' n : ℕ, f n / n ^ s (modulo coercions).

[Alex Kontorovich]

Yes I see the utility of ArithmeticFunction in other contexts, but for Dirichlet series, won't ∑' n : ℕ, f n / n ^ s work just as well for f that are not defined to be zero at zero, because dividing by $0^s$ will anyway kill that term...?

[Michael Stoll]

Well, there are cases where the series converges at s = 0, and then the special case 0^0 = 1 is a problem.

[Michael Stoll]

For Dirichlet L-series, it is of course OK.

[David Loeffler]

Michael Stoll said:

Well, there are cases where the series converges at s = 0, and then the special case 0^0 = 1 is a problem.

Are there, though? I spent a while trying to think of an example of an "arithmetically interesting" function such that $\sum a(n)$ converges and $a(0) \ne 0$, and didn't find any.

[Michael Stoll]

Is 2^(-n) arithmetically interesting?

[David Loeffler]

Does $\sum 2^{-n} n^{-s}$ have any arithmetic significance? If so, I'm not aware of it.

[Michael Stoll]

What I want to say is, we should not make unnecessary assumptions regarding the coefficient sequences that might show up.

[Michael Stoll]

And defining a coercion from Dirichlet characters to arithmetic functions so that we can write LSeries χ when χ is a Dirichlet character works reasonably well.

[Alex Kontorovich]

I guess my question is whether it would go through equally well if we just coerced Dirichlet characters to functions on Nat...?

[Michael Stoll]

Not without changing LSeries (which eats a complex-valued arithmetic function).