NormResidueCharacterCounting.lean

1 import PaperX.NormResidueGeneratorAttachment
2 import PaperX.NormResidueGeneratorSum
3 import PaperX.NormResidueUnitCounting
4 import PaperX.IdealNormCharacterBound
5 
6 /-! Arithmetic norm-character cancellation from a residue-unit witness.
7 The cone estimate, both sign means, and the exact generator/ideal comparison
8 are proved dependencies; the displayed arithmetic hypotheses remain supplied. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.NormResidueLattice
12 open Ideal NumberField
13 open PaperX.IdealClassQuantitative PaperX.ResidueLattice PaperX.NormResidue
14 open PaperX.IdealNormWeighted PaperX.IdealResidueUnitAction
15 open scoped nonZeroDivisors Classical Pointwise Real
16 
17 variable (K : Type*) [Field K] [NumberField K]
18 
19 /-- The finite residue computation equals the actual bounded generator sum. -/
20 theorem normWeightedCount_eq_boundedGeneratorSum (M J : (Ideal (𝓞 K))⁰) (m : ℕ)
21     (hM : (M : Ideal (𝓞 K)) ≤ modulusIdeal (𝓞 K) m)
22     [Fintype (IdealResidues K M J)] (χ : ZMod m → ℂ) {t : ℝ} (ht : 0 < t) :
23     normWeightedCount K M J m hM χ t =
24       boundedGeneratorSum K J (fun n => χ (n : ZMod m)) (t ^ Module.finrank ℚ K) := by
25   rw [normWeightedCount_eq_generatorPointSum K M J m hM χ ht]
26   exact latticeGeneratorSum_eq_boundedGeneratorSum K J (fun n => χ (n : ZMod m)) ht
27 
28 /-- The canonical modulus count is independent of its chosen finite enumeration. -/
29 theorem modulusNormWeightedCount_eq_boundedGeneratorSum (J : (Ideal (𝓞 K))⁰)
30     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m → ℂ) {t : ℝ} (ht : 0 < t) :
31     modulusNormWeightedCount K J m hm χ t =
32       boundedGeneratorSum K J (fun n => χ (n : ZMod m)) (t ^ Module.finrank ℚ K) := by
33   let := Fintype.ofFinite (IdealResidues K (modulusTimesIdeal K J m hm) J)
34   unfold modulusNormWeightedCount
35   exact normWeightedCount_eq_boundedGeneratorSum K _ J m _ χ ht
36 
37 /-- The unit witness gives a power-saving estimate on actual algebraic generators,
38 with all finite-mean and geometric estimates discharged. -/
39 theorem exists_boundedGeneratorSum_bound_of_unit (J : (Ideal (𝓞 K))⁰)
40     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →* ℂ)
41     (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ)
42     (hu : χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1) :
43     ∃ B : ℝ, 0 ≤ B ∧ ∀ Y : ℝ, 1 ≤ Y →
44       ‖boundedGeneratorSum K J (fun n => χ (n : ZMod m)) Y‖ ≤
45         B * (Y ^ countExponent K + 1) := by
46   obtain ⟨B, hB0, hB⟩ := exists_modulusNormWeightedCount_bound K J m hm χ u hu
47   refine ⟨B, hB0, fun Y hY => ?_⟩
48   have hY0 : 0 < Y := lt_of_lt_of_le zero_lt_one hY
49   have hd : Module.finrank ℚ K ≠ 0 := (Module.finrank_pos (R := ℚ) (M := K)).ne'
50   have ht : 1 ≤ Y ^ (Module.finrank ℚ K : ℝ)⁻¹ :=
51     Real.one_le_rpow hY (by positivity)
52   have H := hB (Y ^ (Module.finrank ℚ K : ℝ)⁻¹) ht
53   rw [modulusNormWeightedCount_eq_boundedGeneratorSum K J m hm χ
54       (Real.rpow_pos_of_pos hY0 _),
55     Real.rpow_inv_natCast_pow hY0.le hd, root_boundary_power K Y hY0.le] at H
56   exact H
57 
58 /-- Actual ideal norm-character sums in a class have power-saving cancellation
59 under a residue-unit witness and nonvanishing on the inverse-class representative. -/
60 theorem exists_classNormSum_bound_of_unit {C : ClassGroup (𝓞 K)}
61     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹)
62     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
63     (u : (𝓞 K ⧸ modulusIdeal (𝓞 K) m)ˣ)
64     (hu : χ (integerQuotientNorm K m (u : 𝓞 K ⧸ modulusIdeal (𝓞 K) m)) ≠ 1)
65     (hχJ : χ (absNorm (J : Ideal (𝓞 K)) : ZMod m) ≠ 0) :
66     ∃ B : ℝ, 0 ≤ B ∧ ∀ X : ℝ, 1 ≤ X →
67       ‖classNormSum K C (fun n => χ (n : ZMod m)) X‖ ≤
68         B * X ^ countExponent K :=
69   exists_classNormSum_bound_of_generator_bound K hJ m χ hχJ
70     (exists_boundedGeneratorSum_bound_of_unit K J m hm χ.toMonoidHom u hu)
71 
72 end PaperX.NormResidueLattice

Back to source controls