English
The limit as s→∞ of the count of integral ideals with absNorm ≤ s, divided by s, tends to a constant given by the usual Dedekind-type density formula (involving regulator, discriminant, and class number).
Русский
Предел количества интегральных идеалов с нормой до s, делённой на s, при s→∞ совпадает с константой, задаваемой по норме-распределению для поля (регулятор, дискриминант, класс).
LaTeX
$$$\\lim_{s\\to\\infty} \\frac{\\#\\{ I : I \\subseteq \\mathcal{O}_K \\;|\\; |\\mathrm{absNorm}(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 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 ≤ s } : ℝ) / s) atTop
(𝓝
((2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * classNumber K) /
(torsionOrder K * Real.sqrt |discr K|))) :=
by
have := (tendsto_norm_le_div_atTop₀ K).add tendsto_inv_atTop_zero
rw [add_zero] at this
apply this.congr'
filter_upwards [eventually_ge_atTop 0] with s hs
simp_rw [← Nat.le_floor_iff hs]
rw [Ideal.card_norm_le_eq_card_norm_le_add_one, Nat.cast_add, Nat.cast_one, add_div, one_div]
