Positive Definite Matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 {to_has_inner := {inner := λ (x y : n → 𝕜), matrix.dot_product (has_star.star x) (M.mul_vec y)}, conj_symm := _, nonneg_re := _, definite := _, add_left := _, smul_left := _}