NormResidueMellinAttachment.lean

1 import PaperX.NormResidueScalarCounting
2 import PaperX.IdealClassCharacterBound
3 import PaperX.IdealNormCharacterMellin
4 
5 /-! Real-axis Mellin control for the actual ideal norm-character sum under the
6 checked scalar-unit arithmetic criteria. -/
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 open Ideal NumberField MeasureTheory Filter Set Asymptotics
12 open scoped nonZeroDivisors Classical Topology
13 
14 namespace PaperX.NormResidueLattice
15 
16 open PaperX.NormResidue
17 open PaperX.IdealClassQuantitative PaperX.IdealNormWeighted
18 open PaperX.RealAxisMellinMoment
19 
20 variable (K : Type*) [Field K] [NumberField K]
21 
22 /-- Actual norm-character Mellin factor attached to one ordinary ideal class. -/
23 def normCharacterMellin (C : ClassGroup (𝓞 K)) (m : ℕ)
24     (χ : ZMod m →*₀ ℂ) (h : ℝ) : ℂ :=
25   normMellin K C (fun n => χ (n : ZMod m)) h
26 
27 /-- The scalar-unit arithmetic criteria imply the logarithmic first moment for
28 the actual ideal norm-character sum. -/
29 theorem integrable_normCharacter_logMoment_of_scalar_units
30     {C : ClassGroup (𝓞 K)} {J : (Ideal (𝓞 K))⁰}
31     (hJ : ClassGroup.mk0 J = C⁻¹) (m : ℕ) (hm : m ≠ 0)
32     (χ : ZMod m →*₀ ℂ)
33     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
34     (hdeg : (Module.finrank ℚ K).Coprime m.totient)
35     (hJcop : (absNorm (J : Ideal (𝓞 K))).Coprime m) :
36     Integrable (fun x : ℝ =>
37       (1 + Real.log x) *
38         ‖(x ^ (-2 : ℝ)) • classNormSum K C (fun n => χ (n : ZMod m)) x‖)
39       (volume.restrict (Ioi 1)) := by
40   obtain ⟨B, _, hB⟩ :=
41     exists_classNormSum_bound_of_scalar_units K hJ m hm χ hχ hdeg hJcop
42   exact integrable_weighted_moment_of_power_bound
43     (measurable_classNormSum K C (fun n => χ (n : ZMod m))).aestronglyMeasurable
44     (PaperX.IdealClassCharacter.countExponent_lt_one K) (fun x hx => hB x hx.le)
45 
46 /-- The actual norm-character Mellin factor has first-order right-endpoint
47 variation. This is the analytic input used by the pole-rigidity assembly. -/
48 theorem normCharacterMellin_sub_isBigO_of_scalar_units
49     {C : ClassGroup (𝓞 K)} {J : (Ideal (𝓞 K))⁰}
50     (hJ : ClassGroup.mk0 J = C⁻¹) (m : ℕ) (hm : m ≠ 0)
51     (χ : ZMod m →*₀ ℂ)
52     (hχ : χ.toMonoidHom.comp (Units.coeHom (ZMod m)) ≠ 1)
53     (hdeg : (Module.finrank ℚ K).Coprime m.totient)
54     (hJcop : (absNorm (J : Ideal (𝓞 K))).Coprime m) :
55     (fun h => normCharacterMellin K C m χ h - normCharacterMellin K C m χ 0)
56       =O[𝓝[>] (0 : ℝ)] (fun h : ℝ => h) := by
57   obtain ⟨B, _, hB⟩ :=
58     exists_classNormSum_bound_of_scalar_units K hJ m hm χ hχ hdeg hJcop
59   exact mellinIntegral_sub_isBigO_of_power_bound
60     (measurable_classNormSum K C (fun n => χ (n : ZMod m))).aestronglyMeasurable
61     (PaperX.IdealClassCharacter.countExponent_lt_one K) (fun x hx => hB x hx.le)
62 
63 end PaperX.NormResidueLattice

Back to source controls