English
If abscissaOfAbsConv f < Re(s) for a complex-valued f, then the L-series converges at s and the real part controls convergence.
Русский
Если абсцисса абсолютной сходимости функции f меньше Re(s) для комплексной f, то серия сходится при s и вещественная часть управляет сходимостью.
LaTeX
$$$\\forall f:\\mathbb{N}\\to\\mathbb{C},\\; \\operatorname{abscissaOfAbsConv}(f) < \\Re(s) \\Rightarrow LSeriesSummable f s.$$$
Lean4
/-- If `F` is a binary operation on `ℕ → ℂ` with the property that the `LSeries` of `F f g`
converges whenever the `LSeries` of `f` and `g` do, then the abscissa of absolute convergence
of `F f g` is at most the maximum of the abscissa of absolute convergence of `f`
and that of `g`. -/
theorem abscissaOfAbsConv_binop_le {F : (ℕ → ℂ) → (ℕ → ℂ) → (ℕ → ℂ)}
(hF : ∀ {f g s}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s) (f g : ℕ → ℂ) :
abscissaOfAbsConv (F f g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g) :=
by
refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun x hx ↦ hF ?_ ?_
· exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ (le_max_left ..).trans_lt hx
· exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ (le_max_right ..).trans_lt hx
