IdealClassQuantitativeTransfer.lean

1 import PaperX.IdealClassQuantitativeConstant
2 
3 /-!
4 # Transfer of a quantitative bound on the actual cone to actual ideal classes
5 
6 The geometric hypothesis is deliberately stated on the actual ideal lattice and
7 ordinary fundamental cone. The resulting ideal-class count is not an abstract
8 label or a supplied arithmetic counting function.
9 -/
10 
11 set_option autoImplicit false
12 noncomputable section
13 
14 open Ideal MeasureTheory Filter Asymptotics
15 open scoped nonZeroDivisors Real Classical Pointwise
16 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
17 open NumberField.mixedEmbedding.euclidean NumberField.mixedEmbedding.fundamentalCone
18 open NumberField.Units
19 
20 namespace PaperX.IdealClassQuantitative
21 
22 variable (K : Type*) [Field K] [NumberField K]
23 
24 /-- The codimension-one boundary exponent in the ideal norm variable. -/
25 def countExponent : ℝ := 1 - (Module.finrank ℚ K : ℝ)⁻¹
26 
27 theorem countExponent_nonneg : 0 ≤ countExponent K := by
28   have hdeg : (1 : ℝ) ≤ Module.finrank ℚ K := by
29     exact_mod_cast (Module.finrank_pos (R := ℚ) (M := K))
30   exact sub_nonneg.mpr (inv_le_one_of_one_le₀ hdeg)
31 
32 /-- Reparametrization changes boundary degree `d-1` into norm exponent `1-1/d`. -/
33 theorem root_boundary_power (y : ℝ) (hy : 0 ≤ y) :
34     (y ^ (Module.finrank ℚ K : ℝ)⁻¹) ^ (Module.finrank ℚ K - 1) =
35       y ^ countExponent K := by
36   have hd : 1 ≤ Module.finrank ℚ K := Module.finrank_pos (R := ℚ) (M := K)
37   have hd0 : (Module.finrank ℚ K : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_zero_of_lt hd)
38   rw [← Real.rpow_natCast, ← Real.rpow_mul hy]
39   congr 1
40   rw [Nat.cast_sub hd, Nat.cast_one, countExponent]
41   field_simp
42 
43 /-- A boundary bound in radial scale yields the corresponding norm-scale bound. -/
44 theorem norm_bound_of_dilation_bound (J : (Ideal (𝓞 K))⁰) (B : ℝ)
45     (hB : ∀ t : ℝ, 1 ≤ t →
46       |(Nat.card (t • coneRegion K 1 ∩ idealEuclideanLattice K J :
47         Set (euclidean.mixedSpace K)) : ℝ) -
48         latticeDensity K J * t ^ Module.finrank ℚ K| ≤
49           B * (t ^ (Module.finrank ℚ K - 1) + 1)) :
50     ∀ y : ℝ, 1 ≤ y →
51       |(latticeCount K J y : ℝ) - latticeDensity K J * y| ≤
52         B * (y ^ countExponent K + 1) := by
53   intro y hy
54   have hy0 : 0 < y := lt_of_lt_of_le zero_lt_one hy
55   have hd : Module.finrank ℚ K ≠ 0 := (Module.finrank_pos (R := ℚ) (M := K)).ne'
56   have ht : 1 ≤ y ^ (Module.finrank ℚ K : ℝ)⁻¹ :=
57     Real.one_le_rpow hy (by positivity)
58   have h := hB (y ^ (Module.finrank ℚ K : ℝ)⁻¹) ht
59   rw [smul_coneRegion_one K (Real.rpow_pos_of_pos hy0 _),
60     Real.rpow_inv_natCast_pow hy0.le hd, root_boundary_power K y hy0.le] at h
61   exact h
62 
63 /-- A bound for the actual ideal lattice yields a uniform-in-threshold ideal-class bound. -/
64 theorem class_bound_of_norm_bound {C : ClassGroup (𝓞 K)} {J : (Ideal (𝓞 K))⁰}
65     (hJ : ClassGroup.mk0 J = C⁻¹) {B : ℝ} (hB0 : 0 ≤ B)
66     (hB : ∀ y : ℝ, 1 ≤ y →
67       |(latticeCount K J y : ℝ) - latticeDensity K J * y| ≤
68         B * (y ^ countExponent K + 1)) :
69     ∀ s : ℝ, 1 ≤ s →
70       |(classCount K C s : ℝ) - classResidue K * s| ≤
71         (B / torsionOrder K * ((absNorm (J : Ideal (𝓞 K)) : ℝ) ^ countExponent K + 1)) *
72           s ^ countExponent K := by
73   intro s hs
74   have hN : (1 : ℝ) ≤ absNorm (J : Ideal (𝓞 K)) := by
75     exact_mod_cast absNorm_pos_of_nonZeroDivisors J
76   have hs0 : 0 ≤ s := le_trans zero_le_one hs
77   have hN0 : (0 : ℝ) ≤ absNorm (J : Ideal (𝓞 K)) := le_trans zero_le_one hN
78   have hy : 1 ≤ s * absNorm (J : Ideal (𝓞 K)) := by
79     nlinarith [mul_nonneg (sub_nonneg.mpr hs) (sub_nonneg.mpr hN)]
80   have hp : 1 ≤ s ^ countExponent K := Real.one_le_rpow hs (countExponent_nonneg K)
81   rw [class_error_eq_lattice_error K hJ, abs_div, abs_of_pos (torsionOrder_cast_pos K)]
82   calc
83     _ ≤ B * ((s * (absNorm (J : Ideal (𝓞 K)) : ℝ)) ^ countExponent K + 1) /
84           torsionOrder K :=
85       div_le_div_of_nonneg_right (hB _ hy) (torsionOrder_cast_pos K).le
86     _ ≤ (B / torsionOrder K * ((absNorm (J : Ideal (𝓞 K)) : ℝ) ^ countExponent K + 1)) *
87           s ^ countExponent K := by
88       rw [Real.mul_rpow hs0 hN0]
89       have hpos : 0 ≤ B / (torsionOrder K : ℝ) := div_nonneg hB0 (torsionOrder_cast_pos K).le
90       calc
91         _ = (B / torsionOrder K) * (s ^ countExponent K *
92             (absNorm (J : Ideal (𝓞 K)) : ℝ) ^ countExponent K + 1) := by ring
93         _ ≤ (B / torsionOrder K) * (s ^ countExponent K *
94             (absNorm (J : Ideal (𝓞 K)) : ℝ) ^ countExponent K +
95             s ^ countExponent K) := mul_le_mul_of_nonneg_left (by linarith) hpos
96         _ = _ := by ring
97 
98 /-- The concrete error is big-O once the concrete lattice discrepancy is bounded. -/
99 theorem class_isBigO_of_dilation_bound {C : ClassGroup (𝓞 K)} {J : (Ideal (𝓞 K))⁰}
100     (hJ : ClassGroup.mk0 J = C⁻¹) {B : ℝ} (hB0 : 0 ≤ B)
101     (hB : ∀ t : ℝ, 1 ≤ t →
102       |(Nat.card (t • coneRegion K 1 ∩ idealEuclideanLattice K J :
103         Set (euclidean.mixedSpace K)) : ℝ) -
104         latticeDensity K J * t ^ Module.finrank ℚ K| ≤
105           B * (t ^ (Module.finrank ℚ K - 1) + 1)) :
106     (fun s : ℝ => (classCount K C s : ℝ) - classResidue K * s) =O[atTop]
107       (fun s : ℝ => s ^ countExponent K) := by
108   apply IsBigO.of_bound
109     (B / torsionOrder K * ((absNorm (J : Ideal (𝓞 K)) : ℝ) ^ countExponent K + 1))
110   filter_upwards [eventually_ge_atTop (1 : ℝ)] with s hs
111   rw [Real.norm_eq_abs, Real.norm_eq_abs,
112     abs_of_nonneg (Real.rpow_nonneg (le_trans zero_le_one hs) _)]
113   exact class_bound_of_norm_bound K hJ hB0 (norm_bound_of_dilation_bound K J B hB) s hs
114 
115 end PaperX.IdealClassQuantitative

Back to source controls