TheoremStatement: 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.

Equivalence criterion for D-optimal approximate designs

Statement

Let $X$ be a finite nonempty candidate set, $f : X \to R^{p}$ , and let $ξ^{*}$ be a nonsingular approximate design as in Approximate designs and linear-model optimality criteria. Write $M^{*} = M (ξ^{*})$ and $u^{*} (x) = f (x)^{T} (M^{*})^{- 1} f (x)$ . Then $ξ^{*}$ is D-optimal among nonsingular approximate designs if and only if $u^{*} (x) \leq p$ for every $x \in X$ . Whenever this holds, $u^{*} (x) = p$ for every $x \in supp (ξ^{*})$ . No existence of a nonsingular optimum is asserted.

Facts & Assumptions

Given: A finite nonempty $X$ , $p \geq 1$ , a regression-vector map $f$ , a nonsingular approximate design $ξ^{*}$ , and its matrix $M^{*}$ .

[F1]

Approximate designs and linear-model optimality criteria: $M (ξ) = \sum_{x \in X} ξ_{x} f (x) f (x)^{T}$ for an approximate design $ξ$ .

[F2]

Approximate designs and linear-model optimality criteria: D-optimality maximizes $\log \det M (ξ)$ among nonsingular designs.

[F3]

The log determinant is concave on positive-definite matrices: for positive-definite $A_{0}, A_{1}$ , $\log \det ((1 - t) A_{0} + t A_{1}) \geq (1 - t) \log \det A_{0} + t \log \det A_{1}$ for $0 \leq t \leq 1$ .

[F4]

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

[F5]

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

[F6]

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}$ .

[F7]

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.

[F8]

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$ .

[F9]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t gives $\log^{'} (r) = 1 / r$ for $r > 0$ ; The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ composes it with the determinant differential and affine matrix paths, using the entrywise Euclidean coordinates on real matrix space. Thus, along an affine path $A_{t} = A + t H$ with positive determinant, $(\log \det A_{t})^{'} = tr (A_{t}^{- 1} H)$ by [F4]. Determinant continuity keeps its positive value in the logarithm domain locally at every path point.

Proof

technique · use feasible directional derivatives for necessity and concavity for sufficiency

1.1givenF1choosealgebra

Fix $x \in X$ and let $δ_{x}$ be the design putting weight $1$ at $x$ . For $0 \leq t < 1$ , $ξ_{t} = (1 - t) ξ^{*} + t δ_{x}$ has matrix $M_{t} = (1 - t) M^{*} + t f (x) f (x)^{T}$ , which is positive definite because $M^{*}$ is positive definite and $f (x) f (x)^{T}$ is positive semidefinite.

1.2givenF1F3F4F6F7F8F9choosealgebra

Conversely, suppose $u^{*} (x) \leq p$ for every candidate. Let $η$ be any nonsingular approximate design and put $N = M (η)$ . The segment $M_{s} = (1 - s) M^{*} + s N$ is positive definite; by [F3], $g (s) = \log \det M_{s}$ is concave. By [F4], with its cofactor and adjugate support [F6], [F7], and [F8], and the logarithm-chain rule [F9], and by [F1], $g^{'} (0) = tr ((M^{*})^{- 1} (N - M^{*})) = \sum_{x} η_{x} u^{*} (x) - p \leq 0$ .

2.1givenF2F4F5F6F7F8F9step 1.1choosealgebra

If $ξ^{*}$ is D-optimal, the defining maximum property in [F2] gives $g_{x} (t) = \log \det M_{t} \leq g_{x} (0)$ for $0 \leq t < 1$ , so its right derivative at $0$ is nonpositive. By [F4], with its cofactor and adjugate support [F6], [F7], and [F8], the logarithm-chain rule [F9] gives $g_{x}^{'} (0) = tr ((M^{*})^{- 1} (f (x) f (x)^{T} - M^{*})) = u^{*} (x) - p$ ; the trace of the rank-one term is $f (x)^{T} (M^{*})^{- 1} f (x)$ by the coordinate sum, and $tr (I_{p}) = p$ by [F5]. Thus $u^{*} (x) \leq p$ . Since $x$ was arbitrary, the pointwise bound is necessary.

2.2F3step 1.2algebra

For $0 < s < 1$ , the concavity in step 1.2 gives $g (s) \geq (1 - s) g (0) + s g (1)$ , hence $g (1) - g (0) \leq (g (s) - g (0)) / s$ . Let $s ↓ 0$ ; the right derivative already computed in step 1.2 gives $g (1) - g (0) \leq g^{'} (0) \leq 0$ . Thus $\log \det N \leq \log \det M^{*}$ . Since $η$ was arbitrary among nonsingular designs, $ξ^{*}$ is D-optimal.

3.1F1F5step 1.2algebra∎

Finally, $\sum_{x} ξ_{x}^{*} u^{*} (x) = tr ((M^{*})^{- 1} \sum_{x} ξ_{x}^{*} f (x) f (x)^{T}) = tr (I_{p}) = p$ by [F1] and [F5]. Each term is at most $p$ by the bound assumed in step 1.2, so every term with $ξ_{x}^{*} > 0$ equals $p$ . This proves equality on the support and completes both directions.

Depends on

Used by

Dependency tree · two levels

44 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 and 7.5 (standard reference, not scraped)