Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.differentiable_divisorCanonicalProduct_univ

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization.lean:78 to 86

Mathematical statement

Exact Lean statement

theorem differentiable_divisorCanonicalProduct_univ (m : ℕ) (f : ℂ → ℂ)
    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>
      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :
    Differentiable ℂ (divisorCanonicalProduct m f (Set.univ : Set ℂ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem differentiable_divisorCanonicalProduct_univ (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    Differentiable ℂ (divisorCanonicalProduct m f (Set.univ : Set ℂ)) := by  intro z  have hdiffOn :      DifferentiableOn ℂ (divisorCanonicalProduct m f (Set.univ : Set ℂ)) (Set.univ : Set ℂ) :=    differentiableOn_divisorCanonicalProduct_univ (m := m) (f := f) h_sum  exact (hdiffOn z (by simp)).differentiableAt (by simp)