# Positive Definite Matrices #

This file defines positive (semi)definite matrices and connects the notion to positive definiteness of quadratic forms. In `Mathlib/Analysis/Matrix/Order.lean`, positive semi-definiteness is used to define the partial order on matrices on `ℝ` or `ℂ`.

## Main definitions #

- `Matrix.PosSemidef` : a matrix `M : Matrix n n R` is positive semidefinite if it is Hermitian and `xᴴMx` is nonnegative for all `x`.
- `Matrix.PosDef` : 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`.
- `Matrix.InnerProductSpace.ofMatrix`: the inner product on `n → 𝕜` induced by a positive definite matrix `M`, and is given by `⟪x, y⟫ = xᴴMy`.

## Main results #

- `Matrix.PosSemidef.fromBlocks₁₁` and `Matrix.PosSemidef.fromBlocks₂₂`: If a matrix `A` is positive definite, then `[A B; Bᴴ D]` is positive semidefinite if and only if `D - Bᴴ A⁻¹ B` is positive semidefinite.
- `Matrix.PosDef.isUnit`: A positive definite matrix in a field is invertible.

## Positive semidefinite matrices #

source
def Matrix.PosSemidef {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] (M : Matrix n n R) :
Prop

A matrix `M : Matrix n n R` is positive semidefinite if it is Hermitian and `xᴴ * M * x` is nonnegative for all `x`.

Equations

- M.PosSemidef = (M.IsHermitian ∧ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M.mulVec x)

Instances For

source
theorem Matrix.PosSemidef.diagonal {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] {d : n → R} (h : 0 ≤ d) :
(diagonal d).PosSemidef
source
theorem Matrix.posSemidef_diagonal_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] {d : n → R} :
(diagonal d).PosSemidef ↔ ∀ (i : n), 0 ≤ d i

A diagonal matrix is positive semidefinite iff its diagonal entries are nonnegative.

source
theorem Matrix.PosSemidef.isHermitian {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) :
M.IsHermitian
source
theorem Matrix.PosSemidef.re_dotProduct_nonneg {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {M : Matrix n n 𝕜} (hM : M.PosSemidef) (x : n → 𝕜) :
0 ≤ RCLike.re (star x ⬝ᵥ M.mulVec x)
source
theorem Matrix.PosSemidef.conjTranspose_mul_mul_same {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {A : Matrix n n R} (hA : A.PosSemidef) {m : Type u_6} [Fintype m] (B : Matrix n m R) :
(B.conjTranspose * A * B).PosSemidef
source
theorem Matrix.PosSemidef.mul_mul_conjTranspose_same {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {A : Matrix n n R} (hA : A.PosSemidef) {m : Type u_6} [Fintype m] (B : Matrix m n R) :
(B * A * B.conjTranspose).PosSemidef
source
theorem Matrix.PosSemidef.submatrix {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) (e : m → n) :
(M.submatrix e e).PosSemidef
source
theorem Matrix.PosSemidef.transpose {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] {M : Matrix n n R'} (hM : M.PosSemidef) :
M.transpose.PosSemidef
source
@[simp]
theorem Matrix.posSemidef_transpose_iff {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] {M : Matrix n n R'} :
M.transpose.PosSemidef ↔ M.PosSemidef
source
theorem Matrix.PosSemidef.conjTranspose {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) :
M.conjTranspose.PosSemidef
source
@[simp]
theorem Matrix.posSemidef_conjTranspose_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} :
M.conjTranspose.PosSemidef ↔ M.PosSemidef
source
theorem Matrix.PosSemidef.zero {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] :
PosSemidef 0
source
theorem Matrix.PosSemidef.one {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] :
PosSemidef 1
source
theorem Matrix.PosSemidef.natCast {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] (d : ℕ) :
(↑d).PosSemidef
source
theorem Matrix.PosSemidef.ofNat {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] (d : ℕ) [d.AtLeastTwo] :
(OfNat.ofNat d).PosSemidef
source
theorem Matrix.PosSemidef.intCast {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] (d : ℤ) (hd : 0 ≤ d) :
(↑d).PosSemidef
source
@[simp]
theorem Matrix.posSemidef_intCast_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [Nonempty n] [Nontrivial R] (d : ℤ) :
(↑d).PosSemidef ↔ 0 ≤ d
source
theorem Matrix.PosSemidef.pow {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] {M : Matrix n n R} (hM : M.PosSemidef) (k : ℕ) :
(M ^ k).PosSemidef
source
theorem Matrix.PosSemidef.inv {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] [DecidableEq n] {M : Matrix n n R'} (hM : M.PosSemidef) :
M⁻¹.PosSemidef
source
theorem Matrix.PosSemidef.zpow {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] [StarOrderedRing R'] [DecidableEq n] {M : Matrix n n R'} (hM : M.PosSemidef) (z : ℤ) :
(M ^ z).PosSemidef
source
theorem Matrix.PosSemidef.add {m : Type u_1} {R : Type u_3} [Fintype m] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A B : Matrix m m R} (hA : A.PosSemidef) (hB : B.PosSemidef) :
(A + B).PosSemidef
source
theorem Matrix.PosSemidef.smul {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {α : Type u_6} [CommSemiring α] [PartialOrder α] [StarRing α] [StarOrderedRing α] [Algebra α R] [StarModule α R] [PosSMulMono α R] {x : Matrix n n R} (hx : x.PosSemidef) {a : α} (ha : 0 ≤ a) :
(a • x).PosSemidef
source
theorem Matrix.PosSemidef.diag_nonneg {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {A : Matrix n n R} (hA : A.PosSemidef) {i : n} :
0 ≤ A i i
source
theorem Matrix.PosSemidef.trace_nonneg {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A : Matrix n n R} (hA : A.PosSemidef) :
0 ≤ A.trace
source
@[simp]
theorem Matrix.posSemidef_submatrix_equiv {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (e : m ≃ n) :
(M.submatrix ⇑e ⇑e).PosSemidef ↔ M.PosSemidef
source
theorem Matrix.posSemidef_conjTranspose_mul_self {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) :
(A.conjTranspose * A).PosSemidef

The conjugate transpose of a matrix multiplied by the matrix is positive semidefinite

source
theorem Matrix.posSemidef_self_mul_conjTranspose {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) :
(A * A.conjTranspose).PosSemidef

A matrix multiplied by its conjugate transpose is positive semidefinite

source
theorem Matrix.posSemidef_sum {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {ι : Type u_6} [AddLeftMono R] {x : ι → Matrix n n R} (s : Finset ι) (h : ∀ i ∈ s, (x i).PosSemidef) :
(∑ i ∈ s, x i).PosSemidef
source
theorem Matrix.trace_conjTranspose_mul_self_eq_zero_iff {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] {R : Type u_6} [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {A : Matrix m n R} :
(A.conjTranspose * A).trace = 0 ↔ A = 0
source
theorem Matrix.trace_mul_conjTranspose_self_eq_zero_iff {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] {R : Type u_6} [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {A : Matrix m n R} :
(A * A.conjTranspose).trace = 0 ↔ A = 0
source
theorem Matrix.IsUnit.posSemidef_star_left_conjugate_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [DecidableEq n] {U x : Matrix n n R} (hU : IsUnit U) :
(star U * x * U).PosSemidef ↔ x.PosSemidef

For an invertible matrix `U`, `star U * x * U` is positive semi-definite iff `x` is. This works on any ⋆-ring with a partial order.

See `IsUnit.star_left_conjugate_nonneg_iff` for a similar statement for star-ordered rings.

source
theorem Matrix.IsUnit.posSemidef_star_right_conjugate_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [DecidableEq n] {U x : Matrix n n R} (hU : IsUnit U) :
(U * x * star U).PosSemidef ↔ x.PosSemidef

For an invertible matrix `U`, `U * x * star U` is positive semi-definite iff `x` is. This works on any ⋆-ring with a partial order.

See `IsUnit.star_right_conjugate_nonneg_iff` for a similar statement for star-ordered rings.

source
theorem Matrix.posSemidef_vecMulVec_self_star {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (a : n → R) :
(vecMulVec a (star a)).PosSemidef

The matrix `vecMulVec a (star a)` is always positive semi-definite.

source
theorem Matrix.posSemidef_vecMulVec_star_self {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (a : n → R) :
(vecMulVec (star a) a).PosSemidef

The matrix `vecMulVec (star a) a` is always postive semi-definite.

## Positive definite matrices #

source
def Matrix.PosDef {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] (M : Matrix n n R) :
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

- M.PosDef = (M.IsHermitian ∧ ∀ (x : n → R), x ≠ 0 → 0 < star x ⬝ᵥ M.mulVec x)

Instances For

source
theorem Matrix.PosDef.isHermitian {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosDef) :
M.IsHermitian
source
theorem Matrix.PosDef.re_dotProduct_pos {n : Type u_2} {𝕜 : Type u_5} [Fintype n] [RCLike 𝕜] {M : Matrix n n 𝕜} (hM : M.PosDef) {x : n → 𝕜} (hx : x ≠ 0) :
0 < RCLike.re (star x ⬝ᵥ M.mulVec x)
source
theorem Matrix.PosDef.posSemidef {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosDef) :
M.PosSemidef
source
theorem Matrix.PosDef.transpose {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] {M : Matrix n n R'} (hM : M.PosDef) :
M.transpose.PosDef
source
@[simp]
theorem Matrix.PosDef.transpose_iff {n : Type u_2} {R' : Type u_4} [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] {M : Matrix n n R'} :
M.transpose.PosDef ↔ M.PosDef
source
theorem Matrix.PosDef.diagonal {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] {d : n → R} (h : ∀ (i : n), 0 < d i) :
(diagonal d).PosDef
source
@[simp]
theorem Matrix.posDef_diagonal_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nontrivial R] {d : n → R} :
(diagonal d).PosDef ↔ ∀ (i : n), 0 < d i
source
theorem Matrix.PosDef.one {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] :
PosDef 1
source
theorem Matrix.PosDef.natCast {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] (d : ℕ) (hd : d ≠ 0) :
(↑d).PosDef
source
@[simp]
theorem Matrix.posDef_natCast_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nonempty n] [Nontrivial R] {d : ℕ} :
(↑d).PosDef ↔ 0 < d
source
theorem Matrix.PosDef.ofNat {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] (d : ℕ) [d.AtLeastTwo] :
(OfNat.ofNat d).PosDef
source
theorem Matrix.PosDef.intCast {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] (d : ℤ) (hd : 0 < d) :
(↑d).PosDef
source
@[simp]
theorem Matrix.posDef_intCast_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nonempty n] [Nontrivial R] {d : ℤ} :
(↑d).PosDef ↔ 0 < d
source
theorem Matrix.PosDef.add_posSemidef {m : Type u_1} {R : Type u_3} [Fintype m] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A B : Matrix m m R} (hA : A.PosDef) (hB : B.PosSemidef) :
(A + B).PosDef
source
theorem Matrix.PosDef.posSemidef_add {m : Type u_1} {R : Type u_3} [Fintype m] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A B : Matrix m m R} (hA : A.PosSemidef) (hB : B.PosDef) :
(A + B).PosDef
source
theorem Matrix.PosDef.add {m : Type u_1} {R : Type u_3} [Fintype m] [Ring R] [PartialOrder R] [StarRing R] [AddLeftMono R] {A B : Matrix m m R} (hA : A.PosDef) (hB : B.PosDef) :
(A + B).PosDef
source
theorem Matrix.posDef_sum {m : Type u_1} {R : Type u_3} [Fintype m] [Ring R] [PartialOrder R] [StarRing R] {ι : Type u_6} [AddLeftMono R] {A : ι → Matrix m m R} {s : Finset ι} (hs : s.Nonempty) (hA : ∀ i ∈ s, (A i).PosDef) :
(∑ i ∈ s, A i).PosDef
source
theorem Matrix.PosDef.smul {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {α : Type u_6} [CommSemiring α] [PartialOrder α] [StarRing α] [StarOrderedRing α] [Algebra α R] [StarModule α R] [PosSMulStrictMono α R] {x : Matrix n n R} (hx : x.PosDef) {a : α} (ha : 0 < a) :
(a • x).PosDef
source
theorem Matrix.PosDef.conjTranspose_mul_mul_same {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {A : Matrix n n R} {B : Matrix n m R} (hA : A.PosDef) (hB : Function.Injective B.mulVec) :
(B.conjTranspose * A * B).PosDef
source
theorem Matrix.PosDef.mul_mul_conjTranspose_same {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {A : Matrix n n R} {B : Matrix m n R} (hA : A.PosDef) (hB : Function.Injective fun (v : m → R) => vecMul v B) :
(B * A * B.conjTranspose).PosDef
source
theorem Matrix.PosDef.conjTranspose_mul_self {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (hA : Function.Injective A.mulVec) :
(A.conjTranspose * A).PosDef
source
theorem Matrix.PosDef.mul_conjTranspose_self {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R] (A : Matrix m n R) (hA : Function.Injective fun (v : m → R) => vecMul v A) :
(A * A.conjTranspose).PosDef
source
theorem Matrix.PosDef.conjTranspose {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosDef) :
M.conjTranspose.PosDef
source
@[simp]
theorem Matrix.posDef_conjTranspose_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] {M : Matrix n n R} :
M.conjTranspose.PosDef ↔ M.PosDef
source
theorem Matrix.PosDef.of_toQuadraticForm' {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.IsSymm) (hMq : M.toQuadraticMap'.PosDef) :
M.PosDef
source
theorem Matrix.PosDef.toQuadraticForm' {n : Type u_2} [Fintype n] [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosDef) :
M.toQuadraticMap'.PosDef
source
theorem Matrix.PosDef.diag_pos {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [Nontrivial R] {A : Matrix n n R} (hA : A.PosDef) {i : n} :
0 < A i i
source
theorem Matrix.PosDef.trace_pos {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [Nontrivial R] [IsOrderedCancelAddMonoid R] [Nonempty n] {A : Matrix n n R} (hA : A.PosDef) :
0 < A.trace
source
theorem Matrix.PosDef.isUnit {n : Type u_2} [Fintype n] {K : Type u_6} [Field K] [PartialOrder K] [StarRing K] [DecidableEq n] {M : Matrix n n K} (hM : M.PosDef) :
IsUnit M
source
theorem Matrix.PosDef.inv {n : Type u_2} [Fintype n] {K : Type u_6} [Field K] [PartialOrder K] [StarRing K] [DecidableEq n] {M : Matrix n n K} (hM : M.PosDef) :
M⁻¹.PosDef
source
@[simp]
theorem Matrix.posDef_inv_iff {n : Type u_2} [Fintype n] {K : Type u_6} [Field K] [PartialOrder K] [StarRing K] [DecidableEq n] {M : Matrix n n K} :
M⁻¹.PosDef ↔ M.PosDef
source
theorem Matrix.IsUnit.posDef_star_left_conjugate_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [DecidableEq n] {x U : Matrix n n R} (hU : IsUnit U) :
(star U * x * U).PosDef ↔ x.PosDef

For an invertible matrix `U`, `star U * x * U` is positive definite iff `x` is. This works on any ⋆-ring with a partial order.

See `IsUnit.isStrictlyPositive_star_left_conjugate_iff'` for a similar statement for star-ordered rings. For matrices, positive definiteness is equivalent to strict positivity when the underlying field is `ℝ` or `ℂ` (see `Matrix.isStrictlyPositive_iff_posDef`).

source
theorem Matrix.IsUnit.posDef_star_right_conjugate_iff {n : Type u_2} {R : Type u_3} [Fintype n] [Ring R] [PartialOrder R] [StarRing R] [DecidableEq n] {x U : Matrix n n R} (hU : IsUnit U) :
(U * x * star U).PosDef ↔ x.PosDef

For an invertible matrix `U`, `U * x * star U` is positive definite iff `x` is. This works on any ⋆-ring with a partial order.

See `IsUnit.isStrictlyPositive_star_right_conjugate_iff` for a similar statement for star-ordered rings. For matrices, positive definiteness is equivalent to strict positivity when the underlying field is `ℝ` or `ℂ` (see `Matrix.isStrictlyPositive_iff_posDef`).

source
theorem Matrix.PosDef.fromBlocks₁₁ {m : Type u_1} {n : Type u_2} {R' : Type u_4} [Fintype m] [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] [StarOrderedRing R'] [DecidableEq m] {A : Matrix m m R'} (B : Matrix m n R') (D : Matrix n n R') (hA : A.PosDef) [Invertible A] :
(fromBlocks A B B.conjTranspose D).PosSemidef ↔ (D - B.conjTranspose * A⁻¹ * B).PosSemidef
source
theorem Matrix.PosDef.fromBlocks₂₂ {m : Type u_1} {n : Type u_2} {R' : Type u_4} [Fintype m] [Fintype n] [CommRing R'] [PartialOrder R'] [StarRing R'] [StarOrderedRing R'] [DecidableEq n] (A : Matrix m m R') (B : Matrix m n R') {D : Matrix n n R'} (hD : D.PosDef) [Invertible D] :
(fromBlocks A B B.conjTranspose D).PosSemidef ↔ (A - B * D⁻¹ * B.conjTranspose).PosSemidef
source
theorem QuadraticForm.posDef_of_toMatrix' {n : Type u_1} [Fintype n] [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)} (hQ : (QuadraticMap.toMatrix' Q).PosDef) :
QuadraticMap.PosDef Q
source
theorem QuadraticForm.posDef_toMatrix' {n : Type u_1} [Fintype n] [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)} (hQ : QuadraticMap.PosDef Q) :
(QuadraticMap.toMatrix' Q).PosDef
source
@[reducible, inline]
noncomputable abbrev Matrix.NormedAddCommGroup.ofMatrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {M : Matrix n n 𝕜} (hM : M.PosDef) :
NormedAddCommGroup (n → 𝕜)

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

Equations

- Matrix.NormedAddCommGroup.ofMatrix hM = InnerProductSpace.Core.toNormedAddCommGroup

Instances For

source
def Matrix.InnerProductSpace.ofMatrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {M : Matrix n n 𝕜} (hM : M.PosDef) :
InnerProductSpace 𝕜 (n → 𝕜)

A positive definite matrix `M` induces an inner product `⟪x, y⟫ = xᴴMy`.

Equations

- One or more equations did not get rendered due to their size.

Instances For