English
The Frobenius norm induces a NormedStarGroup structure on the matrix space, i.e., the star operation is isometric with respect to the Frobenius norm.
Русский
Норма Фробениуса задаёт структуру NormedStarGroup на пространстве матриц: операция сопряжения сохраняет норму.
LaTeX
$$$[\text{Matrix}_{m\times m}(\alpha)] \text{ with Frobenius norm satisfies } \|A^{*}\| = \|A\|.$$$
Lean4
theorem frobenius_nnnorm_def (A : Matrix m n α) : ‖A‖₊ = (∑ i, ∑ j, ‖A i j‖₊ ^ (2 : ℝ)) ^ (1 / 2 : ℝ) :=
by
change ‖toLp 2 fun i => toLp 2 fun j => A i j‖₊ = _
simp_rw [PiLp.nnnorm_eq_of_L2, NNReal.sq_sqrt, NNReal.sqrt_eq_rpow, NNReal.rpow_two, PiLp.toLp_apply]