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 · 3 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 3 also cleared it.

Composite quadrature rules — Examples

1 · Prerequisites

2 · Summary

Objective

For convex data with a defined Riemann integral, convexity brackets the integral between midpoint and trapezoid values. The page also verifies exact Simpson values on a quadratic and a cubic over a complete two-panel block. The examples use the exact-arithmetic conventions of the A page.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

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

Convex data bracket the integral between composite midpoint and trapezoid values

Example

Let $f : [a, b] \to R$ be convex and Darboux integrable on $[a, b]$ , with $a < b$ , and let $n \geq 1$ be an integer. Then

$Q_{M} (f; a, b, n) \leq \int_{a}^{b} f (x) d x \leq T_{n} (f),$

where $Q_{M}$ is the composite midpoint value and $T_{n} (f)$ is the published composite trapezoidal value of Composite trapezoidal rule on the same interval and uniform grid. Darboux integrability is the explicit premise that makes the displayed Riemann integral defined. The proof uses convexity directly for both inequalities and assumes no differentiability.

Facts & Assumptions

Given: Reals $a < b$ , an integer $n \geq 1$ , and a convex Darboux-integrable $f : [a, b] \to R$ .

[F1]

Convex, strictly convex, concave, strictly concave, and midpoint-convex real functions on an interval: convexity means $f (λ x + (1 - λ) y) \leq λ f (x) + (1 - λ) f (y)$ for $0 \leq λ \leq 1$ .

[F2]

The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ , The Darboux and Riemann definitions agree: a bounded $f$ on $[a, b]$ is Darboux integrable with integral $I$ if and only if for every real $ε > 0$ there is a real $δ > 0$ such that $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged partition of mesh below $δ$ , For bounded $f$ on $[a, b]$ and a partition $P$ : the infimum $m_{i}$ and supremum $M_{i}$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L (f, P) = \sum_{i} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ , and Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions: Darboux integrability means the lower and upper integrals agree, and this integral agrees with the tagged-Riemann definition.

[F3]

A finite sum is unchanged by a permutation of its index range: $\sum_{k < n} a_{π (k)} = \sum_{k < n} a_{k}$ for every bijection $π : n \to n$ : reordering a finite list of terms by a permutation does not change its sum.

[F4]

Composite midpoint rule on a uniform grid: the composite midpoint value is the sum of the panel midpoint values multiplied by the common width $h$ .

[F5]

Composite trapezoidal rule: the composite value is $h$ times the sum of endpoint values with half weights and interior node values with unit weights.

[F6]

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 of integrable functions on an increasing interval implies the same order for their integrals.

[F7]

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$ : sums and scalar multiples of integrable functions are integrable, and their integrals are linear.

[F8]

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 remains integrable on subintervals, and its integral adds over adjacent subintervals.

[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: affine functions and polynomials are continuous.

[F10]

Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable: every continuous function on a closed interval (the case $q = 1$ ) is Riemann integrable.

[F11]

[F12]

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$ : the sum, scalar-multiple, and product rules give the corresponding derivatives.

[F13]

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.

Verification

1.1F2F3F8construct

Fix a panel $[u, v] = [x_{j}, x_{j + 1}]$ , write $h = v - u$ and $m = (u + v) / 2$ , and let $g (x) : = f (u + v - x)$ . The restriction of $f$ to this panel is integrable by [F8]. Reflect any partition of $[u, v]$ about $m$ and reverse the order of its nodes; this gives an involution on the set of partitions. Each reflected subinterval has the same length and the same range values of $g$ as the corresponding original subinterval has for $f$ . Thus the lower and upper Darboux sums agree after reversing their finite lists of terms, by [F3]. Since the reflected partitions run through all partitions, [F2] shows that $g$ is integrable and $\int_{u}^{v} g = \int_{u}^{v} f$ .

1.2givenF1F5F6F8F9F10F11F12F13algebra

For each panel put $u = x_{j}$ , $v = x_{j + 1}$ and $h = v - u$ , and define the endpoint chord $L_{j} (x) : = \frac{v - x}{h} f (u) + \frac{x - u}{h} f (v)$ . For $x \in [u, v]$ , the coefficients are in $[0, 1]$ and sum to $1$ , so [F1] gives $f (x) \leq L_{j} (x)$ . The functions are integrable by the given premise and by continuity of the affine chord [F9] with [F10]. Monotonicity [F6] gives $\int_{u}^{v} f \leq \int_{u}^{v} L_{j}$ . Set $G_{j} (x) : = f (u) (x - u) + \frac{f (v) - f (u)}{2 h} (x - u)^{2} .$ The power, product, sum, and scalar rules [F11, F12] give $G_{j}^{'} = L_{j}$ , so [F13] gives $\int_{u}^{v} L_{j} = G_{j} (v) - G_{j} (u) = \frac{h}{2} (f (u) + f (v))$ . Summing over panels, additivity [F8] gives the integral over $[a, b]$ , and each interior node is counted twice with half weight while each endpoint is counted once with half weight. By [F5] this sum is $T_{n} (f)$ , so $\int_{a}^{b} f \leq T_{n} (f)$ .

2.1givenF1F6F7F10F11F12F13step 1.1

For every $x \in [u, v]$ , convexity [F1] at weight $1 / 2$ gives $2 f (m) \leq f (x) + g (x)$ . The constant function is integrable by [F10], and $f + g$ is integrable by [F7] and step 1.1. Monotonicity [F6] and linearity [F7] therefore give $\int_{u}^{v} 2 f (m) d x \leq \int_{u}^{v} (f + g) d x = 2 \int_{u}^{v} f d x$ . The function $G (x) = 2 f (m) x$ is an antiderivative of the constant integrand, by [F11] and [F12]. Hence [F13] gives $2 h f (m) \leq 2 \int_{u}^{v} f d x$ , so $h f (m) \leq \int_{u}^{v} f d x$ .

3.1step 2.1step 1.2F4F8∎

Summing the panel inequalities from step 2.1 by [F8] and using the composite midpoint formula [F4] gives $Q_{M} (f; a, b, n) \leq \int_{a}^{b} f$ . Combining this with step 1.2 proves the bracketing.

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

Simpson rule integrates a quadratic exactly on one two-panel block

Example

On $[0, 2]$ , the function $f (x) = x^{2}$ has exact integral $8 / 3$ . With $n = 2$ , $h = 1$ , and the composite Simpson rule,

$Q_{S} (f; 0, 2, 2) = \frac{1}{3} (f (0) + 4 f (1) + f (2)) = \frac{8}{3} .$

This is the quadratic case of exactness through degree three.

Facts & Assumptions

Given: $f (x) = x^{2}$ on $[0, 2]$ and the composite Simpson rule with $n = 2$ .

[F1]

Composite Simpson rule on an even uniform grid: for $n = 2$ , the returned value is $\frac{h}{3} (f (x_{0}) + 4 f (x_{1}) + f (x_{2}))$ .

[F2]

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 an integrable derivative, the integral is the increment of its antiderivative.

[F3]

Composite Simpson rule is exact through cubic degree: Simpson is exact for every displayed polynomial of degree at most three.

[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 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$ : the power and scalar rules give $(x^{3} / 3)^{'} = x^{2}$ .

[F5]

Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable: $x \mapsto x^{2}$ is Riemann integrable on $[0, 2]$ because it is continuous.

Verification

1.1givenF2F4F5

The function $x^{2}$ is continuous and integrable by [F5]. By [F4], $x^{3} / 3$ is an antiderivative, so [F2] gives $\int_{0}^{2} x^{2} d x = 8 / 3$ .

2.1F1step 1.1algebra

Here $h = 1$ and the nodes are $0, 1, 2$ . By [F1], $Q_{S} = \frac{1}{3} (0 + 4 \cdot 1 + 4) = 8 / 3$ . Thus the computed rule value equals the integral.

3.1F3step 2.1∎

The equality also follows from the degree-at-most-three exactness theorem [F3], since $x^{2}$ has degree two.

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

Simpson rule integrates a cubic exactly on one two-panel block

Example

On $[0, 2]$ , let $f (x) = x^{3}$ . With $n = 2$ and $h = 1$ , the Simpson value is

$Q_{S} (f; 0, 2, 2) = \frac{1}{3} (f (0) + 4 f (1) + f (2)) = 4,$

which equals the exact integral $\int_{0}^{2} x^{3} d x = 4$ . The full two-panel block is exact because the rule annihilates the Peano remainder of every cubic.

Facts & Assumptions

Given: $f (x) = x^{3}$ on $[0, 2]$ and the composite Simpson rule with $n = 2$ .

[F1]

Composite Simpson rule on an even uniform grid: for $n = 2$ , the returned value is $\frac{h}{3} (f (x_{0}) + 4 f (x_{1}) + f (x_{2}))$ .

[F2]

[F3]

Composite Simpson rule is exact through cubic degree: Simpson is exact for every displayed polynomial of degree at most three.

[F4]

[F5]

Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable: $x \mapsto x^{3}$ is Riemann integrable on $[0, 2]$ because it is continuous.

Verification

1.1givenF2F4F5

The function $x^{3}$ is continuous and integrable by [F5]. By [F4], $x^{4} / 4$ is an antiderivative, so [F2] gives $\int_{0}^{2} x^{3} d x = 4$ .

2.1F1step 1.1algebra

Here $h = 1$ and the nodes are $0, 1, 2$ . By [F1], $Q_{S} = \frac{1}{3} (0 + 4 \cdot 1 + 8) = 4$ . Thus the rule value equals the integral.

3.1F3step 2.1∎

The equality is the cubic case of [F3], since $x^{3}$ has degree three.

Composite quadrature rules — Examples

1 · Prerequisites

2 · Summary

Objective

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Convex data bracket the integral between composite midpoint and trapezoid values

Example

Facts & Assumptions

Verification

Simpson rule integrates a quadratic exactly on one two-panel block

Example

Facts & Assumptions

Verification

Simpson rule integrates a cubic exactly on one two-panel block

Example

Facts & Assumptions

Verification

Sources