IdealClassCharacterBound.lean

1 import PaperX.IdealClassCharacterSum
2 
3 /-!
4 # Power saving for actual ordinary class character sums
5 
6 The common leading coefficient in the actual ideal-class asymptotic cancels for
7 weights of total sum zero. Nontrivial ordinary ideal-class characters satisfy this
8 condition by finite-group character orthogonality, proved in the preceding file.
9 These are not characters of an additional norm-residue or ray-class quotient.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 
14 open Ideal NumberField Filter Asymptotics
15 open scoped nonZeroDivisors Classical BigOperators
16 
17 namespace PaperX.IdealClassCharacter
18 
19 open PaperX.IdealClassQuantitative
20 
21 variable (K : Type*) [Field K] [NumberField K]
22 
23 /-- The actual number-field counting exponent is strictly below one. -/
24 theorem countExponent_lt_one : countExponent K < 1 := by
25   apply sub_lt_self
26   apply inv_pos.mpr
27   exact_mod_cast Module.finrank_pos (R := ℚ) (M := K)
28 
29 /-- Zero total weight cancels the common leading term exactly. -/
30 theorem weightedSum_eq_sum_errors (w : ClassGroup (𝓞 K) → ℂ)
31     (hw : ∑ C, w C = 0) (X : ℝ) :
32     weightedSum K w X = ∑ C, w C *
33       (((classCount K C X : ℝ) - classResidue K * X : ℝ) : ℂ) := by
34   rw [weightedSum_eq_sum_classCount]
35   simp only [Complex.ofReal_sub, Complex.ofReal_natCast, mul_sub, Finset.sum_sub_distrib]
36   rw [← Finset.sum_mul, hw, zero_mul, sub_zero]
37 
38 /-- Every zero-sum family of class weights has a power-saving bound at all `X ≥ 1`. -/
39 theorem exists_weightedSum_bound (w : ClassGroup (𝓞 K) → ℂ)
40     (hw : ∑ C, w C = 0) :
41     ∃ M : ℝ, 0 ≤ M ∧ ∀ X : ℝ, 1 ≤ X →
42       ‖weightedSum K w X‖ ≤ M * X ^ countExponent K := by
43   choose M hM0 hM using exists_classCount_bound K
44   refine ⟨∑ C, ‖w C‖ * M C, Finset.sum_nonneg (fun C _ =>
45     mul_nonneg (norm_nonneg _) (hM0 C)), ?_⟩
46   intro X hX
47   rw [weightedSum_eq_sum_errors K w hw]
48   calc
49     _ ≤ ∑ C, ‖w C *
50         (((classCount K C X : ℝ) - classResidue K * X : ℝ) : ℂ)‖ :=
51       norm_sum_le _ _
52     _ ≤ ∑ C, (‖w C‖ * M C) * X ^ countExponent K := by
53       apply Finset.sum_le_sum
54       intro C _
55       rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, mul_assoc]
56       exact mul_le_mul_of_nonneg_left (hM C X hX) (norm_nonneg _)
57     _ = _ := (Finset.sum_mul _ _ _).symm
58 
59 /-- The actual ideal sum of a nontrivial ordinary class character has a power saving. -/
60 theorem exists_characterSum_bound (χ : ClassGroup (𝓞 K) →* ℂ) (hχ : χ ≠ 1) :
61     ∃ M : ℝ, 0 ≤ M ∧ ∀ X : ℝ, 1 ≤ X →
62       ‖weightedSum K χ X‖ ≤ M * X ^ countExponent K :=
63   exists_weightedSum_bound K χ (sum_character_eq_zero χ hχ)
64 
65 /-- Asymptotic form of the uniform bound for zero-sum class weights. -/
66 theorem weightedSum_isBigO (w : ClassGroup (𝓞 K) → ℂ)
67     (hw : ∑ C, w C = 0) :
68     weightedSum K w =O[atTop] (fun X : ℝ => X ^ countExponent K) := by
69   obtain ⟨M, _, hM⟩ := exists_weightedSum_bound K w hw
70   apply IsBigO.of_bound M
71   filter_upwards [eventually_ge_atTop (1 : ℝ)] with X hX
72   rw [Real.norm_eq_abs, abs_of_nonneg (Real.rpow_nonneg (by linarith) _)]
73   exact hM X hX
74 
75 /-- Asymptotic power saving for each actual nontrivial ordinary ideal-class character. -/
76 theorem characterSum_isBigO (χ : ClassGroup (𝓞 K) →* ℂ) (hχ : χ ≠ 1) :
77     weightedSum K χ =O[atTop] (fun X : ℝ => X ^ countExponent K) :=
78   weightedSum_isBigO K χ (sum_character_eq_zero χ hχ)
79 
80 end PaperX.IdealClassCharacter

Back to source controls