Degree Comparison of Polynomials

Stream: Is there code for X?

[Han Han]

Is there any code for the following statement ? If P and Q are two nonconstant polynomials in ℝ[X] with positive leading coefficients, and if ∀ x : ℝ, eval x P ≤ eval x Q, then it follows that P.natDegree ≤ Q.natDegree. I find #docsPolynomial.isEquivalent_atTop_lead. But I don't know how to prove the above statement using this.

[Damiano Testa]

I think that assuming all x satisfy the inequality may imply that the polynomials are equal? Maybe you should assume positive x? Or sufficiently large?

[Yaël Dillies]

Not sure, Damiano :wink: Certainly x ≤ x + 1 but X ≠ X + 1. Though I agree that only assuming the inequality for sufficiently large x is the interesting case

[Damiano Testa]

Ah, yes, the difference is an everywhere nonnegative polynomial, not a vanishing one! :man_facepalming:

[Han Han]

I also agree that it's sufficient to assume the inequality holds for all sufficiently large x.

[Junyan Xu]

Would be nice to endow ℝ(X) with an ordered field structure this way:
image.png

[Antoine Chambert-Loir]

Yes and no. The orderings of R(X) are known. There are two orderings at each real number, one at + infinity and one at - infinity. No one is preferable.