frobenius_nnnorm_map_eq — Mathlib

English

For a bounded linear map f, the matrix representation has the same Frobenius norm as f itself under the appropriate norm mapping.

Русский

Для ограниченного линейного отображения f матричное представление имеет такую же норму Фробениуса, как и сама функция f под соответствующей нормой.

LaTeX

$$$\|\mathrm{toMatrix}'(f)\|_{F} = \|f\|_{F}.$$$

Lean4

@[simp]
theorem frobenius_nnnorm_map_eq (A : Matrix m n α) (f : α → β) (hf : ∀ a, ‖f a‖₊ = ‖a‖₊) : ‖A.map f‖₊ = ‖A‖₊ := by
  simp_rw [frobenius_nnnorm_def, Matrix.map_apply, hf]

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