TheoremStatement: 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 positive-definite multivariate normal law has its Gaussian density

Statement

Assume AC. Let $d \geq 1$ , $m \in R^{d}$ , and let $Σ$ be a real symmetric positive-definite $d \times d$ matrix. If $X \sim N_{d} (m, Σ)$ , then its law has Lebesgue density $f_{m, Σ} (x) = (2 π)^{- d / 2} \det (Σ)^{- 1 / 2} \exp ⁣ (- \frac{1}{2} (x - m)^{T} Σ^{- 1} (x - m)), x \in R^{d} .$

Facts & Assumptions

Given: AC, a finite dimension $d \geq 1$ , a mean vector $m$ , and a positive-definite covariance matrix $Σ$ .

[F1]

The standard normal law has density $(2 π)^{- 1 / 2} e^{- z^{2} / 2}$ , and the multivariate-normal construction permits singular covariance. Standard normal and normal laws, Multivariate normal law, including singular covariance.

[F2]

Finite independent random elements have product joint law. Independent random elements have product joint law.

[F3]

In finite Euclidean dimension, product Lebesgue measure agrees with Euclidean Lebesgue measure on Borel sets; nonnegative product integrals obey Tonelli. 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.

[F4]

Under countable choice, a $C^{1}$ diffeomorphism satisfies the change-of-variables formula for every nonnegative Lebesgue-measurable integrand; continuous maps have Borel preimages of Borel sets. A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions, A continuous map has Borel preimages of Borel sets.

[F5]

Positive-definite $Σ$ has a Cholesky factorization $Σ = L L^{T}$ with $L$ lower triangular and positive diagonal. A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique.

[F6]

Characteristic functions of finite independent sums and affine images follow the stated product and affine rules. Characteristic functions under affine maps and independent sums.

[F7]

Scalar normal characteristic functions determine their laws. Characteristic function of a normal law, Uniqueness of a law from its characteristic function.

[F8]

A multivariate-normal law is specified by its scalar projection laws and is uniquely determined by its multivariate characteristic function. Multivariate normal law, including singular covariance, Characteristic function of a multivariate normal law.

[F9]

The determinant is multiplicative, invariant under transpose, and equals the product of diagonal entries for triangular matrices. For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ , The determinant of a triangular matrix is the product of its diagonal entries.

[A1]

AC holds; the cited bridge supplies countable and dependent choice (CC and DC), as defined by The Axiom of Countable Choice ( ${A C}_{ω}$ ) and The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, for the Gaussian construction and linear change-of-variables theorem. The Axiom of Choice, AC supplies countable selections and prescribed serial paths.

Proof

Given: The hypotheses in the Statement.

1.1F1F2F3A1

By [A1], take $d$ independent standard-normal coordinates $Z_{1}, \dots, Z_{d}$ . Their joint law is the product of the coordinate laws by [F2]. Thus, using [F1] and [F3], the vector $Z = (Z_{1}, \dots, Z_{d})^{T}$ has Lebesgue density $f_{Z} (z) = (2 π)^{- d / 2} \exp (- z^{T} z / 2) .$

2.1F5F6F7F8step 1.1algebra

Let $Σ = L L^{T}$ be the factorization from [F5]. For any $u \in R^{d}$ , the scalar $u^{T} L Z$ is a finite linear combination of the independent standard normals. By [F6] its characteristic function is $\prod_{k = 1}^{d} \exp ⁣ (- s^{2} (L^{T} u)_{k}^{2} / 2) = \exp ⁣ (- s^{2} u^{T} Σ u / 2),$ so [F7] gives $u^{T} L Z \sim N (0, u^{T} Σ u)$ . Therefore $m + L Z$ has all the projection laws defining $N_{d} (m, Σ)$ , and [F8] identifies its law with that of $X$ .

3.1A1F4F5step 1.1step 2.1

Let $T (z) = m + L z$ . It is a $C^{1}$ diffeomorphism with Jacobian determinant $\det L > 0$ . For any Borel set $E \subseteq R^{d}$ , define the nonnegative Borel function $g (x) = 1_{E} (x) f_{Z} (L^{- 1} (x - m)) / \det L$ . By [F4] and the countable choice supplied by [A1], $\int_{E} f_{Z} (L^{- 1} (x - m)) (\det L)^{- 1} d x = \int_{T^{- 1} (E)} f_{Z} (z) d z = P (T Z \in E) .$ Thus the density in step 2.1 is $f_{Z} (L^{- 1} (x - m)) (\det L)^{- 1}$ . The determinant is positive because $L$ is triangular with positive diagonal.

4.1F9step 1.1step 3.1algebra∎

Since $\det Σ = \det (L L^{T}) = (\det L)^{2}$ by [F9], and $(L^{- 1})^{T} L^{- 1} = Σ^{- 1}$ , substituting the expression for $f_{Z}$ from step 1.1 into step 3.1 gives exactly $f_{m, Σ} (x)$ .

Remarks

Positive definiteness is essential for this Lebesgue-density formula. Singular Gaussian laws remain defined, but are supported on lower-dimensional affine subspaces and are not covered by this theorem.

Depends on

Used by

Dependency tree · two levels

98 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

Fan Li, STA610 Lecture 4: Maximum Likelihood Estimation and Inference for the Hierarchical Normal Model, PDF p. 2 (standard reference, not scraped)
Duchateau, Janssen, and Rowlands, Linear Mixed Models, Chapter 2 §2.4.2 (standard reference, not scraped)