Newton's inequalities

If a real polynomial of degree n is real-rooted, its elementary symmetric functions e_k of the roots satisfy e_k² · C(n, k-1) · C(n, k+1) ≥ e_{k-1} · e_{k+1} · C(n, k)²; equivalently the normalized means e_k / C(n, k) form a log-concave sequence.

The proof is the classical reduction: real-rootedness is preserved by differentiation (Rolle) and by reversal x ↦ 1/x, and suitable derivatives and one reversal reduce each index to a real-rooted quadratic, whose discriminant is nonnegative.

Main results

• Newton.RealRooted.derivative, Newton.RealRooted.reverse: real-rootedness is preserved by derivative and Polynomial.reverse.
• Newton.realRooted_quadratic_discrim: a real-rooted quadratic has nonnegative discriminant.
• Newton.newton_inequality_coeff: the coefficient form a_i² · C(n, i-1) · C(n, i+1) ≥ a_{i-1} · a_{i+1} · C(n, i)².
• Newton.newton_inequality: the form with Multiset.esymm of the roots, for monic p.
• Newton.newton_logConcave: log-concavity of the normalized means.

References

• G. H. Hardy, J. E. Littlewood, G. Pólya, Inequalities, 2nd ed., Cambridge University Press, 1952, Chapter II.
• I. Newton, Arithmetica universalis, 1707.

theorem Newton.RealRooted.derivative {p : Polynomial ℝ} (hp : MSS.RealRooted p) : MSS.RealRooted (Polynomial.derivative p)

(1) Rolle lemma. The derivative of a real-rooted real polynomial is real-rooted.

theorem Newton.RealRooted.reverse {p : Polynomial ℝ} (hp : MSS.RealRooted p) : MSS.RealRooted p.reverse

Real-rootedness is preserved by the reversal x ↦ 1/x. (The constant term may vanish: reversal just drops trailing zeros, and the resulting product of ≤ 1-degree factors still splits.)

theorem Newton.realRooted_quadratic_discrim {a b c : ℝ} (ha : a ≠ 0) (h : MSS.RealRooted (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)) : b ^ 2 - 4 * a * c ≥ 0

(2) Base case. A real-rooted real quadratic a x² + b x + c (a ≠ 0) has b² - 4ac ≥ 0.

theorem Newton.RealRooted.iterate_derivative {p : Polynomial ℝ} (hp : MSS.RealRooted p) (k : ℕ) : MSS.RealRooted ((⇑Polynomial.derivative)^[k] p)

Real-rootedness is preserved by iterated differentiation (iterate Rolle).

theorem Newton.realRooted_discrim_coeff {q : Polynomial ℝ} (hq : MSS.RealRooted q) (hdeg : q.natDegree ≤ 2) : q.coeff 1 ^ 2 ≥ 4 * q.coeff 2 * q.coeff 0

(2′) Base case, coefficient form. A real-rooted polynomial of natDegree ≤ 2 satisfies the discriminant inequality on its low coefficients: a₁² ≥ 4 a₂ a₀. (For natDegree < 2 the leading a₂ = 0 makes it a₁² ≥ 0.) This is the form the reduction below consumes.

theorem Newton.newton_inequality_coeff {p : Polynomial ℝ} (hp : MSS.RealRooted p) {i : ℕ} (hi : 1 ≤ i) (hi2 : i + 1 ≤ p.natDegree) : p.coeff i ^ 2 * (↑(p.natDegree.choose (i - 1)) * ↑(p.natDegree.choose (i + 1))) ≥ p.coeff (i - 1) * p.coeff (i + 1) * ↑(p.natDegree.choose i) ^ 2

Newton's inequalities, coefficient form. For a real-rooted real polynomial p of degree n, the coefficients aⱼ = p.coeff j satisfy, for 1 ≤ i ≤ n-1, a_i² · C(n,i-1)·C(n,i+1) ≥ a_{i-1}·a_{i+1} · C(n,i)².

Proof (the classical reduction): g := Dᴺ⁻²(reverse(Dⁱ⁻¹ p)) with N = n-i+1 is a real-rooted polynomial of natDegree ≤ 2 whose three low coefficients are factorial multiples of a_{i-1}, a_i, a_{i+1}; its discriminant b²-4ac ≥ 0 (realRooted_discrim_coeff) is exactly this inequality after clearing positive factorials (Nat.choose_mul_factorial_mul_factorial).

theorem Newton.newton_inequality {p : Polynomial ℝ} (hp : MSS.RealRooted p) (hmonic : p.Monic) {k : ℕ} (hk : 1 ≤ k) (hk2 : k + 1 ≤ p.natDegree) : p.roots.esymm k ^ 2 * (↑(p.natDegree.choose (k - 1)) * ↑(p.natDegree.choose (k + 1))) ≥ p.roots.esymm (k - 1) * p.roots.esymm (k + 1) * ↑(p.natDegree.choose k) ^ 2

(3) Newton's inequalities. For a monic real-rooted polynomial of degree n with roots multiset s = p.roots, for 1 ≤ k ≤ n-1, e_k(s)² · C(n,k-1)·C(n,k+1) ≥ e_{k-1}(s)·e_{k+1}(s) · C(n,k)².

theorem Newton.newton_logConcave {p : Polynomial ℝ} (hp : MSS.RealRooted p) (hmonic : p.Monic) {k : ℕ} (hk : 1 ≤ k) (hk2 : k + 1 ≤ p.natDegree) : p.roots.esymm (k - 1) / ↑(p.natDegree.choose (k - 1)) * (p.roots.esymm (k + 1) / ↑(p.natDegree.choose (k + 1))) ≤ (p.roots.esymm k / ↑(p.natDegree.choose k)) ^ 2

Corollary (log-concavity of normalized means). p_{k-1} · p_{k+1} ≤ p_k².