English
If abscissaOfAbsConv( f· ) < x for a real-valued f, then the real series ∑ f(n)/n^x converges.
Русский
Если abscissaOfAbsConv( f· ) < x для вещественной функции f, то ряд ∑ f(n)/n^x сходится.
LaTeX
$$$\\text{If } f:\\mathbb{N}\\to\\mathbb{R},\\; \\operatorname{abscissaOfAbsConv}(f) < x \\Rightarrow \\Summable\\ {n:\\mathbb{N}}\\; \\frac{f(n)}{n^{x}}.$$$
Lean4
/-- If `f` is real-valued and `x` is strictly greater than the abscissa of absolute convergence
of `f`, then the real series `∑' n, f n / n ^ x` converges. -/
theorem summable_real_of_abscissaOfAbsConv_lt {f : ℕ → ℝ} {x : ℝ} (h : abscissaOfAbsConv (f ·) < x) :
Summable fun n : ℕ ↦ f n / (n : ℝ) ^ x :=
by
have aux : term (f ·) x = fun n ↦ ↑(if n = 0 then 0 else f n / (n : ℝ) ^ x) :=
by
ext n
simp [term_def, apply_ite ((↑) : ℝ → ℂ), ofReal_cpow n.cast_nonneg]
have := LSeriesSummable_of_abscissaOfAbsConv_lt_re (ofReal_re x ▸ h)
simp only [LSeriesSummable, aux, summable_ofReal] at this
refine this.congr_cofinite ?_
filter_upwards [(Set.finite_singleton 0).compl_mem_cofinite] with n hn using if_neg (by simpa using hn)
