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

Pointwise Lagrange interpolation remainder

Statement

Let $n \in N$ , $n \geq 0$ , let $a < b$ , let $x_{0} < \dots < x_{n}$ lie in $[a, b]$ , and let $f \in C^{n + 1} ([a, b], R)$ with the convention of Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ . Put $p = I_{n} f$ and $ω_{n} (X) = \prod_{j = 0}^{n} (X - x_{j})$ as in Cardinal-polynomial interpolation. If $x = x_{j}$ for a node, then $f (x) - p (x) = 0$ . If $x \in [a, b]$ is not a node, there is $ξ \in (\min {x, x_{0}}, \max {x, x_{n}})$ such that $f (x) - p (x) = \frac{f^{(n + 1)} (ξ)}{(n + 1)!_{R}} ω_{n} (x),$ where $(n + 1)!_{R} : = \prod_{j = 1}^{n + 1} j$ , with each natural factor read as its canonical real image under The canonical natural $ι (n) = n \cdot 1_{F}$ of a field.

Facts & Assumptions

Given: A natural $n \geq 0$ , a nondegenerate closed interval $[a, b]$ , distinct nodes $x_{0} < \dots < x_{n}$ in that interval, $f \in C^{n + 1} ([a, b], R)$ , and a query $x \in [a, b]$ .

[F1]

Cardinal-polynomial interpolation: $ω_{n} (X) = \prod_{j = 0}^{n} (X - x_{j})$ , $ℓ_{j} (X) = \prod_{k \neq j} (X - x_{k}) / (x_{j} - x_{k})$ , and $I_{n} f = \sum_{j = 0}^{n} f (x_{j}) ℓ_{j}$ .

[F2]

Existence and uniqueness of the cardinal-polynomial interpolant: $I_{n} f$ is a polynomial of degree at most $n$ and satisfies $I_{n} f (x_{j}) = f (x_{j})$ at every node.

[F3]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $f \in C^{n + 1} ([a, b])$ means its derivatives through order $n + 1$ exist on $[a, b]$ (one-sided at endpoints) and are continuous there.

[F4]

Higher-order Rolle theorem: if $m \in N$ , $m \geq 1$ , $z_{0} < \dots < z_{m}$ , $g$ is continuous on $[z_{0}, z_{m}]$ , $m$ -times differentiable on $(z_{0}, z_{m})$ , and $g (z_{j}) = 0$ for all $j$ , then $g^{(m)} (η) = 0$ for some $η \in (z_{0}, z_{m})$ .

[F5]

The highest derivative of a polynomial: if $q (X) = \sum_{k = 0}^{m} a_{k} X^{k}$ has degree at most $m$ , then $q^{(m)} (t) = a_{m} m!_{R}$ ; the coefficient $a_{m}$ is zero when $\deg q < m$ , and it is $1$ when $q$ is monic of degree $m$ .

[F6]

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$ : at a limit point of a common domain, sums and scalar multiples of differentiable functions are differentiable with the sum and scalar-multiple derivative rules; the hypotheses and conclusion also apply to their restrictions to intervals.

[F7]

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: polynomial functions are continuous on their domain, and finite sums and scalar multiples of continuous functions are continuous.

[F8]

Cardinal interpolation functions are polynomials of the stated degrees: $I_{n} f$ is a polynomial function of degree at most $n$ , $ω_{n}$ is monic of degree $n + 1$ , and $ω_{n} (x) \neq 0$ off the nodes.

[F9]

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ and Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ : the real product $m!_{R} = \prod_{j = 1}^{m} j$ is the canonical real image of the nonzero natural factorial $m!$ ; thus it is nonzero, and The reals form a field supplies its inverse.

Proof

1.1givenF2algebra

If $x = x_{j}$ for some node, [F2] gives $p (x) = f (x)$ , so the error is zero.

1.2givenF1F2F8construct

Suppose $x$ is not a node. By [F8], $ω_{n} (x) \neq 0$ , so set $c = (f (x) - p (x)) / ω_{n} (x)$ and define $g (t) = f (t) - p (t) - c ω_{n} (t)$ on $[a, b]$ . At every node $x_{j}$ , [F2] gives $f (x_{j}) = p (x_{j})$ and [F1] gives $ω_{n} (x_{j}) = 0$ , so $g (x_{j}) = 0$ ; by the choice of $c$ , also $g (x) = 0$ .

1.3F5F8algebra

By [F8], $ω_{n}$ is monic of degree $n + 1$ and $p$ has degree at most $n$ , so their coefficients at degree $n + 1$ are respectively $1$ and $0$ . Applying [F5] to these two polynomials gives $p^{(n + 1)} (ξ) = 0$ and $ω_{n}^{(n + 1)} (ξ) = (n + 1)!_{R}$ .

2.1givenstep 1.2F3F4F5F6F7F8choose

Sort the $n + 2$ distinct points consisting of the nodes and $x$ as $z_{0} < \dots < z_{n + 1}$ . The function $f$ is $C^{n + 1}$ by [F3]; $p$ has degree at most $n$ and $ω_{n}$ has degree $n + 1$ by [F8]. Their iterated derivatives through order $n + 1$ exist by [F5]. Repeated application of the sum and scalar-multiple rules [F6] shows that $g$ is $(n + 1)$ -times differentiable on $(z_{0}, z_{n + 1})$ . Also, $f$ is continuous by [F3], the polynomial functions $p$ and $ω_{n}$ are continuous by [F7], and the finite linear combination defining $g$ is continuous on $[z_{0}, z_{n + 1}]$ by [F7]. Apply [F4] with $m = n + 1$ to the zeros from step 1.2. This yields $ξ \in (z_{0}, z_{n + 1})$ with $g^{(n + 1)} (ξ) = 0$ .

3.1step 2.1step 1.3F6F9algebra

Differentiate the defining identity for $g$ $n + 1$ times at $ξ$ . Step 2.1 licenses these derivatives and [F6] preserves the linear combination, so $0 = g^{(n + 1)} (ξ) = f^{(n + 1)} (ξ) - c (n + 1)!_{R}$ . By [F9] the factorial factor is nonzero, so $c = f^{(n + 1)} (ξ) / (n + 1)!_{R}$ .

4.1step 1.2step 2.1step 3.1algebra∎

Substituting the value of $c$ into its definition in step 1.2 gives the claimed remainder formula. Since $z_{0} = \min {x, x_{0}}$ and $z_{n + 1} = \max {x, x_{n}}$ , $ξ$ lies in the stated interval.

Depends on

Used by

Dependency tree · two levels

70 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

Mark Embree, Lecture Notes on Numerical Analysis, lecture 3 (standard reference, not scraped)
Jean-Paul Berrut and Lloyd N. Trefethen, Barycentric Lagrange Interpolation (standard reference, not scraped)