frobenius_norm_replicateCol — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem frobenius_norm_replicateCol (v : n → α) : ‖replicateCol ι v‖ = ‖toLp 2 v‖ := by
  simp [frobenius_norm_def, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]

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