hf_top' — Mathlib

English

As x tends to infinity, f(x) decays faster than any power of x; for every r ∈ R, f(x) = O(x^{r}) as x → ∞.

Русский

При x → ∞ функция f(x) уменьшается быстрее любой степенной скорости; для каждого r ∈ R имеет место f(x) = O(x^{r}) при x → ∞.

LaTeX

$$f = O[atTop] (·^r) for all real r$$

Lean4

/-- As `x → ∞`, `f x` decays faster than any power of `x`. -/
theorem hf_top' (r : ℝ) : P.f =O[atTop] (· ^ r) := by simpa [P.hf₀] using P.hf_top r

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