English
Lagrange interpolation assigns to each function r a unique polynomial of degree < |s| that matches r at the nodes v(i).
Русский
Интерполяция Лагранжа сопоставляет каждому r единственный многочлен степени < |s|, совпадающий с r в узлах v(i).
LaTeX
$$$\text{interpolate}(s,v,r)=\sum_{i\in s} C(r(i)) \cdot L_{s,v,i}$$$
Lean4
/-- Lagrange interpolation: given a finset `s : Finset ι`, a nodal map `v : ι → F` injective on
`s` and a value function `r : ι → F`, `interpolate s v r` is the unique
polynomial of degree `< #s` that takes value `r i` on `v i` for all `i` in `s`. -/
@[simps]
def interpolate (s : Finset ι) (v : ι → F) : (ι → F) →ₗ[F] F[X]
where
toFun r := ∑ i ∈ s, C (r i) * Lagrange.basis s v i
map_add' f
g := by
simp_rw [← Finset.sum_add_distrib]
have h :
(fun x => C (f x) * Lagrange.basis s v x + C (g x) * Lagrange.basis s v x) =
(fun x => C ((f + g) x) * Lagrange.basis s v x) :=
by simp_rw [← add_mul, ← C_add, Pi.add_apply]
rw [h]
map_smul' c f := by simp_rw [Finset.smul_sum, C_mul', smul_smul, Pi.smul_apply, RingHom.id_apply, smul_eq_mul]
