Affine invariance of the Löwner–John ellipsoid

Proved

ConvexOptimization.lowner_john_affine_invariant

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

convexgeometryconvexoptimizationellipsoids

The Löwner–John ellipsoid commutes with nonsingular affine changes of coordinates.

Let $S \subseteq \mathbb{R}^n$ , let $T \in \mathbb{R}^{n \times n}$ be invertible, let $t \in \mathbb{R}^n$ , and write $\Phi(v) = Tv + t$ for the corresponding affine bijection. If $(A,b)$ is a Löwner–John pair for $S$ , then the image set $\Phi(S)$ also admits a Löwner–John pair $(A',b')$ , and its ellipsoid is the affine image of the original:

\mathcal{E}(A',b') \;=\; \Phi\bigl(\mathcal{E}(A,b)\bigr), \qquad \mathcal{E}(A,b) = \{v : \lVert Av+b\rVert_2 \le 1\}.

(Concretely one may take $A' = A T^{-1}$ and $b' = b - A T^{-1} t$ , which is again symmetric-positive-definite up to the normalization built into the predicate.)

Affine invariance is what makes the normalization step of this mission legitimate: an arbitrary configuration can be mapped so that its Löwner–John ellipsoid becomes the unit ball, where the KKT identities take their clean isotropic form, and the conclusion transported back. It also shows the rounding factor $1/n$ is an affine invariant of the body, not an artefact of a particular position — determinant ratios, unlike volumes, are unchanged by $\Phi$ .

Formalization Note Nonsingularity is stated as IsUnit T.det; the image is (fun v => T.mulVec v + t) '' S. The conclusion is existential in $(A',b')$ together with the set identity, even though uniqueness makes the pair determined. Source: Boyd & Vandenberghe §8.4.3, pp. 415–416.

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_affine_invariant {nn : ℕ}
    (T : Matrix (Fin nn) (Fin nn) ℝ) (hT : IsUnit T.det) (t : Fin nn → ℝ)
    (S : Set (Fin nn → ℝ)) (A : Matrix (Fin nn) (Fin nn) ℝ) (b : Fin nn → ℝ)
    (h : IsLownerJohn A b S) :
    ∃ (A' : Matrix (Fin nn) (Fin nn) ℝ) (b' : Fin nn → ℝ),
      IsLownerJohn A' b' ((fun v => T.mulVec v + t) '' S) ∧
      ellipsoidBody A' b' = (fun v => T.mulVec v + t) '' ellipsoidBody A b := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 415-416, §8.4.3 (affine invariance of the extremal volume ellipsoids)

Read-back

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

Theorem. For every $nn\in\mathbb{N}$ , every $nn\times nn$ real matrix $T$ whose determinant is a unit in $\mathbb{R}$ (over the reals this means exactly $\det T\neq 0$ , i.e. $T$ invertible), every translation vector $t\in\mathbb{R}^{nn}$ , every set $S\subseteq\mathbb{R}^{nn}$ (an arbitrary set — not required to be finite, a point range, convex, bounded, or full-dimensional), and every pair $(A,b)$ satisfying the Löwner–John predicate for $S$ (unfolded: $A$ symmetric; $A$ positive definite, which in Mathlib includes symmetry; $S\subseteq\{v:\lVert Av+b\rVert^{2}\le 1\}$ ; and $\det A'\le\det A$ for every symmetric positive-definite $A'$ with any offset $b'$ whose body contains $S$ ), there exist a matrix $A'$ and a vector $b'$ such that both conjuncts hold for the same witness pair: (i) $(A',b')$ satisfies the Löwner–John predicate for the image set $\{Tv+t : v\in S\}$ , and (ii) as an equality of sets, $\{v:\lVert A'v+b'\rVert^{2}\le 1\}=\{Tw+t : \lVert Aw+b\rVert^{2}\le 1\}$ — the new body is exactly the image of the old body under the same affine map $v\mapsto Tv+t$ . Only existence is claimed; no formula for $(A',b')$ is given and no uniqueness is asserted. Edge cases: for $nn=0$ the unique matrix has determinant $1$ (a unit) and everything lives in a one-point space; for any $S$ for which the Löwner–John predicate is unsatisfiable, the hypothesis on $(A,b)$ cannot hold and the statement is vacuous for that $S$ .

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