isBigO' — Mathlib

English

A bounded bilinear map f satisfies f = O_top foci with product of norms in a canonical way: f =O Top (‖p.fst‖ · ‖p.snd‖).

Русский

Ограниченное билинейное отображение удовлетворяет неравенству роста через произведение норм аргументов.

LaTeX

$$$IsBoundedBilinearMap\ 𝕜 f \Rightarrow f =O[Top] (\|p.1\| \cdot \|p.2\|)$$$

Lean4

protected theorem isBigO' (h : IsBoundedBilinearMap 𝕜 f) : f =O[⊤] fun p : E × F => ‖p‖ * ‖p‖ :=
  h.isBigO.trans <|
    (@Asymptotics.isBigO_fst_prod' _ E F _ _ _ _).norm_norm.mul (@Asymptotics.isBigO_snd_prod' _ E F _ _ _ _).norm_norm

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