LSeriesSummable_of_bounded_of_one_lt_real

English

Let f: N → C be a bounded function, i.e. there exists m > 0 with ∥f(n)∥ ≤ m for all n ≠ 0. Then for every real s with s > 1, the associated L-series converges: LSeriesSummable f s.

Русский

Пусть f: N → C ограничена, то есть существует m > 0 такое, что ∥f(n)∥ ≤ m для всех n ≠ 0. Тогда для всякого действительного s > 1 соответствующая L‑серия сходится: LSeriesSummable f s.

LaTeX

$$$\\forall f:\\mathbb{N}\\to\\mathbb{C},\\; (\\exists m>0\\,\\forall n\\neq 0,\\; \\|f(n)\\| \\le m) \\Rightarrow (\\forall s\\in\\mathbb{R},\\; 1

Lean4

/-- If `f` is bounded, then its `LSeries` is summable at `s : ℝ` when `s > 1`. -/ theorem LSeriesSummable_of_bounded_of_one_lt_real {f : ℕ → ℂ} {m : ℝ} (h : ∀ n ≠ 0, ‖f n‖ ≤ m) {s : ℝ} (hs : 1 < s) : LSeriesSummable f s := LSeriesSummable_of_bounded_of_one_lt_re h <| by simp [hs]

~~Похожие утверждения~~