Theorems · Theorem · special functions

PeriodPair.hasFPowerSeriesAt_weierstrassPExcept

∀ (L : PeriodPair) (l : ℂ),
  HasFPowerSeriesAt (L.weierstrassPExcept l)
    (FormalMultilinearSeries.ofScalars ℂ fun i =>
      if i = 0 then L.weierstrassPExcept l l else (↑i + 1) * L.sumInvPow l (i + 2))
    l

Defined in

Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Cited by

1 results in Mathlib

Foundations

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