TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge 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.

Romberg cancels a proved finite even-power expansion

Statement

Let $a < b$ , let $m \geq 1$ and $L \geq m$ be integers, and let $f \in C^{2 m + 2} ([a, b])$ . Write $h_{ℓ} = (b - a) 2^{- ℓ}$ and let $(R_{ℓ, j})$ be the table from Finite Romberg table from nested composite trapezoid levels. If the trapezoid expansion has coefficients $c_{1}, \dots, c_{m}$ as in Even-power expansion of trapezoid levels with a uniform remainder, then the recurrence cancels all first $m$ even powers and there is a finite $C_{m, L}$ such that $∣ R_{L, m} - \int_{a}^{b} f (x) d x ∣ \leq C_{m, L} h_{L}^{2 m + 2} .$ No error-order conclusion is made from a ratio of observed consecutive trapezoid errors.

Facts & Assumptions

Given: $a < b$ , integers $m \geq 1$ , $L \geq m$ , $f \in C^{2 m + 2} ([a, b])$ , and its finite Romberg table.

[F1]

Finite Romberg table from nested composite trapezoid levels: $R_{ℓ, 0} = T_{2^{ℓ}} (f)$ and $R_{ℓ, j} = R_{ℓ, j - 1} + (R_{ℓ, j - 1} - R_{ℓ - 1, j - 1}) / (4^{j} - 1)$ for $1 \leq j \leq ℓ$ .

[F2]

Even-power expansion of trapezoid levels with a uniform remainder: for every level $ℓ$ , $R_{ℓ, 0} = I + \sum_{r = 1}^{m} c_{r} h_{ℓ}^{2 r} + ε_{ℓ, 0}$ with $∣ ε_{ℓ, 0} ∣ \leq C_{0} h_{ℓ}^{2 m + 2}$ , where $I = \int_{a}^{b} f$ and $C_{0}$ is independent of $ℓ$ .

[F3]

Composite trapezoidal rule: $h_{ℓ - 1} = 2 h_{ℓ}$ and the initial table entries are the nested trapezoid values on these levels.

[F4]

The principle of mathematical induction: induction on the finite extrapolation-column index is valid.

Proof

1.1givenF1F2baseinduction

By [F1]–[F2], column zero has the expansion $R_{ℓ, 0} = I + \sum_{r = 1}^{m} c_{r} h_{ℓ}^{2 r} + ε_{ℓ, 0}$ uniformly for $ℓ \geq 0$ . We prove by induction on the column $j$ that, for every $ℓ \geq j$ , $R_{ℓ, j} = I + \sum_{r = j + 1}^{m} d_{r, j} h_{ℓ}^{2 r} + ε_{ℓ, j}, ∣ ε_{ℓ, j} ∣ \leq C_{j} h_{ℓ}^{2 m + 2},$ with coefficients $d_{r, j}$ independent of $ℓ$ . For $j = 0$ , this is [F2] with $d_{r, 0} = c_{r}$ .

2.1givenF1F3step 1.1IHinductionalgebra

Assume the induction hypothesis for column $j - 1$ with $1 \leq j \leq m$ . Then $R_{ℓ, j - 1}$ has terms indexed $r = j, \dots, m$ and $R_{ℓ - 1, j - 1}$ has the same coefficients with $h_{ℓ - 1}^{2 r} = 4^{r} h_{ℓ}^{2 r}$ by [F3]. Substitution in [F1] multiplies the coefficient of $h_{ℓ}^{2 r}$ by $1 + \frac{1 - 4^{r}}{4^{j} - 1} = \frac{4^{j} - 4^{r}}{4^{j} - 1} .$ For $r = j$ this factor is zero, so the $j$ th error power cancels; the remaining powers have indices $r > j$ .

3.1givenF1step 2.1IHalgebra

The new remainder is $ε_{ℓ, j} = ε_{ℓ, j - 1} + (ε_{ℓ, j - 1} - ε_{ℓ - 1, j - 1}) / (4^{j} - 1)$ . Thus $∣ ε_{ℓ, j} ∣ \leq C_{j - 1} (1 + \frac{1 + 2^{2 m + 2}}{4^{j} - 1}) h_{ℓ}^{2 m + 2},$ so a finite level-independent $C_{j}$ exists under the inductive remainder bound.

4.1F2F4step 1.1step 2.1step 3.1inductiondischarge-inductionalgebra∎

Step 1.1 supplies the base column, and steps 2.1 and 3.1 advance the expansion and its uniform remainder from column $j - 1$ to column $j$ . By [F4], induction therefore gives the asserted expansion at every column through $m$ . At $j = m$ the coefficient sum is empty, so $R_{L, m} = I + ε_{L, m}$ , and step 3.1 bounds its remainder by $C_{m} h_{L}^{2 m + 2}$ .

Depends on

Used by

The square-root endpoint does not have Romberg's even-power order Example

Dependency tree · two levels

17 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., §13.3 (standard reference, not scraped)
NIST Digital Library of Mathematical Functions, §3.5(iii), Romberg Integration (standard reference, not scraped)