l2_opNNNorm_conjTranspose_mul_self

English

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

Русский

NN-норма произведения AB не превосходит произведения NN-норм: ‖AB‖NN ≤ ‖A‖NN · ‖B‖NN.

LaTeX

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

Lean4

theorem l2_opNNNorm_conjTranspose_mul_self (A : Matrix m n 𝕜) : ‖Aᴴ * A‖₊ = ‖A‖₊ * ‖A‖₊ :=
  Subtype.ext <|
    l2_opNorm_conjTranspose_mul_self
      _
        -- note: with only a type ascription in the left-hand side, Lean picks the wrong norm.

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