Hermitian and semidefinite matrices

Stream: maths

[Yakov Pechersky]

Now that we have eigenvalues, is anyone working on defining Hermitian matrices, positive semidefinite matrices, the order on them, eigendecompositions? Someone mentioned they are working on formalizing the spectral theorem.

[Yakov Pechersky]

This could use the is_R_or_C class that was mentioned also.

[Frédéric Dupuis]

I'm currently working on defining inner products based on is_R_or_C, so we should have complex inner products fairly soon, and hopefully stating results for both the real and complex case should be reasonable comfortable (at least I hope!). And then we can define the adjoint, Hermitian operators, and so on!

[Frédéric Dupuis]

There is now a work-in-progress PR for this here: #4057. Comments are very welcome!

[Alexander Bentkamp]

I am working on getting the theorem "generalized eigenvectors span the vectorspace" into mathlib. This should be another important ingredient of the spectral theorem, complementing @Frédéric Dupuis 's work. It will roughly look like this pull request, which I am now splitting into smaller parts: https://github.com/leanprover-community/mathlib/pull/3864

[Frédéric Dupuis]

Looks good! We'll be in very good shape soon for the spectral theorem I think.