isBigOWith_comp — Mathlib

English

As above, composition with a bounded linear map preserves a big-O bound with the operator norm as the constant.

Русский

Как выше, композиция с ограниченным линейным отображением сохраняет границу big-O с константой равной норме оператора.

LaTeX

$$$$\\text{IsBigOWith} \\|g\\| l (g \\circ f) $$$$

Lean4

theorem isBigOWith_comp [RingHomIsometric σ₂₃] {α : Type*} (g : F →SL[σ₂₃] G) (f : α → F) (l : Filter α) :
    IsBigOWith ‖g‖ l (fun x' => g (f x')) f :=
  (g.isBigOWith_id ⊤).comp_tendsto le_top

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