Theorems · Theorem · special functions

PeriodPair.summable_weierstrassPExceptSummand

∀ (L : PeriodPair) (l₀ z x : ℂ),
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖) →
    Summable (Function.uncurry fun b c => L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)

In the power series expansion of ℘(z) = ∑ᵢ aᵢ (z - x)ⁱ at some x ∉ L, each aᵢ can be written as a sum over l ∈ L, i.e. aᵢ = ∑ₗ, (i + 1) * (l - x)⁻ⁱ⁻² for i ≠ 0 and a₀ = ∑ₗ, (l - x)⁻² - l⁻². We show that the double sum converges if z falls in a ball centered at x that doesn't touch L.

Defined in

Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Cited by

3 results in Mathlib

Foundations

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