Documentation Verification Report

PosDef

📁 Source: Mathlib/Analysis/Matrix/PosDef.lean

Statistics

Metric	Count
Definitions `ofMatrix`, `ofMatrix`, `toInnerProductSpace`, `toNormedAddCommGroup`, `toSeminormedAddCommGroup`	5
Theorems `posDef_iff_eigenvalues_pos`, `posSemidef_iff_eigenvalues_nonneg`, `posSemidef_of_eigenvalues_nonneg`, `det_pos`, `eigenvalues_pos`, `re_dotProduct_pos`, `det_nonneg`, `eigenvalues_nonneg`, `re_dotProduct_nonneg`, `trace_eq_zero_iff`, `eigenvalues_conjTranspose_mul_self_nonneg`, `eigenvalues_self_mul_conjTranspose_nonneg`	12
Total	17

Matrix

Definitions

Name	Category	Theorems
`toInnerProductSpace` 📖	CompOp	1 math math: `LDL.lowerInv_eq_gramSchmidtBasis`
`toNormedAddCommGroup` 📖	CompOp	1 math math: `LDL.lowerInv_eq_gramSchmidtBasis`
`toSeminormedAddCommGroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eigenvalues_conjTranspose_mul_self_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `IsHermitian.eigenvalues` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `RCLike.toStarRing` `isHermitian_conjTranspose_mul_self`	—	`PosSemidef.eigenvalues_nonneg` `posSemidef_conjTranspose_mul_self` `Finite.of_fintype` `RCLike.toStarOrderedRing`
`eigenvalues_self_mul_conjTranspose_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `IsHermitian.eigenvalues` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `RCLike.toStarRing` `isHermitian_mul_conjTranspose_self`	—	`PosSemidef.eigenvalues_nonneg` `posSemidef_self_mul_conjTranspose` `Finite.of_fintype` `RCLike.toStarOrderedRing`

Matrix.InnerProductSpace

Definitions

Name	Category	Theorems
`ofMatrix` 📖	CompOp	—

Matrix.IsHermitian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`posDef_iff_eigenvalues_pos` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `StarRing.toStarAddMonoid` `RCLike.toStarRing`	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `RCLike.toPartialOrder` `Real` `Real.instLT` `Real.instZero` `eigenvalues`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `spectral_theorem` `Matrix.IsUnit.posDef_star_right_conjugate_iff` `Unitary.isUnit_coe` `RCLike.toStarOrderedRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`posSemidef_iff_eigenvalues_nonneg` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `StarRing.toStarAddMonoid` `RCLike.toStarRing`	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `RCLike.toPartialOrder` `Pi.hasLe` `Real` `Real.instLE` `Pi.instZero` `Real.instZero` `eigenvalues`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `spectral_theorem` `Matrix.IsUnit.posSemidef_star_right_conjugate_iff` `Unitary.isUnit_coe` `RCLike.toStarOrderedRing`
`posSemidef_of_eigenvalues_nonneg` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `StarRing.toStarAddMonoid` `RCLike.toStarRing` `Pi.hasLe` `Real` `Real.instLE` `Pi.instZero` `Real.instZero` `eigenvalues`	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `RCLike.toPartialOrder`	—	`posSemidef_iff_eigenvalues_nonneg`

Matrix.NormedAddCommGroup

Definitions

Name	Category	Theorems
`ofMatrix` 📖	CompOp	—

Matrix.PosDef

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_pos` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Matrix.det` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField`	—	`isHermitian` `Matrix.IsHermitian.det_eq_prod_eigenvalues` `Finset.prod_pos` `RCLike.toZeroLEOneClass` `IsStrictOrderedRing.toPosMulStrictMono` `RCLike.toIsStrictOrderedRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `eigenvalues_pos`
`eigenvalues_pos` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Real` `Real.instLT` `Real.instZero` `Matrix.IsHermitian.eigenvalues` `Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid`	—	`isHermitian` `Matrix.IsHermitian.posDef_iff_eigenvalues_pos`
`re_dotProduct_pos` 📖	mathematical	`Matrix.PosDef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `Matrix.mulVec`	—	`RCLike.pos_iff` `dotProduct_mulVec_pos`

Matrix.PosSemidef

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_nonneg` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Matrix.det` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField`	—	`isHermitian` `Matrix.IsHermitian.det_eq_prod_eigenvalues` `Finset.prod_nonneg` `RCLike.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `StarOrderedRing.toIsOrderedRing` `RCLike.toStarOrderedRing` `eigenvalues_nonneg`
`eigenvalues_nonneg` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Real` `Real.instLE` `Real.instZero` `Matrix.IsHermitian.eigenvalues` `Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid`	—	`isHermitian` `Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg`
`re_dotProduct_nonneg` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `Matrix.mulVec`	—	`RCLike.nonneg_iff` `dotProduct_mulVec_nonneg`
`trace_eq_zero_iff` 📖	mathematical	`Matrix.PosSemidef` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toPartialOrder` `RCLike.toStarRing`	`Matrix.trace` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Matrix` `Matrix.zero`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `Matrix.IsHermitian.spectral_theorem` `Unitary.conjStarAlgAut_apply` `Matrix.trace_mul_cycle` `Unitary.coe_star_mul_self` `one_mul` `Matrix.trace_diagonal` `Finset.sum_eq_zero_iff_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `RCLike.toIsOrderedAddMonoid` `eigenvalues_nonneg` `isHermitian` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Matrix.IsHermitian.eigenvalues_eq_zero_iff`

---

← Back to Index