eventually_atTop_le_nat — Mathlib

English

Discrete version: for natural n and b∈(0,1), there exists c>0 with f(u) ≤ c f(n) for u ∈ [bn, n] for large n.

Русский

Дискретная версия: для натурального n и b∈(0,1) существует c>0 такое, что для больших n и для всех u∈[bn,n], f(u) ≤ c f(n).

LaTeX

$$$\\exists c>0,\\∀^\\infty n,\\forall u\\in Icc(b n,n), f(u) ≤ c f(n).$$$

Lean4

theorem eventually_atTop_le_nat {b : ℝ} (hb : b ∈ Set.Ioo 0 1) (hf : GrowsPolynomially f) :
    ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * n) n, f u ≤ c * f n :=
  by
  obtain ⟨c, hc_mem, hc⟩ := hf.eventually_atTop_le hb
  exact ⟨c, hc_mem, hc.natCast_atTop⟩

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