Summary
Add a fixed-domain barycentric interpolation surface to CompPoly.CPolynomial.CLagrange for repeated-query univariate evaluation over a field.
For pairwise distinct nodes x : Fin n → R, store the barycentric weights
w_i = ∏_{j ≠ i} (x_i - x_j)⁻¹
once and evaluate by the classical second barycentric formula:
- if
z = x_i, return y_i;
- otherwise return
(∑ i, w_i * y_i * (z - x_i)⁻¹) / (∑ i, w_i * (z - x_i)⁻¹).
Correctness target
Prove that for every y : Fin n → R and z : R,
BarycentricDomain.eval y z = (Lagrange.interpolate Finset.univ x y).eval z.
Also derive the CompPoly-facing corollary
BarycentricDomain.eval y z = (CLagrange.interpolate Finset.univ x y).eval z,
together with the roots-of-unity specialization agreeing with CLagrange.interpolatePow.
Motivation
This supports the Phase 2 evaluation/interpolation track by separating one-time nodal preprocessing from per-query evaluation on a fixed domain.
Summary
Add a fixed-domain barycentric interpolation surface to
CompPoly.CPolynomial.CLagrangefor repeated-query univariate evaluation over a field.For pairwise distinct nodes
x : Fin n → R, store the barycentric weightsw_i = ∏_{j ≠ i} (x_i - x_j)⁻¹once and evaluate by the classical second barycentric formula:
z = x_i, returny_i;(∑ i, w_i * y_i * (z - x_i)⁻¹) / (∑ i, w_i * (z - x_i)⁻¹).Correctness target
Prove that for every
y : Fin n → Randz : R,BarycentricDomain.eval y z = (Lagrange.interpolate Finset.univ x y).eval z.Also derive the CompPoly-facing corollary
BarycentricDomain.eval y z = (CLagrange.interpolate Finset.univ x y).eval z,together with the roots-of-unity specialization agreeing with
CLagrange.interpolatePow.Motivation
This supports the Phase 2 evaluation/interpolation track by separating one-time nodal preprocessing from per-query evaluation on a fixed domain.