frobenius_nnnorm_replicateCol

Mathlib.Analysis.Matrix

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

English

The NN-norm of replicateCol ι v equals the NN-norm of toLp 2 v.

Русский

NN-нормa replicateCol ι v равна NNNorm toLp 2 v.

LaTeX

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

Lean4

@[simp]
theorem frobenius_nnnorm_replicateCol (v : n → α) : ‖replicateCol ι v‖₊ = ‖toLp 2 v‖₊ :=
  Subtype.ext <| frobenius_norm_replicateCol v

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

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

Разделы

Аффилиация

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