English
For square matrices A and B of compatible sizes over a complex-like normed field, the Frobenius nn-norm is submultiplicative: the nn-norm of AB does not exceed the product of the nn-norms.
Русский
Для совместимых по размеру матриц A, B над нормированным полем типа ℂ норма Фробениуса nn не превышает произведение норм отдельно взятых матриц.
LaTeX
$$$\\|A B\\|_{nn} \\le \\|A\\|_{nn} \\; \\|B\\|_{nn}$$$
Lean4
theorem frobenius_nnnorm_mul (A : Matrix l m α) (B : Matrix m n α) : ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊ :=
by
simp_rw [frobenius_nnnorm_def, Matrix.mul_apply]
rw [← NNReal.mul_rpow, @Finset.sum_comm _ _ m, Finset.sum_mul_sum]
gcongr with i _ j
rw [← NNReal.rpow_le_rpow_iff one_half_pos, ← NNReal.rpow_mul, mul_div_cancel₀ (1 : ℝ) two_ne_zero, NNReal.rpow_one,
NNReal.mul_rpow]
simpa only [PiLp.toLp_apply, PiLp.inner_apply, RCLike.inner_apply', starRingEnd_apply, Pi.nnnorm_def,
PiLp.nnnorm_eq_of_L2, star_star, nnnorm_star, NNReal.sqrt_eq_rpow, NNReal.rpow_two] using
nnnorm_inner_le_nnnorm (𝕜 := α) (toLp 2 (star <| A i ·)) (toLp 2 (B · j))
