Per-centering potential gap

Proved

ConvexOptimization.barrier_centering_potential_gap

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

convex-optimizationinterior-pointself-concordance

The objective gap at the start of each centering step is bounded by $m(\mu - 1 - \log\mu)$ — inequalities (11.25)–(11.26) of Boyd & Vandenberghe.

With the notation above, fix $t > 0$ and $\mu > 1$ , and let $x^{\star}(t)$ and $x^{\star}(\mu t)$ be central points for $t$ and $\mu t$ respectively. The barrier method starts the next centering problem, whose objective is $\mu t f_0 + \varphi$ , at the previous central point $x^{\star}(t)$ . Then

\bigl(\mu t f_0(x^{\star}(t)) + \varphi(x^{\star}(t))\bigr) \;-\; \bigl(\mu t f_0(x^{\star}(\mu t)) + \varphi(x^{\star}(\mu t))\bigr) \;\le\; m\,\bigl(\mu - 1 - \log\mu\bigr).

The initial suboptimality of every centering problem is therefore bounded by a quantity depending only on $m$ and $\mu$ — not on $t$ , and not on how far along the path the method has travelled. Feeding it into the Newton iteration bound gives a uniform per-centering cost of $m(\mu - 1 - \log\mu)/\gamma + c$ Newton steps. The trade-off in $\mu$ is now visible: large $\mu$ means few outer steps but expensive centering, and since $\mu - 1 - \log\mu \approx (\mu-1)^2/2$ for $\mu$ near $1$ , the choice $\mu = 1 + 1/\sqrt{m}$ makes the per-centering cost $O(1)$ while keeping the outer count $O(\sqrt{m}\log(1/\varepsilon))$ — the balance that produces the mission's goal.

Formalization Note Both central points are hypotheses (strictly feasible minimizers of the respective centering objectives over the strictly feasible set), so the statement asserts nothing about existence of the central path. Source: B&V §11.5.2, pp. 588–589, eqs. (11.25)–(11.26).

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_logBarrier

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.barrier_centering_potential_gap {n mI : ℕ} (t μ : ℝ)
    (ht : 0 < t) (hμ : 1 < μ)
    (f₀ : EuclideanSpace ℝ (Fin n) → ℝ) (hf₀ : ConvexOn ℝ Set.univ f₀)
    (fc : Fin mI → EuclideanSpace ℝ (Fin n) → ℝ)
    (hfc : ∀ i, ConvexOn ℝ Set.univ (fc i))
    (hfc_diff : ∀ i, Differentiable ℝ (fc i)) (hf₀_diff : Differentiable ℝ f₀)
    (xc xc' : EuclideanSpace ℝ (Fin n))
    (hxc_str : ∀ i, fc i xc < 0) (hxc'_str : ∀ i, fc i xc' < 0)
    (hxc_min : IsMinOn (fun x => t * f₀ x + logBarrier fc x)
      {x | ∀ i, fc i x < 0} xc)
    (hxc'_min : IsMinOn (fun x => μ * t * f₀ x + logBarrier fc x)
      {x | ∀ i, fc i x < 0} xc') :
    μ * t * f₀ xc + logBarrier fc xc - (μ * t * f₀ xc' + logBarrier fc xc') ≤
      (mI : ℝ) * (μ - 1 - Real.log μ) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 588-589, §11.5.2 eq. (11.25)-(11.26) (bound on the objective gap at the start of each centering step)

Read-back

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

Fix naturals $n, m_I$ (either may be $0$ ) and reals $t, \mu$ with $t > 0$ and $\mu > 1$ . Hypotheses: $f_0 : \mathbb{R}^n \to \mathbb{R}$ convex on all of $\mathbb{R}^n$ and differentiable everywhere; a family of $m_I$ functions $f_i$ , each convex on all of $\mathbb{R}^n$ and differentiable everywhere; two points $x_c$ and $x_c'$ , each strictly feasible ( $f_i(x_c) < 0$ and $f_i(x_c') < 0$ for every $i$ ); $x_c$ minimizes $x \mapsto t\,f_0(x) + B(x)$ over $S = \{x : f_i(x) < 0 \text{ for all } i\}$ , and $x_c'$ minimizes $x \mapsto \mu t\,f_0(x) + B(x)$ over the same $S$ — in each case "minimizes over $S$ " means the function value at the named point is $\le$ its value at every $y \in S$ (the predicate does not itself include membership; strict feasibility is hypothesized separately), and $B(x) = -\sum_i \log(-f_i(x))$ is the log-barrier with the total real logarithm ( $\log 0 = 0$ , $\log y = \log|y|$ for $y < 0$ ; genuine on $S$ ). Conclusion:

\bigl(\mu t\,f_0(x_c) + B(x_c)\bigr) - \bigl(\mu t\,f_0(x_c') + B(x_c')\bigr) \le m_I\,(\mu - 1 - \log\mu),

i.e. the value of the scaled objective $\mu t f_0 + B$ at the old center $x_c$ exceeds its value at its own minimizer $x_c'$ by at most $m_I(\mu - 1 - \log\mu)$ , where $m_I$ is the constraint count cast to a real and $\log\mu$ is the genuine logarithm since $\mu > 1$ . Edge case: $m_I = 0$ gives $B \equiv 0$ , vacuous feasibility, and right-hand side $0$ . No uniqueness of minimizers, attainment, or further regularity is asserted or assumed beyond the listed hypotheses.

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