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–Lobatto interpolation remainder bound

Statement

Let $N \geq 1$ and $f \in C^{N + 1} ([- 1, 1])$ . Let $I_{N}^{L} f$ be interpolation at the nodes $x_{j} = \cos (j π / N)$ . Then $∥ f - I_{N}^{L} f ∥_{C} \leq \sqrt{π} \frac{2^{1 - N}}{(N + 1)!} \max_{x \in [- 1, 1]} ∣ f^{(N + 1)} (x) ∣ .$

Facts & Assumptions

Given: $N \geq 1$ and $f \in C^{N + 1} ([- 1, 1])$ .

[F1]

Chebyshev–Gauss–Lobatto collocation grid: the $N + 1$ distinct nodes are $x_{j} = \cos (j π / N)$ , including both endpoints.

[F2]

Chebyshev polynomials of the first and second kinds by their three-term recurrences and Degrees and leading coefficients of the Chebyshev polynomials: $T_{N}$ has degree $N$ and leading coefficient $2^{N - 1}$ for $N \geq 1$ .

[F3]

$T_{n} (\cos θ) = \cos (n θ)$ and $U_{n} (\cos θ) \sin θ = \sin ((n + 1) θ)$ for every $n \in N$ , 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)$ , and The derivatives of sine and cosine are cosine and minus sine: for $x = \cos θ$ , $0 < θ < π$ , $T_{N}^{'} (x) = N \sin (N θ) / \sin θ$ .

[F4]

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

[F5]

Parity and the Pythagorean identity for sine and cosine: $∣ \sin t ∣ \leq 1$ for every real $t$ .

[F6]

Cardinal-polynomial interpolation: the node polynomial is $ω_{N} (x) = \prod_{j = 0}^{N} (x - x_{j})$ and $I_{N}^{L} f$ is its degree-at-most- $N$ Lagrange interpolant after reversing the decreasing node order.

[F7]

Pointwise Lagrange interpolation remainder: for $x$ off the nodes, $f (x) - I_{N}^{L} f (x) = f^{(N + 1)} (ξ) ω_{N} (x) / (N + 1)!$ for some $ξ$ in the interval between the extreme nodes and $x$ ; at a node the error is zero.

[F8]

Arcsine-weighted inner product on the Chebyshev interval: $∥ h ∥_{C} \leq \sqrt{π} ∥ h ∥_{\infty}$ because the angular measure has total mass $π$ .

[F9]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ , Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, and Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value: $f^{(N + 1)}$ is continuous on the compact interval, so the displayed finite maximum exists.

[F10]

A nonzero real polynomial of degree $n$ has no more than $n$ distinct real roots: a polynomial with more distinct roots than its degree is the zero polynomial.

Proof

1.1F2algebra

By the recurrence in [F2], $T_{N}$ has leading coefficient $2^{N - 1}$ for every $N \geq 1$ . Hence $q_{N} (x) : = \frac{2^{1 - N}}{N} (x^{2} - 1) T_{N}^{'} (x)$ is monic of degree $N + 1$ .

1.2F1F2F3F4F6F10algebra

For $1 \leq j < N$ , put $θ_{j} = j π / N$ . Then [F3] and [F4] give $T_{N}^{'} (x_{j}) = N \sin (j π) / \sin θ_{j} = 0$ . Also $q_{N} (1) = q_{N} (- 1) = 0$ . Thus $q_{N}$ vanishes at all $N + 1$ distinct nodes in [F1]. The node product $ω_{N}$ is also monic of degree $N + 1$ by [F6]; their difference has degree at most $N$ and $N + 1$ distinct roots, so [F10] gives $q_{N} = ω_{N}$ .

2.1F1F3F5step 1.2algebra

For $x = \cos θ$ with $0 < θ < π$ , the derivative formula in [F3] gives $∣ ω_{N} (x) ∣ = 2^{1 - N} ∣ \sin θ \sin (N θ) ∣ \leq 2^{1 - N} .$ The inequality uses [F5]. At the endpoints $ω_{N} = 0$ , so this bound holds on all of $[- 1, 1]$ .

3.1F1F7F9step 2.1algebra

At nodes the interpolation error is zero; off the nodes apply [F7] and step 2.1. Since the maximum in [F9] is finite, this gives $∥ f - I_{N}^{L} f ∥_{\infty} \leq \frac{2^{1 - N}}{(N + 1)!} \max_{[- 1, 1]} ∣ f^{(N + 1)} ∣ .$

4.1F8step 3.1algebra∎

Apply the weighted-norm estimate [F8] to the uniform error in step 3.1. This proves the stated inequality.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

77 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, §1.8 (standard reference, not scraped)
Mark Embree, Lecture Notes on Numerical Analysis, Lecture 3 (standard reference, not scraped)