Bilinear and quadratic forms
Bilinear and quadratic forms on vector spaces and modules: rank, orthogonal sums, inertia and congruence, and lattices with their duals and neighbours.
- Dual lattices
- Kneser p-neighbors
- Orthogonal product of bilinear forms
- Rank of a bilinear form
- Simultaneous diagonalization by congruence
- Systems of quadratic forms
TheoremSylvester's law of inertia#✓fully proved
Let \(A\) and \(B\) be real symmetric square matrices with rows and columns indexed by a finite set \(n\), and suppose \(B = P^{\mathsf T} A P\) for some invertible real matrix \(P\) indexed by \(n\). Then \(A\) and \(B\) have the same number of positive eigenvalues, the same number of negative eigenvalues and the same number of zero eigenvalues, each counted with multiplicity.
Proof: By the spectral theorem, the quadratic form of each matrix is a weighted sum of squares whose weights are its eigenvalues. Congruence gives an equivalence of quadratic forms, and invariance of the signature fixes the positive and negative counts; the zero count follows by trichotomy.
theorem sylvester_law_of_inertia {n : Type*} [Fintype n] [DecidableEq n]
{A B : Matrix n n ℝ} (hA : A.IsHermitian) (hB : B.IsHermitian)
(P : Matrix n n ℝ) (hP : IsUnit P.det)
(hcong : B = P.transpose * A * P) :
(Finset.univ.filter (fun i => 0 < hA.eigenvalues i)).card =
(Finset.univ.filter (fun i => 0 < hB.eigenvalues i)).card ∧
(Finset.univ.filter (fun i => hA.eigenvalues i < 0)).card =
(Finset.univ.filter (fun i => hB.eigenvalues i < 0)).card ∧
(Finset.univ.filter (fun i => hA.eigenvalues i = 0)).card =
(Finset.univ.filter (fun i => hB.eigenvalues i = 0)).cardSources
- J. J. Sylvester, A demonstration of the theorem that every homogeneous quadratic polynomial is reducible by real orthogonal substitutions to the form of a sum of positive and negative squares, Philosophical Magazine Ser. 4, 4(23) (1852), 138-142.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.