1 Bilinear forms and their profiles
All matrices are real. Matrix norms are Frobenius norms. The Lean development uses their squares to avoid unnecessary square roots.
For \(L\in M_N(\mathbb {R})\), put
\[ S=\tfrac 12(L+L^T),\qquad T=\tfrac 12(L-L^T),\qquad \lVert L\rVert ^2=\operatorname {tr}(L^TL). \]
Then \(L=S+T\), with \(S\) symmetric and \(T\) antisymmetric.
For \(L\ne 0\), let \(\alpha \) and \(\beta \) be the decreasing lists of positive eigenvalues of \(S\) and absolute values of its negative eigenvalues, padded with zeros to equal length. Define \(\pi (L)=(a,b,c,d)\) by
\[ a=\frac{\lVert T\rVert ^2}{\lVert L\rVert ^2},\qquad b=\frac{2\langle \alpha ,\beta \rangle }{\lVert L\rVert ^2},\qquad c=\frac{\lVert (\alpha -\beta )_+\rVert ^2}{\lVert L\rVert ^2},\qquad d=\frac{\lVert (\alpha -\beta )_-\rVert ^2}{\lVert L\rVert ^2}. \]
Positive and negative parts are taken entrywise. Lean pads both lists to length \(N\) and includes the denominator in each definition.