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.

Fejer convolution formula for the lattice periodogram

Statement

Let $d \geq 1$ and let $(Y_{j})_{j \in Z^{d}}$ be real square-integrable random variables with constant mean $μ$ and lag-dependent covariance $c (h) : = Cov (Y_{j + h}, Y_{j}),$ independent of $j$ . Assume the Axiom of Choice and Dependent Choice. Then there is a unique finite positive Radon measure $F$ on the angular torus $T^{d}$ such that $c (h) = \int_{T^{d}} e^{i h \cdot θ} F (d θ), h \in Z^{d} .$ For the periodogram $I_{n}$ of Regular-grid spatial periodogram and smoothed estimator, define the product Fejer kernel $Φ_{n} (x) : = \frac{1}{(2 π)^{d} n^{d}} {∣ \sum_{j \in {0, \dots, n - 1}^{d}} e^{- i j \cdot x} ∣}^{2} = \prod_{r = 1}^{d} \frac{1}{2 π n} {∣ \sum_{a = 0}^{n - 1} e^{- i a x_{r}} ∣}^{2} .$ Then, for every $n \geq 1$ and $λ \in T^{d}$ , $E [I_{n} (λ)] = \int_{T^{d}} Φ_{n} (λ - θ) F (d θ) .$ The kernel is nonnegative and has integral one with respect to product angular Lebesgue measure. The spectral measure and density here belong to the lattice-indexed observations on the dual torus.

Facts & Assumptions

Given: The lattice field, constant mean, covariance convention, and periodogram definition in the Statement; assume AC and DC.

[A1]

The Axiom of Choice: the Axiom of Choice is assumed.

[A2]

The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain: Dependent Choice is assumed.

[F1]

Positive definite functions on an abelian group: a function $c : G \to C$ is positive definite when every finite quadratic form $\sum_{r, s} a_{r} \overline{a_{s}} c (x_{r} - x_{s})$ is nonnegative.

[F2]

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.

[F3]

The Pontryagin dual of the integer lattice is the torus: $\hat{Z^{d}}$ is identified with the product torus by $χ_{θ} (j) = e^{i j \cdot θ}$ .

[F4]

Transport of a lattice spectral measure to torus coordinates: a finite positive Radon measure on $\hat{Z^{d}}$ transports to a finite positive Radon measure on $T^{d}$ while preserving integrals after composition.

[F5]

Regular-grid spatial periodogram and smoothed estimator: for $Λ_{n} = {0, \dots, n - 1}^{d}$ and $N_{n} = n^{d}$ , $I_{n} (λ) = \frac{1}{(2 π)^{d} N_{n}} {∣ \sum_{j \in Λ_{n}} (Y_{j} - μ) e^{- i j \cdot λ} ∣}^{2} .$

[F6]

Moments, variance, and covariance on a probability space: covariance is the expected centered product of square-integrable real random variables.

[F7]

Linearity, monotonicity, and the modulus bound for expectation and Cauchy-Schwarz for random variables: expectation is linear on finite integrable sums, and products of square-integrable variables are integrable.

[F8]

The product measure of two sigma-finite measure spaces and Fubini's theorem for L^1 functions on a sigma-finite product: the product angular Lebesgue measure exists and integrals can be evaluated by sections.

[F9]

The integer lattice is a discrete locally compact abelian group: $Z^{d}$ with the discrete topology is Hausdorff, abelian and locally compact, and every function on it is continuous.

[F10]

Integer exponentials are orthogonal for angular Lebesgue measure: under Countable Choice, for every integer $k$ , $\int_{- π}^{π} e^{i k x} d x$ is $2 π$ when $k = 0$ and zero otherwise.

[F11]

AC implies DC implies countable choice: AC implies Countable Choice (through DC).

[F12]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable Choice selects one element from each set in a countable family of nonempty sets.

Proof

Proof technique: prove the covariance sequence is positive definite, apply Bochner on the discrete lattice, then expand the finite Fourier square.

1.1F1F6F7givenalgebra

For any finite lattice points $k_{1}, \dots, k_{m} \in Z^{d}$ and complex coefficients $a_{1}, \dots, a_{m}$ , the finite sum $\sum_{r} a_{r} (Y_{k_{r}} - μ)$ is square-integrable. Expanding its squared modulus, using [F6] and stationarity, gives $\sum_{r, s} a_{r} \overline{a_{s}} c (k_{r} - k_{s}) = E {∣ \sum_{r} a_{r} (Y_{k_{r}} - μ) ∣}^{2} \geq 0.$ Thus $c$ is positive definite by [F1].

1.2A1A2F2F9given

By [F9], $Z^{d}$ is a locally compact Hausdorff abelian group and every function on it is continuous, so $c$ is continuous. By Bochner's theorem [F2], using AC [A1] and DC [A2], there is a unique finite positive Radon measure $F_{0}$ on $\hat{Z^{d}}$ such that $c (h) = \int_{\hat{Z^{d}}} χ (h) F_{0} (d χ) .$

1.3F5F6F7givenalgebra

Expand the finite squared modulus in [F5]. Every product is integrable by [F7], and stationarity gives $E [I_{n} (λ)] = \frac{1}{(2 π)^{d} n^{d}} \sum_{j, k \in Λ_{n}} c (j - k) e^{- i (j - k) \cdot λ} .$

2.1F3F4step 1.2

By [F3] and [F4], transport $F_{0}$ to the unique finite positive Radon measure $F$ on $T^{d}$ . Applying the integral-transport identity [F4] to $χ \mapsto χ (h)$ gives $c (h) = \int_{T^{d}} e^{i h \cdot θ} F (d θ) .$

3.1F5step 2.1step 1.3F7algebra

Substitute the spectral representation from step 2.1 into each summand of step 1.3. Linearity permits moving the finite sum through the integral, and $\sum_{j, k \in Λ_{n}} e^{- i (j - k) \cdot (λ - θ)} = {∣ \sum_{j \in Λ_{n}} e^{- i j \cdot (λ - θ)} ∣}^{2} .$ After dividing by $(2 π)^{d} n^{d}$ this is precisely $E [I_{n} (λ)] = \int_{T^{d}} Φ_{n} (λ - θ) F (d θ) .$

4.1A1F8F10F11F12algebra∎

The displayed kernel factors into nonnegative one-dimensional kernels. For each coordinate, expanding the finite square and applying angular orthogonality [F10] to each integer exponent $a - b$ gives $\int_{- π}^{π} \frac{1}{2 π n} {∣ \sum_{a = 0}^{n - 1} e^{- i a x} ∣}^{2} d x = 1.$ The Countable Choice hypothesis of [F10] follows from AC by [F11] and [A1]. Fubini [F8] for the finite product then gives $\int_{T^{d}} Φ_{n} (x) d x = 1,$ and nonnegativity follows from the squared modulus.

Depends on

Used by

Dependency tree · two levels

106 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), Section 2.3, Definition 2.9 and Lemma 2.10 (standard reference, not scraped)
Oxford Mathematical Institute, Harmonic Analysis lecture notes, characters of Z^d, pp. 17–18 (standard reference, not scraped)