Source indexedlemma · leanprover/lean4:v4.32.0

Complex.hasDerivAt_weierstrassFactor_div_at_self

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:130 to 139

Mathematical statement

Exact Lean statement

lemma hasDerivAt_weierstrassFactor_div_at_self (m : ℕ) {a : ℂ} (ha : a ≠ 0) :
    HasDerivAt (fun z : ℂ ↦ weierstrassFactor m (z / a))
      ((-Complex.exp (partialLogSum m 1)) / a) a

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasDerivAt_weierstrassFactor_div_at_self (m : ℕ) {a : ℂ} (ha : a ≠ 0) :    HasDerivAt (fun z : ℂ ↦ weierstrassFactor m (z / a))      ((-Complex.exp (partialLogSum m 1)) / a) a := by  have hcomp :      HasDerivAt ((weierstrassFactor m) ∘ fun z : ℂ ↦ z / a)        ((-Complex.exp (partialLogSum m 1)) * (1 / a)) a :=    HasDerivAt.comp (x := a) (h := fun z : ℂ ↦ z / a) (h₂ := weierstrassFactor m)      (by simpa [ha] using hasDerivAt_weierstrassFactor_at_one m)      ((hasDerivAt_id a).div_const a)  simpa [Function.comp, div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using! hcomp