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.

Floater–Hormann blend partial sums are positive in each node gap

Statement

Let $x_{0} < \dots < x_{n}$ and $0 \leq d < n$ , and use the $μ_{i}$ and $s = \sum_{i = 0}^{n - d} μ_{i}$ of Floater–Hormann weights equal the local-polynomial blend weights. For $x_{α} < x < x_{α + 1}$ , partition the indices into $I_{1} = {i \leq α - d}, I_{2} = {α - d + 1 \leq i \leq α}, I_{3} = {i \geq α + 1},$ intersecting each set with ${0, \dots, n - d}$ . Each nonempty partial sum $\sum_{i \in I_{k}} μ_{i} (x)$ is positive. More precisely, if $I_{3}$ is nonempty, its terms alternate starting positive with strictly decreasing magnitudes; if $I_{1}$ is nonempty, its terms have the same property when read backward from $i = α - d$ . If $d \geq 1$ , every term in $I_{2}$ is positive.

Facts & Assumptions

Given: Ordered distinct nodes $x_{0} < \dots < x_{n}$ , $0 \leq d < n$ , and a query point in one open node gap.

[F1]

Floater–Hormann weights equal the local-polynomial blend weights: $μ_{i} (x) = \prod_{j < i} (x - x_{j}) \prod_{k > i + d} (x_{k} - x)$ .

Proof

1.1givenF1algebra

If $i \in I_{2}$ , every factor in $μ_{i} (x)$ is positive: left indices lie strictly below $x_{α} < x$ , and right indices lie strictly above $x < x_{α + 1}$ . Thus all terms in a nonempty $I_{2}$ are positive. If $d = 0$ , $I_{2}$ is empty.

1.2givenF1algebra

If $I_{3}$ is nonempty, its first index is $α + 1$ and $μ_{α + 1} (x) > 0$ . For $α + 1 \leq i < n - d$ , $\frac{μ_{i + 1} (x)}{μ_{i} (x)} = \frac{x - x_{i}}{x_{i + d + 1} - x} < 0, ∣ \frac{μ_{i + 1} (x)}{μ_{i} (x)} ∣ < 1.$ The numerator is negative and its magnitude is smaller than the positive denominator because $x_{i} < x_{i + d + 1}$ . Consecutive terms therefore alternate with strictly decreasing magnitudes. Pairing from the first positive term gives a positive sum, including when one positive term remains.

2.1givenF1algebra∎

If $I_{1}$ is nonempty, its last index is $α - d$ and $μ_{α - d} (x) > 0$ . Read backward. For $i \leq α - d$ with $i > 0$ , $\frac{μ_{i - 1} (x)}{μ_{i} (x)} = \frac{x_{i + d} - x}{x - x_{i - 1}} < 0, ∣ \frac{μ_{i - 1} (x)}{μ_{i} (x)} ∣ < 1.$ Here $x_{i + d} \leq x_{α} < x$ and $x_{i - 1} < x_{i} \leq x_{i + d}$ , so the numerator is negative and its magnitude is smaller than the positive denominator. Pairing backward from the first positive term proves the $I_{1}$ sum is positive.

Depends on

Used by

Dependency tree · two levels

5 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

Michael S. Floater and Kai Hormann, Barycentric rational interpolation with no poles and high rates of approximation, proof of Theorem 1 (standard reference, not scraped)