Newton-Raphson method

Given a single-variable polynomial P with derivative P', Newton's method concerns iteration of the rational map: x ↦ x - P(x) / P'(x).

Over a field it can serve as a root-finding algorithm. It is also useful tool in certain proofs such as Hensel's lemma and Jordan-Chevalley decomposition.

Main definitions / results:

• Polynomial.newtonMap: the map x ↦ x - P(x) / P'(x), where P' is the derivative of the polynomial P.
• Polynomial.isFixedPt_newtonMap_of_isUnit_iff: x is a fixed point for Newton iteration iff it is a root of P (provided P'(x) is a unit).
• Polynomial.exists_unique_nilpotent_sub_and_aeval_eq_zero: if x is almost a root of P in the sense that that P(x) is nilpotent (and P'(x) is a unit) then we may write x as a sum x = n + r where n is nilpotent and r is a root of P. This can be used to prove the Jordan-Chevalley decomposition of linear endomorphims.

def Polynomial.newtonMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Polynomial R) (x : S) : S

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.

Equations

• Polynomial.newtonMap P x = x - Ring.inverse ((Polynomial.aeval x) (Polynomial.derivative P)) * (Polynomial.aeval x) P

theorem Polynomial.newtonMap_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Polynomial R) {x : S} : Polynomial.newtonMap P x = x - Ring.inverse ((Polynomial.aeval x) (Polynomial.derivative P)) * (Polynomial.aeval x) P

theorem Polynomial.newtonMap_apply_of_isUnit {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) : Polynomial.newtonMap P x = x - ↑(IsUnit.unit h)⁻¹ * (Polynomial.aeval x) P

theorem Polynomial.newtonMap_apply_of_not_isUnit {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : ¬IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) : Polynomial.newtonMap P x = x

theorem Polynomial.isNilpotent_iterate_newtonMap_sub_of_isNilpotent {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : IsNilpotent ((Polynomial.aeval x) P)) (n : ℕ) : IsNilpotent ((Polynomial.newtonMap P)^[n] x - x)

theorem Polynomial.isFixedPt_newtonMap_of_aeval_eq_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : (Polynomial.aeval x) P = 0) : Function.IsFixedPt (Polynomial.newtonMap P) x

theorem Polynomial.isFixedPt_newtonMap_of_isUnit_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) : Function.IsFixedPt (Polynomial.newtonMap P) x ↔ (Polynomial.aeval x) P = 0

theorem Polynomial.aeval_pow_two_pow_dvd_aeval_iterate_newtonMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : IsNilpotent ((Polynomial.aeval x) P)) (h' : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) (n : ℕ) : (Polynomial.aeval x) P ^ 2 ^ n ∣ (Polynomial.aeval ((Polynomial.newtonMap P)^[n] x)) P

This is really an auxiliary result, en route to Polynomial.exists_unique_nilpotent_sub_and_aeval_eq_zero.

theorem Polynomial.exists_unique_nilpotent_sub_and_aeval_eq_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : IsNilpotent ((Polynomial.aeval x) P)) (h' : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) : ∃! r : S, IsNilpotent (x - r) ∧ (Polynomial.aeval r) P = 0

If x is almost a root of P in the sense that that P(x) is nilpotent (and P'(x) is a unit) then we may write x as a sum x = n + r where n is nilpotent and r is a root of P. Moreover, n and r are unique.

This can be used to prove the Jordan-Chevalley decomposition of linear endomorphims.