Theorems · Theorem · special functions

PeriodPair.hasSumLocallyUniformly_aux

∀ (L : PeriodPair) (f : ↥L.lattice → ℂ → ℂ) (u : ℝ → ↥L.lattice → ℝ),
  (∀ r > 0, Summable (u r)) →
    (∀ r > 0, ∀ᶠ (R : ℝ) in Filter.atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l) →
      HasSumLocallyUniformly f fun x => ∑' (j : ↥L.lattice), f j x

Defined in

Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Cited by

2 results in Mathlib

Foundations

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