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

Finite linear Gaussian inverse posterior with singular prior covariance

Statement

Assume AC. Let $n, m \geq 1$ , $m_{0} \in R^{n}$ , and let $C_{0} \in R^{n \times n}$ be symmetric with $v^{T} C_{0} v \geq 0$ for every $v \in R^{n}$ . Let $A \in R^{m \times n}$ and let $Γ \in R^{m \times m}$ be symmetric positive definite, meaning $u^{T} Γ u > 0$ for every nonzero $u \in R^{m}$ . Suppose $X$ and $η$ are independent random vectors with laws $X \sim N_{n} (m_{0}, C_{0})$ and $η \sim N_{m} (0, Γ)$ , and set $Y = A X + η$ . Define $μ_{0} (E) = P (X \in E)$ for Borel $E \subseteq R^{n}$ , and set $S = A C_{0} A^{T} + Γ$ . Then $S$ is positive definite. For each $y \in R^{m}$ , define $Φ_{y} (x) = \frac{1}{2} (y - A x)^{T} Γ^{- 1} (y - A x), Z (y) = \int_{R^{n}} e^{- Φ_{y} (x)} μ_{0} (d x) .$ For every $y$ , $0 < Z (y) < \infty$ , so the normalized potential update $Π^{y} (E) = \frac{\int_{E} e^{- Φ_{y} (x)} μ_{0} (d x)}{Z (y)} (E \in B (R^{n}))$ is a probability measure and equals the conditional-law version obtained by conditioning the observation model at $y$ . Its Gaussian formula, defined for every $y$ , is $N_{n} ⁣ (m_{0} + C_{0} A^{T} S^{- 1} (y - A m_{0}), C_{0} - C_{0} A^{T} S^{- 1} A C_{0}) .$ Let $P_{Y} (B) = P (Y \in B)$ for Borel $B \subseteq R^{m}$ . Conditional-law versions are unique only $P_{Y}$ -almost surely. The displayed mean and covariance formulas invert only $S$ , not $C_{0}$ ; $C_{0}$ and the posterior covariance may be singular. The prior support is $m_{0} + Ran (C_{0})$ .

Statement references

A positive finite evidence defines the normalized potential update, and the dominated version convention identifies it as a conditional law.

Finite Gaussian conditioning permits singular prior and predictive covariance blocks when the observed covariance is positive definite.

For a singular finite Gaussian prior, the affine support is the mean plus the covariance range.

Facts & Assumptions

Given: AC; a finite-dimensional Gaussian prior $N_{n} (m_{0}, C_{0})$ with $C_{0} ⪰ 0$ ; independent Gaussian observation noise $N_{m} (0, Γ)$ with $Γ ≻ 0$ ; and the linear observation map $A$ .

[A1]

AC is assumed by the repository's multivariate-normal, Gaussian-process, and finite Gaussian conditioning interfaces. The Axiom of Choice

[F1]

A finite Gaussian law is characterized by its Gaussian scalar projections, permits singular covariance, and has the covariance-square-root representation. Multivariate normal law, including singular covariance

[F2]

The prior is supported on $m_{0} + Ran (C_{0})$ and admits coordinates $C_{0} = U Λ U^{T}$ with a standard Gaussian vector on that range. Support and pseudoinverse coordinates of a finite singular Gaussian

[F3]

A real process is Gaussian when all its finite linear combinations are normal. Gaussian process

[F4]

Independence of random elements is independence of their generated sigma-algebras. Independent random elements

[F5]

Measurable functions of independent random elements remain independent. Measurable coordinatewise functions preserve independence

[F6]

For a finite Gaussian process with independent Gaussian observation noise, if the observed covariance is positive definite, the conditional law of the test vector is the Gaussian with mean $m_{*} + K_{* X} (K_{X X} + R)^{- 1} (y - m_{X})$ and covariance $K_{* *} - K_{* X} (K_{X X} + R)^{- 1} K_{X *}$ , defined for every $y$ even when the prior or conditional covariance is singular. Finite Gaussian-process posterior and predictive laws

[F7]

A positive-definite Gaussian observation-noise covariance has the Lebesgue density proportional to $\exp (- \frac{1}{2} z^{T} Γ^{- 1} z)$ , which is strictly positive everywhere. A positive-definite multivariate normal law has its Gaussian density

[F8]

The inverse-problem potential update is the prior reweighted by $e^{- Φ_{y}}$ and normalized by its evidence when that evidence is positive and finite. Misfit evidence and the potential posterior law

[F9]

A finite continuous potential with lower envelope $0$ under a proper prior on a separable Banach space has positive finite evidence at every datum. Function-space posterior propriety from a common lower envelope

Proof

Given: The hypotheses in the Statement.

1.1givenalgebra

For $v \in R^{m} ∖ {0}$ , $v^{T} S v = (A^{T} v)^{T} C_{0} (A^{T} v) + v^{T} Γ v > 0$ , since the first term is nonnegative and the second is positive. Thus $S ≻ 0$ and $S^{- 1}$ exists.

1.2A1F1F3givenconstructalgebra

Let $T$ be the finite index set with state indices $s_{1}, \dots, s_{n}$ and observation indices $o_{1}, \dots, o_{m}$ . Define $f_{s_{i}} = X_{i}$ and $f_{o_{j}} = (A X)_{j}$ . Every finite linear combination of these coordinates is a linear projection of $X$ , so it is normal by [F1] and $f$ is a Gaussian process by [F3]. Its covariance blocks are $K_{S S} = C_{0}$ , $K_{S O} = C_{0} A^{T}$ , and $K_{O O} = A C_{0} A^{T}$ .

1.3F7F8F9givenalgebra

For each fixed $y$ , $Φ_{y}$ is finite, continuous, and nonnegative on $R^{n}$ , and $(x, y) \mapsto Φ_{y} (x)$ is jointly continuous. The prior $μ_{0}$ is a probability on the separable Banach space $R^{n}$ , and the envelope $M_{1} (r) = 0$ satisfies $\int e^{M_{1} (∥ x ∥_{2})} μ_{0} (d x) = 1$ . Therefore [F9] gives $0 < Z (y) < \infty$ for every $y$ , and [F8] defines $Π^{y}$ . The likelihood density from [F7] is a positive constant independent of $x$ times $e^{- Φ_{y} (x)}$ ; its constant cancels in the normalized update.

2.1A1F4F5F6givenstep 1.1step 1.2algebra

The vector $f$ is a measurable function of $X$ , so [F4] and [F5] make $η$ independent of $f$ . The observed covariance is $K_{O O} + Γ = S ≻ 0$ by step 1.1. Applying [F6] with test list $S$ and observation list $O$ gives the displayed Gaussian conditional-law version for every $y$ .

2.2F2F7F8step 1.3given

Suppose $r = rank (C_{0}) > 0$ . By [F2], write $C_{0} = U Λ U^{T}$ and represent $X$ as $m_{0} + L ξ$ , where $L = U Λ^{1 / 2}$ and $ξ \sim N_{r} (0, I_{r})$ . Put $B = A L$ and $d = y - A m_{0}$ . By the pushforward formula for $μ_{0}$ and the likelihood in [F7], the density of the normalized update in these coordinates is proportional, for every $y$ , to $\exp ⁣ (- \frac{1}{2} [ξ^{T} ξ + (d - B ξ)^{T} Γ^{- 1} (d - B ξ)]) .$ This is a pointwise fixed-data calculation; it does not replace the all-data version convention in step 1.3.

3.1F2F7step 2.2algebra

Set $Q = I_{r} + B^{T} Γ^{- 1} B$ and $h = B^{T} Γ^{- 1} d$ . Then $Q ≻ 0$ , and expansion gives $ξ^{T} ξ + (d - B ξ)^{T} Γ^{- 1} (d - B ξ) = (ξ - Q^{- 1} h)^{T} Q (ξ - Q^{- 1} h) + d^{T} Γ^{- 1} d - h^{T} Q^{- 1} h .$ Thus the update in step 2.2 is the Gaussian law of $ξ$ with mean $Q^{- 1} h$ and covariance $Q^{- 1}$ , so the update of $X = m_{0} + L ξ$ has mean $m_{0} + L Q^{- 1} B^{T} Γ^{- 1} d$ and covariance $L Q^{- 1} L^{T}$ .

4.1step 1.1step 3.1algebra

Since $S = Γ + B B^{T}$ , multiplication gives $Q B^{T} = B^{T} Γ^{- 1} S$ , hence $Q^{- 1} B^{T} Γ^{- 1} = B^{T} S^{- 1}$ . Also $Q (I_{r} - B^{T} S^{- 1} B) = Q - Q B^{T} S^{- 1} B = I_{r}$ , so $Q^{- 1} = I_{r} - B^{T} S^{- 1} B$ . Substituting these identities into step 3.1 yields $m_{0} + L Q^{- 1} B^{T} Γ^{- 1} d = m_{0} + C_{0} A^{T} S^{- 1} d$ and $L Q^{- 1} L^{T} = C_{0} - C_{0} A^{T} S^{- 1} A C_{0} .$ These are exactly the mean and covariance in the Statement.

5.1F2F7F8step 2.1step 1.3algebra∎

If $r = 0$ , [F2] gives $C_{0} = 0$ and $X = m_{0}$ almost surely. Reweighting a point mass by the positive likelihood leaves that point mass, while the displayed formulas reduce to mean $m_{0}$ and covariance $0$ . This also matches the conditional version from step 2.1 and proves the rank-zero boundary. Thus the fixed-data update and the stated all-data conditional version have the displayed law in every rank case.

Depends on

Used by

Dependency tree · two levels

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