Eventual sign of polynomials

This file proves that a polynomial has a fixed sign beyond its largest or smallest root.

Main statements

• zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg: If x is larger than all roots of P and the leading coefficient of P is nonnegative then P (x) is positive.
• zero_le_eval_of_roots_le_of_leadingCoeff_nonneg: If we only assume that x is at least as large as all roots, then P (x) is nonnegative.
• eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos, eval_le_zero_of_roots_le_of_leadingCoeff_nonpos: Versions of the above when the leading coefficient of P is nonpositive.
• zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg, zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg, negOnePow_mul_eval_lt_zero_of_lt_roots_of_leadingCoeff_nonpos, negOnePow_mul_eval_le_zero_of_le_roots_of_leadingCoeff_nonpos: Analogous results for x which is smaller than (or at least as small as) all roots.

TODO

Generalize to real-closed fields.

theorem Polynomial.zero_lt_eval_of_roots_lt_of_leadingCoeff_nonneg {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → y < x) (hlc : 0 ≤ P.leadingCoeff) : 0 < eval x P

theorem Polynomial.zero_le_eval_of_roots_le_of_leadingCoeff_nonneg {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x) (hlc : 0 ≤ P.leadingCoeff) : 0 ≤ eval x P

theorem Polynomial.eval_lt_zero_of_roots_lt_of_leadingCoeff_nonpos {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → y < x) (hlc : P.leadingCoeff ≤ 0) : eval x P < 0

theorem Polynomial.eval_le_zero_of_roots_le_of_leadingCoeff_nonpos {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → y ≤ x) (hlc : P.leadingCoeff ≤ 0) : eval x P ≤ 0

theorem Polynomial.zero_lt_negOnePow_mul_eval_of_lt_roots_of_leadingCoeff_nonneg {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → x < y) (hlc : 0 ≤ P.leadingCoeff) : 0 < ↑↑(↑P.natDegree).negOnePow * eval x P

theorem Polynomial.zero_le_negOnePow_mul_eval_of_le_roots_of_leadingCoeff_nonneg {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y) (hlc : 0 ≤ P.leadingCoeff) : 0 ≤ ↑↑(↑P.natDegree).negOnePow * eval x P

theorem Polynomial.negOnePow_mul_eval_lt_zero_of_lt_roots_of_leadingCoeff_nonpos {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → x < y) (hlc : P.leadingCoeff ≤ 0) : ↑↑(↑P.natDegree).negOnePow * eval x P < 0

theorem Polynomial.negOnePow_mul_eval_le_zero_of_le_roots_of_leadingCoeff_nonpos {P : Polynomial ℝ} {x : ℝ} (hroots : ∀ (y : ℝ), P.IsRoot y → x ≤ y) (hlc : P.leadingCoeff ≤ 0) : ↑↑(↑P.natDegree).negOnePow * eval x P ≤ 0