norm_mkContinuous₂_aux — Mathlib

English

If a bilinear map f is built via mkContinuous₂ with a 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 norm_mkContinuous₂_aux (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (C : ℝ) (h : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) (x : E) :
    ‖(f x).mkContinuous (C * ‖x‖) (h x)‖ ≤ max C 0 * ‖x‖ :=
  (mkContinuous_norm_le' (f x) (h x)).trans_eq <| by rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

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