NormResidueAutomaticCounting.lean

1 import PaperX.NormResidueCoprimeRepresentative
2 import PaperX.NormResidueMellinAttachment
3 
4 /-!
5 # Automatic representative selection for norm-character counting
6 
7 The coprime inverse-class representative is now constructed internally, so the
8 public counting and Mellin interfaces require only the scalar character
9 criterion and the degree--totient coprimality condition.
10 -/
11 
12 set_option autoImplicit false
13 noncomputable section
14 
15 open Ideal NumberField MeasureTheory Filter Set Asymptotics
16 open scoped NumberField nonZeroDivisors Classical Topology
17 
18 namespace PaperX.NormResidueLattice
19 
20 open PaperX.NormResidue
21 open PaperX.IdealClassQuantitative PaperX.IdealNormWeighted
22 open PaperX.RealAxisMellinMoment
23 
24 variable (K : Type*) [Field K] [NumberField K]
25 
26 /-- Automatic-representative form of the Paper X norm-character power saving. -/
27 theorem exists_classNormSum_bound_of_scalar_units_autoRep
28     (C : ClassGroup (𝓞 K)) (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
29     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
30     (hdeg : (Module.finrank ℚ K).Coprime m.totient) :
31     ∃ B : ℝ, 0 ≤ B ∧ ∀ X : ℝ, 1 ≤ X →
32       ‖classNormSum K C (fun n => χ (n : ZMod m)) X‖ ≤
33         B * X ^ countExponent K := by
34   obtain ⟨J, hJ, hJcop⟩ :=
35     exists_coprime_inverse_class_representative K C m hm
36   exact exists_classNormSum_bound_of_scalar_units K hJ m hm χ hχ hdeg hJcop
37 
38 /-- Automatic-representative logarithmic first-moment bound. -/
39 theorem integrable_normCharacter_logMoment_of_scalar_units_autoRep
40     (C : ClassGroup (𝓞 K)) (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
41     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
42     (hdeg : (Module.finrank ℚ K).Coprime m.totient) :
43     Integrable (fun x : ℝ =>
44       (1 + Real.log x) *
45         ‖(x ^ (-2 : ℝ)) • classNormSum K C (fun n => χ (n : ZMod m)) x‖)
46       (volume.restrict (Ioi 1)) := by
47   obtain ⟨J, hJ, hJcop⟩ :=
48     exists_coprime_inverse_class_representative K C m hm
49   exact integrable_normCharacter_logMoment_of_scalar_units K hJ m hm χ hχ hdeg hJcop
50 
51 /-- Automatic-representative first-order endpoint variation of the actual
52 norm-character Mellin factor. -/
53 theorem normCharacterMellin_sub_isBigO_of_scalar_units_autoRep
54     (C : ClassGroup (𝓞 K)) (m : ℕ) (hm : m ≠ 0) (χ : ZMod m →*₀ ℂ)
55     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
56     (hdeg : (Module.finrank ℚ K).Coprime m.totient) :
57     (fun h => normCharacterMellin K C m χ h - normCharacterMellin K C m χ 0)
58       =O[𝓝[>] (0 : ℝ)] (fun h : ℝ => h) := by
59   obtain ⟨J, hJ, hJcop⟩ :=
60     exists_coprime_inverse_class_representative K C m hm
61   exact normCharacterMellin_sub_isBigO_of_scalar_units K hJ m hm χ hχ hdeg hJcop
62 
63 end PaperX.NormResidueLattice

Back to source controls