isBigO_id — Mathlib

English

If f is a bounded linear map, then f = O_l(id_E) for every filter l on E; i.e., f is bounded by a constant times the identity near infinity.

Русский

Если f является ограниченным линейным отображением, то f = O_l(id_E) для любого фильтра l на E; то есть окольная оценка near infinity относительно тождественной функции.

LaTeX

$$$f\ \text{is bounded linear} \Rightarrow f =O[l] \ \mathrm{id}_E$$$

Lean4

theorem isBigO_id {f : E → F} (h : IsBoundedLinearMap 𝕜 f) (l : Filter E) : f =O[l] fun x => x :=
  let ⟨_, _, hM⟩ := h.bound
  IsBigO.of_bound _ (mem_of_superset univ_mem fun x _ => hM x)

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