feat(NumberTheory/NumberField): summability of the prime ideal zeta sum

[xroblot]

No description provided.

[github-actions]

PR summary 285760098a

Import changes exceeding 2%

%	File
+32.95%	Mathlib.NumberTheory.NumberField.DirichletDensity

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.NumberField.DirichletDensity	2540	3377	+837 (+32.95%)
Mathlib.NumberTheory.Padics.HeightOneSpectrum	2483	2500	+17 (+0.68%)
Mathlib.NumberTheory.NumberField.Completion.FinitePlace	3183	3185	+2 (+0.06%)

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.EllipticCurve.LFunction Mathlib.NumberTheory.Height.NumberField	1
3 files Mathlib.NumberTheory.NumberField.Completion.FinitePlace Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.ProductFormula	2
Mathlib.NumberTheory.Padics.HeightOneSpectrum	17
Mathlib.NumberTheory.NumberField.DirichletDensity	837

---

Declarations diff (regex)

+ Int.absNorm_under_span_natCast
+ Int.under_span_natCast
+ _root_.Ideal.one_lt_absNorm
+ _root_.IsDedekindDomain.HeightOneSpectrum.absNorm_ne_zero
+ absNorm_ne_zero_nnreal
+ absNorm_under_dvd_absNorm
+ algebraMap_dvd_algebraMap_iff
+ dirichletDensity_univ
+ hasDirichletDensity_univ
+ infinite_of_isIntegral
+ instance : Infinite (HeightOneSpectrum ℤ) := primesEquivInt.infinite_iff.mpr inferInstance
+ instance : NeZero v.asIdeal := ⟨v.ne_bot⟩
+ instance [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B]
+ instance [NumberField K] : Infinite (HeightOneSpectrum (𝓞 K))
+ ncard_primesOver_le
+ primeIdealZetaSum_pos
+ primesEquivInt
+ primesEquiv_apply_coe
+ primesEquiv_symm_apply_asIdeal
+ primesOverEquiv
+ sum_fiber_le
+ summable_primeIdealZetaSum
+ under_eq_iff

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 2857600).

• +27 new declarations
• −3 removed declarations

+Ideal.absNorm_under_dvd_absNorm
+Ideal.ncard_primesOver_le
+Ideal.one_lt_absNorm
+Int.absNorm_under_span_natCast
+Int.under_span_natCast
+IsDedekindDomain.HeightOneSpectrum.absNorm_ne_zero
+IsDedekindDomain.HeightOneSpectrum.infinite_of_isIntegral
+IsDedekindDomain.HeightOneSpectrum.instFiniteSubtypeEqUnderOfIsTorsionFree
+IsDedekindDomain.HeightOneSpectrum.instInfiniteInt
+IsDedekindDomain.HeightOneSpectrum.instNeZeroIdealAsIdeal
+IsDedekindDomain.HeightOneSpectrum.primesEquiv
+IsDedekindDomain.HeightOneSpectrum.primesEquiv.congr_simp
+IsDedekindDomain.HeightOneSpectrum.primesEquivInt
+IsDedekindDomain.HeightOneSpectrum.primesEquivInt_apply_coe
+IsDedekindDomain.HeightOneSpectrum.primesEquivInt_symm_apply
+IsDedekindDomain.HeightOneSpectrum.primesEquiv_apply_coe
+IsDedekindDomain.HeightOneSpectrum.primesEquiv_symm_apply_asIdeal
+IsDedekindDomain.HeightOneSpectrum.primesOverEquiv
+IsDedekindDomain.HeightOneSpectrum.under.congr_simp
+IsDedekindDomain.HeightOneSpectrum.under_eq_iff
+IsIntegrallyClosed.algebraMap_dvd_algebraMap_iff
+NumberField.HeightOneSpectrum.absNorm_ne_zero_nnreal
+NumberField.Set.dirichletDensity_univ
+NumberField.Set.hasDirichletDensity_univ
+NumberField.Set.primeIdealZetaSum_pos
+NumberField.Set.summable_primeIdealZetaSum
-Rat.HeightOneSpectrum.natGenerator.congr_simp
-Rat.HeightOneSpectrum.primesEquiv
-Rat.IsIntegralClosure.intEquiv.congr_simp
+instInfiniteHeightOneSpectrumRingOfIntegersOfNumberField

---

Decrease in strong tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (strong)
3986	-1	backward.isDefEq.respectTransparency.types

No changes to weak technical debt.

Current commit 285760098a
Reference commit 87adeaebd3

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).