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.

Periodic Fourier collocation differentiates its interpolant exactly

Statement

Let $N \geq 2$ , let $U = (U_{j})_{j = 0}^{N - 1} \in R^{N}$ , and let $p = I_{N} U \in T_{N}$ be the interpolant defined in Periodic Fourier collocation grid and even-grid Nyquist convention. The matrix Periodic Fourier collocation differentiation matrix satisfies

(D_{N} U)_{i} = p^{'} (x_{i}), 0 \leq i < N .

For even $N$ , this statement includes the Nyquist cosine mode, whose derivative vanishes at the grid nodes.

Facts & Assumptions

Given: An integer $N \geq 2$ , the periodic grid and interpolant, and real nodal data $U$ .

[F1]

Periodic Fourier collocation grid and even-grid Nyquist convention: $I_{N} U = \sum_{j} U_{j} L_{j}$ on the $N$ equally spaced nodes; its frequency set is a complete set of residues modulo $N$ , with only the cosine Nyquist mode when $N$ is even.

[F2]

Periodic Fourier collocation differentiation matrix: $(D_{N})_{i j}$ is the termwise derivative of $L_{j}$ evaluated at $x_{i}$ ; in the even case the Nyquist sine term is zero at these nodes.

[F3]

Orthogonality of the characters $x \mapsto e^{2 π i k x / N}$ on $Z / N Z$ : summing all $N$ characters over $Z / N Z$ gives $N$ when the two indices agree modulo $N$ and $0$ otherwise.

[F4]

Finite Fourier inversion for the unitary transform on $Z / N Z$ : the finite Fourier transform on $Z / N Z$ has an inverse, so the frequency coefficients representing nodal data are unique.

[F5]

The derivatives of sine and cosine are cosine and minus sine: $(\cos k x)^{'} = - k \sin (k x)$ and $(\sin k x)^{'} = k \cos (k x)$ .

[F6]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ : $e^{i t} = \cos t + i \sin t$ for real $t$ .

[F7]

Quarter-turn values and shifts by pi/2 and pi: $\sin (k π) = 0$ for every integer $k$ .

[F8]

The subtraction formulas for sine and cosine: $\cos (u - v) = \cos u \cos v + \sin u \sin v$ , so each $\cos (k (x - x_{j}))$ expands into cosine and sine modes with frequency $k$ .

[F9]

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)$ : differentiating a trigonometric function composed with $x \mapsto k (x - x_{j})$ multiplies its derivative by $k$ .

[F10]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : differentiating a finite sum of differentiable functions gives the sum of their derivatives.

Proof

1.1F1F3F6F7F8algebra

By [F8], each low-frequency cosine difference in $L_{j}$ expands into the corresponding cosine/sine modes in $T_{N}$ . For even $N = 2 K$ , its Nyquist term expands into $\cos (K x) \cos (K x_{j}) + \sin (K x) \sin (K x_{j})$ ; [F7] makes the second coefficient zero because $K x_{j} = π j$ . At a grid difference $x_{i} - x_{j} = 2 π (i - j) / N$ , Euler's identity [F6] rewrites the cosine sum defining $L_{j} (x_{i})$ as the normalized sum of all characters in a complete residue system modulo $N$ : for odd $N = 2 K + 1$ the residues are $- K, \dots, K$ , and for even $N = 2 K$ they are $- K + 1, \dots, K$ . Character orthogonality [F3] gives $L_{j} (x_{i}) = 1$ when $i = j$ and $0$ otherwise. Thus $I_{N} U$ takes the prescribed nodal values and lies in $T_{N}$ .

1.2F1F4F6algebra

Let $q \in T_{N}$ . Euler's formula expands each low-frequency cosine/sine pair into the characters $e^{i k x_{j}}$ and $e^{- i k x_{j}}$ . If $N = 2 K + 1$ , the resulting residues are $- K, \dots, K$ ; if $N = 2 K$ , they are $- K + 1, \dots, K - 1$ together with the Nyquist residue $K$ , because $\cos (K x_{j}) = e^{i K x_{j}}$ . In either case this is one coefficient for each residue modulo $N$ , and the change from the real basis coefficients to these character coefficients is invertible (for each low mode it is the usual two-by-two Euler change, and the Nyquist coefficient is unchanged). Thus if $q$ vanishes at the nodes, its finite Fourier transform is zero and inversion [F4] makes every character coefficient, hence every real basis coefficient, zero. This proves uniqueness.

2.1F2F5F7F9F10step 1.1algebra

Differentiate the finite sum $p (x) = \sum_{j} U_{j} L_{j} (x)$ term by term using [F10]. By [F5] and [F9], $p^{'} (x_{i}) = \sum_{j} U_{j} L_{j}^{'} (x_{i})$ . When $N$ is odd this is exactly the sine sum defining $D_{N} U$ in [F2]. When $N = 2 K$ the derivative of the remaining Nyquist term is proportional to $\sin (K (x_{i} - x_{j})) = \sin (π (i - j)) = 0$ by [F7], so the same equality holds with the Nyquist term omitted.

3.1step 1.1step 1.2step 2.1∎

Steps 1.1–2.1 establish the nodal interpolation and derivative identity for every data vector, including both parity branches of $N$ .

Depends on

Used by

Dependency tree · two levels

56 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

Jie Shen and Tao Tang, Spectral and High-Order Methods with Applications, §2.2 (standard reference, not scraped)
Lloyd N. Trefethen, Finite Difference and Spectral Methods for Ordinary and Partial Differential Equations, Ch. 7 (standard reference, not scraped)