English
For a nonempty index set, the l2-operator norm of a permutation matrix equals 1.
Русский
Для непустого множества индексов норма l2 оператора перестановочной матрицы равна 1.
LaTeX
$$$[\\text{Nonempty } n] \\Rightarrow \\|\\sigma\\text{.permMatrix }R\\|_{2} = 1$$$
Lean4
/-- The l2-operator norm of a nonempty permutation matrix is equal to 1.
Note that this is not true for the empty case, since the empty matrix has l2-operator norm 0.
See `Matrix.permMatrix_l2_opNorm_le` for the inequality version of the empty case.
-/
theorem permMatrix_l2_opNorm_eq [Nonempty n] : ‖σ.permMatrix 𝕜‖ = 1 :=
le_antisymm (permMatrix_l2_opNorm_le σ) <| by
inhabit n
simpa [EuclideanSpace.norm_eq, permMatrix_mulVec, ← Equiv.eq_symm_apply, apply_ite] using
(σ.permMatrix 𝕜).l2_opNorm_mulVec (WithLp.toLp _ (Pi.single default 1))
