Polynomial signs at infinity over an ordered field #
A coefficient bound makes the leading term dominate all lower terms. The bound belongs to the field itself; no Archimedean assumption is used.
theorem
Polynomial.exists_sign_atTop
{R : Type u_1}
[Field R]
[LinearOrder R]
[IsStrictOrderedRing R]
(p : Polynomial R)
:
∃ (B : R), ∀ (x : R), B < x → SignType.sign (eval x p) = SignType.sign p.leadingCoeff
Beyond a field-valued coefficient bound, a polynomial has the sign of its leading coefficient.
theorem
Polynomial.exists_sign_atBot
{R : Type u_1}
[Field R]
[LinearOrder R]
[IsStrictOrderedRing R]
(p : Polynomial R)
:
∃ (B : R), ∀ x < B, SignType.sign (eval x p) = SignType.sign (p.leadingCoeff * (-1) ^ p.natDegree)
Below some field-valued bound, the sign gains the degree-parity factor.
theorem
List.exists_signs_atTop
{R : Type u_1}
[Field R]
[LinearOrder R]
[IsStrictOrderedRing R]
(cs : List (Polynomial R))
:
∃ (B : R), ∀ p ∈ cs, ∀ (x : R), B < x → SignType.sign (Polynomial.eval x p) = SignType.sign p.leadingCoeff
A uniform right bound for the leading-coefficient signs of a polynomial list.
theorem
List.exists_signs_atBot
{R : Type u_1}
[Field R]
[LinearOrder R]
[IsStrictOrderedRing R]
(cs : List (Polynomial R))
:
∃ (B : R), ∀ p ∈ cs, ∀ x < B, SignType.sign (Polynomial.eval x p) = SignType.sign (p.leadingCoeff * (-1) ^ p.natDegree)
A uniform left bound for the degree-parity signs of a polynomial list.