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

Mathlib.lean

@@ -999,6 +999,7 @@ import Mathlib.Analysis.BoxIntegral.Partition.Measure
 import Mathlib.Analysis.BoxIntegral.Partition.Split
 import Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
 import Mathlib.Analysis.BoxIntegral.Partition.Tagged
+import Mathlib.Analysis.BoxIntegral.UnitPartition
 import Mathlib.Analysis.CStarAlgebra.Basic
 import Mathlib.Analysis.CStarAlgebra.Classes
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
@@ -3584,6 +3585,7 @@ import Mathlib.NumberTheory.LSeries.HurwitzZetaValues
 import Mathlib.NumberTheory.LSeries.Linearity
 import Mathlib.NumberTheory.LSeries.MellinEqDirichlet
 import Mathlib.NumberTheory.LSeries.Positivity
+import Mathlib.NumberTheory.LSeries.Residue
 import Mathlib.NumberTheory.LSeries.RiemannZeta
 import Mathlib.NumberTheory.LSeries.ZMod
 import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
@@ -3624,13 +3626,16 @@ import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
 import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
+import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLessThanOne
 import Mathlib.NumberTheory.NumberField.ClassNumber
+import Mathlib.NumberTheory.NumberField.DedekindZeta
 import Mathlib.NumberTheory.NumberField.Discriminant.Basic
 import Mathlib.NumberTheory.NumberField.Discriminant.Defs
 import Mathlib.NumberTheory.NumberField.Embeddings
 import Mathlib.NumberTheory.NumberField.EquivReindex
 import Mathlib.NumberTheory.NumberField.FractionalIdeal
 import Mathlib.NumberTheory.NumberField.House
+import Mathlib.NumberTheory.NumberField.Ideal
 import Mathlib.NumberTheory.NumberField.Norm
 import Mathlib.NumberTheory.NumberField.Units.Basic
 import Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Mathlib/Algebra/Group/Indicator.lean

@@ -122,6 +122,11 @@ theorem mem_of_mulIndicator_ne_one (h : mulIndicator s f a ≠ 1) : a ∈ s :=
 @[to_additive]
 theorem eqOn_mulIndicator : EqOn (mulIndicator s f) f s := fun _ hx => mulIndicator_of_mem hx f
 
+/-- Docstring. -/
+@[to_additive]
+theorem eqOn_mulIndicator' : EqOn (mulIndicator s f) 1 sᶜ :=
+  fun _ hx => mulIndicator_of_not_mem hx f
+
 @[to_additive]
 theorem mulSupport_mulIndicator_subset : mulSupport (s.mulIndicator f) ⊆ s := fun _ hx =>
   hx.imp_symm fun h => mulIndicator_of_not_mem h f

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -180,6 +180,12 @@ theorem mul_mem_nonZeroDivisors {a b : M₁} : a * b ∈ M₁⁰ ↔ a ∈ M₁
     apply hb
     rw [mul_assoc, hx]
 
+theorem nonZeroDivisors_dvd_iff_dvd_coe {a b : M₁⁰} :
+    a ∣ b ↔ (a : M₁) ∣ (b : M₁) :=
+  ⟨fun ⟨c, hc⟩ ↦ by simp_rw [hc, Submonoid.coe_mul, dvd_mul_right],
+  fun ⟨c, hc⟩ ↦ ⟨⟨c, (mul_mem_nonZeroDivisors.mp (hc ▸ b.prop)).2⟩,
+    by simp_rw [Subtype.ext_iff, Submonoid.coe_mul, hc]⟩⟩
+
 theorem isUnit_of_mem_nonZeroDivisors {G₀ : Type*} [GroupWithZero G₀] {x : G₀}
     (hx : x ∈ nonZeroDivisors G₀) : IsUnit x :=
   ⟨⟨x, x⁻¹, mul_inv_cancel₀ (nonZeroDivisors.ne_zero hx),

Mathlib/Algebra/Module/ZLattice/Basic.lean

@@ -61,11 +61,17 @@ variable (b : Basis ι K E)
 
 theorem span_top : span K (span ℤ (Set.range b) : Set E) = ⊤ := by simp [span_span_of_tower]
 
-
 theorem map {F : Type*} [NormedAddCommGroup F] [NormedSpace K F] (f : E ≃ₗ[K] F) :
     Submodule.map (f.restrictScalars ℤ) (span ℤ (Set.range b)) = span ℤ (Set.range (b.map f)) := by
   simp_rw [Submodule.map_span, LinearEquiv.restrictScalars_apply, Basis.coe_map, Set.range_comp]
 
+open scoped Pointwise in
+theorem smul {c : K} (hc : c ≠ 0) :
+    c • span ℤ (Set.range b) = span ℤ (Set.range (b.isUnitSMul (fun _ ↦ Ne.isUnit hc))) := by
+  rw [smul_span, Set.smul_set_range]
+  congr!
+  rw [Basis.isUnitSMul_apply]
+
 /-- The fundamental domain of the ℤ-lattice spanned by `b`. See `ZSpan.isAddFundamentalDomain`
 for the proof that it is a fundamental domain. -/
 def fundamentalDomain : Set E := {m | ∀ i, b.repr m i ∈ Set.Ico (0 : K) 1}
@@ -305,9 +311,16 @@ instance [Finite ι] : DiscreteTopology (span ℤ (Set.range b)) := by
   · exact discreteTopology_pi_basisFun
   · refine Subtype.map_injective _ (Basis.equivFun b).injective
 
-instance [Finite ι] : DiscreteTopology (span ℤ (Set.range b)).toAddSubgroup :=
+instance instDiscreteTopology [Finite ι] : DiscreteTopology (span ℤ (Set.range b)).toAddSubgroup :=
   inferInstanceAs <| DiscreteTopology (span ℤ (Set.range b))
 
+theorem setFinite_inter [ProperSpace E] [Finite ι] {s : Set E} (hs : Bornology.IsBounded s) :
+    Set.Finite (s ∩ (span ℤ (Set.range b))) := by
+  have : DiscreteTopology (span ℤ (Set.range b)) := by infer_instance
+  refine Metric.finite_isBounded_inter_isClosed hs ?_
+  change IsClosed (span ℤ (Set.range b)).toAddSubgroup
+  exact inferInstance
+
 @[measurability]
 theorem fundamentalDomain_measurableSet [MeasurableSpace E] [OpensMeasurableSpace E] [Finite ι] :
     MeasurableSet (fundamentalDomain b) := by
@@ -694,4 +707,21 @@ theorem Basis.ofZLatticeComap_repr_apply (e : F ≃ₗ[K] E) {ι : Type*} (b : B
 
 end comap
 
+section NormedLinearOrderedField_comap
+
+variable (K : Type*) [NormedLinearOrderedField K] [HasSolidNorm K] [FloorRing K]
+variable {E : Type*} [NormedAddCommGroup E]  [NormedSpace K E] [FiniteDimensional K E]
+  [ProperSpace E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace K F]  [FiniteDimensional K F]
+  [ProperSpace F]
+variable (L : Submodule ℤ E) [DiscreteTopology L] [IsZLattice K L]
+
+theorem Basis.ofZLatticeBasis_comap (e : F ≃L[K] E) {ι : Type*} (b : Basis ι ℤ L) :
+    (b.ofZLatticeComap K L e.toLinearEquiv).ofZLatticeBasis K (ZLattice.comap K L e.toLinearMap) =
+    (b.ofZLatticeBasis K L).map e.symm.toLinearEquiv := by
+  ext
+  simp
+
+end NormedLinearOrderedField_comap
+
 end ZLattice

Mathlib/Algebra/Module/ZLattice/Covolume.lean

@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
 import Mathlib.Algebra.Module.ZLattice.Basic
+import Mathlib.Analysis.BoxIntegral.UnitPartition
+import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
+import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 
 /-!
 # Covolume of ℤ-lattices
@@ -23,6 +26,25 @@ choice of the fundamental domain of `L`.
 * `ZLattice.covolume_eq_det`: if `L` is a lattice in `ℝ^n`, then its covolume is the absolute
 value of the determinant of any `ℤ`-basis of `L`.
 
+* `Zlattice.covolume.tendsto_card_div_pow`: Let `s` be a bounded measurable set of `ι → ℝ`, then
+the number of points in `s ∩ n⁻¹ • L` divided by `n ^ card ι` tends to `volume s / covolume L`
+when `n : ℕ` tends to infinity. See also `Zlattice.covolume.tendsto_card_div_pow'` for a version
+for `InnerProductSpace ℝ E` and `Zlattice.covolume.tendsto_card_div_pow''` for the general version.
+
+* `Zlattice.covolume.tendsto_card_le_div`: Let `X` be a cone in `ι → ℝ` and let `F : (ι → ℝ) → ℝ`
+be a function such that `F (c • x) = c ^ card ι * F x`. Then the number of points `x ∈ X` such that
+`F x ≤ c` divided by `c` tends to `volume {x ∈ X | F x ≤ 1} / covolume L` when `c : ℝ` tends to
+infinity. See also `Zlattice.covolume.tendsto_card_le_div'` for a version for
+`InnerProductSpace ℝ E` and `Zlattice.covolume.tendsto_card_le_div''` for the general version.
+
+## Naming conventions
+
+Many of the same results are true in the pi case `E` is `ι → ℝ` and in the case `E` is an
+`InnerProductSpace`. We use the following convention: the plain name is for the pi case, for eg.
+`volume_image_eq_volume_div_covolume`. For the same result in the `InnerProductSpace` case, we add
+a `prime`, for eg. `volume_image_eq_volume_div_covolume'`. When the same result exists in the
+general case, we had two primes, eg. `Zlattice.covolume.tendsto_card_div_pow''`.
+
 -/
 
 noncomputable section
@@ -42,7 +64,7 @@ def covolume (μ : Measure E := by volume_tac) : ℝ := (addCovolume L E μ).toR
 
 end General
 
-section Real
+section Basic
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
 variable [MeasurableSpace E] [BorelSpace E]
@@ -96,6 +118,206 @@ theorem covolume_eq_det {ι : Type*} [Fintype ι] [DecidableEq ι] (L : Submodul
   ext1
   exact b.ofZLatticeBasis_apply ℝ L _
 
-end Real
+theorem covolume_eq_det_inv {ι : Type*} [Fintype ι] [DecidableEq ι] (L : Submodule ℤ (ι → ℝ))
+    [DiscreteTopology L] [IsZLattice ℝ L] (b : Basis ι ℤ L) :
+    covolume L = |(LinearEquiv.det (b.ofZLatticeBasis ℝ L).equivFun : ℝ)|⁻¹ := by
+  rw [covolume_eq_det L b, ← Pi.basisFun_det_apply, show (((↑) : L → _) ∘ ⇑b) =
+    (b.ofZLatticeBasis ℝ) by ext; simp, ← Basis.det_inv, ← abs_inv, Units.val_inv_eq_inv_val,
+    IsUnit.unit_spec, Basis.det_basis, LinearEquiv.coe_det]
+  rfl
+
+theorem volume_image_eq_volume_div_covolume {ι : Type*} [Fintype ι] [DecidableEq ι]
+    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L] [IsZLattice ℝ L] (b : Basis ι ℤ L)
+    {s : Set (ι → ℝ)} :
+    volume ((b.ofZLatticeBasis ℝ L).equivFun '' s) = volume s / ENNReal.ofReal (covolume L) := by
+  rw [LinearEquiv.image_eq_preimage, Measure.addHaar_preimage_linearEquiv, LinearEquiv.symm_symm,
+    covolume_eq_det_inv L b, ENNReal.div_eq_inv_mul, ENNReal.ofReal_inv_of_pos
+    (abs_pos.mpr (LinearEquiv.det _).ne_zero), inv_inv, LinearEquiv.coe_det]
+
+/-- Docstring. -/
+theorem volume_image_eq_volume_div_covolume' {E : Type*} [NormedAddCommGroup E]
+    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
+    (L : Submodule ℤ E) [DiscreteTopology L] [IsZLattice ℝ L] {ι : Type*} [Fintype ι]
+    (b : Basis ι ℤ L) {s : Set E} (hs : NullMeasurableSet s) :
+    volume ((b.ofZLatticeBasis ℝ).equivFun '' s) = volume s / ENNReal.ofReal (covolume L) := by
+  classical
+  let e : Fin (finrank ℝ E) ≃ ι :=
+    Fintype.equivOfCardEq (by rw [Fintype.card_fin, finrank_eq_card_basis (b.ofZLatticeBasis ℝ)])
+  let f := (EuclideanSpace.equiv ι ℝ).symm.trans
+    ((stdOrthonormalBasis ℝ E).reindex e).repr.toContinuousLinearEquiv.symm
+  have hf : MeasurePreserving f :=
+    ((stdOrthonormalBasis ℝ E).reindex e).measurePreserving_repr_symm.comp
+      (EuclideanSpace.volume_preserving_measurableEquiv ι).symm
+  rw [← hf.measure_preimage hs, ← (covolume_comap L volume volume hf),
+    ← volume_image_eq_volume_div_covolume (ZLattice.comap ℝ L f.toLinearMap)
+    (b.ofZLatticeComap ℝ L f.toLinearEquiv), Basis.ofZLatticeBasis_comap,
+    ← f.image_symm_eq_preimage, ← Set.image_comp]
+  simp
+
+end Basic
+
+namespace covolume
+
+section General
+
+open Filter Fintype Pointwise Topology BoxIntegral Bornology
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+variable {L : Submodule ℤ E} [DiscreteTopology L] [IsZLattice ℝ L]
+variable {ι : Type*} [Fintype ι] (b : Basis ι ℤ L)
+
+/-- Docstring. -/
+theorem tendsto_card_div_pow'' [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
+    {s : Set E} (hs₁ : IsBounded s) (hs₂ : MeasurableSet s)
+    (hs₃ : volume (frontier ((b.ofZLatticeBasis ℝ).equivFun '' s)) = 0):
+    Tendsto (fun n : ℕ ↦ (Nat.card (s ∩ (n : ℝ)⁻¹ • L : Set E) : ℝ) / n ^ card ι)
+      atTop (𝓝 (volume ((b.ofZLatticeBasis ℝ).equivFun '' s)).toReal) := by
+  refine Tendsto.congr' ?_
+    (unitPartition.tendsto_card_div_pow' ((b.ofZLatticeBasis ℝ).equivFun '' s) ?_ ?_ hs₃)
+  · filter_upwards [eventually_gt_atTop 0] with n hn
+    congr
+    refine Nat.card_congr <| ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.subtypeEquiv fun x ↦ ?_).symm
+    simp_rw [Set.mem_inter_iff, ← b.ofZLatticeBasis_span ℝ, LinearEquiv.coe_toEquiv,
+      Basis.equivFun_apply, Set.mem_image, DFunLike.coe_fn_eq, EmbeddingLike.apply_eq_iff_eq,
+      exists_eq_right, and_congr_right_iff, Set.mem_inv_smul_set_iff₀ (by aesop : (n:ℝ) ≠ 0),
+      ← Finsupp.coe_smul, ← LinearEquiv.map_smul, SetLike.mem_coe, Basis.mem_span_iff_repr_mem,
+      Pi.basisFun_repr, implies_true]
+  · rw [← NormedSpace.isVonNBounded_iff ℝ] at hs₁ ⊢
+    exact Bornology.IsVonNBounded.image hs₁ ((b.ofZLatticeBasis ℝ).equivFunL : E →L[ℝ] ι → ℝ)
+  · exact (b.ofZLatticeBasis ℝ).equivFunL.toHomeomorph.toMeasurableEquiv.measurableSet_image.mpr hs₂
+
+private theorem tendsto_card_le_div''_aux {X : Set E} (hX : ∀ ⦃x⦄ ⦃r:ℝ⦄, x ∈ X → 0 < r → r • x ∈ X)
+    {F : E → ℝ} (hF₁ : ∀ x ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * (F x)) {c : ℝ} (hc : 0 < c) :
+    c • {x ∈ X | F x ≤ 1} = {x ∈ X | F x ≤ c ^ card ι} := by
+  ext x
+  simp_rw [Set.mem_smul_set_iff_inv_smul_mem₀ hc.ne', Set.mem_setOf_eq, hF₁ _
+    (inv_pos_of_pos hc).le, inv_pow, inv_mul_le_iff₀ (pow_pos hc _), mul_one, and_congr_left_iff]
+  exact fun _ ↦ ⟨fun h ↦ (smul_inv_smul₀ hc.ne' x) ▸ hX h hc, fun h ↦ hX h (inv_pos_of_pos hc)⟩
+
+/-- Docstring. -/
+theorem tendsto_card_le_div'' [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
+    [Nonempty ι] {X : Set E} (hX : ∀ ⦃x⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X)
+    {F : E → ℝ} (h₁ : ∀ x ⦃r : ℝ⦄, 0 ≤ r →  F (r • x) = r ^ card ι * (F x))
+    (h₂ : IsBounded {x ∈ X | F x ≤ 1}) (h₃ : MeasurableSet {x ∈ X | F x ≤ 1})
+    (h₄ : volume (frontier ((b.ofZLatticeBasis ℝ L).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0) :
+    Tendsto (fun c : ℝ ↦
+      Nat.card ({x ∈ X | F x ≤ c} ∩ L : Set E) / (c : ℝ))
+        atTop (𝓝 (volume ((b.ofZLatticeBasis ℝ).equivFun '' {x ∈ X | F x ≤ 1})).toReal) := by
+  have h : (card ι : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr card_ne_zero
+  refine Tendsto.congr' ?_ <| (unitPartition.tendsto_card_div_pow
+      ((b.ofZLatticeBasis ℝ).equivFun '' {x ∈ X | F x ≤ 1}) ?_ ?_ h₄ fun x y hx hy ↦ ?_).comp
+        (tendsto_rpow_atTop <| inv_pos.mpr
+          (Nat.cast_pos.mpr card_pos) : Tendsto (fun x ↦ x ^ (card ι : ℝ)⁻¹) atTop atTop)
+  · filter_upwards [eventually_gt_atTop 0] with c hc
+    obtain ⟨hc₁, hc₂⟩ := lt_iff_le_and_ne.mp hc
+    rw [Function.comp_apply, ← Real.rpow_natCast, Real.rpow_inv_rpow hc₁ h, eq_comm]
+    congr
+    refine Nat.card_congr <| Equiv.subtypeEquiv ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.trans
+          (Equiv.smulRight (a := c ^ (- (card ι : ℝ)⁻¹)) (by aesop))) fun _ ↦ ?_
+    rw [Set.mem_inter_iff, Set.mem_inter_iff, Equiv.trans_apply, LinearEquiv.coe_toEquiv,
+      Equiv.smulRight_apply, Real.rpow_neg hc₁, Set.smul_mem_smul_set_iff₀ (by aesop),
+      ← Set.mem_smul_set_iff_inv_smul_mem₀ (by aesop), ← image_smul_set,
+      tendsto_card_le_div''_aux hX h₁ (by positivity), ← Real.rpow_natCast, ← Real.rpow_mul hc₁,
+      inv_mul_cancel₀ h, Real.rpow_one]
+    simp_rw [SetLike.mem_coe, Set.mem_image, EmbeddingLike.apply_eq_iff_eq, exists_eq_right,
+      and_congr_right_iff, ← b.ofZLatticeBasis_span ℝ, Basis.mem_span_iff_repr_mem,
+      Pi.basisFun_repr, Basis.equivFun_apply, implies_true]
+  · rw [← NormedSpace.isVonNBounded_iff ℝ] at h₂ ⊢
+    exact Bornology.IsVonNBounded.image h₂ ((b.ofZLatticeBasis ℝ).equivFunL : E →L[ℝ] ι → ℝ)
+  · exact (b.ofZLatticeBasis ℝ).equivFunL.toHomeomorph.toMeasurableEquiv.measurableSet_image.mpr h₃
+  · simp_rw [← image_smul_set]
+    apply Set.image_mono
+    rw [tendsto_card_le_div''_aux hX h₁ hx,
+      tendsto_card_le_div''_aux hX h₁ (lt_of_lt_of_le hx hy)]
+    exact fun a ⟨ha₁, ha₂⟩ ↦ ⟨ha₁, le_trans ha₂ <| pow_le_pow_left (le_of_lt hx) hy _⟩
+
+end General
+
+section Pi
+
+open Filter Fintype Pointwise Topology Bornology
+
+private theorem frontier_equivFun {E : Type*} [AddCommGroup E] [Module ℝ E] {ι : Type*} [Fintype ι]
+    [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E]
+    (b : Basis ι ℝ E) (s : Set E) :
+    frontier (b.equivFun '' s) = b.equivFun '' (frontier s) := by
+  rw [LinearEquiv.image_eq_preimage, LinearEquiv.image_eq_preimage]
+  exact (Homeomorph.preimage_frontier b.equivFunL.toHomeomorph.symm s).symm
+
+variable {ι : Type*} [Fintype ι]
+variable (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L] [IsZLattice ℝ L]
+
+theorem tendsto_card_div_pow (b : Basis ι ℤ L) {s : Set (ι → ℝ)} (hs₁ : IsBounded s)
+    (hs₂ : MeasurableSet s) (hs₃ : volume (frontier s) = 0) :
+    Tendsto (fun n : ℕ ↦ (Nat.card (s ∩ (n : ℝ)⁻¹ • L : Set (ι → ℝ)) : ℝ) / n ^ card ι)
+      atTop (𝓝 ((volume s).toReal / covolume L)) := by
+  classical
+  convert tendsto_card_div_pow'' b hs₁ hs₂ ?_
+  · rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
+      ENNReal.toReal_ofReal (covolume_pos L volume).le]
+  · rw [frontier_equivFun, volume_image_eq_volume_div_covolume, hs₃, ENNReal.zero_div]
+
+theorem tendsto_card_le_div {X : Set (ι → ℝ)} (hX : ∀ ⦃x⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X)
+    {F : (ι → ℝ) → ℝ} (h₁ : ∀ x ⦃r : ℝ⦄, 0 ≤ r →  F (r • x) = r ^ card ι * (F x))
+    (h₂ : IsBounded {x ∈ X | F x ≤ 1}) (h₃ : MeasurableSet {x ∈ X | F x ≤ 1})
+    (h₄ : volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0) [Nonempty ι] :
+    Tendsto (fun c : ℝ ↦
+      Nat.card ({x ∈ X | F x ≤ c} ∩ L : Set (ι → ℝ)) / (c : ℝ))
+        atTop (𝓝 ((volume {x ∈ X | F x ≤ 1}).toReal / covolume L)) := by
+  classical
+  let e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := by
+    refine Fintype.equivOfCardEq ?_
+    rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]
+  let b := (Module.Free.chooseBasis ℤ L).reindex e
+  convert tendsto_card_le_div'' b hX h₁ h₂ h₃ ?_
+  · rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
+      ENNReal.toReal_ofReal (covolume_pos L volume).le]
+  · rw [frontier_equivFun, volume_image_eq_volume_div_covolume, h₄, ENNReal.zero_div]
+
+end Pi
+
+section InnerProductSpace
+
+open Filter Pointwise Topology Bornology
+
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+  [MeasurableSpace E] [BorelSpace E]
+variable (L : Submodule ℤ E) [DiscreteTopology L] [IsZLattice ℝ L]
+
+/-- Docstring. -/
+theorem tendsto_card_div_pow' {s : Set E} (hs₁ : IsBounded s) (hs₂ : MeasurableSet s)
+    (hs₃ : volume (frontier s) = 0) :
+    Tendsto (fun n : ℕ ↦ (Nat.card (s ∩ (n : ℝ)⁻¹ • L : Set E) : ℝ) / n ^ finrank ℝ E)
+      atTop (𝓝 ((volume s).toReal / covolume L)) := by
+  let b := Module.Free.chooseBasis ℤ L
+  convert tendsto_card_div_pow'' b hs₁ hs₂ ?_
+  · rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]
+  · rw [volume_image_eq_volume_div_covolume' L b hs₂.nullMeasurableSet, ENNReal.toReal_div,
+      ENNReal.toReal_ofReal (covolume_pos L volume).le]
+  · rw [frontier_equivFun, volume_image_eq_volume_div_covolume', hs₃, ENNReal.zero_div]
+    exact NullMeasurableSet.of_null hs₃
+
+/-- Docstring. -/
+theorem tendsto_card_le_div' [Nontrivial E] {X : Set E} {F : E → ℝ}
+    (hX : ∀ ⦃x⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X)
+    (h₁ : ∀ x ⦃r : ℝ⦄, 0 ≤ r →  F (r • x) = r ^ finrank ℝ E * (F x))
+    (h₂ : IsBounded {x ∈ X | F x ≤ 1}) (h₃ : MeasurableSet {x ∈ X | F x ≤ 1})
+    (h₄ : volume (frontier {x ∈ X | F x ≤ 1}) = 0) :
+    Tendsto (fun c : ℝ ↦
+      Nat.card ({x ∈ X | F x ≤ c} ∩ L : Set E) / (c : ℝ))
+        atTop (𝓝 ((volume {x ∈ X | F x ≤ 1}).toReal / covolume L)) := by
+  let b := Module.Free.chooseBasis ℤ L
+  convert tendsto_card_le_div'' b hX ?_ h₂ h₃ ?_
+  · rw [volume_image_eq_volume_div_covolume' L b h₃.nullMeasurableSet, ENNReal.toReal_div,
+      ENNReal.toReal_ofReal (covolume_pos L volume).le]
+  · have : Nontrivial L := nontrivial_of_finrank_pos <| (ZLattice.rank ℝ L).symm ▸ finrank_pos
+    infer_instance
+  · rwa [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]
+  · rw [frontier_equivFun, volume_image_eq_volume_div_covolume', h₄, ENNReal.zero_div]
+    exact NullMeasurableSet.of_null h₄
+
+end InnerProductSpace
+
+end covolume
 
 end ZLattice