eval_nodal_derivative_eval_node_eq

English

Evaluating the derivative at a node yields the same as evaluating the residual nodal after removing that node.

Русский

Для i ∈ s, значение при x = v(i) производной nodal совпадает с значением nodal на s\\{i}.

LaTeX

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

Lean4

theorem eval_nodal_derivative_eval_node_eq [DecidableEq ι] {i : ι} (hi : i ∈ s) :
    eval (v i) (derivative (nodal s v)) = eval (v i) (nodal (s.erase i) v) :=
  by
  rw [derivative_nodal, eval_finset_sum, ← add_sum_erase _ _ hi, add_eq_left]
  exact sum_eq_zero fun j hj => (eval_nodal_at_node (mem_erase.mpr ⟨(mem_erase.mp hj).1.symm, hi⟩))

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