l2OpNormedRingAux — Mathlib

English

The L2-operator norm of a matrix equals the operator norm of the corresponding Euclidean endomorphism.

Русский

L2-операторная норма матрицы равна операторной норме соответствующего унитарного отображения Евклидова пространства.

LaTeX

$$$\\|A\\| = \\|(toEuclideanLin(𝕜)(m)(n)).trans toContinuousLinearMap A\\|$$$

Lean4

/-- 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

Похожие утверждения