English
Let hvs be an injectivity condition and hs nonempty. Then eval x (interpolate(s,v,r)) equals the ratio of two sums: the numerator is sum over i ∈ s of nodalWeight(s,v,i) · (x − v(i))^{-1} · r(i), and the denominator is sum over i ∈ s of nodalWeight(s,v,i) · (x − v(i))^{-1}.
Русский
Пусть выполнено условие вводимости hvs и hs непусто. Тогда eval_x(interpolate(s,v,r)) равняется отношению сумм: числитель — ∑_{i∈s} nodalWeight(s,v,i) · (x − v(i))^{-1} · r(i); знаменатель — ∑_{i∈s} nodalWeight(s,v,i) · (x − v(i))^{-1}.
LaTeX
$$$\mathrm{eval}_x(\text{interpolate}(s,v,r)) = \dfrac{\sum_{i \in s} \text{nodalWeight}(s,v,i) \cdot (x - v_i)^{-1} \cdot r_i}{\sum_{i \in s} \text{nodalWeight}(s,v,i) \cdot (x - v_i)^{-1}}.$$$
Lean4
/-- This is the second barycentric form of the Lagrange interpolant. -/
theorem eval_interpolate_not_at_node' (hvs : Set.InjOn v s) (hs : s.Nonempty) (hx : ∀ i ∈ s, x ≠ v i) :
eval x (interpolate s v r) =
(∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ :=
by
rw [← div_one (eval x (interpolate s v r)), ← @eval_one _ _ x, ← interpolate_one hvs hs,
eval_interpolate_not_at_node r hx, eval_interpolate_not_at_node 1 hx]
simp only [mul_div_mul_left _ _ (eval_nodal_not_at_node hx), Pi.one_apply, mul_one]
