eventually_atTop_le — Mathlib

English

For any b in (0,1) and any polynomially growing f, there exists c>0 such that for large x and all u in [b x, x], f(u) ≤ c f(x).

Русский

Для любого b∈(0,1) и функции f с полиномиальным ростом существует c>0 such that для больших x и всех u∈[b x, x], f(u) ≤ c f(x).

LaTeX

$$$\\exists c>0,\\ ∀^{\\infty} x \\to atTop, \\forall u\\in Icc(bx,x),\\ f(u) \\le c f(x).$$$

Lean4

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

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