Pipeline-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.

✓ 1 result · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Spectral measures and periodogram bias — Examples

1 · Prerequisites

2 · Summary

An explicit weakly stationary sinusoid has an atomic spectrum, while a causal AR(1) process with $∣ ρ ∣ < 1$ has a continuous spectral density. Their expected periodograms are the corresponding Fejér averages: two shifted kernels in the atomic case and a convolution against a continuous density in the AR(1) case.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

An atomic sinusoid and an AR(1) process have different spectra

Example

Use the finite uniform space $Ω = {- 1, 1}^{2}$ for the sinusoid model, and use the probability space carrying $(ε_{t})_{t \in Z}$ for the AR(1) model. Both models have exact expected-periodogram formulas but different types of spectral measure. The first has two atoms and no spectral density. The second is an AR(1) process whose one-sided innovation series is shown below to converge almost surely and in $L^{2}$ ; this is its causal representation using only current and past innovations, and it has a continuous spectral density. No raw-periodogram limit distribution is asserted.

Facts & Assumptions

Given: A parameter $v > 0$ , a frequency $λ_{s} \in (0, π)$ , a two-sided IID sequence $(ε_{t})_{t \in Z}$ of centered real random variables with variance $σ^{2} \geq 0$ , a parameter $ρ \in (- 1, 1)$ , the Axiom of Choice, and Dependent Choice.

[F1]

Finite probability spaces, outcome weights, events, and event probabilities: on a finite outcome set, uniform weights $1 / ∣ Ω ∣$ define a probability space and event probabilities by finite sums.

[F2]

Expectation of a real random variable on a finite probability space: expectation on a finite probability space is the finite weighted sum.

[F3]

Variance, standard deviation, and covariance on a finite probability space: variance and covariance are expectations of centered squares and products.

[F4]

Identical distribution and IID families: IID means mutual independence and a common marginal law.

[F5]

Expectation factors over a finite product of mutually independent random variables: for a finite independent family of integrable real variables, the expectation of their product is the product of their expectations.

[F6]

Riesz-Fischer completeness of $L^{p}$ for $1 \leq p \leq \infty$ : assuming the Axiom of Choice, $L^{2}$ of a measure space is complete.

[F7]

Cauchy-Schwarz for random variables: if $Y, Z \in L^{2}$ , then $E [∣ Y Z ∣] \leq ∥ Y ∥_{2} ∥ Z ∥_{2}$ .

[F8]

Linearity, monotonicity, and the modulus bound for expectation: expectation is linear on integrable real or complex random variables, and $∣ E [Y] ∣ \leq E [∣ Y ∣]$ .

[F9]

Moments, variance, and covariance on a probability space: the variance of a square-integrable real variable is the expectation of its centered square.

[F10]

Strict and weak stationarity for integer-indexed time series and Autocovariance and sample autocovariance: weak stationarity means finite second moments, a constant mean, and $γ (h) = Cov (X_{t + h}, X_{t})$ independent of $t$ .

[F11]

Spectral measures and the known-mean periodogram: a spectral measure represents the autocovariance by $γ (h) = \int_{T} e^{i h λ} F (d λ)$ .

[F12]

Herglotz spectral measure and the summable-covariance density: under AC and DC, an absolutely summable autocovariance has spectral density $f (λ) = (2 π)^{- 1} \sum_{h} γ (h) e^{- i h λ}$ .

[F13]

Expected periodogram and smoothed spectral-density bias: given a spectral measure $F$ , the known-mean periodogram satisfies $E [I_{n} (λ)] = \int Φ_{n} (λ - θ) F (d θ)$ .

[F14]

Monotone convergence for the integral: the integral of an increasing limit of nonnegative measurable functions is the limit of their integrals.

[F15]

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : $v > 0$ has a positive square root with $(\sqrt{v})^{2} = v$ .

[F16]

The addition formulas for sine and cosine and Parity and the Pythagorean identity for sine and cosine: the sine and cosine addition formulas hold, $\sin (- x) = - \sin x$ , and $\cos (- x) = \cos x$ .

[F17]

For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges and For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ : for real $r$ with $∣ r ∣ < 1$ , $\sum_{j \geq 0} r^{j} = (1 - r)^{- 1}$ and $r^{N} \to 0$ .

[F18]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ and Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive: $e^{i x} = \cos x + i \sin x$ , $∣ e^{i x} ∣ = 1$ , and complex modulus is multiplicative and satisfies the triangle inequality.

[F19]

Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable: sequential limits, limsups and convergence sets of measurable real functions are measurable.

[F20]

The Dirac set function at a point and A Dirac set function is a probability measure: each Dirac set function on the Borel sigma-algebra is a probability measure.

[F21]

The multiplicative unit circle is a compact metrizable topological abelian group and Radon measure on an LCH space: $T$ is compact Hausdorff, and a finite Borel measure is Radon when it is finite on compact sets, outer regular on Borel sets, and inner regular on open sets.

[F22]

$t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle, The zero sets of sine and cosine and the least positive common period 2 pi, and A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included and [F18]: the half-open interval $[- π, π)$ has at most one angular representative of each circle point, and a singleton in $R$ has Lebesgue measure zero under Countable Choice. Thus $d λ ({z}) = 0$ for each $z \in T$ by the definition in [F11].

[F23]

A nonnegative integral over a null set vanishes: a nonnegative measurable function integrates to zero over a measurable null set.

[F24]

The nonnegative Lebesgue integral, The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions, and Every nonnegative measurable function is the increasing limit of simple measurable functions: nonnegative measurable functions have increasing simple approximations, and the integral of a nonnegative simple function is its finite weighted sum.

[F25]

Integrable real and complex functions, and their integrals and Monotonicity and nonnegative homogeneity of the nonnegative integral: a bounded complex Borel function is integrable against a finite measure; the nonnegative integral is monotone.

[F26]

The Pontryagin dual of the discrete integers is the circle, On a discrete domain the compact-open topology is the topology of pointwise convergence, The topology of pointwise convergence on $Y^{X}$ , which is the product topology, and its restriction to $C (X, Y)$ , The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, and A continuous map has Borel preimages of Borel sets: in the angular coordinate, $λ \mapsto e^{i h λ}$ is a continuous evaluation coordinate of the dual character and hence is Borel measurable.

[F27]

A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere: a nonnegative measurable function with integral zero vanishes almost surely on a probability space.

[F28]

$C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ , Integer powers in the complex field, Complex series, absolute convergence, complex power series, and radius of convergence, and The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane: complex arithmetic obeys the field laws; $z^{0} = 1$ and $z^{N + 1} = z^{N} z$ ; a complex series is the limit of its finite partial sums in the metric $d (z, w) = ∣ z - w ∣$ .

[A1]

The Axiom of Choice: every family of nonempty sets has a choice function; it supplies the hypothesis used in [F6] and [F12].

[A2]

The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain: dependent choice supplies the second hypothesis used in [F12].

[A3]

AC implies DC implies countable choice: the assumed Axiom of Choice supplies Countable Choice for the angular Lebesgue measure convention in [F11] and the singleton calculation in [F22].

Verification

Given: The finite sinusoid construction and the IID innovations and parameters above; AC and DC.

1.1F1F2F3F10F15F16givenalgebra

On $Ω = {- 1, 1}^{2}$ with weight $1 / 4$ at each outcome, let $A (a, b) = \sqrt{v} a$ , $B (a, b) = \sqrt{v} b$ , and define the sinusoid model $X_{t}^{(s)} = A \cos (t λ_{s}) + B \sin (t λ_{s})$ . Direct finite sums and [F15] give $E [A] = E [B] = E [A B] = 0$ and $E [A^{2}] = E [B^{2}] = v$ . Thus $E [X_{t}^{(s)}] = 0$ , and [F16] gives $γ_{s} (h) = E [X_{t + h}^{(s)} X_{t}^{(s)}] = v \cos (h λ_{s})$ , independent of $t$ ; this model is weakly stationary by [F1]–[F3], [F10].

1.2F4F5F7F9F17givenalgebra

Let $S_{t, N} : = \sum_{j = 0}^{N} ρ^{j} ε_{t - j}$ . For $M > N$ , independence and centering make all cross terms vanish, so $∥ S_{t, M} - S_{t, N} ∥_{2}^{2} = σ^{2} \sum_{j = N + 1}^{M} ρ^{2 j} ⟶ 0$ by convergence of the real geometric series [F17]. Thus $(S_{t, N})_{N}$ is Cauchy in $L^{2}$ for every $t$ .

1.3F17F18F28algebra

For a complex $z$ with $∣ z ∣ < 1$ , put $C_{N} (z) = \sum_{j = 0}^{N} z^{j}$ . The field and power laws in [F28] give $z C_{N} (z) = \sum_{j = 1}^{N + 1} z^{j}$ , so subtracting the two finite sums yields $(1 - z) C_{N} (z) = 1 - z^{N + 1}$ . Since $∣ 1 ∣ = 1$ , $z \neq 1$ and this factor is invertible. Multiplicativity of modulus in [F18] gives $∣ z^{N + 1} ∣ = ∣ z ∣^{N + 1}$ by finite induction, hence $∣ C_{N} (z) - \frac{1}{1 - z} ∣ = \frac{∣ z ∣^{N + 1}}{∣ 1 - z ∣} ⟶ 0$ by [F17] applied to the real number $∣ z ∣ < 1$ . The metric and partial-sum definition in [F28] therefore give $\sum_{j = 0}^{\infty} z^{j} = (1 - z)^{- 1}$ , and subtracting its first term gives $\sum_{j = 1}^{\infty} z^{j} = z / (1 - z)$ . This proof includes $z = 0$ with $z^{0} = 1$ .

2.1A3F11F14F20F21F22F23F24F25F26step 1.1F18algebra

Put $a = λ_{s}$ , $b = - λ_{s}$ , and $F_{s} = (v / 2) (δ_{a} + δ_{b})$ . By [F20] this is a finite positive Borel measure. It satisfies the Radon regularity clauses [F21]: for a Borel $E \subseteq T$ , the open set $U = T ∖ {x \in {a, b} : x \notin E}$ contains $E$ and has $F_{s} (U) = F_{s} (E)$ ; for an open $O \subseteq T$ , the finite set $K = O \cap {a, b}$ is compact and has $F_{s} (K) = F_{s} (O)$ ; finiteness on compact sets follows from $F_{s} (T) = v$ . For a nonnegative simple $q = \sum_{j} c_{j} 1_{E_{j}}$ with pairwise disjoint measurable $E_{j}$ , its integral is $\int q d F_{s} = \sum_{j} c_{j} (v / 2) (1_{a \in E_{j}} + 1_{b \in E_{j}}) = (v / 2) (q (a) + q (b))$ by [F20] and [F24]. Increasing simple approximation [F24] and monotone convergence [F14] extend this formula to nonnegative measurable $q$ , and decomposition into positive and negative real and imaginary parts extends it to bounded complex Borel $q$ , which is integrable because $F_{s}$ is finite by [F25]. By [F26] the character $λ \mapsto e^{i h λ}$ is Borel, and its modulus is one by [F18], so it is integrable. The evaluation formula now gives $\int_{T} e^{i h λ} F_{s} (d λ) = \frac{v}{2} (e^{i h λ_{s}} + e^{- i h λ_{s}}) = v \cos (h λ_{s}) = γ_{s} (h)$ . Thus $F_{s}$ is a spectral measure. Its two atoms are distinct because $0 < λ_{s} < π$ , and each has mass $v / 2 > 0$ . By [F22]–[F23], any density relative to $d λ$ assigns zero mass to ${a}$ , whereas $F_{s} ({a}) = v / 2$ ; hence $F_{s}$ has no spectral density.

2.2A1A3F6F7F8F14F17F19F25F27step 1.2given

By [F6] and AC, for each $t$ the Cauchy sequence $S_{t, N}$ has an $L^{2}$ limit class represented by a real random variable $X_{t}^{(ρ)}$ . Cauchy–Schwarz [F7] gives $E ∣ ε_{0} ∣ \leq \sqrt{E ε_{0}^{2}} = \sqrt{σ^{2}}$ . Monotone convergence [F14] and the real geometric series [F17] therefore give $E [\sum_{j = 0}^{\infty} ∣ ρ ∣^{j} ∣ ε_{t - j} ∣] = \sum_{j = 0}^{\infty} ∣ ρ ∣^{j} E ∣ ε_{0} ∣ \leq \sqrt{σ^{2}} / (1 - ∣ ρ ∣) < \infty$ . Let $A_{t, N} : = \sum_{j = 0}^{N} ∣ ρ ∣^{j} ∣ ε_{t - j} ∣$ and $A_{t} : = \lim_{N} A_{t, N}$ . For each $M > 0$ , $M 1_{{A_{t} = \infty}} \leq A_{t}$ , so monotonicity [F25] gives $M P (A_{t} = \infty) \leq E A_{t} < \infty$ ; letting $M$ increase shows the absolute series is finite almost surely. Each $A_{t, N}$ and $S_{t, N}$ is measurable with respect to $F_{t} : = σ (ε_{s} : s \leq t)$ , so [F19] makes $A_{t}$ , $C_{t} : = {A_{t} < \infty}$ , and ${lim sup}_{N} S_{t, N}$ measurable. On $C_{t}$ the absolute convergence implies $S_{t, N}$ has a finite limit. Define $Y_{t}$ to be ${lim sup}_{N} S_{t, N}$ on $C_{t}$ and $0$ off $C_{t}$ ; it is $F_{t}$ -measurable and equals the signed series with value $0$ on the null divergence set. Its absolute tail satisfies $E ∣ Y_{t} - S_{t, N} ∣ \leq \sqrt{σ^{2}} ∣ ρ ∣^{N + 1} / (1 - ∣ ρ ∣) \to 0$ . Since $S_{t, N} \to X_{t}^{(ρ)}$ in $L^{2}$ , [F7] applied with the constant $1$ gives $E ∣ S_{t, N} - X_{t}^{(ρ)} ∣ \to 0$ , and hence $E ∣ Y_{t} - X_{t}^{(ρ)} ∣ \leq E ∣ Y_{t} - S_{t, N} ∣ + E ∣ S_{t, N} - X_{t}^{(ρ)} ∣ \to 0$ . Hence $E ∣ Y_{t} - X_{t}^{(ρ)} ∣ = 0$ , and [F27] implies $Y_{t} = X_{t}^{(ρ)}$ almost surely. Choose the causal version $X_{t}^{(ρ)} : = Y_{t}$ . For $N \geq 1$ , $S_{t, N} = ε_{t} + ρ S_{t - 1, N - 1}$ , and $∥ ρ (S_{t - 1, N - 1} - X_{t - 1}^{(ρ)}) ∥_{2} = ∣ ρ ∣ ∥ S_{t - 1, N - 1} - X_{t - 1}^{(ρ)} ∥_{2} \to 0$ , so uniqueness of $L^{2}$ limits gives $X_{t}^{(ρ)} = ε_{t} + ρ X_{t - 1}^{(ρ)}$ in $L^{2}$ . Finite partial sums have mean zero by [F8], and $∣ E X_{t}^{(ρ)} ∣ \leq ∥ X_{t}^{(ρ)} - S_{t, N} ∥_{2} \to 0$ by [F7]; hence $E X_{t}^{(ρ)} = 0$ .

3.1F4F5F7F9F10F17step 2.2algebra

Finite second moments make every $ε_{t}$ integrable by [F7], and its variance is as specified in [F9]. For $h \geq 0$ , the only nonzero terms in $E [S_{t + h, N} S_{t, N}]$ pair the identical innovation indices; by [F4]–[F5], for $N \geq h$ this expectation equals $σ^{2} \sum_{k = 0}^{N - h} ρ^{h + 2 k} ⟶ \frac{σ^{2} ρ^{h}}{1 - ρ^{2}}$ by [F17]. For the passage to the limit, Cauchy–Schwarz [F7] gives $∣ E [S_{a, N} S_{b, N}] - E [X_{a}^{(ρ)} X_{b}^{(ρ)}] ∣ \leq ∥ S_{a, N} - X_{a}^{(ρ)} ∥_{2} ∥ S_{b, N} ∥_{2} + ∥ X_{a}^{(ρ)} ∥_{2} ∥ S_{b, N} - X_{b}^{(ρ)} ∥_{2} \to 0,$ because $∥ S_{b, N} ∥_{2} \leq ∥ X_{b}^{(ρ)} ∥_{2} + ∥ S_{b, N} - X_{b}^{(ρ)} ∥_{2}$ is bounded by the $L^{2}$ convergence. Covariance symmetry for these mean-zero variables follows from commutativity of real products, so the formula for $h \geq 0$ gives $γ_{ρ} (h) = σ^{2} ρ^{∣ h ∣} / (1 - ρ^{2})$ for every integer $h$ , with $ρ^{0} : = 1$ . It is independent of $t$ , so $X^{(ρ)}$ is weakly stationary by [F10].

4.1F12F17F18step 3.1step 1.3A1A2algebra

Since $∣ ρ ∣ < 1$ , the autocovariance is absolutely summable by its formula in step 3.1 and the real geometric series [F17]. Put $z_{-} = ρ e^{- i λ}$ and $z_{+} = ρ e^{i λ}$ . By [F18], both have modulus $∣ ρ ∣ < 1$ , so step 1.3 sums their series from index $1$ as $z_{-} / (1 - z_{-})$ and $z_{+} / (1 - z_{+})$ . Applying [F12], these two sums and [F18] yield $f_{ρ} (λ) = \frac{σ^{2}}{2 π (1 - ρ^{2})} (1 + \sum_{h = 1}^{\infty} ρ^{h} (e^{- i h λ} + e^{i h λ})) = \frac{σ^{2}}{2 π (1 - 2 ρ \cos λ + ρ^{2})} = \frac{σ^{2}}{2 π ∣ 1 - ρ e^{- i λ} ∣^{2}} .$ The denominator is at least $(1 - ∣ ρ ∣)^{2} > 0$ , so this is a continuous nonnegative density.

5.1F13step 2.1step 4.1algebra∎

Applying [F13] to the two spectral representations gives $E [I_{n}^{(s)} (λ)] = \frac{v}{2} {Φ_{n} (λ - λ_{s}) + Φ_{n} (λ + λ_{s})}, E [I_{n}^{(ρ)} (λ)] = \int_{T} Φ_{n} (λ - θ) f_{ρ} (θ) d θ .$ The first expectation is a sum of two shifted kernels because the spectrum is atomic; the second averages a continuous density. These are exact finite-sample bias formulas and make no distributional or coverage claim.