eventually_atTop_ge — Mathlib

English

The relation of polynomial growth is preserved under eventual equality: GrowsPolynomially f iff GrowsPolynomially g when f =ᶠ[atTop] g.

Русский

Рассмотрение полиномиального роста сохраняется при эквивалентности на бесконечности: GrowsPolynomially f ⇔ GrowsPolynomially g, если f =ᶠ[atTop] g.

LaTeX

$$f =ᶠ[atTop] g → GrowsPolynomially g → GrowsPolynomially f and vice versa.$$

Lean4

theorem eventually_atTop_ge {b : ℝ} (hb : b ∈ Set.Ioo 0 1) (hf : GrowsPolynomially f) :
    ∃ c > 0, ∀ᶠ x in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u :=
  by
  obtain ⟨c₁, hc₁, c₂, _, h⟩ := hf b hb
  refine ⟨c₁, hc₁, ?_⟩
  filter_upwards [h]
  exact fun _ H u hu => (H u hu).1

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