TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Polynomial exactness and best-approximation error for Clenshaw–Curtis

Statement

Let $a < b$ , $n \in N$ , and $f \in C [a, b]$ . Put $m = (a + b) / 2$ , $d = (b - a) / 2$ , and $g (t) = f (m + d t)$ on $[- 1, 1]$ . Let $E_{n} (g)$ and $Λ_{n}^{L}$ be the best uniform polynomial error and the Chebyshev–Lobatto interpolation norm from Best uniform polynomial error and Chebyshev interpolation operators. Interpreting polynomial inputs by their evaluation functions, the rule $Q_{n, [a, b]}$ of Clenshaw–Curtis quadrature with the midpoint zero-degree case is exact for the zero polynomial and every nonzero formal polynomial of degree at most $n$ , and $∣ \int_{a}^{b} f (x) d x - Q_{n, [a, b]} (f) ∣ \leq (b - a) (1 + Λ_{n}^{L}) E_{n} (g) .$ Because affine pullback preserves the supremum norm and polynomial degree, $E_{n} (g)$ is also the best degree- $n$ uniform error of $f$ on $[a, b]$ .

Facts & Assumptions

Given: $a < b$ , $n \in N$ , and $f \in C [a, b]$ .

[A1]

$n \in N$ , and the normalized function is $g (t) = f (m + d t)$ with $m = (a + b) / 2$ and $d = (b - a) / 2 > 0$ .

[F1]

Clenshaw–Curtis quadrature with the midpoint zero-degree case: for $n \geq 1$ , $Q_{n, [a, b]} (f) = d \sum_{k = 0}^{n} a_{k} μ_{k}$ with the DCT-I coefficients and Chebyshev moments; at $n = 0$ it is $(b - a) f (m)$ .

[F2]

DCT-I coefficients of the Chebyshev–Lobatto interpolant: for $n \geq 1$ , $\sum_{k = 0}^{n} a_{k} T_{k} = I_{n}^{L} g$ .

[F3]

Exact integrals of Chebyshev polynomials: $μ_{k} = \int_{- 1}^{1} T_{k} (t) d t$ for every $k \geq 0$ .

[F4]

Chebyshev cardinal interpolation reproduces polynomials and its norm is the cardinal sum: $I_{n}^{L} p = p$ for every $p \in P_{n}$ , including $n = 0$ .

[F5]

Chebyshev interpolation error is controlled by best polynomial error: $∥ g - I_{n}^{L} g ∥_{\infty} \leq (1 + Λ_{n}^{L}) E_{n} (g)$ for every $n \geq 0$ .

[F6]

Best uniform polynomial error and Chebyshev interpolation operators: $E_{n} (g) = \inf_{p \in P_{n}} ∥ g - p ∥_{\infty}$ , $Λ_{n}^{L}$ is the operator norm of $I_{n}^{L}$ , and $I_{0}^{L} g = g (0)$ .

[F7]

Formal real polynomials, evaluation, degree, leading coefficient, and monic polynomials and The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ : if $q (X) = \sum_{k = 0}^{n} c_{k} X^{k}$ and $α, β \in R$ , then $q (α + β t) = \sum_{k = 0}^{n} c_{k} \sum_{j = 0}^{k} ι (\binom{k}{j}) α^{k - j} β^{j} t^{j}$ . Regrouping these finite sums gives a coefficient list with no index above $n$ ; since $d = (b - a) / 2 > 0$ , this applies to both affine maps $t \mapsto m + d t$ and $x \mapsto (x - m) / d$ .

[F8]

If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ and 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)$ : if $∣ u (x) ∣ \leq M$ on $[a, b]$ , then $∣ \int_{a}^{b} u (x) d x ∣ \leq (b - a) M$ .

[F9]

Monotone change of variable for Riemann-integrable functions: for the increasing affine bijection $t \mapsto m + d t$ , $\int_{a}^{b} P (x) d x = d \int_{- 1}^{1} P (m + d t) d t$ .

[F10]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion and Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ : the continuous functions here are integrable and finite sums may be integrated termwise.

Proof

1.1givenF1F2F3F9F10algebra

For $n \geq 1$ , let $p_{n} (t) = \sum_{k = 0}^{n} a_{k} T_{k} (t)$ . By [F1]–[F3] and [F10], $Q_{n, [a, b]} (f) = d \sum_{k} a_{k} \int_{- 1}^{1} T_{k} (t) d t = d \int_{- 1}^{1} p_{n} (t) d t$ . The affine substitution [F9] makes this $\int_{a}^{b} P (x) d x$ for $P (x) = p_{n} ((x - m) / d)$ , and [F2] identifies $P$ with the interpolant pullback. For $n = 0$ , [F1] is the integral of the constant polynomial $P (x) = f (m)$ by [F9]. Thus $Q_{n, [a, b]} (f) = \int_{a}^{b} P (x) d x$ in every case.

2.1givenF4F7step 1.1algebra

Let $q$ be the zero polynomial or a nonzero formal polynomial of degree at most $n$ , interpreted by its evaluation function on $[a, b]$ , and put $\tilde{q} (t) = q (m + d t)$ . By [F7], $\tilde{q} \in P_{n}$ . The interpolation reproduction in [F4] gives $I_{n}^{L} \tilde{q} = \tilde{q}$ , so step 1.1 yields $Q_{n, [a, b]} (q) = \int_{a}^{b} q (x) d x$ . This proves polynomial exactness.

2.2givenF5F8F10step 1.1algebra

Set $P (x) = I_{n}^{L} g ((x - m) / d)$ as in step 1.1. The pullback bijection gives $∥ f - P ∥_{\infty, [a, b]} = ∥ g - I_{n}^{L} g ∥_{\infty, [- 1, 1]}$ . By [F8], $∣ \int_{a}^{b} (f - P) ∣ \leq (b - a) ∥ f - P ∥_{\infty}$ . Combining this with $Q (f) = \int P$ from step 1.1 and [F5] proves the displayed bound.

3.1givenF6F7algebra∎

For each $p \in P_{n}$ on $[- 1, 1]$ , the pullback $x \mapsto p ((x - m) / d)$ is in $P_{n}$ on $[a, b]$ by [F7] and has the same supremum error against $f$ as $p$ has against $g$ . Conversely, every degree-at-most- $n$ polynomial on $[a, b]$ pulls back to one on $[- 1, 1]$ . The two infima defining best uniform error are therefore equal.

Depends on

Used by

A four-dimensional product exactly integrated on a sparse node union Example

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

L. Ridgway Scott, Numerical Analysis, 2nd ed., §13.1 and §13.4.1 (standard reference, not scraped)
Lloyd N. Trefethen, Is Gauss Quadrature Better than Clenshaw–Curtis?, §2 (standard reference, not scraped)