Convexity of log-sum-exp

Proved

ConvexOptimization.log_sum_exp_convexOn

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

convexanalysisconvexoptimizationlog-concavity

Convexity of the log-sum-exp function.

The function

x \;\longmapsto\; \log\Bigl(\sum_{i=1}^{n} e^{x_i}\Bigr)

is convex on $\mathbb{R}^n$ .

Log-sum-exp is the smooth approximation of the maximum, satisfying $\max_i x_i \le \log\sum_i e^{x_i} \le \max_i x_i + \log n$ , so its convexity is a differentiable surrogate for the (also convex, but nonsmooth) maximum function. It is the log-partition function of an exponential family — its gradient is the softmax, its Hessian the covariance of the associated distribution — and it is the Fenchel conjugate of the negative entropy on the probability simplex.

Together with $\log\det$ it is the most frequently reused convexity fact in the book: geometric programming, logistic regression, maximum-entropy estimation and softmax classifiers all rest on it.

Formalization Note The variable is an element of EuclideanSpace ℝ (Fin n) and x i denotes its $i$ -th coordinate; convexity is asserted on Set.univ. Source: B&V §3.1.5, p. 72.

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.log_sum_exp_convexOn {n : ℕ} :
    ConvexOn ℝ Set.univ
      (fun x : EuclideanSpace ℝ (Fin n) => Real.log (∑ i, Real.exp (x i))) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 72, §3.1.5 Examples, the Log-sum-exp item

Read-back

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

Theorem statement. For every natural number $n$ , the function $x \mapsto \log\big(\sum_{i<n} e^{x_i}\big)$ on Euclidean $n$ -space is convex on the whole space: Mathlib's ConvexOn over the universal set, i.e. (the universal set is convex, trivially, and) for all $x, y \in \mathbb{R}^n$ and all $a, b \ge 0$ with $a + b = 1$ , $\log\sum_i e^{(ax+by)_i} \le a\,\log\sum_i e^{x_i} + b\,\log\sum_i e^{y_i}$ . The sum is over the finite index set of size $n$ and the log is Real.log with junk convention $\log t = 0$ for $t \le 0$ . Degenerate case $n = 0$ : the sum is empty, hence $0$ , and $\log 0 = 0$ by the convention, so the function is the constant $0$ on a one-point space and the claim is trivial; for $n \ge 1$ the sum of exponentials is strictly positive and the logarithm is genuine.

Human review

Endorsed by Community (Bot) · Aug 11, 2026
Endorsed by Shuze Chen · Aug 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph