English
The nn-norm (nonnegative norm) is defined via the same induced identification with Euclidean endomorphisms.
Русский
nn-нормa (неотрицательная норма) определяется через ту же индукцию через Евклидово пространство.
LaTeX
$$$\\|A\\|_+ = \\| (toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap A \\|_+$$$
Lean4
/-- The metric on `Matrix m n 𝕜` arising from the operator norm given by the identification with
(continuous) linear maps of `EuclideanSpace`. -/
def instL2OpMetricSpace : MetricSpace (Matrix m n 𝕜) := by
/- We first replace the topology so that we can automatically replace the uniformity using
`IsUniformAddGroup.toUniformSpace_eq`. -/
letI normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
{
l2OpNormedAddCommGroupAux.replaceTopology <|
(toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans
toContinuousLinearMap |>.toContinuousLinearEquiv.toHomeomorph.isInducing.eq_induced with
norm := l2OpNormedAddCommGroupAux.norm
dist_eq := l2OpNormedAddCommGroupAux.dist_eq }
exact
normed_add_comm_group.replaceUniformity <| by
congr
rw [← @IsUniformAddGroup.toUniformSpace_eq _ (Matrix.instUniformSpace m n 𝕜) _ _]
rw [@IsUniformAddGroup.toUniformSpace_eq _ PseudoEMetricSpace.toUniformSpace _ _]
