feat(NumberTheory/NumberField): proof of the Analytic Class Number Formula

[xroblot]

---

• [ ] depends on: #16675
• [x] depends on: #16822
• [ ] depends on: #12488
• [ ] depends on: #12405
• [x] depends on: #17943
• [ ] depends on: #17944
• [x] depends on: #18130
• [x] depends on: #18166
• [ ] depends on: #18231
• [x] depends on: #18246
• [ ] depends on: #18245
• [ ] depends on: #18248

[github-actions[bot]]

PR summary 8de2417b09

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.NumberField.DedekindZeta (new file)	2812

---

Declarations diff

+ classNumber_ne_zero + classNumber_pos + dedekindZeta + dedekindZeta_residue + dedekindZeta_residue_def + dedekindZeta_residue_ne_zero + dedekindZeta_residue_pos + tendsto_sub_one_mul_dedekindZeta_nhdsGT

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[riccardobrasca]

Can you please fix the error?

[xroblot]

Can you please fix the error?

Yes, I haven't updated this PR for quite some time, so it might take a bit to get it ready for review.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#16675~~
• ~~leanprover-community/mathlib4#16822~~
• ~~leanprover-community/mathlib4#12488~~
• ~~leanprover-community/mathlib4#12405~~
• ~~leanprover-community/mathlib4#17943~~
• ~~leanprover-community/mathlib4#17944~~
• ~~leanprover-community/mathlib4#18130~~
• ~~leanprover-community/mathlib4#18166~~
• ~~leanprover-community/mathlib4#18231~~
• ~~leanprover-community/mathlib4#18246~~
• ~~leanprover-community/mathlib4#18245~~
• ~~leanprover-community/mathlib4#18248~~
• ~~leanprover-community/mathlib4#18400~~
• ~~leanprover-community/mathlib4#20660~~
• ~~leanprover-community/mathlib4#22115~~
• ~~leanprover-community/mathlib4#22397~~
• ~~leanprover-community/mathlib4#22779~~
• ~~leanprover-community/mathlib4#22866~~
• ~~leanprover-community/mathlib4#23440~~
• ~~leanprover-community/mathlib4#24713~~ By Dependent Issues (🤖). Happy coding!

[xroblot]

I agree that the names are not really optimal. I was taking riemannZeta_residue_one as model. However, the names you suggested sound good too

[riccardobrasca]

I agree that the names are not really optimal. I was taking riemannZeta_residue_one as model. However, the names you suggested sound good too

I see. Let's keep dedekindZeta_residue for the second one. What about making the first one a local notation? If I want to use the class number formula I probably want to see the explicit number (with the class number, the regulator and so on) rather than a constant residue.

[xroblot]

If I make it a local notation that probably means that the results residue_pos and residue_ne_zero should be removed, right?

[riccardobrasca]

If I make it a local notation that probably means that the results residue_pos and residue_ne_zero should be removed, right?

Hmm, we can keep them with some stupid names...

[loefflerd]

If I make it a local notation that probably means that the results residue_pos and residue_ne_zero should be removed, right?

Hmm, we can keep them with some stupid names...

Hi folks,

It looks like almost everything is settled here except the naming issue.

Among the various namings that have been proposed, the one I personally prefer is closer to the first suggestion from Riccardo: that the actual value (currently residue) should become dedekindZeta_residue; and the lemma stating that this is indeed the residue should be tendsto_dedekindZeta_mul_sub_one_nhdsGT, because nhdsGT is the standard name for the 𝓝[>] filter. That way it's clear what names we should give to different versions of the residue computation (with limits along punctured neighbourhoods in C) once we have meromorphic continuation of the zeta function; and these will of course involve the same value dedekindZeta_residue, just different notions of limit.

This is indeed incompatible with riemannZeta_residue_one, but that name is not set in stone; perhaps it should be renamed to tendsto_riemannZeta_mul_sub_one_nhdsNE [edit: fixed typo] (with a deprecation alias for the old name), but that is a matter for another PR.

Best regards, David

[xroblot]

Hi David, thanks for the feedback. I think I prefer the solution where the value of the residue becomes dedekindZeta_residue and the result is named tendsto_dedekindZeta_mul_sub_one_nhdsGT as you suggested and, in a future PR, the name of the residue computation for the Riemann Zeta function is changed to match. Indeed, since the expression for the residue is quite complicated, I think it would be easier to have a name for it.

We could also make dedekindZeta_residue an abbrev so that it is easier to access to the actual value or/and add a dedekindZeta_residue_def result to replace it with the actual value.

[riccardobrasca]

Hi David, thanks for the feedback. I think I prefer the solution where the value of the residue becomes dedekindZeta_residue and the result is named tendsto_dedekindZeta_mul_sub_one_nhdsGT as you suggested and, in a future PR, the name of the residue computation for the Riemann Zeta function is changed to match. Indeed, since the expression for the residue is quite complicated, I think it would be easier to have a name for it.

We could also make dedekindZeta_residue an abbrev so that it is easier to access to the actual value or/and add a dedekindZeta_residue_def result to replace it with the actual value.

OK, let's do that! Thanks a lot!!

bors d+

[mathlib-bors[bot]]

:v: xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[xroblot]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style