mathlib documentation

linear_algebra.matrix.pos_def

Positive Definite Matrices #

This file defines positive definite matrices and connects this notion to positive definiteness of quadratic forms.

Main definition #

def matrix.pos_def {π•œ : Type u_1} [is_R_or_C π•œ] {n : Type u_2} [fintype n] (M : matrix n n π•œ) :
Prop

A matrix M : matrix n n R 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_2} [fintype n] {M : matrix n n π•œ} (hM : M.pos_def) :
theorem matrix.pos_def_of_to_quadratic_form' {n : Type u_2} [fintype n] [decidable_eq n] {M : matrix n n ℝ} (hM : M.is_symm) (hMq : M.to_quadratic_form'.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) :
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