The affine log barrier is self-concordant

Proved

ConvexOptimization.log_barrier_affine_self_concordant

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

convex-optimizationinterior-pointself-concordance

The logarithmic barrier of a polyhedron is self-concordant — example 9.6 of Boyd & Vandenberghe.

Let $a_1,\dots,a_m \in \mathbb{R}^n$ and $b \in \mathbb{R}^m$ , and consider the open polyhedron $\Omega = \{x : \langle a_i, x\rangle < b_i \text{ for all } i\}$ . Then

\varphi(x) \;=\; -\sum_{i=1}^{m} \log\bigl(b_i - \langle a_i, x\rangle\bigr)

is self-concordant on $\Omega$ .

This is the concrete anchor of the abstract theory: every line restriction of $\varphi$ is a sum of terms $-\log(\text{affine})$ , each of which meets the defining inequality with equality, and the closure of self-concordance under sums does the rest. It supplies the self-concordance hypothesis for linear and quadratic programming barriers, and hence for the complexity theorem that is the goal of this mission.

Formalization Note The domain is written as the set-builder {x | ∀ i, ⟪a i, x⟫ < b i} and the barrier is spelled out rather than routed through the mission's logBarrier definition, so that the constraint functions appear in the affine form $\langle a_i,x\rangle - b_i$ used in the book's example. Source: B&V §9.6.1, example 9.6, p. 497.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_selfConcordance

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.log_barrier_affine_self_concordant {n mI : ℕ}
    (a : Fin mI → EuclideanSpace ℝ (Fin n)) (b : Fin mI → ℝ) :
    IsSelfConcordantOn {x | ∀ i, ⟪a i, x⟫ < b i}
      (fun x => -∑ i, Real.log (b i - ⟪a i, x⟫)) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 499, §9.6.1 example 9.4 (log barrier for linear inequalities is self-concordant)

Read-back

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

For every natural number $n$ , every natural number $m_I$ , every family of vectors $a_i \in \mathbb{R}^n$ and reals $b_i$ (index $i$ over an $m_I$ -element type; no nondegeneracy is assumed — any $a_i$ may be the zero vector, and the family may be empty), the function

F(x) = -\sum_i \log\bigl(b_i - \langle a_i, x\rangle\bigr)

is self-concordant on the set $\Omega = \{x \in \mathbb{R}^n : \langle a_i, x\rangle < b_i \text{ for all } i\}$ . "Self-concordant on $\Omega$ " means the conjunction: (i) $\Omega$ is convex and $F(ax+by) \le aF(x)+bF(y)$ for $x,y \in \Omega$ , $a,b \ge 0$ , $a+b = 1$ ; (ii) $F$ is three times continuously differentiable on $\Omega$ (within-set sense); (iii) for every $x \in \Omega$ and every $v \in \mathbb{R}^n$ (arbitrary), the line restriction $\varphi(t) = F(x + tv)$ satisfies $|\varphi'''(0)| \le 2(\varphi''(0))^{3/2}$ at $t = 0$ , with total (possibly junk) derivatives and the real-power convention $b^{3/2} = 0$ for $b \le 0$ . Notes: on $\Omega$ every argument $b_i - \langle a_i, x\rangle$ is strictly positive, so the logarithms are genuine there; off $\Omega$ the function is still defined everywhere via the total logarithm ( $\log 0 = 0$ , $\log y = \log|y|$ for $y < 0$ ), but the self-concordance conditions only quantify over $\Omega$ (and only at $t = 0$ on each line). There are no openness, nonemptiness, or boundedness hypotheses: the claim includes the case $\Omega = \emptyset$ (everything vacuous) and $m_I = 0$ (empty sum, so $F \equiv 0$ and $\Omega = \mathbb{R}^n$ ). This theorem is stated with the sum written out directly; it does not syntactically reference the ConvexOptimization_logBarrier definition.

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