Sufficiency of the KKT conditions for the barrier problems (points on the central path)

Proved

LinearOptimization.interior_point_kkt_sufficiency

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

central-pathconvex-optimizationinterior-pointkkt

(Lemma 9.5, p. 421) If $\mathbf{x}^*$ , $\mathbf{p}^*$ , and $\mathbf{s}^*$ satisfy conditions (9.17) [ $A\mathbf{x}^* = \mathbf{b}$ , $\mathbf{x}^* \ge \mathbf{0}$ , $A'\mathbf{p}^* + \mathbf{s}^* = \mathbf{c}$ , $\mathbf{s}^* \ge \mathbf{0}$ , $X^*S^*\mathbf{e} = \mu\mathbf{e}$ for a given $\mu > 0$ ], then they are optimal solutions to problems (9.15) and (9.16), i.e., $\mathbf{x}^* = \mathbf{x}(\mu)$ , $\mathbf{p}^* = \mathbf{p}(\mu)$ , $\mathbf{s}^* = \mathbf{s}(\mu)$ :

B_\mu(\mathbf{x}^*) \le B_\mu(\mathbf{x})

for every $\mathbf{x} > \mathbf{0}$ with $A\mathbf{x} = \mathbf{b}$ (with equality iff $\mathbf{x} = \mathbf{x}^*$ , so $\mathbf{x}^*$ is the unique minimizer), and symmetrically $(\mathbf{p}^*, \mathbf{s}^*)$ is optimal for the dual barrier problem (9.16).

Preamble

import Definitions.Def_LinearOptimization_LogBarrier_CentralPath


open Matrix

/-- **Bertsimas & Tsitsiklis, Lemma 9.5 (p. 421).** KKT sufficiency for the barrier problems:
a solution `(x*, p*, s*)` of (9.17) at `μ > 0` has `x*` as the unique
minimizer of `B_μ` over the interior primal feasible set, and `(p*, s*)`
as a maximizer of the dual barrier objective over the interior dual
feasible set. -/

Formal statement

theorem LinearOptimization.interior_point_kkt_sufficiency {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (c : Fin n → ℝ)
    (mu : ℝ) (hmu : 0 < mu)
    (xstar : Fin n → ℝ) (pstar : Fin m → ℝ) (sstar : Fin n → ℝ)
    (hkkt : IsCentralPathPoint A b c mu xstar pstar sstar) :
    (∀ x : Fin n → ℝ, A.mulVec x = b → (∀ j, 0 < x j) →
      logBarrier c mu xstar ≤ logBarrier c mu x ∧
        (logBarrier c mu x = logBarrier c mu xstar → x = xstar)) ∧
    (∀ (p : Fin m → ℝ) (s : Fin n → ℝ), Aᵀ.mulVec p + s = c →
      (∀ j, 0 < s j) →
      dualLogBarrier b mu p s ≤ dualLogBarrier b mu pstar sstar) := by
  sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Lemma 9.5, p. 421

Read-back

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

Fix a real $m\times n$ matrix $A$ , vectors $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ , a real $\mu>0$ , and a triple $(x^\ast,p^\ast,s^\ast)$ that is a central-path point at $\mu$ : $Ax^\ast=b$ , $x^\ast\ge0$ componentwise (non-strict), $A^{\mathsf T}p^\ast+s^\ast=c$ , $s^\ast\ge0$ , and $x^\ast_j s^\ast_j=\mu$ for every $j$ . Writing $B_\mu(x)=c\cdot x-\mu\sum_j\log x_j$ and $B^\ast_\mu(p,s)=p\cdot b+\mu\sum_j\log s_j$ (real $\log$ with $\log 0=0$ , $\log$ of a negative $=\log$ of its absolute value), the conclusion is a conjunction: (a) for every $x$ with $Ax=b$ and $x_j>0$ strictly for all $j$ : $B_\mu(x^\ast)\le B_\mu(x)$ , and if $B_\mu(x)=B_\mu(x^\ast)$ then $x=x^\ast$ (so $x^\ast$ is the unique minimizer among strictly positive primal-feasible points — note $x^\ast$ itself is only assumed $\ge0$ , and the comparison set is the strictly positive one); (b) for every $(p,s)$ with $A^{\mathsf T}p+s=c$ and $s_j>0$ strictly: $B^\ast_\mu(p,s)\le B^\ast_\mu(p^\ast,s^\ast)$ — a maximality claim with no uniqueness clause on the dual side.

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