IdealCharacterMellinPole.lean

1 import PaperX.IdealCharacterMellin
2 import PaperX.RealAxisMellinPole
3 
4 /-! The pole criterion now uses actual ordinary class-character ideal sums.
5 Their growth and endpoint regularity are theorems. Residues and the arithmetic
6 product identity remain explicit inputs; this is not an Euler-product proof. -/
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 open NumberField Filter Asymptotics
12 open scoped Topology BigOperators
13 
14 namespace PaperX.IdealClassCharacter
15 
16 variable (K : Type*) [Field K] [NumberField K]
17 
18 /-- For actual ordinary class characters, only the pole residues and product
19 identity remain to apply the real-axis nonvanishing and index-one argument. -/
20 theorem classCharacter_pole_criterion {ι : Type*} [Fintype ι]
21     (χ : ι → ClassGroup (𝓞 K) →* ℂ) (hχ : ∀ i, χ i ≠ 1)
22     (p Z : ℝ → ℂ) (P Q : ℂ) (d : ℕ)
23     (hp : Tendsto (fun h : ℝ => (h : ℂ) * p h) (𝓝[>] 0) (𝓝 P)) (hP : P ≠ 0)
24     (hZ : Tendsto (fun h : ℝ => (h : ℂ) * Z h) (𝓝[>] 0) (𝓝 Q)) (hQ : Q ≠ 0)
25     (hid : Z =ᶠ[𝓝[>] 0] fun h => (p h * ∏ i, classMellin K (χ i) h) ^ d) :
26     d = 1 ∧ ∀ i, classMellin K (χ i) 0 ≠ 0 := by
27   apply PaperX.RealAxisPoleRigidity.right_endpoint_index_one_and_factors_nonzero
28     p Z (fun i => classMellin K (χ i)) P Q d hp hP hZ hQ _ hid
29   intro i
30   exact PaperX.RealAxisMellinPole.isBigO_complex_scale_iff.mpr
31     (characterMellin_sub_isBigO K (χ i) (hχ i))
32 
33 end PaperX.IdealClassCharacter

Back to source controls