interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C

English

Let s be a finite index set, v: s → F, and r: s → F. Then the Lagrange interpolant interpolate(s,v,r) equals the sum over i in s of C(nodalWeight(s,v,i)) · (nodal(s,v) / (X − C(v(i)))) · C(r(i)).

Русский

Пусть s — конечное множество индексов, v: s → F, r: s → F. Тогда интерполянт Лагранжа interpolate(s,v,r) равен сумме по i∈s от nodalWeight(s,v,i) · nodal(s,v) / (X − v(i)) · C(r(i)).

LaTeX

$$$\text{interpolate}(s,v,r) = \sum_{i \in s} C(\text{nodalWeight}(s,v,i)) \cdot \frac{\text{nodal}(s,v)}{X - C(v(i))} \cdot C(r(i)).$$$

Lean4

theorem interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C :
    interpolate s v r = ∑ i ∈ s, C (nodalWeight s v i) * (nodal s v / (X - C (v i))) * C (r i) :=
  sum_congr rfl fun j hj => by rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hj]

Похожие утверждения