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.

A mean and positive-semidefinite kernel define a Gaussian process

Statement

Assume the Axiom of Choice. Let $T$ be a set, let $m : T \to R$ , and let $k : T \times T \to R$ be symmetric and positive semidefinite, meaning that for every finite list $t_{1}, \dots, t_{n} \in T$ and every $a \in R^{n}$ , $\sum_{i, j = 1}^{n} a_{i} a_{j} k (t_{i}, t_{j}) \geq 0.$ There is a unique probability measure $μ$ on the cylinder sigma-algebra $C_{T}$ of $R^{T}$ whose marginal on each finite-coordinate space $R^{F}$ , for $F \subseteq T$ finite, is the Gaussian law with mean $(m (t))_{t \in F}$ and covariance matrix $(k (s, t))_{s, t \in F}$ . The coordinate process $X_{t} (x) = x (t)$ is Gaussian, has mean function $m$ , and has covariance kernel $k$ . This construction gives only the cylinder-space process; it asserts no sample-path continuity, joint measurability in $(t, x)$ , or tight Banach-valued law.

Facts & Assumptions

Given: AC, a set $T$ , a real-valued mean function $m$ , and a symmetric positive-semidefinite kernel $k$ as stated.

[A1]

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

[F1]

Every finite-dimensional symmetric positive-semidefinite matrix has a unique positive-semidefinite square root. A non-negative operator has a unique non-negative square root

[F2]

Under AC, a finite mean vector and symmetric positive-semidefinite covariance matrix define a possibly singular multivariate normal law; its scalar projections have the corresponding normal laws. Multivariate normal law, including singular covariance

[F3]

Under AC, the characteristic function of $N_{n} (a, Σ)$ is $u \mapsto \exp (i u^{T} a - \frac{1}{2} u^{T} Σ u)$ , and it uniquely determines the law, including when $Σ$ is singular. Characteristic function of a multivariate normal law

[F4]

A family of finite-coordinate probability laws is consistent when each larger law pushes forward under restriction to the smaller law. A consistent family of finite-dimensional distributions

[F5]

The real line with its Borel sigma-algebra is standard Borel. The real line with its Borel sigma-algebra is standard Borel

[F6]

Under AC, a consistent family on arbitrary standard-Borel coordinates has a unique extension to the cylinder sigma-algebra. Assuming the Axiom of Choice, Kolmogorov extension for arbitrary families of standard Borel coordinate spaces

[F7]

On the cylinder sigma-algebra of $R^{T}$ , every coordinate map is measurable. Coordinate maps, finite-coordinate cylinders, and the cylinder $σ$ -algebra

[F8]

A stochastic process is a family of random elements on one probability space; it is Gaussian when every finite linear combination of its coordinates is normally distributed. Stochastic processes and their finite-dimensional distributions Gaussian process

Proof

Given: AC, $T$ , $m$ , and $k$ as in the Statement.

1.1A1F1F2F3givenchooseconstruct

For each nonempty finite $F \subseteq T$ , use AC to choose an enumeration $e_{F} : {1, \dots, n} \to F$ . Set $a_{i} = m (e_{F} (i))$ and $Σ_{i j} = k (e_{F} (i), e_{F} (j))$ . Positive semidefiniteness of $k$ makes $Σ$ positive semidefinite; [F1] supplies its positive square root and [F2] gives the possibly singular law $N_{n} (a, Σ)$ . Push this law to $R^{F}$ by relabelling coordinate $i$ as $e_{F} (i)$ . A different enumeration changes both the mean and covariance by the same permutation; [F3] shows that the relabelled law is unchanged. For $F = \emptyset$ , take the unique law on the singleton empty product.

2.1F3F4step 1.1algebra

If $F \subseteq G$ are finite, the characteristic function of the restriction pushforward of the $G$ -law at $u \in R^{F}$ is $\exp ⁣ (i \sum_{t \in F} u_{t} m (t) - \frac{1}{2} \sum_{s, t \in F} u_{s} u_{t} k (s, t)) .$ This is also the characteristic function of the $F$ -law. By [F3] the two pushforward laws agree, so the family constructed in step 1.1 is consistent in the sense of [F4]. The empty marginal is the singleton law.

3.1A1F5F6step 2.1construct

Each coordinate space $(R, B (R))$ is standard Borel by [F5]. The consistent family from step 2.1 therefore satisfies [F6], which gives a unique probability measure $μ$ on $C_{T}$ with exactly these finite-coordinate marginals.

4.1F2F6F7F8step 3.1algebra

Define $X_{t} (x) = x (t)$ on $(R^{T}, C_{T}, μ)$ . By [F7] these coordinates are measurable, and step 3.1 gives each finite evaluation vector the stated multivariate normal law. Every finite linear combination is a scalar projection of such a vector, hence is normal by [F2]. Thus [F8] makes $X$ a Gaussian process. Its one- and two-coordinate laws give mean $m$ and covariance $k$ , including zero-variance coordinates and singular finite covariance matrices.

5.1F6step 3.1∎

The extension in step 3.1 is unique on $C_{T}$ . It supplies no topology or probability law on a path-continuous or Banach-valued function space, so no such regularity or tightness conclusion is included.

Source notes

van der Vaart–van Zanten define an arbitrary-index Gaussian process through its finite-dimensional Gaussian laws and covariance function. Rasmussen–Williams give the mean/covariance and marginalization convention for Gaussian processes. The finite-coordinate consistency and cylinder extension are proved here from the cited local suppliers; neither source is used to infer path regularity.

Depends on

Used by

Dependency tree · two levels

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