# 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 bound 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β.
theorem entry_norm_bound_of_unitary {π : Type u_1} {n : Type u_3} [RCLike π] [] [] {U : Matrix n n π} (hU : U β Matrix.unitaryGroup n π) (i : n) (j : n) :
theorem entrywise_sup_norm_bound_of_unitary {π : Type u_1} {n : Type u_3} [RCLike π] [] [] {U : Matrix n n π} (hU : U β Matrix.unitaryGroup n π) :

The entrywise sup norm of a unitary matrix is at most 1.

def Matrix.toEuclideanCLM {π : Type u_1} {n : Type u_3} [RCLike π] [] [] :
Matrix n n π βββ[π] EuclideanSpace π n βL[π] EuclideanSpace π n

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Matrix.coe_toEuclideanCLM_eq_toEuclideanLin {π : Type u_1} {n : Type u_3} [RCLike π] [] [] (A : Matrix n n π) :
β(Matrix.toEuclideanCLM A) = Matrix.toEuclideanLin A
@[simp]
theorem Matrix.toEuclideanCLM_piLp_equiv_symm {π : Type u_1} {n : Type u_3} [RCLike π] [] [] (A : Matrix n n π) (x : n β π) :
(Matrix.toEuclideanCLM A) ((WithLp.equiv 2 ((i : n) β (fun (x : n) => π) i)).symm x) = (WithLp.equiv 2 (n β π)).symm ((Matrix.toLin' A) x)
@[simp]
theorem Matrix.piLp_equiv_toEuclideanCLM {π : Type u_1} {n : Type u_3} [RCLike π] [] [] (A : Matrix n n π) (x : EuclideanSpace π n) :
(WithLp.equiv 2 ((i : n) β (fun (x : n) => π) i)) ((Matrix.toEuclideanCLM A) x) = (Matrix.toLin' A) ((WithLp.equiv 2 (n β π)) x)
def Matrix.l2OpNormedAddCommGroupAux {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] :
NormedAddCommGroup (Matrix m n π)

An auxiliary definition used only to construct the true NormedAddCommGroup (and Metric) structure provided by Matrix.instMetricSpaceL2Op and Matrix.instNormedAddCommGroupL2Op.

Equations
Instances For
def Matrix.l2OpNormedRingAux {π : Type u_1} {n : Type u_3} [RCLike π] [] [] :
NormedRing (Matrix n n π)

An auxiliary definition used only to construct the true NormedRing (and Metric) structure provided by Matrix.instMetricSpaceL2Op and Matrix.instNormedRingL2Op.

Equations
Instances For
def Matrix.instL2OpMetricSpace {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] :
MetricSpace (Matrix m n π)

The metric on Matrix m n π arising from the operator norm given by the identification with (continuous) linear maps of EuclideanSpace.

Equations
• Matrix.instL2OpMetricSpace = NormedAddCommGroup.toMetricSpace.replaceUniformity β―
Instances For
def Matrix.instL2OpNormedAddCommGroup {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] :
NormedAddCommGroup (Matrix m n π)

The norm structure on Matrix m n π arising from the operator norm given by the identification with (continuous) linear maps of EuclideanSpace.

Equations
Instances For
theorem Matrix.l2_opNorm_def {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) :
= β(Matrix.toEuclideanLin βͺβ«β LinearMap.toContinuousLinearMap) Aβ
@[deprecated Matrix.l2_opNorm_def]
theorem Matrix.l2_op_norm_def {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) :
= β(Matrix.toEuclideanLin βͺβ«β LinearMap.toContinuousLinearMap) Aβ

Alias of Matrix.l2_opNorm_def.

theorem Matrix.l2_opNNNorm_def {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) :
= β(Matrix.toEuclideanLin βͺβ«β LinearMap.toContinuousLinearMap) Aββ
@[deprecated Matrix.l2_opNNNorm_def]
theorem Matrix.l2_op_nnnorm_def {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) :
= β(Matrix.toEuclideanLin βͺβ«β LinearMap.toContinuousLinearMap) Aββ

Alias of Matrix.l2_opNNNorm_def.

theorem Matrix.l2_opNorm_conjTranspose {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] [] (A : Matrix m n π) :
βA.conjTransposeβ =
@[deprecated Matrix.l2_opNorm_conjTranspose]
theorem Matrix.l2_op_norm_conjTranspose {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] [] (A : Matrix m n π) :
βA.conjTransposeβ =

Alias of Matrix.l2_opNorm_conjTranspose.

theorem Matrix.l2_opNNNorm_conjTranspose {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] [] (A : Matrix m n π) :
βA.conjTransposeββ =
@[deprecated Matrix.l2_opNNNorm_conjTranspose]
theorem Matrix.l2_op_nnnorm_conjTranspose {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] [] (A : Matrix m n π) :
βA.conjTransposeββ =

Alias of Matrix.l2_opNNNorm_conjTranspose.

theorem Matrix.l2_opNorm_conjTranspose_mul_self {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) :
βA.conjTranspose * Aβ =
@[deprecated Matrix.l2_opNorm_conjTranspose_mul_self]
theorem Matrix.l2_op_norm_conjTranspose_mul_self {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) :
βA.conjTranspose * Aβ =

Alias of Matrix.l2_opNorm_conjTranspose_mul_self.

theorem Matrix.l2_opNNNorm_conjTranspose_mul_self {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) :
βA.conjTranspose * Aββ =
@[deprecated Matrix.l2_opNNNorm_conjTranspose_mul_self]
theorem Matrix.l2_op_nnnorm_conjTranspose_mul_self {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) :
βA.conjTranspose * Aββ =

Alias of Matrix.l2_opNNNorm_conjTranspose_mul_self.

theorem Matrix.l2_opNorm_mulVec {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) (x : EuclideanSpace π n) :
β(EuclideanSpace.equiv m π).symm (A.mulVec x)β β€
@[deprecated Matrix.l2_opNorm_mulVec]
theorem Matrix.l2_op_norm_mulVec {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) (x : EuclideanSpace π n) :
β(EuclideanSpace.equiv m π).symm (A.mulVec x)β β€

Alias of Matrix.l2_opNorm_mulVec.

theorem Matrix.l2_opNNNorm_mulVec {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) (x : EuclideanSpace π n) :
β(EuclideanSpace.equiv m π).symm (A.mulVec x)ββ β€
@[deprecated Matrix.l2_opNNNorm_mulVec]
theorem Matrix.l2_op_nnnorm_mulVec {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] (A : Matrix m n π) (x : EuclideanSpace π n) :
β(EuclideanSpace.equiv m π).symm (A.mulVec x)ββ β€

Alias of Matrix.l2_opNNNorm_mulVec.

theorem Matrix.l2_opNorm_mul {π : Type u_1} {m : Type u_2} {n : Type u_3} {l : Type u_4} [RCLike π] [] [] [] [] [] (A : Matrix m n π) (B : Matrix n l π) :
@[deprecated Matrix.l2_opNorm_mul]
theorem Matrix.l2_op_norm_mul {π : Type u_1} {m : Type u_2} {n : Type u_3} {l : Type u_4} [RCLike π] [] [] [] [] [] (A : Matrix m n π) (B : Matrix n l π) :

Alias of Matrix.l2_opNorm_mul.

theorem Matrix.l2_opNNNorm_mul {π : Type u_1} {m : Type u_2} {n : Type u_3} {l : Type u_4} [RCLike π] [] [] [] [] [] (A : Matrix m n π) (B : Matrix n l π) :
@[deprecated Matrix.l2_opNNNorm_mul]
theorem Matrix.l2_op_nnnorm_mul {π : Type u_1} {m : Type u_2} {n : Type u_3} {l : Type u_4} [RCLike π] [] [] [] [] [] (A : Matrix m n π) (B : Matrix n l π) :

Alias of Matrix.l2_opNNNorm_mul.

def Matrix.instL2OpNormedSpace {π : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike π] [] [] [] :
NormedSpace π (Matrix m n π)

The normed algebra structure on Matrix n n π arising from the operator norm given by the identification with (continuous) linear endmorphisms of EuclideanSpace π n.

Equations
• Matrix.instL2OpNormedSpace =
Instances For
def Matrix.instL2OpNormedRing {π : Type u_1} {n : Type u_3} [RCLike π] [] [] :
NormedRing (Matrix n n π)

The normed ring structure on Matrix n n π arising from the operator norm given by the identification with (continuous) linear endmorphisms of EuclideanSpace π n.

Equations
Instances For
theorem Matrix.cstar_norm_def {π : Type u_1} {n : Type u_3} [RCLike π] [] [] (A : Matrix n n π) :
= βMatrix.toEuclideanCLM Aβ

This is the same as Matrix.l2_opNorm_def, but with a more bundled RHS for square matrices.

theorem Matrix.cstar_nnnorm_def {π : Type u_1} {n : Type u_3} [RCLike π] [] [] (A : Matrix n n π) :
= βMatrix.toEuclideanCLM Aββ

This is the same as Matrix.l2_opNNNorm_def, but with a more bundled RHS for square matrices.

def Matrix.instL2OpNormedAlgebra {π : Type u_1} {n : Type u_3} [RCLike π] [] [] :
NormedAlgebra π (Matrix n n π)

The normed algebra structure on Matrix n n π arising from the operator norm given by the identification with (continuous) linear endmorphisms of EuclideanSpace π n.

Equations
• Matrix.instL2OpNormedAlgebra =
Instances For
theorem Matrix.instCstarRing {π : Type u_1} {n : Type u_3} [RCLike π] [] [] :
CstarRing (Matrix n n π)

The operator norm on Matrix n n π given by the identification with (continuous) linear endmorphisms of EuclideanSpace π n makes it into a L2OpRing.