basis_eq_prod_sub_inv_mul_nodal_div

English

Each Lagrange basis polynomial equals the nodal weight times the nodal divided by the corresponding linear factor.

Русский

Для i ∈ s базис Лагранжа равен произведению nodalWeight(s,v,i) на nodal(s,v) делённое на X − C(v(i)).

LaTeX

$$$ Lagrange.basis(s,v,i) = C(nodalWeight(s,v,i)) \\cdot \\dfrac{nodal(s,v)}{X - C(v(i))}. $$$

Lean4

theorem basis_eq_prod_sub_inv_mul_nodal_div (hi : i ∈ s) :
    Lagrange.basis s v i = C (nodalWeight s v i) * (nodal s v / (X - C (v i))) := by
  simp_rw [Lagrange.basis, basisDivisor, nodalWeight, prod_mul_distrib, map_prod, ← nodal_erase_eq_nodal_div hi, nodal]

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