frobenius_nnnorm_replicateRow

Mathlib.Analysis.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.frobenius_nnnorm_replicateRow

English

The NN-norm of the replicateRow matrix equals the NN-norm of toLp 2 v.

Русский

NN-нормa матрицы replicateRow равна NNNorm toLp 2 v.

LaTeX

$$$\|\mathrm{replicateRow}_{\iota} v\|_{NN} = \|\mathrm{toLp}_2(v)\|_{NN}.$$$

Lean4

@[simp]
theorem frobenius_nnnorm_replicateRow (v : m → α) : ‖replicateRow ι v‖₊ = ‖toLp 2 v‖₊ :=
  Subtype.ext <| frobenius_norm_replicateRow v

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru