English
Let s be a finite set of indices, v: ι → F a choice of distinct nodes, and i ∈ s with x ≠ v(i). Then the value of the i-th Lagrange basis polynomial at x is the value of the nodal polynomial at x multiplied by the weight at i and by the inverse of (x − v(i)): L_i(x) = nodal(s,v)(x) · (nodalWeight(s,v,i) · (x − v(i))^{-1}).
Русский
Пусть s — конечное множество индексов, v: ι → F выбор узлов, i ∈ s и x ≠ v(i). Тогда значение i-го базиса Лагранжа в точке x равно nodal(s,v)(x), умноженному на nodalWeight(s,v,i) и на (x − v(i))^{-1}: L_i(x) = nodal(s,v)(x) · (nodalWeight(s,v,i) · (x − v(i))^{-1}).
LaTeX
$$$\mathrm{eval}(x, \text{basis}(s,v,i)) = \mathrm{eval}(x, \text{nodal}(s,v)) \cdot (\text{nodalWeight}(s,v,i) \cdot (x - v_i)^{-1}).$$$
Lean4
theorem eval_basis_not_at_node (hi : i ∈ s) (hxi : x ≠ v i) :
eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹) := by
rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ← nodal_erase_eq_nodal_div hi, eval_nodal,
eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ← mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi),
one_mul]
