NormResidueAutomaticPole.lean

1 import PaperX.NormResidueAutomaticCounting
2 import PaperX.RealAxisMellinPole
3 
4 /-!
5 # Automatic-representative pole-rigidity assembly
6 
7 The ideal-class representative is constructed internally for each character.
8 Thus the pole-rigidity theorem exposes only the scalar-unit arithmetic
9 criterion, degree--totient coprimality, and the genuinely external arithmetic
10 Euler-product data.
11 -/
12 
13 set_option autoImplicit false
14 noncomputable section
15 
16 open Ideal NumberField Filter Asymptotics
17 open scoped NumberField nonZeroDivisors Classical Topology BigOperators
18 
19 namespace PaperX.NormResidueLattice
20 
21 variable (K : Type*) [Field K] [NumberField K]
22 
23 /-- Pole rigidity with automatic coprime inverse-class representatives. -/
24 theorem normCharacter_pole_criterion_of_scalar_units_autoRep
25     {ι : Type*} [Fintype ι]
26     (C : ι → ClassGroup (𝓞 K))
27     (m : ι → ℕ)
28     (χ : ∀ i, ZMod (m i) →*₀ ℂ)
29     (hm : ∀ i, m i ≠ 0)
30     (hχ : ∀ i, (χ i).toMonoidHom.comp (Units.coeHom (ZMod (m i))) ≠ 1)
31     (hdeg : ∀ i, (Module.finrank ℚ K).Coprime (m i).totient)
32     (p Z : ℝ → ℂ) (P Q : ℂ) (d : ℕ)
33     (hp : Tendsto (fun h : ℝ => (h : ℂ) * p h) (𝓝[>] 0) (𝓝 P))
34     (hP : P ≠ 0)
35     (hZ : Tendsto (fun h : ℝ => (h : ℂ) * Z h) (𝓝[>] 0) (𝓝 Q))
36     (hQ : Q ≠ 0)
37     (hid : Z =ᶠ[𝓝[>] 0] fun h =>
38       (p h * ∏ i, normCharacterMellin K (C i) (m i) (χ i) h) ^ d) :
39     d = 1 ∧ ∀ i, normCharacterMellin K (C i) (m i) (χ i) 0 ≠ 0 := by
40   apply PaperX.RealAxisPoleRigidity.right_endpoint_index_one_and_factors_nonzero
41     p Z (fun i => normCharacterMellin K (C i) (m i) (χ i)) P Q d
42     hp hP hZ hQ _ hid
43   intro i
44   exact PaperX.RealAxisMellinPole.isBigO_complex_scale_iff.mpr
45     (normCharacterMellin_sub_isBigO_of_scalar_units_autoRep K
46       (C i) (m i) (hm i) (χ i) (hχ i) (hdeg i))
47 
48 end PaperX.NormResidueLattice

Back to source controls