CyclotomicPoleRigidity.lean

1 import Mathlib.Analysis.Meromorphic.Order
2 import Mathlib.Tactic
3 
4 /-! The local pole argument needed for a cyclotomic Euler-product proof.
5 These are actual analytic/meromorphic functions. No arithmetic L-function
6 attachment, Euler product, or analytic continuation is asserted here. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.CyclotomicPoleRigidity
10 open Filter
11 open scoped Topology
12 
13 /-- A natural power of a meromorphic function can have a simple pole only
14 when the exponent is one. -/
15 theorem exponent_one_of_simple_pole {f : ℂ → ℂ} {z : ℂ} {d : ℕ}
16     (hf : MeromorphicAt f z)
17     (hp : meromorphicOrderAt (fun w => f w ^ d) z = (-1 : WithTop ℤ)) :
18     d = 1 := by
19   rw [show (fun w => f w ^ d) = f ^ d from rfl, meromorphicOrderAt_pow hf] at hp
20   have hi := congrArg (fun a : WithTop ℤ => a.untopD 0) hp
21   simp only [WithTop.untopD_zero_mul] at hi
22   change (d : ℤ) * (meromorphicOrderAt f z).untopD 0 = -1 at hi
23   have hd : (0 : ℤ) ≤ d := Nat.cast_nonneg d
24   have hm : (meromorphicOrderAt f z).untopD 0 < 0 := by
25     by_contra h
26     have := mul_nonneg hd (le_of_not_gt h)
27     omega
28   have he : (d : ℤ) = 1 := by nlinarith
29   exact_mod_cast he
30 
31 /-- Multiplication by an analytic factor preserves a supplied simple pole
32 only if that factor is nonzero at the point. -/
33 theorem analytic_factor_nonzero_of_simple_pole {p a : ℂ → ℂ} {z : ℂ}
34     (hp : MeromorphicAt p z) (ha : AnalyticAt ℂ a z)
35     (hpo : meromorphicOrderAt p z = (-1 : WithTop ℤ))
36     (hprod : meromorphicOrderAt (fun w => p w * a w) z = (-1 : WithTop ℤ)) :
37     a z ≠ 0 := by
38   rw [show (fun w => p w * a w) = p * a from rfl,
39     meromorphicOrderAt_mul hp ha.meromorphicAt, hpo] at hprod
40   change ((-1 : ℤ) : WithTop ℤ) + meromorphicOrderAt a z =
41     ((-1 : ℤ) : WithTop ℤ) at hprod
42   have hao : meromorphicOrderAt a z = 0 := by
43     cases h : meromorphicOrderAt a z with
44     | top =>
45       simp only [h, add_top] at hprod
46       exact False.elim (WithTop.top_ne_coe hprod)
47     | coe k =>
48       rw [h] at hprod
49       have hk : (-1 : ℤ) + k = -1 := by exact_mod_cast hprod
50       have hk0 : k = 0 := by omega
51       simp [hk0]
52   obtain ⟨c, hc, hl⟩ := tendsto_ne_zero_of_meromorphicOrderAt_eq_zero
53     ha.meromorphicAt hao
54   have he : a z = c := tendsto_nhds_unique
55     ha.continuousAt.continuousWithinAt.tendsto hl
56   simpa [he] using hc
57 
58 /-- A finite analytic Euler-factor family cannot cancel a simple pole when
59 the entire product, raised to an unknown natural index, again has a simple pole.
60 The index and all nonvanishing conclusions are derived. -/
61 theorem index_one_and_factors_nonzero {ι : Type*} [Fintype ι]
62     (p : ℂ → ℂ) (a : ι → ℂ → ℂ) (z : ℂ) (d : ℕ)
63     (hp : MeromorphicAt p z) (ha : ∀ i, AnalyticAt ℂ (a i) z)
64     (hpo : meromorphicOrderAt p z = (-1 : WithTop ℤ))
65     (hwhole : meromorphicOrderAt
66       (fun w => (p w * ∏ i, a i w) ^ d) z = (-1 : WithTop ℤ)) :
67     d = 1 ∧ ∀ i, a i z ≠ 0 := by
68   classical
69   have hA : AnalyticAt ℂ (fun w => ∏ i, a i w) z :=
70     by fun_prop
71   have hd := exponent_one_of_simple_pole (hp.mul hA.meromorphicAt) hwhole
72   refine ⟨hd, ?_⟩
73   have hprod : meromorphicOrderAt (fun w => p w * ∏ i, a i w) z =
74       (-1 : WithTop ℤ) := by simpa [hd] using hwhole
75   have hn := analytic_factor_nonzero_of_simple_pole hp hA hpo hprod
76   exact fun i => (Finset.prod_ne_zero_iff.mp hn) i (Finset.mem_univ i)
77 
78 /-- The criterion accepts a punctured-neighborhood product identity with a
79 second supplied meromorphic function of simple-pole order. -/
80 theorem index_one_and_factors_nonzero_of_identity {ι : Type*} [Fintype ι]
81     (p Z : ℂ → ℂ) (a : ι → ℂ → ℂ) (z : ℂ) (d : ℕ)
82     (hp : MeromorphicAt p z) (ha : ∀ i, AnalyticAt ℂ (a i) z)
83     (hpo : meromorphicOrderAt p z = (-1 : WithTop ℤ))
84     (hZo : meromorphicOrderAt Z z = (-1 : WithTop ℤ))
85     (hidentity : Z =ᶠ[𝓝[≠] z] fun w => (p w * ∏ i, a i w) ^ d) :
86     d = 1 ∧ ∀ i, a i z ≠ 0 := by
87   apply index_one_and_factors_nonzero p a z d hp ha hpo
88   rw [← meromorphicOrderAt_congr hidentity]
89   exact hZo
90 
91 end PaperX.CyclotomicPoleRigidity

Back to source controls