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.

Bochner spectral measure of a continuous stationary field covariance

Statement

Assume the Axiom of Choice and Dependent Choice. Let $G = (R^{d}, +)$ , $d \geq 1$ , with its usual locally compact Hausdorff topology, and let $X = (X (t))_{t \in R^{d}}$ be a real wide-stationary field whose covariance function $C (h) : = Cov (X (s), X (s + h))$ is continuous on $R^{d}$ . There is a unique finite positive Radon measure $μ$ on the Pontryagin dual $\hat{G}$ such that $C (h) = \int_{\hat{G}} χ (h) μ (d χ) (h \in R^{d}),$ and $μ (\hat{G}) = C (0)$ . This is a measure representation and makes no density assertion.

Facts & Assumptions

Given: AC, DC, the usual locally compact Hausdorff additive group $G = R^{d}$ , and a real wide-stationary field on $R^{d}$ with continuous covariance function $C$ .

[A1]

AC says every family of nonempty sets has a choice function. The Axiom of Choice

[A2]

DC supplies an $N$ -indexed chain for every total relation with a prescribed starting point. The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain

[F1]

Random fields, stationarity, covariance, and variograms: wide stationarity means square-integrable coordinates, one constant mean, and $Cov (X (s), X (t)) = C (t - s)$ .

[F2]

Covariance kernels of square-integrable fields are positive semidefinite: every finite real covariance matrix of field coordinates is symmetric and positive semidefinite.

[F3]

Positive definite functions on an abelian group: a function on an abelian group is positive definite when every finite complex quadratic form with conjugated coefficients is a nonnegative real number.

[F4]

The Fourier transform on an LCA group and The Pontryagin dual with the compact-open topology: for a locally compact Hausdorff abelian group $G$ , $\hat{G}$ is its group of continuous circle-valued characters with the compact-open topology, and $χ (h)$ is the evaluation pairing.

[F5]

Bochner's theorem for LCA groups: under AC and DC, every continuous positive-definite function on an LCA group has a unique finite positive Radon representing measure on its Pontryagin dual, with total mass equal to its value at zero.

Axiom use: AC and DC are used in step 3.1 only through the LCA Bochner supplier [F5]. This theorem gives no density, path-continuity, or joint-measurability conclusion.

Proof

Given: AC, DC, $G = R^{d}$ , and the wide-stationary field with continuous covariance in the statement.

1.1F1F2givenalgebra

By wide stationarity [F1], $C (h) = Cov (X (0), X (h))$ and $C (- h) = Cov (X (h), X (0))$ . Covariance symmetry in [F2] gives $C (- h) = C (h)$ . For any finite $h_{1}, \dots, h_{n} \in R^{d}$ , the matrix $M_{i j} : = C (h_{i} - h_{j})$ is the covariance matrix of $(X (h_{1}), \dots, X (h_{n}))$ : indeed, $Cov (X (h_{i}), X (h_{j})) = C (h_{j} - h_{i}) = C (h_{i} - h_{j})$ by evenness. Thus $M$ is real symmetric positive semidefinite by [F2].

2.1F2F3step 1.1algebra

Write any complex coefficients as $z_{i} = u_{i} + i v_{i}$ with $u_{i}, v_{i} \in R$ . Since $M$ is real symmetric, $\sum_{i, j} z_{i} \overline{z_{j}} M_{i j} = \sum_{i, j} u_{i} u_{j} M_{i j} + \sum_{i, j} v_{i} v_{j} M_{i j} \geq 0.$ The imaginary cross terms cancel after interchanging $i$ and $j$ , and each real quadratic form is nonnegative by step 1.1. Therefore $C : G \to C$ is positive definite in the complex-coefficient sense of [F3].

3.1A1A2F4F5givenstep 2.1∎

The given covariance is continuous, so it satisfies the continuity hypothesis of [F5]. The given usual topology on $G$ is locally compact, Hausdorff, and abelian, so [F4] identifies the dual and its evaluation pairing required there. Applying [F5] with the hypotheses [A1] and [A2] gives a unique finite positive Radon measure $μ$ on $\hat{G}$ with the displayed representation and $μ (\hat{G}) = C (0)$ . The zero-covariance case is included: then the mass is zero and uniqueness gives the zero measure.

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

Evgeny Spodarev, Spatial Statistics: Lecture Notes (2024) (standard reference, not scraped)
Evgeny Spodarev, Random Fields I: Lecture Notes (Draft, 2009) (standard reference, not scraped)
Hermine Biermé, Introduction to random fields and scale invariance: Lecture I (2016) (standard reference, not scraped)