frobenius_norm_def — Mathlib

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]

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