linearGrowthSup_le_iff — Mathlib

English

The supremum growth is bounded by a iff for every b > a, there are infinitely many n with u(n) ≤ b n.

Русский

Предел линейного роста снизу ограничен сверху неравенством, если для каждого $b > a$ существует бесконечное множество $n$, удовлетворяющих $u(n) ≤ b n$.

LaTeX

$$$\operatorname{linearGrowthSup}(u) \le a \iff \forall b > a,\; \exists^{\infty} n \in \mathbb{N},\; u(n) \le b \cdot n.$$$

Lean4

theorem linearGrowthSup_le_iff : linearGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ n : ℕ in atTop, u n ≤ b * n :=
  by
  rw [linearGrowthSup, limsup_le_iff']
  refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
  rw [div_le_iff_le_mul (by norm_cast) (natCast_ne_top n), mul_comm _ b]

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