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 grid and even-grid Nyquist convention
Definition
Let be an integer, let for , and identify with periodically. The real trigonometric interpolation space is For real nodal data , define its periodic Fourier interpolant by
where, for ,
and, for ,
Thus the even-grid Nyquist component is the real cosine only. Its sampled derivative is defined by differentiating this interpolant; the resulting Nyquist derivative values are zero at every grid point.
Depends on
- Sine and cosine defined by their real power series
- Quarter-turn values and shifts by pi/2 and pi
- The derivatives of sine and cosine are cosine and minus sine
- 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)$
Used by
- Periodic Fourier collocation differentiation matrix Algorithm
- A high Fourier mode aliases to a different periodic PIC grid force Example
- A quadratic Fourier product aliases two high modes on an even grid Example
- Four-point Fourier collocation differentiates the Nyquist cosine at its nodes Example
- Periodic Fourier modes alias modulo the grid size Lemma
- Periodic Fourier collocation differentiates its interpolant exactly Theorem
Dependency tree · two levels
19 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, Ch. 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)