LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Kullback–Leibler divergence between nondegenerate centered Gaussian laws

Statement

Let $p \geq 1$ and let $Σ_{0}, Σ_{1}$ be real symmetric positive-definite $p \times p$ matrices. Under the Gaussian law and directional KL conventions of Multivariate normal law, including singular covariance and Kullback–Leibler divergence, $D (N_{p} (0, Σ_{0}) ∥ N_{p} (0, Σ_{1})) = \frac{1}{2} [tr (Σ_{1}^{- 1} Σ_{0}) - p + \log \frac{\det Σ_{1}}{\det Σ_{0}}] .$

Facts & Assumptions

Given: Axiom of Choice, an integer $p \geq 1$ , and positive-definite real symmetric matrices $Σ_{0}, Σ_{1} \in R^{p \times p}$ .

[F1]

Multivariate normal law, including singular covariance: $N_{p} (0, Σ)$ is the law of $Σ^{1 / 2} Z$ for independent standard-normal coordinates and has mean zero and covariance $Σ$ .

[F2]

Standard normal and normal laws: each standard-normal coordinate has density $ϕ_{1} (t) = (2 π)^{- 1 / 2} e^{- t^{2} / 2}$ with respect to one-dimensional Lebesgue measure.

[F3]

Independent random elements have product joint law: independent coordinates have their finite product law.

[F4]

On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, and Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system: coordinate Lebesgue product measure agrees with Euclidean Lebesgue measure; nonnegative product integrals factor; finite measures agreeing on a generating pi-system agree on its sigma-algebra.

[F5]

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis and If $χ_{T} (x) = \prod_{i < n} (x - λ_{i})$ in $F [x]$ , then $\det (T) = \prod_{i < n} λ_{i}$ : determinant is the product of the eigenvalues counted with algebraic multiplicity: a positive-definite symmetric matrix has positive eigenvalues, and its determinant is their product.

[F6]

Borel change of variables from the compact-support formula and Radon uniqueness: for an invertible linear map $T : R^{p} \to R^{p}$ and nonnegative Borel $h$ , $\int h (y) d y = \int h (T x) ∣ \det T ∣ d x$ . Its Countable Choice hypothesis follows from the assumed AC by AC supplies countable selections and prescribed serial paths.

[F7]

Change of variables for expectation: expectation of a measurable function of a random vector is integration against its law when the function is integrable.

[F8]

Kullback–Leibler divergence: for mutually absolutely continuous probability laws with positive Lebesgue densities $f_{0}, f_{1}$ , $D (P_{0} ∥ P_{1}) = \int \log (f_{0} / f_{1}) d P_{0}$ .

[F9]

The trace $tr (A)$ as the sum of the diagonal entries and For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix define trace as the finite diagonal sum and determinant as the finite Leibniz sum.

Proof

1.1F1F2F3F4

Let $Z = (Z_{1}, \dots, Z_{p})$ be the independent standard-normal vector in [F1], and put $ϕ_{p} (z) = \prod_{i = 1}^{p} ϕ_{1} (z_{i}) = (2 π)^{- p / 2} e^{- ∥ z ∥_{2}^{2} / 2}$ . For every Borel rectangle $R = \prod_{i} B_{i}$ , [F3] gives $P (Z \in R) = \prod_{i} \int_{B_{i}} ϕ_{1} (t) d t$ . Tonelli's theorem and the product-Lebesgue identity in [F4] show that this equals $\int_{R} ϕ_{p} (z) d z$ . Rectangles generate the Borel sigma-algebra, so measure uniqueness in [F4] proves that $Z$ has density $ϕ_{p}$ .

2.1F1F5F6step 1.1algebra

Let $Σ$ be positive definite and write $A = Σ^{1 / 2}$ using the real spectral theorem. If $λ_{1}, \dots, λ_{p} > 0$ are the eigenvalues of $Σ$ , then $A$ has eigenvalues $\sqrt{λ_{i}}$ ; [F5] gives $\det A = \sqrt{\det Σ} > 0$ . For a Borel set $E \subseteq R^{p}$ , apply [F6] to $T = A$ and the nonnegative Borel function $g_{E} (x) = 1_{E} (x) ϕ_{p} (A^{- 1} x) ∣ \det A^{- 1} ∣$ . This gives $P (A Z \in E) = \int_{E} ϕ_{p} (A^{- 1} x) ∣ \det A^{- 1} ∣ d x .$ Because $∥ A^{- 1} x ∥_{2}^{2} = x^{T} Σ^{- 1} x$ and $∣ \det A^{- 1} ∣ = (\det Σ)^{- 1 / 2}$ , [F1] yields the positive density $f_{Σ} (x) = (2 π)^{- p / 2} (\det Σ)^{- 1 / 2} \exp ⁣ (- \frac{1}{2} x^{T} Σ^{- 1} x) .$

3.1F1F7F8F9step 2.1algebra

The two densities in step 2.1 are strictly positive. Their log ratio is $\log \frac{f_{Σ_{0}} (x)}{f_{Σ_{1}} (x)} = \frac{1}{2} \log \frac{\det Σ_{1}}{\det Σ_{0}} + \frac{1}{2} x^{T} (Σ_{1}^{- 1} - Σ_{0}^{- 1}) x .$ It is integrable under $N_{p} (0, Σ_{0})$ because it is a constant plus a finite quadratic form and [F1] gives finite second moments. Applying [F7] and [F8], $D (N_{p} (0, Σ_{0}) ∥ N_{p} (0, Σ_{1})) = \frac{1}{2} \log \frac{\det Σ_{1}}{\det Σ_{0}} + \frac{1}{2} tr ((Σ_{1}^{- 1} - Σ_{0}^{- 1}) Σ_{0}) .$ The trace identity follows by expanding the quadratic form as a finite sum and using $E [X_{i} X_{j}] = (Σ_{0})_{i j}$ .

4.1F9step 3.1algebra∎

Finite trace linearity and $Σ_{0}^{- 1} Σ_{0} = I_{p}$ give $tr ((Σ_{1}^{- 1} - Σ_{0}^{- 1}) Σ_{0}) = tr (Σ_{1}^{- 1} Σ_{0}) - p$ . Substitution into step 3.1 proves the formula.

Depends on

Used by

Dependency tree · two levels

108 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

Mengjie Chen, Chao Gao and Zhao Ren, Robust Covariance and Scatter Matrix Estimation under Huber's Contamination Model, Theorems 3.2 and 5.1 proofs (standard reference, not scraped)
Philippe Rigollet, 18.S997 High-Dimensional Statistics Lecture Notes, MIT OpenCourseWare, Chapter 5 (standard reference, not scraped)