frequently_mul_le — Mathlib

English

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

Русский

Если бесконечно много n удовлетворяют u(n) ≤ a n, то линейный инфим линейного роста не превышает 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_mul_le (h : a < linearGrowthSup u) : ∃ᶠ n : ℕ in atTop, a * n ≤ u n :=
  le_linearGrowthSup_iff.1 (le_refl (linearGrowthSup u)) a h

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