English
The abscissa of absolute convergence of f is defined as the infimum (in the extended real line) of the reals x for which the L-series is summable at x. Equivalently, abscissaOfAbsConv f = sInf (Real.toEReal '' { x ∈ ℝ | LSeriesSummable f x }).
Русский
Абсцисса абсолютной сходимости функции f определяется как инфимум множества вещественных чисел x, для которых сумма L‑порядка сходится; другими словами, abscissaOfAbsConv f = sInf (Real.toEReal '' { x ∈ ℝ | LSeriesSummable f x }).
LaTeX
$$$\\operatorname{abscissaOfAbsConv}(f) = \\inf\\{ \\operatorname{Real.toEReal}(x) : x\\in\\mathbb{R}, \\ LSeriesSummable\\ f\\ x \\}.$$$
Lean4
/-- The abscissa `x : EReal` of absolute convergence of the L-series associated to `f`:
the series converges absolutely at `s` when `re s > x` and does not converge absolutely
when `re s < x`. -/
noncomputable def abscissaOfAbsConv (f : ℕ → ℂ) : EReal :=
sInf <| Real.toEReal '' {x : ℝ | LSeriesSummable f x}
