Yakov Pechersky (Sep 02 2020 at 20:42):
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 (Sep 02 2020 at 20:43):
This could use the
is_R_or_C class that was mentioned also.
Frédéric Dupuis (Sep 03 2020 at 00:13):
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 (Sep 07 2020 at 00:37):
There is now a work-in-progress PR for this here: #4057. Comments are very welcome!
Alexander Bentkamp (Sep 08 2020 at 14:10):
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 (Sep 08 2020 at 23:41):
Looks good! We'll be in very good shape soon for the spectral theorem I think.
Last updated: May 19 2021 at 02:10 UTC