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, that is, when 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 [ 9 , 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 [ 9 , 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; this is 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\).