CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 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 Gaussian MAP, posterior mean, and support-restricted Tikhonov minimizer coincide

Statement

Assume AC and let $n, m \geq 1$ , $m_{0} \in R^{n}$ , $C_{0} \in R^{n \times n}$ symmetric with $v^{T} C_{0} v \geq 0$ for all $v \in R^{n}$ , $A \in R^{m \times n}$ , and $Γ \in R^{m \times m}$ symmetric with $u^{T} Γ u > 0$ for all nonzero $u \in R^{m}$ . Let $X \sim N_{n} (m_{0}, C_{0})$ and $η \sim N_{m} (0, Γ)$ be independent, and observe $Y = A X + η$ . Put $S_{0} = m_{0} + Ran (C_{0})$ and $r = \dim Ran (C_{0})$ . The $r$ -dimensional Euclidean Lebesgue measure on $S_{0}$ is the pushforward of Lebesgue measure on $R^{r}$ under any affine isometry onto $S_{0}$ ; this measure is independent of the chosen orthonormal coordinates. A MAP point means a maximizer of the posterior density with respect to this measure; for $r = 0$ , the unique point of $S_{0}$ is the MAP point. The Moore–Penrose pseudoinverse $C_{0}^{†}$ satisfies $C_{0} C_{0}^{†} C_{0} = C_{0}, C_{0}^{†} C_{0} C_{0}^{†} = C_{0}^{†},$ and $C_{0} C_{0}^{†}$ and $C_{0}^{†} C_{0}$ are symmetric. The optimization below is restricted to $S_{0}$ . Then for every $y \in R^{m}$ , the unique MAP point equals the posterior mean and the unique minimizer over $x \in S_{0}$ of $J_{y} (x) = (A x - y)^{T} Γ^{- 1} (A x - y) + (x - m_{0})^{T} C_{0}^{†} (x - m_{0}) .$ All objects are finite-dimensional; no minimization over points outside the prior support is asserted when $C_{0}$ is singular.

Statement references

The finite Gaussian posterior mean and covariance are given by the displayed conditioning formulas.

A singular Gaussian prior is supported on the mean plus the covariance range, and its pseudoinverse has range coordinates.

The pseudoinverse is characterized by the four Penrose equations.

Facts & Assumptions

Given: AC; the finite linear Gaussian inverse model with $C_{0} ⪰ 0$ , $Γ ≻ 0$ , and the support and MAP conventions in the Statement.

[A1]

AC is inherited from the finite Gaussian posterior and multivariate-normal interfaces. The Axiom of Choice

[F1]

The posterior update is the finite Gaussian law with the stated mean and covariance, defined for every datum. Finite linear Gaussian inverse posterior with singular prior covariance

[F2]

There are orthonormal range coordinates $C_{0} = U Λ U^{T}$ , $C_{0}^{†} = U Λ^{- 1} U^{T}$ , and the prior support is $m_{0} + Ran (U)$ . Support and pseudoinverse coordinates of a finite singular Gaussian

[F3]

The Moore–Penrose pseudoinverse is characterized by the four Penrose equations. The Moore--Penrose pseudoinverse $A^{+}$ as the solution of the four Penrose equations

[F4]

A finite-dimensional non-negative matrix has a unique non-negative square root, and a non-negative self-adjoint matrix has an orthonormal eigenbasis. A non-negative operator has a unique non-negative square root, 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

[F5]

The Tikhonov objective is $∥ D z - b ∥_{2}^{2} + λ ∥ z ∥_{2}^{2}$ for $λ > 0$ . The Tikhonov regularised least-squares objective $∥ A x - b ∥_{2}^{2} + λ ∥ x ∥_{2}^{2}$ for $λ > 0$

[F6]

For this objective the unique minimizer is $(D^{T} D + λ I)^{- 1} D^{T} b$ . For every $λ > 0$ , the Tikhonov objective is strictly convex and has the unique minimiser $(A^{*} A + λ I)^{- 1} A^{*} b$

[F7]

A positive-definite Gaussian law has a density proportional to its positive quadratic exponential. A positive-definite multivariate normal law has its Gaussian density

Proof

Given: The hypotheses in the Statement.

1.1F1F2givenalgebra

If $r = 0$ , [F2] gives $C_{0} = 0$ and $S_{0} = {m_{0}}$ . The posterior is the point mass at $m_{0}$ by [F1], so its mean and unique MAP point are $m_{0}$ . The objective $J_{y}$ has only this admissible point, hence it has the same unique minimizer on $S_{0}$ .

1.2F2F3givenalgebraconstruct

Suppose $r > 0$ . By [F2], choose $U, Λ$ with $C_{0} = U Λ U^{T}$ , $C_{0}^{†} = U Λ^{- 1} U^{T}$ , and write $L = U Λ^{1 / 2}$ . The map $z \mapsto m_{0} + L z$ is a bijection from $R^{r}$ onto $S_{0}$ . For $x = m_{0} + L z$ , $(x - m_{0})^{T} C_{0}^{†} (x - m_{0}) = z^{T} z$ .

2.1F4F5F6step 1.2algebra

Let $W$ be the non-negative square root of $Γ^{- 1}$ . Since $Γ ≻ 0$ , $W$ is symmetric positive definite and $W^{T} W = Γ^{- 1}$ by [F4]. Set $D = W A L$ and $b = W (y - A m_{0})$ . Substituting $x = m_{0} + L z$ into the objective in the Statement gives $J_{y} (m_{0} + L z) = ∥ D z - b ∥_{2}^{2} + ∥ z ∥_{2}^{2}$ . This is the Tikhonov objective in [F5] with $λ = 1$ , so [F6] gives the unique minimizer $\hat{z} = (D^{T} D + I_{r})^{- 1} D^{T} b$ .

3.1A1F1F2F7step 1.2step 2.1algebra∎

By the Gaussian representation in [F2], the prior coordinate $z$ has standard Gaussian density. The likelihood is proportional to $\exp (- \frac{1}{2} ∥ D z - b ∥_{2}^{2})$ by [F7]. Thus the posterior density in $z$ is proportional to $\exp [- \frac{1}{2} (∥ D z - b ∥_{2}^{2} + ∥ z ∥_{2}^{2})]$ . Its precision matrix $H = I_{r} + D^{T} D$ is positive definite, and completing the square gives a Gaussian density with mean $H^{- 1} D^{T} b = \hat{z}$ and covariance $H^{- 1}$ . This density has its unique maximum at its mean. The affine bijection in step 1.2 has constant positive Jacobian in orthonormal coordinates on $S_{0}$ , so its image has the unique MAP point $\hat{x} = m_{0} + L \hat{z}$ . Its posterior mean is also $m_{0} + L \hat{z}$ , and step 2.1 makes this point the unique minimizer of $J_{y}$ on $S_{0}$ .

Depends on

Used by

Dependency tree · two levels

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