permMatrix_l2_opNorm_le — Mathlib

English

The l2-operator norm of a permutation matrix is at most 1.

Русский

Норма l2 оператора перестановочной матрицы не превышает 1.

LaTeX

$$$\\|\\sigma\\text{.permMatrix }R\\|_{2} \\le 1$$$

Lean4

/-- The l2-operator norm of a permutation matrix is bounded above by 1.
See `Matrix.permMatrix_l2_opNorm_eq` for the equality statement assuming the matrix is nonempty.
-/
theorem permMatrix_l2_opNorm_le : ‖σ.permMatrix 𝕜‖ ≤ 1 :=
  ContinuousLinearMap.opNorm_le_bound _ (by simp) <| by
    simp [EuclideanSpace.norm_eq, toEuclideanLin_apply, permMatrix_mulVec, σ.sum_comp _ (fun i ↦ ‖_‖ ^ 2)]

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