abscissaOfAbsConv_le_of_le_const — Mathlib

English

If f is bounded, then abscissaOfAbsConv f ≤ 1.

Русский

Если f ограничена, то abscissaOfAbsConv f ≤ 1.

LaTeX

$$$\\text{If } \\exists C\\,\\forall n\\neq 0,\\; \\|f(n)\\| \\le C,\\ \\Rightarrow \\operatorname{abscissaOfAbsConv}(f) \\le 1.$$$

Lean4

/-- If `f` is bounded, then the abscissa of absolute convergence of `f` is bounded above by `1`. -/
theorem abscissaOfAbsConv_le_of_le_const {f : ℕ → ℂ} (h : ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C) : abscissaOfAbsConv f ≤ 1 := by
  simpa using abscissaOfAbsConv_le_of_le_const_mul_rpow (x := 0) (by simpa using h)

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