mathlib documentation

linear_algebra.matrix.pos_def

Positive Definite Matrices #

This file defines positive (semi)definite matrices and connects the notion to positive definiteness of quadratic forms.

Main definition #

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
theorem matrix.pos_def.is_hermitian {π•œ : Type u_1} [is_R_or_C π•œ] {n : Type u_3} [fintype n] {M : matrix n n π•œ} (hM : M.pos_def) :
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
theorem matrix.pos_def.pos_semidef {π•œ : Type u_1} [is_R_or_C π•œ] {n : Type u_3} [fintype n] {M : matrix n n π•œ} (hM : M.pos_def) :
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) :
@[simp]
theorem matrix.pos_semidef_submatrix_equiv {π•œ : Type u_1} [is_R_or_C π•œ] {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {M : matrix n n π•œ} (e : m ≃ n) :
theorem matrix.pos_def.transpose {π•œ : Type u_1} [is_R_or_C π•œ] {n : Type u_3} [fintype 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] :
0 < M.det
noncomputable 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