English
If LSeriesSummable f s, then there exists C such that ∥f(n)∥ ≤ C n^{s.re} for all n ≠ 0.
Русский
Если LSeriesSummable f s, существует константа C, такая что ∥f(n)∥ ≤ C n^{s.re} при n ≠ 0.
LaTeX
$$∃ C, ∀ n ≠ 0, ∥f(n)∥ ≤ C · n^{s.re}$$
Lean4
/-- If the `LSeries` of `f` is summable at `s`, then `f n` is bounded in absolute value
by a constant times `n^(re s)`. -/
theorem le_const_mul_rpow {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) : ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C * n ^ s.re :=
by
replace h := h.norm
by_contra! H
obtain ⟨n, hn₀, hn⟩ := H (tsum fun n ↦ ‖term f s n‖)
have := h.le_tsum n fun _ _ ↦ norm_nonneg _
rw [norm_term_eq, if_neg hn₀,
div_le_iff₀ <| Real.rpow_pos_of_pos (Nat.cast_pos.mpr <| Nat.pos_of_ne_zero hn₀) _] at this
exact (this.trans_lt hn).false.elim
