English
The NN-norm (nonnegative NNReal norm) of a matrix equals the Frobenius norm expressed in NNReal terms: the sum of squares is taken in NNReal and square rooted.
Русский
NN-нормa матрицы равна норме Фробениуса, выраженной в NNReal: сумма квадратов элементов в NNReal, затем извлечение квадратного корня.
LaTeX
$$$\|A\|_{NN} = \left( \sum_{i,j} \|A_{ij}\|_{NN}^{2} \right)^{1/2}.$$$
Lean4
theorem frobenius_norm_def (A : Matrix m n α) : ‖A‖ = (∑ i, ∑ j, ‖A i j‖ ^ (2 : ℝ)) ^ (1 / 2 : ℝ) :=
(congr_arg ((↑) : ℝ≥0 → ℝ) (frobenius_nnnorm_def A)).trans <| by simp [NNReal.coe_sum]