l2_opNorm_conjTranspose_mul_self — Mathlib

English

The L2-norm of A* A equals the square of the L2-norm of A: ||A* A||2 = ||A||2^2.

Русский

Норма L2 матрицы A* A равна квадрату нормы L2 матрицы A: ||A* A||2 = ||A||2^2.

LaTeX

$$$\\forall A: M_{m\\times n}(\\mathbb{C}), \\|A^{\\ast} A\\|_{2} = \\|A\\|_{2}^{2}$$$

Lean4

theorem l2_opNorm_conjTranspose_mul_self (A : Matrix m n 𝕜) : ‖Aᴴ * A‖ = ‖A‖ * ‖A‖ := by
  classical
  rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
  exact ContinuousLinearMap.norm_adjoint_comp_self _

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