frobenius_norm_diagonal — Mathlib

English

Let v be a finite n-tuple taking values in a normed additive group. The Frobenius norm of the diagonal matrix with diagonal entries v equals the Euclidean (L2) norm of the vector v.

Русский

Пусть v — функция из конечного множества в нормированную аддитивную группу; диагональная матрица с диагональю v имеет норму Фробениуса, равную евклидовой (L2) норме вектора v.

LaTeX

$$$\\|\\mathrm{diag}(v)\\|_F = \\|v\\|_2$$$

Lean4

@[simp]
theorem frobenius_norm_diagonal [DecidableEq n] (v : n → α) : ‖diagonal v‖ = ‖toLp 2 v‖ :=
  (congr_arg ((↑) : ℝ≥0 → ℝ) <| frobenius_nnnorm_diagonal v :).trans rfl

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