CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Best polynomial errors vanish for continuous functions

Statement

For every $f \in C [- 1, 1]$ , $E_{n} (f) \to 0$ as $n \to \infty$ . This statement concerns best polynomial errors only; it does not assert convergence of interpolation at arbitrary node arrays.

Facts & Assumptions

Given: $f \in C [- 1, 1]$ and $ε > 0$ .

[F1]

Polynomials are uniformly dense in $C ([a, b], R)$ for every closed interval: every continuous real function on a closed interval is uniformly approximable by polynomials.

[F2]

Best uniform polynomial error and Chebyshev interpolation operators: $E_{n} (f) = \inf_{p \in P_{n}} ∥ f - p ∥_{\infty}$ , and $P_{m} \subseteq P_{n}$ when $m \leq n$ .

Proof

1.1givenF1choose

By [F1], choose a polynomial $p$ and an integer $m$ with $p \in P_{m}$ such that $∥ f - p ∥_{\infty} < ε$ ; if $p = 0$ , take $m = 0$ .

2.1givenF1F2step 1.1algebra∎

For every $n \geq m$ , $p \in P_{n}$ , so [F2] gives $0 \leq E_{n} (f) \leq ∥ f - p ∥_{\infty} < ε$ . Since $ε > 0$ was arbitrary, $E_{n} (f) \to 0$ . This conclusion concerns $E_{n}$ alone; it does not show that $(1 + Λ_{n}^{σ}) E_{n} (f) \to 0$ .

Depends on

Used by

Equispaced interpolation of Runge's function diverges Example

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

Lloyd N. Trefethen, Approximation Theory and Approximation Practice, Ch. 6 (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Polynomial interpolation (standard reference, not scraped)