Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.hasProdUniformlyOn_canonicalProduct_compact

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CanonicalProduct.lean:61 to 69

Source documentation

The canonical product converges uniformly on compact sets under the standard summability hypothesis.

Exact Lean statement

theorem hasProdUniformlyOn_canonicalProduct_compact {m : ℕ} {a : ℕ → ℂ}
    (h_sum : Summable (fun n : ℕ => ‖a n‖⁻¹ ^ (m + 1))) (h_nonzero : ∀ n, a n ≠ 0)
    {K : Set ℂ} (hK : IsCompact K) :
    HasProdUniformlyOn (fun n z ↦ weierstrassFactor m (z / a n)) (canonicalProduct m a) K

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem hasProdUniformlyOn_canonicalProduct_compact {m : ℕ} {a : ℕ → ℂ}    (h_sum : Summable (fun n : ℕ => ‖a n‖⁻¹ ^ (m + 1))) (h_nonzero : ∀ n, a n ≠ 0)    {K : Set ℂ} (hK : IsCompact K) :    HasProdUniformlyOn (fun n z ↦ weierstrassFactor m (z / a n)) (canonicalProduct m a) K := by  have hloc :      HasProdLocallyUniformlyOn (fun n z ↦ weierstrassFactor m (z / a n))        (canonicalProduct m a) K :=    (hasProdLocallyUniformlyOn_canonicalProduct h_sum h_nonzero).mono (by simp : K ⊆ Set.univ)  exact hloc.hasProdUniformlyOn_of_isCompact hK