Documentation

Mathlib.Dynamics.Newton

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: #

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
Instances For
    theorem Polynomial.newtonMap_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Polynomial R) {x : S} :
    P.newtonMap 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))) :
    P.newtonMap x = x - h.unit⁻¹ * (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))) :
    P.newtonMap 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 (P.newtonMap^[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 P.newtonMap 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))) :
    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 (P.newtonMap^[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 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.