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.

Author: xroblot

Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

@@ -71,6 +71,16 @@ theorem integrableOn_exp_mul_complex_Iic {a : ℂ} (ha : 0 < a.re) (c : ℝ) :
   simpa using integrableOn_Iic_iff_integrableOn_Iio.mpr
     (integrableOn_exp_mul_complex_Ioi (a := -a) (by simpa) (-c)).comp_neg_Iio
 
+theorem integrableOn_exp_mul_Ioi {a : ℝ} (ha : a < 0) (c : ℝ) :
+    IntegrableOn (fun x : ℝ => Real.exp (a * x)) (Ioi c) := by
+  have := Integrable.norm <| integrableOn_exp_mul_complex_Ioi (a := a) (by simpa using ha) c
+  simpa [Complex.norm_exp] using this
+
+theorem integrableOn_exp_mul_Iic {a : ℝ} (ha : 0 < a) (c : ℝ) :
+    IntegrableOn (fun x : ℝ => Real.exp (a * x)) (Iic c) := by
+  have := Integrable.norm <| integrableOn_exp_mul_complex_Iic (a := a) (by simpa using ha) c
+  simpa [Complex.norm_exp] using this
+
 theorem integral_exp_mul_complex_Ioi {a : ℂ} (ha : a.re < 0) (c : ℝ) :
     ∫ x : ℝ in Set.Ioi c, Complex.exp (a * x) = - Complex.exp (a * c) / a := by
   refine tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi c
@@ -86,6 +96,18 @@ theorem integral_exp_mul_complex_Iic {a : ℂ} (ha : 0 < a.re) (c : ℝ) :
     integral_comp_neg_Ioi (f := fun x : ℝ ↦ Complex.exp (a * x))]
     using integral_exp_mul_complex_Ioi (a := -a) (by simpa) (-c)
 
+theorem integral_exp_mul_Ioi {a : ℝ} (ha : a < 0) (c : ℝ) :
+    ∫ x : ℝ in Set.Ioi c, Real.exp (a * x) = - Real.exp (a * c) / a := by
+  simp_rw [Real.exp, ← RCLike.re_to_complex, Complex.ofReal_mul]
+  rw [integral_re, integral_exp_mul_complex_Ioi (by simpa using ha), RCLike.re_to_complex,
+    RCLike.re_to_complex, Complex.div_ofReal_re, Complex.neg_re]
+  exact integrableOn_exp_mul_complex_Ioi  (by simpa using ha) _
+
+theorem integral_exp_mul_Iic {a : ℝ} (ha : 0 < a) (c : ℝ) :
+    ∫ x : ℝ in Set.Iic c, Real.exp (a * x) = Real.exp (a * c) / a := by
+  simpa [neg_mul, ← mul_neg, integral_comp_neg_Ioi (f := fun x : ℝ ↦ Real.exp (a * x))]
+    using integral_exp_mul_Ioi (a := -a) (by simpa) (-c)
+
 /-- If `0 < c`, then `(fun t : ℝ ↦ t ^ a)` is integrable on `(c, ∞)` for all `a < -1`. -/
 theorem integrableOn_Ioi_rpow_of_lt {a : ℝ} (ha : a < -1) {c : ℝ} (hc : 0 < c) :
     IntegrableOn (fun t : ℝ => t ^ a) (Ioi c) := by

Mathlib/Data/ENNReal/Real.lean

@@ -170,6 +170,9 @@ theorem ofReal_pos {p : ℝ} : 0 < ENNReal.ofReal p ↔ 0 < p := by simp [ENNRea
 @[simp]
 theorem ofReal_eq_zero {p : ℝ} : ENNReal.ofReal p = 0 ↔ p ≤ 0 := by simp [ENNReal.ofReal]
 
+theorem ofReal_ne_zero_iff {r : ℝ} : ENNReal.ofReal r ≠ 0 ↔ 0 < r := by
+  rw [← zero_lt_iff, ENNReal.ofReal_pos]
+
 @[simp]
 theorem zero_eq_ofReal {p : ℝ} : 0 = ENNReal.ofReal p ↔ p ≤ 0 :=
   eq_comm.trans ofReal_eq_zero

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -360,6 +360,12 @@ theorem pi_hyperplane (i : ι) [NoAtoms (μ i)] (x : α i) :
 theorem ae_eval_ne (i : ι) [NoAtoms (μ i)] (x : α i) : ∀ᵐ y : ∀ i, α i ∂Measure.pi μ, y i ≠ x :=
   compl_mem_ae_iff.2 (pi_hyperplane μ i x)
 
+theorem restrict_pi_pi (s : (i : ι) → Set (α i)) :
+    (Measure.pi μ).restrict (Set.univ.pi fun i ↦ s i) = .pi (fun i ↦ (μ i).restrict (s i)) := by
+  refine (pi_eq fun _ h ↦ ?_).symm
+  simp_rw [restrict_apply (MeasurableSet.univ_pi h), restrict_apply (h _),
+    ← Set.pi_inter_distrib, pi_pi]
+
 variable {μ}
 
 theorem tendsto_eval_ae_ae {i : ι} : Tendsto (eval i) (ae (Measure.pi μ)) (ae (μ i)) := fun _ hs =>

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

@@ -379,6 +379,11 @@ theorem exists_normAtPlace_ne_zero_iff {x : mixedSpace K} :
     (∃ w, normAtPlace w x ≠ 0) ↔ x ≠ 0 := by
   rw [ne_eq, ← forall_normAtPlace_eq_zero_iff, not_forall]
 
+theorem continuous_normAtPlace (w : InfinitePlace K) :
+    Continuous (normAtPlace w) := by
+  simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
+  split_ifs <;> fun_prop
+
 variable [NumberField K]
 
 open scoped Classical in
@@ -459,6 +464,12 @@ theorem norm_eq_zero_iff' {x : mixedSpace K} (hx : x ∈ Set.range (mixedEmbeddi
   rw [norm_eq_norm, Rat.cast_abs, abs_eq_zero, Rat.cast_eq_zero, Algebra.norm_eq_zero_iff,
     map_eq_zero]
 
+variable (K) in
+protected theorem continuous_norm : Continuous (mixedEmbedding.norm : (mixedSpace K) → ℝ) := by
+  refine continuous_finset_prod Finset.univ fun _ _ ↦ ?_
+  simp_rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, dite_pow]
+  split_ifs <;> fun_prop
+
 end norm
 
 noncomputable section stdBasis
@@ -1228,6 +1239,14 @@ theorem normAtAllPlaces_eq_of_normAtComplexPlaces_eq {x y : mixedSpace K}
   · simpa [normAtAllPlaces_apply, normAtPlace_apply_of_isComplex hw,
       normAtComplexPlaces_apply_isComplex ⟨w, hw⟩] using congr_fun h w
 
+theorem normAtAllPlaces_image_preimage_of_nonneg {s : Set (realSpace K)}
+    (hs : ∀ x ∈ s, ∀ w, 0 ≤ x w) :
+    normAtAllPlaces '' (normAtAllPlaces ⁻¹' s) = s := by
+  rw [Set.image_preimage_eq_iff]
+  rintro x hx
+  refine ⟨mixedSpaceOfRealSpace x, funext fun w ↦ ?_⟩
+  rw [normAtAllPlaces_apply, normAtPlace_mixedSpaceOfRealSpace (hs x hx w)]
+
 end realSpace
 
 end NumberField.mixedEmbedding

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

@@ -177,6 +177,17 @@ def fundamentalCone : Set (mixedSpace K) :=
   logMap⁻¹' (ZSpan.fundamentalDomain ((basisUnitLattice K).ofZLatticeBasis ℝ _)) \
       {x | mixedEmbedding.norm x = 0}
 
+theorem measurableSet_fundamentalCone :
+    MeasurableSet (fundamentalCone K) := by
+  classical
+  refine MeasurableSet.diff ?_ ?_
+  · unfold logMap
+    refine MeasurableSet.preimage (ZSpan.fundamentalDomain_measurableSet _) <|
+      measurable_pi_iff.mpr fun w ↦ measurable_const.mul ?_
+    exact (continuous_normAtPlace _).measurable.log.sub <|
+      (mixedEmbedding.continuous_norm _).measurable.log.mul measurable_const
+  · exact measurableSet_eq_fun (mixedEmbedding.continuous_norm K).measurable measurable_const
+
 namespace fundamentalCone
 
 variable {K} {x y : mixedSpace K} {c : ℝ}

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
+import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
 import Mathlib.NumberTheory.NumberField.Units.Regulator
 
 /-!
@@ -12,7 +13,7 @@ import Mathlib.NumberTheory.NumberField.Units.Regulator
 In this file, we study the subset `NormLeOne` of the `fundamentalCone` of elements `x` with
 `mixedEmbedding.norm x ≤ 1`.
 
-Mainly, we prove that this is bounded, its frontier has volume zero and compute its volume.
+Mainly, we prove that it is bounded, its frontier has volume zero and compute its volume.
 
 ## Strategy of proof
 
@@ -47,6 +48,12 @@ The proof is loosely based on the strategy given in [D. Marcus, *Number Fields*]
   `expMapBasis_apply'`. Then, we prove a change of variable formula for `expMapBasis`, see
   `setLIntegral_expMapBasis_image`.
 
+6. We define a set `paramSet` in `realSpace K` and prove that
+  `normAtAllPlaces '' (normLeOne K) = expMapBasis (paramSet K)`, see
+  `normAtAllPlaces_normLeOne_eq_image`. Using this, `setLIntegral_expMapBasis_image` and the results
+  from `mixedEmbedding.polarCoord`, we can then compute the volume of `normLeOne K`, see
+  `volume_normLeOne`.
+
 ## Spaces and maps
 
 To help understand the proof, we make a list of (almost) all the spaces and maps used and
@@ -127,6 +134,11 @@ variable {K} in
 theorem mem_normLeOne {x : mixedSpace K} :
     x ∈ normLeOne K ↔ x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1 := Set.mem_sep_iff
 
+theorem measurableSet_normLeOne :
+    MeasurableSet (normLeOne K) :=
+  (measurableSet_fundamentalCone K).inter <|
+    measurableSet_le (mixedEmbedding.continuous_norm K).measurable measurable_const
+
 theorem normLeOne_eq_primeage_image :
     normLeOne K = normAtAllPlaces⁻¹' (normAtAllPlaces '' (normLeOne K)) := by
   refine subset_antisymm (Set.subset_preimage_image _ _) ?_
@@ -407,8 +419,6 @@ end completeBasis
 
 noncomputable section expMapBasis
 
-open ENNReal MeasureTheory
-
 variable [NumberField K]
 
 variable {K}
@@ -456,6 +466,14 @@ theorem expMapBasis_apply' (x : realSpace K) :
     expMap_sum, expMap_smul, expMap_basis_of_ne, Pi.smul_def, smul_eq_mul, prod_apply, Pi.pow_apply,
     normAtAllPlaces_mixedEmbedding]
 
+open scoped Classical in
+theorem expMapBasis_apply'' (x : realSpace K) :
+    expMapBasis x = Real.exp (x w₀) • expMapBasis (fun i ↦ if i = w₀ then 0 else x i) := by
+ rw [expMapBasis_apply', expMapBasis_apply', if_pos rfl, smul_smul, ← Real.exp_add, add_zero]
+ conv_rhs =>
+   enter [2, w, 2, i]
+   rw [if_neg i.prop]
+
 theorem prod_expMapBasis_pow (x : realSpace K) :
     ∏ w, (expMapBasis x w) ^ w.mult = Real.exp (x w₀) ^ Module.finrank ℚ K := by
   simp_rw [expMapBasis_apply', Pi.smul_def, smul_eq_mul, mul_pow, prod_mul_distrib,
@@ -465,6 +483,44 @@ theorem prod_expMapBasis_pow (x : realSpace K) :
     fun _ _ ↦ pow_nonneg (apply_nonneg _ _) _, prod_eq_abs_norm, Units.norm, Rat.cast_one,
     Real.one_rpow, prod_const_one, mul_one]
 
+theorem norm_expMapBasis (x : realSpace K) :
+    mixedEmbedding.norm (mixedSpaceOfRealSpace (expMapBasis x)) =
+      Real.exp (x w₀) ^ Module.finrank ℚ K := by
+  simpa only [mixedEmbedding.norm_apply,
+    normAtPlace_mixedSpaceOfRealSpace (expMapBasis_pos _ _).le] using prod_expMapBasis_pow x
+
+theorem norm_expMapBasis_ne_zero (x : realSpace K) :
+    mixedEmbedding.norm (mixedSpaceOfRealSpace (expMapBasis x)) ≠ 0 :=
+  norm_expMapBasis x ▸ pow_ne_zero _ (Real.exp_ne_zero _)
+
+open scoped Classical in
+theorem logMap_expMapBasis (x : realSpace K) :
+    logMap (mixedSpaceOfRealSpace (expMapBasis x)) ∈
+        ZSpan.fundamentalDomain ((basisUnitLattice K).ofZLatticeBasis ℝ (unitLattice K))
+      ↔ ∀ w, w ≠ w₀ → x w ∈ Set.Ico 0 1 := by
+  classical
+  simp_rw [ZSpan.mem_fundamentalDomain, equivFinRank.forall_congr_left, Subtype.forall]
+  refine forall₂_congr fun w hw ↦ ?_
+  rw [expMapBasis_apply'', map_smul, logMap_real_smul (norm_expMapBasis_ne_zero _)
+    (Real.exp_ne_zero _), expMapBasis_apply, logMap_expMap (by rw [← expMapBasis_apply,
+    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]), Basis.equivFun_symm_apply,
+    Fintype.sum_eq_add_sum_subtype_ne _ w₀, if_pos rfl, zero_smul, zero_add]
+  conv_lhs =>
+    enter [2, 1, 2, w, 2, i]
+    rw [if_neg i.prop]
+  simp_rw [sum_apply, ← sum_fn, map_sum, Pi.smul_apply, ← Pi.smul_def, map_smul,
+    completeBasis_apply_of_ne, expMap_symm_apply, normAtAllPlaces_mixedEmbedding,
+    ← logEmbedding_component, logEmbedding_fundSystem, Finsupp.coe_finset_sum, Finsupp.coe_smul,
+    sum_apply, Pi.smul_apply, Basis.ofZLatticeBasis_repr_apply, Basis.repr_self,
+    Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Int.cast_ite, Int.cast_one, Int.cast_zero,
+    smul_ite, smul_eq_mul, mul_one, mul_zero, Fintype.sum_ite_eq']
+
+theorem normAtAllPlaces_image_preimage_expMapBasis (s : Set (realSpace K)) :
+    normAtAllPlaces '' (normAtAllPlaces ⁻¹' (expMapBasis '' s)) = expMapBasis '' s := by
+  apply normAtAllPlaces_image_preimage_of_nonneg
+  rintro _ ⟨x, _, rfl⟩ w
+  exact (expMapBasis_pos _ _).le
+
 open scoped Classical in
 theorem prod_deriv_expMap_single (x : realSpace K) :
     ∏ w, deriv_expMap_single w ((completeBasis K).equivFun.symm x w) =
@@ -505,7 +561,9 @@ theorem abs_det_fderiv_expMapBasis (x : realSpace K) :
     abs_inv, abs_prod, abs_of_nonneg (expMapBasis_nonneg _ _), Nat.abs_ofNat]
   ring
 
-variable {S}
+variable {K}
+
+open ENNReal MeasureTheory
 
 open scoped Classical in
 theorem setLIntegral_expMapBasis_image {s : Set (realSpace K)} (hs : MeasurableSet s)
@@ -531,4 +589,87 @@ theorem setLIntegral_expMapBasis_image {s : Set (realSpace K)} (hs : MeasurableS
 
 end expMapBasis
 
+section paramSet
+
+variable [NumberField K]
+
+open scoped Classical in
+/--
+The set that parametrizes `normAtAllPlaces '' (normLeOne K)`, see
+`normAtAllPlaces_normLeOne_eq_image`.
+-/
+abbrev paramSet : Set (realSpace K) :=
+  Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Ico 0 1
+
+theorem measurableSet_paramSet :
+    MeasurableSet (paramSet K) := by
+  refine MeasurableSet.univ_pi fun _ ↦ ?_
+  split_ifs
+  · exact measurableSet_Iic
+  · exact measurableSet_Ico
+
+theorem normAtAllPlaces_normLeOne_eq_image :
+    normAtAllPlaces '' (normLeOne K) = expMapBasis '' (paramSet K) := by
+  ext x
+  by_cases hx : ∀ w, 0 < x w
+  · rw [← expMapBasis.right_inv (Set.mem_univ_pi.mpr hx), (injective_expMapBasis K).mem_set_image]
+    simp only [normAtAllPlaces_normLeOne, Set.mem_inter_iff, Set.mem_setOf_eq, expMapBasis_nonneg,
+      Set.mem_preimage, logMap_expMapBasis, implies_true, and_true, norm_expMapBasis,
+      pow_le_one_iff_of_nonneg (Real.exp_nonneg _) Module.finrank_pos.ne', Real.exp_le_one_iff,
+      ne_eq, pow_eq_zero_iff', Real.exp_ne_zero, false_and, not_false_eq_true,  Set.mem_univ_pi]
+    refine ⟨fun ⟨h₁, h₂⟩ w ↦ ?_, fun h ↦ ⟨fun w hw ↦ by simpa [hw] using h w, by simpa using h w₀⟩⟩
+    · split_ifs with hw
+      · exact hw ▸ h₂
+      · exact h₁ w hw
+  · refine ⟨?_, ?_⟩
+    · rintro ⟨a, ⟨ha, _⟩, rfl⟩
+      exact (hx fun w ↦ fundamentalCone.normAtPlace_pos_of_mem ha w).elim
+    · rintro ⟨a, _, rfl⟩
+      exact (hx fun w ↦ expMapBasis_pos a w).elim
+
+theorem normLeOne_eq_preimage :
+    normLeOne K = normAtAllPlaces⁻¹' (expMapBasis '' (paramSet K)) := by
+  rw [normLeOne_eq_primeage_image, normAtAllPlaces_normLeOne_eq_image]
+
+open ENNReal MeasureTheory
+
+theorem setLIntegral_paramSet_exp {n : ℕ} (hn : 0 < n) :
+    ∫⁻ (x : realSpace K) in paramSet K, .ofReal (Real.exp (x w₀ * n)) = (n : ℝ≥0∞)⁻¹ := by
+  classical
+  have hn : 0 < (n : ℝ) := Nat.cast_pos.mpr hn
+  rw [volume_pi, paramSet, Measure.restrict_pi_pi, lintegral_eq_lmarginal_univ 0,
+    lmarginal_erase' _ (by fun_prop) (Finset.mem_univ w₀), if_pos rfl]
+  simp_rw [Function.update_self, lmarginal, lintegral_const, Measure.pi_univ, if_neg
+    (Finset.ne_of_mem_erase (Subtype.prop _)), Measure.restrict_apply_univ, Real.volume_Ico,
+    sub_zero, ofReal_one, prod_const_one, mul_one, mul_comm _ (n : ℝ)]
+  rw [← ofReal_integral_eq_lintegral_ofReal (integrableOn_exp_mul_Iic hn _), integral_exp_mul_Iic
+    hn, mul_zero, Real.exp_zero, ofReal_div_of_pos hn, ofReal_one, ofReal_natCast, one_div]
+  filter_upwards with _ using Real.exp_nonneg _
+
+end paramSet
+
+section main_results
+
+variable [NumberField K]
+
+open ENNReal MeasureTheory
+
+open scoped Classical in
+theorem volume_normLeOne : volume (normLeOne K) =
+    2 ^ nrRealPlaces K * NNReal.pi ^ nrComplexPlaces K * .ofReal (regulator K) := by
+  rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral (normLeOne_eq_primeage_image K).symm
+    (measurableSet_normLeOne K), normLeOne_eq_preimage,
+    normAtAllPlaces_image_preimage_expMapBasis,
+    setLIntegral_expMapBasis_image (measurableSet_paramSet K) (by fun_prop)]
+  simp_rw [ENNReal.inv_mul_cancel_right
+    (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ ofReal_ne_zero_iff.mpr (expMapBasis_pos _ _))
+    (prod_ne_top fun _ _ ↦ ofReal_ne_top)]
+  rw [setLIntegral_paramSet_exp K Module.finrank_pos, ofReal_mul zero_le_two, mul_pow,
+    ofReal_ofNat, ENNReal.mul_inv_cancel_right (Nat.cast_ne_zero.mpr Module.finrank_pos.ne')
+    (natCast_ne_top _), coe_nnreal_eq, NNReal.coe_real_pi, mul_mul_mul_comm, ← ENNReal.inv_pow,
+    ← mul_assoc, ← mul_assoc, ENNReal.inv_mul_cancel_right (pow_ne_zero _ two_ne_zero)
+    (pow_ne_top ENNReal.ofNat_ne_top)]
+
+end main_results
+
 end NumberField.mixedEmbedding.fundamentalCone