mathlib3 documentation

analysis.matrix

Matrices as a normed space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 elementwise supremum norm #

source
@[protected]
def matrix.seminormed_add_comm_group {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] :
seminormed_add_comm_group (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
source
theorem matrix.norm_le_iff {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] {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] [seminormed_add_comm_group α] {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] [seminormed_add_comm_group α] {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] [seminormed_add_comm_group α] {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] [seminormed_add_comm_group α] (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] [seminormed_add_comm_group α] (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] [seminormed_add_comm_group α] [seminormed_add_comm_group β] (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] [seminormed_add_comm_group α] [seminormed_add_comm_group β] (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] [seminormed_add_comm_group α] (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] [seminormed_add_comm_group α] (A : matrix m n α) :
‖A.transpose‖ = ‖A‖
source
@[simp]
theorem matrix.nnnorm_conj_transpose {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] [star_add_monoid α] [normed_star_group α] (A : matrix m n α) :
‖A.conj_transpose‖₊ = ‖A‖₊
source
@[simp]
theorem matrix.norm_conj_transpose {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] [star_add_monoid α] [normed_star_group α] (A : matrix m n α) :
‖A.conj_transpose‖ = ‖A‖
source
@[protected, instance]
def matrix.normed_star_group {m : Type u_3} {α : Type u_5} [fintype m] [seminormed_add_comm_group α] [star_add_monoid α] [normed_star_group α] :
normed_star_group (matrix m m α)
source
@[simp]
theorem matrix.nnnorm_col {m : Type u_3} {α : Type u_5} [fintype m] [seminormed_add_comm_group α] (v : m → α) :
‖matrix.col v‖₊ = ‖v‖₊
source
@[simp]
theorem matrix.norm_col {m : Type u_3} {α : Type u_5} [fintype m] [seminormed_add_comm_group α] (v : m → α) :
‖matrix.col v‖ = ‖v‖
source
@[simp]
theorem matrix.nnnorm_row {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] (v : n → α) :
‖matrix.row v‖₊ = ‖v‖₊
source
@[simp]
theorem matrix.norm_row {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] (v : n → α) :
‖matrix.row v‖ = ‖v‖
source
@[simp]
theorem matrix.nnnorm_diagonal {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] [decidable_eq n] (v : n → α) :
‖matrix.diagonal v‖₊ = ‖v‖₊
source
@[simp]
theorem matrix.norm_diagonal {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] [decidable_eq n] (v : n → α) :
‖matrix.diagonal v‖ = ‖v‖
source
@[protected, nolint, instance]
def matrix.norm_one_class {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] [nonempty n] [decidable_eq n] [has_one α] [norm_one_class α] :
norm_one_class (matrix n n α)

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

source
@[protected]
def matrix.normed_add_comm_group {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [normed_add_comm_group α] :
normed_add_comm_group (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
source
@[protected]
def matrix.normed_space {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [normed_field R] [seminormed_add_comm_group α] [normed_space R α] :
normed_space 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

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
@[protected]
noncomputable def matrix.linfty_op_seminormed_add_comm_group {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] :
seminormed_add_comm_group (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
source
@[protected]
noncomputable def matrix.linfty_op_normed_add_comm_group {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [normed_add_comm_group α] :
normed_add_comm_group (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
source
@[protected]
noncomputable def matrix.linfty_op_normed_space {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [normed_field R] [seminormed_add_comm_group α] [normed_space R α] :
normed_space 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
source
theorem matrix.linfty_op_norm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] (A : matrix m n α) :
‖A‖ = ↑(finset.univ.sup (λ (i : m), finset.univ.sum (λ (j : n), ‖A i j‖₊)))
source
theorem matrix.linfty_op_nnnorm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] (A : matrix m n α) :
‖A‖₊ = finset.univ.sup (λ (i : m), finset.univ.sum (λ (j : n), ‖A i j‖₊))
source
@[simp]
theorem matrix.linfty_op_nnnorm_col {m : Type u_3} {α : Type u_5} [fintype m] [seminormed_add_comm_group α] (v : m → α) :
‖matrix.col v‖₊ = ‖v‖₊
source
@[simp]
theorem matrix.linfty_op_norm_col {m : Type u_3} {α : Type u_5} [fintype m] [seminormed_add_comm_group α] (v : m → α) :
‖matrix.col v‖ = ‖v‖
source
@[simp]
theorem matrix.linfty_op_nnnorm_row {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] (v : n → α) :
‖matrix.row v‖₊ = finset.univ.sum (λ (i : n), ‖v i‖₊)
source
@[simp]
theorem matrix.linfty_op_norm_row {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] (v : n → α) :
‖matrix.row v‖ = finset.univ.sum (λ (i : n), ‖v i‖)
source
@[simp]
theorem matrix.linfty_op_nnnorm_diagonal {m : Type u_3} {α : Type u_5} [fintype m] [seminormed_add_comm_group α] [decidable_eq m] (v : m → α) :
‖matrix.diagonal v‖₊ = ‖v‖₊
source
@[simp]
theorem matrix.linfty_op_norm_diagonal {m : Type u_3} {α : Type u_5} [fintype m] [seminormed_add_comm_group α] [decidable_eq m] (v : m → α) :
‖matrix.diagonal v‖ = ‖v‖
source
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] [non_unital_semi_normed_ring α] (A : matrix l m α) (B : matrix m n α) :
‖A.mul B‖₊ ≤ ‖A‖₊ * ‖B‖₊
source
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] [non_unital_semi_normed_ring α] (A : matrix l m α) (B : matrix m n α) :
‖A.mul B‖ ≤ ‖A‖ * ‖B‖
source
theorem matrix.linfty_op_nnnorm_mul_vec {l : Type u_2} {m : Type u_3} {α : Type u_5} [fintype l] [fintype m] [non_unital_semi_normed_ring α] (A : matrix l m α) (v : m → α) :
‖A.mul_vec v‖₊ ≤ ‖A‖₊ * ‖v‖₊
source
theorem matrix.linfty_op_norm_mul_vec {l : Type u_2} {m : Type u_3} {α : Type u_5} [fintype l] [fintype m] [non_unital_semi_normed_ring α] (A : matrix l m α) (v : m → α) :
‖A.mul_vec v‖ ≤ ‖A‖ * ‖v‖
source
@[protected]
noncomputable def matrix.linfty_op_non_unital_semi_normed_ring {n : Type u_4} {α : Type u_5} [fintype n] [non_unital_semi_normed_ring α] :
non_unital_semi_normed_ring (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
source
@[protected, instance]
def matrix.linfty_op_norm_one_class {n : Type u_4} {α : Type u_5} [fintype n] [semi_normed_ring α] [norm_one_class α] [decidable_eq n] [nonempty n] :
norm_one_class (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
@[protected]
noncomputable def matrix.linfty_op_semi_normed_ring {n : Type u_4} {α : Type u_5} [fintype n] [semi_normed_ring α] [decidable_eq n] :
semi_normed_ring (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
source
@[protected]
noncomputable def matrix.linfty_op_non_unital_normed_ring {n : Type u_4} {α : Type u_5} [fintype n] [non_unital_normed_ring α] :
non_unital_normed_ring (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
source
@[protected]
noncomputable def matrix.linfty_op_normed_ring {n : Type u_4} {α : Type u_5} [fintype n] [normed_ring α] [decidable_eq n] :
normed_ring (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
source
@[protected]
def matrix.linfty_op_normed_algebra {R : Type u_1} {n : Type u_4} {α : Type u_5} [fintype n] [normed_field R] [semi_normed_ring α] [normed_algebra R α] [decidable_eq n] :
normed_algebra 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

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
noncomputable def matrix.frobenius_seminormed_add_comm_group {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] :
seminormed_add_comm_group (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
source
noncomputable def matrix.frobenius_normed_add_comm_group {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [normed_add_comm_group α] :
normed_add_comm_group (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
source
noncomputable def matrix.frobenius_normed_space {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [normed_field R] [seminormed_add_comm_group α] [normed_space R α] :
normed_space 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
source
theorem matrix.frobenius_nnnorm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] (A : matrix m n α) :
‖A‖₊ = finset.univ.sum (λ (i : m), finset.univ.sum (λ (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] [seminormed_add_comm_group α] (A : matrix m n α) :
‖A‖ = finset.univ.sum (λ (i : m), finset.univ.sum (λ (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] [seminormed_add_comm_group α] [seminormed_add_comm_group β] (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] [seminormed_add_comm_group α] [seminormed_add_comm_group β] (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] [seminormed_add_comm_group α] (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] [seminormed_add_comm_group α] (A : matrix m n α) :
‖A.transpose‖ = ‖A‖
source
@[simp]
theorem matrix.frobenius_nnnorm_conj_transpose {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] [star_add_monoid α] [normed_star_group α] (A : matrix m n α) :
‖A.conj_transpose‖₊ = ‖A‖₊
source
@[simp]
theorem matrix.frobenius_norm_conj_transpose {m : Type u_3} {n : Type u_4} {α : Type u_5} [fintype m] [fintype n] [seminormed_add_comm_group α] [star_add_monoid α] [normed_star_group α] (A : matrix m n α) :
‖A.conj_transpose‖ = ‖A‖
source
@[protected, instance]
def matrix.frobenius_normed_star_group {m : Type u_3} {α : Type u_5} [fintype m] [seminormed_add_comm_group α] [star_add_monoid α] [normed_star_group α] :
normed_star_group (matrix m m α)
source
@[simp]
theorem matrix.frobenius_norm_row {m : Type u_3} {α : Type u_5} [fintype m] [seminormed_add_comm_group α] (v : m → α) :
‖matrix.row v‖ = ‖⇑((pi_Lp.equiv 2 (λ (ᾰ : m), α)).symm) v‖
source
@[simp]
theorem matrix.frobenius_nnnorm_row {m : Type u_3} {α : Type u_5} [fintype m] [seminormed_add_comm_group α] (v : m → α) :
‖matrix.row v‖₊ = ‖⇑((pi_Lp.equiv 2 (λ (ᾰ : m), α)).symm) v‖₊
source
@[simp]
theorem matrix.frobenius_norm_col {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] (v : n → α) :
‖matrix.col v‖ = ‖⇑((pi_Lp.equiv 2 (λ (ᾰ : n), α)).symm) v‖
source
@[simp]
theorem matrix.frobenius_nnnorm_col {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] (v : n → α) :
‖matrix.col v‖₊ = ‖⇑((pi_Lp.equiv 2 (λ (ᾰ : n), α)).symm) v‖₊
source
@[simp]
theorem matrix.frobenius_nnnorm_diagonal {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] [decidable_eq n] (v : n → α) :
‖matrix.diagonal v‖₊ = ‖⇑((pi_Lp.equiv 2 (λ (ᾰ : n), α)).symm) v‖₊
source
@[simp]
theorem matrix.frobenius_norm_diagonal {n : Type u_4} {α : Type u_5} [fintype n] [seminormed_add_comm_group α] [decidable_eq n] (v : n → α) :
‖matrix.diagonal v‖ = ‖⇑((pi_Lp.equiv 2 (λ (ᾰ : n), α)).symm) v‖
source
theorem matrix.frobenius_nnnorm_one {n : Type u_4} {α : Type u_5} [fintype n] [decidable_eq n] [seminormed_add_comm_group α] [has_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] [is_R_or_C α] (A : matrix l m α) (B : matrix m n α) :
‖A.mul 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] [is_R_or_C α] (A : matrix l m α) (B : matrix m n α) :
‖A.mul B‖ ≤ ‖A‖ * ‖B‖
source
noncomputable def matrix.frobenius_normed_ring {m : Type u_3} {α : Type u_5} [fintype m] [is_R_or_C α] [decidable_eq m] :
normed_ring (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
source
def matrix.frobenius_normed_algebra {R : Type u_1} {m : Type u_3} {α : Type u_5} [fintype m] [is_R_or_C α] [decidable_eq m] [normed_field R] [normed_algebra R α] :
normed_algebra 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