Pipeline-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.

✓ 3 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Polynomial approximation and Chebyshev interpolation — Examples

1 · Prerequisites

2 · Summary

The examples compute the degree-one root and Lobatto operator norms, transfer an explicit factorial best-error rate for the exponential, and prove divergence for equispaced interpolation of Runge's function. The last example shows why polynomial density alone does not imply convergence for a fixed interpolation array.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Equispaced interpolation of Runge's function diverges

Example

Let $f (x) = 1 / (1 + 25 x^{2})$ on $[- 1, 1]$ . For each integer $n \geq 2$ , take the $n + 1$ equispaced nodes $x_{j} = - 1 + \frac{2 j}{n}, 0 \leq j \leq n,$ let $ℓ_{j, n} (x) = \prod_{k \neq j} (x - x_{k}) / (x_{j} - x_{k})$ , and put $p_{n} (x) = \sum_{j = 0}^{n} f (x_{j}) ℓ_{j, n} (x)$ . Then, at the evaluation point $y_{n} = 1 - 1 / n$ , $∣ f (y_{n}) - p_{n} (y_{n}) ∣ ⟶ \infty .$ Thus the uniform interpolation errors diverge, although the best polynomial errors $E_{n} (f)$ tend to zero by Best polynomial errors vanish for continuous functions.

Facts & Assumptions

Given: An integer $n \geq 2$ , the equispaced nodes above, $a = 1 / 5$ , $i \in C$ with $i^{2} = - 1$ , and $f (x) = 1 / (1 + 25 x^{2})$ .

[F1]

Best uniform polynomial error and Chebyshev interpolation operators: $P_{n}$ , $C [- 1, 1]$ , and $∥ \cdot ∥_{\infty}$ have the stated meanings.

[F2]

Best polynomial errors vanish for continuous functions: $E_{n} (g) \to 0$ for every $g \in C [- 1, 1]$ .

[F3]

A nonzero real polynomial of degree $n$ has no more than $n$ distinct real roots: a nonzero real polynomial of degree at most $n$ has at most $n$ distinct real roots.

[F4]

The real exponential function and the number $e$ by a power series and The exponential series converges absolutely for every real argument: $e = \sum_{k = 0}^{\infty} 1 / k!$ , and the series converges absolutely.

[F5]

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ : $n!$ is positive and $n! = 1 \cdot 2 \dots n$ .

[F6]

For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges: $\sum_{k = 1}^{\infty} 2^{- k} = 1$ .

[F7]

The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ : $(x + y)^{n} = \sum_{k = 0}^{n} ι ⁣ ((\binom{n}{k})) x^{k} y^{n - k}$ in $R$ , where $ι : N \to R$ is the canonical embedding of [F9].

[F8]

$(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ and The binomial coefficients are symmetric and increase to the middle level before decreasing: $(\binom{n}{k}) k! = n^{\underline{k}}$ , and the central binomial coefficient is maximal.

[F9]

The canonical natural $ι (n) = n \cdot 1_{F}$ of a field and Canonical naturals are positive and strictly increasing: throughout all real expressions, including identities and inequalities, natural numbers, factorials, and binomial coefficients abbreviate their canonical real images under $ι$ . This embedding preserves addition, multiplication, and order, sends $0$ to $0$ , and sends positive naturals to positive reals.

[F10]

The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ and $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ : $i^{2} = - 1$ , $C$ is a field, and each complex number has unique coordinates $a + b i$ ; Formal complex polynomials, evaluation, degree, leading coefficient, and monic polynomials: complex polynomials are finite coefficient lists; Real and imaginary parts, complex conjugation, and modulus and Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive: $∣ a + b i ∣ = \sqrt{a^{2} + b^{2}}$ , modulus is multiplicative and vanishes only at zero; Complex modulus restricts to real absolute value: complex modulus restricts to real absolute value.

[F11]

Positive rational bases have rational powers as in Rational powers $a^{r}$ of a positive base. By Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ , powers decrease with the rational exponent when $0 < a < 1$ , increase when $a > 1$ , and increase with the positive base for a positive rational exponent. Laws of rational exponents gives $(a^{r})^{s} = a^{r s}$ . Integer indices and natural counts embed into $Q$ by The integers embed in the rationals, and rational comparisons use Order on the rationals.

[F12]

For every real $x$ , $x^{2} = 0$ if $x = 0$ by Integer powers $a^{m}$ and Multiplication by zero: $0 \cdot a = 0$ , while $x^{2} > 0$ if $x \neq 0$ by Squares of nonzero elements are positive. The positive integer $25$ and the real number $1$ are positive by [F9]; the ordered-field axioms Ordered field therefore give $1 + 25 x^{2} > 0$ .

[F13]

Every real polynomial function, including $d (x) = 1 + 25 x^{2}$ , is continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).

[F14]

If $d$ is continuous and nowhere zero, its reciprocal is continuous on its domain (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, claim 4). By [F12], $d (x) > 0$ for every real $x$ , so $f = 1 / d$ belongs to $C [- 1, 1]$ .

Proof

1.1givenF1F3F10constructalgebra

For $0 \leq j < n$ , $x_{j + 1} - x_{j} = 2 / n > 0$ , so the nodes are distinct. Each product $ℓ_{j, n} (x)$ has $n$ linear factors and degree at most $n$ ; at $x_{j}$ all its factors equal $1$ , while at any other node $x_{k}$ the factor indexed by $k$ is zero. Thus $p_{n} \in P_{n}$ and $p_{n} (x_{j}) = f (x_{j})$ . Define $ω_{n} (x) = \prod_{j = 0}^{n} (x - x_{j})$ and for nodal data define the complex-linear Lagrange map $J_{n} g = \sum_{j} g (x_{j}) ℓ_{j, n}$ . For non-real $z$ , put $g_{z} (x) = 1 / (x - z)$ and $q_{n, z} (x) = (1 - ω_{n} (x) / ω_{n} (z)) / (x - z)$ . The denominator is nonzero because the roots of $ω_{n}$ are real and $C$ is a field [F10]. Expanding $ω_{n} (x) - ω_{n} (z)$ termwise and using $x^{k} - z^{k} = (x - z) \sum_{r = 0}^{k - 1} x^{k - 1 - r} z^{r}$ shows $q_{n, z}$ is a complex polynomial of degree at most $n$ ; at each node $x_{j}$ it equals $1 / (x_{j} - z)$ . The difference $q_{n, z} - J_{n} g_{z}$ is a complex polynomial of degree at most $n$ with $n + 1$ distinct real roots. By unique complex coordinates [F10], its real and imaginary coefficient polynomials are real polynomials; both vanish at all the nodes, so [F3] forces both to be zero. Since $g_{z} - q_{n, z} = ω_{n} (x) / ((x - z) ω_{n} (z))$ , this proves $g_{z} (x) - J_{n} g_{z} (x) = ω_{n} (x) / ((x - z) ω_{n} (z))$ for real $x$ .

1.2givenF4F5F6F7F8F9algebra

At $y_{n} = 1 - 1 / n$ , direct multiplication gives $∣ ω_{n} (y_{n}) ∣ = \prod_{k = 1}^{n} (2 k - 1) / n^{n + 1} = (\binom{2 n}{n}) n! / (2^{n} n^{n + 1})$ . By [F8], $(\binom{2 n}{n})$ is the largest of the $2 n + 1$ binomial coefficients, and [F7] says their sum is $4^{n}$ , so $(\binom{2 n}{n}) \geq 4^{n} / (2 n + 1)$ . Also $e < 3$ : for $k \geq 2$ , $k! = 2 \cdot 3 \dots k \geq 2^{k - 1}$ because each of these $k - 1$ factors is at least $2$ , with strict inequality for $k \geq 3$ ; therefore [F4]–[F6] give $e = 2 + \sum_{k = 2}^{\infty} 1 / k! < 3$ . By [F8], $(\binom{n}{k}) k! = n (n - 1) \dots (n - k + 1) \leq n^{k}$ , hence $(\binom{n}{k}) / n^{k} \leq 1 / k!$ ; applying [F7] gives $(1 + 1 / n)^{n} \leq \sum_{k = 0}^{n} 1 / k! < e < 3$ . Induction then yields $n! \geq (n / 3)^{n}$ : it holds at $n = 1$ , and the ratio of successive values of $n! / (n / 3)^{n}$ is $3 / (1 + 1 / n)^{n} > 1$ . Therefore $∣ ω_{n} (y_{n}) ∣ \geq (2 / 3)^{n} / [n (2 n + 1)]$ .

1.3givenF1F10F11algebra

The positive node radii form an arithmetic progression in $(0, 1]$ of spacing $δ = 2 / n$ ; for even $n$ there is also the central node $0$ . Pairing $r, - r$ in $ω_{n} (i a)$ gives the factor $∣ (i a - r) (i a + r) ∣ = a^{2} + r^{2}$ by [F10], and the even-grid central factor is $∣ i a ∣ = a \leq 1$ . Each bin has length $1 / 4$ , and the radius progression begins within $δ$ of $0$ and ends at $1$ . Thus for each bin its endpoint gaps are at most $δ$ and its internal gaps equal $δ$ : if it contains $m_{b} \geq 1$ radii, its length lies between $(m_{b} - 1) δ$ and $(m_{b} + 1) δ$ ; if it contains none, its length is at most one progression gap, so the same count bounds hold. Therefore $n / 8 - 1 \leq m_{b} \leq n / 8 + 1$ . Partition the radii into $(0, 1 / 4], (1 / 4, 1 / 2], (1 / 2, 3 / 4], (3 / 4, 1]$ . The paired factors in these bins are bounded above by $B_{1} = 41 / 400$ , $B_{2} = 29 / 100$ , $B_{3} = 241 / 400$ , and $B_{4} = 26 / 25$ . By [F11], for $b = 1, 2, 3$ the bound $B_{b} < 1$ and $m_{b} \geq n / 8 - 1$ imply $B_{b}^{m_{b}} \leq B_{b}^{n / 8 - 1}$ ; for $b = 4$ , $B_{4} > 1$ and $m_{4} \leq n / 8 + 1$ imply $B_{4}^{m_{4}} \leq B_{4}^{n / 8 + 1}$ . Multiplying these bounds and the central factor gives $∣ ω_{n} (i a) ∣ \leq A (B_{1} B_{2} B_{3} B_{4})^{n / 8}$ , where $A = B_{1}^{- 1} B_{2}^{- 1} B_{3}^{- 1} B_{4}$ . Direct rational multiplication gives $B_{1} B_{2} B_{3} B_{4} < 1 / 50 < (5 / 8)^{8}$ ; base monotonicity and the iterated-power law in [F11] then give $(B_{1} B_{2} B_{3} B_{4})^{n / 8} < (5 / 8)^{n}$ .

2.1givenF1F10step 1.1algebra

With $a = 1 / 5$ , direct subtraction gives $f (x) = \frac{a}{2 i} (1 / (x - i a) - 1 / (x + i a))$ , and the finite Lagrange sum is complex-linear by field distributivity [F10], so it preserves the identity. Since $x_{n - j} = - x_{j}$ , reindexing the factors gives $ω_{n} (- x) = (- 1)^{n + 1} ω_{n} (x)$ ; thus $ω_{n}$ is odd for even $n$ and even for odd $n$ . Every factor $i a - x_{j}$ is nonzero, so $ω_{n} (i a) \neq 0$ ; real coefficients and parity give $ω_{n} (i a) = i W$ for a nonzero real $W$ when $n$ is even, and $ω_{n} (i a) = ω_{n} (- i a) = W$ for a nonzero real $W$ when $n$ is odd. For even $n$ , substituting the pole-error identities from step 1.1 and using $1 / (x - i a) + 1 / (x + i a) = 2 x / (x^{2} + a^{2})$ gives $f (x) - p_{n} (x) = a x ω_{n} (x) / (i (x^{2} + a^{2}) ω_{n} (i a))$ . For odd $n$ , using $1 / (x - i a) - 1 / (x + i a) = 2 i a / (x^{2} + a^{2})$ gives $f (x) - p_{n} (x) = a^{2} ω_{n} (x) / ((x^{2} + a^{2}) ω_{n} (i a))$ . Taking moduli and using [F10] gives, for real $x$ , $∣ f (x) - p_{n} (x) ∣ = {\begin{cases} \frac{a ∣ x ∣}{x^{2} + a^{2}} \frac{∣ ω_{n} (x) ∣}{∣ ω_{n} (i a) ∣}, & n even, \\ \frac{a^{2}}{x^{2} + a^{2}} \frac{∣ ω_{n} (x) ∣}{∣ ω_{n} (i a) ∣}, & n odd . \end{cases}$

3.1givenF2F9F10F12F13F14step 2.1step 1.2step 1.3algebra∎

For $n \geq 2$ , $y_{n} \geq 1 / 2$ and $y_{n}^{2} + a^{2} \leq 26 / 25$ , so the coefficient in step 2.1 is at least $5 / 52$ for even $n$ and $1 / 26$ for odd $n$ , hence at least $1 / 26$ . By [F10], the complex-modulus identity in step 2.1 is the stated real absolute error; steps 1.2 and 1.3 then give $∣ f (y_{n}) - p_{n} (y_{n}) ∣ > \frac{1}{26 A} (16 / 15)^{n} / [n (2 n + 1)]$ . The right-hand side tends to infinity because the ratio of successive terms tends to $16 / 15 > 1$ and is eventually bounded below by a fixed ratio greater than $1$ . Therefore $∥ f - p_{n} ∥_{\infty} \to \infty$ . By [F12]–[F14], $f \in C [- 1, 1]$ , so [F2] applies and $E_{n} (f) \to 0$ .

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Degree-one root and Lobatto interpolation norms

Example

For degree $n = 1$ , the first-kind roots are $1 / \sqrt{2}$ and $- 1 / \sqrt{2}$ , while the Lobatto nodes are $1$ and $- 1$ . The corresponding interpolation operator norms are $Λ_{1}^{R} = \sqrt{2}, Λ_{1}^{L} = 1.$

Facts & Assumptions

Given: Degree $n = 1$ and the two node conventions of Best uniform polynomial error and Chebyshev interpolation operators.

[F1]

Best uniform polynomial error and Chebyshev interpolation operators: the two node families and cardinal interpolation operators are defined by the displayed cosine and product formulas.

[F2]

Chebyshev cardinal interpolation reproduces polynomials and its norm is the cardinal sum: the operator norm is the supremum of the cardinal sum $\sum_{j} ∣ ℓ_{j} (x) ∣$ .

[F3]

Half-angle identities with the sign determined by the quadrant, Signs, monotonicity intervals, and ranges of sine and cosine, The subtraction formulas for sine and cosine, and Quarter-turn values and shifts by pi/2 and pi: $\cos (π / 4) = 1 / \sqrt{2}$ because $\cos (π / 4) > 0$ ; the subtraction formula gives $\cos (3 π / 4) = - 1 / \sqrt{2}$ , and $\cos (π / 2) = 0$ .

Proof

1.1givenF1F3algebra

Put $c = 1 / \sqrt{2}$ . The root nodes are $c, - c$ , so their cardinal polynomials are $ℓ_{0} (x) = (x + c) / (2 c)$ and $ℓ_{1} (x) = (c - x) / (2 c)$ . For $∣ x ∣ \leq c$ both are nonnegative and their sum is $1$ . For $c \leq x \leq 1$ , their absolute-value sum is $x / c \leq 1 / c$ ; for $- 1 \leq x \leq - c$ , it is $- x / c \leq 1 / c$ . Equality holds at $x = \pm 1$ , so the root-family cardinal-sum supremum is $1 / c = \sqrt{2}$ .

1.2givenF1F3algebra

The Lobatto nodes are $1, - 1$ , with cardinal polynomials $(1 + x) / 2$ and $(1 - x) / 2$ . Both are nonnegative on $[- 1, 1]$ and sum to $1$ , so their cardinal-sum supremum is $1$ .

2.1givenF2step 1.1step 1.2∎

Applying the operator-norm identity [F2] to the two cardinal-sum calculations gives $Λ_{1}^{R} = \sqrt{2}$ and $Λ_{1}^{L} = 1$ , as claimed.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

An exponential best-error rate transferred to Chebyshev interpolation

Example

Let $f (x) = \exp (x)$ on $[- 1, 1]$ . For every $n \geq 1$ , $E_{n} (f) \leq \frac{e}{(n + 1)!}, ∥ f - I_{n}^{σ} f ∥_{\infty} \leq (1 + C \log (n + 1)) \frac{e}{(n + 1)!}, σ \in {R, L},$ where $C = 4 + (π + 4) / \log 2$ . In particular, both Chebyshev interpolants converge uniformly for this function with the displayed rate.

Facts & Assumptions

Given: $n \geq 1$ , the function $f (x) = \exp (x)$ , and either Chebyshev node family.

[F1]

Best uniform polynomial error and Chebyshev interpolation operators: $E_{n} (f) = \inf_{p \in P_{n}} ∥ f - p ∥_{\infty}$ , and $I_{n}^{σ}$ is its specified interpolation operator.

[F2]

Chebyshev interpolation error is controlled by best polynomial error: $∥ f - I_{n}^{σ} f ∥_{\infty} \leq (1 + Λ_{n}^{σ}) E_{n} (f)$ .

[F3]

Chebyshev-root and Lobatto interpolation norms have logarithmic upper bounds: $Λ_{n}^{σ} \leq C \log (n + 1)$ for $n \geq 1$ .

[F4]

The real exponential function and the number $e$ by a power series: $\exp (x) = \sum_{k = 0}^{\infty} x^{k} / k!$ and $e = \exp (1) = \sum_{k = 0}^{\infty} 1 / k!$ .

[F5]

The exponential series converges absolutely for every real argument: the exponential series converges absolutely for every real argument.

[F6]

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ : $0! = 1$ and $(m + 1)! = (m + 1) m!$ .

[F7]

The natural logarithm as the inverse of the exponential function and The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $\log$ is the natural logarithm and $\log x = \int_{1}^{x} d t / t$ for $x > 0$ .

[F8]

For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ : if $0 < q < 1$ , then $q^{n} \to 0$ .

[F9]

The canonical natural $ι (n) = n \cdot 1_{F}$ of a field and Canonical naturals are positive and strictly increasing: natural indices and factorials in real inequalities are read through their canonical real images, and every positive natural has positive real image.

[F10]

The exponential function is strictly increasing: $\exp$ is continuous on $R$ , so $f \in C [- 1, 1]$ and the quantities in [F1]–[F3] apply.

Verification

1.1givenF1F4F5F6F10algebra

By [F10], $f = \exp$ is continuous on $[- 1, 1]$ . Put $p_{n} (x) = \sum_{k = 0}^{n} x^{k} / k!$ , which belongs to $P_{n}$ . For $∣ x ∣ \leq 1$ , [F4]–[F6] give $∣ \exp (x) - p_{n} (x) ∣ \leq \sum_{m = 0}^{\infty} 1 / (n + 1 + m)! \leq \frac{1}{(n + 1)!} \sum_{m = 0}^{\infty} 1 / m! = e / (n + 1)!$ . The middle inequality follows from $(n + 2) \dots (n + 1 + m) \geq 1 \dots m = m!$ , including the empty product for $m = 0$ . Taking the infimum over $P_{n}$ proves $E_{n} (\exp) \leq e / (n + 1)!$ .

2.1givenF2F3step 1.1algebra

Apply the near-best estimate [F2] and then the norm bound [F3] to step 1.1. This gives $∥ \exp - I_{n}^{σ} \exp ∥_{\infty} \leq (1 + Λ_{n}^{σ}) E_{n} (\exp) \leq (1 + C \log (n + 1)) e / (n + 1)!$ for each $σ \in {R, L}$ .

3.1givenF7F8F9step 2.1algebra∎

By [F7], $\log (n + 1) = \int_{1}^{n + 1} d t / t \leq n$ and $\log 2 = \int_{1}^{2} d t / t > 0$ , so $C > 0$ . For $n \geq 1$ , $(n + 1)! = 2 \cdot 3 \dots (n + 1) \geq 2^{n}$ because this product has $n$ factors, each at least $2$ , so the bound in step 2.1 is at most $e (1 + C n) / 2^{n}$ . For $n \geq 2$ , the ratio of successive terms of $n 2^{- n}$ is $(n + 1) / (2 n) \leq 3 / 4$ , hence induction gives $n 2^{- n} \leq 2 (3 / 4)^{n - 2}$ . The geometric-sequence limit [F8] now shows both $2^{- n}$ and $n 2^{- n}$ tend to zero, so the interpolation errors tend to zero.

Polynomial approximation and Chebyshev interpolation — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Equispaced interpolation of Runge's function diverges

Example

Facts & Assumptions

Proof

Degree-one root and Lobatto interpolation norms

Example

Facts & Assumptions

Proof

An exponential best-error rate transferred to Chebyshev interpolation

Example

Facts & Assumptions

Verification

Sources