isBigO_norm_left — Mathlib

English

Let α be a type, E' a normed space, F' a normed space, and l a filter on α. For any f': α → E' and g': α → F', the norm of f' is Big-O of g' along l if and only if f' is Big-O of g' along l.

Русский

Пусть α—множество; E', F' — нормированные пространства; l — фильтр на α. Для любых f' : α → E' и g' : α → F' выполняется, что функция x ↦ ‖f'(x)‖ есть O_l(g') тогда и только тогда, когда f' есть O_l(g').

LaTeX

$$$\\bigl(x \\mapsto \\|f'(x)\\|\\bigr) =O_l\, g' \\;\\Longleftrightarrow\\; f' =O_l\, g'$$

Lean4

@[simp]
theorem isBigO_norm_left : (fun x => ‖f' x‖) =O[l] g ↔ f' =O[l] g :=
  by
  simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_norm_left

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