Self-concordance is stable under affine additions

Proved

ConvexOptimization.self_concordant_add_linear

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

convex-optimizationinterior-pointself-concordance

Self-concordance is preserved by adding an affine function.

Let $\Omega \subseteq \mathbb{R}^n$ be open, let $f$ be self-concordant on $\Omega$ , and let $c \in \mathbb{R}^n$ , $r \in \mathbb{R}$ . Then

x \;\longmapsto\; f(x) + \langle c, x\rangle + r

is self-concordant on $\Omega$ .

An affine term contributes nothing to the second or third derivative of any line restriction, so both sides of the defining inequality are unchanged. Together with closure under sums this is what makes the barrier objective tractable: adding the scaled objective $t f_0$ to the barrier $\varphi$ preserves self-concordance whenever $f_0$ is affine — the case of linear programming — and more generally reduces the verification to $f_0$ alone.

Formalization Note Openness of Ω is required for the same reason as in the additivity statement: the line-restriction derivatives are only meaningful at interior points. Source: B&V §9.6.1, p. 497.

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_selfConcordance

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.self_concordant_add_linear {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n)))
    (hΩo : IsOpen Ω)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : IsSelfConcordantOn Ω f)
    (c : EuclideanSpace ℝ (Fin n)) (r : ℝ) :
    IsSelfConcordantOn Ω (fun x => f x + ⟪c, x⟫ + r) := 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 (self-concordance is preserved by scaling and by adding an affine function)

Read-back

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

For every natural number $n$ , every open set $\Omega \subseteq \mathbb{R}^n$ (openness is an explicit hypothesis), every total function $f : \mathbb{R}^n \to \mathbb{R}$ that is self-concordant on $\Omega$ , every fixed vector $c \in \mathbb{R}^n$ , and every real constant $r$ , the function $x \mapsto f(x) + \langle c, x\rangle + r$ (real Euclidean inner product; $c$ and $r$ arbitrary, e.g. $c = 0$ ) is self-concordant on $\Omega$ . Here "self-concordant on $\Omega$ " for a function $F$ means the conjunction: (i) $\Omega$ is convex and $F(ax+by) \le aF(x)+bF(y)$ for all $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$ , the line restriction $\varphi(t) = F(x+tv)$ satisfies $|\varphi'''(0)| \le 2(\varphi''(0))^{3/2}$ at $t = 0$ , with total (possibly junk) derivative values and real power convention $b^{3/2} = 0$ for $b \le 0$ . Vacuous when $\Omega = \emptyset$ .

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