linfty_opNNNorm_mulVec — Mathlib

English

For A ∈ Mat_{l×m}(α) and v ∈ α^m, the NNNorm of A.mulVec v is bounded by ∥A∥₊ ∥v∥₊: ∥A.mulVec v∥₊ ≤ ∥A∥₊ ∥v∥₊.

Русский

Для A ∈ Mat_{l×m}(α) и вектора v ∈ α^m, NNNorm вектора A·v ограничен: ∥A·v∥₊ ≤ ∥A∥₊ ∥v∥₊.

LaTeX

$$$\\|A \\cdot v\\|_{nn} \\leq \\|A\\|_{nn} \\cdot \\|v\\|_{nn}.$$$

Lean4

theorem linfty_opNNNorm_mulVec (A : Matrix l m α) (v : m → α) : ‖A *ᵥ v‖₊ ≤ ‖A‖₊ * ‖v‖₊ :=
  by
  rw [← linfty_opNNNorm_replicateCol (ι := Fin 1) (A *ᵥ v), ← linfty_opNNNorm_replicateCol v (ι := Fin 1)]
  exact linfty_opNNNorm_mul A (replicateCol (Fin 1) v)

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