Borcea–Brändén finite-symbol theorems

A linear operator on a finite multidegree box preserves stability precisely in the rank-one or stable-symbol cases. The real univariate theorem gives the corresponding positive-symbol criterion for bounded-degree polynomials.

References

J. Borcea and P. Brändén, “The Lee–Yang and Pólya–Schur programs. I. Linear operators preserving stability,” Inventiones Mathematicae 177 (2009), 541–569. See the finite-symbol discussion on symmetricfunctions.com.

Definitions

Stability preserver on a degree box

RealRooted.BorceaBranden.PreservesComplexStabilityOnDegreeBoxsource

def PreservesComplexStabilityOnDegreeBox
    {σ : Type*} [Fintype σ] (κ : σ → ℕ)
    (T : MvPolynomial.degreeOfLE σ ℂ κ →ₗ[ℂ] MvPolynomial σ ℂ) : Prop :=
  ∀ f, MvUpperHalfPlaneStable f.1 →
    MvUpperHalfPlaneStableOrZero (T f)

Rank-one operator with stable image

RealRooted.BorceaBranden.HasStableRankOneRepresentationsource

def HasStableRankOneRepresentation
    {σ : Type*} [Fintype σ] (κ : σ → ℕ)
    (T : MvPolynomial.degreeOfLE σ ℂ κ →ₗ[ℂ] MvPolynomial σ ℂ) : Prop :=
  ∃ (α : MvPolynomial.degreeOfLE σ ℂ κ →ₗ[ℂ] ℂ)
      (P : MvPolynomial σ ℂ),
    MvUpperHalfPlaneStable P ∧ ∀ f, T f = (α f) • P

Algebraic symbol of an operator

RealRooted.BorceaBranden.finiteAlgebraicSymbolsource

def finiteAlgebraicSymbol (d : ℕ) (T : ℝ[X] →ₗ[ℝ] ℝ[X]) :
    MvPolynomial (Fin 2) ℝ :=
  ∑ k ∈ Finset.range (d + 1),
    MvPolynomial.C (Nat.choose d k : ℝ) *
      polynomialInFirstMv (T ((X : ℝ[X]) ^ k)) *
        (MvPolynomial.X (1 : Fin 2)) ^ (d - k)

Real-rootedness preserver up to degree d

RealRooted.BorceaBranden.PreservesRealRootedUpTosource

def PreservesRealRootedUpTo
    (d : ℕ) (T : ℝ[X] →ₗ[ℝ] ℝ[X]) : Prop :=
  ∀ {p : ℝ[X]}, p.natDegree ≤ d → p.Splits → T p = 0 ∨ (T p).Splits

Theorems

Classification of stability preservers on a degree box

RealRooted.BorceaBranden.finiteComplexSymbolClassificationsource

theorem finiteComplexSymbolClassification :
    finiteComplexSymbolClassificationStatement

Finite-symbol theorem for real-rootedness preservers

RealRooted.BorceaBranden.finiteSymbolTheoremsource

theorem finiteSymbolTheorem :
    RealRooted.BorceaBranden.finiteSymbolTheoremStatement

A stable symbol gives a real-rootedness preserver

RealRooted.BorceaBranden.finiteSymbol_preservesRealRootedUpTosource

theorem finiteSymbol_preservesRealRootedUpTo
    {d : ℕ} {T : ℝ[X] →ₗ[ℝ] ℝ[X]}
    (hSymbol : MvUpperHalfPlaneStable
      (complexifyMv
        (RealRooted.BorceaBranden.finiteAlgebraicSymbol d T))) :
    RealRooted.BorceaBranden.PreservesRealRootedUpTo d T

Borcea–Brändén finite-symbol theorems

References

≔ Definitions

⊢ Theorems

Definitions

Theorems