English
The NN-norm of the diagonal matrix diag(v) equals the NN-norm of toLp 2 v.
Русский
NN-нормa диагональной матрицы diag(v) равна NNNorm toLp 2 v.
LaTeX
$$$\|\mathrm{diagonal}(v)\|_{NN} = \|\mathrm{toLp}_2(v)\|_{NN}.$$$
Lean4
@[simp]
theorem frobenius_nnnorm_diagonal [DecidableEq n] (v : n → α) : ‖diagonal v‖₊ = ‖toLp 2 v‖₊ :=
by
simp_rw [frobenius_nnnorm_def, ← Finset.sum_product', Finset.univ_product_univ, PiLp.nnnorm_eq_of_L2]
let s := (Finset.univ : Finset n).map ⟨fun i : n => (i, i), fun i j h => congr_arg Prod.fst h⟩
rw [← Finset.sum_subset (Finset.subset_univ s) fun i _hi his => ?_]
· rw [Finset.sum_map, NNReal.sqrt_eq_rpow]
dsimp
simp_rw [diagonal_apply_eq, NNReal.rpow_two]
· suffices i.1 ≠ i.2 by rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
intro h
exact Finset.mem_map.not.mp his ⟨i.1, Finset.mem_univ _, Prod.ext rfl h⟩
