LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The log determinant is concave on positive-definite matrices

Statement

For $p \geq 1$ , if $A_{0}, A_{1} \in R^{p \times p}$ are symmetric and $v^{T} A_{i} v > 0$ for every nonzero $v \in R^{p}$ and $i \in {0, 1}$ , then for every $t \in [0, 1]$ , $\log \det ((1 - t) A_{0} + t A_{1}) \geq (1 - t) \log \det A_{0} + t \log \det A_{1} .$

Facts & Assumptions

Given: Two real symmetric positive-definite $p \times p$ matrices $A_{0}, A_{1}$ , with $p \geq 1$ .

[F1]

The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products: the standard pairing on $R^{p}$ is $⟨ x, y ⟩ = \sum_{i < p} x_{i} y_{i}$ .

[F2]

In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose: $T$ is self-adjoint if and only if $A = A^{*}$ ; over $R$ , $A^{*}$ is $A^{T}$ .

[F3]

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis: a self-adjoint endomorphism of a finite-dimensional real inner-product space has an orthonormal eigenbasis.

[F4]

The determinant of a triangular matrix is the product of its diagonal entries: the determinant of a triangular matrix is the product of its diagonal entries.

[F5]

For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ : for same-sized square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ .

[F6]

For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix: $\det (A) : = \sum_{σ \in S_{n}} sgn (σ) \prod_{i < n} a_{σ (i), i}$ .

[F7]

Matrix differentials obey the sum rule, product rule, and adjoint rule: $d (A B) = d A B + A d B$ .

[F8]

The determinant differential is $D \det (A) [H] = tr (adj (A) H)$ at every matrix, and Jacobi's formula holds on the invertible locus: on the invertible locus, $D \det (A) [H] = \det (A) tr (A^{- 1} H)$ .

[F9]

On the invertible locus, $D inv (A) [H] = - A^{- 1} H A^{- 1}$ : for invertible $A$ , $D inv (A) [H] = - A^{- 1} H A^{- 1}$ .

[F10]

Trace and Frobenius-linear matrix functionals differentiate by inspection: $D (tr) (A) [H] = tr (H)$ .

[F11]

The trace $tr (A)$ as the sum of the diagonal entries: $tr (A)$ is the sum of the diagonal entries of $A$ .

[F12]

Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring: for a positive-sized square matrix, the cofactors are signed deleted-row-and-column minors and $adj (A) = cof (A)^{T}$ .

[F13]

Laplace expansion computes the determinant along every row and every column over a commutative ring: for a positive-sized square matrix over a commutative ring, determinant expansion along any row or column is the sum of entries times their corresponding cofactors.

[F14]

For every positive-sized square matrix over a commutative ring, $A adj (A) = adj (A) A = \det (A) I$ : for a positive-sized square matrix over a commutative ring, $A adj (A) = adj (A) A = \det (A) I$ .

[F15]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $\log^{'} (x) = 1 / x$ for $x > 0$ . Under the entrywise identification of a real matrix space with a finite-dimensional Euclidean space, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ composes its Fréchet derivatives with the scalar logarithm and an affine matrix path. The path $t \mapsto A_{0} + t H$ has derivative $H$ and zero remainder.

[F16]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : a real function continuous on a closed interval and differentiable on its interior has an increment equal to the interval length times an interior derivative.

Proof

technique · restrict to a line and compute its second derivative

1.1givenF1F2F3algebra

For $t \in [0, 1]$ , put $A_{t} = (1 - t) A_{0} + t A_{1}$ and $H = A_{1} - A_{0}$ . For every nonzero $v$ , $v^{T} A_{t} v = (1 - t) v^{T} A_{0} v + t v^{T} A_{1} v > 0$ , so $A_{t}$ is symmetric positive definite. By [F1] the standard coordinate basis is orthonormal, [F2] makes the symmetric matrix self-adjoint, and [F3] gives an orthonormal eigenbasis. Each eigenvalue $λ_{i} (t)$ is positive because for its unit eigenvector $v_{i}$ , $λ_{i} (t) = v_{i}^{T} A_{t} v_{i} > 0$ .

2.1F4F5F6step 1.1algebra

In that eigenbasis $A_{t} = Q Λ Q^{T}$ with $Q Q^{T} = I_{p}$ and $Λ = diag (λ_{1} (t), \dots, λ_{p} (t))$ . By [F4] and [F5], $\det A_{t} = \det Q \det Λ \det Q^{T} = \det Λ = \prod_{i} λ_{i} (t) > 0$ , since [F5] gives $\det Q \det Q^{T} = \det I_{p}$ and [F6] gives $\det I_{p} = 1$ from the Leibniz formula. Thus $g (t) = \log \det A_{t}$ is real-valued on $[0, 1]$ .

3.1F8F12F13F14F15step 2.1algebra

Since $A_{t}$ is invertible, the determinant differential in [F8] is Jacobi's formula; its cofactor representation and invertible-matrix reduction use [F12], [F13], and [F14]. Because the determinant is differentiable, it is continuous; its positive value at each $A_{t}$ remains positive on a small neighborhood of that path point, so the logarithm's domain condition in [F15] is met, including at $t = 0, 1$ . The logarithm derivative and total chain rule [F15] then give $g^{'} (t) = (\det A_{t})^{- 1} D \det (A_{t}) [H] = tr (A_{t}^{- 1} H)$ .

4.1F7F9F10F15step 3.1algebra

Differentiate this trace along the same line. The product rule [F7], inverse derivative [F9], and trace derivative [F10], composed with the affine path by [F15], give $g^{''} (t) = - tr (A_{t}^{- 1} H A_{t}^{- 1} H)$ .

5.1F3F11step 4.1algebra

Fix $t$ and define the symmetric matrix $S = A_{t}^{- 1 / 2} H A_{t}^{- 1 / 2}$ by diagonalizing $A_{t}$ from [F3] and taking the positive inverse square roots of its eigenvalues. By [F11], $tr (X Y) = tr (Y X)$ because both sides are $\sum_{i, j} X_{i j} Y_{j i}$ with indices interchanged; applying this identity gives $tr (A_{t}^{- 1} H A_{t}^{- 1} H) = tr (S^{2}) = \sum_{i, j} S_{i j}^{2} \geq 0$ . Hence [step 4.1] implies $g^{''} (t) \leq 0$ .

6.1F16step 3.1step 4.1step 5.1givenalgebra∎

The formulas in steps 3.1–4.1 make $g$ differentiable on a neighborhood of $[0, 1]$ and $g^{'}$ differentiable there; in particular each is continuous on the closed subintervals used below. For $0 \leq r < s \leq 1$ , apply [F16] to $g^{'}$ on $[r, s]$ ; step 5.1 gives $g^{'} (s) - g^{'} (r) = g^{''} (c) (s - r) \leq 0$ for some $c \in (r, s)$ . Thus $g^{'}$ is nonincreasing. If $0 < t < 1$ , apply [F16] to $g$ on $[0, t]$ and $[t, 1]$ . The respective slopes equal $g^{'} (a)$ and $g^{'} (b)$ for $a < t < b$ , hence $(g (t) - g (0)) / t \geq (g (1) - g (t)) / (1 - t)$ . Rearrangement gives $g (t) \geq (1 - t) g (0) + t g (1)$ . At $t = 0, 1$ it is equality. This is precisely the stated log-determinant chord inequality.

Depends on

Used by

Dependency tree · two levels

71 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Stephen Boyd and Lieven Vandenberghe, Convex Optimization, §3.1.5 (standard reference, not scraped)