English
For any v: n → α, the nnnorm of diagonal v equals the nnnorm of v: ∥diagonal v∥₊ = ∥v∥₊.
Русский
Для любого v: n → α норма nnnorm диагональной матрицы равна норме nnnorm самого вектора: ∥diagonal v∥₊ = ∥v∥₊.
LaTeX
$$$\|\text{diagonal } v\|_+ = \|v\|_+.$$$
Lean4
@[simp]
theorem nnnorm_diagonal [DecidableEq n] (v : n → α) : ‖diagonal v‖₊ = ‖v‖₊ :=
by
simp_rw [nnnorm_def, Pi.nnnorm_def]
congr 1 with i : 1
refine le_antisymm (Finset.sup_le fun j hj => ?_) ?_
· obtain rfl | hij := eq_or_ne i j
· rw [diagonal_apply_eq]
· rw [diagonal_apply_ne _ hij, nnnorm_zero]
exact zero_le _
· refine Eq.trans_le ?_ (Finset.le_sup (Finset.mem_univ i))
rw [diagonal_apply_eq]
