linfty_opNNNorm_def — Mathlib

English

The NNNorm of a matrix A, denoted ∥A∥, equals the NNReal supremum of row sums of NNNorms of entries: ∥A∥ = sup_i ∑_j ∥A_{ij}∥.

Русский

NNNorm матрицы A равна супреме NNReal сумм норм её элементов по строкам: ∥A∥ = sup_i ∑_j ∥A_{ij}∥.

LaTeX

$$$\\|A\\|_{nn} = \\sup_{i\\in m} \\sum_{j\\in n} \\|A_{ij}\\|_{nn}.$$$

Lean4

theorem linfty_opNNNorm_def (A : Matrix m n α) : ‖A‖₊ = (Finset.univ : Finset m).sup fun i : m => ∑ j : n, ‖A i j‖₊ :=
  Subtype.ext <| linfty_opNorm_def A

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