mkContinuous₂_norm_le — Mathlib

English

If a bilinear map f is constructed as mkContinuous₂ with a nonnegative bound C, then its operator norm is at most max(C,0).

Русский

Если билинейное отображение f строится как mkContinuous₂ с неотрицательной границей C, тогда его норма оператора не превосходит max(C,0).

LaTeX

$$$ \|f.mkContinuous₂ C hC\| \le \max\{C,0\} $$$

Lean4

theorem mkContinuous₂_norm_le (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ} (h0 : 0 ≤ C) (hC : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) :
    ‖f.mkContinuous₂ C hC‖ ≤ C :=
  (f.mkContinuous₂_norm_le' hC).trans_eq <| max_eq_left h0

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