isBigO_comp — Mathlib

English

For any h: IsBoundedBilinearMap 𝕜 f, and any l, (fun x => f (g x, h x)) =O[l] f.

Русский

Для любой ограничено билинейной карты f и любого l выполняется (f (g x, h x)) =O[l] f.

LaTeX

$$$IsBoundedBilinearMap\ 𝕜 f \Rightarrow (\forall {g}, {h}, {l}, (\lambda x => f (g x, h x)) =O[l] f)$$$

Lean4

theorem isBigO_comp {α : Type*} (H : IsBoundedBilinearMap 𝕜 f) {g : α → E} {h : α → F} {l : Filter α} :
    (fun x => f (g x, h x)) =O[l] fun x => ‖g x‖ * ‖h x‖ :=
  H.isBigO.comp_tendsto le_top

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