Positive Definite Matrices #
This file defines positive (semi)definite matrices and connects the notion to positive definiteness of quadratic forms.
Main definition #
matrix.pos_def: a matrixM : matrix n n πis positive definite if it is hermitian andxα΄΄Mxis greater than zero for all nonzerox.matrix.pos_semidef: a matrixM : matrix n n πis positive semidefinite if it is hermitian andxα΄΄Mxis nonnegative for allx.
def
matrix.pos_def
{π : Type u_1}
[is_R_or_C π]
{n : Type u_3}
[fintype n]
(M : matrix n n π) :
Prop
A matrix M : matrix n n π is positive definite if it is hermitian
and xα΄΄Mx is greater than zero for all nonzero x.
Equations
- M.pos_def = (M.is_hermitian β§ β (x : n β π), x β 0 β 0 < βis_R_or_C.re (matrix.dot_product (has_star.star x) (M.mul_vec x)))
def
matrix.pos_semidef
{π : Type u_1}
[is_R_or_C π]
{n : Type u_3}
[fintype n]
(M : matrix n n π) :
Prop
A matrix M : matrix n n π is positive semidefinite if it is hermitian
and xα΄΄Mx is nonnegative for all x.
Equations
- M.pos_semidef = (M.is_hermitian β§ β (x : n β π), 0 β€ βis_R_or_C.re (matrix.dot_product (has_star.star x) (M.mul_vec x)))
theorem
matrix.pos_semidef.submatrix
{π : Type u_1}
[is_R_or_C π]
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{M : matrix n n π}
(hM : M.pos_semidef)
(e : m β n) :
(M.submatrix βe βe).pos_semidef
theorem
matrix.pos_def_of_to_quadratic_form'
{n : Type u_3}
[fintype n]
[decidable_eq n]
{M : matrix n n β}
(hM : M.is_symm)
(hMq : M.to_quadratic_form'.pos_def) :
M.pos_def
theorem
matrix.pos_def_to_quadratic_form'
{n : Type u_3}
[fintype n]
[decidable_eq n]
{M : matrix n n β}
(hM : M.pos_def) :
theorem
matrix.pos_def.det_pos
{n : Type u_3}
[fintype n]
{M : matrix n n β}
(hM : M.pos_def)
[decidable_eq n] :
theorem
quadratic_form.pos_def_of_to_matrix'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{Q : quadratic_form β (n β β)}
(hQ : Q.to_matrix'.pos_def) :
Q.pos_def
theorem
quadratic_form.pos_def_to_matrix'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{Q : quadratic_form β (n β β)}
(hQ : Q.pos_def) :
@[reducible]
noncomputable
def
matrix.normed_add_comm_group.of_matrix
{π : Type u_1}
[is_R_or_C π]
{n : Type u_2}
[fintype n]
{M : matrix n n π}
(hM : M.pos_def) :
normed_add_comm_group (n β π)
A positive definite matrix M induces a norm βxβ = sqrt (re xα΄΄Mx).
def
matrix.inner_product_space.of_matrix
{π : Type u_1}
[is_R_or_C π]
{n : Type u_2}
[fintype n]
{M : matrix n n π}
(hM : M.pos_def) :
inner_product_space π (n β π)
A positive definite matrix M induces an inner product βͺx, yβ« = xα΄΄My.
Equations
- matrix.inner_product_space.of_matrix hM = inner_product_space.of_core {inner := Ξ» (x y : n β π), matrix.dot_product (has_star.star x) (M.mul_vec y), conj_symm := _, nonneg_re := _, definite := _, add_left := _, smul_left := _}