frequently_le_mul — Mathlib

English

If there are infinitely many n with u(n) ≤ a n, then linearGrowthInf(u) ≤ a.

Русский

Если бесконечно много $n$ удовлетворяют $u(n) \le a n$, то $\operatorname{linearGrowthInf}(u) \le a$.

LaTeX

$$$\bigl( \exists^{\infty} n \in \mathbb{N},\; u(n) \le a \cdot n \bigr) \implies \operatorname{linearGrowthInf}(u) \le a.$$$

Lean4

theorem frequently_le_mul (h : linearGrowthInf u < a) : ∃ᶠ n : ℕ in atTop, u n ≤ a * n :=
  linearGrowthInf_le_iff.1 (le_refl (linearGrowthInf u)) a h

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