Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.hasProdLocallyUniformlyOn_divisorComplementCanonicalProduct_univ

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorComplement.lean:304 to 320

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem hasProdLocallyUniformlyOn_divisorComplementCanonicalProduct_univ    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    HasProdLocallyUniformlyOn      (fun (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) (z : ℂ) =>        divisorComplementFactor m f z₀ p z)      (divisorComplementCanonicalProduct m f z₀)      (Set.univ : Set ℂ) := by  refine hasProdLocallyUniformlyOn_of_forall_compact      (f := fun p z => divisorComplementFactor m f z₀ p z)      (g := divisorComplementCanonicalProduct m f z₀) (s := (Set.univ : Set ℂ))      isOpen_univ ?_  intro K hKU hK  simpa using    (hasProdUniformlyOn_divisorComplementCanonicalProduct_univ (m := m) (f := f) (z₀ := z₀)      (K := K) hK h_sum)