LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

A uniform positive eigenvalue floor controls log-determinant error

Statement

Let $p \geq 1$ and let $A, B \in R^{p \times p}$ be symmetric. Put $E = B - A$ and $A_{t} = (1 - t) A + t B$ for $0 \leq t \leq 1$ . Suppose there is $α > 0$ such that $v^{T} A_{t} v \geq α ∥ v ∥_{2}^{2}$ for every $v \in R^{p}$ and every $t \in [0, 1]$ . Then $A_{t}$ is positive definite and $∣ \log \det B - \log \det A ∣ \leq \frac{p ∥ E ∥_{2}}{α} .$

Facts & Assumptions

Given: Symmetric real matrices $A, B \in R^{p \times p}$ , $p \geq 1$ , and the uniform quadratic-form bound $v^{T} A_{t} v \geq α ∥ v ∥_{2}^{2}$ with $α > 0$ for every $t \in [0, 1]$ .

[F1]

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

[F2]

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

[F3]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: for $z > 0$ , $(\log z)^{'} = 1 / z$ .

[F4]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ and The trace $tr (A)$ as the sum of the diagonal entries: trace is the sum of diagonal entries and is invariant under cyclic exchange of conformable products.

[F5]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv|| and Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∥ E v ∥_{2} \leq ∥ E ∥_{2} ∥ v ∥_{2}$ and $∣ u^{T} v ∣ \leq ∥ u ∥_{2} ∥ v ∥_{2}$ .

[F6]

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 $[0, 1]$ and differentiable on $(0, 1)$ has its endpoint increment equal to its derivative at some interior point.

[F7]

For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , The determinant of a triangular matrix is the product of its diagonal entries, and For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix: determinant is multiplicative, a diagonal determinant is the product of its diagonal entries, and $\det I_{p} = 1$ .

[F8]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : along a differentiable matrix path, derivatives of scalar compositions are given by the chain rule.

Proof

technique · direct

1.1givenF1F2F3F7F8algebra

Fix $t \in [0, 1]$ . The matrix $A_{t}$ is symmetric. By [F1], it has an orthonormal eigenbasis; if $q$ is a unit eigenvector with eigenvalue $λ$ , the assumed quadratic-form inequality gives $λ = q^{T} A_{t} q \geq α > 0$ . Thus $A_{t}$ is invertible, and if $A_{t} = Q Λ Q^{T}$ then [F7] gives $\det A_{t} = \det (Q) \det (Λ) \det (Q^{T}) = \det (Q Q^{T}) \prod_{i} λ_{i} = \prod_{i} λ_{i} > 0$ . The determinant is Fréchet differentiable by [F2] and hence continuous, and $\log$ is differentiable, hence continuous, on the positive reals by [F3]. Thus $g (t) = \log \det A_{t}$ is continuous on $[0, 1]$ and differentiable on $(0, 1)$ by [F2], [F3], and [F8].

2.1step 1.1F2F3F8algebra

Since $A_{t} = A + t E$ and is invertible, [F2], [F3], and the chain rule [F8] give $g^{'} (t) = tr (A_{t}^{- 1} E)$ .

2.2step 1.1F1F4F5algebra

Diagonalize $A_{t} = Q Λ Q^{T}$ as in step 1.1. By [F4], $tr (A_{t}^{- 1} E) = tr (Λ^{- 1} Q^{T} E Q) = \sum_{i = 1}^{p} λ_{i}^{- 1} q_{i}^{T} E q_{i}$ . Each $q_{i}$ is unit, so [F5] gives $∣ q_{i}^{T} E q_{i} ∣ \leq ∥ E q_{i} ∥_{2} \leq ∥ E ∥_{2}$ , while $λ_{i} \geq α$ ; hence $∣ g^{'} (t) ∣ \leq p ∥ E ∥_{2} / α$ for every $t$ .

3.1step 2.1step 2.2F6∎

Apply [F6] to $g$ on $[0, 1]$ . For some $c \in (0, 1)$ , $\log \det B - \log \det A = g (1) - g (0) = g^{'} (c)$ , whose absolute value is bounded by step 2.2.

Depends on

Used by

Dependency tree · two levels

70 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)