mathlib3 documentation

monlib / linear_algebra.my_matrix.star_ordered_ring

Matrix algebras are star ordered rings #

This file contains the instance of star_ordered_ring for matrix n n ℂ.

Main definitions #

matrix.partial_order: The partial order on matrix n n ℂ induced by the positive semidefinite matrices.
matrix.pos_semidef.add_submonoid: The additive submonoid of positive semidefinite matrices.
matrix.star_ordered_ring: The instance of star_ordered_ring for matrix n n ℂ.

You need to open_locale matrix_order to use these instances.

theorem matrix.pos_semidef.zero {n : Type u_1} [fintype n] :

theorem matrix.pos_semidef.add {n : Type u_1} [fintype n] {x y : matrix n n ℂ} (hx : x.pos_semidef) (hy : y.pos_semidef) :

(x + y).pos_semidef

theorem matrix.eq_zero_iff {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} :

x = 0 ↔ ∀ (a : n → ℂ), matrix.dot_product (has_star.star a) (x.mul_vec a) = 0

theorem matrix.to_euclidean_lin_apply {n : Type u_1} [fintype n] [decidable_eq n] (x : matrix n n ℂ) (a : n → ℂ) :

⇑(⇑matrix.to_euclidean_lin x) a = x.mul_vec a

def matrix.partial_order {n : Type u_1} [fintype n] [decidable_eq n] :

partial_order (matrix n n ℂ)

Equations

matrix.partial_order = {le := λ (x y : matrix n n ℂ), (y - x).pos_semidef, lt := preorder.lt._default (λ (x y : matrix n n ℂ), (y - x).pos_semidef), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

theorem matrix.le_iff {n : Type u_1} [fintype n] [decidable_eq n] {x y : matrix n n ℂ} :

x ≤ y ↔ (y - x).pos_semidef

noncomputable def matrix.star_ordered_ring {n : Type u_1} [fintype n] [decidable_eq n] :

star_ordered_ring (matrix n n ℂ)

Equations

matrix.star_ordered_ring = star_ordered_ring.of_le_iff matrix.star_ordered_ring._proof_1 matrix.star_ordered_ring._proof_2

theorem matrix.pi.le_iff_sub_nonneg {ι : Type u_1} [fintype ι] [decidable_eq ι] {n : ι → Type u_2} [Π (i : ι), fintype (n i)] [Π (i : ι), decidable_eq (n i)] (x y : Π (i : ι), matrix (n i) (n i) ℂ) :

x ≤ y ↔ ∃ (z : Π (i : ι), matrix (n i) (n i) ℂ), y = x + has_star.star z * z

noncomputable def matrix.pi.star_ordered_ring {ι : Type u_1} [fintype ι] [decidable_eq ι] {n : ι → Type u_2} [Π (i : ι), fintype (n i)] [Π (i : ι), decidable_eq (n i)] :

star_ordered_ring (Π (i : ι), matrix (n i) (n i) ℂ)

Equations

matrix.pi.star_ordered_ring = star_ordered_ring.of_le_iff matrix.pi.star_ordered_ring._proof_1 matrix.pi.star_ordered_ring._proof_2

def matrix.neg_semidef {n : Type u_1} [fintype n] [decidable_eq n] (x : matrix n n ℂ) :

Prop

Equations

x.neg_semidef = (x.is_hermitian ∧ ∀ (a : n → ℂ), ⇑is_R_or_C.re (matrix.dot_product (has_star.star a) (x.mul_vec a)) ≤ 0)

theorem matrix.is_hermitian.neg_iff {n : Type u_1} [fintype n] [decidable_eq n] (x : matrix n n ℂ) :

(-x).is_hermitian ↔ x.is_hermitian

theorem matrix.neg_semidef_iff_neg_pos_semidef {n : Type u_1} [fintype n] [decidable_eq n] (x : matrix n n ℂ) :

x.neg_semidef ↔ (-x).pos_semidef

theorem matrix.neg_semidef_iff_nonpos {n : Type u_1} [fintype n] [decidable_eq n] (x : matrix n n ℂ) :

x.neg_semidef ↔ x ≤ 0

theorem matrix.pos_semidef_and_neg_semidef_iff_eq_zero {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} :

x.pos_semidef ∧ x.neg_semidef ↔ x = 0