isBigO_comp — Mathlib

English

Let g be a bounded linear map and f any map. Then the composition g ∘ f is big-O of f with respect to any filter l on E, i.e., (g ∘ f) =O[l] f.

Русский

Пусть g — ограниченное линейное отображение, a f — произвольное отображение. Тогда композиция g ∘ f является большим-O от f по отношению к любому фильтру l на E, то есть (g ∘ f) =O[l] f.

LaTeX

$$$IsBoundedLinearMap\ 𝕜\ g\rightarrow (g\circ f)=O[l] f$$$

Lean4

theorem isBigO_comp {E : Type*} {g : F → G} (hg : IsBoundedLinearMap 𝕜 g) {f : E → F} (l : Filter E) :
    (fun x' => g (f x')) =O[l] f :=
  (hg.isBigO_id ⊤).comp_tendsto le_top

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