English
Let hx hold: for all i ∈ s, x ≠ v(i). Then eval x (interpolate(s,v,r)) equals eval x (nodal(s,v)) times the sum over i ∈ s of nodalWeight(s,v,i) · (x − v(i))^{-1} · r(i).
Русский
Пусть выполняется hx: для всех i ∈ s x ≠ v(i). Тогда eval_x(interpolate(s,v,r)) равно eval_x(nodal(s,v)) умножить на сумму по i∈s nodalWeight(s,v,i) · (x − v(i))^{-1} · r(i).
LaTeX
$$$\mathrm{eval}_x(\text{interpolate}(s,v,r)) = \mathrm{eval}_x(\text{nodal}(s,v)) \cdot \sum_{i \in s} \text{nodalWeight}(s,v,i) \cdot (x - v_i)^{-1} \cdot r_i.$$$
Lean4
/-- This is the first barycentric form of the Lagrange interpolant. -/
theorem eval_interpolate_not_at_node (hx : ∀ i ∈ s, x ≠ v i) :
eval x (interpolate s v r) = eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i :=
by
simp_rw [interpolate_apply, mul_sum, eval_finset_sum, eval_mul, eval_C]
refine sum_congr rfl fun i hi => ?_
rw [← mul_assoc, mul_comm, eval_basis_not_at_node hi (hx _ hi)]
