Parity-change bound on real zeros

DefinitionNewton-type coefficient differences#✓fully proved

For a real polynomial \(f = \sum_k a_k x^k\) and a natural number \(k\), \(\tilde c_k(f) = (k+1)\,a_k^2 - k\,a_{k-1}a_{k+1}\), where \(a_j = 0\) for \(j\) above the degree of \(f\); for \(k = 0\) the second term vanishes, so \(\tilde c_0(f) = a_0^2\).

def cTilde (f : Polynomial ℝ) (k : ℕ) : ℝ :=
  ((k + 1 : ℕ) : ℝ) * (f.coeff k) ^ 2 -
    (k : ℝ) * f.coeff (k - 1) * f.coeff (k + 1)

Used by 1

Used byIndices with positive Newton-type difference

DefinitionIndices with positive Newton-type difference#✓fully proved

For a real polynomial \(f = a_0 + a_1 x + \dots + a_n x^n\) of degree \(n\) (with \(n = 0\) for \(f = 0\)), set \(a_{n+1} = 0\), \(\tilde c_0(f) = a_0^2\) and \(\tilde c_k(f) = (k+1)\,a_k^2 - k\,a_{k-1}a_{k+1}\) for \(1 \le k \le n\). This is the list of the indices \(k \in \{0, \dots, n\}\) with \(\tilde c_k(f) > 0\), in increasing order.

noncomputable def posIndices (f : Polynomial ℝ) : List ℕ :=
  ((Finset.range (f.natDegree + 1)).filter (fun k => 0 < cTilde f k)).sort (· ≤ ·)

Uses 1 · Used by 1

Statement usesNewton-type coefficient differences

Used byParity changes of the positive-difference indices

DefinitionParity changes of the positive-difference indices#✓fully proved

For a real polynomial \(f = a_0 + a_1 x + \dots + a_n x^n\) of degree \(n\) (with \(n = 0\) for \(f = 0\)), set \(a_{n+1} = 0\), \(\tilde c_0(f) = a_0^2\) and \(\tilde c_k(f) = (k+1)\,a_k^2 - k\,a_{k-1}a_{k+1}\) for \(1 \le k \le n\). Let \(k_1 < k_2 < \dots < k_m\) be the indices \(k \le n\) with \(\tilde c_k(f) > 0\). Then \(v(f)\) is the number of \(i < m\) such that \(k_i\) and \(k_{i+1}\) have different parities.

noncomputable def vVal (f : Polynomial ℝ) : ℕ :=
  ((posIndices f).zip ((posIndices f).drop 1)).countP
    (fun p => p.1 % 2 ≠ p.2 % 2)

Uses 1 · Used by 1

Statement usesIndices with positive Newton-type difference

Used byParity-change bound on real zeros (conjecture)

DefinitionParity-change bound on real zeros (conjecture)#✓fully proved

For a real polynomial \(f = a_0 + a_1 x + \dots + a_n x^n\) of degree \(n\), set \(a_{n+1} = 0\), \(\tilde c_0(f) = a_0^2\) and \(\tilde c_k(f) = (k+1)\,a_k^2 - k\,a_{k-1}a_{k+1}\) for \(1 \le k \le n\), and let \(v(f)\) be the number of parity changes between consecutive terms of the increasing list of indices \(k \le n\) with \(\tilde c_k(f) > 0\). The conjecture asserts that every such \(f\) with \(a_k > 0\) for all \(0 \le k \le n\) has at most \(v(f)\) distinct real zeros.

def conjecture : Prop :=
  ∀ f : Polynomial ℝ,
    (∀ k ∈ Finset.range (f.natDegree + 1), 0 < f.coeff k) →
    Set.ncard {x : ℝ | f.eval x = 0} ≤ vVal f

Sources

• AMR-021-0014.

Uses 1 · Used by 1

Statement usesParity changes of the positive-difference indices

Used byThe parity-change bound on real zeros is false

TheoremThe parity-change bound on real zeros is false#●ready to prove

For a real polynomial \(f = a_0 + a_1 x + \dots + a_n x^n\) of degree \(n\), set \(a_{n+1} = 0\), \(\tilde c_0(f) = a_0^2\) and \(\tilde c_k(f) = (k+1)\,a_k^2 - k\,a_{k-1}a_{k+1}\) for \(1 \le k \le n\), and let \(v(f)\) be the number of parity changes between consecutive terms of the increasing list of indices \(k \le n\) with \(\tilde c_k(f) > 0\). There is such an \(f\) with \(a_k > 0\) for all \(0 \le k \le n\) whose number of distinct real zeros exceeds \(v(f)\).

Katkova, Shapiro and Vishnyakova (Sec. 5) disprove Conjecture 9 via iterated primitives \(Q_n\) of an explicit \(Q_{15}\). Splitting the repeated root also refutes the distinct-zero reading used here: \(\prod_{j<23}(x+1+j/10^4)\,(38x^2-199x+363)\) has positive coefficients, 23 distinct real zeros and \(v = 21\).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• Olga Katkova, Boris Shapiro and Anna Vishnyakova, In search of Newton-type inequalities, arXiv:2403.12200 (2024), https://arxiv.org/abs/2403.12200.

Uses 1

Statement usesParity-change bound on real zeros (conjecture)

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.