analytical number theory

Stream: maths

[Kevin Buzzard]

This is a question for #maths

[Notification Bot]

2 messages were moved here from #lean4 > mathlib4 by Mario Carneiro.

[Kevin Buzzard]

There has been some offline talk about finding a good analytic number theory project but a good project needs a leader. Without good projects progress is eratic because it just happens when someone feels like doing something. Bhavik Mehta and Thomas Bloom formalised Bloom's theorem that any set of naturals with positive density contains a finite subset such that the sum of the reciprocals is 1, but we don't have the Riemann zeta function yet.

[Kevin Buzzard]

On the p-adic branch we have the p-adic zeta function though ;-) (although it will be factored out into its own project at some point)

[Meow]

Thanks, I'm writing some Lean code towards Riemann zeta function.

[Meow]

The project by Bhavik and Thomas is really famous and I knew it already. It's the first math result that was verified by machine before the paper was published in a peer-reviewed journal.

[Meow]

https://github.com/mmew-2022/Riemann_zeta/blob/main/theta_function.lean

[Meow]

Defined theta function, proved its convergence but not its functional equation.

[Kevin Buzzard]

I think @David Loeffler might be thinking about related issues

[Meow]

Where is the GitHub repository of p-adic zeta function in Lean?

[Meow]

I googled it but not given result.

[Kevin Buzzard]

Right now Ashvni's work is on the p-adic branch of mathlib, but she's going to move it to a separate repository at some point. She has the definition and is currently proving that its values at negative integers are related to Bernoulli numbers (in fact she is proving a more general result for p-adic L-functions attached to Dirichlet characters).

[David Loeffler]

Hi guys! As Kevin says, I've been working towards formalising some properties of Riemann zeta in Lean. I have a complete proof of the formula for zeta(2k), k >= 1, in terms of Bernoulli numbers; see PR #14701 for a complete working draft. I'm working on getting this cleaned up for inclusion into mathlib (it's waiting on some modifications to the Fourier series code, see #17598).

My longer-term goal is to prove the functional equation for zeta. There are proofs via contour integration, but that seems a bit tricky to formalise (because we don't have things like winding numbers in mathlib yet); so I'm hoping to prove it the way Riemann did, by taking the Mellin transform on both sides of the identity theta(i / (4x) ) = sqrt(x) theta(ix).

To get the modularity law for the theta function there are two steps:

• (1) prove Poisson summation for smooth rapidly-decaying functions on the real line;
• (2) show that exp(-x^2) is its own Fourier transform.
  I'm vaguely working towards (1) at the moment. If anyone wants to take on (2) then please be my guest :-)

[Kevin Buzzard]

@Alex Kontorovich you were asking about analytic number theory recently, here is evidence of some progress :-)

[Moritz Doll]

David Loeffler said:

Hi guys! As Kevin says, I've been working towards formalising some properties of Riemann zeta in Lean. I have a complete proof of the formula for zeta(2k), k >= 1, in terms of Bernoulli numbers; see PR #14701 for a complete working draft. I'm working on getting this cleaned up for inclusion into mathlib (it's waiting on some modifications to the Fourier series code, see #17598).

My longer-term goal is to prove the functional equation for zeta. There are proofs via contour integration, but that seems a bit tricky to formalise (because we don't have things like winding numbers in mathlib yet); so I'm hoping to prove it the way Riemann did, by taking the Mellin transform on both sides of the identity theta(i / (4x) ) = sqrt(x) theta(ix).

To get the modularity law for the theta function there are two steps:

• (1) prove Poisson summation for smooth rapidly-decaying functions on the real line;
• (2) show that exp(-x^2) is its own Fourier transform.
  I'm vaguely working towards (1) at the moment. If anyone wants to take on (2) then please be my guest :-)

Actually, I did think a bit about (1) as well, but haven't made any real progress - mainly because it is a bit more of a side goal for #16386 and more importantly I am spending too much time on the mathlib4 port.
I think I was trying to prove some trivial identities for the Fourier transform, which are needed to show that the Fourier transform is a continuous map on Schwartz space, but I haven't finished it yet

[Moritz Doll]

As for (2) I have put that on hold, because the proof of $e^{-|x|^2}$ being Schwartz is nicer if you have the Hermite polynomials

[David Loeffler]

If you just want to get to the theta transformation law, then I think you don't need a full theory of Schwartz functions. I'm no analyst, but it looks to me as if it is probably quite technical to show that "f Schwartz" implies "f-hat Schwartz". However that statement is automatic for the Gaussian because f-hat is f. I had envisaged proving a version of Poisson summation in which rapid decay of both f and f-hat were hypotheses.

[Moritz Doll]

ah that makes sense. I was going for the full distribution theory version (i.e., using the Dirac comb), as I am mainly interested in developing the Fourier theory and getting nice results about the zeta function would just be a cool bonus.
$\hat{f} \in \mathcal{S}$ provided that $f \in \mathcal{S}$ is mathematically trivial since $D_\xi \hat{f}(\xi) = \mathcal{F}_{x \to \xi} \{xf(x)\}$ and vice-versa (modulo constants). But since we are not using partial derivatives it is more annoying in mathlib. Then it reduces to commuting derivatives and multiplication by polynomials which is easy for humans, but hell for machines..

[Meow]

I'm working in almost same route ...

[Meow]

trying proof Poisson summation and Fourier transform for exp(-x^2)

[Meow]

-_-

[Moritz Doll]

Calculating the Fourier transform of $e^{-⟨Q x, x⟩/2}$ for a symmetric positive definite matrix $Q$ should be rather easy in Lean. The correct formulation would be of course in terms of an continuous linear map on an inner product space not a matrix. This just needs the diagonalization from docs#analysis.inner_product_space.spectrum and of course docs#integral_gaussian

[Alex Kontorovich]

Yes, @Heather Macbeth and I have been making slow but steady progress towards Poisson summation. You don't need step (2) to do zeta the "proper" way (with Mellin transforms of theta functions) - just do it a la Tate with test functions. You'll get Mellin transforms of those test functions instead of Gamma functions, and get meromorphic continuation that way. (Of course if you want to derive particular properties, it'll certainly help to take your test function to be the Gaussian...)

[Alex Kontorovich]

PS perhaps our progress is particularly slow because we want to do is as a "baby" trace formula; there are much slicker proofs of Poisson summation. But of course our goal is a "warmup" to Selberg...

[Alex Kontorovich]

PPS the mathematics of this is covered in lectures 2 and 3 in my grad course from last spring: https://sites.math.rutgers.edu/~alexk/2022S572/index.html

[Alex Kontorovich]

PPPS The Selberg trace formula is of course itself a warmup for Jacquet-Langlands, which is a rather important stepping stone on the path to Fermat/Wiles-Taylor...

[David Loeffler]

Moritz Doll said:

Calculating the Fourier transform of $e^{-⟨Q x, x⟩/2}$ for a symmetric positive definite matrix $Q$ should be rather easy in Lean. The correct formulation would be of course in terms of an continuous linear map on an inner product space not a matrix. This just needs the diagonalization from docs#analysis.inner_product_space.spectrum and of course docs#integral_gaussian

It seems to me that arguing with diagonalizations and linear maps will help you reduce from general Q to $Q = 1 \times 1$ identity matrix; but to prove that, some work needs to happen on the analytic side, to show that $\int exp(-(x + t i)^2)\, dx$ is independent of t. Probably this is not so hard though (we don't have integration over general contours, but we do have rectangular ones and that is all that's needed here).

[Moritz Doll]

I think that works only if all eigenvalues of $Q$ have non-negative real part. You cannot Fourier transform $e^{x^2}$.

[Moritz Doll]

It is not a tempered distribution, so you would need to come up with some regularization to make sense of the Fourier transform (that might exist, but I am not aware of it).

[Moritz Doll]

but for instance for $e^{i⟨Q x, x⟩}$ for $Q$ symmetric and real the contour argument works

[Moritz Doll]

There is the crucial point however is that we still lack some undergrad analysis both for real and complex variables.

[Moritz Doll]

Alex Kontorovich said:

PS perhaps our progress is particularly slow because we want to do is as a "baby" trace formula; there are much slicker proofs of Poisson summation. But of course our goal is a "warmup" to Selberg...

It would be really great to have Selberg's trace formula formalized, but that probably will take a while

[Meow]

Alex Kontorovich said:

PS perhaps our progress is particularly slow because we want to do it as a "baby" trace formula; there are much slicker proofs of Poisson summation. But of course our goal is a "warmup" to Selberg...

In details, which version of trace formula do you want to implement in Lean?

[Meow]

A Selberg trace formula for non-commutative discrete subgroup $\Gamma \subseteq G$, or a simpler version for commutative groups?

[Meow]

There are lots of technical details towards a formalized trace formula. For example, when we are considering Poisson summation, we need $f$ to be rapidly decreasing, a condition such as $|f(x)| \le C(1+|x|^{-1-\delta})$. What is the similar condition in general trace formula case?

[Meow]

@David Loeffler I proved
lemma integral_exp_neg_sq : (∫ (x : ℝ), ℝexp (-x^2) = √π)
now.

[Meow]

The code are in github repository https://github.com/mmew-2022/Riemann_zeta/blob/main/theta_function.lean

[Meow]

So it's really not far to prove (2).

[Meow]

Oh that's already done in mathlib -_-

[Meow]

I found it right now.

[David Loeffler]

Meow said:

So it's really not far to prove (2).

I think this takes some nontrivial work, evaluating $\int e^{itx} e^{-x^2}$ for general $t$ is not a straightforward generalisation of the $t = 0$ case.

[Moritz Doll]

if we can do linear changes of coordinates, then it should be rather easy.

[David Loeffler]

Moritz Doll said:

if we can do linear changes of coordinates, then it should be rather easy.

You want to just substitute x + it for x? Not as easy as it sounds. The substitution changes the path of integration in the complex plane, so it isn't just a case of linear variable change but you also need some argument about Cauchy's integral formula.

[Meow]

David Loeffler said:

Moritz Doll said:

if we can do linear changes of coordinates, then it should be rather easy.

You want to just substitute x + it for x? Not as easy as it sounds. The substitution changes the path of integration in the complex plane, so it isn't just a case of linear variable change but you also need some argument about Cauchy's integral formula.

Yes, I'm doing such computation about Cauchy's integral formula -_-

[Meow]

It needs estimation of exp(-z^2) when |Re z| is large

[Vincent Beffara]

Perhaps looking first at $\int e^{tx-x^2}$ (which can be obtained by a change of variable) and then using analytic continuation would be quicker?

[Meow]

@David Loeffler Now I finished proving it.
lemma fourier_exp_negsq (n : ℂ) : ∫ (x : ℝ), exp (Inx) * exp (-x^2) = exp (-n^2/4) * √π

[Meow]

https://github.com/mmew-2022/Riemann_zeta/blob/main/theta_function.lean

[Meow]

Vincent Beffara said:

Perhaps looking first at $\int e^{tx-x^2}$ (which can be obtained by a change of variable) and then using analytic continuation would be quicker?

Yes, that's a good method. But I've finished it before I seen the message :joy:

[Meow]

How can you proof $\int e^{tx-x^2}$ is analytic in variable t? It may be non-trivial in Lean.

[Meow]

We need a lemma that asserts $\int_{x \in X} f(t, x)$ is analytical in $t$, where $f(t, x)$ is a multi-variable analytic function, and $X$ is a set with some good properties.

[Vincent Beffara]

There is docs#has_deriv_at_integral_of_dominated_loc_of_lip which gives you complex differentiable, and then docs#differentiable_on.analytic_on gives you analytic, and then docs#analytic_on.eq_on_of_preconnected_of_frequently_eq extends the formula from the reals to the complex plane.

[Vincent Beffara]

Although, one important thing that is missing is contour integrals - but that will take a while ...

[Meow]

@Vincent Beffara Thanks!

[David Loeffler]

Meow said:

David Loeffler Now I finished proving it.
lemma fourier_exp_negsq (n : ℂ) : ∫ (x : ℝ), exp (Inx) * exp (-x^2) = exp (-n^2/4) * √π

Can you make a mathlib pull request for this? It would be good to have it in the library soon (maybe you could add it into analysis.special_functions.gaussian) rather than waiting for the conclusion of your whole theta-functions project.

[Meow]

David Loeffler said:

Meow said:

David Loeffler Now I finished proving it.
lemma fourier_exp_negsq (n : ℂ) : ∫ (x : ℝ), exp (Inx) * exp (-x^2) = exp (-n^2/4) * √π

Can you make a mathlib pull request for this? It would be good to have it in the library soon (maybe you could add it into analysis.special_functions.gaussian) rather than waiting for the conclusion of your whole theta-functions project.

Yes. It's my first time for making a pull request.

[David Loeffler]

@Meow Did you make a pull request for your Gaussian Fourier transform code?

[Meow]

https://github.com/leanprover-community/mathlib/pull/17845

[Meow]

@David Loeffler What is the counterexample for integral_prod_mulcan't be generalized to arbitrary Banach algebra?

[Meow]

Also, is there some relation between an integral and a summation in Lean? For example, in Lean we have Stieltjes measures, and the Stieltjes measure of $M$ when $f(x)=[x]$ is just the number of integral points of $M$. Then, summation can be viewed as a special type of integral, and swapping two $\sum$ symbols should be an application of Fubini's theorem.

[David Loeffler]

What is the counterexample for integral_prod_mul can't be generalized to arbitrary Banach algebra?

The point is that the underlying lemma integral_mul_left is carefully formulated so it's valid without assuming the function is integrable, with mathlib's convention that the integral of a non-integrable function is 0. If c = 0 then the assertion is just 0 = 0; and if c ≠ 0, then c * f is integrable iff f is, and c * 0 = 0, so we are safe. However, this breaks down in a more general ring: if c is neither zero nor a unit, it can occur that f is non-integrable, but c * f is integrable and has non-zero integral, in which case we're stuck. If you assume f is integrable then there is no problem, but adding this extra assumption would be annoying and would require adjusting every single place in the library where this lemma is used.

[Yaël Dillies]

Why can't we have both lemmas? Seems like neither subsumes the other.

[David Loeffler]

Sure, it would be worthwhile to have integral_mul_left_of_integrable (or integral_mul_left_of_unit, or both) with coefficients in an arbitrary Banach algebra, but I wanted to make the least invasive change to the library consistent with getting #18090 working.

[David Loeffler]

@Meow Regarding the rest of your message, I have no idea -- I suggest you might want to re-ask the question in a new zulip thread, since you want some input from measure theory / analysis people rather than number theorists.

[Meow]

Yes, for example in ring $\mathbb R \times \mathbb R$, consider $x : \mathbb R \mapsto (f(x),g(x))$ where $f(x)$ has non-zero integration and $g(x)$ is non-integrable, and multiplier $c=(1,0)$.

[Meow]

David Loeffler said:

What is the counterexample for integral_prod_mul can't be generalized to arbitrary Banach algebra?

The point is that the underlying lemma integral_mul_left is carefully formulated so it's valid without assuming the function is integrable, with mathlib's convention that the integral of a non-integrable function is 0. If c = 0 then the assertion is just 0 = 0; and if c ≠ 0, then c * f is integrable iff f is, and c * 0 = 0, so we are safe. However, this breaks down in a more general ring: if c is neither zero nor a unit, it can occur that f is non-integrable, but c * f is integrable and has non-zero integral, in which case we're stuck. If you assume f is integrable then there is no problem, but adding this extra assumption would be annoying and would require adjusting every single place in the library where this lemma is used.

so that is not true for such tricky reason.

[Meow]

David Loeffler said:

Meow Regarding the rest of your message, I have no idea -- I suggest you might want to re-ask the question in a new zulip thread, since you want some input from measure theory / analysis people rather than number theorists.

Analytical number theory relies a lot on some basic methods such as Abel's summation and Euler-Maclaurin summation, so I have to decide whether to work on a more general framework of Stieltjes measure, or only the special case of Abel's summation over $\mathbb R$.