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 Mathlib/Analysis/CStarAlgebra/Matrix.lean and open scoped Matrix.Norms.L2Operator. It is separated to avoid extraneous imports in this file.

The elementwise supremum norm #

source
def Matrix.seminormedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup α] :
SeminormedAddCommGroup (Matrix m n α)

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
    Instances For
      source
      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‖
      source
      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

      source
      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‖₊
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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} :
      ‖A i j‖ ≤ ‖A‖
      source
      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} :
      ‖A i j‖₊ ≤ ‖A‖₊
      source
      @[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‖₊) :
      ‖A.map f‖₊ = ‖A‖₊
      source
      @[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‖) :
      ‖A.map f‖ = ‖A‖
      source
      @[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 α) :
      ‖A.transpose‖₊ = ‖A‖₊
      source
      @[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 α) :
      ‖A.transpose‖ = ‖A‖
      source
      @[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 α) :
      ‖A.conjTranspose‖₊ = ‖A‖₊
      source
      @[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‖
      source
      instance Matrix.instNormedStarGroup {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] [StarAddMonoid α] [NormedStarGroup α] :
      NormedStarGroup (Matrix m m α)
      source
      @[simp]
      theorem Matrix.nnnorm_replicateCol {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
      ‖replicateCol ι v‖₊ = ‖v‖₊
      source
      @[deprecated Matrix.nnnorm_replicateCol (since := "2025-03-20")]
      theorem Matrix.nnnorm_col {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
      ‖replicateCol ι v‖₊ = ‖v‖₊

      Alias of Matrix.nnnorm_replicateCol.

      source
      @[simp]
      theorem Matrix.norm_replicateCol {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
      ‖replicateCol ι v‖ = ‖v‖
      source
      @[deprecated Matrix.norm_replicateCol (since := "2025-03-20")]
      theorem Matrix.norm_col {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
      ‖replicateCol ι v‖ = ‖v‖

      Alias of Matrix.norm_replicateCol.

      source
      @[simp]
      theorem Matrix.nnnorm_replicateRow {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
      ‖replicateRow ι v‖₊ = ‖v‖₊
      source
      @[deprecated Matrix.nnnorm_replicateRow (since := "2025-03-20")]
      theorem Matrix.nnnorm_row {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
      ‖replicateRow ι v‖₊ = ‖v‖₊

      Alias of Matrix.nnnorm_replicateRow.

      source
      @[simp]
      theorem Matrix.norm_replicateRow {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
      ‖replicateRow ι v‖ = ‖v‖
      source
      @[deprecated Matrix.norm_replicateRow (since := "2025-03-20")]
      theorem Matrix.norm_row {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
      ‖replicateRow ι v‖ = ‖v‖

      Alias of Matrix.norm_replicateRow.

      source
      @[simp]
      theorem Matrix.nnnorm_diagonal {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] [DecidableEq n] (v : n → α) :
      ‖diagonal v‖₊ = ‖v‖₊
      source
      @[simp]
      theorem Matrix.norm_diagonal {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] [DecidableEq n] (v : n → α) :
      ‖diagonal v‖ = ‖v‖
      source
      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.

      source
      def Matrix.normedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [NormedAddCommGroup α] :
      NormedAddCommGroup (Matrix m n α)

      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
        Instances For
          source
          theorem Matrix.isBoundedSMul {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [IsBoundedSMul R α] :
          IsBoundedSMul R (Matrix m n α)

          This applies to the sup norm of sup norm.

          source
          @[deprecated Matrix.isBoundedSMul (since := "2025-03-10")]
          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 α] [IsBoundedSMul R α] :
          IsBoundedSMul R (Matrix m n α)

          Alias of Matrix.isBoundedSMul.

          This applies to the sup norm of sup norm.

          source
          theorem Matrix.normSMulClass {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [NormSMulClass R α] :
          NormSMulClass R (Matrix m n α)

          This applies to the sup norm of sup norm.

          source
          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
            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.

              source
              def Matrix.linftyOpSeminormedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup α] :
              SeminormedAddCommGroup (Matrix m n α)

              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
                Instances For
                  source
                  def Matrix.linftyOpNormedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [NormedAddCommGroup α] :
                  NormedAddCommGroup (Matrix m n α)

                  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
                    Instances For
                      source
                      theorem Matrix.linftyOpIsBoundedSMul {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [IsBoundedSMul R α] :
                      IsBoundedSMul R (Matrix m n α)

                      This applies to the sup norm of L1 norm.

                      source
                      theorem Matrix.linftyOpNormSMulClass {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [NormSMulClass R α] :
                      NormSMulClass R (Matrix m n α)

                      This applies to the sup norm of L1 norm.

                      source
                      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
                        Instances For
                          source
                          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‖₊)
                          source
                          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‖₊
                          source
                          @[simp]
                          theorem Matrix.linfty_opNNNorm_replicateCol {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
                          ‖replicateCol ι v‖₊ = ‖v‖₊
                          source
                          @[deprecated Matrix.linfty_opNNNorm_replicateCol (since := "2025-03-20")]
                          theorem Matrix.linfty_opNNNorm_col {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
                          ‖replicateCol ι v‖₊ = ‖v‖₊

                          Alias of Matrix.linfty_opNNNorm_replicateCol.

                          source
                          @[simp]
                          theorem Matrix.linfty_opNorm_replicateCol {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
                          ‖replicateCol ι v‖ = ‖v‖
                          source
                          @[deprecated Matrix.linfty_opNorm_replicateCol (since := "2025-03-20")]
                          theorem Matrix.linfty_opNorm_col {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
                          ‖replicateCol ι v‖ = ‖v‖

                          Alias of Matrix.linfty_opNorm_replicateCol.

                          source
                          @[simp]
                          theorem Matrix.linfty_opNNNorm_replicateRow {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
                          ‖replicateRow ι v‖₊ = ∑ i : n, ‖v i‖₊
                          source
                          @[deprecated Matrix.linfty_opNNNorm_replicateRow (since := "2025-03-20")]
                          theorem Matrix.linfty_opNNNorm_row {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
                          ‖replicateRow ι v‖₊ = ∑ i : n, ‖v i‖₊

                          Alias of Matrix.linfty_opNNNorm_replicateRow.

                          source
                          @[simp]
                          theorem Matrix.linfty_opNorm_replicateRow {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
                          ‖replicateRow ι v‖ = ∑ i : n, ‖v i‖
                          source
                          @[deprecated Matrix.linfty_opNNNorm_replicateRow (since := "2025-03-20")]
                          theorem Matrix.linfty_opNorm_row {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
                          ‖replicateRow ι v‖₊ = ∑ i : n, ‖v i‖₊

                          Alias of Matrix.linfty_opNNNorm_replicateRow.

                          source
                          @[simp]
                          theorem Matrix.linfty_opNNNorm_diagonal {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] [DecidableEq m] (v : m → α) :
                          ‖diagonal v‖₊ = ‖v‖₊
                          source
                          @[simp]
                          theorem Matrix.linfty_opNorm_diagonal {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] [DecidableEq m] (v : m → α) :
                          ‖diagonal v‖ = ‖v‖
                          source
                          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 α) :
                          ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
                          source
                          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 α) :
                          ‖A * B‖ ≤ ‖A‖ * ‖B‖
                          source
                          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 → α) :
                          ‖A.mulVec v‖₊ ≤ ‖A‖₊ * ‖v‖₊
                          source
                          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 → α) :
                          ‖A.mulVec v‖ ≤ ‖A‖ * ‖v‖
                          source
                          def Matrix.linftyOpNonUnitalSemiNormedRing {n : Type u_4} {α : Type u_5} [Fintype n] [NonUnitalSeminormedRing α] :
                          NonUnitalSeminormedRing (Matrix n n α)

                          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
                            Instances For
                              source
                              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.

                              source
                              def Matrix.linftyOpSemiNormedRing {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedRing α] [DecidableEq n] :
                              SeminormedRing (Matrix n 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
                                Instances For
                                  source
                                  def Matrix.linftyOpNonUnitalNormedRing {n : Type u_4} {α : Type u_5} [Fintype n] [NonUnitalNormedRing α] :
                                  NonUnitalNormedRing (Matrix n n α)

                                  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
                                    Instances For
                                      source
                                      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
                                        Instances For
                                          source
                                          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
                                            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).

                                              source
                                              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 := ⋯ }‖₊
                                              source
                                              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 := ⋯ }‖
                                              source
                                              @[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‖₊
                                              source
                                              @[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‖

                                              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.

                                              source
                                              def Matrix.frobeniusSeminormedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [SeminormedAddCommGroup α] :
                                              SeminormedAddCommGroup (Matrix m n α)

                                              Seminormed group instance (using the 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
                                                  source
                                                  def Matrix.frobeniusNormedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [NormedAddCommGroup α] :
                                                  NormedAddCommGroup (Matrix m n α)

                                                  Normed group instance (using the 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
                                                    Instances For
                                                      source
                                                      theorem Matrix.frobeniusIsBoundedSMul {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [IsBoundedSMul R α] :
                                                      IsBoundedSMul R (Matrix m n α)

                                                      This applies to the Frobenius norm.

                                                      source
                                                      theorem Matrix.frobeniusNormSMulClass {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [Fintype m] [Fintype n] [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [NormSMulClass R α] :
                                                      NormSMulClass R (Matrix m n α)

                                                      This applies to the Frobenius norm.

                                                      source
                                                      @[deprecated Matrix.frobeniusIsBoundedSMul (since := "2025-03-10")]
                                                      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 α] [IsBoundedSMul R α] :
                                                      IsBoundedSMul R (Matrix m n α)

                                                      Alias of Matrix.frobeniusIsBoundedSMul.

                                                      This applies to the Frobenius norm.

                                                      source
                                                      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 the 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
                                                        Instances For
                                                          source
                                                          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)
                                                          source
                                                          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)
                                                          source
                                                          @[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‖₊) :
                                                          ‖A.map f‖₊ = ‖A‖₊
                                                          source
                                                          @[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‖) :
                                                          ‖A.map f‖ = ‖A‖
                                                          source
                                                          @[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 α) :
                                                          ‖A.transpose‖₊ = ‖A‖₊
                                                          source
                                                          @[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 α) :
                                                          ‖A.transpose‖ = ‖A‖
                                                          source
                                                          @[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 α) :
                                                          ‖A.conjTranspose‖₊ = ‖A‖₊
                                                          source
                                                          @[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‖
                                                          source
                                                          instance Matrix.frobenius_normedStarGroup {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] [StarAddMonoid α] [NormedStarGroup α] :
                                                          NormedStarGroup (Matrix m m α)
                                                          source
                                                          @[simp]
                                                          theorem Matrix.frobenius_norm_replicateRow {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
                                                          ‖replicateRow ι v‖ = ‖WithLp.toLp 2 v‖
                                                          source
                                                          @[deprecated Matrix.frobenius_norm_replicateRow (since := "2025-03-20")]
                                                          theorem Matrix.frobenius_norm_row {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
                                                          ‖replicateRow ι v‖ = ‖WithLp.toLp 2 v‖

                                                          Alias of Matrix.frobenius_norm_replicateRow.

                                                          source
                                                          @[simp]
                                                          theorem Matrix.frobenius_nnnorm_replicateRow {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
                                                          ‖replicateRow ι v‖₊ = ‖WithLp.toLp 2 v‖₊
                                                          source
                                                          @[deprecated Matrix.frobenius_nnnorm_replicateRow (since := "2025-03-20")]
                                                          theorem Matrix.frobenius_nnnorm_row {m : Type u_3} {α : Type u_5} {ι : Type u_7} [Fintype m] [Unique ι] [SeminormedAddCommGroup α] (v : m → α) :
                                                          ‖replicateRow ι v‖₊ = ‖WithLp.toLp 2 v‖₊

                                                          Alias of Matrix.frobenius_nnnorm_replicateRow.

                                                          source
                                                          @[simp]
                                                          theorem Matrix.frobenius_norm_replicateCol {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
                                                          ‖replicateCol ι v‖ = ‖WithLp.toLp 2 v‖
                                                          source
                                                          @[deprecated Matrix.frobenius_norm_replicateCol (since := "2025-03-20")]
                                                          theorem Matrix.frobenius_norm_col {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
                                                          ‖replicateCol ι v‖ = ‖WithLp.toLp 2 v‖

                                                          Alias of Matrix.frobenius_norm_replicateCol.

                                                          source
                                                          @[simp]
                                                          theorem Matrix.frobenius_nnnorm_replicateCol {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
                                                          ‖replicateCol ι v‖₊ = ‖WithLp.toLp 2 v‖₊
                                                          source
                                                          @[deprecated Matrix.frobenius_nnnorm_replicateCol (since := "2025-03-20")]
                                                          theorem Matrix.frobenius_nnnorm_col {n : Type u_4} {α : Type u_5} {ι : Type u_7} [Fintype n] [Unique ι] [SeminormedAddCommGroup α] (v : n → α) :
                                                          ‖replicateCol ι v‖₊ = ‖WithLp.toLp 2 v‖₊

                                                          Alias of Matrix.frobenius_nnnorm_replicateCol.

                                                          source
                                                          @[simp]
                                                          theorem Matrix.frobenius_nnnorm_diagonal {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] [DecidableEq n] (v : n → α) :
                                                          ‖diagonal v‖₊ = ‖WithLp.toLp 2 v‖₊
                                                          source
                                                          @[simp]
                                                          theorem Matrix.frobenius_norm_diagonal {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] [DecidableEq n] (v : n → α) :
                                                          ‖diagonal v‖ = ‖WithLp.toLp 2 v‖
                                                          source
                                                          theorem Matrix.frobenius_nnnorm_one {n : Type u_4} {α : Type u_5} [Fintype n] [DecidableEq n] [SeminormedAddCommGroup α] [One α] :
                                                          ‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
                                                          source
                                                          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 α) :
                                                          ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊
                                                          source
                                                          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 α) :
                                                          ‖A * B‖ ≤ ‖A‖ * ‖B‖
                                                          source
                                                          def Matrix.frobeniusNormedRing {m : Type u_3} {α : Type u_5} [Fintype m] [RCLike α] [DecidableEq m] :
                                                          NormedRing (Matrix m m α)

                                                          Normed ring instance (using the 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
                                                            Instances For
                                                              source
                                                              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 the 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
                                                                Instances For