Odlyzko bounds

Stream: FLT

[Thomas Browning]

Is anyone planning on tackling (6) anytime soon? If not, I might starting exploring whether it's feasible to formalize some of Odlyzko.

[Kevin Buzzard]

[This is (6) in this message, sorry, I moved the discussion on this bound to a new thread. It's

(6) If $K/\mathbb{Q}$ is a finite Galois extension with discriminant $D$, and if $D^{1/[K:\mathbb{Q}]}<8.25$ then $[K:\mathbb{Q}]<18$. The only reference I know for this is the tables of Diaz y Diaz (F. Diaz y Diaz, Tables minorant la racine n-ième du discriminant d’un corps de degré n,
Publ. Math. d’Orsay, 1980) but IIRC there is no proof there?

I later point out that $K$ is known to be totally imaginary in the application.
]

It's only now that I've made this kind of detail public and I've got no plans to formalise it myself

[Andrew Yang]

I think the PNT+ people have plans about dedekind zeta functions so there might be useful things in their repo?

[David Michael Roberts]

Even before formalisation: has the work of Diaz y Diaz been replicated independently in a trustworthy package (or packages?) Compare the ATLAS work to recompute all those character tables that were only done once in the 70s....

[Chris Birkbeck]

Maybe in the LMFDB?

[David Loeffler]

Andrew Yang said:

I think the PNT+ people have plans about dedekind zeta functions so there might be useful things in their repo?

For anything about Dedekind zeta functions the expert is definitely @Xavier Roblot

[Xavier Roblot]

I have defined the Dedekind zeta function in my work on the Analytic Class Number Formula #17914, but I think there is still a lot of work to get anywhere close to the results needed to get this kind of bounds on the root discriminant. About the question of @David Michael Roberts, I am pretty sure most of the computations of Diaz y Diaz have been redone (and improved) by the PARI/GP team. I can ask them to see what method they used. Also, @Kevin Buzzard, is the bound above sharp or is there a little wiggle room? In this kind of situation, this can make a lot of difference for the difficulty of formalizing the result.

[Andrew Yang]

I think the bound on diaz y diaz gives <= 14 and we only need < 18

[Ruben Van de Velde]

I think this is covered at the end of https://web.stanford.edu/~dkim04/automorphy-lifting/2025-01-10/ , so what Andrew said

[David Michael Roberts]

if we use an improved bound of Poitou, then we get $n\leq 14$ and $6 \mid n$ and so...

uncited, sadly.

[Ruben Van de Velde]

Maybe one of the references of https://encyclopediaofmath.org/wiki/Odlyzko_bounds

[David Michael Roberts]

Thanks, was just looking at that. This seems likely:

• Poitou, Georges. Minorations de discriminants, in Séminaire Bourbaki : vol. 1975/76, exposés 471-488, Séminaire Bourbaki, no. 18 (1977), Talk no. 479, 18 p. http://www.numdam.org/item/SB_1975-1976__18__136_0/

as it explicitly mentions the Minkowski bound and then variations on it (which I can only presume are strengthenings, I didn't read it closely)

[Xavier Roblot]

The paper of Diaz y Diaz is here: http://sites.mathdoc.fr/PMO/PDF/D_DIAZ_80_06.pdf

[Kevin Buzzard]

Oh I should add that in the application the field $K$ is totally imaginary, so the relevant table is on p26 of the pdf linked in the previous message.

[Notification Bot]

14 messages were moved here from #FLT > Notes on the proof of FLT which is being formalized by Kevin Buzzard.

[Ruben Van de Velde]

Also we're missing step 1: formalize the statement :)

[Thomas Browning]

Ultimately, I suspect the paper worth formalizing is "Some Analytic Estimates of Class Numbers and Discriminants" (which has bounds that are good for small n), but the starting point is Stark's discriminant formula in equation (3.1). A proof of this formula is given in "Lower bounds for discriminants of number fields" using the functional equation of the Dedekind zeta function and Hadamard's factorization theorem. So I think those are the two main pieces of machinery that we are missing to at least get off the ground.

[Kevin Buzzard]

Ruben Van de Velde said:

Also we're missing step 1: formalize the statement :)

import Mathlib.NumberTheory.NumberField.Discriminant.Defs

open Polynomial NumberField Module

axiom Odlyzko_statement (K : Type*) [Field K] [NumberField K] [Normal ℚ K]
  (hIm : ¬ Irreducible (X ^ 2 + C (3 : K)))
  (hBound : |(discr K : ℝ)| < 8.25 ^ finrank ℚ K) : finrank ℚ K ≤ 17

[Kevin Buzzard]

hIm is just a way of guaranteeing that K is totally imaginary; it will be true in our application. The $< 8.25$ can be replaced by $< 2^{2/3}3^{3/2} = 8.248377821...$ if it helps.

[Kevin Buzzard]

If someone wants to carefully look at the statement and check that it seems to correspond to what I said above, then I could push the statement to FLT

[Alex Kontorovich]

Thomas Browning said:

Ultimately, I suspect the paper worth formalizing is "Some Analytic Estimates of Class Numbers and Discriminants" (which has bounds that are good for small n), but the starting point is Stark's discriminant formula in equation (3.1). A proof of this formula is given in "Lower bounds for discriminants of number fields" using the functional equation of the Dedekind zeta function and Hadamard's factorization theorem. So I think those are the two main pieces of machinery that we are missing to at least get off the ground.

It's possible that the use of Hadamard here can be substituted by the Borel-Caratheodory theorem, which the PNT+ project hopes to add... (FE for Dedekind zeta should be even more within the realm of possibility...?)

[Johan Commelin]

If K is totally imaginary, then you know that finrank Q K will be even, right? So you might as well sharpen the conclusion to le 16.

[Kevin Buzzard]

That makes it harder to prove, right? In fact the bound in Diaz y Diaz is 14.

[Johan Commelin]

My point is that it will only be epsilon harder, because your hIm implies that K is an extension of $\mathbb{Q}(\sqrt{-3})$.

[Xavier Roblot]

Yeah, the fact that K is an extension of ${Q}(\sqrt{-3})$ could be useful. Do you have any information on the Galois group?

[Kevin Buzzard]

It's a finite subgroup of GL_2(F_p-bar) and I know things about what the decomposition subgroups at 2 and 3 look like.

[Terence Tao]

PNT+ currently only has the barest outline of a proof of Chebotarev for Dedekind zeta functions in the blueprint, and nothing in Lean, so we have nothing to offer you currently. But it would be good to know what other projects are doing with regards to constructing this function (for our Wiener-Ikehara type arguments we need to construct the zeta function to the right of the critical strip, and extend continuously to the edge of the strip with a known pole at s=1 and no zeroes on that edge. Currently we don't even have a definition of a Dedekind zeta in Lean yet, though.)

[Andrew Yang]

After digging through some references:
I think the stark formula itself (with the crudest bound) only gives $n \le 144$.

According to the table on the last page of "Some Analytic Estimates of Class Numbers and Discriminants", it probably only gives a bound between $20$ and $30$.

"Poitou, Georges. Minorations de discriminants" seems to give a bound (for totally imaginary field; see p.148 eq. 21) of $n \le 18.95$. (Or see "Poitou, Georges. Sur les petits discriminants" end of p.12).

[Alex Kontorovich]

Terence Tao said:

PNT+ currently only has the barest outline of a proof of Chebotarev for Dedekind zeta functions in the blueprint, and nothing in Lean, so we have nothing to offer you currently. But it would be good to know what other projects are doing with regards to constructing this function (for our Wiener-Ikehara type arguments we need to construct the zeta function to the right of the critical strip, and extend continuously to the edge of the strip with a known pole at s=1 and no zeroes on that edge. Currently we don't even have a definition of a Dedekind zeta in Lean yet, though.)

Dedekind zeta is making its way into Mathlib, FYI: #17914

[Bhavik Mehta]

@Kevin Buzzard, yesterday before you went home, you mentioned needing a proof of

$$\frac{\pi}{4} \frac{n^2}{{n!}^{\frac2n}} < 2 ^ \frac{2}{3} 3 ^ \frac{7}{8} \Longrightarrow n \leq 14.$$

Today I have a sorry-free proof that

$$\frac{\pi}{4} \frac{n^2}{{n!}^{\frac2n}} < 2 ^ \frac{2}{3} 3 ^ \frac{7}{8} \iff n < 14.$$

I don't know how this fits into the project overall, so just let me know where I should PR it!

[Kevin Buzzard]

I have a WIP PR FLT#409 which it could go into!

[Kevin Buzzard]

In fact let me use this as an excuse to say what I've been doing for the last week or so, which is: spring cleaning. I went through a bunch of old branches and either deleted or revitalised them, opening a bunch more WIP PRs. I made a bit more progress on the impending adele refactor branch; I think what needs to be done now is a rewriting of the plan for $\mathbb{A}_K\otimes L=\mathbb{A}_L$ given that our current one is disrupted (it goes via objects like $\prod_v K_v$ which will no longer have names if #23542 is merged). Today I very much hope to get to the three PRs opened by other people in the last 10 days or so.

[Kevin Buzzard]

The other thing we need is $\pi n^2/(4(n!)^{2/n})<2.75$ implies $n<6$; this is presumably now easy for you.

[Kevin Buzzard]

@Xavier Roblot do we have that if $L$ is a totally complex number field of degree $n$ and discriminant $d$ then $|d|^{1/n}\geq\pi n^2/(4(n!)^{2/n})$?

[Kevin Buzzard]

The hard thing I need is that if $|d|^{1/n}<8.25$ then $n<18$ and Minkowski's bound above isn't enough for this, but the claim follows from the table on the last page of https://www.numdam.org/item/SDPP_1976-1977__18_1_A6_0/

[Ruben Van de Velde]

1977 means we can sorry it, right? :innocent:

[Kevin Buzzard]

Yes. The reason it came up was that I was starting to think about precise formalizations of the things I was planning on sorrying for now.

[Ilmārs Cīrulis]

Kevin Buzzard said:

The other thing we need is $\pi n^2/(4(n!)^{2/n})<2.75$ implies $n<6$; this is presumably now easy for you.

May I try this? :sweat_smile:

[Kevin Buzzard]

I think Bhavik might basically have done it already.

[Xavier Roblot]

Kevin Buzzard said:

Xavier Roblot do we have that if $L$ is a totally complex number field of degree $n$ and discriminant $d$ then $|d|^{1/n}\geq\pi n^2/(4(n!)^{2/n})$?

We don't have this exact theorem but the more general NumberField.abs_discr_ge. Still, all the tools are there to prove this statement so it should be quite easy to prove. Well, it's probably a direct consequence of NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr

[Kevin Buzzard]

By "more general" do you mean "weaker"?

[Xavier Roblot]

I meant also apply to not totally complex fields (and thus is weaker)

[Xavier Roblot]

The statement that is very easy to prove from what we have is:

theorem abs_discr_ge_of_isTotallyComplex [IsTotallyComplex K] :
    (finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (finrank ℚ K) *
      (finrank ℚ K).factorial ^ 2) ≤ |discr K| := by

It is what you want but not necessarily stated as you want. Still, is it good enough?

[Bhavik Mehta]

Kevin Buzzard said:

The other thing we need is $\pi n^2/(4(n!)^{2/n})<2.75$ implies $n<6$; this is presumably now easy for you.

Yup,

theorem kevin2 {n : ℕ} :
    (π / 4) * (n ^ 2 / (n !) ^ (2 / n : ℝ)) < 2.75 ↔ n < 5 := by

was an easy addition

[Kevin Buzzard]

Xavier Roblot said:

The statement that is very easy to prove from what we have is:

theorem abs_discr_ge_of_isTotallyComplex [IsTotallyComplex K] :
    (finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (finrank ℚ K) *
      (finrank ℚ K).factorial ^ 2) ≤ |discr K| := by

It is what you want but not necessarily stated as you want. Still, is it good enough?

Oh sure, that's trivially mathematically equivalent if I got it right. That would be a great addition to mathlib!

[Notification Bot]

16 messages were moved here from #FLT > Rolling update by Kevin Buzzard.

[Xavier Roblot]

#24076

[Kevin Buzzard]

@Bhavik Mehta @Xavier Roblot just flagging that I moved the discussion here.

[Bhavik Mehta]

From this, should I reformulate to n ^ (n * 2) / ((4 / π) ^ n * n! ^ 2) <= _ ^ n? The first step of my proof is rearranging into a form which makes the analysis easier, so it's not a lot of trouble to adjust the main statement in a way which doesn't disrupt the rest of the proof

[Kevin Buzzard]

Xavier is doing the basic theory so for him the fundamental invariant is $|d|$. But for the more advanced paper the fundamental invariant is the so-called "root discriminant" which is $|d|^{1/n}$. It's presumably easy to switch between the two!

[Xavier Roblot]

Yes, at some point, it will be worthwhile to add the root discriminant versions.

[Xavier Roblot]

(I guess I can just add those in this PR)