LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Hermite–Genocchi simplex formula for divided differences

Statement

Let $q \in N$ , let $f \in C^{q} ([a, b])$ , and let $t_{0}, \dots, t_{q} \in [a, b]$ be distinct real nodes. For $q \geq 1$ , define $Δ_{q} = {(u_{1}, \dots, u_{q}) \in [0, \infty)^{q} : u_{1} + \dots + u_{q} \leq 1}, u_{0} = 1 - \sum_{j = 1}^{q} u_{j} .$ Then $f [t_{0}, \dots, t_{q}] = \int_{Δ_{q}} f^{(q)} ⁣ (\sum_{j = 0}^{q} u_{j} t_{j}) d u_{1} \dots d u_{q}, vol (Δ_{q}) = \frac{1}{q!} .$ For $q = 0$ , the integral is by convention evaluation at $t_{0}$ , and $vol (Δ_{0}) : = 1$ . For $q \geq 1$ , the integral over $Δ_{q}$ is the iterated Riemann integral with $0 \leq u_{1} \leq 1$ and, successively, $0 \leq u_{j} \leq 1 - \sum_{k = 1}^{j - 1} u_{k}$ for $2 \leq j \leq q$ .

Facts & Assumptions

Given: $q \in N$ , $f \in C^{q} ([a, b])$ , and distinct nodes $t_{0}, \dots, t_{q} \in [a, b]$ .

[F1]

Divided differences on distinct nodes: divided differences satisfy the recursive endpoint rule.

[F2]

Divided differences are symmetric leading coefficients: divided differences are symmetric in their nodes.

[F3]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $f \in C^{q}$ means its derivatives through order $q$ exist and are continuous, including their one-sided endpoint extensions.

[F4]

Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative: for a continuous function on a closed interval whose interior derivative has a Riemann-integrable extension, the integral of that extension is the endpoint increment.

[F5]

The natural numbers $N$ (von Neumann): $0 \in N$ , so the order-zero base case is included.

[F6]

The principle of mathematical induction: a property true at $0$ and preserved by successor holds for every natural number.

Proof

1.1givenF1F5

For $q = 0$ , which is allowed by [F5], the integral convention gives $f (t_{0}) = f [t_{0}]$ and the zero-dimensional simplex has volume one.

1.2F1F2F3F4F6inductionalgebra

By [F6], use induction on $q \in N$ . Suppose the formula is established in order $q - 1$ , where $q \geq 1$ . In the recursive rule [F1], express the two order- $(q - 1)$ divided differences by the induction hypothesis. The bottom face $u_{q} = 0$ has argument $t_{0} + \sum_{j = 1}^{q - 1} u_{j} (t_{j} - t_{0})$ and gives $f [t_{0}, \dots, t_{q - 1}]$ . On the top face $u_{q} = 1 - \sum_{j = 1}^{q - 1} u_{j}$ , the same argument is $t_{q} + \sum_{j = 1}^{q - 1} u_{j} (t_{j} - t_{q})$ and gives $f [t_{1}, \dots, t_{q}]$ by symmetry [F2]. For fixed $u_{1}, \dots, u_{q - 1}$ with sum less than $1$ , the derivative with respect to $u_{q}$ of $f^{(q - 1)} ⁣ (t_{0} + \sum_{j = 1}^{q} u_{j} (t_{j} - t_{0}))$ is $(t_{q} - t_{0}) f^{(q)} (\sum_{j = 0}^{q} u_{j} t_{j})$ . The derivative is continuous by [F3], hence Riemann integrable. Applying [F4] on the $u_{q}$ interval, followed by integration over the other coordinates, shows that the difference of the two face integrals is $(t_{q} - t_{0})$ times the $q$ -dimensional integral in the statement. When the outer coordinates sum to $1$ , the inner $u_{q}$ interval is $[0, 0]$ and its integral is zero; for $q = 1$ there are no outer coordinates and the interval is $[0, 1]$ . Division by $t_{q} - t_{0} \neq 0$ gives the order- $q$ formula.

2.1step 1.1F4F6inductionalgebra∎

By [F6], prove the volume formula by induction, with its $q = 0$ case from step 1.1. For $q \geq 1$ , fix the outer coordinate $u_{1} \in [0, 1]$ . The remaining coordinates form a $(q - 1)$ -simplex scaled by $1 - u_{1}$ . If $q = 1$ , its zero-dimensional volume is $1$ ; if $q \geq 2$ and $u_{1} < 1$ , the dilation to $Δ_{q - 1}$ has Jacobian $(1 - u_{1})^{q - 1}$ , while the section at $u_{1} = 1$ has $(q - 1)$ -volume zero. Thus, by induction, the section volume is $(1 - u_{1})^{q - 1} / (q - 1)!$ . The function $H (u) = - (1 - u)^{q} / q!$ has derivative $(1 - u)^{q - 1} / (q - 1)!$ ; applying [F4] to $H$ on $[0, 1]$ gives $H (1) - H (0) = 1 / q!$ . $vol (Δ_{q}) = \int_{0}^{1} \frac{(1 - u_{1})^{q - 1}}{(q - 1)!} d u_{1} = \frac{1}{q!} .$ The induction and the divided-difference identity prove the statement.

Depends on

Used by

Dependency tree · two levels

19 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

Carl de Boor, Divided Differences, Section 9, Genocchi–Hermite, pages 63–65, formula (52) (standard reference, not scraped)