Commit 2025-04-16 09:34 9c97e7a8

View on Github →

feat(NumberField/CanonicalEmbedding/NormLeOne): compute the volume of NormLeOne (#22777) We compute the volume of normLeOne K. This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

added theorem integrableOn_exp_mul_Iic

added theorem integrableOn_exp_mul_Ioi

added theorem integral_exp_mul_Iic

added theorem integral_exp_mul_Ioi

Modified Mathlib/Data/ENNReal/Real.lean

added theorem ENNReal.ofReal_ne_zero_iff

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

added theorem MeasureTheory.Measure.restrict_pi_pi

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

added theorem NumberField.mixedEmbedding.continuous_normAtPlace

added theorem NumberField.mixedEmbedding.normAtAllPlaces_image_preimage_of_nonneg

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

added theorem NumberField.mixedEmbedding.measurableSet_fundamentalCone

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

added theorem NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply''

added theorem NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis

added theorem NumberField.mixedEmbedding.fundamentalCone.measurableSet_normLeOne

added theorem NumberField.mixedEmbedding.fundamentalCone.measurableSet_paramSet

added theorem NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_image_preimage_expMapBasis

added theorem NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne_eq_image

added theorem NumberField.mixedEmbedding.fundamentalCone.normLeOne_eq_preimage

added theorem NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis

added theorem NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis_ne_zero

added theorem NumberField.mixedEmbedding.fundamentalCone.setLIntegral_paramSet_exp

added theorem NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne