Liu's opposite-sign compatibility theorem

Two real polynomials $f$ and $g$ are compatible if every combination $\alpha f + \beta g$ with $\alpha, \beta \geq 0$ is real-rooted. When $f$ and $g$ have leading coefficients of the same sign, compatibility is governed by common interleavers (Chudnovsky–Seymour). Liu treats the case of opposite leading signs, where the answer is a root-count condition.

Write $n_p(x)$ for the number of roots of $p$ in $[x, \infty)$, counted with multiplicity.

Theorem (Liu, Theorem 2.1, corrected). Let $f$ and $g$ be nonconstant real-rooted polynomials with opposite leading signs. Then $f$ and $g$ are compatible if and only if one of the following holds:

after deleting the largest root from whichever of $f$ and $g$ has the larger largest root (from $f$ in case of a tie), the root counts of the resulting pair differ by at most one at every point;
$f$ and $g$ share a root $r$, and the cofactors $f/(x-r)$ and $g/(x-r)$ are compatible.

The second branch is missing from the published statement, and it is necessary: the forward direction of the published version fails for $x$ and $-x^2$, which share the root $0$.

Corollary (Liu, Corollary 2.2). Compatible real-rooted polynomials with opposite leading signs have degrees differing by at most two.

For pairs without common roots, the forward direction is first proved for polynomials with simple roots. Small derivative-shift regularizations, which preserve compatibility, reduce the general case to that one, and root matching passes back to the limit.

References

Lily L. Liu, “Polynomials with real zeros and compatible sequences,” Electronic Journal of Combinatorics 19(3) (2012), #P33.

Definitions

Opposite leading signs

RealRooted.LiuOppositeSigns.OppositeLeadingSignssource

def OppositeLeadingSigns (p q : ℝ[X]) : Prop :=
  p.leadingCoeff * q.leadingCoeff < 0

Number of roots in [x, ∞)

RealRooted.LiuOppositeSigns.rootCountAtOrAbovesource

def rootCountAtOrAbove (p : ℝ[X]) (x : ℝ) : ℕ :=
  (p.roots.filter (fun r => x ≤ r)).card

Root-count condition of the corrected Theorem 2.1

RealRooted.LiuOppositeSigns.theorem21RootCountBranchesWithCommonsource

def theorem21RootCountBranchesWithCommon (f g : ℝ[X]) : Prop :=
  theorem21RootCountBranches f g ∨ CommonRootDeletionCompatibleBranch f g

Theorems

Liu, Theorem 2.1 (corrected)

RealRooted.LiuOppositeSigns.compatible_iff_theorem21RootCountBranchesWithCommon_nonconstantsource

theorem compatible_iff_theorem21RootCountBranchesWithCommon_nonconstant
    {f g : ℝ[X]} (hf : f.Splits) (hg : g.Splits)
    (hsgn : OppositeLeadingSigns f g)
    (hf_deg : f.natDegree ≠ 0) (hg_deg : g.natDegree ≠ 0) :
    Compatible f g ↔ theorem21RootCountBranchesWithCommon f g

Theorem 2.1 for pairs without common roots

RealRooted.LiuOppositeSigns.theorem21CompatibleRootCountNoCommonNonconstantsource

theorem theorem21CompatibleRootCountNoCommonNonconstant :
    theorem21CompatibleRootCountNoCommonNonconstantStatement

The published Theorem 2.1 fails

RealRooted.LiuOppositeSigns.not_theorem21CompatibleToRootCountBranchesNonconstantStatementsource

theorem not_theorem21CompatibleToRootCountBranchesNonconstantStatement :
    ¬ theorem21CompatibleToRootCountBranchesNonconstantStatement

Liu, Corollary 2.2: degrees differ by at most two

RealRooted.LiuOppositeSigns.corollary22DegreeDiff_proofsource

theorem corollary22DegreeDiff_proof : corollary22DegreeDiffStatement

Liu's opposite-sign compatibility theorem

References

≔ Definitions

⊢ Theorems

Definitions

Theorems