English
The NNNorm is submultiplicative: ∥A B∥₊ ≤ ∥A∥₊ ∥B∥₊ for A ∈ Mat_{l×m}(α), B ∈ Mat_{m×n}(α).
Русский
NNNorm подмножество: ∥AB∥₊ ≤ ∥A∥₊ ∥B∥₊ для матриц A и B.
LaTeX
$$$\\|A B\\|_{nn} \\leq \\|A\\|_{nn} \\cdot \\|B\\|_{nn}.$$$
Lean4
theorem linfty_opNNNorm_mul (A : Matrix l m α) (B : Matrix m n α) : ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊ :=
by
simp_rw [linfty_opNNNorm_def, Matrix.mul_apply]
calc
(Finset.univ.sup fun i => ∑ k, ‖∑ j, A i j * B j k‖₊) ≤ Finset.univ.sup fun i => ∑ k, ∑ j, ‖A i j‖₊ * ‖B j k‖₊ :=
Finset.sup_mono_fun fun i _hi =>
Finset.sum_le_sum fun k _hk => nnnorm_sum_le_of_le _ fun j _hj => nnnorm_mul_le _ _
_ = Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊ := by simp_rw [@Finset.sum_comm m, Finset.mul_sum]
_ ≤ Finset.univ.sup fun i => ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ :=
by
refine Finset.sup_mono_fun fun i _hi => ?_
gcongr with j hj
exact Finset.le_sup (f := fun i ↦ ∑ k : n, ‖B i k‖₊) hj
_ ≤ (Finset.univ.sup fun i => ∑ j, ‖A i j‖₊) * Finset.univ.sup fun i => ∑ j, ‖B i j‖₊ :=
by
simp_rw [← Finset.sum_mul, ← NNReal.finset_sup_mul]
rfl
