nodalWeight_eq_eval_derivative_nodal

English

Weight at i equals the inverse of the derivative evaluation at node i (on s\\{i}).

Русский

Вес нодала равен обратному значению eval при v(i) производной nodal(s\\{i}, v).

LaTeX

$$$ \\operatorname{nodalWeight}(s,v,i) = \\operatorname{eval}(v(i), \\operatorname{derivative}(\\operatorname{nodal}(s\\setminus i, v)))^{-1}. $$$

Lean4

theorem nodalWeight_eq_eval_derivative_nodal (hi : i ∈ s) :
    nodalWeight s v i = (eval (v i) (Polynomial.derivative (nodal s v)))⁻¹ := by
  rw [eval_nodal_derivative_eval_node_eq hi, nodalWeight_eq_eval_nodal_erase_inv]

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