Commit 2025-04-24 13:51 3a0bc63f

View on Github →

feat(NumberField/CanonicalEmbedding/NormLeOne): prove that the frontier of normLeOne has zero-volume (#22779) This is the last PR about normLeOne K. We prove that it is a bounded set and that its frontier has volume zero. This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

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

added theorem NumberField.mixedEmbedding.continuous_normAtAllPlaces

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

added theorem NumberField.mixedEmbedding.fundamentalCone.closure_normLeOne_subset

added theorem NumberField.mixedEmbedding.fundamentalCone.closure_paramSet

added theorem NumberField.mixedEmbedding.fundamentalCone.closure_paramSet_ae_interior

added theorem NumberField.mixedEmbedding.fundamentalCone.compactSet_ae

added theorem NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union

added theorem NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union_aux₁

added theorem NumberField.mixedEmbedding.fundamentalCone.compactSet_eq_union_aux₂

added theorem NumberField.mixedEmbedding.fundamentalCone.expMapBasis_closure_subset_compactSet

added theorem NumberField.mixedEmbedding.fundamentalCone.interior_paramSet

added theorem NumberField.mixedEmbedding.fundamentalCone.isBounded_normLeOne

added theorem NumberField.mixedEmbedding.fundamentalCone.isCompact_compactSet

added theorem NumberField.mixedEmbedding.fundamentalCone.measurableSet_interior_paramSet

added theorem NumberField.mixedEmbedding.fundamentalCone.nonneg_of_mem_compactSet

added theorem NumberField.mixedEmbedding.fundamentalCone.subset_interior_normLeOne

added theorem NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne

added theorem NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure

added theorem NumberField.mixedEmbedding.fundamentalCone.zero_mem_compactSet