ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generated

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.

An iid Gaussian cylinder process is not an ℓ²-valued prior

Example

Assume AC.

Let $T = N$ , $m (i) = 0$ , and $k (i, j) = 1_{{i = j}}$ . The cylinder Gaussian process with this mean and kernel has independent $N (0, 1)$ coordinates, but its coordinate sequence is almost surely not in $ℓ^{2}$ . Thus its cylinder law is not a tight Borel prior on $ℓ^{2}$ .

Facts & Assumptions

[F1]

Under AC, a mean function and a positive-semidefinite covariance kernel on an arbitrary set define a unique law on the cylinder sigma-algebra with the prescribed finite Gaussian means and covariances (A mean and positive-semidefinite kernel define a Gaussian process).

[F2]

The standard normal assigns a probability $q = P (∣ Z ∣ > 1) > 0$ to ${∣ Z ∣ > 1}$ , and finite independent standard-normal coordinates have product Gaussian law (Standard normal and normal laws, Multivariate normal law, including singular covariance).

[F3]

Probabilities are continuous from above for decreasing events (Continuity from above when one set has finite measure).

[F4]

Probability is countably subadditive on sequences of measurable sets (Finite and countable subadditivity of measures).

[F5]

Finite-coordinate cylinders form a generating pi-system: intersections are cylinders on the union of the finite coordinate sets. For two probability laws agreeing on these cylinders, the constant exhaustion by the full space has equal finite mass one, so the measure-uniqueness theorem gives equality on the cylinder sigma-algebra (Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system).

[F6]

Under AC, the characteristic function $u \mapsto \exp (i u^{T} a - u^{T} Σ u / 2)$ uniquely determines $N_{d} (a, Σ)$ , including singular covariance (Characteristic function of a multivariate normal law).

Verification

Given: AC, $T = N$ , mean $m (i) = 0$ , covariance $k (i, j) = 1_{{i = j}}$ , and the resulting cylinder law with coordinate maps $(Z_{k})_{k \in N}$ .

1.1F1F2F6givenalgebra

For any finite list of indices $t_{i}$ and real coefficients $a_{i}$ , $\sum_{i, j} a_{i} a_{j} k (t_{i}, t_{j}) = \sum_{t} (\sum_{i : t_{i} = t} a_{i})^{2} \geq 0$ , so $k$ is positive semidefinite. By [F1], its zero-mean cylinder law has marginal $N_{d} (0, I_{d})$ on every set of $d$ distinct coordinates. The independent standard-normal vector in [F2] also has law $N_{d} (0, I_{d})$ . Their characteristic functions agree by [F6], whose uniqueness assertion identifies the two laws. Thus every finite family of distinct coordinates is independent and standard normal.

2.1F2F3F4step 1.1algebra

Fix $N$ . For $M \geq N$ , finite-coordinate independence gives $P (∣ Z_{k} ∣ \leq 1 for all N \leq k \leq M) = (1 - q)^{M - N + 1}$ . These events decrease as $M \to \infty$ , so [F3] shows $P (∣ Z_{k} ∣ \leq 1 for every k \geq N) = 0$ . The event that only finitely many $∣ Z_{k} ∣$ exceed $1$ is the countable union over $N$ of these null events; [F4] makes that union null, so almost surely infinitely many coordinates satisfy $∣ Z_{k} ∣ > 1$ .

3.1F5step 2.1algebracontradiction∎

Infinitely many terms of $\sum_{k} Z_{k}^{2}$ exceed $1$ , hence the sum diverges almost surely. The set $ℓ^{2} \subset R^{N}$ is cylinder-measurable because it equals $⋃_{m \geq 1} ⋂_{N \geq 1} {\sum_{k \leq N} x_{k}^{2} \leq m}$ ; its cylinder probability is therefore zero by step 2.1. If an $ℓ^{2}$ -valued Borel random element had these finite-coordinate laws, its coordinate map into $R^{N}$ would be measurable for the cylinder sigma-algebra, so its pushforward would agree with the given cylinder law on every finite-coordinate cylinder. By [F5], the two probability measures are equal; but the pushforward assigns probability one to $ℓ^{2}$ , contradicting its zero cylinder probability. Thus no Borel $ℓ^{2}$ -valued random element, and in particular no tight Borel $ℓ^{2}$ prior, has these finite-coordinate laws.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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, Rates of contraction of posterior distributions based on Gaussian process priors (2008) (standard reference, not scraped)