Theorem 3.14 — the space-dilation ellipsoid method keeps $x^*$ in $\{x : \|A_k(x_k - x)\| \le (n+1)h_k\}$

Open

ShorNonsmooth.Ellipsoid.ellipsoid_method_localizes

by mikedeng1 · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

ellipsoid-methodp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1space-dilationsubgradient-method

Let $n > 1$ and let $g : E_n \to E_n$ be a vector field, not necessarily continuous. Let $x^* \in E_n$ solve the problem

(g(x), x - x^*) \ge 0 \qquad \text{for all } x \in E_n ,

and suppose it is known a priori that $x^* \in S(x_0, R) = \{x : \|x - x_0\| \le R\}$ for some $R > 0$ . Run the algorithm (3.57)–(3.60) from $x_0$ , $B_0 = I_n$ , $h_0 = R/(n+1)$ :

\xi_k = \frac{B_k^* g(x_k)}{\|B_k^* g(x_k)\|},\quad x_{k+1} = x_k - h_k B_k \xi_k,\quad B_{k+1} = B_k R_\beta(\xi_k),\quad h_{k+1} = \frac{n}{\sqrt{n^2-1}}\,h_k ,

with $\beta = \sqrt{(n-1)/(n+1)}$ , stopping if $g(x_k) = 0$ . Then, with $A_k = B_k^{-1}$ ,

\|A_k(x_k - x^*)\| \le h_k (n + 1) \qquad \text{for all } k = 0, 1, \dots \tag{3.61}

In words, $x^*$ lies in the ellipsoid $\{x : \|A_k(x - x_k)\| \le (n+1) h_k\}$ centered at the current iterate, for every $k$ . Combined with the volume computation on p. 87 this shows that the region known to contain $x^*$ shrinks in volume by the factor $q_n < 1$ per iteration, whatever the field $g$ .

Formalization Note If $g(x_k) = 0$ the method stops; the Lean sequence then repeats the state $(x_k, B_k, h_k)$ , so the inequality is asserted for every $k$ of the stopped sequence. The book also assumes, in the description of the algorithm, that $g(x) \ne 0$ for $x \ne x^*$ ; its proof on pp. 86–87 does not use this, and neither do its applications (3.62), (3.65), so the hypothesis is omitted and the statement is correspondingly stronger. $A_k$ is the matrix inverse of $B_k$ , which is nonsingular ( $\det B_k = \beta^k$ ).

Preamble

import Mathlib
import Definitions.Def_ShorNonsmooth_Ellipsoid_EllipsoidMethod

Formal statement

namespace ShorNonsmooth.Ellipsoid

/-- Shor (1985), p. 86, Theorem 3.14. Let `n > 1`, let `g` be a vector field on `E_n` (not
necessarily continuous) and let `x*` solve the problem `(g(x), x - x*) ≥ 0` for all `x ∈ E_n`,
with `x* ∈ S(x₀, R)`, `R > 0`. Then the sequence generated by the algorithm (3.57)–(3.60)
(`B₀ = I`, `h₀ = R/(n + 1)`) satisfies `‖A_k (x_k - x*)‖ ≤ h_k (n + 1)` for all `k = 0, 1, …`,
where `A_k = B_k⁻¹` (3.61). If `g(x_k) = 0` the method stops and the state is repeated
(see `ellStep`). The book's standing assumption "`g(x) ≠ 0` if `x ≠ x*`" is not used by the
proof on pp. 86–87 and is dropped. -/
theorem ellipsoid_method_localizes {n : ℕ} (hn : 1 < n)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (R : ℝ) (hR : 0 < R)
    (x₀ xstar : EuclideanSpace ℝ (Fin n))
    (hsol : ∀ x : EuclideanSpace ℝ (Fin n), 0 ≤ inner ℝ (g x) (x - xstar))
    (hball : xstar ∈ Metric.closedBall x₀ R) (k : ℕ) :
    ‖Matrix.toEuclideanLin (ellipsoidMethod g R x₀ k).B⁻¹
        ((ellipsoidMethod g R x₀ k).x - xstar)‖ ≤
      (ellipsoidMethod g R x₀ k).h * ((n : ℝ) + 1) := by sorry

end ShorNonsmooth.Ellipsoid

Source

Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, p. 86, Theorem 3.14, Eq. (3.61), with the setting of §3.8 (p. 86) and the algorithm (3.57)–(3.60)

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 3.14 — the space-dilation ellipsoid method keeps x∗x^*x∗ in {x:∥Ak(xk−x)∥≤(n+1)hk}\{x : \|A_k(x_k - x)\| \le (n+1)h_k\}{x:∥Ak​(xk​−x)∥≤(n+1)hk​}

Theorem 3.14 — the space-dilation ellipsoid method keeps $x^*$ in $\{x : \|A_k(x_k - x)\| \le (n+1)h_k\}$