Documentation

Mathlib.Analysis.CStarAlgebra.Matrix

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 #

Main statements #

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 #

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 : n) (j : n) :
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 π•œ) :

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

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 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 π•œ] [Fintype n] [DecidableEq n] (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 π•œ] [Fintype n] [DecidableEq n] (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 π•œ] [Fintype n] [DecidableEq n] (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 π•œ] [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
    Instances For
      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
      Instances For
        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
        • Matrix.instL2OpMetricSpace = NormedAddCommGroup.toMetricSpace.replaceUniformity β‹―
        Instances For
          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
          Instances For
            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β€– = β€–(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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n π•œ) :
            β€–Aβ€– = β€–(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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n π•œ) :
            β€–Aβ€–β‚Š = β€–(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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n π•œ) :
            β€–Aβ€–β‚Š = β€–(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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] [DecidableEq m] (A : Matrix m n π•œ) :
            β€–A.conjTransposeβ€– = β€–Aβ€–
            @[deprecated Matrix.l2_opNorm_conjTranspose]
            theorem Matrix.l2_op_norm_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β€–

            Alias of Matrix.l2_opNorm_conjTranspose.

            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 π•œ) :
            @[deprecated Matrix.l2_opNNNorm_conjTranspose]
            theorem Matrix.l2_op_nnnorm_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 π•œ) :

            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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n π•œ) :
            @[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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n π•œ) :

            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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n π•œ) :
            @[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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n π•œ) :

            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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m n π•œ) (x : EuclideanSpace π•œ n) :
            @[deprecated Matrix.l2_opNorm_mulVec]
            theorem Matrix.l2_op_norm_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) :

            Alias of Matrix.l2_opNorm_mulVec.

            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) :
            @[deprecated Matrix.l2_opNNNorm_mulVec]
            theorem Matrix.l2_op_nnnorm_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) :

            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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] [Fintype l] [DecidableEq l] (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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] [Fintype l] [DecidableEq l] (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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] [Fintype l] [DecidableEq l] (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 π•œ] [Fintype m] [Fintype n] [DecidableEq n] [Fintype l] [DecidableEq l] (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 π•œ] [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
            Instances For
              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
              Instances For
                theorem Matrix.cstar_norm_def {π•œ : Type u_1} {n : Type u_3} [RCLike π•œ] [Fintype n] [DecidableEq n] (A : Matrix n n π•œ) :
                β€–Aβ€– = β€–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 π•œ] [Fintype n] [DecidableEq n] (A : Matrix n n π•œ) :
                β€–Aβ€–β‚Š = β€–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 π•œ] [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
                Instances For
                  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.