le_linearGrowthInf_iff — Mathlib

English

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

Русский

Пусть $a$—вещественное; тогда $a \le \operatorname{linearGrowthInf}(u)$ эквивалентно тому, что для каждого $b < a$ бесконечно many $n$ удовлетворяют $b n \le u(n)$.

LaTeX

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

Lean4

theorem le_linearGrowthInf_iff : a ≤ linearGrowthInf u ↔ ∀ b < a, ∀ᶠ n : ℕ in atTop, b * n ≤ u n :=
  by
  rw [linearGrowthInf, le_liminf_iff']
  refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
  nth_rw 1 [le_div_iff_mul_le (by norm_cast) (natCast_ne_top n)]

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