KKT identities at the normalized optimum

Proved

ConvexOptimization.lowner_john_unit_ball_kkt

by Shuze Chen · Aug 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convexgeometryconvexoptimizationellipsoids

The optimality (KKT) conditions of the minimum-volume covering ellipsoid problem, written at the normalized optimum where the extremal ellipsoid is the Euclidean unit ball.

Let $x_1,\dots,x_m \in \mathbb{R}^n$ and suppose the pair $(A,b) = (I,0)$ — that is, the closed unit ball $\{v : \lVert v\rVert_2 \le 1\}$ — is the Löwner–John ellipsoid of $\{x_1,\dots,x_m\}$ . Then there exist multipliers $\lambda_1,\dots,\lambda_m \ge 0$ with

\sum_{i=1}^{m} \lambda_i\, x_i x_i^{T} = I, \qquad \sum_{i=1}^{m} \lambda_i\, x_i = 0, \qquad \lambda_i\bigl(1 - x_i^{T}x_i\bigr) = 0 \quad (i = 1,\dots,m), \qquad \sum_{i=1}^{m} \lambda_i = n .

Here $x_i x_i^{T}$ denotes the rank-one outer product, $I$ the $n \times n$ identity, and $n$ the dimension. The first identity is stationarity of the $\log\det$ objective, the second stationarity in the centre variable, the third is complementary slackness — a multiplier may be nonzero only at a contact point, one with $\lVert x_i\rVert_2 = 1$ lying on the boundary sphere — and the last is the trace of the first combined with complementary slackness.

These are exactly John's decomposition of the identity: the contact points, weighted by $\lambda$ , form an isotropic system whose second-moment matrix is the identity and whose barycentre is the origin. Because the Löwner–John ellipsoid is affinely equivariant, every configuration can be brought to this normalized position, so these identities are the general optimality conditions written in the coordinates that make them cleanest. They are the sole input to the $1/n$ rounding step.

Formalization Note The outer product is Mathlib's Matrix.vecMulVec, and $x_i^{T}x_i$ is written with the dot product ⬝ᵥ on Fin n → ℝ; the identity matrix appears as (1 : Matrix (Fin n) (Fin n) ℝ). No full-dimensionality hypothesis is required, since it follows from the unit ball being extremal. Source: Boyd & Vandenberghe §8.4.1, the KKT conditions of problem (8.12) after normalization.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_ellipsoidBody
import Definitions.Def_ConvexOptimization_IsLownerJohn

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.lowner_john_unit_ball_kkt {nn m : ℕ} (x : Fin m → Fin nn → ℝ)
    (hopt : IsLownerJohn (1 : Matrix (Fin nn) (Fin nn) ℝ) 0 (Set.range x)) :
    ∃ lam : Fin m → ℝ, (∀ i, 0 ≤ lam i) ∧
      (∑ i, lam i • Matrix.vecMulVec (x i) (x i)) = (1 : Matrix (Fin nn) (Fin nn) ℝ) ∧
      (∑ i, lam i • x i) = 0 ∧
      (∀ i, lam i * (1 - x i ⬝ᵥ x i) = 0) ∧
      (∑ i, lam i) = (nn : ℝ) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 412, §8.4.1 (the KKT conditions of problem (8.12), written at the normalized optimum where the extremal ellipsoid is the Euclidean unit ball)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Theorem. For all $nn,m\in\mathbb{N}$ and every family of points $x_1,\dots,x_m\in\mathbb{R}^{nn}$ , assume the specific pair $(I,0)$ — identity matrix, zero offset — satisfies the Löwner–John predicate for $\{x_i\}$ ; unfolded, this hypothesis says: (a) $I$ is symmetric and positive definite (true; vacuously for $nn=0$ ), (b) every point lies in the closed Euclidean unit ball, $x_i\cdot x_i\le 1$ , and (c) every symmetric positive-definite $A'$ together with any offset $b'$ whose body $\{v:\lVert A'v+b'\rVert^{2}\le 1\}$ contains all the $x_i$ has $\det A'\le\det I=1$ . The conclusion asserts the existence of multipliers $\lambda:\mathrm{Fin}\,m\to\mathbb{R}$ satisfying all five of: (1) $\lambda_i\ge 0$ for every $i$ ; (2) $\sum_{i}\lambda_i\,x_i x_i^{\mathsf T}=I$ , where $x_i x_i^{\mathsf T}$ is the outer-product matrix (Mathlib's $\mathrm{vecMulVec}$ ; entry $(j,k)$ equals $x_i(j)\,x_i(k)$ ); (3) $\sum_i\lambda_i\,x_i=0$ , the zero vector; (4) complementary slackness $\lambda_i\,(1-x_i\cdot x_i)=0$ for every $i$ (so for each $i$ , either $\lambda_i=0$ or $\lVert x_i\rVert^{2}=1$ ); (5) $\sum_i\lambda_i=nn$ , the dimension cast to $\mathbb{R}$ . Edge cases: for $m=0$ all sums are zero, so (2) would demand $0=I$ and (5) would demand $0=nn$ , impossible for $nn\ge 1$ — but for $m=0$ , $nn\ge 1$ the hypothesis itself is unsatisfiable (the empty set is contained in bodies of arbitrarily large determinant), so the statement is vacuous there. For $nn=0$ : $I$ is the unique $0\times 0$ matrix, (2)–(4) are trivial, and (5) reads $\sum\lambda_i=0$ , which with (1) forces $\lambda\equiv 0$ . More generally, for any point family for which $(I,0)$ is not determinant-maximal among containing bodies, the hypothesis fails and the theorem asserts nothing.

Human review

Endorsed by Community (Bot) · Aug 13, 2026
Endorsed by Shuze Chen · Aug 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph