The operator norm as a unitarily invariant seminorm

On linear maps A : E →ₗ[𝕜] F out of a finite-dimensional inner product space, every linear map is continuous, and the operator norm ‖A‖ of the continuous linear map LinearMap.toContinuousLinearMap A is a seminorm on E →ₗ[𝕜] F. Composing with unitaries of the source or the target does not change it, so it is a unitarily invariant seminorm. Only the source needs to be finite-dimensional.

Main declarations

• TauCeti.UnitarilyInvariantSeminorm.opNorm: the operator norm as a unitarily invariant seminorm on E →ₗ[𝕜] F.
• TauCeti.UnitarilyInvariantSeminorm.opNorm_apply: its value is the operator norm of the associated continuous linear map.

References

• R. Bhatia, Matrix Analysis, Graduate Texts in Mathematics 169, Springer, 1997, Section IV.2.

noncomputable def TauCeti.UnitarilyInvariantSeminorm.opNorm (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : UnitarilyInvariantSeminorm 𝕜 E F

The operator norm A ↦ ‖A‖ on linear maps out of a finite-dimensional inner product space, as a unitarily invariant seminorm.

@[simp]

theorem TauCeti.UnitarilyInvariantSeminorm.opNorm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ[𝕜] F) : (opNorm 𝕜 E F) A = ‖LinearMap.toContinuousLinearMap A‖

The operator-norm seminorm evaluates to the operator norm of the associated continuous linear map.