Central-path duality gap $m/t$

Proved

ConvexOptimization.central_path_duality_gap

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

convex-optimizationinterior-pointself-concordance

The central path has duality gap $m/t$ .

Consider minimizing a convex differentiable $f_0$ subject to $f_i(x) \le 0$ $(i = 1,\dots,m)$ , with each $f_i$ convex and differentiable, and let $\varphi(x) = -\sum_i \log(-f_i(x))$ be the logarithmic barrier on the strictly feasible set. Fix $t > 0$ and let $x^{\star}(t)$ be a strictly feasible minimizer of $t f_0 + \varphi$ — the central point for the parameter $t$ . Then for every feasible $x$ ,

f_0\bigl(x^{\star}(t)\bigr) - \frac{m}{t} \;\le\; f_0(x),

i.e. $x^{\star}(t)$ is at most $m/t$ -suboptimal.

The bound comes from reading the stationarity condition of the centering problem as a dual feasible point: the multipliers $\lambda_i = -1/(t f_i(x^{\star}(t)))$ are dual feasible and yield exactly the gap $m/t$ . Its consequences organize the whole method: to reach accuracy $\varepsilon$ it suffices to follow the path to $t = m/\varepsilon$ , and since the outer loop multiplies $t$ by $\mu$ each round, the number of centering steps is logarithmic in $m/(t^{(0)}\varepsilon)$ .

Formalization Note The central point is given as a hypothesis — a strictly feasible point minimizing $t f_0 + \varphi$ over {x | ∀ i, fc i x < 0} — rather than constructed, so no existence or uniqueness argument is packed into the statement; $m$ appears as the cast (mI : ℝ) of the number of inequality constraints. Source: B&V §11.2.2, p. 566.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_logBarrier

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.central_path_duality_gap {n mI : ℕ} (t : ℝ) (ht : 0 < t)
    (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 : EuclideanSpace ℝ (Fin n)) (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)
    (x : EuclideanSpace ℝ (Fin n)) (hx : ∀ i, fc i x ≤ 0) :
    f₀ xc - (mI : ℝ) / t ≤ f₀ x := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 566, §11.2.2 (the central point x*(t) is no more than m/t suboptimal; stated unnumbered in the text)

Read-back

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

Fix naturals $n, m_I$ (either may be $0$ ) and a real $t > 0$ . Hypotheses: $f_0 : \mathbb{R}^n \to \mathbb{R}$ is convex on all of $\mathbb{R}^n$ ; a family of $m_I$ constraint functions $f_i : \mathbb{R}^n \to \mathbb{R}$ , each convex on all of $\mathbb{R}^n$ and each differentiable everywhere; $f_0$ is differentiable everywhere; a point $x_c$ with $f_i(x_c) < 0$ for every $i$ (strictly feasible); the minimality hypothesis that for every $y$ in $S = \{x : f_i(x) < 0 \text{ for all } i\}$ ,

t\,f_0(x_c) + B(x_c) \le t\,f_0(y) + B(y),

where $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$ ; on $S$ all arguments $-f_i(x)$ are positive so the logs there are genuine) — note the minimality predicate quantifies over $S$ but does not itself assert $x_c \in S$ ; that follows from the separate strict-feasibility hypothesis; and finally a point $x$ with $f_i(x) \le 0$ for every $i$ (weak inequalities — the boundary is allowed). Conclusion:

f_0(x_c) - \frac{m_I}{t} \le f_0(x).

That is, for each such feasible $x$ , the objective value at the barrier minimizer $x_c$ exceeds $f_0(x)$ by at most $m_I/t$ (here $m_I$ is the natural number of constraints cast to a real). Edge cases: if $m_I = 0$ then both feasibility hypotheses are vacuous (every point of $\mathbb{R}^n$ qualifies), $B \equiv 0$ , $m_I/t = 0$ , and the claim reads: a global minimizer of $t f_0$ satisfies $f_0(x_c) \le f_0(x)$ for every $x$ . No boundedness, attainment, or constraint-qualification hypotheses appear; the existence of the minimizer $x_c$ is itself a hypothesis, not a conclusion.

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

Central-path duality gap m/tm/tm/t

Central-path duality gap $m/t$