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.

PCHIP slopes are second-order accurate 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$ for every $x \in [a, b]$ . For an integer $N \geq 2$ , put $h = (b - a) / N > 0$ and $x_{j} = a + j h$ for $j = 0, \dots, N$ . Let $m_{j}$ be the slopes selected by PCHIP slope selection from the values $f (x_{j})$ . There are constants $C, h_{0} > 0$ , depending on $f$ , $c$ , and $[a, b]$ , such that for every such grid with $h < h_{0}$ , $\max_{0 \leq j \leq N} ∣ m_{j} - f^{'} (x_{j}) ∣ \leq C h^{2} .$

Facts & Assumptions

Given: Reals $a < b$ , a $C^{3}$ real function on an open neighborhood of $[a, b]$ , a positive lower bound for $∣ f^{'} ∣$ on $[a, b]$ , an integer $N \geq 2$ , and the uniform grid with $h = (b - a) / N > 0$ .

[F1]

PCHIP slope selection: interior slopes use the weighted harmonic formula when neighboring secants have the same nonzero sign; the one-sided endpoint estimate is $((2 h_{0} + h_{1}) d_{0} - h_{0} d_{1}) / (h_{0} + h_{1})$ , followed by a sign clip and an opposite-sign cap.

[F2]

PCHIP slope selection has no zero denominator: for admissible inputs every selected slope is a finite real number and every formula denominator is nonzero.

[F3]

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

[F4]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : for a function continuous on a closed interval and differentiable in its interior, its secant slope equals its derivative at some interior point.

[F5]

Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ : a continuous real function on a closed interval takes every value between its endpoint values.

[F6]

Taylor's theorem with an integral remainder: if derivatives through order $r + 1$ are continuous, the degree- $r$ Taylor polynomial at $c$ has remainder bounded by $M ∣ x - c ∣^{r + 1} / (r + 1)!$ when $∣ f^{(r + 1)} ∣ \leq M$ on the segment.

[F7]

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.

[F8]

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

[F9]

Every nonempty finite set of reals has a maximum and a minimum: every finite list of real numbers has a maximum.

Proof

1.1F1F3F4F5F7F8given

By [F3], $f^{'}$ is continuous. It cannot take both a positive and a negative value on $[a, b]$ , since [F5] would then give a zero of $f^{'}$ , contradicting $∣ f^{'} ∣ \geq c$ . Thus $f^{'}$ has one sign throughout. On each grid cell [F4] gives $d_{j} = f^{'} (ξ_{j})$ for some interior $ξ_{j}$ , so all secants have that sign and $∣ d_{j} ∣ \geq c$ . Since $a < b$ and $h = (b - a) / N > 0$ , the grid is admissible for [F1], and [F8] makes $[a, b]$ compact. Since $f^{'}$ , $f^{''}$ , and $f^{'''}$ are continuous by [F3], [F7] supplies $M_{1}, M_{2}, M_{3} \geq 0$ with $∣ f^{'} ∣ \leq M_{1}$ , $∣ f^{''} ∣ \leq M_{2}$ , and $∣ f^{'''} ∣ \leq M_{3}$ on $[a, b]$ .

1.2F3F6givenalgebra

Fix an interior node $x_{k}$ and set $s = f^{'} (x_{k})$ and $q = f^{''} (x_{k})$ . Applying [F6] with degree two at $x_{k}$ to $x_{k} - h$ and $x_{k} + h$ and dividing the remainders by $h$ gives $d_{k - 1} = s - h q / 2 + e_{-}$ and $d_{k} = s + h q / 2 + e_{+}$ , where $∣ e_{-} ∣, ∣ e_{+} ∣ \leq M_{3} h^{2} / 6$ . Since $∣ s ∣ \geq c$ , for sufficiently small $h$ both secants stay bounded away from zero. The identity $1 / (s + u) = 1 / s - u / s^{2} + u^{2} / (s^{2} (s + u))$ then gives, with a uniform constant, $1 / d_{k - 1} = 1 / s + h q / (2 s^{2}) + O (h^{2})$ and $1 / d_{k} = 1 / s - h q / (2 s^{2}) + O (h^{2})$ .

2.1F1F2step 1.2givenalgebra

On a uniform grid the two weights in [F1] are both $3 h$ , so the interior slope equals $2 / (1 / d_{k - 1} + 1 / d_{k})$ . The first-order terms in step 1.2 cancel, giving $1 / d_{k - 1} + 1 / d_{k} = 2 / s + O (h^{2})$ . Since $∣ s ∣ \leq M_{1}$ , the leading term has magnitude at least $2 / M_{1}$ ; thus the denominator stays bounded away from zero for sufficiently small $h$ , and its reciprocal yields $m_{k} = s + O (h^{2})$ with a constant uniform in $k$ .

2.2F1F2F6step 1.1givenalgebra

At the left endpoint, [F6] at $a$ gives $d_{0} = f^{'} (a) + h f^{''} (a) / 2 + O (M_{3} h^{2})$ and $d_{1} = f^{'} (a) + 3 h f^{''} (a) / 2 + O (M_{3} h^{2})$ , by expanding $f (a + h)$ and $f (a + 2 h)$ . Therefore the raw endpoint estimate in [F1] is ${\hat{m}}_{0} = (3 d_{0} - d_{1}) / 2 = f^{'} (a) + O (M_{3} h^{2})$ . For small $h$ it has the sign of $f^{'} (a)$ ; step 1.1 gives that same sign for $d_{0}, d_{1}$ , so neither the sign clip nor the opposite-sign cap changes it. Reflecting the expansions at $b$ gives the identical $O (h^{2})$ error for $m_{N}$ .

3.1step 2.1step 2.2F9given∎

The interior and endpoint estimates above use the bounds $M_{1}, M_{2}, M_{3}$ and $c^{- 1}$ on the fixed interval; their constants and smallness thresholds are therefore uniform in the node index. Taking a common maximum for the error constants and a common positive minimum for the thresholds gives $C, h_{0}$ valid at every interior node and both endpoints. The finite list $∣ m_{j} - f^{'} (x_{j}) ∣$ , $0 \leq j \leq N$ , has a maximum by [F9], and the uniform pointwise estimate bounds it by $C h^{2}$ .

Depends on

Used by

PCHIP has third-order value accuracy on uniform nonstationary grids Theorem

Dependency tree · two levels

50 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)