Source indexedtheorem · leanprover/lean4:v4.32.0

Complex.Hadamard.differentiable_divisorPartialProduct

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorComplement.lean:102 to 111

Mathematical statement

Exact Lean statement

theorem differentiable_divisorPartialProduct (m : ℕ) (f : ℂ → ℂ)
    (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))) :
    Differentiable ℂ (divisorPartialProduct m f s)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem differentiable_divisorPartialProduct (m : ℕ) (f : ℂ → ℂ)    (s : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ))) :    Differentiable ℂ (divisorPartialProduct m f s) := by  let Φ : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℂ → ℂ :=    fun p z => weierstrassFactor m (z / divisorZeroIndex₀_val p)  have hΦ : ∀ p ∈ s, Differentiable ℂ (Φ p) := by    intro p _hp    exact differentiable_weierstrassFactor_divisorZeroIndex₀ m p  simpa [divisorPartialProduct, Φ] using!    (Differentiable.fun_finsetProd (𝕜 := ℂ) (f := Φ) (u := s) hΦ)