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

Log marginal likelihood for a finite Gaussian-process regression model

Statement

Assume AC. Let $X$ be a set, let $f = (f_{t})_{t \in X}$ be a real Gaussian process with mean $m$ and symmetric positive-semidefinite covariance kernel $k$ , and let $X = (x_{i})_{i = 1}^{n} \in X^{n}$ with $n \geq 1$ . For independent observation noise $ε \sim N_{n} (0, R)$ with symmetric positive-semidefinite covariance $R$ , set $Y = f_{X} + ε$ , $m_{X} = (m (x_{i}))$ , $K_{X X} = (k (x_{i}, x_{j}))$ , and $A_{X} = K_{X X} + R$ . Suppose $A_{X}$ is positive definite. Define the log marginal likelihood at $y \in R^{n}$ as the logarithm of the Lebesgue density of $Y$ at $y$ under this prior-predictive model. Then $Y \sim N_{n} (m_{X}, A_{X})$ and $\log p (y ∣ X, m, k, R) = - \frac{1}{2} (y - m_{X})^{T} A_{X}^{- 1} (y - m_{X}) - \frac{1}{2} \log \det (A_{X}) - \frac{n}{2} \log (2 π) .$ This formula is asserted only for the nonsingular observed-covariance case $A_{X} ≻ 0$ .

Statement references

Rasmussen and Williams, GPML, Chapter 2 §§2.2–2.3, equations (2.28)–(2.30), printed pp. 18–20

Bishop, PRML, §6.4.2, equations (6.61)–(6.62), printed pp. 306–307

Facts & Assumptions

Given: AC; the finite Gaussian-process observation model, a nonempty evaluation list $X$ , independent noise $ε \sim N_{n} (0, R)$ with $R ⪰ 0$ , and $A_{X} = K_{X X} + R ≻ 0$ .

[A1]

The Axiom of Choice states that every family of nonempty sets has a choice function. The Axiom of Choice

[F1]

The finite observation model defines $Y = f_{X} + ε$ , $m_{X}$ , $K_{X X}$ , and $A_{X} = K_{X X} + R$ , with $ε$ independent of $f$ . Finite Gaussian-process regression observation model

[F2]

A Gaussian process has multivariate-normal finite evaluation vectors, including singular covariance matrices. Gaussian process

[F3]

Under AC, a multivariate-normal law is characterized by its normal scalar projections and allows symmetric positive-semidefinite covariance. Multivariate normal law, including singular covariance

[F4]

A finite stack of independent Gaussian vectors is jointly multivariate normal with block-diagonal covariance. A finite stack of independent Gaussian vectors is jointly Gaussian

[F5]

Under AC, $N_{n} (a, Σ)$ with $Σ ≻ 0$ has Lebesgue density $(2 π)^{- n / 2} \det (Σ)^{- 1 / 2} \exp ⁣ (- \frac{1}{2} (x - a)^{T} Σ^{- 1} (x - a))$ . A positive-definite multivariate normal law has its Gaussian density

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F3F4givenalgebra

By [F1] and [F2], $f_{X} \sim N_{n} (m_{X}, K_{X X})$ . The independent noise has law $N_{n} (0, R)$ , so [F4] makes $U = (f_{X}, ε)$ jointly Gaussian with mean $(m_{X}, 0)$ and block-diagonal covariance $diag (K_{X X}, R)$ . For any $a \in R^{n}$ , $a^{T} Y = (a^{T}, a^{T}) U$ is a normal scalar projection by [F3]; its mean is $a^{T} m_{X}$ and its variance is $a^{T} (K_{X X} + R) a$ . Thus the projection definition [F3] gives $Y \sim N_{n} (m_{X}, A_{X})$ .

2.1A1F5givenstep 1.1algebra∎

Apply [F5] to the law from step 1.1, using the hypothesis $A_{X} ≻ 0$ . Its density at $y$ is $(2 π)^{- n / 2} \det (A_{X})^{- 1 / 2} \exp ⁣ (- \frac{1}{2} (y - m_{X})^{T} A_{X}^{- 1} (y - m_{X}))$ . This is positive, so taking its logarithm and expanding products gives the displayed formula.

Depends on

Used by

Computational costs and limits of finite Gaussian-process regression Remark

Dependency tree · two levels

33 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

Carl Edward Rasmussen and Christopher K. I. Williams, Gaussian Processes for Machine Learning, Chapter 2 §§2.2–2.3 (standard reference, not scraped)
Christopher M. Bishop, Pattern Recognition and Machine Learning, §6.4.2 (standard reference, not scraped)