Zulip Chat Archive

Stream: maths

Topic: Hermitian and semidefinite matrices


view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Sep 02 2020 at 20:43):

This could use the is_R_or_C class that was mentioned also.

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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