Alphabeta MathHow 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.
Simpson rule integrates a cubic exactly on one two-panel block
Example
On , let . With and , the Simpson value is
which equals the exact integral . The full two-panel block is exact because the rule annihilates the Peano remainder of every cubic.
Facts & Assumptions
Given: on and the composite Simpson rule with .
Composite Simpson rule on an even uniform grid: for , the returned value is .
The second fundamental theorem: if is differentiable on with and is integrable, then : for an integrable derivative, the integral is the increment of its antiderivative.
Composite Simpson rule is exact through cubic degree: Simpson is exact for every displayed polynomial of degree at most three.
For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term and Sums, scalar multiples, products and quotients: , , , and when : the power and scalar rules give .
Every continuous function on a closed nondegenerate rectangle in is Riemann integrable: is Riemann integrable on because it is continuous.
Verification
The function is continuous and integrable by [F5]. By [F4], is an antiderivative, so [F2] gives .
Here and the nodes are . By [F1], . Thus the rule value equals the integral.
The equality is the cubic case of [F3], since has degree three.
Depends on
- Composite Simpson rule on an even uniform grid
- Composite Simpson rule is exact through cubic degree
- 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 natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- Every continuous function on a closed nondegenerate rectangle in $\mathbb{R}^m$ is Riemann integrable
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
45 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)