The Garling–Gordon projection theorem

A closed subspace of a Banach space whose codimension is at most n is the kernel of a bounded projection of norm at most √n + ε, for every ε > 0. This is a classical fact of Banach-space geometry (Garling–Gordon 1971; Pietsch, Eigenvalues and s-numbers 1.7.17). It is the dual of Kadets–Snobar (BasicResults.KadetsSnobar).

The theorem is reduced to the John's-ellipsoid development in BasicResults.John: John.exists_projection_ker supplies, for each ε > 0, a projection with kernel M and ‖P‖ ≤ √(codim M) + ε, and we weaken codim M to n; the underlying input is John.john_decomposition, the John decomposition of identity. The ε is intrinsic to the general Banach setting (the quotient norm is an infimum that need not be attained); the applications in SNumbers.Inequalities recover the sharp constant by letting ε → 0.

theorem SNumbers.exists_projection_ker_eq_of_codim_le {𝕜 : Type u} [RCLike 𝕜] {X : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {M : Submodule 𝕜 X} (hM_closed : IsClosed ↑M) {n : ℕ} (hM_codim : Module.rank 𝕜 (X ⧸ M) ≤ ↑n) {ε : ℝ} (hε : 0 < ε) : ∃ (P : X →L[𝕜] X), P ∘SL P = P ∧ (↑P).ker = M ∧ ‖P‖ ≤ √↑n + ε

Garling–Gordon theorem (ε-form). For a closed subspace M of a normed space X of codimension at most n and every ε > 0, there is a bounded projection P : X →L[𝕜] X (P ∘ P = P) with kernel exactly M and operator norm ‖P‖ ≤ √n + ε.