Complex.differentiable_canonicalProduct

theorem differentiable_canonicalProduct {m : ℕ} {a : ℕ → ℂ}    (h_sum : Summable (fun n : ℕ => ‖a n‖⁻¹ ^ (m + 1))) (h_nonzero : ∀ n, a n ≠ 0) :    Differentiable ℂ (canonicalProduct m a) := by  have hloc :=    HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange      (hasProdLocallyUniformlyOn_canonicalProduct h_sum h_nonzero)  have hfactor : ∀ i : ℕ, Differentiable ℂ (fun z ↦ weierstrassFactor m (z / a i)) := by    intro i    simpa using! (differentiable_weierstrassFactor m).comp (differentiable_id.div_const (a i))  have hpartial :      ∀ᶠ N in Filter.atTop,        DifferentiableOn ℂ (fun z ↦ ∏ n ∈ Finset.range N, weierstrassFactor m (z / a n))          Set.univ := by    filter_upwards with N    simpa [differentiableOn_univ] using      (Differentiable.fun_finsetProd (u := Finset.range N) fun i hi ↦ hfactor i)  exact differentiableOn_univ.mp <| hloc.differentiableOn hpartial isOpen_univ