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 α] :

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

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.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} :

‖A i j‖ ≤ ‖A‖

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‖₊

@[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‖₊) :

‖Matrix.map A f‖₊ = ‖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‖) :

‖Matrix.map A f‖ = ‖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 α) :

‖Matrix.transpose A‖₊ = ‖A‖₊

@[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 α) :

‖Matrix.transpose A‖ = ‖A‖

@[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 α) :

‖Matrix.conjTranspose A‖₊ = ‖A‖₊

@[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 α) :

‖Matrix.conjTranspose A‖ = ‖A‖

instance Matrix.instNormedStarGroupMatrixSeminormedAddCommGroupInstStarAddMonoidMatrixAddMonoidToAddMonoidToSubNegMonoidToAddGroupToSeminormedAddGroup {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] [StarAddMonoid α] [NormedStarGroup α] :

NormedStarGroup (Matrix m m α)

Equations

(_ : NormedStarGroup (Matrix m m α)) = (_ : NormedStarGroup (Matrix m m α))

@[simp]

theorem Matrix.nnnorm_col {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] (v : m → α) :

‖Matrix.col v‖₊ = ‖v‖₊

@[simp]

theorem Matrix.norm_col {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] (v : m → α) :

‖Matrix.col v‖ = ‖v‖

@[simp]

theorem Matrix.nnnorm_row {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] (v : n → α) :

‖Matrix.row v‖₊ = ‖v‖₊

@[simp]

theorem Matrix.norm_row {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] (v : n → α) :

‖Matrix.row v‖ = ‖v‖

@[simp]

theorem Matrix.nnnorm_diagonal {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] [DecidableEq n] (v : n → α) :

‖Matrix.diagonal v‖₊ = ‖v‖₊

@[simp]

theorem Matrix.norm_diagonal {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] [DecidableEq n] (v : n → α) :

‖Matrix.diagonal v‖ = ‖v‖

instance Matrix.instNormOneClassMatrixToNormSeminormedAddCommGroupOneToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup {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

(_ : NormOneClass (Matrix n n α)) = (_ : NormOneClass (Matrix n n α))

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

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.

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

Matrix.linftyOpSeminormedAddCommGroup = inferInstance

Instances For

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

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.sup Finset.univ fun (i : m) => Finset.sum Finset.univ fun (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.sup Finset.univ fun (i : m) => Finset.sum Finset.univ fun (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.sup Finset.univ fun (i : m) => Finset.sum Finset.univ fun (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.sup Finset.univ fun (i : m) => Finset.sum Finset.univ fun (j : n) => ‖A i j‖₊

Alias of Matrix.linfty_opNNNorm_def.

@[simp]

theorem Matrix.linfty_opNNNorm_col {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] (v : m → α) :

‖Matrix.col v‖₊ = ‖v‖₊

@[deprecated Matrix.linfty_opNNNorm_col]

theorem Matrix.linfty_op_nnnorm_col {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] (v : m → α) :

‖Matrix.col v‖₊ = ‖v‖₊

Alias of Matrix.linfty_opNNNorm_col.

@[simp]

theorem Matrix.linfty_opNorm_col {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] (v : m → α) :

‖Matrix.col v‖ = ‖v‖

@[deprecated Matrix.linfty_opNorm_col]

theorem Matrix.linfty_op_norm_col {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] (v : m → α) :

‖Matrix.col v‖ = ‖v‖

Alias of Matrix.linfty_opNorm_col.

@[simp]

theorem Matrix.linfty_opNNNorm_row {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] (v : n → α) :

‖Matrix.row v‖₊ = Finset.sum Finset.univ fun (i : n) => ‖v i‖₊

@[deprecated Matrix.linfty_opNNNorm_row]

theorem Matrix.linfty_op_nnnorm_row {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] (v : n → α) :

‖Matrix.row v‖₊ = Finset.sum Finset.univ fun (i : n) => ‖v i‖₊

Alias of Matrix.linfty_opNNNorm_row.

@[simp]

theorem Matrix.linfty_opNorm_row {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] (v : n → α) :

‖Matrix.row v‖ = Finset.sum Finset.univ fun (i : n) => ‖v i‖

@[deprecated Matrix.linfty_opNorm_row]

theorem Matrix.linfty_op_norm_row {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] (v : n → α) :

‖Matrix.row v‖ = Finset.sum Finset.univ fun (i : n) => ‖v i‖

Alias of Matrix.linfty_opNorm_row.

@[simp]

theorem Matrix.linfty_opNNNorm_diagonal {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] [DecidableEq m] (v : m → α) :

‖Matrix.diagonal v‖₊ = ‖v‖₊

@[deprecated Matrix.linfty_opNNNorm_diagonal]

theorem Matrix.linfty_op_nnnorm_diagonal {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] [DecidableEq m] (v : m → α) :

‖Matrix.diagonal v‖₊ = ‖v‖₊

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 → α) :

‖Matrix.diagonal v‖ = ‖v‖

@[deprecated Matrix.linfty_opNorm_diagonal]

theorem Matrix.linfty_op_norm_diagonal {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] [DecidableEq m] (v : m → α) :

‖Matrix.diagonal v‖ = ‖v‖

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 α) :

‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

@[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 α) :

‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

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 α) :

‖A * B‖ ≤ ‖A‖ * ‖B‖

@[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 α) :

‖A * B‖ ≤ ‖A‖ * ‖B‖

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 → α) :

‖Matrix.mulVec A v‖₊ ≤ ‖A‖₊ * ‖v‖₊

@[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 → α) :

‖Matrix.mulVec A v‖₊ ≤ ‖A‖₊ * ‖v‖₊

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 → α) :

‖Matrix.mulVec A v‖ ≤ ‖A‖ * ‖v‖

@[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 → α) :

‖Matrix.mulVec A v‖ ≤ ‖A‖ * ‖v‖

Alias of Matrix.linfty_opNorm_mulVec.

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

One or more equations did not get rendered due to their size.

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

(_ : NormOneClass (Matrix n n α)) = (_ : NormOneClass (Matrix n n α))

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

One or more equations did not get rendered due to their size.

Instances For

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

One or more equations did not get rendered due to their size.

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 (_ : ∀ (x y : Matrix n n α), dist x y = ‖x - y‖) (_ : ∀ (a b : Matrix n n α), ‖a * b‖ ≤ ‖a‖ * ‖b‖)

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 (_ : ∀ (a : R) (b : Matrix n n α), ‖a • b‖ ≤ ‖a‖ * ‖b‖)

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‖₊ = ‖ContinuousLinearMap.mk (Matrix.mulVecLin A)‖₊

@[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‖₊ = ‖ContinuousLinearMap.mk (Matrix.mulVecLin A)‖₊

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‖ = ‖ContinuousLinearMap.mk (Matrix.mulVecLin A)‖

@[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‖ = ‖ContinuousLinearMap.mk (Matrix.mulVecLin A)‖

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.

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

Matrix.frobeniusSeminormedAddCommGroup = inferInstanceAs (SeminormedAddCommGroup (PiLp 2 fun (_i : m) => PiLp 2 fun (_j : n) => α))

Instances For

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 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‖₊ = (Finset.sum Finset.univ fun (i : m) => Finset.sum Finset.univ fun (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‖ = (Finset.sum Finset.univ fun (i : m) => Finset.sum Finset.univ fun (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‖₊) :

‖Matrix.map A f‖₊ = ‖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‖) :

‖Matrix.map A f‖ = ‖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 α) :

‖Matrix.transpose A‖₊ = ‖A‖₊

@[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 α) :

‖Matrix.transpose A‖ = ‖A‖

@[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 α) :

‖Matrix.conjTranspose A‖₊ = ‖A‖₊

@[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 α) :

‖Matrix.conjTranspose A‖ = ‖A‖

instance Matrix.frobenius_normedStarGroup {m : Type u_3} {α : Type u_5} [Fintype m] [SeminormedAddCommGroup α] [StarAddMonoid α] [NormedStarGroup α] :

NormedStarGroup (Matrix m m α)

Equations

(_ : NormedStarGroup (Matrix m m α)) = (_ : NormedStarGroup (Matrix m m α))

@[simp]

theorem Matrix.frobenius_norm_row {m : Type u_3} {α : Type u_5} [Fintype m] [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} [Fintype m] [SeminormedAddCommGroup α] (v : m → α) :

‖Matrix.row v‖₊ = ‖(WithLp.equiv 2 (m → α)).symm v‖₊

@[simp]

theorem Matrix.frobenius_norm_col {n : Type u_4} {α : Type u_5} [Fintype n] [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} [Fintype n] [SeminormedAddCommGroup α] (v : n → α) :

‖Matrix.col v‖₊ = ‖(WithLp.equiv 2 (n → α)).symm v‖₊

@[simp]

theorem Matrix.frobenius_nnnorm_diagonal {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] [DecidableEq n] (v : n → α) :

‖Matrix.diagonal v‖₊ = ‖(WithLp.equiv 2 (n → α)).symm v‖₊

@[simp]

theorem Matrix.frobenius_norm_diagonal {n : Type u_4} {α : Type u_5} [Fintype n] [SeminormedAddCommGroup α] [DecidableEq n] (v : n → α) :

‖Matrix.diagonal v‖ = ‖(WithLp.equiv 2 (n → α)).symm v‖

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‖₊

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] [IsROrC α] (A : Matrix l m α) (B : Matrix m n α) :

‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

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] [IsROrC α] (A : Matrix l m α) (B : Matrix m n α) :

‖A * B‖ ≤ ‖A‖ * ‖B‖

def Matrix.frobeniusNormedRing {m : Type u_3} {α : Type u_5} [Fintype m] [IsROrC α] [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

One or more equations did not get rendered due to their size.

Instances For

def Matrix.frobeniusNormedAlgebra {R : Type u_1} {m : Type u_3} {α : Type u_5} [Fintype m] [IsROrC α] [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 (_ : ∀ (a : R) (b : Matrix m m α), ‖a • b‖ ≤ ‖a‖ * ‖b‖)

Instances For