abscissaOfAbsConv_le_one_of_isBigO_one

English

If f = O(1), then abscissaOfAbsConv f ≤ 1.

Русский

Если f = O(1), тогда abscissaOfAbsConv f ≤ 1.

LaTeX

$$$\\text{If } f =O(1) \\Rightarrow \\operatorname{abscissaOfAbsConv}(f) \\le 1.$$$

Lean4

/-- If `f` is `O(1)`, then the abscissa of absolute convergence of `f` is bounded above by `1`. -/
theorem abscissaOfAbsConv_le_one_of_isBigO_one {f : ℕ → ℂ} (h : f =O[atTop] fun _ ↦ (1 : ℝ)) :
    abscissaOfAbsConv f ≤ 1 := by simpa using abscissaOfAbsConv_le_of_isBigO_rpow (x := 0) (by simpa using h)

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