mathlib3 documentation

linear_algebra.matrix.pos_def

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 #

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
@[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) :

A positive definite matrix M induces a norm ‖x‖ = sqrt (re xᴴMx).

Equations
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