Alphabeta Math
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 barycentric denominator lower bound

Statement

Let n≥1, 0≤d<n, x0<⋯<xn, and h=max⁡j(xj+1−xj). Let Dd(x)=∑j=0nwj/(x−xj) be the Floater–Hormann denominator from Floater–Hormann barycentric interpolant. For every open gap xα<x<xα+1, ∣Dd(x)∣≥{1d! hd+1,d≥1,1h(1+β),d=0, where β is the local ratio of Local mesh ratio for degree-zero Floater–Hormann interpolation.

Facts & Assumptions

Given: Ordered distinct real nodes, n≥1, 0≤d<n, an open node gap, and the associated Floater–Hormann denominator.

[F1]

Floater–Hormann weights equal the local-polynomial blend weights: Dd(x)=∑iλi(x) and ∑iμi(x)=(−1)n−d(∏j(x−xj))Dd(x) away from nodes.

[F2]

Floater–Hormann blend partial sums are positive in each node gap: each nonempty block sum over I1,I2,I3 is positive; for d=0, the first two terms of I3 and the last two terms of I1 form positive pairs.

[F3]

Local mesh ratio for degree-zero Floater–Hormann interpolation: for d=0, β is the maximum of the interior minima of the two adjacent-gap ratios, and is zero when n≤2.

Proof

1.1givenF1F2choosealgebra

Suppose d≥1. The middle block I2 contains at least one index: j=max⁡(0,α−d+1) satisfies j≤α, j+d≥α+1, and j≤n−d. Thus its window contains both endpoints of the gap and μj(x)>0. By [F2], s(x)=s1(x)+s2(x)+s3(x)≥s2(x)≥μj(x), with empty block sums interpreted as zero. From [F1], ∣Dd(x)∣=s(x)∏k=0n∣x−xk∣≥μj(x)∏k=0n∣x−xk∣=∣λj(x)∣=1∏k=jj+d∣x−xk∣. This reduces the denominator estimate to one window product.

1.2givenF1F2algebra

Now let d=0. On the first gap, I1={0} and the other nonempty block sums are positive by [F2], hence s≥μ0 and ∣D0(x)∣≥∣λ0(x)∣=1/(x−x0)≥1/h. On the last gap it gives I3={n} and the other nonempty block sums are positive, hence s≥μn and ∣D0(x)∣≥1/(xn−x)≥1/h. These bounds imply the claimed inequality because β≥0.

2.1givenstep 1.1algebra

Put u=α−j+1 and v=j+d−α, so u,v≥1 and u+v=d+1. For j≤k≤α, ∣x−xk∣≤xα+1−xk≤(α+1−k)h; for α+1≤k≤j+d, ∣x−xk∣≤xk−xα≤(k−α)h. Multiplying these d+1 bounds gives ∏k=jj+d∣x−xk∣≤u! v! hd+1≤d! hd+1. The last inequality follows from (d+1u)=(d+1)!/(u!v!)≥d+1. Substitution in step 1.1 proves the d≥1 bound.

3.1givenF1F2F3step 1.2algebra∎

If 1≤α≤n−2, both I1 and I3 are nonempty. The first two terms from I3 and first two read backward from I1 form positive pairs. With Δ=xα+1−xα, δR=xα+2−xα+1 and δL=xα−xα−1, [F1]–[F2] yield ∣D0(x)∣≥max⁡{1xα+1−x−1xα+2−x,1x−xα−1x−xα−1}. Writing t=xα+1−x≤Δ in the first difference gives δR/[t(t+δR)]≥1/[h(1+Δ/δR)]. Writing u=x−xα≤Δ in the second gives δL/[u(u+δL)]≥1/[h(1+Δ/δL)]. Hence ∣D0(x)∣≥1h(1+min⁡{Δ/δL,Δ/δR})≥1h(1+β) by [F3]. For n≤2 there is no such interior index, so steps 1.2 cover all gaps.

Depends on

Used by

Dependency tree · two levels

7 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