Sums of self-concordant functions

Proved

ConvexOptimization.self_concordant_add

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

convex-optimizationinterior-pointself-concordance

Self-concordance is preserved by addition.

Let $\Omega \subseteq \mathbb{R}^n$ be open and let $f$ and $h$ both be self-concordant on $\Omega$ — convex, $C^3$ , and satisfying $|\varphi'''(0)| \le 2\varphi''(0)^{3/2}$ for every line restriction $\varphi(t) = f(x + tv)$ with $x \in \Omega$ . Then $f + h$ is self-concordant on $\Omega$ :

f, h \text{ self-concordant on } \Omega \;\Longrightarrow\; f + h \text{ self-concordant on } \Omega .

The proof is the elementary inequality $|u + v| \le 2(a^{3/2} + b^{3/2}) \le 2(a+b)^{3/2}$ for the pieces, and the practical consequence is a calculus: a barrier assembled from many self-concordant terms is self-concordant, so one never verifies the third-derivative condition for a composite function directly.

Formalization Note Openness of Ω is an explicit hypothesis, and it is genuinely needed: at a boundary point the iterated derivatives of the line restriction are junk values and the inequality would be asserted about meaningless quantities. 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 {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin n)))
    (hΩo : IsOpen Ω) (f h : EuclideanSpace ℝ (Fin n) → ℝ)
    (hf : IsSelfConcordantOn Ω f) (hh : IsSelfConcordantOn Ω h) :
    IsSelfConcordantOn Ω (f + h) := 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 addition). Openness of the domain is an explicit hypothesis: the line-restriction derivatives carry junk values at boundary points

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), and all total functions $f, h : \mathbb{R}^n \to \mathbb{R}$ such that both $f$ and $h$ are self-concordant on $\Omega$ , the pointwise sum $f + h$ is self-concordant on $\Omega$ . Here " $F$ is self-concordant on $\Omega$ " abbreviates the conjunction: (i) $\Omega$ is convex and $F(ax+by) \le aF(x) + bF(y)$ for all $x, y \in \Omega$ and $a, b \ge 0$ with $a + b = 1$ ; (ii) $F$ is three times continuously differentiable on $\Omega$ (within-set sense); (iii) for every $x \in \Omega$ and every vector $v \in \mathbb{R}^n$ (arbitrary, possibly zero, possibly leaving $\Omega$ ), the line restriction $\varphi(t) = F(x + tv)$ satisfies $|\varphi'''(0)| \le 2(\varphi''(0))^{3/2}$ , with derivatives at $0$ taken as total operators (junk values if $\varphi$ is insufficiently differentiable at $0$ ) and with the real power satisfying $b^{3/2} = 0$ whenever $b \le 0$ . The same constant $2$ and exponent $3/2$ appear in both hypotheses and conclusion — there is no rescaling of the sum. Edge cases: $\Omega = \emptyset$ makes both hypotheses and the conclusion vacuously true; no nonemptiness or properness of $\Omega$ is assumed.

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