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

[xroblot]

---

• depends on: 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: 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: 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: feat(NumberField/CanonicalEmbedding): put an euclidean space structure on the mixed space #18245
• depends on: feat(NumberField/FundamentalCone): generalize the bijection to integral ideals #18248

[github-actions]

PR summary d6b3f8d0b3

Import changes exceeding 2%

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

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.Integral.Pi	1838	1956	+118 (+6.42%)
Mathlib.Algebra.Module.ZLattice.Covolume	1847	1869	+22 (+1.19%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic	2242	2251	+9 (+0.40%)

Import changes for all files

Files	Import difference
3 files Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.Units.DirichletTheorem	2
6 files Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.NumberField.ClassNumber	3
3 files Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic	9
Mathlib.Algebra.Module.ZLattice.Covolume	22
Mathlib.MeasureTheory.Integral.Pi	118
Mathlib.Analysis.BoxIntegral.UnitPartition	1863
Mathlib.NumberTheory.LSeries.Residue	2090
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLessThanOne	2327
Mathlib.NumberTheory.NumberField.Ideal	2348
Mathlib.NumberTheory.NumberField.DedekindZeta	2413

---

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_.MeasureTheory.measurePreserving_prodAssoc
+ _root_.MeasureTheory.volume_preserving_prodAssoc
+ _root_.NumberTheory.LSeries.tendsto_mul_of_sum_div_tendsto
+ admissibleIndex
+ arrowCongr'
+ arrowProdEquivProdArrow
+ box_index_tag_eq_self
+ box_injective
+ box_lower
+ box_upper
+ box₁
+ box₂
+ card_isPrincipal_dvd_norm_le
+ card_u_eq
+ classNumber_ne_zero
+ classNumber_pos
+ closure_box₁
+ closure_box₂
+ closure_subset_mapToUnitsPowComplex_closure
+ coe_neg
+ 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
+ disjoint_negAtPlusPart
+ 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
+ finrank_mul_regulator_eq_det
+ frontier_iUnion
+ frontier_union_subset'
+ hasFDeriv_mapToUnitsPow
+ hasFDeriv_mapToUnitsPow_single
+ iUnion_negAtPart_ae
+ iUnion_negAtPlusPart_union
+ ideal.tendsto_mk_eq_norm_le_div_atop
+ ideal.tendsto_norm_le_div_atop
+ ideal.tendsto_norm_le_div_atop₀
+ idealPoint
+ idealPointEquiv
+ idealPointEquivNorm
+ idealPointEquiv_apply
+ idealPointEquiv_symm_apply
+ idealPointMap
+ idealPointMap_apply
+ index
+ index_apply
+ index_tag
+ instDiscreteTopology
+ instance : BorelSpace (euclidean.mixedSpace K) := ⟨rfl⟩
+ instance : DiscreteTopology (euclidean.integerLattice K) := by
+ instance : IsAddHaarMeasure (volume : Measure (mixedSpace K))
+ instance : IsZLattice ℝ (euclidean.integerLattice K) := by
+ instance : MeasurableSpace (euclidean.mixedSpace K) := borel _
+ instance : Nontrivial (euclidean.mixedSpace K) := (toMixed K).toEquiv.nontrivial
+ instance : Ring (euclidean.mixedSpace K) := by
+ instance : T2Space (euclidean.mixedSpace K) := Prod.t2Space
+ intNorm_idealPointEquiv_apply
+ integerLattice
+ 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_negAtPlusPart
+ measurableSet_normLessThanOne
+ measurableSet_plusPart
+ measurableSet_polarCoordMixedSpace_target
+ measurable_logMap
+ measurable_mapToUnitsPow_image
+ measurable_mapToUnitsPow_symm
+ measurePreserving_arrowCongr'
+ measurePreserving_arrowProdEquivProdArrow
+ 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_idealPoint
+ mem_negAtPlusPart_of_mem
+ mem_normLessThanOne_iff
+ mem_normLessThanOne_of_normAtPlace_eq
+ mem_prepartition_boxes_iff
+ mem_prepartition_iff
+ mixedSpace
+ 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
+ neg
+ negAt
+ negAtPlusPart
+ negAtPlusPart_neg_of_mem
+ negAtPlusPart_pos_of_not_mem
+ negAt_apply_abs_of_isReal
+ negAt_apply_of_isReal_and_mem
+ negAt_apply_of_isReal_and_not_mem
+ negAt_apply_snd
+ negAt_preimage
+ negAt_signSet_apply_of_isComplex
+ negAt_signSet_apply_of_isReal
+ negAt_symm
+ neg_apply
+ nonZeroDivisors_dvd_iff_dvd_coe
+ normAtPlace_negAt
+ normAtPlace_realToMixed
+ normEqOne
+ normLessThanOne
+ normLessThanOne_eq_union_smul_normEqOne
+ norm_mapToUnitsPow₀
+ norm_mixedToReal
+ norm_mixedToRealToMixed
+ norm_negAt
+ norm_realToMixed
+ norm_realToMixed_prod_units_rpow
+ ofReal_ne_zero_iff
+ piCongrRight
+ piCongrRight_apply
+ piCongrRight_symm_apply
+ plusPart
+ 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₁
+ preimage_of_IdealPointMap
+ 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
+ refl_apply
+ 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
+ signSet
+ smul
+ smul_normEqOne
+ smul_normEqOne_subset
+ stdOrthonormalBasis
+ stdOrthonormalBasis_map_eq
+ summable_u_rpow
+ symm_neg
+ 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
+ toMixed
+ tprod_card_pow_eq_tprod
+ u
+ volumePreserving_toMixed
+ volumePreserving_toMixed_symm
+ volume_box
+ volume_eq_two_pow_mul_volume_plusPart
+ volume_eq_zero
+ 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_measurePreserving_arrowProdEquivProdArrow
+ volume_negAtPlusPart
+ volume_normLessThanOne
+ volume_normLessThanOnePlus_aux
+ volume_plusPart_normLessThanOne
+ volume_preserving_arrowCongr'
+ volume_preserving_negAt
+ volume_preserving_realProdComplexProdEquiv
++ box
++ continuous_polarCoord_symm
++ lintegral_comp_polarCoord_symm
++ measurable_polarCoord
++ tendsto_card_div_pow
++ tendsto_card_div_pow'
- card_isPrincipal_norm_le_mul_torsion
- instance : IsAddHaarMeasure (volume : Measure (mixedSpace K)) := prod.instIsAddHaarMeasure _ _
- 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:

• 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
• 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
• feat(NumberField/CanonicalEmbedding): define the plusPart of a set #18231
• [Merged by Bors] - feat(NumberField/Discriminant): Compute some lattices covolume #18246
• feat(NumberField/CanonicalEmbedding): put an euclidean space structure on the mixed space #18245
• feat(NumberField/FundamentalCone): generalize the bijection to integral ideals #18248
  By Dependent Issues (🤖). Happy coding!