English
For a single-variable polynomial P with derivative P', the Newton map is x ↦ x − P(x)/P'(x). If P'(x) is not a unit, a junk value is used and the map returns x.
Русский
Для многочлена P с производной P' однократный Ньютонов переход задаётся как x ↦ x − P(x)/P'(x). Если P'(x) не является единицей, применяется запасная величина и отображение возвращает x.
LaTeX
$$$$N_P(x) = x - P'(x)^{-1} P(x)\,,$$ где $P'(x)$ обозначает производную и $P(x)$ её значение.$$
Lean4
/-- Given a single-variable polynomial `P` with derivative `P'`, this is the map:
`x ↦ x - P(x) / P'(x)`. When `P'(x)` is not a unit we use a junk-value pattern and send `x ↦ x`. -/
def newtonMap (x : S) : S :=
x - (Ring.inverse <| aeval x (derivative P)) * aeval x P
