feat: provide the ℓ² operator norm on matrices (#9474)

This adds the (unique) C⋆-norm on matrices `Matrix n n 𝕜` with `IsROrC 𝕜` within the scope `Matrix.L2OpNorm`. This norm coincides with the operator norm induced by the ℓ² norm (i.e., the norm on `Matrix m n 𝕜` obtained by pulling back the norm from `EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m`). Where possible, we state results for rectangular matrices.

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -514,7 +514,7 @@ variable {m n : Type*} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
 variable [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F]
 variable (v₁ : OrthonormalBasis n 𝕜 E) (v₂ : OrthonormalBasis m 𝕜 F)
 
-/- the linear map associated to the conjugate transpose of a matrix corresponding to two
+/-- The linear map associated to the conjugate transpose of a matrix corresponding to two
 orthonormal bases is the adjoint of the linear map associated to the matrix. -/
 lemma Matrix.toLin_conjTranspose (A : Matrix m n 𝕜) :
     toLin v₂.toBasis v₁.toBasis Aᴴ = adjoint (toLin v₁.toBasis v₂.toBasis A) := by

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -1034,6 +1034,11 @@ theorem toEuclideanLin_eq_toLin :
   rfl
 #align matrix.to_euclidean_lin_eq_to_lin Matrix.toEuclideanLin_eq_toLin
 
+open EuclideanSpace in
+lemma toEuclideanLin_eq_toLin_orthonormal :
+    toEuclideanLin = toLin (basisFun n 𝕜).toBasis (basisFun m 𝕜).toBasis :=
+  rfl
+
 end Matrix
 
 local notation "⟪" x ", " y "⟫ₑ" =>

Mathlib/Analysis/Matrix.lean

@@ -41,6 +41,10 @@ In this file we provide the following non-instances for norms on matrices:
 
 These are not declared as instances because there are several natural choices for defining the norm
 of a matrix.
+
+The norm induced by the identification of `Matrix m n 𝕜` with
+`EuclideanSpace n 𝕜 →L[𝕜] EuclideanSpace m 𝕜` (i.e., the ℓ² operator norm) can be found in
+`Analysis.NormedSpace.Star.Matrix`. It is separated to avoid extraneous imports in this file.
 -/
 
 noncomputable section

Mathlib/Analysis/NormedSpace/Star/Matrix.lean

@@ -3,23 +3,45 @@ Copyright (c) 2022 Hans Parshall. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Hans Parshall
 -/
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 import Mathlib.Analysis.Matrix
 import Mathlib.Analysis.NormedSpace.Basic
 import Mathlib.Data.IsROrC.Basic
 import Mathlib.LinearAlgebra.UnitaryGroup
+import Mathlib.Topology.UniformSpace.Matrix
 
 #align_import analysis.normed_space.star.matrix from "leanprover-community/mathlib"@"468b141b14016d54b479eb7a0fff1e360b7e3cf6"
 
 /-!
-# Unitary matrices
+# Analytic properties of the `star` operation on matrices
+
+This transports the operator norm on `EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m` to
+`Matrix m n 𝕜`. See the file `Analysis.Matrix` for many other matrix norms.
+
+## Main definitions
+
+* `Matrix.instNormedRingL2Op`: the (necessarily unique) normed ring structure on `Matrix n n 𝕜`
+  which ensure it is a `CstarRing` in `Matrix.instCstarRing`. This is a scoped instance in the
+  namespace `Matrix.L2OpNorm` in order to avoid choosing a global norm for `Matrix`.
+
+## Main statements
+
+* `entry_norm_bound_of_unitary`: the entries of a unitary matrix are uniformly boundd by `1`.
+
+## Implementation details
+
+We take care to ensure the topology and uniformity induced by `Matrix.instMetricSpaceL2Op`
+coincide with the existing topology and uniformity on matrices.
+
+## TODO
+
+* Show that `‖diagonal (v : n → 𝕜)‖ = ‖v‖`.
 
-This file collects facts about the unitary matrices over `𝕜` (either `ℝ` or `ℂ`).
 -/
 
 
 open scoped BigOperators Matrix
-
-variable {𝕜 m n E : Type*}
+variable {𝕜 m n l E : Type*}
 
 section EntrywiseSupNorm
 
@@ -70,3 +92,162 @@ theorem entrywise_sup_norm_bound_of_unitary {U : Matrix n n 𝕜} (hU : U ∈ Ma
 #align entrywise_sup_norm_bound_of_unitary entrywise_sup_norm_bound_of_unitary
 
 end EntrywiseSupNorm
+
+noncomputable section L2OpNorm
+
+namespace Matrix
+open LinearMap
+
+variable [IsROrC 𝕜]
+variable [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [Fintype l] [DecidableEq l]
+
+/-- The natural star algebra equivalence between matrices and continuous linear endomoporphisms
+of Euclidean space induced by the orthonormal basis `EuclideanSpace.basisFun`.
+
+This is a more-bundled version of `Matrix.toEuclideanLin`, for the special case of square matrices,
+followed by a more-bundled version of `LinearMap.toContinuousLinearMap`. -/
+def toEuclideanClm :
+    Matrix n n 𝕜 ≃⋆ₐ[𝕜] (EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :=
+  toMatrixOrthonormal (EuclideanSpace.basisFun n 𝕜) |>.symm.trans <|
+    { toContinuousLinearMap with
+      map_mul' := fun _ _ ↦ rfl
+      map_star' := adjoint_toContinuousLinearMap }
+
+lemma coe_toEuclideanClm_eq_toEuclideanLin (A : Matrix n n 𝕜) :
+    (toEuclideanClm (n := n) (𝕜 := 𝕜) A : _ →ₗ[𝕜] _) = toEuclideanLin A :=
+  rfl
+
+@[simp]
+lemma toEuclideanClm_piLp_equiv_symm (A : Matrix n n 𝕜) (x : n → 𝕜) :
+    toEuclideanClm (n := n) (𝕜 := 𝕜) A ((WithLp.equiv _ _).symm x) =
+      (WithLp.equiv _ _).symm (toLin' A x) :=
+  rfl
+
+@[simp]
+lemma piLp_equiv_toEuclideanClm (A : Matrix n n 𝕜) (x : EuclideanSpace 𝕜 n) :
+    WithLp.equiv _ _ (toEuclideanClm (n := n) (𝕜 := 𝕜) A x) =
+      toLin' A (WithLp.equiv _ _ x) :=
+  rfl
+
+/-- An auxiliary definition used only to construct the true `NormedAddCommGroup` (and `Metric`)
+structure provided by `Matrix.instMetricSpaceL2Op` and `Matrix.instNormedAddCommGroupL2Op`.  -/
+def l2OpNormedAddCommGroupAux : NormedAddCommGroup (Matrix m n 𝕜) :=
+  @NormedAddCommGroup.induced ((Matrix m n 𝕜) ≃ₗ[𝕜] (EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m))
+    _ _ _ ContinuousLinearMap.toNormedAddCommGroup.toNormedAddGroup _ _ <|
+    (toEuclideanLin.trans toContinuousLinearMap).injective
+
+/-- An auxiliary definition used only to construct the true `NormedRing` (and `Metric`) structure
+provided by `Matrix.instMetricSpaceL2Op` and `Matrix.instNormedRingL2Op`.  -/
+def l2OpNormedRingAux : NormedRing (Matrix n n 𝕜) :=
+  @NormedRing.induced ((Matrix n n 𝕜) ≃⋆ₐ[𝕜] (EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n))
+    _ _ _ ContinuousLinearMap.toNormedRing _ _ toEuclideanClm.injective
+
+open Bornology Filter
+open scoped Topology Uniformity
+
+/-- 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
+  `UniformAddGroup.toUniformSpace_eq`. -/
+  letI normed_add_comm_group : NormedAddCommGroup (Matrix m n 𝕜) :=
+    { l2OpNormedAddCommGroupAux.replaceTopology <|
+        (toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap
+        |>.toContinuousLinearEquiv.toHomeomorph.inducing.induced with
+      norm := l2OpNormedAddCommGroupAux.norm
+      dist_eq := l2OpNormedAddCommGroupAux.dist_eq }
+  exact normed_add_comm_group.replaceUniformity <| by
+    congr
+    rw [← @UniformAddGroup.toUniformSpace_eq _ (instUniformSpaceMatrix m n 𝕜) _ _]
+    rw [@UniformAddGroup.toUniformSpace_eq _ PseudoEMetricSpace.toUniformSpace _ _]
+
+scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instL2OpMetricSpace
+
+open scoped Matrix.L2OpNorm
+
+/-- The norm structure on `Matrix m n 𝕜` arising from the operator norm given by the identification
+with (continuous) linear maps of `EuclideanSpace`. -/
+def instL2OpNormedAddCommGroup : NormedAddCommGroup (Matrix m n 𝕜) where
+  norm := l2OpNormedAddCommGroupAux.norm
+  dist_eq := l2OpNormedAddCommGroupAux.dist_eq
+
+scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instL2OpNormedAddCommGroup
+
+lemma l2_op_norm_def (A : Matrix m n 𝕜) :
+    ‖A‖ = ‖(toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap A‖ := rfl
+
+lemma l2_op_nnnorm_def (A : Matrix m n 𝕜) :
+    ‖A‖₊ = ‖(toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap A‖₊ := rfl
+
+lemma l2_op_norm_conjTranspose (A : Matrix m n 𝕜) : ‖Aᴴ‖ = ‖A‖ := by
+  rw [l2_op_norm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
+    toLin_conjTranspose, adjoint_toContinuousLinearMap]
+  exact ContinuousLinearMap.adjoint.norm_map _
+
+lemma l2_op_norm_conjTranspose_mul_self (A : Matrix m n 𝕜) : ‖Aᴴ * A‖ = ‖A‖ * ‖A‖ := by
+  rw [l2_op_norm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
+    Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
+  exact ContinuousLinearMap.norm_adjoint_comp_self _
+
+-- note: with only a type ascription in the left-hand side, Lean picks the wrong norm.
+lemma l2_op_norm_mulVec (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
+    ‖(EuclideanSpace.equiv m 𝕜).symm <| A.mulVec x‖ ≤ ‖A‖ * ‖x‖ :=
+  toEuclideanLin (n := n) (m := m) (𝕜 := 𝕜) |>.trans toContinuousLinearMap A |>.le_op_norm x
+
+lemma l2_op_nnnorm_mulVec (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
+    ‖(EuclideanSpace.equiv m 𝕜).symm <| A.mulVec x‖₊ ≤ ‖A‖₊ * ‖x‖₊ :=
+  A.l2_op_norm_mulVec x
+
+lemma l2_op_norm_mul (A : Matrix m n 𝕜) (B : Matrix n l 𝕜) :
+    ‖A * B‖ ≤ ‖A‖ * ‖B‖ := by
+  simp only [l2_op_norm_def]
+  have := (toEuclideanLin (n := n) (m := m) (𝕜 := 𝕜) ≪≫ₗ toContinuousLinearMap) A
+    |>.op_norm_comp_le <| (toEuclideanLin (n := l) (m := n) (𝕜 := 𝕜) ≪≫ₗ toContinuousLinearMap) B
+  convert this
+  ext1 x
+  exact congr($(Matrix.toLin'_mul A B) x)
+
+lemma l2_op_nnnorm_mul (A : Matrix m n 𝕜) (B : Matrix n l 𝕜) : ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊ :=
+  l2_op_norm_mul A B
+
+/-- The normed algebra structure on `Matrix n n 𝕜` arising from the operator norm given by the
+identification with (continuous) linear endmorphisms of `EuclideanSpace 𝕜 n`. -/
+def instL2OpNormedSpace : NormedSpace 𝕜 (Matrix m n 𝕜) where
+  norm_smul_le r x := by
+    rw [l2_op_norm_def, LinearEquiv.map_smul]
+    exact norm_smul_le r ((toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap x)
+
+scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instL2OpNormedSpace
+
+/-- The normed ring structure on `Matrix n n 𝕜` arising from the operator norm given by the
+identification with (continuous) linear endmorphisms of `EuclideanSpace 𝕜 n`. -/
+def instL2OpNormedRing : NormedRing (Matrix n n 𝕜) where
+  dist_eq := l2OpNormedRingAux.dist_eq
+  norm_mul := l2OpNormedRingAux.norm_mul
+
+scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instL2OpNormedRing
+
+/-- This is the same as `Matrix.l2_op_norm_def`, but with a more bundled RHS for square matrices. -/
+lemma cstar_norm_def (A : Matrix n n 𝕜) : ‖A‖ = ‖toEuclideanClm (n := n) (𝕜 := 𝕜) A‖ := rfl
+
+/-- This is the same as `Matrix.l2_op_nnnorm_def`, but with a more bundled RHS for square
+matrices. -/
+lemma cstar_nnnorm_def (A : Matrix n n 𝕜) : ‖A‖₊ = ‖toEuclideanClm (n := n) (𝕜 := 𝕜) A‖₊ := rfl
+
+/-- The normed algebra structure on `Matrix n n 𝕜` arising from the operator norm given by the
+identification with (continuous) linear endmorphisms of `EuclideanSpace 𝕜 n`. -/
+def instL2OpNormedAlgebra : NormedAlgebra 𝕜 (Matrix n n 𝕜) where
+  norm_smul_le := norm_smul_le
+
+scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instL2OpNormedAlgebra
+
+/-- The operator norm on `Matrix n n 𝕜` given by the identification with (continuous) linear
+endmorphisms of `EuclideanSpace 𝕜 n` makes it into a `L2OpRing`. -/
+lemma instCstarRing : CstarRing (Matrix n n 𝕜) where
+  norm_star_mul_self := l2_op_norm_conjTranspose_mul_self _
+
+scoped[Matrix.L2OpNorm] attribute [instance] Matrix.instCstarRing
+
+end Matrix
+
+end L2OpNorm