Source indexedlemma · leanprover/lean4:v4.32.0

Complex.hasDerivAt_weierstrassFactor_at_one

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:110 to 119

Mathematical statement

Exact Lean statement

lemma hasDerivAt_weierstrassFactor_at_one (m : ℕ) :
    HasDerivAt (weierstrassFactor m) (-Complex.exp (partialLogSum m 1)) 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasDerivAt_weierstrassFactor_at_one (m : ℕ) :    HasDerivAt (weierstrassFactor m) (-Complex.exp (partialLogSum m 1)) 1 := by  have hsub : HasDerivAt (fun z : ℂ => 1 - z) (-1) 1 := by    simpa using! (hasDerivAt_const (1 : ℂ) (c := (1 : ℂ))).sub (hasDerivAt_id 1)  have hexp :      HasDerivAt (fun z : ℂ => Complex.exp (partialLogSum m z))        ((∑ j ∈ Finset.range m, (1 : ℂ) ^ j) * Complex.exp (partialLogSum m 1)) 1 := by    simpa [mul_comm] using!      (Complex.hasDerivAt_exp (partialLogSum m 1)).comp 1 (hasDerivAt_partialLogSum m 1)  simpa [weierstrassFactor] using! hsub.mul hexp