Concavity of $\log\det$

Proved

ConvexOptimization.log_det_concaveOn

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

convexanalysisconvexoptimizationlog-concavity

Concavity of $\log\det$ on the positive definite cone.

On the set of symmetric positive definite $n \times n$ real matrices, the function

A \;\longmapsto\; \log \det A

is concave: $\log\det(\theta A + (1-\theta)B) \ge \theta \log\det A + (1-\theta)\log\det B$ for positive definite $A, B$ and $\theta \in [0,1]$ .

Equivalently $-\log\det$ is convex — it is the standard barrier function for the semidefinite cone, and the reason interior-point methods for semidefinite programs work. The same function is the log-likelihood of a centred Gaussian in terms of the precision matrix, so concavity is what makes maximum-likelihood covariance estimation a convex problem, and it is the objective whose maximization defines the Löwner–John ellipsoid.

Formalization Note The domain is the set {A : Matrix (Fin n) (Fin n) ℝ | A.PosDef} inside the space of all matrices, and concavity is Mathlib's ConcaveOn ℝ; positive definiteness in Mathlib includes symmetry (Hermitian-ness), so no separate symmetry hypothesis appears. Source: B&V §3.1.5, p. 74.

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.log_det_concaveOn {n : ℕ} :
    ConcaveOn ℝ {A : Matrix (Fin n) (Fin n) ℝ | A.PosDef}
      (fun A => Real.log A.det) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 73, §3.1.5 Examples, the Log-determinant item (f(X) = log det X is concave on the PD cone)

Read-back

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

Theorem statement. For every natural number $n$ , the function $A \mapsto \log(\det A)$ is concave on the set $\{A \in \mathbb{R}^{n\times n} \mid A \text{ positive definite}\}$ , where Mathlib's ConcaveOn is a conjunction: (i) the set of positive-definite matrices is convex in the real vector space of $n \times n$ matrices, and (ii) for all positive-definite $A, B$ and all $a, b \ge 0$ with $a + b = 1$ , $a \log\det A + b \log\det B \le \log\det(aA + bB)$ — so the convexity of the PSD-interior cone is itself part of the assertion. "Positive definite" is Mathlib's: symmetric (Hermitian over $\mathbb{R}$ ) and $x^{\mathsf T} A x > 0$ for every $x \ne 0$ . The logarithm is the real Real.log with the junk convention $\log t = 0$ for $t \le 0$ ; on positive-definite matrices $\det > 0$ so the convention is not exercised at the points quantified over, but the function in the statement is defined (by that convention) on all matrices. Degenerate case $n = 0$ : the unique $0\times 0$ matrix is positive definite (the $x\ne 0$ condition is vacuous), its determinant is $1$ , and the set is a singleton, making the claim trivial there.

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

Concavity of log⁡det⁡\log\detlogdet

Concavity of $\log\det$