John's ellipsoid — the maximal-volume position

This is the first step towards the Kadets–Snobar and Garling–Gordon projection theorems (BasicResults/KadetsSnobar.lean, BasicResults/GarlingGordon.lean), whose sharp ‖P‖ ≤ √n bounds rest on John's ellipsoid theorem (absent from Mathlib). Everything is done over an arbitrary RCLike field 𝕜 (so both the real and complex cases are covered at once).

We model an ellipsoid inside a symmetric convex body as the image T (B₂) of the Euclidean unit ball under a continuous linear map T : 𝕜^k →L 𝕜^k; its volume is proportional to ‖det T‖. The body is described by a norm, given here as a Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k)) p that is equivalent to the Euclidean norm (c‖x‖ ≤ p x ≤ C‖x‖, c > 0). The ellipsoid T (B₂) lies in the body {p ≤ 1} exactly when T is feasible: p (T u) ≤ ‖u‖ for all u.

Main results

• John.exists_maxVolume — among the feasible operators there is one, T₀, of maximal ‖det‖; it is invertible (det ≠ 0). This is the maximal-volume inscribed ellipsoid.
• John.exists_johnPosition — the John position along any continuous linear equivalence L : 𝕜^k ≃L W: an equivalence M and a body seminorm q with q u ≤ ‖u‖, ‖det S‖ ≤ 1 for every feasible S, and ‖M z‖ = q z. The common core of both projection theorems below.
• John.john_decomposition — the decomposition of identity in John position, ∑ᵢ cᵢ uᵢ⊗uᵢ = id over contact points with ∑ᵢ cᵢ = dim. By the classical variational argument: Hahn–Banach separation of k⁻¹ • id from the compact convex hull of the contact projections, trace duality to produce a self-adjoint trace-zero improving direction, the first-order perturbation (1-ρ)⁻¹ • (id + tH) to contradict maximality, and Carathéodory to extract the finite combination. The general-purpose ingredients (compactness of convex hulls, seminorm Hahn–Banach, trace duality, the product bound ∏(1+aᵢ) ≥ 1-2∑aᵢ²) live in BasicResults/JohnAux.lean.
• John.exists_projection — Kadets–Snobar: every finite-dimensional subspace of a normed 𝕜-space is the range of a projection P with ‖P‖ ≤ √(dim). Its analytic core is the weighted Cauchy–Schwarz bound John.norm_sum_weight_smul_le.
• John.exists_projection_ker — Garling–Gordon (ε-form), dual to Kadets–Snobar: every closed subspace M with finite-dimensional quotient is the kernel of a projection P with ‖P‖ ≤ √(codim M) + ε, for every ε > 0. Built on the dual (X ⧸ M)*, representing contact points via Φ.flip (avoiding the topological double dual).

def John.Feasible {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (p : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))) : Set (EuclideanSpace 𝕜 (Fin k) →L[𝕜] EuclideanSpace 𝕜 (Fin k))

An operator T : 𝕜^k →L 𝕜^k is feasible for the body seminorm p when the image T (B₂) of the Euclidean unit ball lies in {p ≤ 1}, i.e. p (T u) ≤ ‖u‖ for every u.

Equations

• John.Feasible p = {T : EuclideanSpace 𝕜 (Fin k) →L[𝕜] EuclideanSpace 𝕜 (Fin k) | ∀ (u : EuclideanSpace 𝕜 (Fin k)), p (T u) ≤ ‖u‖}

theorem John.isClosed_feasible {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (p : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))) (hp : Continuous ⇑p) : IsClosed (Feasible p)

The feasible set is closed: for each u, T ↦ p (T u) is continuous.

theorem John.feasible_subset_closedBall {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (p : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))) {c : ℝ} (hc : 0 < c) (hlo : ∀ (x : EuclideanSpace 𝕜 (Fin k)), c * ‖x‖ ≤ p x) : Feasible p ⊆ Metric.closedBall 0 (1 / c)

The feasible set is bounded: c‖x‖ ≤ p x forces ‖T‖ ≤ 1/c.

theorem John.exists_maxVolume {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (p : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))) (hp : Continuous ⇑p) {c : ℝ} (hc : 0 < c) (hlo : ∀ (x : EuclideanSpace 𝕜 (Fin k)), c * ‖x‖ ≤ p x) {C : ℝ} (hup : ∀ (x : EuclideanSpace 𝕜 (Fin k)), p x ≤ C * ‖x‖) : ∃ T ∈ Feasible p, T.det ≠ 0 ∧ ∀ S ∈ Feasible p, ‖S.det‖ ≤ ‖T.det‖

Maximal-volume inscribed ellipsoid. For a body seminorm p equivalent to the Euclidean norm (c‖x‖ ≤ p x ≤ C‖x‖, c > 0), among the feasible operators there is one of maximal ‖det‖, and it is invertible.

theorem John.exists_johnPosition {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} {W : Type u} [NormedAddCommGroup W] [NormedSpace 𝕜 W] (hk : 0 < k) (L : EuclideanSpace 𝕜 (Fin k) ≃L[𝕜] W) : ∃ (M : EuclideanSpace 𝕜 (Fin k) ≃L[𝕜] W) (q : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))), Continuous ⇑q ∧ (∀ (u : EuclideanSpace 𝕜 (Fin k)), q u ≤ ‖u‖) ∧ (∀ S ∈ Feasible q, ‖S.det‖ ≤ 1) ∧ ∀ (z : EuclideanSpace 𝕜 (Fin k)), ‖M z‖ = q z

John position along an equivalence. Given a continuous linear equivalence L : 𝕜^k ≃L W onto a normed space W (with 0 < k), there are an equivalence M : 𝕜^k ≃L W and a body seminorm q in John position: q is continuous, the identity is feasible for q (q u ≤ ‖u‖), every feasible operator has ‖det‖ ≤ 1, and q is the pullback of the norm of W along M (‖M z‖ = q z).

Mathematically: pull the norm of W back to a body seminorm p = ‖L ·‖ on 𝕜^k (equivalent to the Euclidean norm since L is an equivalence and k > 0), take a maximal-volume feasible operator T₀ (exists_maxVolume), and set q = p ∘ T₀, M = L ∘ T₀. This is the common core of the Kadets–Snobar and Garling–Gordon projection theorems below.

def John.Contact {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (q : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))) : Set (EuclideanSpace 𝕜 (Fin k))

The contact set of a body seminorm q: unit vectors u whose associated linear functional x ↦ re ⟪x, u⟫ is dominated by q. These are the points where the Euclidean unit sphere touches the boundary {q = 1} with a shared supporting hyperplane; the John decomposition of identity is supported on this set.

Equations

• John.Contact q = {u : EuclideanSpace 𝕜 (Fin k) | ‖u‖ = 1 ∧ ∀ (x : EuclideanSpace 𝕜 (Fin k)), RCLike.re (inner 𝕜 x u) ≤ q x}

theorem John.isCompact_contact {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (q : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))) : IsCompact (Contact q)

The contact set is compact: it is a closed subset of the (compact) unit sphere.

noncomputable def John.rankOneSA {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (u : EuclideanSpace 𝕜 (Fin k)) : EuclideanSpace 𝕜 (Fin k) →L[𝕜] EuclideanSpace 𝕜 (Fin k)

The self-adjoint rank-one operator u ⊗ u : x ↦ ⟪u, x⟫ • u. The John decomposition of identity expresses id as a positive combination of these over contact points.

Equations

• John.rankOneSA u = ((innerSL 𝕜) u).smulRight u

@[simp]

theorem John.rankOneSA_apply {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (u x : EuclideanSpace 𝕜 (Fin k)) : (rankOneSA u) x = inner 𝕜 u x • u

theorem John.norm_inner_le_of_contact {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} {q : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))} {u : EuclideanSpace 𝕜 (Fin k)} (hu : u ∈ Contact q) (x : EuclideanSpace 𝕜 (Fin k)) : ‖inner 𝕜 x u‖ ≤ q x

Contact support. A contact point u has ‖⟪x, u⟫‖ ≤ q x for all x: choosing a unit phase a with re ⟪a • x, u⟫ = ‖⟪x, u⟫‖, the contact bound and 𝕜-homogeneity of q give the claim.

theorem John.sum_weight_inner_sq {𝕜 : Type u} [RCLike 𝕜] {k N : ℕ} (c : Fin N → ℝ) (u : Fin N → EuclideanSpace 𝕜 (Fin k)) (hdec : ∀ (x : EuclideanSpace 𝕜 (Fin k)), ∑ i : Fin N, (↑(c i) * inner 𝕜 (u i) x) • u i = x) (z : EuclideanSpace 𝕜 (Fin k)) : ∑ i : Fin N, c i * ‖inner 𝕜 (u i) z‖ ^ 2 = ‖z‖ ^ 2

Quadratic form of a decomposition of identity. If ∑ᵢ ((cᵢ:𝕜) · ⟪uᵢ, x⟫) • uᵢ = x for all x, then ∑ᵢ cᵢ · ‖⟪uᵢ, z⟫‖² = ‖z‖².

theorem John.sum_weight_mul_le_sqrt {N : ℕ} (c : Fin N → ℝ) (hc : ∀ (i : Fin N), 0 ≤ c i) (t : Fin N → ℝ) : ∑ i : Fin N, c i * t i ≤ √(∑ i : Fin N, c i) * √(∑ i : Fin N, c i * t i ^ 2)

Weighted Cauchy–Schwarz. For nonnegative weights cᵢ, ∑ᵢ cᵢ tᵢ ≤ √(∑ᵢ cᵢ) · √(∑ᵢ cᵢ tᵢ²).

Cauchy–Schwarz applied to the vectors (√cᵢ) and (√cᵢ · tᵢ). Paired with a decomposition of identity (where ∑ᵢ cᵢ is the dimension) this is what turns a quadratic bound into the linear bound needed for a projection norm.

Ingredients for the John decomposition of identity

The proof of john_decomposition below is the classical variational argument (F. John; K. Ball, An elementary introduction to modern convex geometry):

1. mem_contact_of_apply_eq_one — every unit vector where the body touches the Euclidean sphere is a contact point (Hahn–Banach for the seminorm q).
2. exists_selfAdjoint_of_not_mem_convexHull — if k⁻¹ • id did not lie in the convex hull of the contact projections uᵢ ⊗ uᵢ, geometric Hahn–Banach separation plus trace duality would produce a self-adjoint, trace-zero H with re ⟪u, H u⟫ ≤ -δ < 0 at every contact point.
3. no_neg_direction_of_maxVolume — no such H exists: for small t > 0 the operator (1 - ρ)⁻¹ • (id + t H) would be feasible with ‖det‖ > 1, because the feasibility slack grows linearly in t while (trace being zero) the determinant only loses O(t²) — contradicting the John-position maximality. Its four ingredients are the compactness gap exists_gap_of_lt_one_on_compact, the norm estimate norm_add_smul_le_of_inner_le, the rescaling step smul_mem_feasible_of_le_on_sphere, and the determinant bound one_sub_le_norm_det_one_add_smul.
4. Carathéodory (mem_convexHull_iff_exists_fintype) turns hull membership into the finite positive combination.

theorem John.mem_contact_of_apply_eq_one {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} {q : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))} (hq1 : ∀ (x : EuclideanSpace 𝕜 (Fin k)), q x ≤ ‖x‖) {u : EuclideanSpace 𝕜 (Fin k)} (hu : ‖u‖ = 1) (hqu : q u = 1) : u ∈ Contact q

Every touching point is a contact point. If q ≤ ‖·‖ and u is a unit vector with q u = 1, then u ∈ Contact q. The supporting functional of {q ≤ 1} at u produced by seminorm-Hahn–Banach (Seminorm.exists_inner_le_of_apply) is represented by a vector v with re ⟪u, v⟫ = 1 and ‖v‖ ≤ 1; equality in Cauchy–Schwarz forces v = u, so u itself supports the body.

theorem John.continuous_rankOneSA {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} : Continuous fun (u : EuclideanSpace 𝕜 (Fin k)) => rankOneSA u

The map u ↦ u ⊗ u sending a vector to its rank-one projection is continuous.

theorem John.trace_rankOneSA_comp {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (u : EuclideanSpace 𝕜 (Fin k)) (G : EuclideanSpace 𝕜 (Fin k) →L[𝕜] EuclideanSpace 𝕜 (Fin k)) : (LinearMap.trace 𝕜 (EuclideanSpace 𝕜 (Fin k))) (↑(rankOneSA u) ∘ₗ ↑G) = inner 𝕜 u (G u)

The trace of (u ⊗ u) ∘ G is the quadratic-form value ⟪u, G u⟫.

theorem John.exists_selfAdjoint_of_not_mem_convexHull {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (hk : 0 < k) {q : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))} (hmem : (↑k)⁻¹ • ContinuousLinearMap.id 𝕜 (EuclideanSpace 𝕜 (Fin k)) ∉ (convexHull ℝ) (rankOneSA '' Contact q)) : ∃ (H : EuclideanSpace 𝕜 (Fin k) →L[𝕜] EuclideanSpace 𝕜 (Fin k)) (δ : ℝ), 0 < δ ∧ IsSelfAdjoint H ∧ (LinearMap.trace 𝕜 (EuclideanSpace 𝕜 (Fin k))) ↑H = 0 ∧ ∀ u ∈ Contact q, RCLike.re (inner 𝕜 u (H u)) ≤ -δ

The separation step of John's theorem. If, in John position, k⁻¹ • id is not a convex combination of contact projections u ⊗ u, then some self-adjoint trace-zero direction H improves all contact points at once: re ⟪u, H u⟫ ≤ -δ < 0 on Contact q.

Proof: the contact set is compact, so the set of its rank-one projections is compact and (in finite dimensions) its convex hull is compact, hence closed; geometric Hahn–Banach (RCLike.geometric_hahn_banach_closed_point) separates k⁻¹ • id from it. Trace duality (ContinuousLinearMap.exists_trace_repr) writes the separating functional as A ↦ tr (A ∘ G); on rank-one projections this evaluates to re ⟪u, G u⟫ (trace_rankOneSA_comp). Passing to the self-adjoint part of G and subtracting the right multiple of the identity makes the trace zero without changing the inequality.

theorem John.exists_gap_of_lt_one_on_compact {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} {q : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))} (hqc : Continuous ⇑q) {C : Set (EuclideanSpace 𝕜 (Fin k))} (hC : IsCompact C) (hlt : ∀ u ∈ C, q u < 1) : ∃ (η : ℝ), 0 < η ∧ η ≤ 1 ∧ ∀ u ∈ C, q u ≤ 1 - η

Uniform gap on a compact set. If a continuous seminorm satisfies q < 1 on a compact set C, it stays below 1 - η on C for a uniform 0 < η ≤ 1 (extreme value theorem; η ≤ 1 because q ≥ 0).

theorem John.smul_mem_feasible_of_le_on_sphere {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} {q : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))} {T : EuclideanSpace 𝕜 (Fin k) →L[𝕜] EuclideanSpace 𝕜 (Fin k)} {s : ℝ} (hs : 0 < s) (hT : ∀ (u : EuclideanSpace 𝕜 (Fin k)), ‖u‖ = 1 → q (T u) ≤ s) : ↑s⁻¹ • T ∈ Feasible q

Rescaling to feasibility. If q (T u) ≤ s for every unit vector u (with s > 0), then s⁻¹ • T is feasible for q: by homogeneity, q (T x) ≤ s ‖x‖ for every x. Part of the John's-ellipsoid perturbation argument.

theorem John.norm_add_smul_le_of_inner_le {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} {H : EuclideanSpace 𝕜 (Fin k) →L[𝕜] EuclideanSpace 𝕜 (Fin k)} {u : EuclideanSpace 𝕜 (Fin k)} (hu : ‖u‖ = 1) {t δ : ℝ} (ht0 : 0 < t) (h1 : t * ‖H‖ ^ 2 ≤ δ / 2) (h2 : t * δ ≤ 4) (hA : RCLike.re (inner 𝕜 u (H u)) ≤ -(δ / 2)) : ‖u + ↑t • H u‖ ≤ 1 - t * δ / 4

Linear norm shrinking near the touching set. If re ⟪u, H u⟫ ≤ -(δ/2) at a unit vector u, then ‖u + t • H u‖ ≤ 1 - tδ/4 for 0 < t with t‖H‖² ≤ δ/2 and tδ ≤ 4: expanding the square, ‖u + tHu‖² ≤ 1 - tδ + t²‖H‖² ≤ 1 - tδ/2 ≤ (1 - tδ/4)². This is the first-order feasibility gain of the John perturbation.

theorem John.one_sub_le_norm_det_one_add_smul {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} {H : EuclideanSpace 𝕜 (Fin k) →L[𝕜] EuclideanSpace 𝕜 (Fin k)} (hHsa : IsSelfAdjoint H) (htr : (LinearMap.trace 𝕜 (EuclideanSpace 𝕜 (Fin k))) ↑H = 0) {t : ℝ} (ht0 : 0 < t) (htH : t * ‖H‖ ≤ 1 / 2) : 1 - 2 * (t ^ 2 * (↑k * ‖H‖ ^ 2)) ≤ ‖(ContinuousLinearMap.id 𝕜 (EuclideanSpace 𝕜 (Fin k)) + ↑t • H).det‖

Second-order determinant bound for a trace-zero perturbation. For a self-adjoint H with tr H = 0 and 0 < t with t‖H‖ ≤ 1/2, ‖det (id + t • H)‖ ≥ 1 - 2t²·(k·‖H‖²).

In an orthonormal eigenbasis (spectral theorem for symmetric operators), det (id + tH) = ∏ᵢ (1 + tλᵢ) with real eigenvalues λᵢ satisfying ∑ᵢ λᵢ = tr H = 0 and |λᵢ| ≤ ‖H‖; the Weierstrass-type bound one_sub_two_mul_sum_sq_le_prod_one_add then gives ∏(1+tλᵢ) ≥ 1 - 2t²∑λᵢ² ≥ 1 - 2t²k‖H‖². The trace-zero hypothesis is what makes the determinant loss second order in t.

theorem John.no_neg_direction_of_maxVolume {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (hk : 0 < k) {q : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))} (hqc : Continuous ⇑q) (hq1 : ∀ (x : EuclideanSpace 𝕜 (Fin k)), q x ≤ ‖x‖) (hmax : ∀ S ∈ Feasible q, ‖S.det‖ ≤ 1) {H : EuclideanSpace 𝕜 (Fin k) →L[𝕜] EuclideanSpace 𝕜 (Fin k)} (hHsa : IsSelfAdjoint H) (htr : (LinearMap.trace 𝕜 (EuclideanSpace 𝕜 (Fin k))) ↑H = 0) {δ : ℝ} (hδ : 0 < δ) (hneg : ∀ (u : EuclideanSpace 𝕜 (Fin k)), ‖u‖ = 1 → q u = 1 → RCLike.re (inner 𝕜 u (H u)) ≤ -δ) : False

First-order optimality in John position. If the identity has maximal ‖det‖ among feasible operators for q (with q ≤ ‖·‖), then no self-adjoint trace-zero H can satisfy re ⟪u, H u⟫ ≤ -δ < 0 at every unit vector u touching the body (q u = 1).

Otherwise S = (1 - ρ)⁻¹ • (id + t H) with ρ = tδ/4 would be feasible for small t > 0: near the touching set the Euclidean norm of (id + t H) u shrinks linearly in t (norm_add_smul_le_of_inner_le — this is where re ⟪u, H u⟫ ≤ -δ enters), and away from it q is uniformly below 1 by compactness (exists_gap_of_lt_one_on_compact), so S is feasible by rescaling (smul_mem_feasible_of_le_on_sphere). Meanwhile the trace-zero determinant bound one_sub_le_norm_det_one_add_smul shows the perturbation loses only O(t²) of determinant — beaten by the first-order gain (1 - ρ)⁻¹ ≥ 1 + tδ/4. So ‖det S‖ > 1, contradicting maximality.

theorem John.john_decomposition {𝕜 : Type u} [RCLike 𝕜] {k : ℕ} (q : Seminorm 𝕜 (EuclideanSpace 𝕜 (Fin k))) (hq : Continuous ⇑q) (hq1 : ∀ (u : EuclideanSpace 𝕜 (Fin k)), q u ≤ ‖u‖) (hmax : ∀ S ∈ Feasible q, ‖S.det‖ ≤ 1) : ∃ (N : ℕ) (u : Fin N → EuclideanSpace 𝕜 (Fin k)) (c : Fin N → ℝ), (∀ (i : Fin N), u i ∈ Contact q) ∧ (∀ (i : Fin N), 0 ≤ c i) ∧ ∑ i : Fin N, c i = ↑k ∧ ∀ (x : EuclideanSpace 𝕜 (Fin k)), ∑ i : Fin N, (↑(c i) * inner 𝕜 (u i) x) • u i = x

John decomposition of identity — the classical core of John's ellipsoid theorem.

In John position — the identity is a maximal-volume feasible operator for the body seminorm q (q u ≤ ‖u‖, and ‖det S‖ ≤ 1 for every feasible S) — the identity is a positive combination of the rank-one projections onto contact points, with weights summing to the dimension k: ∑ᵢ ((cᵢ:𝕜) · ⟪uᵢ, x⟫) • uᵢ = x, with uᵢ ∈ Contact q, cᵢ ≥ 0, ∑ᵢ cᵢ = k.

Proof: k⁻¹ • id lies in the convex hull of {u ⊗ u : u ∈ Contact q} — otherwise exists_selfAdjoint_of_not_mem_convexHull would produce a self-adjoint trace-zero improving direction, which no_neg_direction_of_maxVolume forbids (all unit vectors with q u = 1 are contact points by mem_contact_of_apply_eq_one). Carathéodory (mem_convexHull_iff_exists_fintype) turns hull membership into a finite convex combination ∑ᵢ wᵢ (uᵢ ⊗ uᵢ) = k⁻¹ • id; multiplying by k and evaluating at x gives the decomposition with cᵢ = k wᵢ.

theorem John.norm_sum_weight_smul_le {𝕜 : Type u} [RCLike 𝕜] {k N : ℕ} (c : Fin N → ℝ) (u : Fin N → EuclideanSpace 𝕜 (Fin k)) (hdec : ∀ (x : EuclideanSpace 𝕜 (Fin k)), ∑ i : Fin N, (↑(c i) * inner 𝕜 (u i) x) • u i = x) (hc : ∀ (i : Fin N), 0 ≤ c i) (a : Fin N → 𝕜) : ‖∑ i : Fin N, (↑(c i) * a i) • u i‖ ≤ √(∑ i : Fin N, c i * ‖a i‖ ^ 2)

Weighted Cauchy–Schwarz for a decomposition of identity (the analytic heart of the Kadets–Snobar estimate). If ∑ᵢ ((cᵢ:𝕜)·⟪uᵢ,x⟫)•uᵢ = x and cᵢ ≥ 0, then for any scalars aᵢ, ‖∑ᵢ ((cᵢ:𝕜)·aᵢ)•uᵢ‖ ≤ √(∑ᵢ cᵢ·‖aᵢ‖²).

theorem John.exists_projection {𝕜 : Type u} [RCLike 𝕜] {Y : Type u} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] (V : Submodule 𝕜 Y) [FiniteDimensional 𝕜 ↥V] : ∃ (P : Y →L[𝕜] Y), P ∘SL P = P ∧ (↑P).range = V ∧ ‖P‖ ≤ √↑(Module.finrank 𝕜 ↥V)

Kadets–Snobar. Every finite-dimensional subspace V of a normed 𝕜-space Y is the range of a bounded projection P : Y →L[𝕜] Y with ‖P‖ ≤ √(dim V).

The proof puts V in John position: transport the Euclidean structure of 𝕜^{dim V} to V through the maximal-volume ellipsoid M (built from the John decomposition of identity ∑ᵢ cᵢ uᵢ⊗uᵢ = id). The contact points uᵢ give unit vectors vᵢ = M uᵢ ∈ V and functionals φᵢ = ⟪uᵢ, M⁻¹ ·⟫ ∈ V* of norm ≤ 1, which Hahn–Banach (exists_extension_norm_eq) extends to gᵢ ∈ Y* without increasing the norm. Then P = ∑ᵢ cᵢ · gᵢ ⊗ vᵢ is the identity on V (so it is a projection onto V), and the weighted Cauchy–Schwarz estimate norm_sum_weight_smul_le together with ∑ᵢ cᵢ = dim V yields ‖P‖ ≤ √(dim V).

Ingredients for the dual (Garling–Gordon) projection

exists_projection_ker below runs the Kadets–Snobar argument in the finite-dimensional dual D = (X ⧸ M)*, where the John-position map is a contraction Φ : 𝕜^k ≃L D. Three steps of that argument are independent of the quotient and are recorded here for a W in place of X ⧸ M.

theorem John.exists_projection_ker {𝕜 : Type u} [RCLike 𝕜] {X : Type u} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (M : Submodule 𝕜 X) [IsClosed ↑M] [FiniteDimensional 𝕜 (X ⧸ M)] {ε : ℝ} (hε : 0 < ε) : ∃ (P : X →L[𝕜] X), P ∘SL P = P ∧ (↑P).ker = M ∧ ‖P‖ ≤ √↑(Module.finrank 𝕜 (X ⧸ M)) + ε

Garling–Gordon, ε-form. Every closed subspace M of a normed 𝕜-space X with finite-dimensional quotient is the kernel of a bounded projection P : X →L[𝕜] X with ‖P‖ ≤ √(codim M) + ε, for every ε > 0.

This is the dual of exists_projection, run in the finite-dimensional dual D = (X ⧸ M)* (so no dual of X is needed). John position of the unit ball of D gives contact points uᵢ and weights cᵢ with ∑ᵢ cᵢ = codim M; the uᵢ become unit functionals fᵢ = Φ uᵢ ∈ D on the quotient, and the contact supports become norm-≤ 1 functionals on D, i.e. — since X ⧸ M is finite-dimensional, hence isometrically reflexive (NormedSpace.inclusionInDoubleDualLi) — vectors wᵢ ∈ X ⧸ M with ‖wᵢ‖ ≤ 1. Lifting each wᵢ to a representative xᵢ ∈ X with ‖xᵢ‖ < 1 + ε' (Submodule.Quotient.norm_mk_lt — the quotient norm is an infimum; this is the sole source of the ε), the operator P y = ∑ᵢ cᵢ · fᵢ(π y) · xᵢ satisfies π ∘ P = π (via the decomposition of identity and the Riesz representation on the Euclidean model), hence is a projection with kernel M; Cauchy–Schwarz and the quadratic identity sum_weight_inner_sq give ‖P‖ ≤ (1 + ε')·√(codim M).