Dan Packer - Matrix Theory in Mathlib?

Stream: new members

[Daniel Packer]

Hi all!
I'm Dan Packer, a grad student in Applied Mathematics at Ohio State University. I'm pretty new to the whole formalization effort, but I'm interested in the idea of using proof checkers to verify results in my field. To this end, I'm wondering how much basic matrix theory (e.g. singular values, trace cyclic property, pseudo-inverses...) has been developed in mathlib (and whether that is the right place to be developing it at all!) I ultimately want to show some results in a specific paper, but it seems worthwhile to contribute to mathlib if it's appropriate.

[Johan Commelin]

@Daniel Packer welcome! I don't think singular values are done, but we have eigenvalues and we have Mᴴ M. The trace cyclic property is done. What exactly are pseudo-inverses in this context?

[Anne Baanen]

Hi! At the moment we don't have a lot in that area. I was planning on working towards pseudoinverses a couple of years ago, but never really got there. Would probably be a nice project to get started with, since the various decompositions would also be very helpful!

[Daniel Packer]

Thanks! The Moore-Penrose pseudo-inverse is what I'm imagining: https://en.wikipedia.org/wiki/Moore%E2%80%93Penrose_inverse
Some results might involve that the formulas for it hold when you have linearly independent rows/columns, that it minimizes 2-norm

[Johan Commelin]

Dan, do you want to focus on proving things, or on computing things? Because it turns out that these are quite different things and typically require different definitions (which you can prove are equal in the end).

[Daniel Packer]

@Anne Baanen Awesome! I would be pretty excited to work in that direction. What library in mathlib should I be building off of?

[Daniel Packer]

@Johan Commelin I'm mostly interested in proving things (I think)

[Johan Commelin]

ls src/data/matrix/*.lean
src/data/matrix/basic.lean  src/data/matrix/block.lean   src/data/matrix/dmatrix.lean   src/data/matrix/kronecker.lean  src/data/matrix/pequiv.lean
src/data/matrix/basis.lean  src/data/matrix/char_p.lean  src/data/matrix/hadamard.lean  src/data/matrix/notation.lean   src/data/matrix/rank.lean

[Daniel Packer]

Thank you! This is exactly what I'm looking for

[Daniel Packer]

@Johan Commelin What is the difference between src/data/matrix and src/linear_algebra/matrix ? I can only find trace in the latter. Is there a relationship between these two folders?

[Riccardo Brasca]

Usually in data we put more basic stuff (like general definitions), but the corresponding theorems go in the appropriate folder.

[Daniel Packer]

So if I wanted to prove additional things in a new file, I would need to import both (one to have definitions to work with and the other for the theorems that I need)?

[Anne Baanen]

Imports are transitive, so if the file A.lean imports B.lean, you only need to import A.lean to get access to everything in both files.

[Riccardo Brasca]

@Daniel Packer Yes, just create a new file and import whatever you need. If you are new to Lean don't try at the beginning to follow to closely the mathlib style, just prove the result you want. You will discover that you need a lot of small missing lemmas (unless you are very lucky!): just prove them as separate results (I mean, not inside the main proof).

[Daniel Packer]

Thanks all for the advice! I'll be sure to follow up if I have more questions

[Daniel Packer]

I'm trying to just mess with some basic statements. So far, I haven't been able to get matrix.trace to work for a specific matrix (even without proving it--it doesn't think the first line type-checks):

example {a b c d : ℝ}: matrix.trace ![![a, b] , ![c, d]] = a + d :=
begin
  sorry
end

This works in the example file for determinants, though:

example {a b c d : ℝ}: matrix.det ![![a, b] , ![c, d]] = a * d - b * c :=
begin
  simp [matrix.det_succ_row_zero, fin.sum_univ_succ],
  ring,
end

Is there a difference between the implementations for these two that's relevant?

[Ruben Van de Velde]

What are your imports?

[Ruben Van de Velde]

Maybe

import linear_algebra.matrix.trace
import data.real.basic

example {a b c d : ℝ}: matrix.trace (fin 2) ℝ ℝ ![![a, b] , ![c, d]] = a + d :=
begin
  sorry
end

[Ruben Van de Velde]

You can use matrix.trace_fin_two

[Reid Barton]

Is the explicitness of those arguments of matrix.trace intentional?

[Anne Baanen]

Wouldn't surprise me if that's a remnant from back when bundled morphisms weren't inferred as nicely. (src#matrix.trace, for the lazy like me)

[Anne Baanen]

Apparently it was commit #1883 by @Oliver Nash, almost exactly 2 years ago.

[Anne Baanen]

Likewise, most of the finsupp definitions should probably become a lot more implicit.

[Reid Barton]

Oh yes that was quite annoying in category theory also.

[Eric Wieser]

You might be interested in https://github.com/eric-wieser/lean-matrix-cookbook, which was a brief attempt to formalize a pdf that someone pointed me at

[Eric Wieser]

Daniel Packer said:

I'm trying to just mess with some basic statements. So far, I haven't been able to get matrix.trace to work for a specific matrix (even without proving it--it doesn't think the first line type-checks):

example {a b c d : ℝ}: matrix.trace ![![a, b] , ![c, d]] = a + d :=
_

...

example {a b c d : ℝ}: matrix.det ![![a, b] , ![c, d]] = a * d - b * c :=
_

These are docs#matrix.trace_fin_two and docs#matrix.det_fin_two !

[Daniel Packer]

Eric Wieser said:

You might be interested in https://github.com/eric-wieser/lean-matrix-cookbook, which was a brief attempt to formalize a pdf that someone pointed me at

Oh, I love the matrix cookbook! That's a pretty chunky collection of results, too. I will give it a look!

[Eric Wieser]

I got most of the way through the first section, and found that one of the results was wrong, and a bunch of the other ones were missing from mathlib. I'm afraid I picked up most of that low hanging fruit already!

I then made a start on the derivatives section, but I'm pretty sure than when the cookbook writes something like ∂(XY) = (∂X)Y + X(∂Y) the correct interpretation is ∂ : derivation _ _ _ (docs#derivation) not docs#deriv. Unfortunately the former doesn't work in a noncommutative setting though.

[Daniel Packer]

Following up on the matrix cookbook thing (let me know if this is the sort of thing that should be a new thread): I haven't been able to find any references to eigenvalues in the mathlib for matrices. Is that theory developed somewhere?

Also, I forked the lean-matrix-cookbook project, and a couple of the lemma references seem to be missing now (e.g. matrix.transpose_list_prod).

[Heather Macbeth]

@Daniel Packer What sorts of results are you after in particular? In mathlib at the moment, eigenvalues are defined for endomorphisms, so you would need to convert the matrix to an endomorphism using docs#matrix.to_lin' and then study the eigenvalues of that.

[Heather Macbeth]

But of course, you might find that the result you want is more elegantly expressed without choosing a basis, in which case why ever state a matrix version? :)

[Eric Wieser]

docs#matrix.transpose_list_prod is alive and well, it sounds like you are somehow on an older mathlib than the one the repo specifies

[Daniel Packer]

Ah, thanks. I'm looking for results like trace (interpreted as sum of diagonal entries of a matrix) is the sum of the eigenvalues of the matrix. Although, it looks like there is a proof that the sum of diagonal entries of a matrix is the general trace is there (so presumably if I dig enough I can find the proof that the trace is the sum of the eigenvalues).

I probably am using an older version of mathlib! Thanks!

[Heather Macbeth]

@Daniel Packer I think this is missing, actually. Feel free to start a conversation on #maths about it. In general, I think we have very little on eigenvalue multiplicities, which is a prerequisite to make that statement work. You can talk about them indirectly as the dimensions of docs#module.End.eigenspace and docs#module.End.generalized_eigenspace. But if I'm thinking about this correctly, to get that the dimensions of the generalized eigenspaces sum to the dimension of the vector space, you need the mutual independence, which seems to be missing (we have only the weaker fact docs#module.End.eigenspaces_independent). I don't think we have Jordan normal form either.

By the way, this is certainly one of those facts that is worth talking about for endomorphisms rather than matrices :)

[Heather Macbeth]

Note that Isabelle and Coq have versions of Jordan normal form:
https://www.isa-afp.org/entries/Jordan_Normal_Form.html
https://cordis.europa.eu/docs/projects/cnect/7/243847/080/deliverables/001-del43.pdf
so if you are very impatient you can always try to make it work there!

[Daniel Packer]

Oh nice! I would be excited to work toward JNF... a lot of this work on my end is also an excuse to get better at working in Lean, so I'm not in any rush. I'm also happy to do the work with endomorphisms.

That said, one of the goals I have is to show continuous dependence of singular values on the entries of a matrix, which is ultimately a matrix thing (though I suppose it isn't too hard to understand continuous dependence of endomorphisms on the entries of defining matrices as long as the domain has a topology). I'll try to do as much as I can with endomorphisms, though

[Kevin Buzzard]

I think that perhaps one reason we've not got JNF is that it's a consequence of the structure theorem for fg modules over a PID which there was some momentum towards recently

[Heather Macbeth]

Oh, that's right, I half-remember such a discussion. Do you know who it was who was working on this?

[Kevin Buzzard]

I don't, all I remember is that we have one of fg torsion-free is free and fg torsion = product of cyclic modules, and not the other

[Heather Macbeth]

OK, so @Daniel Packer, I think your contributions here would be very welcome, but before you get too deep, please start a discussion on the more widely read channel #maths to co-ordinate! :)

[Daniel Packer]

Great! That sounds awesome! I'm not sure I know Lean well enough to be fully contributing yet... I still feel like I'm learning a lot of the style, but I will start a thread on #maths tomorrow about this!

[Karl Palmskog]

Jordan normal form for Coq now lives here: https://github.com/coq-community/coqeal/blob/d9b80c96580cfd480a51cecc0d71242d074c09e4/theory/jordan.v#L191

As seen here, there are many results on matrices and matrix normal forms in MathComp and CoqEAL:https://github.com/coq-community/coqeal/tree/f837e550fa5bd8cca59d2e55eba422c97553d74c#theory

[Daniel Packer]

Karl, thanks for the references on Coq. How plausible do you think it is to port the results over to Lean?

[Kevin Buzzard]

As has already been mentioned, it's not immediately clear that this approach would be the right thing to do. mathlib tends to have an emphasis on the more abstract approach, so using things like structure theorem for modules over a PID to do JNF, and working with endomorphisms rather than matrices wherever possible.

[Karl Palmskog]

@Daniel Packer in general, just porting plain inductive types and theorem statements between Coq and Lean is feasible (I regularly translate between HOL4 and Coq in this way). But the matrix theory in MathComp is constructed using canonical structures and small-scale reflection, which are particular to Coq. So while you can take inspiration from MathComp (e.g., here), it's not straightforward to convert to Lean+Mathlib, which uses type classes and doesn't do much computation/refl/small-scale reflection.

[Karl Palmskog]

I'd recommend taking a look at some papers about the Coq formalizations though (e.g., this or this)

[Karl Palmskog]

I can't speak for MathComp devs, but my view, and what I believe is the general view about mathematics in MathComp is that it's not less abstract than in Mathlib. The use of computations in proofs in MathComp (small-scale reflection) is mainly for reasons of proof engineering productivity, not because we are all fans of constructive mathematics. Small-scale reflection tends to result in fewer rewrite calls, smaller proof terms, shorter proof scripts.

[Karl Palmskog]

the emphasis in MathComp on small-scale reflection in proofs affects the formulations of definitions and theorem statements. For example, if one has a decidable concept, e.g., acyclicity in graphs to take a recent example, it's often considered convenient to work with a boolean decision procedure as the definition of that concept. Not because decidability is amazing in itself, but because it's more convenient in rewriting-based proofs.