isBigO_sub — Mathlib

English

For a continuous linear equivalence e, the map x ↦ e(x − x0) is Big-O of x − x0 with respect to a filter l; equivalently, the negative translation is preserved under e up to a Big-O bound.

Русский

Для непрерывно линейного эквивалента e отображение x ↦ e(x − x0) является Big-O относительно x − x0; перенос через e сохраняет асимптотику при сдвиге.

LaTeX

$$$$ (x \\mapsto e(x - x_0)) =O_l (x \\mapsto x - x_0).$$$$

Lean4

theorem isBigO_sub (x : E) : (fun x' => f (x' - x)) =O[l] fun x' => x' - x :=
  f.isBigO_comp _ l

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