Constant potential reduction yields an explicit iteration bound

Proved

LinearOptimization.interior_point_potential_reduction

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

complexityduality-gapinterior-pointpotential-reduction

(Theorem 9.4, p. 410 — generic potential-reduction iteration bound, Section 9.3) Define the potential function

G(\mathbf{x}, \mathbf{s}) = q\log \mathbf{s}'\mathbf{x} - \sum_{j=1}^n \log x_j - \sum_{j=1}^n \log s_j,

where $q$ is a constant larger than $n$ (p. 409). Let $\mathbf{x}^0 > \mathbf{0}$ and $(\mathbf{p}^0, \mathbf{s}^0)$ with $\mathbf{s}^0 > \mathbf{0}$ be feasible solutions to the primal and dual problem, respectively. Let $\varepsilon > 0$ be the optimality tolerance.

Any algorithm that maintains primal and dual feasibility and reduces $G(\mathbf{x}, \mathbf{s})$ by an amount greater than or equal to $\delta > 0$ at each iteration finds a solution to the primal and dual problems with duality gap

(\mathbf{s}^K)'\mathbf{x}^K \le \varepsilon,

after

K = \left\lceil \frac{G(\mathbf{x}^0, \mathbf{s}^0) + (q-n)\log(1/\varepsilon) - n\log n}{\delta} \right\rceil

iterations.

Preamble

import Definitions.Def_LinearOptimization_LogBarrier_CentralPath
import Definitions.Def_LinearOptimization_InteriorPointPotential


open Matrix

/-- **Bertsimas & Tsitsiklis, Theorem 9.4 (p. 410).** Potential reduction implies an explicit
iteration bound: if every step keeps `(x^k, s^k)` interior primal-dual
feasible and cuts `G` by at least `δ`, then after
`K = ⌈(G(x⁰, s⁰) + (q − n) log(1/ε) − n log n) / δ⌉` iterations the
duality gap satisfies `(s^K)'x^K ≤ ε`. -/

Formal statement

theorem LinearOptimization.interior_point_potential_reduction {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (c : Fin n → ℝ)
    (q delta eps : ℝ) (hq : (n : ℝ) < q) (hdelta : 0 < delta)
    (heps : 0 < eps)
    (x : ℕ → Fin n → ℝ) (p : ℕ → Fin m → ℝ) (s : ℕ → Fin n → ℝ)
    (hfeas : ∀ k, A.mulVec (x k) = b ∧ (∀ j, 0 < x k j) ∧
      Aᵀ.mulVec (p k) + s k = c ∧ (∀ j, 0 < s k j))
    (hdec : ∀ k, interiorPointPotential q (x (k + 1)) (s (k + 1)) ≤
      interiorPointPotential q (x k) (s k) - delta)
    (K : ℕ)
    (hK : K = ⌈(interiorPointPotential q (x 0) (s 0) +
      (q - n) * Real.log (1 / eps) - n * Real.log n) / delta⌉₊) :
    s K ⬝ᵥ x K ≤ eps := by
  sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 9.4, p. 410 (potential function p. 409, Assumption 9.3 p. 409)

Read-back

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

Fix a real $m\times n$ system $(A,b,c)$ , reals $q,\delta,\varepsilon$ with $n<q$ (real comparison against the casted dimension), $\delta>0$ , $\varepsilon>0$ , and sequences $x_k\in\mathbb{R}^n$ , $p_k\in\mathbb{R}^m$ , $s_k\in\mathbb{R}^n$ indexed by $k\in\mathbb{N}$ . Hypotheses: for every $k$ , $Ax_k=b$ , all coordinates of $x_k$ strictly positive, $A^{\mathsf T}p_k+s_k=c$ , and all coordinates of $s_k$ strictly positive; for every $k$ the potential $\Phi_q(x,s)=q\log(s\cdot x)-\sum_j\log x_j-\sum_j\log s_j$ (real $\log$ , $\log 0=0$ ) decreases by at least $\delta$ : $\Phi_q(x_{k+1},s_{k+1})\le\Phi_q(x_k,s_k)-\delta$ ; and $K$ is the natural number

K=\Big\lceil\big(\Phi_q(x_0,s_0)+(q-n)\log(1/\varepsilon)-n\log n\big)/\delta\Big\rceil_+,

the ceiling clamped to $0$ when the argument is nonpositive (and note $\log n$ uses $\log 0=0$ when $n=0$ ). Conclusion: the duality gap at iteration $K$ satisfies $s_K\cdot x_K\le\varepsilon$ (non-strict). Nothing is claimed for other indices, and no algorithm is specified — the decrease of $\Phi_q$ is hypothesized, not derived.

Human review

Endorsed by Community (Bot) · Aug 6, 2026
Endorsed by Shuze Chen · Aug 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph