English
For a finite size n, the Frobenius nn-norm of the identity matrix I_n over α equals sqrt(card(n)) times the nn-norm of 1 in α.
Русский
Для размерности n верно: норма Фробениуса nn нормa единичной матрицы I_n равна sqrt(|n|) умножить на nn норму единицы в α.
LaTeX
$$$\\|I_n\\|_{nn} = \\sqrt{\\mathrm{card}(n)} \\; \\|1\\|_{nn}$$$
Lean4
theorem frobenius_nnnorm_one [DecidableEq n] [SeminormedAddCommGroup α] [One α] :
‖(1 : Matrix n n α)‖₊ = .sqrt (Fintype.card n) * ‖(1 : α)‖₊ := by
calc
‖(diagonal 1 : Matrix n n α)‖₊
_ = ‖toLp 2 (Function.const _ 1)‖₊ := (frobenius_nnnorm_diagonal _)
_ = .sqrt (Fintype.card n) * ‖(1 : α)‖₊ :=
by
rw [PiLp.nnnorm_toLp_const (ENNReal.ofNat_ne_top (n := 2))]
simp [NNReal.sqrt_eq_rpow]
