isBigO_comp — Mathlib

English

For a continuous linear map f: E → F and l a filter, the translated function x' ↦ f(x' − x) is Big-O of x' − x with bound ∥f∥, i.e., there exists a constant C such that ∥f(x' − x)∥ ≤ ∥f∥ ∥x' − x∥ for x' near x.

Русский

Для непрерывно линейного отображения f: E → F и фильтра l отображение x' ↦ f(x' − x) является Big-O по отношению к x' − x с константой ∥f∥.

LaTeX

$$$$ (x' \\mapsto f(x' - x)) =O_l (x' \\mapsto x' - x) \\quad \\text{with bound } \\|f\\|.$$$$

Lean4

theorem isBigO_comp {α : Type*} (f : α → E) (l : Filter α) : (fun x' => e (f x')) =O[l] f :=
  (e : E →SL[σ₁₂] F).isBigO_comp f l

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