Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.tendstoLocallyUniformlyOn_divisorPartialProduct_univ

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorQuotientConvergence.lean:27 to 43

Mathematical statement

Exact Lean statement

theorem tendstoLocallyUniformlyOn_divisorPartialProduct_univ
    (m : ℕ) (f : ℂ → ℂ)
    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>
      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :
    TendstoLocallyUniformlyOn
      (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) => divisorPartialProduct m f s)
      (divisorCanonicalProduct m f (Set.univ : Set ℂ))
      Filter.atTop
      (Set.univ : Set ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem tendstoLocallyUniformlyOn_divisorPartialProduct_univ    (m : ℕ) (f : ℂ → ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    TendstoLocallyUniformlyOn      (fun s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) => divisorPartialProduct m f s)      (divisorCanonicalProduct m f (Set.univ : Set ℂ))      Filter.atTop      (Set.univ : Set ℂ) := by  have hprod :      HasProdLocallyUniformlyOn        (fun (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) (z : ℂ) =>          weierstrassFactor m (z / divisorZeroIndex₀_val p))        (divisorCanonicalProduct m f (Set.univ : Set ℂ))        (Set.univ : Set ℂ) :=    hasProdLocallyUniformlyOn_divisorCanonicalProduct_univ (m := m) (f := f) h_sum  simpa [HasProdLocallyUniformlyOn, divisorPartialProduct] using! hprod