l2_opNNNorm_mulVec — Mathlib

English

The NN-norm of A x is bounded by the product of NN-norms: ‖A x‖NN ≤ ‖A‖NN · ‖x‖NN.

Русский

NN-норма A x не превышает произведение NN-норм A и NN-норм x.

LaTeX

$$$\\forall A: M_{m\\times n}(\\mathbb{C}), x: (\\mathbb{C}^{n}), \\\\ \\|A x\\|_{NN} \\leq \\|A\\|_{NN} \\cdot \\|x\\|_{NN}$$$

Lean4

theorem l2_opNNNorm_mulVec (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
    ‖(EuclideanSpace.equiv m 𝕜).symm <| A *ᵥ x‖₊ ≤ ‖A‖₊ * ‖x‖₊ :=
  A.l2_opNorm_mulVec x

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