NormResidueMellinPole.lean

1 import PaperX.NormResidueMellinAttachment
2 import PaperX.RealAxisMellinPole
3 
4 /-! Pole-rigidity assembly for the actual ideal norm-character Mellin factors.
5 
6 The arithmetic Euler-product identity and the two nonzero residue limits remain
7 explicit hypotheses.  The endpoint regularity of every norm-character factor is
8 proved from the scalar-unit counting criteria. -/
9 
10 set_option autoImplicit false
11 noncomputable section
12 
13 open Ideal NumberField Filter Asymptotics
14 open scoped nonZeroDivisors Classical Topology BigOperators
15 
16 namespace PaperX.NormResidueLattice
17 
18 variable (K : Type*) [Field K] [NumberField K]
19 
20 /-- Once the arithmetic product identity and its nonzero simple-pole residues
21 are supplied, the checked norm-character power savings force the exponent to be
22 one and every endpoint Mellin value to be nonzero. -/
23 theorem normCharacter_pole_criterion_of_scalar_units
24     {ι : Type*} [Fintype ι]
25     (C : ι → ClassGroup (𝓞 K))
26     (J : ι → (Ideal (𝓞 K))⁰)
27     (m : ι → ℕ)
28     (χ : ∀ i, ZMod (m i) →*₀ ℂ)
29     (hJ : ∀ i, ClassGroup.mk0 (J i) = (C i)⁻¹)
30     (hm : ∀ i, m i ≠ 0)
31     (hχ : ∀ i, (χ i).toMonoidHom.comp (Units.coeHom (ZMod (m i))) ≠ 1)
32     (hdeg : ∀ i, (Module.finrank ℚ K).Coprime (m i).totient)
33     (hJcop : ∀ i, (absNorm ((J i : (Ideal (𝓞 K))⁰) : Ideal (𝓞 K))).Coprime (m i))
34     (p Z : ℝ → ℂ) (P Q : ℂ) (d : ℕ)
35     (hp : Tendsto (fun h : ℝ => (h : ℂ) * p h) (𝓝[>] 0) (𝓝 P))
36     (hP : P ≠ 0)
37     (hZ : Tendsto (fun h : ℝ => (h : ℂ) * Z h) (𝓝[>] 0) (𝓝 Q))
38     (hQ : Q ≠ 0)
39     (hid : Z =ᶠ[𝓝[>] 0] fun h =>
40       (p h * ∏ i, normCharacterMellin K (C i) (m i) (χ i) h) ^ d) :
41     d = 1 ∧ ∀ i, normCharacterMellin K (C i) (m i) (χ i) 0 ≠ 0 := by
42   apply PaperX.RealAxisPoleRigidity.right_endpoint_index_one_and_factors_nonzero
43     p Z (fun i => normCharacterMellin K (C i) (m i) (χ i)) P Q d
44     hp hP hZ hQ _ hid
45   intro i
46   exact PaperX.RealAxisMellinPole.isBigO_complex_scale_iff.mpr
47     (normCharacterMellin_sub_isBigO_of_scalar_units K
48       (hJ i) (m i) (hm i) (χ i) (hχ i) (hdeg i) (hJcop i))
49 
50 end PaperX.NormResidueLattice

Back to source controls