LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)

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.

Support and pseudoinverse coordinates of a finite singular Gaussian

Statement

Assume the Axiom of Choice. Let $n \geq 1$ , $m \in R^{n}$ , and let $C \in R^{n \times n}$ be symmetric with $v^{T} C v \geq 0$ for every $v \in R^{n}$ . Let $X$ be a random vector with law $N_{n} (m, C)$ , and define $μ_{X} (E) = P (X \in E)$ for Borel $E \subseteq R^{n}$ . Write $Ran (C) = {C v : v \in R^{n}}$ , and put $r = \dim Ran (C)$ . For a Borel probability $μ$ on $R^{n}$ , define its topological support by $supp (μ) = {x : μ (B (x, ε)) > 0 for every ε > 0},$ where $B (x, ε)$ is the open Euclidean ball. If $r > 0$ , there are $U \in R^{n \times r}$ and a symmetric positive-definite $Λ \in R^{r \times r}$ with $U^{T} U = I_{r}$ such that $C = U Λ U^{T}, Ran (C) = Ran (U), C^{†} = U Λ^{- 1} U^{T} .$ Moreover, $X$ has the same law as $m + U Λ^{1 / 2} Z$ , where $Z \sim N_{r} (0, I_{r})$ , and $supp (μ_{X}) = m + Ran (C) .$ Here $C^{†}$ is the unique matrix satisfying $C C^{†} C = C$ , $C^{†} C C^{†} = C^{†}$ , and such that $C C^{†}$ and $C^{†} C$ are symmetric. If $r = 0$ , then $C = 0$ , $X = m$ almost surely, $C^{†} = 0$ , and the support is ${m}$ .

Statement references

A finite Gaussian law permits singular positive-semidefinite covariance and has the corresponding square-root representation.

The Moore–Penrose pseudoinverse is defined by the four Penrose equations.

Facts & Assumptions

Given: AC, a finite-dimensional real inner-product space, a symmetric positive-semidefinite covariance matrix $C$ , a mean vector $m$ , and a supplied law $X \sim N_{n} (m, C)$ .

[A1]

AC is assumed by the multivariate-normal and standard-normal construction interfaces. The Axiom of Choice

[F1]

A finite-dimensional non-negative operator has an orthonormal eigenbasis with non-negative eigenvalues. A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S

[F2]

A finite-dimensional non-negative operator has a unique non-negative square root. A non-negative operator has a unique non-negative square root

[F3]

A multivariate-normal law permits singular covariance and is the law of its mean plus the covariance square root applied to a vector of independent standard-normal coordinates. Multivariate normal law, including singular covariance

[F4]

A positive-definite multivariate-normal covariance gives a Lebesgue density that is strictly positive everywhere. A positive-definite multivariate normal law has its Gaussian density

[F5]

A matrix is a Moore–Penrose pseudoinverse when it satisfies the four Penrose equations, and every finite real matrix has a unique such matrix. The Moore--Penrose pseudoinverse $A^{+}$ as the solution of the four Penrose equations, Every finite real or complex matrix has a unique Moore--Penrose pseudoinverse

Proof

Given: The hypotheses in the Statement.

1.1givenF1algebra

By [F1], choose an orthonormal eigenbasis of $C$ and order it so the positive eigenvalues are $λ_{1}, \dots, λ_{r}$ . Let $U$ have the corresponding eigenvectors as columns and set $Λ = diag (λ_{1}, \dots, λ_{r})$ . The zero eigenspace is the orthogonal complement of these columns, so $C = U Λ U^{T}$ and $Ran (C) = Ran (U)$ . When $r = 0$ , the eigenbasis gives $C = 0$ .

2.1F5step 1.1algebra

If $r > 0$ , set $P = U Λ^{- 1} U^{T}$ . The decomposition in step 1.1 gives $C P = P C = U U^{T}$ , hence $C P C = C$ and $P C P = P$ ; also $C P$ and $P C$ are symmetric. Thus $P$ satisfies all four equations in [F5], so uniqueness gives $P = C^{†}$ . If $r = 0$ , the zero matrix satisfies the four equations for $C = 0$ , and uniqueness gives $C^{†} = 0$ .

2.2A1F2F3step 1.1algebra

Suppose $r > 0$ . By [F2], the square root is $C^{1 / 2} = U Λ^{1 / 2} U^{T}$ . By [F3], $X$ has the law of $m + U Λ^{1 / 2} U^{T} Z_{n}$ for a standard-normal vector $Z_{n}$ . For every $a \in R^{r}$ , the scalar $a^{T} U^{T} Z_{n} = (U a)^{T} Z_{n}$ is centered normal with variance $∥ U a ∥_{2}^{2} = ∥ a ∥_{2}^{2}$ , so $U^{T} Z_{n}$ has law $N_{r} (0, I_{r})$ . Therefore $X$ has the stated representation. When $r = 0$ , [F3] makes $X = m$ almost surely.

3.1F4step 2.2givenconstruct∎

If $r > 0$ , let $x = m + U Λ^{1 / 2} z$ be any point of $m + Ran (C)$ . The continuous map $t \mapsto m + U Λ^{1 / 2} t$ sends $z$ to $x$ , so the preimage of every open ball about $x$ contains an open ball about $z$ . By [F4], $N_{r} (0, I_{r})$ assigns positive measure to every nonempty open ball. The representation in step 2.2 therefore gives positive $μ_{X}$ -mass to every neighborhood of $x$ . Conversely, the law in step 2.2 is concentrated on the finite-dimensional closed affine subspace $m + Ran (C)$ ; every point outside it has a neighborhood of zero mass. Hence the support is exactly that subspace. If $r = 0$ , the point-mass law from step 2.2 has support ${m}$ .

Depends on

Used by

Dependency tree · two levels

38 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

Christian Clason, Regularization of Inverse Problems: Lecture Notes, arXiv:2001.00617v2 (2021) (standard reference, not scraped)
M. Dashti and A. M. Stuart, The Bayesian Approach to Inverse Problems (full lecture notes, arXiv:1302.6989) (standard reference, not scraped)