LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge 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 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]

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.

[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]

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 every integer $k \geq 1$ .

[F8]

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 their derivatives.

[F9]

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.

[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$ .

Depends on

Used by

Dependency tree · two levels

60 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

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