5 Basic auxiliary results
The companion library BasicResults collects general functional-analysis results that Mathlib lacks: Auerbach’s lemma (this chapter), the singular value decomposition of compact operators (Chapter 6), determinant identities and the bordered-determinant formula, John’s ellipsoid with the Kadets–Snobar and Garling–Gordon projection theorems (Section 7.1), the little Grothendieck bounds (Section 8.3.1), and the spectral projection underlying the Hilbert-space uniqueness theorem.
Every finite-dimensional normed space over \(\mathbb {R}\) admits a basis \((e_i)\) with \(\| e_i\| = 1\) whose dual coordinate functionals also satisfy \(\| e_i^*\| = 1\).
The strategy maximises \(|\det |\) on a product of unit balls, then reads off the basis and dual functionals from the maximiser.