linearGrowthInf_le_iff — Mathlib

English

For a, a real, we have linearGrowthInf(u) ≤ a iff for every b > a there are infinitely many n with u(n) ≤ b n.

Русский

Для любой $a$ имеет место $\operatorname{linearGrowthInf}(u) \le a$ тогда и только тогда, когда для каждого $b > a$ существует бесконечно много $n$ таких, что $u(n) \le b n$.

LaTeX

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

Lean4

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

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