frobenius_norm_map_eq — Mathlib

English

Let f be a continuous linear map from n-dimensional to m-dimensional space. The Frobenius norm of its matrix representation equals the operator norm of f.

Русский

Пусть f — непрерывное линейное отображение; норма Фробениуса его матричного представления равна операторной норме f.

LaTeX

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

Lean4

@[simp]
theorem frobenius_norm_map_eq (A : Matrix m n α) (f : α → β) (hf : ∀ a, ‖f a‖ = ‖a‖) : ‖A.map f‖ = ‖A‖ :=
  (congr_arg ((↑) : ℝ≥0 → ℝ) <| frobenius_nnnorm_map_eq A f fun a => Subtype.ext <| hf a :)

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