TheoremStatement: 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.

PCHIP has third-order value accuracy on uniform nonstationary grids

Statement

Let $a < b$ , let $f$ be $C^{3}$ on an open interval containing $[a, b]$ , and suppose $∣ f^{'} (x) ∣ \geq c > 0$ on $[a, b]$ . For each integer $N \geq 2$ , put $h = (b - a) / N > 0$ and $x_{j} = a + j h$ , $j = 0, \dots, N$ , and let $P_{h}$ be the PCHIP interpolant to the values $f (x_{j})$ . There are constants $C, h_{0} > 0$ , depending only on $f$ , $c$ , and $[a, b]$ , such that for every such grid with $h < h_{0}$ , $\max_{x \in [a, b]} ∣ P_{h} (x) - f (x) ∣ \leq C h^{3} .$ The assertion is limited to uniform grids and intervals on which the derivative stays bounded away from zero; it makes no third-order claim at an extremum.

Facts & Assumptions

Given: Reals $a < b$ , the stated $C^{3}$ function and derivative bound on $[a, b]$ , an integer $N \geq 2$ , and the uniform grid with $h = (b - a) / N > 0$ .

[F1]

PCHIP slope selection: PCHIP uses the prescribed nodal values and selected slopes in the cubic Hermite formula.

[F2]

PCHIP slope selection has no zero denominator: those slopes and pieces are finite and well-defined.

[F3]

Piecewise cubic Hermite interpolant: on a cell the Hermite formula is the linear combination of $H_{00}, H_{01}, H_{10}, H_{11}$ with value and slope data.

[F4]

Interpolation, C1 matching, and cubic reproduction for Hermite pieces: each Hermite piece interpolates its endpoint values and slopes; the resulting interpolant is $C^{1}$ on the closed interval (with one-sided endpoint derivatives); and each piece reproduces any cubic polynomial from its endpoint values and derivatives.

[F5]

PCHIP slopes are second-order accurate on uniform nonstationary grids: for all sufficiently fine uniform grids, every PCHIP nodal slope differs from $f^{'} (x_{j})$ by at most $C_{s} h^{2}$ for a constant $C_{s}$ independent of the cell.

[F6]

Taylor's theorem with an integral remainder: the degree-two Taylor polynomial of a $C^{3}$ function has remainder at most $M h^{3} / 6$ on a cell of width $h$ when $∣ f^{'''} ∣ \leq M$ there. Applied to $f^{'}$ with degree one, the same theorem bounds its remainder by $M h^{2} / 2$ .

[F7]

Continuity and derivative on a real interval: $C^{3}$ on an open interval means the derivatives through order three exist and are continuous there.

[F8]

A continuous real function on a compact subset of $R$ is bounded: a continuous real function on a compact subset of $R$ is bounded there.

[F9]

Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact: every closed interval $[u, v]$ with $u \leq v$ is compact.

[F10]

Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value: a continuous real function on a nonempty compact subset of $R$ attains its maximum and minimum.

[F11]

Real and complex modulus product and triangle inequalities: the real triangle inequality; applying it twice gives $∣ ∣ u ∣ - ∣ v ∣ ∣ \leq ∣ u - v ∣$ .

Proof

1.1F6F7F8F9given

Since $a < b$ and $h = (b - a) / N > 0$ , the grid is admissible and $[a, b]$ is compact by [F9]. By [F7] and [F8], choose $M \geq 0$ with $∣ f^{'''} ∣ \leq M$ on $[a, b]$ . Fix a cell $[x_{i}, x_{i} + h]$ and let $T_{2}$ be the degree-two Taylor polynomial of $f$ at $x_{i}$ . By [F6], the residual $r = f - T_{2}$ satisfies $r (x_{i}) = r^{'} (x_{i}) = 0$ and, for every $x \in [x_{i}, x_{i} + h]$ , $∣ r (x) ∣ \leq M h^{3} / 6$ ; at the right endpoint it also satisfies $∣ r (x_{i} + h) ∣ \leq M h^{3} / 6$ and $∣ r^{'} (x_{i} + h) ∣ \leq M h^{2} / 2$ . The derivative bound is [F6] applied to $f^{'}$ with degree one.

1.2F1F2F3F5givenalgebra

Let $H$ be the exact-derivative Hermite piece for $f$ on this cell. The PCHIP piece $P_{h}$ and $H$ have identical endpoint values. By [F3], their difference is $h (m_{i} - f^{'} (x_{i})) H_{10} (t) + h (m_{i + 1} - f^{'} (x_{i} + h)) H_{11} (t)$ . Since [F2] guarantees these PCHIP slopes are defined and $∣ H_{10} (t) ∣ = t (1 - t)^{2} \leq 1$ , $∣ H_{11} (t) ∣ \leq 1$ , [F5] gives $∣ P_{h} (x) - H (x) ∣ \leq 2 C_{s} h^{3}$ for every $x$ in the cell.

2.1F3F4step 1.1algebra

For this exact-derivative Hermite piece $H$ , linearity of the formula [F3] and reproduction [F4] give $H = T_{2} + H_{r}$ , where $H_{r} (t) = r (x_{i} + h) H_{01} (t) + h r^{'} (x_{i} + h) H_{11} (t)$ . On $0 \leq t \leq 1$ , $∣ H_{01} (t) ∣ = t^{2} (3 - 2 t) \leq 1$ and $∣ H_{11} (t) ∣ = t^{2} (1 - t) \leq 1$ , so $∣ H_{r} (t) ∣ \leq (1 / 6 + 1 / 2) M h^{3} = 2 M h^{3} / 3$ . Together with $∣ r (x) ∣ \leq M h^{3} / 6$ from step 1.1, this yields $∣ H (x) - f (x) ∣ \leq 5 M h^{3} / 6$ for every $x$ in the cell.

3.1step 2.1step 1.2F1F4F7F9F10F11algebra∎

Combining steps 2.1 and 1.2 gives $∣ P_{h} (x) - f (x) ∣ \leq (5 M / 6 + 2 C_{s}) h^{3}$ for every $x \in [a, b]$ , since the cells cover the interval. The constants do not depend on $i$ or $N$ ; put $C = 5 M / 6 + 2 C_{s}$ . To justify the maximum in the statement, admissibility of the grid for [F1] gives $x_{0} < \dots < x_{N}$ , so $a < b$ . By [F4], $P_{h}$ is $C^{1}$ and hence continuous on $[a, b]$ ; by [F7], $f$ is continuous there. Set $E (x) = ∣ P_{h} (x) - f (x) ∣$ . For $x, z \in [a, b]$ , applying the triangle inequality twice gives $∣ ∣ P_{h} (x) - f (x) ∣ - ∣ P_{h} (z) - f (z) ∣ ∣ \leq ∣ (P_{h} (x) - f (x)) - (P_{h} (z) - f (z)) ∣ \leq ∣ P_{h} (x) - P_{h} (z) ∣ + ∣ f (x) - f (z) ∣$ , so $E$ is continuous on $[a, b]$ . By [F9], $[a, b]$ is compact, and it is nonempty; [F10] therefore gives a point where $E$ attains its maximum. The pointwise bound just proved bounds that maximum by $C h^{3}$ .

Depends on

Used by

PCHIP loses third-order value accuracy next to a smooth extremum Example

Dependency tree · two levels

48 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

F. N. Fritsch and J. Butland, A Method for Constructing Local Monotone Piecewise Cubic Interpolants, SIAM Journal on Scientific and Statistical Computing 5 (1984), pp. 300–304 (standard reference, not scraped)
Carl R. de Boor, A Practical Guide to Splines, revised edition, Chapter IV, pp. 39–40 (standard reference, not scraped)