isBigOWith_sub — Mathlib

English

For a continuous linear map f: E → F and l a filter on E, the translated map x ↦ f(x − x0) is Big-O with bound ∥f∥ relative to x ↦ x − x0.

Русский

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

LaTeX

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

Lean4

theorem isBigOWith_sub (x : E) : IsBigOWith ‖f‖ l (fun x' => f (x' - x)) fun x' => x' - x :=
  f.isBigOWith_comp _ l

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