TheoremStatement: 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.

Chebyshev–Gauss–Lobatto differentiation is exact on the interpolant

Statement

Let $N \geq 1$ , let $U_{j} \in R$ be data on the nodes $x_{j} = \cos (j π / N)$ , and let $p$ be the unique polynomial of degree at most $N$ with $p (x_{j}) = U_{j}$ . The matrix Chebyshev–Gauss–Lobatto polynomial differentiation matrix satisfies

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

In particular, applying $D_{N}$ twice gives $p^{''} (x_{i})$ at each node.

Facts & Assumptions

Given: $N \geq 1$ , distinct Chebyshev–Gauss–Lobatto nodes, and real nodal data.

[F1]

Chebyshev–Gauss–Lobatto collocation grid: the nodes are distinct; reversing their order gives increasing nodes $z_{k} = x_{N - k}$ .

[F2]

Chebyshev–Gauss–Lobatto polynomial differentiation matrix: $D_{i j} = ℓ_{N - j}^{'} (x_{i})$ for the cardinal polynomials of the increasing reindexing.

[F3]

Existence and uniqueness of the cardinal-polynomial interpolant: at $N + 1$ distinct ordered nodes, the cardinal sum is the unique polynomial of degree at most $N$ with the prescribed values.

[F4]

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.1givenF1F3construct

Reindex the data by $Y_{k} = U_{N - k}$ . By [F1], the nodes $z_{k} = x_{N - k}$ are strictly increasing, so [F3] gives $p (x) = \sum_{k = 0}^{N} Y_{k} ℓ_{k} (x)$ as the unique degree-at-most- $N$ interpolant. Reversing the finite sum back to the descending index gives $p (x) = \sum_{j = 0}^{N} U_{j} ℓ_{N - j} (x)$ .

2.1F2F4step 1.1algebra

Differentiate the finite polynomial sum in step 1.1 term by term using [F4]. At $x_{i}$ this gives $p^{'} (x_{i}) = \sum_{j = 0}^{N} U_{j} ℓ_{N - j}^{'} (x_{i}) = \sum_{j = 0}^{N} (D_{N})_{i j} U_{j} = (D_{N} U)_{i}$ by [F2]. This proves the first identity for each node.

3.1F1F3step 2.1algebra∎

The polynomial $p^{'}$ has degree at most $N - 1 \leq N$ and its nodal values are $D_{N} U$ by step 2.1. Uniqueness [F3] therefore makes $p^{'}$ the interpolant of the vector $D_{N} U$ . Applying the already proved first-derivative identity of step 2.1 to that vector gives $D_{N} (D_{N} U) = (p^{''} (x_{i}))_{i = 0}^{N}$ .

Depends on

Used by

Dependency tree · two levels

23 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.1 (standard reference, not scraped)
Lloyd N. Trefethen, Finite Difference and Spectral Methods for Ordinary and Partial Differential Equations, Ch. 8 (standard reference, not scraped)