le_linearGrowthSup_iff — Mathlib

English

A ≤ linearGrowthSup(u) iff for every b < a there are infinitely many n with b n ≤ u(n).

Русский

Пусть a ≤ linearGrowthSup(u) тогда и только тогда, когда для каждого b < a бесконечно много n удовлетворяют b n ≤ u(n).

LaTeX

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

Lean4

theorem le_linearGrowthSup_iff : a ≤ linearGrowthSup u ↔ ∀ b < a, ∃ᶠ n : ℕ in atTop, b * n ≤ u n :=
  by
  rw [linearGrowthSup, le_limsup_iff']
  refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
  nth_rw 1 [le_div_iff_mul_le (by norm_cast) (natCast_ne_top n)]
    /- Forward direction of `linearGrowthInf_le_iff`. -/

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