IdealNormCharacterBound.lean

1 import PaperX.IdealNormWeightedAttachment
2 import PaperX.IdealClassQuantitativeTransfer
3 
4 /-! Transfer of a bound for actual generators to actual ideal norm characters.
5 The generator estimate is supplied; no estimate for the ideal sum is assumed.
6 The inverse-class representative's character value must remain nonzero. -/
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 open Ideal NumberField Filter Asymptotics
12 open scoped nonZeroDivisors
13 open NumberField.Units
14 
15 namespace PaperX.IdealNormWeighted
16 
17 open PaperX.IdealClassQuantitative
18 
19 variable (K : Type*) [Field K] [NumberField K]
20 
21 /-- An actual generator estimate gives an explicit power-saving ideal-character estimate. -/
22 theorem classNormSum_bound_of_generator_bound {C : ClassGroup (𝓞 K)}
23     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹)
24     (m : ℕ) (χ : ZMod m →*₀ ℂ)
25     (hχJ : χ (absNorm (J : Ideal (𝓞 K)) : ZMod m) ≠ 0)
26     {B : ℝ} (hB0 : 0 ≤ B)
27     (hB : ∀ Y : ℝ, 1 ≤ Y →
28       ‖boundedGeneratorSum K J (fun n => χ (n : ZMod m)) Y‖ ≤
29         B * (Y ^ countExponent K + 1)) :
30     ∀ X : ℝ, 1 ≤ X →
31       ‖classNormSum K C (fun n => χ (n : ZMod m)) X‖ ≤
32         (B / ‖(torsionOrder K : ℂ) * χ (absNorm (J : Ideal (𝓞 K)) : ZMod m)‖ *
33           ((absNorm (J : Ideal (𝓞 K)) : ℝ) ^ countExponent K + 1)) *
34             X ^ countExponent K := by
35   intro X hX
36   have hN : (1 : ℝ) ≤ absNorm (J : Ideal (𝓞 K)) := by
37     exact_mod_cast absNorm_pos_of_nonZeroDivisors J
38   have hX0 : 0 ≤ X := le_trans zero_le_one hX
39   have hN0 : (0 : ℝ) ≤ absNorm (J : Ideal (𝓞 K)) := le_trans zero_le_one hN
40   have hY : 1 ≤ X * absNorm (J : Ideal (𝓞 K)) := by
41     nlinarith [mul_nonneg (sub_nonneg.mpr hX) (sub_nonneg.mpr hN)]
42   have hp : 1 ≤ X ^ countExponent K := Real.one_le_rpow hX (countExponent_nonneg K)
43   rw [classNormSum_character_eq_div K hJ m χ hχJ X, norm_div]
44   calc
45     _ ≤ B * ((X * (absNorm (J : Ideal (𝓞 K)) : ℝ)) ^ countExponent K + 1) /
46         ‖(torsionOrder K : ℂ) * χ (absNorm (J : Ideal (𝓞 K)) : ZMod m)‖ :=
47       div_le_div_of_nonneg_right (hB _ hY) (norm_nonneg _)
48     _ ≤ _ := by
49       rw [Real.mul_rpow hX0 hN0]
50       have hc : 0 ≤ B /
51           ‖(torsionOrder K : ℂ) * χ (absNorm (J : Ideal (𝓞 K)) : ZMod m)‖ :=
52         div_nonneg hB0 (norm_nonneg _)
53       calc
54         _ = (B / ‖(torsionOrder K : ℂ) * χ (absNorm (J : Ideal (𝓞 K)) : ZMod m)‖) *
55             (X ^ countExponent K * (absNorm (J : Ideal (𝓞 K)) : ℝ) ^ countExponent K + 1) := by ring
56         _ ≤ (B / ‖(torsionOrder K : ℂ) * χ (absNorm (J : Ideal (𝓞 K)) : ZMod m)‖) *
57             (X ^ countExponent K * (absNorm (J : Ideal (𝓞 K)) : ℝ) ^ countExponent K +
58               X ^ countExponent K) := mul_le_mul_of_nonneg_left (by linarith) hc
59         _ = _ := by ring
60 
61 /-- Existence of an actual generator bound transfers to an actual ideal bound. -/
62 theorem exists_classNormSum_bound_of_generator_bound {C : ClassGroup (𝓞 K)}
63     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹)
64     (m : ℕ) (χ : ZMod m →*₀ ℂ)
65     (hχJ : χ (absNorm (J : Ideal (𝓞 K)) : ZMod m) ≠ 0)
66     (hgen : ∃ B : ℝ, 0 ≤ B ∧ ∀ Y : ℝ, 1 ≤ Y →
67       ‖boundedGeneratorSum K J (fun n => χ (n : ZMod m)) Y‖ ≤
68         B * (Y ^ countExponent K + 1)) :
69     ∃ M : ℝ, 0 ≤ M ∧ ∀ X : ℝ, 1 ≤ X →
70       ‖classNormSum K C (fun n => χ (n : ZMod m)) X‖ ≤ M * X ^ countExponent K := by
71   obtain ⟨B, hB0, hB⟩ := hgen
72   refine ⟨B / ‖(torsionOrder K : ℂ) * χ (absNorm (J : Ideal (𝓞 K)) : ZMod m)‖ *
73     ((absNorm (J : Ideal (𝓞 K)) : ℝ) ^ countExponent K + 1), ?_,
74     classNormSum_bound_of_generator_bound K hJ m χ hχJ hB0 hB⟩
75   positivity
76 
77 /-- Asymptotic form of the same transfer, still on the actual bounded ideal sum. -/
78 theorem classNormSum_isBigO_of_generator_bound {C : ClassGroup (𝓞 K)}
79     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹)
80     (m : ℕ) (χ : ZMod m →*₀ ℂ)
81     (hχJ : χ (absNorm (J : Ideal (𝓞 K)) : ZMod m) ≠ 0)
82     (hgen : ∃ B : ℝ, 0 ≤ B ∧ ∀ Y : ℝ, 1 ≤ Y →
83       ‖boundedGeneratorSum K J (fun n => χ (n : ZMod m)) Y‖ ≤
84         B * (Y ^ countExponent K + 1)) :
85     classNormSum K C (fun n => χ (n : ZMod m)) =O[atTop]
86       (fun X : ℝ => X ^ countExponent K) := by
87   obtain ⟨M, _, hM⟩ := exists_classNormSum_bound_of_generator_bound K hJ m χ hχJ hgen
88   apply IsBigO.of_bound M
89   filter_upwards [eventually_ge_atTop (1 : ℝ)] with X hX
90   rw [Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _)]
91   exact hM X hX
92 
93 end PaperX.IdealNormWeighted

Back to source controls