Theorems · Theorem · special functions

PeriodPair.weierstrassPExcept_eq_tsum

∀ (L : PeriodPair) (l₀ z x : ℂ),
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖) →
    L.weierstrassPExcept l₀ z = ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i

Defined in

Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Cited by

1 results in Mathlib

Foundations

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