Class number formula

Stream: maths

[Riccardo Brasca]

How far are we from proving the class number formula? We don't have the regulator, but we have zeta functions, so maybe it's not completely crazy.

@Xavier Roblot @David Loeffler @Michael Stoll

[Michael Stoll]

The regulator would be a good first target. Then we need to define the Dedekind zeta function of a global field (or a Dedekind domain?) and prove its relevant properties. I think we have Minkowski's convex body theorem, which I seem to remember is used somewhere in the proof (of the class number formula)...

[David Loeffler]

I think we are a fair way away from proving the analytic continuation and functional equation for Dedekind zeta if a general number field (abelian fields are much easier of course, since we have Dirichlet L-series). Analytic continuation is not absolutely necessary for the class number formula, of course - it could be formulated as a one-sided limit - but it may mean the statement is less useful than otherwise.

[Xavier Roblot]

Defining the regulator should be easy: it is just the covolume of docs#NumberField.Units.unitLattice. I could
PR that in Mathlib if needed.

[Xavier Roblot]

Now, for the analytic class number formula, I did some work toward the computation of the limit of
$A(n)/n$ where $A(n)$ is the number of principal ideals of norm ≤ n. I have a bunch a PR, most
of them still WIP in that direction.

[Xavier Roblot]

For that, we need to define a cone in ℝ^r₁ × ℂ^r₂ with (r₁, r₂) the signature of a number field K that is a fundamental domain for the action of the image of the group of units. With the obvious norm on ℝ^r₁ × ℂ^r₂, the points of norm n in this cone that are images of elements of 𝓞 K are in bijection with principal ideals of 𝓞 K of norm n. This part is essentially done.

Then, standard techniques from the geometry of numbers give an estimate for the limit of the number of these points divided by n in term of some volume computation. This part is almost done: what is missing is the proof of a theorem of Lebesgue - Vitali that I mentioned in another thread in order to prove that the Riemann integral of the characteristic function of some set exists.

[Xavier Roblot]

Another big piece missing is the actual computation of the volume. This might be tricky to do in Lean since it requires some quite technical change of variables.

Once all of this is done, I think it should be fairly straightforward to prove some basic version of
the analytic class formula, at least as a formula for the limit of a real variable.

[Alex Kontorovich]

It may come in handy that we now have docs#MeasureTheory.addCovolume; @Heather Macbeth and I have been trying to develop these quotient volume techniques for just these kinds of applications... (e.g., see the class docs#MeasureTheory.AddQuotientMeasureEqMeasurePreimage)

[Riccardo Brasca]

Ok, maybe we should try to set up some sort of project in this direction. It seems like it's not completely science fiction. Personally I would be happy with the abelian version, but this is probably not really mathlib style.

[Riccardo Brasca]

Anyway the regulator is surely the first step, then we can try to at least state the formula.

[Johan Commelin]

A summary of this thread as a github project would be good. We can always blueprintify later.

[Antoine Chambert-Loir]

The presentation by Hida in his book Elementary theory ofL functions and Eisenstein series seems well suited to what is wanted here. Using the Shintani method for the meromorphic continuation, which will be a nice addition too.

[Xavier Roblot]

Alex Kontorovich said:

It may come in handy that we now have docs#MeasureTheory.addCovolume; Heather Macbeth and I have been trying to develop these quotient volume techniques for just these kinds of applications... (e.g., see the class docs#MeasureTheory.AddQuotientMeasureEqMeasurePreimage)

Yes, in fact, docs#Zlattice.covolume uses this. I added the definition of the regulator in #12504. As I said, defining the regulator is pretty straightforward, what is a bit trickier is how to formulate the fact that it is independent of the different choices. You can look at #12504 for a possible statement (without the proof yet :sweat_smile: ) but there may be better ways to express that: comments welcome!

[Riccardo Brasca]

A silly comment: I think that the regulator deserves its own file.

[Riccardo Brasca]

Johan Commelin said:

A summary of this thread as a github project would be good. We can always blueprintify later.

Voilà

[Xavier Roblot]

Riccardo Brasca said:

A silly comment: I think that the regulator deserves its own file.

Well, that is easy to solve.

Also, the first PR about the fundamental cone is ready for review #12268

[Xavier Roblot]

I have finally completed the formalization of the computation of the limit of
$A(n)/n$ where $A(n)$ is the number of principal ideals of norm ≤ n. More precisely, I
have a proof of the following result:

example (K : Type*) [Field K] [NumberField K] :
    Tendsto (fun n : ℝ ↦
      (Nat.card {I : (Ideal (𝓞 K))⁰ | IsPrincipal (I : Ideal (𝓞 K)) ∧
        absNorm (I : Ideal (𝓞 K)) ≤ n} : ℝ) / n) atTop
          (𝓝 ((2 ^ NrRealPlaces K * (2 * π) ^ NrComplexPlaces K * regulator K) /
            (torsionOrder K *  Real.sqrt |discr K|))) := by

I think this was the largest roadblock toward the proof of the Analytic Class Number Formula and
the rest of the proof should be (hopefully) relatively easy from here.

I'll start PR'ing this proof shortly while working on the end of the proof of the formula.

[Riccardo Brasca]

Oh wow, that's great!!

[Xavier Roblot]

It took way longer than I expected in the end. Indeed, as I mentioned above, a few months ago I
thought I was almost done since the only part remaining was the computation of some body X in
the mixed space ℝ^r₁ × ℂ^r₂ with (r₁, r₂) the signature of the number field. In the end, this part
was relatively easy. But another result was also needed to apply the theorem of Lebesgue - Vitali
that I mentioned in my post above. It is the fact that the set X is Jordan measurable, that is
that its frontier has (Lebesgue) measure zero. It turns out this part of the proof, which is barely
mentioned if at all in most of the books I looked at, is a lot trickier that expected. In the end,
I used the construction given in Marcus book (which necessitated to refactor the whole proof) where he
actually proves a stronger statement with an error term.

[Riccardo Brasca]

How did you do the computation of the volume mentioned above?

[Xavier Roblot]

This is proved using several changes of variables as it is done in most textbooks. It is a bit tedious but not so difficult.

[Yaël Dillies]

Xavier Roblot said:

But another result was also needed to apply the theorem of Lebesgue - Vitali
that I mentioned in my post above. It is the fact that the set X is Jordan measurable, that is
that its frontier has (Lebesgue) measure zero

Can you describe what the set is in a way I would understand? Jason and I are wondering whether we could golf your proof that it has null frontier.

[Antoine Chambert-Loir]

isn't this set convex?

[Xavier Roblot]

Yaël Dillies said:

Xavier Roblot said:

But another result was also needed to apply the theorem of Lebesgue - Vitali
that I mentioned in my post above. It is the fact that the set X is Jordan measurable, that is
that its frontier has (Lebesgue) measure zero

Can you describe what the set is in a way I would understand? Jason and I are wondering whether we could golf your proof that it has null frontier.

Do you want a textbook reference or some Lean code?

[Xavier Roblot]

Antoine Chambert-Loir said:

isn't this set convex?

I don't think so. I thought about it but could not prove anything in that direction.

[Xavier Roblot]

Xavier Roblot said:

Yaël Dillies said:

Xavier Roblot said:

But another result was also needed to apply the theorem of Lebesgue - Vitali
that I mentioned in my post above. It is the fact that the set X is Jordan measurable, that is
that its frontier has (Lebesgue) measure zero

Can you describe what the set is in a way I would understand? Jason and I are wondering whether we could golf your proof that it has null frontier.

Do you want a textbook reference or some Lean code?

If you want some Lean code, you can have a look at #12268. It is a bit outdated but the definitions are still good. The set in question is the set of elements in the fundamentalCone of norm ≤ 1. That is:

def normLessThanOne : Set (mixedSpace K) := {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1}

[Yaël Dillies]

I guess I will look through your code to piece the definitions together

[Xavier Roblot]

@Yaël Dillies , I have pushed a revised version of the file. Also, you should also know that, in the proof, what is proved is that the frontier of normLessThanOnePlus, the subset elements of normLessThanOne that are positive at real places (see below), has volume zero. From there, it is easy to prove that the frontier of normLessThanOne has also volume zero.

def normLessThanOnePlus : Set (mixedSpace K) := (normLessThanOne K) ∩ {x | ∀ w, 0 < x.1 w}

[Xavier Roblot]

I finally found the time to finish the proof. The PR is #17914. There is still a lot of polishing and breaking into smaller PRs to be done though.

[Riccardo Brasca]

This is great!!

[Riccardo Brasca]

Please ask for reviews!!

[Kevin Buzzard]

Yes congratulations! Although please don't ask me to review a 4000 line PR :-)

[Ruben Van de Velde]

How about a 3700 line one?

[Jz Pan]

Off topic: according to naming convention, NrRealPlaces should be nrRealPlaces, same for NrComplexPlaces.