7.1 John’s ellipsoid and the projection theorems
The sharp constant \(\sqrt{n}\) in both classical projection theorems (Theorems 7.3 and 7.4) rests on John’s ellipsoid theorem [ 3 ] , which is absent from Mathlib. It is developed in John.lean over \(\mathbb {K} \in \{ \mathbb {R}, \mathbb {C}\} \) at once, modelling an inscribed ellipsoid as the image \(T(B_2)\) of the Euclidean unit ball under a linear map and maximising its volume \(|\det T|\). Here a body seminorm on \(\mathbb {K}^k\) is a continuous seminorm \(p\), thought of as the gauge of a convex body; the hypothesis that it is equivalent to the Euclidean norm means \(c\, \| x\| \le p(x) \le C\, \| x\| \) for constants \(0 {\lt} c \le C\). The general-purpose ingredients of the analytic core (closedness of convex hulls of compact sets in finite dimension, the supporting-vector form of Hahn–Banach dominated by a seminorm, trace duality, and a Weierstrass-type product bound) are collected separately, as candidates for Mathlib.
For a body seminorm \(p\) on \(\mathbb {K}^k\) equivalent to the Euclidean norm, among the feasible operators (those \(T\) with \(p(Tu) \le \| u\| \) for all \(u\)) there is one, \(T_0\), of maximal \(|\det |\), and it is invertible (\(\det T_0 \ne 0\)).
The feasible set is closed (each \(T \mapsto p(Tu)\) is continuous) and bounded (the lower norm bound forces \(\| T\| \le 1/c\)), hence compact; \(|\det |\) is continuous, so it attains a maximum. A small multiple of the identity is feasible and has nonzero determinant, so the maximiser does too.
In John position — the identity is a maximal-volume feasible operator for the body seminorm \(q\) — the identity is a positive combination of the rank-one projections onto contact points:
where a contact point is a unit vector \(u\) with \(\operatorname {Re}\langle x, u\rangle \le q(x)\) for all \(x\).
The classical core of John’s theorem, from first-order optimality of the maximal-volume ellipsoid. If \(k^{-1}\mathrm{id}\) lay outside the convex hull of the contact rank-ones — a compact convex set of operators, whose compactness uses that convex hulls of compact sets are compact in finite dimension — then geometric Hahn–Banach separation, followed by trace duality, would produce a self-adjoint trace-zero direction \(H\) with \(\operatorname {Re}\langle u, Hu\rangle {\lt} 0\) at every contact point. The perturbation \((1-\rho )^{-1}(\mathrm{id} + tH)\) then stays feasible for small \(t{\gt}0\) (the feasibility slack grows linearly in \(t\), using that every touching point is a contact point via a seminorm-dominated Hahn–Banach argument), while its determinant loses only \(O(t^2)\) because \(\operatorname {tr} H = 0\); so \(|\det | {\gt} 1\), contradicting maximality. Hence \(k^{-1}\mathrm{id}\) lies in the hull, and Carathéodory yields the finite combination.
Let \(Y\) be a normed \(\mathbb {K}\)-space and \(V \subseteq Y\) a subspace of dimension \(\le n\). Then there is a bounded projection \(P : Y \to Y\) (\(P \circ P = P\)) with \(\operatorname {range} P = V\) and \(\| P\| \le \sqrt{n}\).
A classical result [ 4 ] , see also [ 8 , 1.5.5 ] . Put \(V\) in John position via the maximal-volume ellipsoid (Theorem 7.1): the decomposition of identity (Theorem 7.2) gives contact points \(u_i\), unit vectors \(v_i = M u_i \in V\), and functionals \(\varphi _i = \langle u_i, M^{-1}\cdot \rangle \) of norm \(\le 1\), which Hahn–Banach extends to \(g_i \in Y^*\) without increasing the norm. Then \(P = \sum _i c_i\, g_i \otimes v_i\) is the identity on \(V\), hence a projection onto \(V\), and weighted Cauchy–Schwarz with \(\sum _i c_i = \dim V\) gives \(\| P\| \le \sqrt{\dim V} \le \sqrt{n}\).
Let \(X\) be a normed \(\mathbb {K}\)-space and \(M \subseteq X\) a closed subspace of codimension \(\le n\). Then for every \(\varepsilon {\gt} 0\) there is a bounded projection \(P : X \to X\) (\(P \circ P = P\)) with \(\ker P = M\) and \(\| P\| \le \sqrt{n} + \varepsilon \).
The dual of Kadets–Snobar (Theorem 7.3) [ 2 ] , see also [ 8 , 1.7.17 ] . Run the John development (Theorems 7.1 and 7.2) on the finite-dimensional dual \((X/M)^*\): the contact points are represented by vectors \(w_i \in X/M\) with \(\| w_i\| \le 1\) (obtained by solving the single-dual equation \(\Phi ^{\mathrm{flip}} w_i = \operatorname {toDual} u_i\), avoiding the topological double dual), each lifted to \(x_i \in X\) with \(\| x_i\| {\lt} 1 + \varepsilon '\) (the quotient norm is an infimum — the sole source of \(\varepsilon \)). Then \(P y = \sum _i c_i\, (\Phi u_i)(\pi y)\, x_i\) has kernel \(M\) and \(\| P\| \le \sqrt{\operatorname {codim} M} + \varepsilon \le \sqrt{n} + \varepsilon \). The exact bound \(\sqrt{n}\) (removing \(\varepsilon \)) needs a weak-\(*\) limit argument; it is not needed here, since the applications recover the sharp constant by letting \(\varepsilon \to 0\).