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

Finite Gaussian-process posterior and predictive laws

Statement

Assume AC and let $f = (f_{t})_{t \in T}$ be a real Gaussian process with mean $m$ and covariance kernel $k$ ; when $m$ and $k$ are specified as a prior, the canonical cylinder-space process exists by A mean and positive-semidefinite kernel define a Gaussian process. Let $X = (x_{1}, \dots, x_{n}) \in T^{n}$ and $X_{*} = (x_{1}^{*}, \dots, x_{p}^{*}) \in T^{p}$ , where $n, p \geq 1$ and repeated indices are allowed. Write $f_{X} = (f_{x_{i}})_{i = 1}^{n}$ , $f_{X_{*}} = (f_{x_{j}^{*}})_{j = 1}^{p}$ , $m_{X} = (m (x_{i}))_{i = 1}^{n}$ , and $m_{*} = (m (x_{j}^{*}))_{j = 1}^{p}$ . For finite lists $A = (a_{i})$ and $B = (b_{j})$ , define $K_{A B} = (k (a_{i}, b_{j}))_{i, j}$ .

Let $ϵ \sim N_{n} (0, R)$ be independent of the process, where $R$ is symmetric positive semidefinite, and set $Y = f_{X} + ϵ$ . Assume the observed covariance $C = K_{X X} + R$ is positive definite. Then a version of the conditional law of $f_{X_{*}}$ given $Y = y$ is, for every $y \in R^{n}$ , $N_{p} ⁣ (m_{*} + K_{* X} C^{- 1} (y - m_{X}), K_{* *} - K_{* X} C^{- 1} K_{X *}) .$ The displayed conditional covariance is positive semidefinite and may be singular; $K_{X X}$ and $K_{* *}$ may also be singular. If a prediction-noise vector $η_{*} \sim N_{p} (0, R_{*})$ jointly independent of the process and $ϵ$ is added to $f_{X_{*}}$ , with $R_{*}$ symmetric positive semidefinite, the conditional mean is unchanged and $R_{*}$ is added to the conditional covariance. The displayed kernel is a version defined at every $y$ ; conditional-law versions are determined only $P_{Y}$ -almost surely.

For computation, the occurrences of $C^{- 1} v$ mean solving $C u = v$ . Since $C$ is positive definite, its Cholesky factorization and forward/back substitution evaluate these solves without forming $C^{- 1}$ .

Facts & Assumptions

Given: AC; the Gaussian process and finite lists in the Statement; an independent Gaussian observation-noise vector with covariance $R ⪰ 0$ ; $C = K_{X X} + R ≻ 0$ ; and, for the noisy-prediction clause, an independent Gaussian vector with covariance $R_{*} ⪰ 0$ .

[A1]

The Axiom of Choice is part of the finite Gaussian-law and conditional normal interfaces used below. The Axiom of Choice

[F1]

A Gaussian process has multivariate-normal finite evaluation vectors, including repeated indices and singular covariances. Gaussian process

[F2]

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

[F3]

A finite independent stack of possibly singular Gaussian vectors is jointly multivariate normal. A finite stack of independent Gaussian vectors is jointly Gaussian

[F4]

A multivariate normal law is characterized by its normal scalar projections, and singular positive-semidefinite covariance is allowed. Multivariate normal law, including singular covariance

[F5]

For a jointly Gaussian pair with observed covariance $B ≻ 0$ , the conditional law has mean $a + C B^{- 1} (y - b)$ and covariance $A - C B^{- 1} C^{T}$ , which is positive semidefinite and may be singular. Conditional law of a jointly Gaussian block with positive-definite observed covariance

[F6]

A real symmetric positive-definite matrix has a unique Cholesky factorization $C = 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

[F7]

Forward and backward substitution are the recursive procedures for triangular systems with nonzero diagonal. Forward and backward substitution for triangular linear systems

[F8]

Forward and backward substitution return the unique solutions of their triangular systems. Forward and backward substitution are correct, unique, and quadratic in scalar operations

Proof

Given: The assumptions in the Statement.

1.1A1F1given

By [F1], the concatenated finite evaluation vector $U = (f_{X_{*}}, f_{X})$ is multivariate normal with mean $(m_{*}, m_{X})$ and covariance $(\begin{array}{cc} K_{* *} & K_{* X} \\ K_{X *} & K_{X X} \end{array}) .$ This remains valid when either list has repetitions.

2.1A1F2F3givenstep 1.1

The vector $ϵ$ is multivariate normal with mean zero and covariance $R$ . Each coordinate of $U$ is a measurable function of the process coordinates, so $σ (U) \subseteq σ (f)$ . By [F2] and the independence hypothesis, $σ (ϵ)$ is independent of $σ (f)$ and hence of $σ (U)$ . Applying [F3] to $U$ and $ϵ$ shows that $Z = (f_{X_{*}}, f_{X}, ϵ)$ is jointly multivariate normal with block-diagonal covariance between $U$ and $ϵ$ .

3.1F2F4step 2.1algebra

Apply the linear map $(u, v, e) \mapsto (u, v + e)$ to $Z$ . Every scalar projection of the result is a scalar projection of $Z$ , hence is normal by [F4]; its mean is $(m_{*}, m_{X})$ . The Gaussian vectors have finite second moments, so independence and $E ϵ = 0$ give $Cov (f_{X_{*}}, ϵ) = 0$ and $Cov (Y) = K_{X X} + R = C$ . By step 1.1, $Cov (f_{X_{*}}, f_{X}) = K_{* X}$ , so $(f_{X_{*}}, Y)$ is jointly Gaussian with covariance $(\begin{array}{cc} K_{* *} & K_{* X} \\ K_{X *} & C \end{array}) .$

4.1A1F5givenstep 3.1

Apply [F5] with $A = K_{* *}$ , cross-covariance $K_{* X}$ , and observed covariance $B = C ≻ 0$ . The result is a probability-kernel version for every $y$ , with the displayed mean and Schur-complement covariance; [F5] also proves this covariance is positive semidefinite even if singular.

4.2A1F3F4F5givenstep 3.1algebra

If $η_{*}$ is present, it is jointly independent of the process and $ϵ$ by hypothesis. By [F3], the stack $(f_{X_{*}}, f_{X}, ϵ, η_{*})$ is jointly Gaussian. The linear map $(u, v, e, h) \mapsto (u + h, v + e)$ has mean $(m_{*}, m_{X})$ , cross-covariance $K_{* X}$ , observed covariance $C$ , and prediction covariance $K_{* *} + R_{*}$ . Applying [F5] to this pair gives the stated noisy-prediction law.

5.1F6F7F8algebra∎

By [F6], write $C = L L^{T}$ . For any right-hand side $b$ , solve $L z = b$ by forward substitution and $L^{T} u = z$ by backward substitution; [F8] gives both unique solutions. Then $C u = L (L^{T} u) = L z = b$ , so $u = C^{- 1} b$ . Applying this to $b = y - m_{X}$ and, column by column, to $K_{X *}$ evaluates both formula terms without forming the inverse.

Remarks

Only the observed covariance $C$ is inverted, and its positive-definiteness is an explicit hypothesis. The result makes no pseudoinverse claim when $C$ is singular. The conditional formula specifies a valid all- $y$ version, while another regular conditional version may differ on a $P_{Y}$ -null set.

Source notes

Rasmussen–Williams derive the finite Gaussian-regression mean and covariance for zero-mean priors and independent homoscedastic noise, and describe the multiple-test-vector case. The local proof extends the calculation to nonzero means, general positive-semidefinite noise covariance, singular prior and predictive blocks, and the exact positive-definite observed-block hypothesis. The conditional-normal supplier provides the complete probability-kernel argument.

Depends on

Used by

Dependency tree · two levels

43 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

A. W. van der Vaart and J. H. van Zanten, Reproducing kernel Hilbert spaces of Gaussian priors (2008) (standard reference, not scraped)
Carl Edward Rasmussen and Christopher K. I. Williams, Gaussian Processes for Machine Learning (MIT Press, 2006), Chapter 2 (standard reference, not scraped)