The Kadets–Snobar projection theorem #
Every finite-dimensional subspace of a Banach space is the range of a bounded projection whose norm is at most the square root of its dimension. This is a classical fact of Banach-space geometry (Kadets–Snobar 1971; Pietsch, Eigenvalues and s-numbers 1.5.5).
The theorem is reduced to the John's-ellipsoid development in BasicResults.John:
John.exists_projection supplies the projection with ‖P‖ ≤ √(dim V), and we
weaken dim V to n; the underlying input is John.john_decomposition, the
John decomposition of identity.
theorem
SNumbers.exists_projection_range_eq_of_rank_le
{𝕜 : Type u}
[RCLike 𝕜]
{Y : Type u}
[NormedAddCommGroup Y]
[NormedSpace 𝕜 Y]
{V : Submodule 𝕜 Y}
{n : ℕ}
(hV_rank : Module.rank 𝕜 ↥V ≤ ↑n)
:
Kadets–Snobar theorem. Every finite-dimensional subspace V of a Banach
space Y of dimension at most n is the range of a bounded projection
P : Y →L[𝕜] Y (P ∘ P = P) with operator norm ‖P‖ ≤ √n.