Commit 2025-12-09 04:22 44344519

View on Github →

refactor(LinearAlgebra/Matrix): generalize positive semidefinite matrices to infinite dimensions (#31746)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/GramMatrix.lean

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/Analysis/Matrix/Order.lean

Modified Mathlib/Analysis/Matrix/PosDef.lean

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

Modified Mathlib/Data/Finsupp/Defs.lean

added theorem Finsupp.mapRange_eq_zero

Modified Mathlib/Data/Finsupp/Order.lean

added theorem Finsupp.sum_pos'

added theorem Finsupp.sum_pos

Modified Mathlib/Data/Matrix/Diagonal.lean

added theorem Matrix.intCast_apply

Modified Mathlib/LinearAlgebra/Matrix/PosDef.lean

added theorem Matrix.PosDef.dotProduct_mulVec_pos

added theorem Matrix.PosDef.of_dotProduct_mulVec_pos

added theorem Matrix.PosDef.of_subsingleton

modified theorem Matrix.PosDef.posSemidef

modified theorem Matrix.PosSemidef.conjTranspose_mul_mul_same

added theorem Matrix.PosSemidef.dotProduct_mulVec_nonneg

modified theorem Matrix.PosSemidef.mul_mul_conjTranspose_same

added theorem Matrix.PosSemidef.of_dotProduct_mulVec_nonneg

modified def Matrix.PosSemidef

added theorem Matrix.posDef_iff_dotProduct_mulVec

modified theorem Matrix.posSemidef_diagonal_iff

added theorem Matrix.posSemidef_iff_dotProduct_mulVec

Modified Mathlib/LinearAlgebra/SesquilinearForm/Star.lean