Cauchy's bound on polynomial roots.

The bound is given by Polynomial.cauchyBound, which for a_n x^n + a_(n-1) x^(n - 1) + ⋯ + a_0 is is 1 + max_(0 ≤ i < n) a_i / a_n.

The theorem that this gives a bound to polynomial roots is Polynomial.IsRoot.norm_lt_cauchyBound.

noncomputable def Polynomial.cauchyBound {K : Type u_1} [NormedDivisionRing K] (p : Polynomial K) : NNReal

Cauchy's bound on the roots of a given polynomial. See IsRoot.norm_lt_cauchyBound for the proof that the roots satisfy this bound.

Equations

• p.cauchyBound = ((Finset.range p.natDegree).sup fun (x : ℕ) => ‖p.coeff x‖₊) / ‖p.leadingCoeff‖₊ + 1

@[simp]

theorem Polynomial.one_le_cauchyBound {K : Type u_1} [NormedDivisionRing K] (p : Polynomial K) : 1 ≤ p.cauchyBound

@[simp]

theorem Polynomial.cauchyBound_zero {K : Type u_1} [NormedDivisionRing K] : cauchyBound 0 = 1

@[simp]

theorem Polynomial.cauchyBound_C {K : Type u_1} [NormedDivisionRing K] (x : K) : (C x).cauchyBound = 1

@[simp]

theorem Polynomial.cauchyBound_one {K : Type u_1} [NormedDivisionRing K] : cauchyBound 1 = 1

@[simp]

theorem Polynomial.cauchyBound_X {K : Type u_1} [NormedDivisionRing K] : X.cauchyBound = 1

@[simp]

theorem Polynomial.cauchyBound_X_add_C {K : Type u_1} [NormedDivisionRing K] (x : K) : (X + C x).cauchyBound = ‖x‖₊ + 1

@[simp]

theorem Polynomial.cauchyBound_X_sub_C {K : Type u_1} [NormedDivisionRing K] (x : K) : (X - C x).cauchyBound = ‖x‖₊ + 1

@[simp]

theorem Polynomial.cauchyBound_smul {K : Type u_1} [NormedDivisionRing K] {x : K} (hx : x ≠ 0) (p : Polynomial K) : (x • p).cauchyBound = p.cauchyBound

theorem Polynomial.IsRoot.norm_lt_cauchyBound {K : Type u_1} [NormedDivisionRing K] {p : Polynomial K} (hp : p ≠ 0) {a : K} (h : p.IsRoot a) : ‖a‖₊ < p.cauchyBound

cauchyBound is a bound on the norm of polynomial roots.