Uniqueness of the Löwner–John ellipsoid

Proved

ConvexOptimization.lowner_john_unique

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

convexgeometryconvexoptimizationellipsoids

Uniqueness of the Löwner–John ellipsoid, at the level of its parametrizing pair.

Let $x_1, \dots, x_m \in \mathbb{R}^n$ and suppose $(A_1, b_1)$ and $(A_2, b_2)$ are both Löwner–John pairs for $\{x_1,\dots,x_m\}$ — each symmetric positive definite, covering, and of maximal determinant among covering pairs. Then

A_1 = A_2 \qquad\text{and}\qquad b_1 = b_2 .

Together with existence, this licenses the phrase the minimum-volume covering ellipsoid and makes the affine-invariance and rounding statements well posed: the ellipsoid attached to a point set is a genuine function of the set, so normalizing a configuration by an affine change of coordinates is unambiguous.

No full-dimensionality hypothesis is needed here, because it is already implied: for a point set contained in a proper affine subspace no maximal covering pair exists, so the hypotheses are vacuous in that case.

Formalization Note The conclusion identifies the parameters, which is stronger than identifying the sets $\mathcal{E}(A_1,b_1) = \mathcal{E}(A_2,b_2)$ ; it is the symmetry-plus-positive-definiteness normalization inside the Löwner–John predicate that makes the parametrization rigid. Source: Boyd & Vandenberghe, exercise 8.12.

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_unique {nn m : ℕ} (x : Fin m → Fin nn → ℝ)
    (A₁ A₂ : Matrix (Fin nn) (Fin nn) ℝ) (b₁ b₂ : Fin nn → ℝ)
    (h₁ : IsLownerJohn A₁ b₁ (Set.range x))
    (h₂ : IsLownerJohn A₂ b₂ (Set.range x)) :
    A₁ = A₂ ∧ b₁ = b₂ := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 449, exercise 8.12 (show that the Loewner-John ellipsoid of a set is unique)

Read-back

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

Theorem. For all $nn,m\in\mathbb{N}$ , every family of points $x_1,\dots,x_m\in\mathbb{R}^{nn}$ , all matrices $A_1,A_2$ and vectors $b_1,b_2$ : if both pairs $(A_1,b_1)$ and $(A_2,b_2)$ satisfy the Löwner–John predicate for the point set $\{x_i\}$ — that is, for each $j\in\{1,2\}$ : $A_j$ is symmetric, $A_j$ is positive definite (Mathlib's notion, including symmetry), every $x_i$ satisfies $\lVert A_j x_i+b_j\rVert^{2}\le 1$ , and $\det A'\le\det A_j$ for every symmetric positive-definite $A'$ with any offset $b'$ whose body contains all the $x_i$ — then $A_1=A_2$ and $b_1=b_2$ , exact equality of matrices and of vectors. There is no hypothesis of full-dimensionality, nonemptiness, or $m\ge 1$ : for instances where the predicate is unsatisfiable (e.g. $m=0$ with $nn\ge 1$ , or all points contained in a proper affine subspace, where no determinant-maximal containing body exists), the statement holds vacuously. For $nn=0$ the matrix and vector types each have exactly one element, so the conclusion is automatic.

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