LemmaStatement: Literature-sourcedProof: 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.

Integer exponentials are orthogonal for angular Lebesgue measure

Statement

Assume Countable Choice. For every integer $k$ , with the unnormalized angular Lebesgue measure $d λ$ on $T$ from Spectral measures and the known-mean periodogram, $\int_{T} e^{i k λ} d λ = {\begin{cases} 2 π, & k = 0, \\ 0, & k \neq 0. \end{cases}$

Facts & Assumptions

Given: Countable Choice, an integer $k$ , and angular Lebesgue measure $d λ$ on the circle, integrated over one period $[- π, π)$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): the Countable Choice assumption required for the angular Lebesgue measure and its interval values.

[F1]

Spectral measures and the known-mean periodogram: $d λ$ is ordinary Lebesgue measure on one angular period, with total mass $2 π$ .

[F2]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion and Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous: a continuous real function on a closed bounded interval is Riemann integrable, bounded, and uniformly continuous.

[F3]

The nonnegative Lebesgue integral, The integral of a nonnegative simple function, and Monotonicity and nonnegative homogeneity of the nonnegative integral: the Lebesgue integral is monotone on nonnegative functions, and the integral of a nonnegative step function is the sum of its values times the measures of its intervals.

[F4]

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: an interval has Lebesgue measure equal to its length, and a singleton has measure zero.

[F5]

The Lebesgue integral is linear on $L^{1} (μ)$ : the Lebesgue integral is linear on integrable real functions.

[F6]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , The derivatives of sine and cosine are cosine and minus sine, and The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ : integrating a continuous derivative on a closed interval gives the endpoint difference; the derivatives of sine and cosine and the chain rule give the antiderivatives used below.

[F7]

The zero sets of sine and cosine and the least positive common period 2 pi and Parity and the Pythagorean identity for sine and cosine: for integer $k \neq 0$ , $\sin (k π) = \sin (- k π) = 0$ and $\cos (k π) = \cos (- k π)$ .

[F8]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ and Integrable real and complex functions, and their integrals: $e^{i k λ} = \cos (k λ) + i \sin (k λ)$ , and the integral of a complex function is the integral of its real part plus $i$ times that of its imaginary part.

[F9]

The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ and For bounded $f$ on $[a, b]$ and a partition $P$ : the infimum $m_{i}$ and supremum $M_{i}$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L (f, P) = \sum_{i} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ : for a bounded Riemann-integrable real function, the integral lies between the lower and upper Darboux sums for every partition.

[F10]

A continuous map has Borel preimages of Borel sets: the preimage of every Borel set under a continuous map is Borel; in particular the continuous real function in step 1.1 is Borel measurable.

[F11]

For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ : for every $δ > 0$ there is an $N \geq 1$ with $2 π / N < δ$ .

Proof

Proof technique: compare the Lebesgue integral with Darboux sums, then use the fundamental theorem of calculus.

1.1A1F1F2F3F4F5F9F10F11given

Let $g : [- π, π] \to R$ be continuous and bounded by $B \geq 0$ . For each $N \geq 1$ , partition the interval into the fixed equal pieces $J_{j, N} = [- π + 2 π j / N, - π + 2 π (j + 1) / N)$ , with the endpoint $π$ added to the last piece. On each piece take the infimum and supremum of $g + B$ on its closed hull and use them as the constant values of simple step functions $ℓ_{N}$ and $u_{N}$ . They satisfy $0 \leq ℓ_{N} \leq g + B \leq u_{N}$ . By [F3]–[F4], under [A1], their Lebesgue integrals with respect to $λ_{1}$ are exactly the lower and upper Darboux sums of $g + B$ for this partition. Given $η > 0$ , uniform continuity [F2] gives $δ > 0$ such that the oscillation on any interval of length below $δ$ is less than $η$ . Choose $N$ with $2 π / N < δ$ by [F11]; then every oscillation is below $η$ , and the gap between the sums is at most $2 π η$ . Hence that gap tends to zero. Monotonicity of the Lebesgue integral places $\int_{[- π, π)} (g + B) d λ_{1}$ between the same sums; the Darboux integral of $g + B$ lies between them as well. Therefore the Lebesgue and Darboux integrals of $g + B$ agree. By linearity [F5] and $λ_{1} ([- π, π)) = 2 π$ from [F1], the two integrals of $g$ agree.

1.2A1F1given

If $k = 0$ , the integrand is the constant $1$ , so its integral is $2 π$ by [F1] under [A1].

2.1A1F1F2F6F7F8step 1.1

If $k \neq 0$ , apply step 1.1 to the continuous real functions $g (λ) = \cos (k λ)$ and $g (λ) = \sin (k λ)$ . Their antiderivatives are respectively $\sin (k λ) / k$ and $- \cos (k λ) / k$ by [F6] and the chain rule. Their endpoint differences vanish by [F7], so both Lebesgue integrals on $[- π, π)$ are zero. These functions are $2 π$ -periodic; by the angular integral definition [F1], their integrals on $T$ are those same integrals over $[- π, π)$ . Euler's identity and the complex-integral convention [F8] give $\int_{T} e^{i k λ} d λ = 0$ .

3.1givenstep 1.2step 2.1algebra∎

The cases $k = 0$ and $k \neq 0$ exhaust the integers, and steps 1.2 and 2.1 give the stated formula.

Depends on

Used by

Dependency tree · two levels

115 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

Dewei Wang, STAT 720 Time Series Analysis, Section 4.2 (standard reference, not scraped)
Nicolai Meinshausen, Time Series Analysis: Notes for the course HS 2022 (standard reference, not scraped)