isBigO_principal — Mathlib

English

For functions f, g, and a set s, f =O[𝓟 s] g if and only if there exists a constant c such that for all x in s, ||f(x)|| ≤ c ||g(x)||.

Русский

Для функций f, g и множества s верно: f =O[𝓟 s] g тогда и только тогда, когда существует константа c такая, что для всех x ∈ s выполняется ∥f(x)∥ ≤ c ∥g(x)∥.

LaTeX

$$$f =O[\mathcal{P}s] g \iff \exists c, \forall x \in s, \|f(x)\| \le c \|g(x)\|$$$

Lean4

theorem isBigO_principal {s : Set α} : f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖ := by
  simp_rw [isBigO_iff, eventually_principal]

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