frobenius_nnnorm_def — Mathlib

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]

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