NormResidueScalarCounting.lean

1 import PaperX.NormResidueScalarWitness
2 import PaperX.NormResidueCharacterCounting
3 
4 /-! Scalar-unit criteria discharge the two explicit arithmetic hypotheses in the
5 norm-character counting theorem: the residue-unit witness and nonvanishing on
6 the chosen inverse-class representative. -/
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 open Ideal NumberField
12 open scoped nonZeroDivisors NumberField
13 
14 namespace PaperX.NormResidue
15 
16 /-- A multiplicative character is nonzero on every integer residue coprime to
17 its modulus. -/
18 theorem character_natCast_ne_zero_of_coprime (m n : ℕ) (χ : ZMod m →*₀ ℂ)
19     (h : n.Coprime m) :
20     χ (n : ZMod m) ≠ 0 := by
21   exact (((ZMod.isUnit_iff_coprime n m).2 h).map χ.toMonoidHom).ne_zero
22 
23 end PaperX.NormResidue
24 
25 namespace PaperX.NormResidueLattice
26 
27 open PaperX.NormResidue
28 open PaperX.IdealClassQuantitative PaperX.IdealNormWeighted
29 
30 variable (K : Type*) [Field K] [NumberField K]
31 
32 /-- If the norm character is already nontrivial on scalar residue units, the
33 field degree is coprime to the unit-group order, and the inverse-class
34 representative has norm coprime to the modulus, then the actual ideal
35 norm-character sum has the Paper X power-saving bound with no supplied quotient
36 unit witness and no supplied nonvanishing value. -/
37 theorem exists_classNormSum_bound_of_scalar_units {C : ClassGroup (𝓞 K)}
38     {J : (Ideal (𝓞 K))⁰} (hJ : ClassGroup.mk0 J = C⁻¹)
39     (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
40     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
41     (hdeg : (Module.finrank ℚ K).Coprime m.totient)
42     (hJcop : (absNorm (J : Ideal (𝓞 K))).Coprime m) :
43     ∃ B : ℝ, 0 ≤ B ∧ ∀ X : ℝ, 1 ≤ X →
44       ‖classNormSum K C (fun n => χ (n : ZMod m)) X‖ ≤
45         B * X ^ countExponent K := by
46   obtain ⟨u, hu⟩ :=
47     exists_scalarResidueUnit_witness_of_restricted_nontrivial K m hm χ hχ hdeg
48   exact exists_classNormSum_bound_of_unit K hJ m hm χ u hu
49     (character_natCast_ne_zero_of_coprime m (absNorm (J : Ideal (𝓞 K))) χ hJcop)
50 
51 end PaperX.NormResidueLattice

Back to source controls