Definition. Barycentric interpolation weights [cn-0030]

For distinct real interpolation nodes [cn-0063] \(x_1,\ldots ,x_n\), define the node polynomial and barycentric weights by

\[F(t)=\prod _{p=1}^n(t-x_p),\qquad w_p=\frac 1{F'(x_p)}=\frac 1{\prod _{q\ne p}(x_p-x_q)}.\]

Distinctness makes every denominator nonzero. The usual Lagrange basis polynomial is \(w_p F(t)/(t-x_p)\). See Berrut–Trefethen, Section 3 [cn-0044] for the classical weights. The next lemma extracts the particular cancellation needed by the detector.

Proof dependencies
Interpolation nodes [cn-0063]
Provenance
OpenAI, 23 September 2026 [cn-0042], equation (4.3); reconstructed as a reading account on 9 October 2026. Lean source: NodeMoments.