English
In a number field K, the limit as s → ∞ of the normalized count of integral ideals in a fixed class C with absNorm ≤ s exists and equals a constant given by the standard analytic formula involving nrRealPlaces, nrComplexPlaces, regulator, torsion order, and discriminant.
Русский
Для числа поля K предел, как s → ∞, нормированное среднее число интегральных идеалов в заданном классе класса образуется в константу, выраженную через число реальных мест, комплексных мест, регулятор, torsionOrder и дискриминант.
LaTeX
$$$\\displaystyle \\lim_{s\\to\\infty} \\frac{\\#\\{ I : I \\subseteq \\mathcal{O}_K, \\; |\\mathrm{absNorm}(I)| \\le s, \\; \\mathrm{mk}_0 I = C \\}}{s} = \\frac{2^{nrRealPlaces(K)} (2\\pi)^{nrComplexPlaces(K)} \\mathrm{regulator}(K)}{\\mathrm{torsionOrder}(K) \\sqrt{|\\mathrm{discr}(K)|}}.$$$
Lean4
/-- The limit of the number of nonzero integral ideals of norm `≤ s` in a fixed class `C` of the
class group divided by `s` when `s → +∞`.
-/
theorem tendsto_norm_le_and_mk_eq_div_atTop :
Tendsto
(fun s : ℝ ↦ (Nat.card { I : (Ideal (𝓞 K))⁰ // absNorm (I : Ideal (𝓞 K)) ≤ s ∧ ClassGroup.mk0 I = C } : ℝ) / s)
atTop
(𝓝 ((2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K) / (torsionOrder K * Real.sqrt |discr K|))) :=
by
classical
have h₁ :
∀ s : ℝ,
{x | x ∈ toMixed K ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm (toMixed K x) ≤ s} =
toMixed K ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s} :=
fun _ ↦ rfl
have h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K := by ext; simp
obtain ⟨J, hJ⟩ := ClassGroup.mk0_surjective C⁻¹
have h₃ : (absNorm J.1 : ℝ) ≠ 0 := (Nat.cast_ne_zero.mpr (absNorm_ne_zero_of_nonZeroDivisors J))
convert
((ZLattice.covolume.tendsto_card_le_div'
(ZLattice.comap ℝ (mixedEmbedding.idealLattice K (FractionalIdeal.mk0 K J)) (toMixed K).toLinearMap) (F :=
fun x ↦ mixedEmbedding.norm (toMixed K x)) (X := (toMixed K) ⁻¹' (fundamentalCone K)) (fun _ _ _ h ↦ ?_)
(fun _ _ h ↦ ?_) (isBounded_normLeOne K) ?_ ?_).mul
(tendsto_const_nhds (x := (absNorm (J : Ideal (𝓞 K)) : ℝ) * (torsionOrder K : ℝ)⁻¹))).comp
(tendsto_id.atTop_mul_const' <| Nat.cast_pos.mpr (absNorm_pos_of_nonZeroDivisors J)) using
2 with s
· simp_rw [Ideal.tendsto_norm_le_and_mk_eq_div_atTop_aux₁ K hJ, id_eq,
Nat.card_congr (Ideal.tendsto_norm_le_and_mk_eq_div_atTop_aux₂ K), ← card_isPrincipal_dvd_norm_le,
Function.comp_def, Nat.cast_mul, div_eq_mul_inv, mul_inv, ← mul_assoc, mul_comm _ (torsionOrder K : ℝ)⁻¹,
mul_comm _ (torsionOrder K : ℝ), mul_assoc]
rw [inv_mul_cancel_left₀ (Nat.cast_ne_zero.mpr (torsionOrder_ne_zero K)), inv_mul_cancel₀ h₃, mul_one]
· rw [h₁, h₂, MeasureTheory.measureReal_def,
(volumePreserving_toMixed K).measure_preimage (measurableSet_normLeOne K).nullMeasurableSet, volume_normLeOne,
ZLattice.covolume_comap _ _ _ (volumePreserving_toMixed K), covolume_idealLattice, ENNReal.toReal_mul,
ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_pow, ENNReal.toReal_ofNat, ENNReal.coe_toReal,
NNReal.coe_real_pi, ENNReal.toReal_ofReal (regulator_pos K).le, FractionalIdeal.coe_mk0,
FractionalIdeal.coeIdeal_absNorm, Rat.cast_natCast, div_eq_mul_inv, div_eq_mul_inv, mul_inv, mul_inv, mul_inv,
inv_pow, inv_inv]
ring_nf
rw [mul_inv_cancel_right₀ h₃]
· rwa [Set.mem_preimage, map_smul, smul_mem_iff_mem h.ne']
· dsimp only
rw [map_smul, mixedEmbedding.norm_smul, euclidean.finrank, abs_of_nonneg h]
· exact (toMixed K).continuous.measurable (measurableSet_normLeOne K)
·
rw [h₁, ← (toMixed K).coe_toHomeomorph, ← Homeomorph.preimage_frontier, (toMixed K).coe_toHomeomorph,
(volumePreserving_toMixed K).measure_preimage measurableSet_frontier.nullMeasurableSet, h₂,
volume_frontier_normLeOne]
