isLittleO_iff_nat_mul_le' — Mathlib

English

For functions f and g, f = o[l] g is equivalent to ∀ n ∈ ℕ, ∀ᶠ x in l, n·‖f(x)‖ ≤ ‖g(x)‖.

Русский

Для функций f и g условие f = o[l] g эквивалентно: ∀ n ∈ ℕ, ∀ᶠ x в l: n·|f(x)| ≤ |g(x)|.

LaTeX

$$$ f =o[l] g \iff \forall n : \mathbb{N}, \forall^\infty x in l, n \|f(x)\| \le \|g(x)\| $$$

Lean4

theorem isLittleO_iff_nat_mul_le' : f' =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f' x‖ ≤ ‖g x‖ :=
  isLittleO_iff_nat_mul_le_aux (Or.inl fun _x => norm_nonneg _)

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