English
If ∃ C and x ∈ ℝ such that ∥f(n)∥ ≤ C n^x for all n ≠ 0, then abscissaOfAbsConv f ≤ x+1.
Русский
Если существует константа C и показатель x, такие что ∥f(n)∥ ≤ C n^x для всех n ≠ 0, то абсцисса абсолютной сходимости не превосходит x+1.
LaTeX
$$$\\exists C>0,\\ \\forall n\\neq 0,\\; \\|f(n)\\| \\le C\\, n^{x} \\Rightarrow \\operatorname{abscissaOfAbsConv}(f) \\le x+1.$$$
Lean4
/-- If `‖f n‖` is bounded by a constant times `n^x`, then the abscissa of absolute convergence
of `f` is bounded by `x + 1`. -/
theorem abscissaOfAbsConv_le_of_le_const_mul_rpow {f : ℕ → ℂ} {x : ℝ} (h : ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C * n ^ x) :
abscissaOfAbsConv f ≤ x + 1 := by
rw [show x = x + 1 - 1 by ring] at h
by_contra! H
obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H
exact
(LSeriesSummable_of_le_const_mul_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h |>.abscissaOfAbsConv_le.trans_lt
hy₂).false
