IdealClassQuantitativeConstant.lean

1 import PaperX.IdealClassQuantitativeAttachment
2 
3 /-! Exact normalization of the ordinary ideal-class counting coefficient. -/
4 
5 set_option autoImplicit false
6 noncomputable section
7 
8 open Ideal MeasureTheory
9 open scoped nonZeroDivisors Real Classical
10 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
11 open NumberField.mixedEmbedding.euclidean NumberField.mixedEmbedding.fundamentalCone
12 open NumberField.Units
13 
14 namespace PaperX.IdealClassQuantitative
15 
16 variable (K : Type*) [Field K] [NumberField K]
17 
18 /-- The classical coefficient of the count in one ordinary ideal class. -/
19 def classResidue : ℝ :=
20   (2 ^ nrRealPlaces K * (2 * Real.pi) ^ nrComplexPlaces K * regulator K) /
21     (torsionOrder K * Real.sqrt |discr K|)
22 
23 /-- The cone volume divided by its ideal-lattice covolume. -/
24 def latticeDensity (J : (Ideal (𝓞 K))⁰) : ℝ :=
25   volume.real (coneRegion K 1) / ZLattice.covolume (idealEuclideanLattice K J)
26 
27 /-- Scaling by the norm of the representative and dividing by the roots of unity
28 recovers the coefficient independent of the chosen ideal class. -/
29 theorem latticeDensity_normalization (J : (Ideal (𝓞 K))⁰) :
30     latticeDensity K J * absNorm (J : Ideal (𝓞 K)) * (torsionOrder K : ℝ)⁻¹ =
31       classResidue K := by
32   classical
33   have hJ : (absNorm (J : Ideal (𝓞 K)) : ℝ) ≠ 0 :=
34     Nat.cast_ne_zero.mpr (absNorm_ne_zero_of_nonZeroDivisors J)
35   rw [latticeDensity, classResidue, coneRegion_one, MeasureTheory.measureReal_def,
36     (volumePreserving_toMixed K).measure_preimage (measurableSet_normLeOne K).nullMeasurableSet,
37     volume_normLeOne, ZLattice.covolume_comap _ _ _ (volumePreserving_toMixed K),
38     covolume_idealLattice, ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_pow,
39     ENNReal.toReal_pow, ENNReal.toReal_ofNat, ENNReal.coe_toReal, NNReal.coe_real_pi,
40     ENNReal.toReal_ofReal (regulator_pos K).le, FractionalIdeal.coe_mk0,
41     FractionalIdeal.coeIdeal_absNorm, Rat.cast_natCast, div_eq_mul_inv, div_eq_mul_inv,
42     mul_inv, mul_inv, mul_inv, inv_pow, inv_inv]
43   ring_nf
44   rw [mul_inv_cancel_right₀ hJ]
45 
46 /-- Positivity of the torsion divisor, used for honest division of the count. -/
47 theorem torsionOrder_cast_pos : (0 : ℝ) < torsionOrder K :=
48   Nat.cast_pos.mpr (Nat.pos_of_ne_zero (torsionOrder_ne_zero K))
49 
50 /-- An exact real-valued error identity before any geometric estimate is assumed. -/
51 theorem class_error_eq_lattice_error {C : ClassGroup (𝓞 K)}
52     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹) (s : ℝ) :
53     (classCount K C s : ℝ) - classResidue K * s =
54       ((latticeCount K J (s * absNorm (J : Ideal (𝓞 K))) : ℝ) -
55         latticeDensity K J * (s * absNorm (J : Ideal (𝓞 K)))) /
56           torsionOrder K := by
57   rw [latticeCount_eq_classCount_mul_torsion K hJ, Nat.cast_mul,
58     ← latticeDensity_normalization K J]
59   have ht : (torsionOrder K : ℝ) ≠ 0 := (torsionOrder_cast_pos K).ne'
60   field_simp [ht]
61 
62 end PaperX.IdealClassQuantitative

Back to source controls