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 matrixM : Matrix n n Ris positive semidefinite if it is Hermitian andxᴴMxis nonnegative for allx.Matrix.PosDef: a matrixM : Matrix n n Ris positive definite if it is Hermitian andxᴴMxis greater than zero for all nonzerox.
Main results #
Matrix.PosSemidef.fromBlocks₁₁andMatrix.PosSemidef.fromBlocks₂₂: If a matrixAis positive definite, then[A B; Bᴴ D]is positive semidefinite if and only ifD - Bᴴ A⁻¹ Bis positive semidefinite.Matrix.PosDef.isUnit: A positive definite matrix in a field is invertible.
Positive semidefinite matrices #
def
Matrix.PosSemidef
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
(M : Matrix n n R)
:
A matrix M : Matrix n n R is positive semidefinite if it is Hermitian and xᴴ * M * x is
nonnegative for all x of finite support.
Equations
Instances For
theorem
Matrix.PosSemidef.diagonal
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
{d : n → R}
(h : 0 ≤ d)
:
(diagonal d).PosSemidef
@[simp]
theorem
Matrix.posSemidef_diagonal_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
{d : n → R}
:
A diagonal matrix is positive semidefinite iff its diagonal entries are nonnegative.
theorem
Matrix.PosSemidef.isHermitian
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{M : Matrix n n R}
(hM : M.PosSemidef)
:
theorem
Matrix.PosSemidef.submatrix
{m : Type u_1}
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{M : Matrix n n R}
(hM : M.PosSemidef)
(e : m → n)
:
(M.submatrix e e).PosSemidef
theorem
Matrix.PosSemidef.transpose
{n : Type u_2}
{R' : Type u_4}
[CommRing R']
[PartialOrder R']
[StarRing R']
{M : Matrix n n R'}
(hM : M.PosSemidef)
:
@[simp]
theorem
Matrix.posSemidef_transpose_iff
{n : Type u_2}
{R' : Type u_4}
[CommRing R']
[PartialOrder R']
[StarRing R']
{M : Matrix n n R'}
:
theorem
Matrix.PosSemidef.conjTranspose
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{M : Matrix n n R}
(hM : M.PosSemidef)
:
@[simp]
theorem
Matrix.posSemidef_conjTranspose_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{M : Matrix n n R}
:
theorem
Matrix.PosSemidef.add
{m : Type u_1}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[AddLeftMono R]
{A B : Matrix m m R}
(hA : A.PosSemidef)
(hB : B.PosSemidef)
:
(A + B).PosSemidef
theorem
Matrix.PosSemidef.smul
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{α : Type u_5}
[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
theorem
Matrix.PosSemidef.zero
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
:
theorem
Matrix.PosSemidef.one
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
:
theorem
Matrix.PosSemidef.natCast
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
(d : ℕ)
:
(↑d).PosSemidef
theorem
Matrix.PosSemidef.ofNat
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
(d : ℕ)
[d.AtLeastTwo]
:
theorem
Matrix.PosSemidef.intCast
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
(d : ℤ)
(hd : 0 ≤ d)
:
(↑d).PosSemidef
@[simp]
theorem
Matrix.posSemidef_intCast_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
[Nonempty n]
[Nontrivial R]
(d : ℤ)
:
theorem
Matrix.PosSemidef.diag_nonneg
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{A : Matrix n n R}
(hA : A.PosSemidef)
{i : n}
:
@[simp]
theorem
Matrix.posSemidef_submatrix_equiv
{m : Type u_1}
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{M : Matrix n n R}
(e : m ≃ n)
:
theorem
Matrix.posSemidef_sum
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{ι : Type u_5}
[AddLeftMono R]
{x : ι → Matrix n n R}
(s : Finset ι)
(h : ∀ i ∈ s, (x i).PosSemidef)
:
(∑ i ∈ s, x i).PosSemidef
Positive definite matrices #
def
Matrix.PosDef
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
(M : Matrix n n R)
:
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
Instances For
theorem
Matrix.PosDef.isHermitian
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{M : Matrix n n R}
(hM : M.PosDef)
:
theorem
Matrix.PosDef.posSemidef
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{M : Matrix n n R}
(hM : M.PosDef)
:
theorem
Matrix.PosDef.transpose
{n : Type u_2}
{R' : Type u_4}
[CommRing R']
[PartialOrder R']
[StarRing R']
{M : Matrix n n R'}
(hM : M.PosDef)
:
@[simp]
theorem
Matrix.PosDef.diagonal
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
[NoZeroDivisors R]
{d : n → R}
(h : ∀ (i : n), 0 < d i)
:
@[simp]
theorem
Matrix.posDef_diagonal_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
[NoZeroDivisors R]
[Nontrivial R]
{d : n → R}
:
@[simp]
theorem
Matrix.PosDef.of_subsingleton
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
(h : Subsingleton R)
(M : Matrix n n R)
:
M.PosDef
theorem
Matrix.PosDef.one
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
[NoZeroDivisors R]
:
PosDef 1
theorem
Matrix.PosDef.natCast
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
[NoZeroDivisors R]
(d : ℕ)
(hd : d ≠ 0)
:
(↑d).PosDef
@[simp]
theorem
Matrix.posDef_natCast_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
[NoZeroDivisors R]
[Nonempty n]
[Nontrivial R]
{d : ℕ}
:
theorem
Matrix.PosDef.ofNat
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
[NoZeroDivisors R]
(d : ℕ)
[d.AtLeastTwo]
:
(OfNat.ofNat d).PosDef
theorem
Matrix.PosDef.intCast
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
[NoZeroDivisors R]
(d : ℤ)
(hd : 0 < d)
:
(↑d).PosDef
@[simp]
theorem
Matrix.posDef_intCast_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[StarOrderedRing R]
[DecidableEq n]
[NoZeroDivisors R]
[Nonempty n]
[Nontrivial R]
{d : ℤ}
:
theorem
Matrix.PosDef.add_posSemidef
{m : Type u_1}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[AddLeftMono R]
{A B : Matrix m m R}
(hA : A.PosDef)
(hB : B.PosSemidef)
:
theorem
Matrix.PosDef.posSemidef_add
{m : Type u_1}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[AddLeftMono R]
{A B : Matrix m m R}
(hA : A.PosSemidef)
(hB : B.PosDef)
:
theorem
Matrix.PosDef.add
{m : Type u_1}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[AddLeftMono R]
{A B : Matrix m m R}
(hA : A.PosDef)
(hB : B.PosDef)
:
theorem
Matrix.posDef_sum
{m : Type u_1}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{ι : Type u_5}
[AddLeftMono R]
{A : ι → Matrix m m R}
{s : Finset ι}
(hs : s.Nonempty)
(hA : ∀ i ∈ s, (A i).PosDef)
:
(∑ i ∈ s, A i).PosDef
theorem
Matrix.PosDef.smul
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{α : Type u_5}
[CommSemiring α]
[PartialOrder α]
[StarRing α]
[StarOrderedRing α]
[Algebra α R]
[StarModule α R]
[PosSMulStrictMono α R]
{x : Matrix n n R}
(hx : x.PosDef)
{a : α}
(ha : 0 < a)
:
theorem
Matrix.PosDef.conjTranspose
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{M : Matrix n n R}
(hM : M.PosDef)
:
@[simp]
theorem
Matrix.posDef_conjTranspose_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
{M : Matrix n n R}
:
theorem
Matrix.PosDef.diag_pos
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Nontrivial R]
{A : Matrix n n R}
(hA : A.PosDef)
{i : n}
:
Finite positive semidefinite matrices #
theorem
Matrix.posSemidef_iff_dotProduct_mulVec
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
{M : Matrix n n R}
:
A finite matrix M : Matrix n n R is positive semidefinite iff it is
Hermitian and xᴴ * M * x is nonnegative for all x.
@[simp]
theorem
Matrix.PosSemidef.dotProduct_mulVec_nonneg
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
{M : Matrix n n R}
(hM : M.PosSemidef)
(x : n → R)
:
theorem
Matrix.PosSemidef.of_dotProduct_mulVec_nonneg
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
{M : Matrix n n R}
(hM1 : M.IsHermitian)
(hM2 : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ M.mulVec x)
:
theorem
Matrix.PosSemidef.conjTranspose_mul_mul_same
{m : Type u_1}
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[Finite m]
{A : Matrix n n R}
(hA : A.PosSemidef)
(B : Matrix n m R)
:
(B.conjTranspose * A * B).PosSemidef
theorem
Matrix.PosSemidef.mul_mul_conjTranspose_same
{m : Type u_1}
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[Finite m]
{A : Matrix n n R}
(hA : A.PosSemidef)
(B : Matrix m n R)
:
(B * A * B.conjTranspose).PosSemidef
theorem
Matrix.PosSemidef.pow
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[StarOrderedRing R]
[DecidableEq n]
{M : Matrix n n R}
(hM : M.PosSemidef)
(k : ℕ)
:
(M ^ k).PosSemidef
theorem
Matrix.PosSemidef.inv
{n : Type u_2}
{R' : Type u_4}
[CommRing R']
[PartialOrder R']
[StarRing R']
[Fintype n]
[DecidableEq n]
{M : Matrix n n R'}
(hM : M.PosSemidef)
:
theorem
Matrix.PosSemidef.zpow
{n : Type u_2}
{R' : Type u_4}
[CommRing R']
[PartialOrder R']
[StarRing R']
[Fintype n]
[StarOrderedRing R']
[DecidableEq n]
{M : Matrix n n R'}
(hM : M.PosSemidef)
(z : ℤ)
:
(M ^ z).PosSemidef
theorem
Matrix.PosSemidef.trace_nonneg
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[AddLeftMono R]
{A : Matrix n n R}
(hA : A.PosSemidef)
:
theorem
Matrix.posSemidef_conjTranspose_mul_self
{m : Type u_1}
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype m]
[Finite n]
[StarOrderedRing R]
(A : Matrix m n R)
:
(A.conjTranspose * A).PosSemidef
The conjugate transpose of a matrix multiplied by the matrix is positive semidefinite
theorem
Matrix.posSemidef_self_mul_conjTranspose
{m : Type u_1}
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[Finite m]
[StarOrderedRing R]
(A : Matrix m n R)
:
(A * A.conjTranspose).PosSemidef
A matrix multiplied by its conjugate transpose is positive semidefinite
theorem
Matrix.trace_conjTranspose_mul_self_eq_zero_iff
{m : Type u_1}
{n : Type u_2}
[Fintype n]
[Fintype m]
{R : Type u_5}
[PartialOrder R]
[NonUnitalRing R]
[StarRing R]
[StarOrderedRing R]
[NoZeroDivisors R]
{A : Matrix m n R}
:
theorem
Matrix.trace_mul_conjTranspose_self_eq_zero_iff
{m : Type u_1}
{n : Type u_2}
[Fintype n]
[Fintype m]
{R : Type u_5}
[PartialOrder R]
[NonUnitalRing R]
[StarRing R]
[StarOrderedRing R]
[NoZeroDivisors R]
{A : Matrix m n R}
:
theorem
Matrix.IsUnit.posSemidef_star_left_conjugate_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[DecidableEq n]
{U x : Matrix n n R}
(hU : IsUnit U)
:
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.
theorem
Matrix.IsUnit.posSemidef_star_right_conjugate_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[DecidableEq n]
{U x : Matrix n n R}
(hU : IsUnit U)
:
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.
theorem
Matrix.posSemidef_vecMulVec_self_star
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Finite n]
[StarOrderedRing R]
(a : n → R)
:
(vecMulVec a (star a)).PosSemidef
The matrix vecMulVec a (star a) is always positive semi-definite.
theorem
Matrix.posSemidef_vecMulVec_star_self
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Finite n]
[StarOrderedRing R]
(a : n → R)
:
(vecMulVec (star a) a).PosSemidef
The matrix vecMulVec (star a) a is always positive semi-definite.
Finite Positive definite matrices #
@[simp]
theorem
Matrix.PosDef.dotProduct_mulVec_pos
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
{M : Matrix n n R}
(hM : M.PosDef)
{x : n → R}
(hx : x ≠ 0)
:
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.
theorem
Matrix.PosDef.of_dotProduct_mulVec_pos
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
{M : Matrix n n R}
(hM1 : M.IsHermitian)
(hM2 : ∀ ⦃x : n → R⦄, x ≠ 0 → 0 < star x ⬝ᵥ M.mulVec x)
:
M.PosDef
theorem
Matrix.PosDef.conjTranspose_mul_mul_same
{m : Type u_1}
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[Fintype m]
{A : Matrix n n R}
{B : Matrix n m R}
(hA : A.PosDef)
(hB : Function.Injective B.mulVec)
:
(B.conjTranspose * A * B).PosDef
theorem
Matrix.PosDef.mul_mul_conjTranspose_same
{m : Type u_1}
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[Fintype m]
{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
theorem
Matrix.PosDef.conjTranspose_mul_self
{m : Type u_1}
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[Fintype m]
[StarOrderedRing R]
[NoZeroDivisors R]
(A : Matrix m n R)
(hA : Function.Injective A.mulVec)
:
(A.conjTranspose * A).PosDef
theorem
Matrix.PosDef.mul_conjTranspose_self
{m : Type u_1}
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[Fintype m]
[StarOrderedRing R]
[NoZeroDivisors R]
(A : Matrix m n R)
(hA : Function.Injective fun (v : m → R) => vecMul v A)
:
(A * A.conjTranspose).PosDef
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
theorem
Matrix.PosDef.toQuadraticForm'
{n : Type u_2}
[Fintype n]
[DecidableEq n]
{M : Matrix n n ℝ}
(hM : M.PosDef)
:
theorem
Matrix.PosDef.trace_pos
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[Nontrivial R]
[IsOrderedCancelAddMonoid R]
[Nonempty n]
{A : Matrix n n R}
(hA : A.PosDef)
:
theorem
Matrix.PosDef.isUnit
{n : Type u_2}
[Fintype n]
{K : Type u_5}
[Field K]
[PartialOrder K]
[StarRing K]
[DecidableEq n]
{M : Matrix n n K}
(hM : M.PosDef)
:
IsUnit M
theorem
Matrix.PosDef.inv
{n : Type u_2}
[Fintype n]
{K : Type u_5}
[Field K]
[PartialOrder K]
[StarRing K]
[DecidableEq n]
{M : Matrix n n K}
(hM : M.PosDef)
:
@[simp]
theorem
Matrix.posDef_inv_iff
{n : Type u_2}
[Fintype n]
{K : Type u_5}
[Field K]
[PartialOrder K]
[StarRing K]
[DecidableEq n]
{M : Matrix n n K}
:
theorem
Matrix.IsUnit.posDef_star_left_conjugate_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[DecidableEq n]
{x U : Matrix n n R}
(hU : IsUnit U)
:
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).
theorem
Matrix.IsUnit.posDef_star_right_conjugate_iff
{n : Type u_2}
{R : Type u_3}
[Ring R]
[PartialOrder R]
[StarRing R]
[Fintype n]
[DecidableEq n]
{x U : Matrix n n R}
(hU : IsUnit U)
:
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).
theorem
Matrix.PosDef.fromBlocks₁₁
{m : Type u_1}
{n : Type u_2}
{R' : Type u_4}
[CommRing R']
[PartialOrder R']
[StarRing R']
[Fintype m]
[StarOrderedRing R']
[Finite n]
[DecidableEq m]
{A : Matrix m m R'}
(B : Matrix m n R')
(D : Matrix n n R')
(hA : A.PosDef)
[Invertible A]
:
theorem
Matrix.PosDef.fromBlocks₂₂
{m : Type u_1}
{n : Type u_2}
{R' : Type u_4}
[CommRing R']
[PartialOrder R']
[StarRing R']
[Fintype n]
[StarOrderedRing R']
[Finite m]
[DecidableEq n]
(A : Matrix m m R')
(B : Matrix m n R')
{D : Matrix n n R'}
(hD : D.PosDef)
[Invertible D]
:
theorem
QuadraticForm.posDef_of_toMatrix'
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{Q : QuadraticForm ℝ (n → ℝ)}
(hQ : (QuadraticMap.toMatrix' Q).PosDef)
:
theorem
QuadraticForm.posDef_toMatrix'
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{Q : QuadraticForm ℝ (n → ℝ)}
(hQ : QuadraticMap.PosDef Q)
: