Documentation

Mathlib.Analysis.Matrix

Matrices as a normed space #

In this file we provide the following non-instances for norms on matrices:

These are not declared as instances because there are several natural choices for defining the norm of a matrix.

The norm induced by the identification of Matrix m n š•œ with EuclideanSpace n š•œ ā†’L[š•œ] EuclideanSpace m š•œ (i.e., the ā„“Ā² operator norm) can be found in Analysis.NormedSpace.Star.Matrix. It is separated to avoid extraneous imports in this file.

The elementwise supremum norm #

def Matrix.seminormedAddCommGroup {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] :

Seminormed group instance (using sup norm of sup norm) for matrices over a seminormed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
  • Matrix.seminormedAddCommGroup = Pi.seminormedAddCommGroup
Instances For
    theorem Matrix.norm_def {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
    ā€–Aā€– = ā€–fun (i : m) (j : n) => A i jā€–
    theorem Matrix.norm_eq_sup_sup_nnnorm {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
    ā€–Aā€– = ā†‘(Finset.univ.sup fun (i : m) => Finset.univ.sup fun (j : n) => ā€–A i jā€–ā‚Š)

    The norm of a matrix is the sup of the sup of the nnnorm of the entries

    theorem Matrix.nnnorm_def {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
    ā€–Aā€–ā‚Š = ā€–fun (i : m) (j : n) => A i jā€–ā‚Š
    theorem Matrix.norm_le_iff {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] {r : ā„} (hr : 0 ā‰¤ r) {A : Matrix m n Ī±} :
    ā€–Aā€– ā‰¤ r ā†” āˆ€ (i : m) (j : n), ā€–A i jā€– ā‰¤ r
    theorem Matrix.nnnorm_le_iff {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] {r : NNReal} {A : Matrix m n Ī±} :
    ā€–Aā€–ā‚Š ā‰¤ r ā†” āˆ€ (i : m) (j : n), ā€–A i jā€–ā‚Š ā‰¤ r
    theorem Matrix.norm_lt_iff {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] {r : ā„} (hr : 0 < r) {A : Matrix m n Ī±} :
    ā€–Aā€– < r ā†” āˆ€ (i : m) (j : n), ā€–A i jā€– < r
    theorem Matrix.nnnorm_lt_iff {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] {r : NNReal} (hr : 0 < r) {A : Matrix m n Ī±} :
    ā€–Aā€–ā‚Š < r ā†” āˆ€ (i : m) (j : n), ā€–A i jā€–ā‚Š < r
    theorem Matrix.norm_entry_le_entrywise_sup_norm {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) {i : m} {j : n} :
    theorem Matrix.nnnorm_entry_le_entrywise_sup_nnnorm {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) {i : m} {j : n} :
    @[simp]
    theorem Matrix.nnnorm_map_eq {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} {Ī² : Type u_6} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] [SeminormedAddCommGroup Ī²] (A : Matrix m n Ī±) (f : Ī± ā†’ Ī²) (hf : āˆ€ (a : Ī±), ā€–f aā€–ā‚Š = ā€–aā€–ā‚Š) :
    @[simp]
    theorem Matrix.norm_map_eq {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} {Ī² : Type u_6} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] [SeminormedAddCommGroup Ī²] (A : Matrix m n Ī±) (f : Ī± ā†’ Ī²) (hf : āˆ€ (a : Ī±), ā€–f aā€– = ā€–aā€–) :
    @[simp]
    theorem Matrix.nnnorm_transpose {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
    @[simp]
    theorem Matrix.norm_transpose {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
    @[simp]
    theorem Matrix.nnnorm_conjTranspose {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] [StarAddMonoid Ī±] [NormedStarGroup Ī±] (A : Matrix m n Ī±) :
    @[simp]
    theorem Matrix.norm_conjTranspose {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] [StarAddMonoid Ī±] [NormedStarGroup Ī±] (A : Matrix m n Ī±) :
    ā€–A.conjTransposeā€– = ā€–Aā€–
    instance Matrix.instNormedStarGroup {m : Type u_3} {Ī± : Type u_5} [Fintype m] [SeminormedAddCommGroup Ī±] [StarAddMonoid Ī±] [NormedStarGroup Ī±] :
    Equations
    • ā‹Æ = ā‹Æ
    @[simp]
    theorem Matrix.nnnorm_col {m : Type u_3} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype m] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : m ā†’ Ī±) :
    @[simp]
    theorem Matrix.norm_col {m : Type u_3} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype m] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : m ā†’ Ī±) :
    @[simp]
    theorem Matrix.nnnorm_row {n : Type u_4} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype n] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : n ā†’ Ī±) :
    @[simp]
    theorem Matrix.norm_row {n : Type u_4} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype n] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : n ā†’ Ī±) :
    @[simp]
    @[simp]
    theorem Matrix.norm_diagonal {n : Type u_4} {Ī± : Type u_5} [Fintype n] [SeminormedAddCommGroup Ī±] [DecidableEq n] (v : n ā†’ Ī±) :
    instance Matrix.instNormOneClassOfNonempty {n : Type u_4} {Ī± : Type u_5} [Fintype n] [SeminormedAddCommGroup Ī±] [Nonempty n] [DecidableEq n] [One Ī±] [NormOneClass Ī±] :
    NormOneClass (Matrix n n Ī±)

    Note this is safe as an instance as it carries no data.

    Equations
    • ā‹Æ = ā‹Æ
    def Matrix.normedAddCommGroup {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NormedAddCommGroup Ī±] :

    Normed group instance (using sup norm of sup norm) for matrices over a normed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

    Equations
    • Matrix.normedAddCommGroup = Pi.normedAddCommGroup
    Instances For
      theorem Matrix.boundedSMul {R : Type u_1} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedRing R] [SeminormedAddCommGroup Ī±] [Module R Ī±] [BoundedSMul R Ī±] :
      BoundedSMul R (Matrix m n Ī±)

      This applies to the sup norm of sup norm.

      def Matrix.normedSpace {R : Type u_1} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NormedField R] [SeminormedAddCommGroup Ī±] [NormedSpace R Ī±] :
      NormedSpace R (Matrix m n Ī±)

      Normed space instance (using sup norm of sup norm) for matrices over a normed space. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

      Equations
      • Matrix.normedSpace = Pi.normedSpace
      Instances For

        The $L_\infty$ operator norm #

        This section defines the matrix norm $\|A\|_\infty = \operatorname{sup}_i (\sum_j \|A_{ij}\|)$.

        Note that this is equivalent to the operator norm, considering $A$ as a linear map between two $L^\infty$ spaces.

        Seminormed group instance (using sup norm of L1 norm) for matrices over a seminormed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

        Equations
        • Matrix.linftyOpSeminormedAddCommGroup = inferInstance
        Instances For
          def Matrix.linftyOpNormedAddCommGroup {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NormedAddCommGroup Ī±] :

          Normed group instance (using sup norm of L1 norm) for matrices over a normed ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

          Equations
          • Matrix.linftyOpNormedAddCommGroup = inferInstance
          Instances For
            theorem Matrix.linftyOpBoundedSMul {R : Type u_1} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedRing R] [SeminormedAddCommGroup Ī±] [Module R Ī±] [BoundedSMul R Ī±] :
            BoundedSMul R (Matrix m n Ī±)

            This applies to the sup norm of L1 norm.

            def Matrix.linftyOpNormedSpace {R : Type u_1} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NormedField R] [SeminormedAddCommGroup Ī±] [NormedSpace R Ī±] :
            NormedSpace R (Matrix m n Ī±)

            Normed space instance (using sup norm of L1 norm) for matrices over a normed space. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

            Equations
            • Matrix.linftyOpNormedSpace = inferInstance
            Instances For
              theorem Matrix.linfty_opNorm_def {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
              ā€–Aā€– = ā†‘(Finset.univ.sup fun (i : m) => āˆ‘ j : n, ā€–A i jā€–ā‚Š)
              @[deprecated Matrix.linfty_opNorm_def]
              theorem Matrix.linfty_op_norm_def {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
              ā€–Aā€– = ā†‘(Finset.univ.sup fun (i : m) => āˆ‘ j : n, ā€–A i jā€–ā‚Š)

              Alias of Matrix.linfty_opNorm_def.

              theorem Matrix.linfty_opNNNorm_def {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
              ā€–Aā€–ā‚Š = Finset.univ.sup fun (i : m) => āˆ‘ j : n, ā€–A i jā€–ā‚Š
              @[deprecated Matrix.linfty_opNNNorm_def]
              theorem Matrix.linfty_op_nnnorm_def {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
              ā€–Aā€–ā‚Š = Finset.univ.sup fun (i : m) => āˆ‘ j : n, ā€–A i jā€–ā‚Š

              Alias of Matrix.linfty_opNNNorm_def.

              @[simp]
              theorem Matrix.linfty_opNNNorm_col {m : Type u_3} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype m] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : m ā†’ Ī±) :
              @[deprecated Matrix.linfty_opNNNorm_col]
              theorem Matrix.linfty_op_nnnorm_col {m : Type u_3} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype m] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : m ā†’ Ī±) :

              Alias of Matrix.linfty_opNNNorm_col.

              @[simp]
              theorem Matrix.linfty_opNorm_col {m : Type u_3} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype m] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : m ā†’ Ī±) :
              @[deprecated Matrix.linfty_opNorm_col]
              theorem Matrix.linfty_op_norm_col {m : Type u_3} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype m] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : m ā†’ Ī±) :

              Alias of Matrix.linfty_opNorm_col.

              @[simp]
              theorem Matrix.linfty_opNNNorm_row {n : Type u_4} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype n] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : n ā†’ Ī±) :
              @[deprecated Matrix.linfty_opNNNorm_row]
              theorem Matrix.linfty_op_nnnorm_row {n : Type u_4} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype n] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : n ā†’ Ī±) :

              Alias of Matrix.linfty_opNNNorm_row.

              @[simp]
              theorem Matrix.linfty_opNorm_row {n : Type u_4} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype n] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : n ā†’ Ī±) :
              ā€–Matrix.row Ī¹ vā€– = āˆ‘ i : n, ā€–v iā€–
              @[deprecated Matrix.linfty_opNorm_row]
              theorem Matrix.linfty_op_norm_row {n : Type u_4} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype n] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : n ā†’ Ī±) :
              ā€–Matrix.row Ī¹ vā€– = āˆ‘ i : n, ā€–v iā€–

              Alias of Matrix.linfty_opNorm_row.

              @[deprecated Matrix.linfty_opNNNorm_diagonal]

              Alias of Matrix.linfty_opNNNorm_diagonal.

              @[simp]
              theorem Matrix.linfty_opNorm_diagonal {m : Type u_3} {Ī± : Type u_5} [Fintype m] [SeminormedAddCommGroup Ī±] [DecidableEq m] (v : m ā†’ Ī±) :
              @[deprecated Matrix.linfty_opNorm_diagonal]

              Alias of Matrix.linfty_opNorm_diagonal.

              theorem Matrix.linfty_opNNNorm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype l] [Fintype m] [Fintype n] [NonUnitalSeminormedRing Ī±] (A : Matrix l m Ī±) (B : Matrix m n Ī±) :
              @[deprecated Matrix.linfty_opNNNorm_mul]
              theorem Matrix.linfty_op_nnnorm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype l] [Fintype m] [Fintype n] [NonUnitalSeminormedRing Ī±] (A : Matrix l m Ī±) (B : Matrix m n Ī±) :

              Alias of Matrix.linfty_opNNNorm_mul.

              theorem Matrix.linfty_opNorm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype l] [Fintype m] [Fintype n] [NonUnitalSeminormedRing Ī±] (A : Matrix l m Ī±) (B : Matrix m n Ī±) :
              @[deprecated Matrix.linfty_opNorm_mul]
              theorem Matrix.linfty_op_norm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype l] [Fintype m] [Fintype n] [NonUnitalSeminormedRing Ī±] (A : Matrix l m Ī±) (B : Matrix m n Ī±) :

              Alias of Matrix.linfty_opNorm_mul.

              theorem Matrix.linfty_opNNNorm_mulVec {l : Type u_2} {m : Type u_3} {Ī± : Type u_5} [Fintype l] [Fintype m] [NonUnitalSeminormedRing Ī±] (A : Matrix l m Ī±) (v : m ā†’ Ī±) :
              @[deprecated Matrix.linfty_opNNNorm_mulVec]
              theorem Matrix.linfty_op_nnnorm_mulVec {l : Type u_2} {m : Type u_3} {Ī± : Type u_5} [Fintype l] [Fintype m] [NonUnitalSeminormedRing Ī±] (A : Matrix l m Ī±) (v : m ā†’ Ī±) :

              Alias of Matrix.linfty_opNNNorm_mulVec.

              theorem Matrix.linfty_opNorm_mulVec {l : Type u_2} {m : Type u_3} {Ī± : Type u_5} [Fintype l] [Fintype m] [NonUnitalSeminormedRing Ī±] (A : Matrix l m Ī±) (v : m ā†’ Ī±) :
              @[deprecated Matrix.linfty_opNorm_mulVec]
              theorem Matrix.linfty_op_norm_mulVec {l : Type u_2} {m : Type u_3} {Ī± : Type u_5} [Fintype l] [Fintype m] [NonUnitalSeminormedRing Ī±] (A : Matrix l m Ī±) (v : m ā†’ Ī±) :

              Alias of Matrix.linfty_opNorm_mulVec.

              Seminormed non-unital ring instance (using sup norm of L1 norm) for matrices over a semi normed non-unital ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

              Equations
              • Matrix.linftyOpNonUnitalSemiNormedRing = let __src := Matrix.linftyOpSeminormedAddCommGroup; let __src_1 := Matrix.instNonUnitalRing; NonUnitalSeminormedRing.mk ā‹Æ ā‹Æ
              Instances For
                instance Matrix.linfty_opNormOneClass {n : Type u_4} {Ī± : Type u_5} [Fintype n] [SeminormedRing Ī±] [NormOneClass Ī±] [DecidableEq n] [Nonempty n] :
                NormOneClass (Matrix n n Ī±)

                The Lā‚-Lāˆž norm preserves one on non-empty matrices. Note this is safe as an instance, as it carries no data.

                Equations
                • ā‹Æ = ā‹Æ
                def Matrix.linftyOpSemiNormedRing {n : Type u_4} {Ī± : Type u_5} [Fintype n] [SeminormedRing Ī±] [DecidableEq n] :

                Seminormed ring instance (using sup norm of L1 norm) for matrices over a semi normed ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

                Equations
                • Matrix.linftyOpSemiNormedRing = let __src := Matrix.linftyOpNonUnitalSemiNormedRing; let __src_1 := Matrix.instRing; SeminormedRing.mk ā‹Æ ā‹Æ
                Instances For

                  Normed non-unital ring instance (using sup norm of L1 norm) for matrices over a normed non-unital ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

                  Equations
                  • Matrix.linftyOpNonUnitalNormedRing = let __src := Matrix.linftyOpNonUnitalSemiNormedRing; NonUnitalNormedRing.mk ā‹Æ ā‹Æ
                  Instances For
                    def Matrix.linftyOpNormedRing {n : Type u_4} {Ī± : Type u_5} [Fintype n] [NormedRing Ī±] [DecidableEq n] :
                    NormedRing (Matrix n n Ī±)

                    Normed ring instance (using sup norm of L1 norm) for matrices over a normed ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

                    Equations
                    • Matrix.linftyOpNormedRing = let __src := Matrix.linftyOpSemiNormedRing; NormedRing.mk ā‹Æ ā‹Æ
                    Instances For
                      def Matrix.linftyOpNormedAlgebra {R : Type u_1} {n : Type u_4} {Ī± : Type u_5} [Fintype n] [NormedField R] [SeminormedRing Ī±] [NormedAlgebra R Ī±] [DecidableEq n] :
                      NormedAlgebra R (Matrix n n Ī±)

                      Normed algebra instance (using sup norm of L1 norm) for matrices over a normed algebra. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

                      Equations
                      • Matrix.linftyOpNormedAlgebra = let __src := Matrix.linftyOpNormedSpace; let __src_1 := Matrix.instAlgebra; NormedAlgebra.mk ā‹Æ
                      Instances For

                        For a matrix over a field, the norm defined in this section agrees with the operator norm on ContinuousLinearMaps between function types (which have the infinity norm).

                        theorem Matrix.linfty_opNNNorm_eq_opNNNorm {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NontriviallyNormedField Ī±] [NormedAlgebra ā„ Ī±] (A : Matrix m n Ī±) :
                        ā€–Aā€–ā‚Š = ā€–{ toLinearMap := A.mulVecLin, cont := ā‹Æ }ā€–ā‚Š
                        @[deprecated Matrix.linfty_opNNNorm_eq_opNNNorm]
                        theorem Matrix.linfty_op_nnnorm_eq_op_nnnorm {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NontriviallyNormedField Ī±] [NormedAlgebra ā„ Ī±] (A : Matrix m n Ī±) :
                        ā€–Aā€–ā‚Š = ā€–{ toLinearMap := A.mulVecLin, cont := ā‹Æ }ā€–ā‚Š

                        Alias of Matrix.linfty_opNNNorm_eq_opNNNorm.

                        theorem Matrix.linfty_opNorm_eq_opNorm {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NontriviallyNormedField Ī±] [NormedAlgebra ā„ Ī±] (A : Matrix m n Ī±) :
                        ā€–Aā€– = ā€–{ toLinearMap := A.mulVecLin, cont := ā‹Æ }ā€–
                        @[deprecated Matrix.linfty_opNorm_eq_opNorm]
                        theorem Matrix.linfty_op_norm_eq_op_norm {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NontriviallyNormedField Ī±] [NormedAlgebra ā„ Ī±] (A : Matrix m n Ī±) :
                        ā€–Aā€– = ā€–{ toLinearMap := A.mulVecLin, cont := ā‹Æ }ā€–

                        Alias of Matrix.linfty_opNorm_eq_opNorm.

                        @[simp]
                        theorem Matrix.linfty_opNNNorm_toMatrix {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NontriviallyNormedField Ī±] [NormedAlgebra ā„ Ī±] [DecidableEq n] (f : (n ā†’ Ī±) ā†’L[Ī±] m ā†’ Ī±) :
                        ā€–LinearMap.toMatrix' ā†‘fā€–ā‚Š = ā€–fā€–ā‚Š
                        @[deprecated Matrix.linfty_opNNNorm_toMatrix]
                        theorem Matrix.linfty_op_nnnorm_toMatrix {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NontriviallyNormedField Ī±] [NormedAlgebra ā„ Ī±] [DecidableEq n] (f : (n ā†’ Ī±) ā†’L[Ī±] m ā†’ Ī±) :
                        ā€–LinearMap.toMatrix' ā†‘fā€–ā‚Š = ā€–fā€–ā‚Š

                        Alias of Matrix.linfty_opNNNorm_toMatrix.

                        @[simp]
                        theorem Matrix.linfty_opNorm_toMatrix {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NontriviallyNormedField Ī±] [NormedAlgebra ā„ Ī±] [DecidableEq n] (f : (n ā†’ Ī±) ā†’L[Ī±] m ā†’ Ī±) :
                        ā€–LinearMap.toMatrix' ā†‘fā€– = ā€–fā€–
                        @[deprecated Matrix.linfty_opNorm_toMatrix]
                        theorem Matrix.linfty_op_norm_toMatrix {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NontriviallyNormedField Ī±] [NormedAlgebra ā„ Ī±] [DecidableEq n] (f : (n ā†’ Ī±) ā†’L[Ī±] m ā†’ Ī±) :
                        ā€–LinearMap.toMatrix' ā†‘fā€– = ā€–fā€–

                        Alias of Matrix.linfty_opNorm_toMatrix.

                        The Frobenius norm #

                        This is defined as $\|A\| = \sqrt{\sum_{i,j} \|A_{ij}\|^2}$. When the matrix is over the real or complex numbers, this norm is submultiplicative.

                        Seminormed group instance (using frobenius norm) for matrices over a seminormed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

                        Equations
                        Instances For
                          def Matrix.frobeniusNormedAddCommGroup {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NormedAddCommGroup Ī±] :

                          Normed group instance (using frobenius norm) for matrices over a normed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

                          Equations
                          • Matrix.frobeniusNormedAddCommGroup = inferInstance
                          Instances For
                            theorem Matrix.frobeniusBoundedSMul {R : Type u_1} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedRing R] [SeminormedAddCommGroup Ī±] [Module R Ī±] [BoundedSMul R Ī±] :
                            BoundedSMul R (Matrix m n Ī±)

                            This applies to the frobenius norm.

                            def Matrix.frobeniusNormedSpace {R : Type u_1} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [NormedField R] [SeminormedAddCommGroup Ī±] [NormedSpace R Ī±] :
                            NormedSpace R (Matrix m n Ī±)

                            Normed space instance (using frobenius norm) for matrices over a normed space. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

                            Equations
                            • Matrix.frobeniusNormedSpace = inferInstance
                            Instances For
                              theorem Matrix.frobenius_nnnorm_def {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
                              ā€–Aā€–ā‚Š = (āˆ‘ i : m, āˆ‘ j : n, ā€–A i jā€–ā‚Š ^ 2) ^ (1 / 2)
                              theorem Matrix.frobenius_norm_def {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
                              ā€–Aā€– = (āˆ‘ i : m, āˆ‘ j : n, ā€–A i jā€– ^ 2) ^ (1 / 2)
                              @[simp]
                              theorem Matrix.frobenius_nnnorm_map_eq {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} {Ī² : Type u_6} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] [SeminormedAddCommGroup Ī²] (A : Matrix m n Ī±) (f : Ī± ā†’ Ī²) (hf : āˆ€ (a : Ī±), ā€–f aā€–ā‚Š = ā€–aā€–ā‚Š) :
                              @[simp]
                              theorem Matrix.frobenius_norm_map_eq {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} {Ī² : Type u_6} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] [SeminormedAddCommGroup Ī²] (A : Matrix m n Ī±) (f : Ī± ā†’ Ī²) (hf : āˆ€ (a : Ī±), ā€–f aā€– = ā€–aā€–) :
                              @[simp]
                              theorem Matrix.frobenius_nnnorm_transpose {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
                              @[simp]
                              theorem Matrix.frobenius_norm_transpose {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] (A : Matrix m n Ī±) :
                              @[simp]
                              theorem Matrix.frobenius_nnnorm_conjTranspose {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] [StarAddMonoid Ī±] [NormedStarGroup Ī±] (A : Matrix m n Ī±) :
                              @[simp]
                              theorem Matrix.frobenius_norm_conjTranspose {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup Ī±] [StarAddMonoid Ī±] [NormedStarGroup Ī±] (A : Matrix m n Ī±) :
                              ā€–A.conjTransposeā€– = ā€–Aā€–
                              Equations
                              • ā‹Æ = ā‹Æ
                              @[simp]
                              theorem Matrix.frobenius_norm_row {m : Type u_3} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype m] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : m ā†’ Ī±) :
                              ā€–Matrix.row Ī¹ vā€– = ā€–(WithLp.equiv 2 (m ā†’ Ī±)).symm vā€–
                              @[simp]
                              theorem Matrix.frobenius_nnnorm_row {m : Type u_3} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype m] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : m ā†’ Ī±) :
                              @[simp]
                              theorem Matrix.frobenius_norm_col {n : Type u_4} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype n] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : n ā†’ Ī±) :
                              ā€–Matrix.col Ī¹ vā€– = ā€–(WithLp.equiv 2 (n ā†’ Ī±)).symm vā€–
                              @[simp]
                              theorem Matrix.frobenius_nnnorm_col {n : Type u_4} {Ī± : Type u_5} {Ī¹ : Type u_7} [Fintype n] [Unique Ī¹] [SeminormedAddCommGroup Ī±] (v : n ā†’ Ī±) :
                              @[simp]
                              theorem Matrix.frobenius_nnnorm_diagonal {n : Type u_4} {Ī± : Type u_5} [Fintype n] [SeminormedAddCommGroup Ī±] [DecidableEq n] (v : n ā†’ Ī±) :
                              @[simp]
                              theorem Matrix.frobenius_norm_diagonal {n : Type u_4} {Ī± : Type u_5} [Fintype n] [SeminormedAddCommGroup Ī±] [DecidableEq n] (v : n ā†’ Ī±) :
                              theorem Matrix.frobenius_nnnorm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype l] [Fintype m] [Fintype n] [RCLike Ī±] (A : Matrix l m Ī±) (B : Matrix m n Ī±) :
                              theorem Matrix.frobenius_norm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {Ī± : Type u_5} [Fintype l] [Fintype m] [Fintype n] [RCLike Ī±] (A : Matrix l m Ī±) (B : Matrix m n Ī±) :
                              def Matrix.frobeniusNormedRing {m : Type u_3} {Ī± : Type u_5} [Fintype m] [RCLike Ī±] [DecidableEq m] :
                              NormedRing (Matrix m m Ī±)

                              Normed ring instance (using frobenius norm) for matrices over ā„ or ā„‚. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

                              Equations
                              • Matrix.frobeniusNormedRing = let __src := Matrix.frobeniusSeminormedAddCommGroup; let __src_1 := Matrix.instRing; NormedRing.mk ā‹Æ ā‹Æ
                              Instances For
                                def Matrix.frobeniusNormedAlgebra {R : Type u_1} {m : Type u_3} {Ī± : Type u_5} [Fintype m] [RCLike Ī±] [DecidableEq m] [NormedField R] [NormedAlgebra R Ī±] :
                                NormedAlgebra R (Matrix m m Ī±)

                                Normed algebra instance (using frobenius norm) for matrices over ā„ or ā„‚. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

                                Equations
                                • Matrix.frobeniusNormedAlgebra = let __src := Matrix.frobeniusNormedSpace; let __src_1 := Matrix.instAlgebra; NormedAlgebra.mk ā‹Æ
                                Instances For