Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.differentiableOn_divisorComplementCanonicalProduct_univ

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorComplement.lean:355 to 377

Mathematical statement

Exact Lean statement

theorem differentiableOn_divisorComplementCanonicalProduct_univ
    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ)
    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>
      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :
    DifferentiableOn ℂ (divisorComplementCanonicalProduct m f z₀) (Set.univ : Set ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem differentiableOn_divisorComplementCanonicalProduct_univ    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    DifferentiableOn ℂ (divisorComplementCanonicalProduct m f z₀) (Set.univ : Set ℂ) := by  have hloc :      TendstoLocallyUniformlyOn        (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) =>          divisorComplementPartialProduct m f z₀ s)        (divisorComplementCanonicalProduct m f z₀)        Filter.atTop        (Set.univ : Set ℂ) :=    tendstoLocallyUniformlyOn_divisorComplementPartialProduct_univ (m := m) (f := f)      (z₀ := z₀) h_sum  have hF :      ∀ᶠ s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) in Filter.atTop,        DifferentiableOn ℂ (divisorComplementPartialProduct m f z₀ s) (Set.univ : Set ℂ) := by    refine Filter.Eventually.of_forall ?_    intro s    exact (differentiable_divisorComplementPartialProduct m f z₀ s).differentiableOn  haveI : (Filter.atTop : Filter (Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)))).NeBot :=    Filter.atTop_neBot  exact hloc.differentiableOn hF isOpen_univ