le_of_opNorm₂_le_of_le — Mathlib

English

If an operator valued as a bilinear map satisfies certain bound conditions, then a two-variable version of the operator-norm inequality holds.

Русский

Если билинейное отображение удовлетворяет условиям границы, то выполняется неравенство нормы в двух переменных.

LaTeX

$$$ \|f x y\| \le \|f\| \cdot \|x\| \cdot \|y\| $$$

Lean4

theorem le_of_opNorm₂_le_of_le [RingHomIsometric σ₁₃] (f : E →SL[σ₁₃] F →SL[σ₂₃] G) {x : E} {y : F} {a b c : ℝ}
    (hf : ‖f‖ ≤ a) (hx : ‖x‖ ≤ b) (hy : ‖y‖ ≤ c) : ‖f x y‖ ≤ a * b * c :=
  (f x).le_of_opNorm_le_of_le (f.le_of_opNorm_le_of_le hf hx) hy

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