frobenius_norm_replicateRow — Mathlib

English

The Frobenius norm of the matrix obtained by replicating a row vector v along rows equals the Frobenius norm of the vector v interpreted in the L2 sense.

Русский

Норма Фробениуса матрицы, полученной повторением строки v по строкам, равна норме Фробениуса векторa v в смысле L2.

LaTeX

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

Lean4

@[simp]
theorem frobenius_norm_replicateRow (v : m → α) : ‖replicateRow ι v‖ = ‖toLp 2 v‖ :=
  by
  rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]
  simp only [replicateRow_apply, Real.rpow_two, PiLp.toLp_apply]

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