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 Mathlib/Analysis/Matrix.lean 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.Norms.L2Operator 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.

theorem entry_norm_bound_of_unitary {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] {U : Matrix n n 𝕜} (hU : U ∈ Matrix.unitaryGroup n 𝕜) (i j : n) : ‖U i j‖ ≤ 1

theorem entrywise_sup_norm_bound_of_unitary {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] {U : Matrix n n 𝕜} (hU : U ∈ Matrix.unitaryGroup n 𝕜) : ‖U‖ ≤ 1

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

noncomputable def Matrix.toEuclideanCLM {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] : Matrix n n 𝕜 ≃⋆ₐ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n

The natural star algebra equivalence between matrices and continuous linear endomorphisms 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.

theorem Matrix.coe_toEuclideanCLM_eq_toEuclideanLin {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) : ↑(toEuclideanCLM A) = toEuclideanLin A

@[simp]

theorem Matrix.toEuclideanCLM_toLp {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) (x : n → 𝕜) : (toEuclideanCLM A) (WithLp.toLp 2 x) = WithLp.toLp 2 (A.mulVec x)

@[simp]

theorem Matrix.ofLp_toEuclideanCLM {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) (x : EuclideanSpace 𝕜 n) : ((toEuclideanCLM A) x).ofLp = A.mulVec x.ofLp

theorem Matrix.inner_toEuclideanCLM {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) (x y : EuclideanSpace ℝ n) : inner ℝ x ((toEuclideanCLM A) y) = x.ofLp ⬝ᵥ A.mulVec y.ofLp

@[implicit_reducible]

noncomputable def Matrix.l2OpNormedAddCommGroupAux {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] : 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

• Matrix.l2OpNormedAddCommGroupAux = NormedAddCommGroup.induced (Matrix m n 𝕜) (EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m) (Matrix.toEuclideanLin.trans LinearMap.toContinuousLinearMap) ⋯

@[implicit_reducible]

noncomputable def Matrix.l2OpNormedRingAux {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] : 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

• Matrix.l2OpNormedRingAux = NormedRing.induced (Matrix n n 𝕜) (EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) Matrix.toEuclideanCLM ⋯

@[implicit_reducible]

noncomputable def Matrix.instL2OpMetricSpace {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] : 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

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable def Matrix.instL2OpNormedAddCommGroup {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] : 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

• Matrix.instL2OpNormedAddCommGroup = { toNorm := Matrix.l2OpNormedAddCommGroupAux.toNorm, toAddCommGroup := Matrix.addCommGroup, toMetricSpace := Matrix.instL2OpMetricSpace, dist_eq := ⋯ }

theorem Matrix.l2_opNorm_def {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) : ‖A‖ = ‖(toEuclideanLin ≪≫ₗ LinearMap.toContinuousLinearMap) A‖

theorem Matrix.l2_opNNNorm_def {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) : ‖A‖₊ = ‖(toEuclideanLin ≪≫ₗ LinearMap.toContinuousLinearMap) A‖₊

theorem Matrix.l2_opNorm_conjTranspose {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] [DecidableEq m] (A : Matrix m n 𝕜) : ‖A.conjTranspose‖ = ‖A‖

theorem Matrix.l2_opNNNorm_conjTranspose {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] [DecidableEq m] (A : Matrix m n 𝕜) : ‖A.conjTranspose‖₊ = ‖A‖₊

theorem Matrix.l2_opNorm_conjTranspose_mul_self {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) : ‖A.conjTranspose * A‖ = ‖A‖ * ‖A‖

theorem Matrix.l2_opNNNorm_conjTranspose_mul_self {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) : ‖A.conjTranspose * A‖₊ = ‖A‖₊ * ‖A‖₊

theorem Matrix.l2_opNorm_mulVec {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) : ‖(EuclideanSpace.equiv m 𝕜).symm (A.mulVec x.ofLp)‖ ≤ ‖A‖ * ‖x‖

theorem Matrix.l2_opNNNorm_mulVec {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) : ‖(EuclideanSpace.equiv m 𝕜).symm (A.mulVec x.ofLp)‖₊ ≤ ‖A‖₊ * ‖x‖₊

theorem Matrix.l2_opNorm_mul {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} {l : Type u_4} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] [Fintype l] [DecidableEq l] (A : Matrix m n 𝕜) (B : Matrix n l 𝕜) : ‖A * B‖ ≤ ‖A‖ * ‖B‖

theorem Matrix.l2_opNNNorm_mul {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} {l : Type u_4} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] [Fintype l] [DecidableEq l] (A : Matrix m n 𝕜) (B : Matrix n l 𝕜) : ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

theorem Matrix.l2_opNorm_toEuclideanCLM {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) : ‖toEuclideanCLM A‖ = ‖A‖

@[simp]

theorem Matrix.l2_opNorm_diagonal {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] (v : n → 𝕜) : ‖diagonal v‖ = ‖v‖

@[simp]

theorem Matrix.l2_opNNNorm_diagonal {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] (v : n → 𝕜) : ‖diagonal v‖₊ = ‖v‖₊

@[implicit_reducible]

def Matrix.instL2OpNormedSpace {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [Fintype n] [DecidableEq n] : 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 = { toModule := Matrix.module, norm_smul_le := ⋯ }

@[implicit_reducible]

noncomputable def Matrix.instL2OpNormedRing {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] : 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

• Matrix.instL2OpNormedRing = { toNorm := Matrix.instL2OpNormedAddCommGroup.toNorm, toRing := Matrix.instRing, toMetricSpace := Matrix.instL2OpMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }

theorem Matrix.cstar_norm_def {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) : ‖A‖ = ‖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 𝕜] [Fintype n] [DecidableEq n] (A : Matrix n n 𝕜) : ‖A‖₊ = ‖toEuclideanCLM A‖₊

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

@[implicit_reducible]

def Matrix.instL2OpNormedAlgebra {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] : 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 = { toAlgebra := Matrix.instAlgebra, norm_smul_le := ⋯ }

theorem Matrix.instCStarRing {𝕜 : Type u_1} {n : Type u_3} [RCLike 𝕜] [Fintype n] [DecidableEq n] : 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.