Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.differentiableOn_divisorCanonicalProduct_div_pow_sub

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorQuotientRemovable.lean:57 to 73

Mathematical statement

Exact Lean statement

theorem differentiableOn_divisorCanonicalProduct_div_pow_sub
    (m : ℕ) (f : ℂ → ℂ) (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>
      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))
    (z₀ : ℂ) (k : ℕ) : DifferentiableOn ℂ
      (fun z : ℂ => (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) / (z - z₀) ^ k)
      ((Set.univ : Set ℂ) \ {z₀})

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem differentiableOn_divisorCanonicalProduct_div_pow_sub    (m : ℕ) (f : ℂ → ℂ) (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (z₀ : ℂ) (k : ℕ) : DifferentiableOn ℂ      (fun z : ℂ => (divisorCanonicalProduct m f (Set.univ : Set ℂ) z) / (z - z₀) ^ k)      ((Set.univ : Set ℂ) \ {z₀}) := by  have hopen : IsOpen ((Set.univ : Set ℂ) \ {z₀}) := by    have hset : ((Set.univ : Set ℂ) \ {z₀}) = ({z₀} : Set ℂ)ᶜ := by      ext z; simp    simp [hset]  have hconv :=    tendstoLocallyUniformlyOn_divisorPartialProduct_div_pow_sub      (m := m) (f := f) h_sum (z₀ := z₀) (k := k)  refine hconv.differentiableOn ?_ hopen  refine Filter.Eventually.of_forall ?_  intro s  exact differentiableOn_divisorPartialProduct_div_pow_sub (m := m) (f := f) (z₀ := z₀) (k := k) s