LSeriesSummable — Mathlib

English

LSeriesSummable f s indicates that the L-series converges absolutely at s, i.e., Summable (term f s).

Русский

LSeriesSummable f s означает, что L-ряд сходится абсолютно в точке s, то есть Summable (term f s).

LaTeX

$$$LSeriesSummable(f,s) \\equiv \\mathrm{Summable}(\\operatorname{term}(f,s))$$$

Lean4

/-- `LSeriesSummable f s` indicates that the L-series of `f` converges absolutely at `s`. -/
def LSeriesSummable (f : ℕ → ℂ) (s : ℂ) : Prop :=
  Summable (term f s)

Похожие утверждения