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.

✓ 5 results · all verified · 5 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; all 5 also cleared it.

Composite quadrature rules

1 · Prerequisites

2 · Summary

Objective

This page supplies exact uniform-panel midpoint and composite Simpson procedures, their derivative-norm error bounds, and Simpson exactness through cubic degree. The composite trapezoid definition and its matching $C^{2}$ error theorem already have canonical published homes: Composite trapezoidal rule and Second-derivative error bound for the composite trapezoidal rule. They are used here without duplicating their carriers. All bounds concern exact-real quadrature; floating point evaluation and summation error are separate. The midpoint proof uses an explicit nonnegative panel kernel. The Simpson proof supplies its own signed Peano kernel and then sums over the even number of panels.

3 · Logical flowchart

4 · Definitions, theorems and proofs

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Composite midpoint rule on a uniform grid

Definition

Input real endpoints $a, b$ , an integer $n$ , and a function $f$ . If $a \geq b$ or $n < 1$ , return invalid-grid without evaluating $f$ . For the remaining inputs, require a real-valued function $f : [a, b] \to R$ evaluable at every point of $[a, b]$ . Put $h = (b - a) / n$ and $m_{j} = a + (j + \frac{1}{2}) h$ for $0 \leq j < n$ . The composite midpoint rule returns

$Q_{M} (f; a, b, n) : = h \sum_{j < n} f (m_{j}) .$

The sum is the finite sum of Finite sums and finite products, by recursion. The admissibility conditions $a < b$ and $n \geq 1$ ensure $h > 0$ and all $m_{j} \in (a + j h, a + (j + 1) h)$ . The rule is an exact-real formula; floating-point evaluation and summation error are separate from its quadrature error.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Composite Simpson rule on an even uniform grid

Definition

Input real endpoints $a, b$ , an integer $n$ , and an evaluation function $f$ . If $a \geq b$ or $n < 2$ , return invalid-grid without evaluating $f$ . For the remaining inputs require $f : [a, b] \to R$ to be evaluable at every point of $[a, b]$ . If $n$ is odd, the procedure returns invalid-Simpson-panel-count. If $n$ is even, put $h = (b - a) / n$ and $x_{j} = a + j h$ for $0 \leq j \leq n$ ; return

$Q_{S} (f; a, b, n) : = \frac{h}{3} \sum_{j < n / 2} (f (x_{2 j}) + 4 f (x_{2 j + 1}) + f (x_{2 j + 2})) .$

The sum is a finite sum of Finite sums and finite products, by recursion. Each two-panel block $[x_{2 j}, x_{2 j + 2}]$ uses its endpoints and midpoint. Expanding the block sum gives weights $1, 4, 2, \dots, 4, 1$ . The even condition $n \geq 2$ makes the number of blocks a positive integer. The formula is an exact-real procedure; floating point evaluation and summation error are separate from its quadrature error.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Midpoint panel error kernel and second-derivative bound

Statement

Let $a < b$ , $m = (a + b) / 2$ , and $f \in C^{2} ([a, b])$ in the sense of Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ . Define

$K (t) = {\begin{cases} \frac{1}{2} (t - a)^{2}, & a \leq t \leq m, \\ \frac{1}{2} (b - t)^{2}, & m \leq t \leq b . \end{cases}$

Then $K$ is nonnegative and continuous,

$\int_{a}^{b} f (t) d t - (b - a) f (m) = \int_{a}^{b} K (t) f^{''} (t) d t,$

and, with $M_{2} : = \max_{t \in [a, b]} ∣ f^{''} (t) ∣$ ,

$∣ \int_{a}^{b} f (t) d t - (b - a) f (m) ∣ \leq \frac{(b - a)^{3}}{24} M_{2} .$

In particular, if $f^{''} \geq 0$ on $[a, b]$ , the panel midpoint value does not exceed the integral.

Facts & Assumptions

Given: Reals $a < b$ and $f \in C^{2} ([a, b])$ .

[F1]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $C^{2} ([a, b])$ means that $f$ , $f^{'}$ , and $f^{''}$ are continuous on the closed interval, with endpoint derivatives interpreted from within the interval.

[F2]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : for differentiable $u, v$ with integrable derivatives, $\int u v^{'} = [u v] - \int u^{'} v$ on a closed interval.

[F3]

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$ : an integrable function's integral over two adjacent intervals is the sum of the two integrals.

[F4]

Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable: every continuous real function on a closed nondegenerate rectangle in $R^{q}$ , $q \geq 1$ , is Riemann integrable; here $q = 1$ and the rectangle is $[a, b]$ .

[F5]

Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact: the closed interval $[a, b]$ is compact.

[F6]

Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value: a continuous real function on a nonempty compact subset of $R$ attains its maximum and minimum.

[F7]

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)$ : pointwise order between integrable functions on an increasing interval gives the same order between their integrals.

[F8]

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 integral of a scalar multiple of an integrable function is the same scalar multiple of its integral.

[F9]

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 $G$ is differentiable on $[a, b]$ , $G^{'} = g$ , and $g$ is integrable, then $\int_{a}^{b} g = G (b) - G (a)$ .

[F10]

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: constants and the identity are continuous; sums, scalar multiples and products preserve continuity, so every polynomial function and its product with $f^{''}$ are continuous on each interval where the polynomial formula for $K$ applies.

[F11]

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)$ : the derivative of a differentiable composition is the outer derivative at the image multiplied by the inner derivative.

[F12]

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: $(x^{k})^{'} = k x^{k - 1}$ for each integer $k \geq 1$ .

[F13]

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$ : derivatives of sums and scalar multiples are the corresponding sums and scalar multiples of the derivatives.

Proof

1.1givenF1F4F5F6F10construct

By [F1], $f^{''}$ is continuous and $[a, b]$ is compact by [F5], so [F6] gives the finite maximum $M_{2} = \max_{[a, b]} ∣ f^{''} ∣$ . Each formula for $K$ is polynomial and hence continuous by [F10]; the two formulas agree at $m$ , so $K$ is continuous on $[a, b]$ and nonnegative on both halves. Thus $K f^{''}$ is continuous by [F10], and $f$ , $K$ , $K f^{''}$ , and their restrictions are integrable by [F4].

2.1givenF1F2F4step 1.1

On $[a, m]$ , $K (a) = K^{'} (a) = 0$ , $K (m) = (b - a)^{2} / 8$ , $K^{'} (m) = (b - a) / 2$ , and $K^{''} = 1$ inside; applying [F2] first to $u = K, v = f^{'}$ and then to $u = K^{'}, v = f$ gives $\int_{a}^{m} K f^{''} = K (m) f^{'} (m) - K^{'} (m) f (m) + \int_{a}^{m} f$ , with all hypotheses valid because $K$ is polynomial on this half and $f \in C^{2}$ .

2.2givenF1F2F4step 1.1

On $[m, b]$ , $K (b) = K^{'} (b) = 0$ , $K (m) = (b - a)^{2} / 8$ , $K^{'} (m) = - (b - a) / 2$ , and $K^{''} = 1$ inside; the same two applications of [F2] give $\int_{m}^{b} K f^{''} = - K (m) f^{'} (m) + K^{'} (m) f (m) + \int_{m}^{b} f$ .

3.1step 2.1step 2.2F3algebra

Adding steps 2.1 and 2.2 cancels the $f^{'} (m)$ terms, sums the $f (m)$ terms to $- (b - a) f (m)$ , and by additivity [F3] yields $\int_{a}^{b} K f^{''} = \int_{a}^{b} f - (b - a) f (m)$ .

4.1step 1.1step 3.1F3F4F7F8F9F11F12F13algebra∎

The chain rule [F11], power rule [F12], and scalar rule [F13] show that $(t - a)^{3} / 6$ is an antiderivative of the left formula for $K$ , and $- (b - t)^{3} / 6$ is an antiderivative of the right formula. The FTC [F9] therefore gives $\int_{a}^{m} K = (m - a)^{3} / 6 = (b - a)^{3} / 48$ and $\int_{m}^{b} K = (b - m)^{3} / 6 = (b - a)^{3} / 48$ ; additivity [F3] gives $\int_{a}^{b} K = (b - a)^{3} / 24$ . Since $0 \leq K$ and $∣ f^{''} ∣ \leq M_{2}$ , one has $- M_{2} K \leq K f^{''} \leq M_{2} K$ ; monotonicity [F7] and linearity [F8] give $∣ \int_{a}^{b} K f^{''} ∣ \leq M_{2} \int_{a}^{b} K = M_{2} (b - a)^{3} / 24$ , and if $f^{''} \geq 0$ they also give $\int_{a}^{b} K f^{''} \geq 0$ . Step 3.1 transfers the bound and sign to the midpoint error.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Composite midpoint error bound for a twice continuously differentiable function

Statement

Let $a < b$ , let $n \geq 1$ be an integer, and put $h = (b - a) / n$ . If $f \in C^{2} ([a, b])$ , define $M_{2} = \max_{x \in [a, b]} ∣ f^{''} (x) ∣$ . The composite midpoint value $Q_{M} (f; a, b, n)$ of Composite midpoint rule on a uniform grid satisfies

$∣ \int_{a}^{b} f (x) d x - Q_{M} (f; a, b, n) ∣ \leq \frac{(b - a) h^{2}}{24} M_{2} .$

The integral is the Riemann integral. This is an exact-arithmetic quadrature bound; evaluation and summation roundoff are not included.

Facts & Assumptions

Given: Reals $a < b$ , an integer $n \geq 1$ , $h = (b - a) / n$ , and $f \in C^{2} ([a, b])$ .

[F1]

Composite midpoint rule on a uniform grid: $Q_{M}$ is the sum of the values at the $n$ panel midpoints, each multiplied by $h$ .

[F2]

Midpoint panel error kernel and second-derivative bound: on a panel of length $h$ , the difference between its integral and its midpoint value times $h$ has absolute value at most $M_{2} h^{3} / 24$ .

[F3]

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$ : the integral over a finite partition is the sum of the integrals over its adjacent panels.

[F4]

Triangle inequality for finite sums: the absolute value of a finite sum is at most the sum of the absolute values.

Proof

1.1givenF2construct

Put $x_{j} = a + j h$ and $m_{j} = (x_{j} + x_{j + 1}) / 2$ for $0 \leq j < n$ . Each panel $[x_{j}, x_{j + 1}]$ has length $h$ and inherits the $C^{2}$ restriction of $f$ ; $\max_{[x_{j}, x_{j + 1}]} ∣ f^{''} ∣ \leq M_{2}$ . By [F2], its midpoint error $E_{j}$ obeys $∣ E_{j} ∣ \leq M_{2} h^{3} / 24$ .

2.1step 1.1F1F3algebra

Repeated application of [F3] gives $\int_{a}^{b} f = \sum_{j = 0}^{n - 1} \int_{x_{j}}^{x_{j + 1}} f$ . By [F1], $Q_{M} = h \sum_{j = 0}^{n - 1} f (m_{j})$ , so subtraction gives $\int_{a}^{b} f - Q_{M} = \sum_{j = 0}^{n - 1} E_{j}$ .

3.1step 1.1step 2.1F4algebra∎

The finite-sum triangle inequality [F4] and step 1.1 yield $∣ \int_{a}^{b} f - Q_{M} ∣ \leq \sum_{j = 0}^{n - 1} ∣ E_{j} ∣ \leq n M_{2} h^{3} / 24$ . Since $n h = b - a$ , this is the claimed bound.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Peano kernel identity for one Simpson panel

Statement

Let $a < b$ , put $L = b - a$ and $m = (a + b) / 2$ , and let $f \in C^{4} ([a, b])$ . Define the one-block Simpson value and its kernel by

$S (f; a, b) : = \frac{L}{6} (f (a) + 4 f (m) + f (b)), K_{a, b} (x) : = {\begin{cases} \frac{(x - a)^{3} (3 (x - a) - 2 L)}{72}, & a \leq x \leq m, \\ \frac{(b - x)^{3} (3 (b - x) - 2 L)}{72}, & m \leq x \leq b . \end{cases}$

Then

$\int_{a}^{b} f (x) d x - S (f; a, b) = \int_{a}^{b} K_{a, b} (x) f^{(4)} (x) d x,$

and $K_{a, b} \leq 0$ with $\int_{a}^{b} ∣ K_{a, b} (x) ∣ d x = L^{5} / 2880$ . The value $S (f; a, b)$ is the one-block specialization of Composite Simpson rule on an even uniform grid.

Facts & Assumptions

Given: Reals $a < b$ , $L = b - a$ , $m = (a + b) / 2$ , and $f \in C^{4} ([a, b])$ .

[F1]

Composite Simpson rule on an even uniform grid: on two subintervals of equal width $L / 2$ , the Simpson output is $\frac{L}{6} (f (a) + 4 f (m) + f (b))$ .

[F2]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $C^{4} ([a, b])$ means all derivatives through order four exist and are continuous, with endpoint derivatives taken from within the interval.

[F3]

[F4]

Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable: every continuous function on a closed nondegenerate interval is Riemann integrable.

[F5]

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)$ : an integrable derivative has integral equal to the endpoint increment of its antiderivative.

[F6]

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: constants and the identity are continuous; sums, scalar multiples and products preserve continuity, so the polynomial pieces of $K_{a, b}$ and their products with $f^{(4)}$ are continuous on each half-panel.

[F7]

[F8]

[F9]

[F10]

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$ : the integral over two adjacent closed subintervals is the sum of their integrals.

Proof

1.1givenF2F4F6algebra

On the left half, $K_{a, b} (x) = (3 y^{4} - 2 L y^{3}) / 72$ with $y = x - a$ ; hence $K^{(4)} = 1$ , $K (a) = K^{'} (a) = K^{''} (a) = 0$ , and at $m$ its value and first two derivatives are $- L^{4} / 1152$ , $0$ , and $L^{2} / 24$ , while $K^{'''} (m -) = L / 3$ . The right-half formula gives $K^{(4)} = 1$ , $K (b) = K^{'} (b) = K^{''} (b) = 0$ , and $K^{'''} (m +) = - L / 3$ . Thus $K, K^{'}, K^{''}$ match at $m$ . Each polynomial formula for $K$ and its product with the continuous $f^{(4)}$ is continuous on its closed half by [F2] and [F6]. Both formulas agree at $m$ , so $K$ and $K f^{(4)}$ are continuous on $[a, b]$ ; also $f$ is continuous by [F2]. These functions and their restrictions are integrable by [F4].

2.1F1F2F3F4F6F10step 1.1algebra

On each closed half, every derivative $K^{(r)}$ for $0 \leq r \leq 4$ is polynomial and continuous by [F6], and every $f^{(s)}$ for $0 \leq s \leq 4$ is continuous by [F2]. They are all integrable by [F4], so the four applications of integration by parts [F3] satisfy their derivative-integrability hypotheses. They give $\int K_{a, b} f^{(4)} = [B] + \int f$ , where $B = K f^{'''} - K^{'} f^{''} + K^{''} f^{'} - K^{'''} f$ and the bracket is the endpoint difference for that half. Summing the brackets, the terms at $m$ involving $K, K^{'}, K^{''}$ cancel, while the jump in $K^{'''}$ contributes $- 2 L f (m) / 3$ ; the outer endpoints contribute $- L (f (a) + f (b)) / 6$ . Additivity [F10] combines both half-integrals of $K f^{(4)}$ and of $f$ ; the remaining integral is $\int_{a}^{b} f$ because $K^{(4)} = 1$ . By [F1], this is precisely $\int_{a}^{b} f - S (f; a, b)$ , proving the identity.

3.1F5F7F8F9F10step 1.1algebra∎

Since $0 \leq x - a \leq L / 2$ on the left half, $3 (x - a) - 2 L < 0$ , so $K_{a, b} \leq 0$ there; the right formula gives the same sign. Define $H (x) = \frac{3}{5} (x - a)^{5} - \frac{L}{2} (x - a)^{4}$ on $[a, m]$ . The power rule [F7], chain rule [F9], and sum/scalar rules [F8] give $H^{'} (x) = 3 (x - a)^{4} - 2 L (x - a)^{3}$ . By the FTC [F5], additivity [F10], and symmetry of the two kernel pieces, and $H (m) - H (a) = - L^{5} / 80$ , $\int_{a}^{b} ∣ K_{a, b} ∣ = - 2 (H (m) - H (a)) / 72 = L^{5} / 2880$ .

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Composite Simpson rule is exact through cubic degree

Statement

Let $a < b$ , let $n \geq 2$ be an even integer, and let $p (x) = c_{0} + c_{1} x + c_{2} x^{2} + c_{3} x^{3}$ with real coefficients. Then

$\int_{a}^{b} p (x) d x = Q_{S} (p; a, b, n),$

where $Q_{S}$ is the composite Simpson value of Composite Simpson rule on an even uniform grid.

Facts & Assumptions

Given: Reals $a < b$ , an even integer $n \geq 2$ , and $p (x) = c_{0} + c_{1} x + c_{2} x^{2} + c_{3} x^{3}$ .

[F1]

Composite Simpson rule on an even uniform grid: the composite value is $\frac{h}{3} \sum_{j < n / 2} (f (x_{2 j}) + 4 f (x_{2 j + 1}) + f (x_{2 j + 2}))$ .

[F2]

Peano kernel identity for one Simpson panel: on a panel, the error equals the integral of its Peano kernel times the fourth derivative.

[F3]

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$ : the integral over the partition is the sum of the integrals over its adjacent blocks.

[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: for $k \geq 1$ , $(x^{k})^{'} = k x^{k - 1}$ , and $x^{0}$ has derivative zero.

[F5]

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$ : sums and scalar multiples of differentiable functions have the corresponding derivatives.

[F6]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $p \in C^{4} ([a, b])$ requires that $p$ and its derivatives through order four exist and are continuous on $[a, b]$ .

[F7]

Proof

1.1givenF4F5F6F7algebra

Repeated use of [F4] and the sum/scalar rules in [F5] gives, for every real $x$ , $p^{'} (x) = c_{1} + 2 c_{2} x + 3 c_{3} x^{2}, p^{''} (x) = 2 c_{2} + 6 c_{3} x, p^{'''} (x) = 6 c_{3}, p^{(4)} (x) = 0.$ These formulas establish existence of all derivatives through order four, including their restrictions to the endpoints with the one-sided convention. Each of $p, p^{'}, p^{''}, p^{'''}$ and $p^{(4)}$ is a polynomial function, hence continuous by [F7]. Thus $p \in C^{4} ([a, b])$ by [F6], and $p^{(4)} \equiv 0$ .

2.1step 1.1F2

For every block $[x_{2 j}, x_{2 j + 2}]$ , the restriction of $p$ is $C^{4}$ and has fourth derivative zero. The Peano-kernel identity [F2] makes that block's Simpson error $\int_{x_{2 j}}^{x_{2 j + 2}} K_{x_{2 j}, x_{2 j + 2}} (x) 0 d x = 0$ .

3.1step 2.1F1F3algebra∎

By [F3], summing the exact block integrals gives $\int_{a}^{b} p$ . Summing the block Simpson values from [F1], each endpoint appears once, each odd interior node appears with coefficient $4$ , and each even interior node appears with coefficient $2$ . This is exactly the composite formula [F1], so the global rule is exact.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Composite Simpson error bound for a four-times continuously differentiable function

Statement

Let $a < b$ , let $n \geq 2$ be an even integer, and put $h = (b - a) / n$ . If $f \in C^{4} ([a, b])$ , set $M_{4} = \max_{x \in [a, b]} ∣ f^{(4)} (x) ∣$ . Then the value $Q_{S} (f; a, b, n)$ of Composite Simpson rule on an even uniform grid satisfies

$∣ \int_{a}^{b} f (x) d x - Q_{S} (f; a, b, n) ∣ \leq \frac{(b - a) h^{4}}{180} M_{4} .$

The integral is the Riemann integral. This is an exact-arithmetic quadrature bound; evaluation and summation roundoff are not included.

Facts & Assumptions

Given: Reals $a < b$ , an even integer $n \geq 2$ , $h = (b - a) / n$ , and $f \in C^{4} ([a, b])$ .

[F1]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $C^{4} ([a, b])$ makes $f^{(4)}$ continuous on the closed interval.

[F2]

Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact: every closed bounded interval $[a, b]$ is compact.

[F3]

[F4]

Composite Simpson rule on an even uniform grid: the composite value is the sum, over $j < n / 2$ , of $\frac{h}{3} (f (x_{2 j}) + 4 f (x_{2 j + 1}) + f (x_{2 j + 2}))$ .

[F5]

Peano kernel identity for one Simpson panel: on a panel of length $L$ , the Simpson error is $\int K f^{(4)}$ , where $K \leq 0$ and $\int ∣ K ∣ = L^{5} / 2880$ .

[F6]

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$ : the integral over a finite partition is the sum of its integrals over the adjacent panels.

[F7]

Triangle inequality for finite sums: the absolute value of a finite sum is at most the sum of the absolute values.

[F8]

[F9]

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$ : scalar multiples of integrable functions are integrable and their integrals scale by that scalar.

Proof

1.1givenF1F2F3F4F5F8F9construct

By [F1], $f^{(4)}$ is continuous. The interval is compact by [F2], so [F3] gives $M_{4} = \max_{[a, b]} ∣ f^{(4)} ∣ < \infty$ . For each $j = 0, \dots, n / 2 - 1$ , put $u = x_{2 j}$ and $L = 2 h$ . The local rule from [F4] is $S (f; u, u + L)$ ; by [F5], its error is $E_{j} = \int_{u}^{u + L} K_{u, u + L} f^{(4)}$ and $\int_{u}^{u + L} ∣ K_{u, u + L} ∣ = (2 h)^{5} / 2880$ . Since $K_{u, u + L} \leq 0$ , its absolute value equals its negative, hence is integrable by [F5] and [F9]. The integrable functions satisfy $- M_{4} ∣ K_{u, u + L} ∣ \leq K_{u, u + L} f^{(4)} \leq M_{4} ∣ K_{u, u + L} ∣$ . Monotonicity [F8] and scalar linearity [F9] therefore give $∣ E_{j} ∣ \leq M_{4} \int_{u}^{u + L} ∣ K_{u, u + L} ∣ = M_{4} (2 h)^{5} / 2880$ .

2.1step 1.1F4F6algebra

Additivity [F6] gives $\int_{a}^{b} f$ as the sum of the local panel integrals. Summing the local Simpson expressions in [F4], each interior even-indexed value appears in two adjacent blocks and each odd-indexed value appears once; hence their sum is exactly $Q_{S} (f; a, b, n)$ . Therefore the global error is $\sum_{j = 0}^{n / 2 - 1} E_{j}$ .

3.1step 1.1step 2.1F7algebra∎

The finite-sum triangle inequality [F7] yields $∣ \sum_{j} E_{j} ∣ \leq (n / 2) M_{4} (2 h)^{5} / 2880 = n M_{4} h^{5} / 180$ . Using $n h = b - a$ gives the stated bound.

5 · Examples, counterexamples and false statements

None yet.

Composite quadrature rules

1 · Prerequisites

2 · Summary

Objective

3 · Logical flowchart

4 · Definitions, theorems and proofs

Composite midpoint rule on a uniform grid

Definition

Composite Simpson rule on an even uniform grid

Definition

Midpoint panel error kernel and second-derivative bound

Statement

Facts & Assumptions

Proof

Composite midpoint error bound for a twice continuously differentiable function

Statement

Facts & Assumptions

Proof

Peano kernel identity for one Simpson panel

Statement

Facts & Assumptions

Proof

Composite Simpson rule is exact through cubic degree

Statement

Facts & Assumptions

Proof

Composite Simpson error bound for a four-times continuously differentiable function

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources