Lemma. A finite real self-adjoint spectral decomposition [fdip-002R]

Let \((E,h)\) be a real inner-product space of dimension \(n\geq 0\), and let \(T:E\to E\) be linear and self-adjoint. There is an orthonormal basis \(u_1,\ldots ,u_n\) with real eigenvalues \(q_i\). Put \(P_ix=h(u_i,x)u_i\). Then \[\begin {aligned} I&=\sum _iP_i,&T&=\sum _iq_iP_i,\\ P_iP_j&=\delta _{ij}P_i,&\det T&=\prod _iq_i. \end {aligned}\] Moreover \(h(x,Tx)>0\) for every nonzero \(x\) exactly when every \(q_i>0\). In that case \(T^{-1}=\sum _iq_i^{-1}P_i\) is self-adjoint and positive.

This gives the operator proof of the real symmetric decomposition in [boyd2004convex, Appendix A.5.2, pp. 646-647]. Mathlib's LinearMap.IsSymmetric.eigenvectorBasis supplies an orthonormal eigenbasis for a finite-dimensional inner-product space; here its scalar field is specialized to \(\mathbb R\). The declaration alone asserts neither Gaussian normalization nor a graph spectrum.