QWF result formalized in Lean

@article{BergIlch12a,

title = {The quasi-Weierstraß form for regular matrix pencils},

author = {Thomas Berger and Achim Ilchmann and Stephan Trenn},

url = {http://stephantrenn.net/wp-content/uploads/2017/09/Preprint-BIT091017.pdf, Preprint

http://dx.doi.org/10.1016/S0024-3795(11)00688-4, Corrections (see Paragraph 6 of Note to Editors)

https://github.com/Mrc-Smn/QWF_lean, Lean formalization of the main result (Theorem 2.6)},

doi = {10.1016/j.laa.2009.12.036},

year  = {2012},

date = {2012-01-01},

urldate = {2012-01-01},

journal = {Linear Algebra Appl.},

volume = {436},

number = {10},

pages = {4052--4069},

abstract = {Regular linear matrix pencils A- E d in K^{n x n}[d], where K=Q, R or C, and the associated differential algebraic equation (DAE) E x' = A x are studied. The Wong sequences of subspaces are investigate and invoked to decompose the K^n into V* + W*, where any bases of the linear spaces V* and W* transform the matrix pencil into the Quasi-Weierstraß form. The Quasi-Weierstraß form of the matrix pencil decouples the original DAE into the underlying ODE and the pure DAE or, in other words, decouples the set of initial values into the set of consistent initial values  V* and  ``pure'' inconsistent initial values W* - {0}. Furthermore, V* and  W*  are spanned by the generalized eigenvectors at the finite and infinite eigenvalues, resp. The Quasi-Weierstraß form is used to show how chains of generalized eigenvectors at finite and infinite eigenvalues of A- E d lead to the well-known Weierstraß form. So the latter can be viewed as a generalized Jordan form. Finally, it is shown how eigenvector chains constitute a basis for the solution space of  E x' = A x.},

note = {published online February 2010},

keywords = {},

pubstate = {published},

tppubtype = {article}

}