Prove2Me

Iteration bound O(n log⁡(nμ0/ε))O(\sqrt{n}\,\log(n\mu^0/\varepsilon)) for the primal path following algorithm

Proved
LinearOptimization.interior_point_path_following_iterations

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

complexityduality-gapinterior-pointnewton-methodpath-following

(Theorem 9.7, p. 426, GOAL — iteration bound for primal path following) Assume that the primal path following algorithm uses

α=1−β−ββ+n,\alpha = 1 - \frac{\sqrt{\beta} - \beta}{\sqrt{\beta} + \sqrt{n}},

where β<1\beta < 1 [formally 0<β<10 < \beta < 1; see design_note], and starts with an initial primal and dual feasible solution (x0,s0,p0)(\mathbf{x}^0, \mathbf{s}^0, \mathbf{p}^0), with x0>0\mathbf{x}^0 > \mathbf{0}, s0>0\mathbf{s}^0 > \mathbf{0}, that satisfies

∥1μ0X0S0e−e∥≤β.\left\| \frac{1}{\mu^0} X_0 S_0 \mathbf{e} - \mathbf{e} \right\| \le \beta.

Then, after

K=⌈β+nβ−β log⁡(s0)′x0(1+β)ε(1−β)⌉K = \left\lceil \frac{\sqrt{\beta} + \sqrt{n}}{\sqrt{\beta} - \beta} \, \log \frac{(\mathbf{s}^0)'\mathbf{x}^0 (1+\beta)}{\varepsilon(1-\beta)} \right\rceil

iterations, it finds a primal and dual feasible solution (xK,sK,pK)(\mathbf{x}^K, \mathbf{s}^K, \mathbf{p}^K) with duality gap

(sK)′xK≤ε.(\mathbf{s}^K)'\mathbf{x}^K \le \varepsilon.
Preamble
import Definitions.Def_LinearOptimization_PathFollowing


open Matrix

/-- **Bertsimas & Tsitsiklis, Theorem 9.7 (p. 426).** Primal path following reaches duality
gap `≤ ε` — primal and dual feasibly — within
`K = ⌈((√β + √n)/(√β − β)) log((s⁰)'x⁰(1+β)/(ε(1−β)))⌉` iterations, when
run with `α = 1 − (√β − β)/(√β + √n)` from a `β`-close interior feasible
start. -/
Formal statement
theorem LinearOptimization.interior_point_path_following_iterations {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (c : Fin n → ℝ)
    (hrank : LinearIndependent ℝ (fun i => A i))
    (beta eps alpha : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1)
    (heps : 0 < eps)
    (halpha : alpha = 1 -
      (Real.sqrt beta - beta) / (Real.sqrt beta + Real.sqrt n))
    (x : ℕ → Fin n → ℝ) (p : ℕ → Fin m → ℝ) (s : ℕ → Fin n → ℝ)
    (mu : ℕ → ℝ) (hmu0 : 0 < mu 0)
    (hxfeas0 : A.mulVec (x 0) = b) (hx0 : ∀ j, 0 < x 0 j)
    (hsfeas0 : Aᵀ.mulVec (p 0) + s 0 = c) (hs0 : ∀ j, 0 < s 0 j)
    (hprox0 : centralPathProximity (mu 0) (x 0) (s 0) ≤ beta)
    (hrun : IsPathFollowingRun A c alpha x p s mu)
    (K : ℕ)
    (hK : K = ⌈(Real.sqrt beta + Real.sqrt n) / (Real.sqrt beta - beta) *
      Real.log ((s 0 ⬝ᵥ x 0) * (1 + beta) / (eps * (1 - beta)))⌉₊) :
    A.mulVec (x K) = b ∧ 0 ≤ x K ∧
      Aᵀ.mulVec (p K) + s K = c ∧ 0 ≤ s K ∧
      s K ⬝ᵥ x K ≤ eps := by
  sorry
Source
Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 9.7, p. 426 (proof pp. 427-429; final display and Eq. (9.23) p. 429)
Read-back

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

Fix a real m×nm\times n system (A,b,c)(A,b,c) whose mm rows AiA_i are linearly independent as vectors of Rn\mathbb{R}^n; reals β∈(0,1)\beta\in(0,1) (both bounds strict), ε>0\varepsilon>0, and α\alpha defined by α=1−β−ββ+n\alpha=1-\frac{\sqrt\beta-\beta}{\sqrt\beta+\sqrt n}; sequences xk,sk∈Rnx_k,s_k\in\mathbb{R}^n, pk∈Rmp_k\in\mathbb{R}^m, μk∈R\mu_k\in\mathbb{R} with: μ0>0\mu_0>0; Ax0=bAx_0=b with all coordinates of x0x_0 strictly positive; ATp0+s0=cA^{\mathsf T}p_0+s_0=c with s0s_0 strictly positive; the proximity ∑j(x0,js0,j/μ0−1)2≤β\sqrt{\sum_j(x_{0,j}s_{0,j}/\mu_0-1)^2}\le\beta; and the sequences form a path-following run: for every kk, xk>0x_k>0 strictly, μk+1=αμk\mu_{k+1}=\alpha\mu_k, and there is dd with μk+1diag(xk,j−2)d−ATpk+1=μk+1diag(xk,j−1)1−c\mu_{k+1}\mathrm{diag}(x_{k,j}^{-2})d-A^{\mathsf T}p_{k+1}=\mu_{k+1}\mathrm{diag}(x_{k,j}^{-1})\mathbf 1-c, Ad=0Ad=0, xk+1=xk+dx_{k+1}=x_k+d, sk+1=c−ATpk+1s_{k+1}=c-A^{\mathsf T}p_{k+1}. Let

K=⌈β+nβ−β ln⁡ ⁣((s0⋅x0)(1+β)ε(1−β))⌉+K=\Big\lceil\tfrac{\sqrt\beta+\sqrt n}{\sqrt\beta-\beta}\,\ln\!\big(\tfrac{(s_0\cdot x_0)(1+\beta)}{\varepsilon(1-\beta)}\big)\Big\rceil_+

(natural ceiling, clamped at 00). Conclusion, a five-fold conjunction about iterate KK only: AxK=bAx_K=b; xK≥0x_K\ge0 componentwise (non-strict); ATpK+sK=cA^{\mathsf T}p_K+s_K=c; sK≥0s_K\ge0; and sK⋅xK≤εs_K\cdot x_K\le\varepsilon. Note the run definition itself does not mention bb; primal feasibility of xKx_K is part of the conclusion, derived from Ax0=bAx_0=b and Ad=0Ad=0-type steps.

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