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

[xroblot]

---

• depends on: [Merged by Bors] - feat(Analysis/BoxIntegral): Add BoxPartition defined by subdivision of the integer lattice #16675
• depends on: [Merged by Bors] - feat(Module/ZLattice): define the pullback of a ZLattice #16822
• depends on: feat (Lattice/Covolume): Add results linking point counting in lattices and covolume #12488
• depends on: feat(Analysis/BoxIntegral/UnitPartition): Prove results linking integral point counting and integrals #12405
• depends on: [Merged by Bors] - feat(Analysis/Complex): Prove that Complex.ofReal is a uniform embedding #17943
• depends on: [Merged by Bors] - feat(MeasureTheory): prove that some equivalences are measure preserving #17944
• depends on: [Merged by Bors] - feat(NumberField/CanonicalEmbedding): prove that idealLattice is a ZLattice #18130
• depends on: [Merged by Bors] - feat(LSeries/RiemannZeta): versions of the residue computation of the zeta function with tsum and for a real variable #18166
• depends on: [Merged by Bors] - feat(NumberField/CanonicalEmbedding): define the plusPart of a set #18231
• depends on: [Merged by Bors] - feat(NumberField/Discriminant): Compute some lattices covolume #18246
• depends on: [Merged by Bors] - feat(NumberField/CanonicalEmbedding): put an euclidean space structure on the mixed space #18245
• depends on: [Merged by Bors] - feat(NumberField/FundamentalCone): generalize the bijection to integral ideals #18248
• depends on: feat(Integral/Pi): a version of polarCoord for pi integrals #18400

[github-actions]

PR summary 877b6f4ca1

Import changes exceeding 2%

%	File
+6.70%	Mathlib.MeasureTheory.Integral.Pi

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Integral.Pi	1881	2007	+126 (+6.70%)
Mathlib.Algebra.Module.ZLattice.Covolume	1890	1912	+22 (+1.16%)

Import changes for all files

Files	Import difference
5 files Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.NumberField.ClassNumber	1
Mathlib.Algebra.Module.ZLattice.Covolume	22
Mathlib.MeasureTheory.Integral.Pi	126
Mathlib.Analysis.BoxIntegral.UnitPartition	1906
Mathlib.NumberTheory.LSeries.Residue	2152
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLessThanOne	2392
Mathlib.NumberTheory.NumberField.Ideal	2413
Mathlib.NumberTheory.NumberField.DedekindZeta	2484

---

Declarations diff

+ A
+ A_u_lt
+ Basis.det_basis
+ Basis.det_inv
+ Basis.ofZLatticeBasis_comap
+ BoxIntegral.hasIntegralCorners
+ BoxIntegral.le_hasIntegralVertices_of_isBounded
+ Complex.lintegral_pi_comp_polarCoord_symm
+ ContinuousOn.continuousAt_mulIndicator
+ FDerivAt_polarCoord_symm_det
+ Finset.frontier_biUnion
+ LSeries_eq_of_summable
+ Pi.basisFun_det_apply
+ _root_.Measurable.lmarginal_update
+ _root_.NumberTheory.LSeries.tendsto_mul_of_sum_div_tendsto
+ admissibleIndex
+ box_index_tag_eq_self
+ box_injective
+ box_lower
+ box_upper
+ box₁
+ box₂
+ card_u_eq
+ classNumber_ne_zero
+ classNumber_pos
+ closure_box₁
+ closure_box₂
+ closure_subset_mapToUnitsPowComplex_closure
+ continuousOn_logMap
+ continuous_mapToUnitsPow
+ continuous_mapToUnitsPowComplex
+ continuous_mapToUnitsPow₀
+ continuous_mapToUnitsPow₀_aux
+ continuous_norm
+ continuous_normAtPlace
+ continuous_polarCoordMixedSpace_symm
+ covolume_eq_det_inv
+ dedekindZeta
+ dedekindZeta_residue
+ diam_boxIcc
+ disjoint
+ eqOn_mulIndicator'
+ eq_of_index_eq_index_and_mem_smul_span
+ equivFinRank
+ exist_finset_lt_tsum_u_lt
+ exists_admissibleIndex
+ exists_mem_smul_normEqOne
+ finrank_mul_regulator_eq_det
+ frontier_iUnion
+ frontier_union_subset'
+ hasFDeriv_mapToUnitsPow
+ hasFDeriv_mapToUnitsPow_single
+ ideal.tendsto_mk_eq_norm_le_div_atop
+ ideal.tendsto_norm_le_div_atop
+ ideal.tendsto_norm_le_div_atop₀
+ index
+ index_apply
+ index_tag
+ instDiscreteTopology
+ integralSum_eq_tsum_div
+ interior_box₁
+ interior_box₂
+ interior_subset_mapToUnitsPowComplex_source
+ isBounded
+ isBounded_Icc
+ isBounded_box₁
+ isBounded_box₂
+ isBounded_normEqOne
+ isBounded_normLessThanOne
+ isClosed_mapToUnitsPowComplex_closure
+ isEquivalent_comm
+ isOpen_mapToUnitsPowComplex_interior
+ le_A_u
+ lintegral_eq_lintegral_polarCoordMixedSpace_symm
+ lmarginal_const_smul
+ lmarginal_const_smul'
+ logMap_mixedToRealToMixed_of_norm_one
+ logMap_realToMixed
+ lt_u_rpow_lt
+ mapToUnitsPow
+ mapToUnitsPowComplex
+ mapToUnitsPowComplex_apply
+ mapToUnitsPowComplex_image_prod
+ mapToUnitsPowComplex_interior_subset_interior
+ mapToUnitsPowComplex_prod_indicator
+ mapToUnitsPowComplex_prod_indicator_aux
+ mapToUnitsPowComplex_source
+ mapToUnitsPowComplex_target
+ mapToUnitsPow_apply
+ mapToUnitsPow_apply'
+ mapToUnitsPow_fDeriv_single
+ mapToUnitsPow_image_minus_image_inter
+ mapToUnitsPow_image_minus_image_inter_aux
+ mapToUnitsPow_jacobian
+ mapToUnitsPow_jacobianCoeff
+ mapToUnitsPow_jacobian_det
+ mapToUnitsPow_nonneg
+ mapToUnitsPow_pos
+ mapToUnitsPow_single
+ mapToUnitsPow_zero_iff
+ mapToUnitsPow_zero_iff'
+ mapToUnitsPow₀
+ mapToUnitsPow₀_apply
+ mapToUnitsPow₀_aux
+ mapToUnitsPow₀_aux_symm_apply
+ mapToUnitsPow₀_eq_prod_single
+ mapToUnitsPow₀_pos
+ mapToUnitsPow₀_source
+ mapToUnitsPow₀_symm_apply_of_norm_one
+ mapToUnitsPow₀_symm_prod_fundSystem_rpow
+ mapToUnitsPow₀_target
+ measurableSet_box₁
+ measurableSet_box₂
+ measurableSet_frontier
+ measurableSet_fundamentalCone
+ measurableSet_normLessThanOne
+ measurableSet_polarCoordMixedSpace_target
+ measurable_logMap
+ measurable_mapToUnitsPow_image
+ measurable_mapToUnitsPow_symm
+ mem_Ico_of_mem_box₁
+ mem_Ioc_of_mem_box₁
+ mem_admissibleIndex_iff
+ mem_admissibleIndex_of_mem_box
+ mem_admissibleIndex_of_mem_box_aux₁
+ mem_admissibleIndex_of_mem_box_aux₂
+ mem_box_iff
+ mem_box_iff'
+ mem_box_iff_index
+ mem_normLessThanOne_iff
+ mem_normLessThanOne_of_normAtPlace_eq
+ mem_prepartition_boxes_iff
+ mem_prepartition_iff
+ mixedToReal
+ mixedToRealToMixed
+ mixedToReal_apply_of_isComplex
+ mixedToReal_apply_of_isReal
+ mixedToReal_mapToUnitsPowComplex
+ mixedToReal_mem_target
+ mixedToReal_nonneg
+ mixedToReal_plusPart_normEqOne
+ mixedToReal_plusPart_normLessThanOne
+ mixedToReal_smul
+ monotone_A
+ monotone_u
+ mult_coe_ne_zero
+ nonZeroDivisors_dvd_iff_dvd_coe
+ normAtPlace_realToMixed
+ normEqOne
+ normLessThanOne
+ normLessThanOne_eq_union_smul_normEqOne
+ norm_mapToUnitsPow₀
+ norm_mixedToReal
+ norm_mixedToRealToMixed
+ norm_realToMixed
+ norm_realToMixed_prod_units_rpow
+ ofReal_ne_zero_iff
+ plusPart_normLessThanOne
+ polarCoordMixedSpace
+ polarCoordMixedSpace_apply
+ polarCoordMixedSpace_source
+ polarCoordMixedSpace_symm_apply
+ polarCoordMixedSpace_target
+ polarCoord_symm_mem_polarCoord_source_iff
+ pos_at_place
+ pos_norm_realToMixed
+ pos_of_mem_box₁
+ prepartition
+ prepartition_isHenstock
+ prepartition_isPartition
+ prepartition_isSubordinate
+ prepartition_tag
+ prod_mapToUnitsPow_single
+ prod_mapToUnitsPow₀(c
+ realProdComplexProdEquiv
+ realProdComplexProdEquiv_apply
+ realProdComplexProdEquiv_preimage_target
+ realProdComplexProdEquiv_symm_apply
+ realProdComplexProdMeasurableEquiv
+ realSpace
+ realToMixed
+ realToMixedToReal
+ realToMixedToReal_eq_self_of_nonneg
+ realToMixed_apply_of_isComplex
+ realToMixed_apply_of_isReal
+ repr_isUnitSMul
+ residue
+ residue_ne_zero
+ residue_pos
+ restrict_pi_pi
+ restrict_prod_eq_univ_prod
+ rpow_ne_zero_of_pos
+ setFinite_index
+ setFinite_inter
+ setLIntegral_mapToUnitsPow
+ smul
+ smul_normEqOne
+ smul_normEqOne_subset
+ summable_u_rpow
+ tag
+ tag_apply
+ tag_index_eq_self_of_mem_smul_span
+ tag_injective
+ tag_mem
+ tag_mem_smul_span
+ tends_atTop_A
+ tendsto_atTop_u
+ tendsto_atTop_u_div
+ tendsto_card_div_pow''
+ tendsto_card_le_div
+ tendsto_card_le_div'
+ tendsto_card_le_div''
+ tendsto_mul_sum_rpow
+ tendsto_mul_u_rpow
+ tendsto_rpow_mul_tsum_rpow
+ tendsto_tsum_div_pow
+ term_eq_coe
+ tprod_card_pow_eq_tprod
+ u
+ volume_box
+ volume_frontier_normLessThanOne
+ volume_frontier_plusPart_normLessThanOne
+ volume_image_eq_volume_div_covolume
+ volume_image_eq_volume_div_covolume'
+ volume_mapToUnitsPowComplex_interior_eq_volume_mapToUnitsPowComplex_closure
+ volume_mapToUnitsPowComplex_set_prod_set
+ volume_normLessThanOne
+ volume_normLessThanOnePlus_aux
+ volume_plusPart_normLessThanOne
+ volume_preserving_realProdComplexProdEquiv
++ box
++ continuous_polarCoord_symm
++ lintegral_comp_polarCoord_symm
++ measurable_polarCoord
++ tendsto_card_div_pow
++ tendsto_card_div_pow'
- instance [Finite ι] : DiscreteTopology (span ℤ (Set.range b)).toAddSubgroup

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Analysis/BoxIntegral): Add BoxPartition defined by subdivision of the integer lattice #16675
• [Merged by Bors] - feat(Module/ZLattice): define the pullback of a ZLattice #16822
• feat (Lattice/Covolume): Add results linking point counting in lattices and covolume #12488
• feat(Analysis/BoxIntegral/UnitPartition): Prove results linking integral point counting and integrals #12405
• [Merged by Bors] - feat(Analysis/Complex): Prove that Complex.ofReal is a uniform embedding #17943
• [Merged by Bors] - feat(MeasureTheory): prove that some equivalences are measure preserving #17944
• [Merged by Bors] - feat(NumberField/CanonicalEmbedding): prove that idealLattice is a ZLattice #18130
• [Merged by Bors] - feat(LSeries/RiemannZeta): versions of the residue computation of the zeta function with tsum and for a real variable #18166
• [Merged by Bors] - feat(NumberField/CanonicalEmbedding): define the plusPart of a set #18231
• [Merged by Bors] - feat(NumberField/Discriminant): Compute some lattices covolume #18246
• [Merged by Bors] - feat(NumberField/CanonicalEmbedding): put an euclidean space structure on the mixed space #18245
• [Merged by Bors] - feat(NumberField/FundamentalCone): generalize the bijection to integral ideals #18248
• feat(Integral/Pi): a version of polarCoord for pi integrals #18400
  By Dependent Issues (🤖). Happy coding!