English
The weight derivRootWeight(P,z,w) assigns to a root w of P a weight in a convex combination representing z as a center of mass of the roots of P; it is defined by the given piecewise rule.
Русский
Вес derivRootWeight(P,z,w) задаёт вклад корня w полинома P в представление точки z как центр масс корней P; задаётся по кусочной формуле.
LaTeX
$$\\operatorname{derivRootWeight}(P,z,w) = \\begin{cases} \\delta_{w,z}, & P(z)=0, \\\\ \\ \\frac{\\operatorname{rootMultiplicity}(w;P)}{|z-w|^2}, & P(z)\\neq 0. \\end{cases}$$
Lean4
/-- Given a polynomial `P` of positive degree and a root `z` of its derivative,
`derivRootWeight P z w` gives the weight of a root `w` of `P` in a convex combination
that is equal to `z`. -/
noncomputable def derivRootWeight (P : ℂ[X]) (z w : ℂ) : ℝ :=
if P.eval z = 0 then (Pi.single z 1 : ℂ → ℝ) w else P.rootMultiplicity w / ‖z - w‖ ^ 2
