Euler products

Stream: Is there code for X?

[Michael Stoll]

Is there support somewhere for proving that certain L-series have Euler products (and that both sides of the equation converge in a suitable right half-plane)?

Context: One of the projects in my formalization "seminar" is to formalize the L-series proof that asymptotically there are as many primes that are congruent to 1 mod 4 as primes that are congruent to 3 mod 4 (in terms of Dirichlet density). The student doing this will need the Euler product expansion of the zeta function and the Dirichlet L-function of the quadratic character mod 4.

• There seems to be quite a lot of API for infinite sums, but I have not found anything for infinite products. Am I missing something?
• There is some material on the zeta function, but it does not include the Euler product, as far as I can see. @David Loeffler ?

[David Loeffler]

Hi Michael:

• AFAIK there is barely any general API for infinite products. It's been discussed before on zulip, and got a bit bogged down in arguments over what the definitions should be, e.g. what it means for a product to "converge" when some of its terms are zero. For the infinite product for the sine function (a product due to Euler, but not an "Euler product" in the usual sense!) I ducked the issue by working with the sequence of partial products over fin n.

• There is a lot of material on the zeta function – specifically, the formula for even integer values in terms of Bernoulli numbers, and the meromorphic continuation. The former is already mostly there for general Dirichlet characters, but that doesn't seem to be so relevant here. Adapting the analytic-continuation proof to handle more general Dirichlet characters should be no problem, it's just a matter of adding an extra parameter into a bunch of already-written stuff (the starting point would be to generalise docs#Complex.tsum_exp_neg_mul_int_sq, which is the Poisson summation formula applied to $x \mapsto exp(-a x ^ 2)$, to allow $x \mapsto \exp(-a x ^ 2 + i t x)$ for an arbitrary $t$). I meant to do this myself but it got overtaken by the lean4 port and then I forgot about it :embarrassed:

[David Loeffler]

Here is the previous discussion I mentioned: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/infinite.20product.20clash.20with.20type.20product/near/326028832
The stumbling block, if I understand correctly, is that there doesn't seem to be a single notion of "infinitely iterated operation in a topological monoid" that is consistent with the usual mathematical usage of infinite sums and infinite products.

[Michael Stoll]

Thanks. It looks like we will have to see what it is precisely that we need (I assume, in the end it's the logarithmic derivative as a Dirichlet series) and then come up with some way of getting there. I assume we'll need something like products over {p : Finset.range n | p.val.Prime} ...

[Michael Stoll]

Here is a suitable statement for the zeta function.

import Mathlib -- being lazy

def primesBelow (n : ℕ) : Finset ℕ := (Finset.range n).filter (fun p ↦ p.Prime)

open scoped Topology

open Filter in
example {s : ℂ} (hs : 1 < s.re) :
    Tendsto (fun n : ℕ ↦ ∏ p in primesBelow n, 1 / (1 - p^(-s)) ) atTop (𝓝 (riemannZeta s)) := by
  sorry

Let's see if/how we get there... (EDIT: fixed the filter on ℕ)

[Michael Stoll]

@David Loeffler: In the module docstring for file#Mathlib/NumberTheory/ZetaFunction, zeta_eq_tsum_of_one_lt_reshould be replaced by zeta_eq_tsum_one_div_nat_add_one_cpow.

[Michael Stoll]

Writing example {s : ℂ} (h : |s| < 1) : ... I get the message failed to synthesize instance Abs ℂ.
OK; I guess I want the real absolute value, which is not compatible with the Abs notation class.
Do I really have to write Complex.abs.toFun s? There should be something more like |s|.

[David Loeffler]

I think using norm (rather than abs) works better for ℂ.

[Ruben Van de Velde]

Definitely Complex.abs s should work, no need for Complex.abs.toFun s

[Michael Stoll]

OK. But s.absdoes not...

[Ruben Van de Velde]

Yeah, dot notation like that seems to only work if Complex.abs is a real function, not for a bundled one

[Ruben Van de Velde]

Not sure if anyone filed an issue about that

[David Loeffler]

Michael Stoll said:

David Loeffler: In the module docstring for file#Mathlib/NumberTheory/ZetaFunction, zeta_eq_tsum_of_one_lt_reshould be replaced by zeta_eq_tsum_one_div_nat_add_one_cpow.

PR at #8153

[Yaël Dillies]

Sorry but can we just not use Complex.abs anymore and use ‖ ‖ instead?

[Yaël Dillies]

One of my most hated simp lemmas of all time is docs#Complex.norm_eq_abs.

[Michael Stoll]

There is geom_sum and friends, but tsum_geometric. Sigh...

[Michael Stoll]

BTW, #find (∑' (n : ℕ), _ ^ n) times out.

[Yaël Dillies]

Let me advertise !3#18405 which I think is a necessary first step.

[Eric Rodriguez]

!3 :shocked:

[Michael Stoll]

I don't find

import Mathlib

example {n : ℕ} (h : n ≠ 0) (s : ℂ) : Complex.abs ((n : ℂ) ^ s) = (n : ℝ) ^ s.re := sorry

(same with Complex.norm)

[Ruben Van de Velde]

example {n : ℕ} (h : n ≠ 0) (s : ℂ) : Complex.abs ((n : ℂ) ^ s) = (n : ℝ) ^ s.re :=
  Complex.abs_cpow_eq_rpow_re_of_pos (Nat.cast_pos.mpr h.bot_lt) s

[Michael Stoll]

I have now produced some 300 lines of code culminating in the following results.

theorem euler_product {F : Type*} [NormedField F] [CompleteSpace F] {f : ℕ → F} (hsum : Summable (‖f ·‖))
    (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) (hmul : ∀ {m n}, Nat.Coprime m n → f (m * n) = f m * f n) :
    Tendsto (fun n : ℕ ↦ ∏ p in primesBelow n, ∑' e, f (p ^ e)) atTop (𝓝 (∑' n, f n)) := sorry

theorem euler_product_multiplicative {F : Type*} [NormedField F] [CompleteSpace F] {f : ℕ →*₀ F}
    (hsum : Summable fun x => ‖f x‖) :
    Tendsto (fun n : ℕ ↦ ∏ p in primesBelow n, (1 - f p)⁻¹) atTop (𝓝 (∑' n, f n)) := sorry

theorem riemannZeta_eulerProduct {s : ℂ} (hs : 1 < s.re) :
    Tendsto (fun n : ℕ ↦ ∏ p in primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹) atTop (𝓝 (riemannZeta s))

Thanks for all the help!

[Michael Stoll]

On the way, I am intrducing definitions

namespace Nat

/-- `primesBelow n` is the set of primes less than `n` as a finset. -/
abbrev primesBelow (n : ℕ) : Finset ℕ := (Finset.range n).filter (fun p ↦ p.Prime)

/-- `factorsBelow n` is the set of positive natural numbers all of whose prime factors
are less than `n`. -/
abbrev factorsBelow (n : ℕ) : Set ℕ := {m | m ≠ 0 ∧ ∀ p ∈ factors m, p < n}

with some API. My plan would be to begin with a PR adding these to Mathlib, to be followed by the general theorems above, and finally the special case with the zeta function.

[Gareth Ma]

I just saw this thread, RIP. I have been working on the exact same results and same APIs for the past week, and for my project in general.

[Michael Stoll]

@Gareth Ma My current version is here.
Is yours available somewhere, so we can compare?

[Gareth Ma]

[here] is the relevant parts, prime_Ico is your primesBelow, and smooth is your factorsBelow. I also had Pr which is Primorial and rough for a funny name. You saw my #maths thread, that one is in progress but shouldn't be terrible, and I think it's a slightly more general version of your result.

[Gareth Ma]

At least it's very closely related

[Gareth Ma]

Also I think you can replace all your Tendsto ... atTop ... with hasSum (and swapping the arguments), though not sure if that's what you want

[Michael Stoll]

Gareth Ma said:

[here] is the relevant parts,

You did not put in the URL.

[Gareth Ma]

lmao here

[Michael Stoll]

Gareth Ma said:

Also I think you can replace all your Tendsto ... atTop ... with hasSum (and swapping the arguments), though not sure if that's what you want

I don't think so, as the LHS is a product, not a sum. Once infinite products are in, it can be written more succinctly.

[Gareth Ma]

ok

[Gareth Ma]

But yes, if you get your results into Mathlib I can also add mine in I guess

[Michael Stoll]

I'll have to go home now. I'll have a look later.

[Michael Stoll]

I have now made the first PR (#8252). It sets up a new file Mathlib.NumberTheory.SmoothNumbers with the definitions of primesBelow and smoothNumbers, the relevant API lemmas and the equivalence ℕ × smoothNumbers p ≃ smoothNumbers p.succ when p is prime.

[Michael Stoll]

Here is another small preparatory PR: #8325 . It adds two API lemmas on HasSum/tsum that I found useful.

[Antoine Chambert-Loir]

Is it worthy to expand tsum_eq_tsum_diff_singleton to a set of zero-values, to a finite set of values, or given an inclusion of supports?

[Michael Stoll]

Maybe. The case I need is functions on Nat taking the value zero at zero, so the current version is already generalized a bit. But I can try to come up with something more general that is as easy to use.

[Michael Stoll]

I've added a version for arbitrary set differences.

[Michael Stoll]

The first real Euler products PR is now at #8410 . It proves the general formula for Euler products, once for functions that are only multiplicative on coprime arguments (which is the minimal requirement) and once for completely multiplicative ones (using the formula for the geometric series).

[Michael Stoll]

#8751 is the next PR. It proves the Euler product formula for the Riemann zeta function and for Dirichlet L-series.