LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

Leading composite Simpson error coefficient

Statement

Let $a < b$ , let $k \geq 1$ be an integer, set $n_{k} = 2^{k}$ and $h_{k} = (b - a) / n_{k}$ , and let $Q_{k} = Q_{S} (f; a, b, n_{k})$ for $f \in C^{4} ([a, b])$ . With $I = \int_{a}^{b} f (x) d x$ , one has $I - Q_{k} = - \frac{h_{k}^{4}}{180} \int_{a}^{b} f^{(4)} (x) d x + o (h_{k}^{4}) (k \to \infty) .$ Here $r_{k} = o (h_{k}^{4})$ means $r_{k} / h_{k}^{4} \to 0$ along this sequence. The integral is the Riemann integral.

Facts & Assumptions

Given: A real interval $[a, b]$ with $a < b$ , $f \in C^{4} ([a, b])$ , and the composite Simpson values on the grids with $n_{k} = 2^{k}$ subintervals.

[F1]

Peano kernel identity for one Simpson panel: on a panel $[α, β]$ of length $L$ , the Simpson kernel has the two quartic pieces displayed in its Statement; they agree at the midpoint, satisfy $K \leq 0$ , and have $\int_{α}^{β} ∣ K ∣ = L^{5} / 2880$ . The panel error is $\int_{α}^{β} K (x) f^{(4)} (x) d x$ .

[F2]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $f \in C^{4} ([a, b])$ means $f$ and its derivatives through order four are continuous on the closed interval, in particular both $f$ and $f^{(4)}$ are continuous.

[F3]

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

[F4]

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

[F5]

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

[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$ : for Riemann-integrable $f$ on $[a, b]$ and $a < c < b$ , the restrictions to $[a, c]$ and $[c, b]$ are integrable and $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; iterating this two-piece identity gives additivity over any finite adjacent partition.

[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)$ and 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$ : pointwise bounds pass to integrals, and integrals are linear.

[F8]

If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ : for a constant $q$ , $\int_{α}^{β} q d x = q (β - α)$ .

[F9]

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: sums, scalar multiples, and products of continuous real functions are continuous.

[F10]

Composite Simpson rule on an even uniform grid: for even $n \geq 2$ , $Q_{S}$ is the sum of the one-block Simpson values on the adjacent panels $[x_{2 j}, x_{2 j + 2}]$ , $0 \leq j < n / 2$ .

[F11]

Every complete ordered field is Archimedean: for every real $R$ there is a natural number $N \geq 1$ with $R < N$ .

[F12]

Bernoulli's inequality $(1 + x)^{n} \geq 1 + n x$ : if $x \geq - 1$ and $k \in N$ , then $(1 + x)^{k} \geq 1 + k x$ .

Proof

1.1givenF11F12choosealgebra

Let $δ > 0$ and put $R = (b - a) / δ$ . By [F11] choose $N \geq 1$ with $R < N$ . For every $k \geq N$ , [F12] with $x = 1$ gives $2^{k} \geq 1 + k \geq 1 + N > R$ , so $h_{k} = (b - a) / 2^{k} < δ$ . Since $δ > 0$ was arbitrary, $h_{k} \to 0$ .

1.2givenF1F2F3F4F5F7F9algebra

Put $g = f^{(4)}$ . By [F2] and [F5], both $f$ and $g$ are integrable. By [F3]–[F4], $g$ is uniformly continuous on the compact interval. The two formulas for $K_{j}$ in [F1] agree at their shared midpoint, so $K_{j}$ is continuous; [F9] makes $K_{j} (g - g (c_{j}))$ continuous and [F5] makes it integrable. Fix $ε > 0$ ; choose $δ > 0$ so that $∣ g (x) - g (y) ∣ < ε$ whenever $x, y \in [a, b]$ and $∣ x - y ∣ < δ$ . For $h_{k} < δ$ , write each Simpson block as $P_{j} = [c_{j} - h_{k}, c_{j} + h_{k}]$ with midpoint $c_{j}$ . By [F1] and linearity, its error minus $- ((2 h_{k})^{5} / 2880) g (c_{j})$ is $\int_{P_{j}} K_{j} (x) (g (x) - g (c_{j})) d x$ . Since $K_{j} \leq 0$ and $∣ g (x) - g (c_{j}) ∣ < ε$ , [F7] bounds the absolute value of this difference by $ε (2 h_{k})^{5} / 2880$ .

2.1step 1.1step 1.2

The $δ$ chosen in step 1.2 is positive, so step 1.1 gives an index after which $h_{k} < δ$ ; hence the panel estimate of step 1.2 holds for all sufficiently large $k$ .

3.1givenF5F6F7F8F10step 1.2step 2.1algebra

There are $n_{k} / 2 = (b - a) / (2 h_{k})$ blocks. By [F10], $Q_{k}$ is the sum of their one-block Simpson values; repeated application of additivity [F6] sums their integrals to $I$ . Hence their local errors sum to $I - Q_{k}$ . If $J_{k} = - ((2 h_{k})^{5} / 2880) \sum_{j} g (c_{j})$ , step 1.2 gives $∣ (I - Q_{k}) - J_{k} ∣ \leq (b - a) h_{k}^{4} ε / 180$ . Also, on each block the uniform-continuity bound gives $g (c_{j}) - ε \leq g (x) \leq g (c_{j}) + ε$ . By [F7] and [F8], integrating these constant bounds gives $2 h_{k} (g (c_{j}) \pm ε)$ , so $∣ \int_{P_{j}} g - 2 h_{k} g (c_{j}) ∣ \leq 2 h_{k} ε$ . Repeated additivity [F6] then yields $∣ 2 h_{k} \sum_{j} g (c_{j}) - \int_{a}^{b} g ∣ \leq (b - a) ε$ .

4.1givenstep 3.1algebra∎

Since $J_{k} / h_{k}^{4} = - (2 h_{k} \sum_{j} g (c_{j})) / 180$ , step 3.1 shows that $∣ (I - Q_{k}) / h_{k}^{4} + (1 / 180) \int_{a}^{b} g ∣ \leq (b - a) ε / 90$ for all sufficiently large $k$ . As $ε > 0$ was arbitrary, the displayed limit follows.

Depends on

Used by

Conditional asymptotic validity of the Simpson /15 indicator Theorem

Dependency tree · two levels

82 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., Chapter 13, §13.2 (standard reference, not scraped)
Art B. Owen, Monte Carlo Theory, Methods and Examples, Chapter 7, §7.2 (standard reference, not scraped)
Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, §5.7 (standard reference, not scraped)