isBoundedBilinearMap — Mathlib

English

A bounded bilinear map f is Big-O of the product of norms: f =O (‖x‖‖y‖) on E×F.

Русский

Ограниченное билинейное отображение удовлетворяет неравенству роста: ‖f(x,y)‖ ≤ C‖x‖‖y‖.

LaTeX

$$$IsBoundedBilinearMap\ 𝕜 f \Rightarrow f =O[⊤] (\|x\| \cdot \|y\|)$$$

Lean4

theorem isBoundedBilinearMap (f : E →L[𝕜] F →L[𝕜] G) : IsBoundedBilinearMap 𝕜 fun x : E × F => f x.1 x.2 :=
  { add_left := f.map_add₂
    smul_left := f.map_smul₂
    add_right := fun x => (f x).map_add
    smul_right := fun c x => (f x).map_smul c
    bound :=
      ⟨max ‖f‖ 1, zero_lt_one.trans_le (le_max_right _ _), fun x y =>
        (f.le_opNorm₂ x y).trans <| by apply_rules [mul_le_mul_of_nonneg_right, norm_nonneg, le_max_left]⟩ }

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