nodalWeight_eq_eval_nodal_erase_inv

English

nodalWeight is the reciprocal product of differences with all other nodes.

Русский

Для конечного s и функции v вес узла i задаётся как произведение по j ∈ s\\{i} (v(i) − v(j))^{-1}.

LaTeX

$$$ \\operatorname{nodalWeight}(s,v,i) = \\prod_{j \\in s\\setminus i} (v(i) - v(j))^{-1}. $$$

Lean4

theorem nodalWeight_eq_eval_nodal_erase_inv : nodalWeight s v i = (eval (v i) (nodal (s.erase i) v))⁻¹ := by
  rw [eval_nodal, nodalWeight, prod_inv_distrib]

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