Theorems · Theorem · special functions

PeriodPair.iteratedDeriv_weierstrassPExcept_self

∀ (L : PeriodPair) (l : ℂ) {n : ℕ},
  iteratedDeriv n (L.weierstrassPExcept l) l =
    if n = 0 then L.weierstrassPExcept l l else ↑(n + 1).factorial * L.sumInvPow l (n + 2)

Defined in

Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Cited by

0 results in Mathlib

Foundations

Depth 305 from the axioms · uses propext, Classical.choice, Quot.sound