Source indexedtheorem · leanprover/lean4:v4.32.0

logDeriv_hasSimplePolesOn_of_meromorphicOrderAt_ne_top

PrimeNumberTheoremAnd.RectangleArgumentPrinciple · PrimeNumberTheoremAnd/RectangleArgumentPrinciple.lean:194 to 210

Mathematical statement

Exact Lean statement

theorem logDeriv_hasSimplePolesOn_of_meromorphicOrderAt_ne_top
    {f : ℂ → ℂ} {R : Set ℂ}
    (hf : MeromorphicOn f R) (hlog : MeromorphicOn (logDeriv f) R)
    (hfinite_order : ∀ p ∈ R, meromorphicOrderAt f p ≠ ⊤) :
    HasSimplePolesOn (logDeriv f) R

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem logDeriv_hasSimplePolesOn_of_meromorphicOrderAt_ne_top    {f : ℂ → ℂ} {R : Set ℂ}    (hf : MeromorphicOn f R) (hlog : MeromorphicOn (logDeriv f) R)    (hfinite_order : ∀ p ∈ R, meromorphicOrderAt f p ≠ ⊤) :    HasSimplePolesOn (logDeriv f) R := by  intro p hpR  obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp (hfinite_order p hpR)  by_cases hn0 : n = 0  · have hord0 : meromorphicOrderAt f p = (0 : WithTop ℤ) := by      simpa [hn0] using hn.symm    have hnonneg :=      logDeriv_meromorphicOrderAt_nonneg_of_order_zero (hf p hpR) (hlog p hpR) hord0    exact le_trans (WithTop.coe_le_coe.2 (by norm_num : (-1 : ℤ) ≤ 0)) hnonneg  · have hneg_one :=      logDeriv_meromorphicOrderAt_eq_neg_one_of_order_ne_zero (hf p hpR) (hlog p hpR)        hn.symm hn0    rw [hneg_one]