English
The limit of the normalized count of integral ideals with absNorm ≤ s, as s → ∞, equals a constant involving nrRealPlaces, nrComplexPlaces, regulator, and discriminant, with a zero-threshold variant.
Русский
Предел нормированного счёта интегральных идеалов с absNorm ≤ s при s→∞ равен константе, зависящей от nrRealPlaces, nrComplexPlaces, регулятора и дискриминанта; существует особый вариант для нулевого порога.
LaTeX
$$$\\lim_{s\\to\\infty} \\frac{\\#\\{ I : I \\subseteq \\mathcal{O}_K, \\\\; |I| \\le s \\}}{s} = \\frac{2^{nrRealPlaces(K)} (2\\pi)^{nrComplexPlaces(K)} \\mathrm{regulator}(K) \\mathrm{classNumber}(K)}{\\mathrm{torsionOrder}(K) \\sqrt{|\\mathrm{discr}(K)|}}.$$$
Lean4
/-- The limit of the number of nonzero integral ideals of norm `≤ s` divided by `s` when `s → +∞`.
-/
theorem tendsto_norm_le_div_atTop₀ :
Tendsto (fun s : ℝ ↦ (Nat.card { I : (Ideal (𝓞 K))⁰ // absNorm (I : Ideal (𝓞 K)) ≤ s } : ℝ) / s) atTop
(𝓝
((2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * classNumber K) /
(torsionOrder K * Real.sqrt |discr K|))) :=
by
classical
convert Filter.Tendsto.congr' ?_ (tendsto_finset_sum Finset.univ (fun C _ ↦ tendsto_norm_le_and_mk_eq_div_atTop K C))
· rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, classNumber]
ring
· filter_upwards [eventually_ge_atTop 0] with s hs
have : Fintype { I : (Ideal (𝓞 K))⁰ // absNorm (I : Ideal (𝓞 K)) ≤ s } :=
by
simp_rw [← Nat.le_floor_iff hs]
refine @Fintype.ofFinite _ (finite_setOf_absNorm_le₀ ⌊s⌋₊)
let e := fun C : ClassGroup (𝓞 K) ↦
Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ ↦ absNorm I.1 ≤ s) (fun I ↦ ClassGroup.mk0 I = C)
simp_rw [← Nat.card_congr (e _), Nat.card_eq_fintype_card, Fintype.subtype_card]
rw [Fintype.card,
Finset.card_eq_sum_card_fiberwise (f := fun I ↦ ClassGroup.mk0 I.1) (t := Finset.univ)
(fun _ _ ↦ Finset.mem_univ _),
Nat.cast_sum, Finset.sum_div]
