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.

Peano representation and L1 error bound

Statement

Let $a < b$ , let $x_{1}, \dots, x_{s} \in [a, b]$ and $w_{1}, \dots, w_{s} \in R$ define the finite quadrature $Q$ and residual $L$ of Peano kernel of a finite quadrature functional, and let $r \in N$ with $r \geq 1$ . Assume $L$ vanishes on the evaluation functions of the zero polynomial and every nonzero formal polynomial of degree at most $r - 1$ , and let $f \in C^{r} ([a, b])$ . For the kernel $K_{r} (t) = L (g_{r, t})$ of Peano kernel of a finite quadrature functional, $L (f) = \int_{a}^{b} K_{r} (t) f^{(r)} (t) d t, ∣ L (f) ∣ \leq (\int_{a}^{b} ∣ K_{r} (t) ∣ d t) ∥ f^{(r)} ∥_{\infty} .$

Facts & Assumptions

Given: A nondegenerate interval $[a, b]$ , a finite real weighted quadrature exact on $P_{r - 1}$ , an integer $r \geq 1$ , and $f \in C^{r} ([a, b])$ .

[A1]

$a < b$ , $r \in N$ with $r \geq 1$ , $L$ vanishes on the evaluation functions of the zero polynomial and every nonzero formal polynomial of degree at most $r - 1$ , and $f$ has continuous derivatives through order $r$ .

[F1]

Peano kernel of a finite quadrature functional: $L (f) = \int_{a}^{b} f - \sum_{i} w_{i} f (x_{i})$ and $K_{r} (t) = L (g_{r, t})$ , where $g_{r, t} (x) = (x - t)_{+}^{r - 1} / (r - 1)!$ for $r \geq 2$ and $g_{1, t} (x) = 1_{{x > t}}$ ; the factorial image is positive and invertible.

[F2]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $f \in C^{r} ([a, b])$ has continuous derivatives through order $r$ , including one-sided endpoint derivatives.

[F3]

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)$ : for a continuous derivative, integration over $[a, x]$ equals the endpoint increment of a primitive.

[F4]

For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, 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 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$ : polynomial powers and their products with derivatives obey the usual differentiation rules on each interval; together with FTC these give the integration-by-parts identity used below.

[F5]

A continuous function on a closed rectangle has repeated Riemann integrals in every coordinate order, all equal to its multiple integral: a continuous function on a closed rectangle has equal repeated Riemann integrals in either coordinate order.

[F6]

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$ and For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ : integrals are linear and additive over adjacent intervals. The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ supplies the natural factorials; their canonical real images in real denominators are the convention fixed by [F1].

[F7]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: continuous functions on closed intervals are Riemann-integrable.

[F8]

Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous: a continuous function on a compact metric rectangle is uniformly continuous.

[F9]

Changing an integrable function at finitely many points changes neither its integrability nor its integral: changing finitely many values preserves Riemann integrability and leaves the integral unchanged.

[F10]

If $f, g$ are integrable on $[a, b]$ then so are $∣ f ∣$ , $f^{2}$ , $f g$ , $\max (f, g)$ and $\min (f, g)$ , and $∣ \int_{a}^{b} f ∣ \leq \int_{a}^{b} ∣ f ∣$ and 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)$ : products and absolute values of integrable functions are integrable, and pointwise order passes to their integrals.

[F11]

For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent: every continuous real function on the compact interval $[a, b]$ is bounded and attains its extrema.

Proof

1.1givenF2F3F4inductionalgebra

We first establish Taylor's integral remainder by induction on the natural order $q$ (The principle of mathematical induction). For $r = 1$ , [F3] gives $f (x) = f (a) + \int_{a}^{x} f^{'} (t) d t$ . If the remainder formula holds at order $q \geq 1$ , put $u (t) : = (x - t)^{q} / q!$ . The product rule and FTC give $\int_{a}^{x} u^{'} (t) f^{(q)} (t) d t = [u (t) f^{(q)} (t)]_{a}^{x} - \int_{a}^{x} u (t) f^{(q + 1)} (t) d t$ , and $u^{'} (t) = - (x - t)^{q - 1} / (q - 1)!$ . Rearranging yields $\int_{a}^{x} \frac{(x - t)^{q - 1}}{(q - 1)!} f^{(q)} (t) d t = \frac{(x - a)^{q}}{q!} f^{(q)} (a) + \int_{a}^{x} \frac{(x - t)^{q}}{q!} f^{(q + 1)} (t) d t .$ Thus induction yields $f (x) = \sum_{j = 0}^{r - 1} f^{(j)} (a) (x - a)^{j} / j! + \int_{a}^{x} (x - t)^{r - 1} f^{(r)} (t) / (r - 1)! d t$ .

2.1givenA1F1F6step 1.1

Extend the last integral to $[a, b]$ by setting its kernel to zero when $t \geq x$ . With $P_{r - 1} (x) : = \sum_{j = 0}^{r - 1} f^{(j)} (a) (x - a)^{j} / j!$ , the result is $f (x) = P_{r - 1} (x) + \int_{a}^{b} g_{r, t} (x) f^{(r)} (t) d t$ . Since $P_{r - 1}$ is zero or has degree at most $r - 1$ , [A1] gives $L (P_{r - 1}) = 0$ .

3.1givenF1F2F5F6F7F8step 2.1

Suppose first that $r \geq 2$ . The function $(x, t) \mapsto g_{r, t} (x) f^{(r)} (t)$ is continuous on $[a, b]^{2}$ because $r - 1 \geq 1$ and $f^{(r)}$ is continuous. By [F5]–[F7], applying the integral part of $L$ to step 2.1 and interchanging the two rectangle integrals gives $\int_{a}^{b} (\int_{a}^{b} g_{r, t} (x) d x) f^{(r)} (t) d t$ . Each finite evaluation term of $Q$ commutes with the $t$ -integral by [F6]. Therefore $L (f) = \int_{a}^{b} L (g_{r, t}) f^{(r)} (t) d t = \int_{a}^{b} K_{r} (t) f^{(r)} (t) d t$ . The function $(x, t) \mapsto g_{r, t} (x)$ is uniformly continuous on the compact square by [F8], so its $x$ -integral and its finite weighted evaluations vary continuously with $t$ ; hence $K_{r}$ is continuous and integrable.

3.2givenF1F3F4F6F7F9F10step 2.1algebra

If $r = 1$ , exactness on constants gives $\sum_{i} w_{i} = b - a$ . For $t$ outside the finite node set, [F1] gives $K_{1} (t) = (b - t) - \sum_{x_{i} > t} w_{i}$ . It is bounded and affine between consecutive nodes. Extend each affine piece continuously to its closed subinterval; the resulting pieces are integrable by [F7] and add to an integrable piecewise function by [F6]. The kernel differs from that function at only finitely many nodes, so it is integrable and has the same integral by [F9]. Since $f^{'}$ is continuous, [F10] makes $K_{1} f^{'}$ integrable; changing the kernel values at the finite node set does not change that product integral by [F9]. By [F3]–[F4] and integration by parts, $\int_{a}^{b} (b - t) f^{'} (t) d t = \int_{a}^{b} f (t) d t - (b - a) f (a)$ , while $\sum_{i} w_{i} \int_{a}^{x_{i}} f^{'} (t) d t = Q (f) - (b - a) f (a)$ . Subtracting gives $\int_{a}^{b} K_{1} (t) f^{'} (t) d t = L (f)$ .

4.1givenF2F10F11step 3.1step 3.2algebra∎

By [F2] and [F11], $f^{(r)}$ is bounded on $[a, b]$ , so $∥ f^{(r)} ∥_{\infty} < \infty$ . In either case, the kernel is integrable and $∣ K_{r} ∣$ is integrable by [F10]. Apply monotonicity in [F10] to $- ∣ K_{r} ∣ ∥ f^{(r)} ∥_{\infty} \leq K_{r} f^{(r)} \leq ∣ K_{r} ∣ ∥ f^{(r)} ∥_{\infty}$ , and use the representation in step 3.1 or 3.2. This gives the asserted bound.

Depends on

Used by

Peano remainder bound for the eight-panel rule Corollary

Dependency tree · two levels

102 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.2 (standard reference, not scraped)