Contribute Schur decomposition

Stream: mathlib4

[Gordon Hsu]

Hi, I am a programmer working in the semiconductor industry. My GitHub handle is kuotsanhsu. I have been learning about Lean4 in my spare time, and I am convinced that the industry can benefit from certified programming a la Adam Chlipala. Recently, I tried contributing to the HepLean project, and I formalized the Schur decomposition during the process. I would like to upstream Matrix.schur_triangulation to Mathlib. Since this is my first time contributing to Mathlib, how should I go about this? Also, is anyone working on formalizing the Jordan normal form? If not, I would like to give it a try.

[Luigi Massacci]

See here for the contribution guide, and for github access you just need to wait for an admin to click on this thread. If it doesn’t happen in a reasonable timeframe, ask on #mathlib4 > github permission

[Kim Morrison]

@Gordon Hsu, would you mind adding your github handle to your zulip profile information? It's often helpful for reviewers.

[Kim Morrison]

@Gordon Hsu, please check your (email) inbox for the invitation.

[Gordon Hsu]

Thanks, I have created PR#20730. Could someone review it?

[David Loeffler]

Also, is anyone working on formalizing the Jordan normal form? If not, I would like to give it a try.

Tagging @Alex Brodbelt who has been looking at this.

[Alex Brodbelt]

I have only formalized the 2x2 case (essentially by brute force), the general nxn case I have not touched.

[Alex Brodbelt]

I was thinking of classifying nilpotent matrices and proving some results about these, but haven't got round to this and I am not sure I will any time soon.

[Gordon Hsu]

I see, here's what I will try:

As commented by Kevin Buzzard somewhere in Zulip and the Mathlib doc, I shall start with Mathlib.LinearAlgebra.JordanChevalley and prove the case where the linear map has just one eigenvalue, i.e., the argument k to Module.End.HasGenEigenvector is Module.finrank R E for f : Module.End R E. Then, generalize to linear maps with more than one eigenvalues by way of DirectSum.Decomposition. From my experience with proving the Schur decomposition, it's easier to start with linear maps. Then, the decomposition of a matrix can be justified with Matrix.toEuclideanLin.

[Matteo Cipollina]

This file in PhysLean provides Matrix.det_exp for AlgClosed C and for reals, which I needed to prove several results regarding Lorentz Algebra and LorentzGroup, in particular that the exponential of an element of the Lorentz algebra is a member of the Lorentz group.

https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Mathematics/DataStructures/Matrix/LieTrace.lean
https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Relativity/LorentzAlgebra/ExponentialMap.lean

I 'd like to PR it to Mathlib since it is a TODO in Analysis.Normed.Algebra.MatrixExponential, but It depends on SchurTriangulation in #20730 (originally PRd to PhysLean), which seems to be stuck. I also cannot build on the fork because in conflict and cannot merge master according to the reviews, the PR needed some clean-up before merging, so I have DM'd the author offering help to address the comments and complete the PR but haven't had an answer yet. Perhaps this message here helps reaching out to him :)

[Yaël Dillies]

How long has it been since you DMed? #20730 is made from the repo and therefore will need to be closed for you or the original author to edit it. Maybe it's a good opportunity for you to take over the PR

[Matteo Cipollina]

Yaël Dillies ha scritto:

How long has it been since you DMed? #20730 is made from the repo and therefore will need to be closed for you or the original author to edit it. Maybe it's a good opportunity for you to take over the PR

It has been one week now, let's see, if nothing happens I'm fine to take it over - with all credits to him of course

[Eric Wieser]

Instead of directly taking it over, you could instead create a new PR with some of the helper lemmas (as I suggested in https://github.com/leanprover-community/mathlib4/pull/20730/files#r1931348621), and mark it Co-authored-by in the commit message to attribute credit

[Eric Wieser]

Relatedly, you might want to try to adapt https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Mathematics/DataStructures/Matrix/LieTrace.lean#L29-L107 to use docs#Matrix.BlockTriangular instead

[Ruben Van de Velde]

Though note there's a new guideline about using empty commits to tag coauthors

[Matteo Cipollina]

Eric Wieser ha scritto:

Relatedly, you might want to try to adapt https://github.com/HEPLean/PhysLean/blob/master/PhysLean/Mathematics/DataStructures/Matrix/LieTrace.lean#L29-L107 to use docs#Matrix.BlockTriangular instead

thanks, refactoring with BlockTriangular was indeed necessary : +119 −204

https://github.com/HEPLean/PhysLean/pull/678

[Eric Wieser]

Excellent!