l2_opNorm_mulVec — Mathlib

English

For any A and x, the Euclidean norm of A x is bounded by the operator norm of A times the Euclidean norm of x: ||A x|| ≤ ||A|| · ||x||.

Русский

Для любых A и x евклидова нормы выполняется неравенство: ||A x|| ≤ ||A|| · ||x||.

LaTeX

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

Lean4

theorem l2_opNorm_mulVec (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
    ‖(EuclideanSpace.equiv m 𝕜).symm <| A *ᵥ x‖ ≤ ‖A‖ * ‖x‖ :=
  toEuclideanLin (n := n) (m := m) (𝕜 := 𝕜) |>.trans toContinuousLinearMap A |>.le_opNorm x

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