eventually_atTop_ge_nat — Mathlib

English

For a polynomially growing function f and b ∈ (0,1), there exists c>0 such that for all sufficiently large n and all u ∈ [bn, n], c f(n) ≤ f(u).

Русский

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

LaTeX

$$$\forall {f : \mathbb{R} \to \mathbb{R}}\; b \in (0,1)\; (GrowsPolynomially\ f) \Rightarrow \exists c>0, \forall^\infty n:\, \forall u \in [b n, n], c f(n) \le f(u).$$$

Lean4

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

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