Stable polynomials

12 fully proved

Mv Polynomial

DefinitionStable polynomials#✓fully proved

A complex multivariate polynomial is stable if it has no zero when every variable lies in the open upper half-plane.

public def IsStable {σ : Type*} (p : MvPolynomial σ ℂ) : Prop :=
  ∀ z : σ → ℂ, (∀ i, 0 < (z i).im) → eval z p ≠ 0

Used by 9

Used byReal-rootedness of univariate specializations of real stable polynomials · Real stable polynomials · The mixed differential preserves stability · Roots of specializations of stable polynomials lie in the closed lower half-plane · Subtracting a partial derivative preserves stability · Subtracting a partial derivative preserves real stability · Marcus--Spielman--Srivastava barrier bound · Real stability of the determinant polynomial · Stability of the determinant polynomial

DefinitionReal stable polynomials#✓fully proved

A complex multivariate polynomial is real stable if it is stable and has real coefficients.

public def IsRealStable {σ : Type*} (p : MvPolynomial σ ℂ) : Prop :=
  map (starRingEnd ℂ) p = p ∧ p.IsStable

Uses 1 · Used by 6

Statement usesStable polynomials

Used byReal-rootedness of univariate specializations of real stable polynomials · The mixed differential preserves real stability · Subtracting a partial derivative preserves real stability · Mixed characteristic polynomials of positive semidefinite matrices are real-rooted · Marcus--Spielman--Srivastava barrier bound · Real stability of the determinant polynomial

DefinitionUnivariate specialization#✓fully proved

Let \(R\) be a commutative ring, let \(p\) be a multivariate polynomial over \(R\) in variables \(X_j\) indexed by \(j \in \sigma\), and let \(i \in \sigma\) and \(x : \sigma \to R\). The univariate specialization of \(p\) at \(i\) and \(x\) is the polynomial in \(R[X]\) obtained from \(p\) by substituting \(X\) for \(X_i\) and the constant \(x_j\) for every \(X_j\) with \(j \ne i\); the value \(x_i\) is not used.

public noncomputable def univariateSpecialization {σ R : Type*} [CommRing R]
    (i : σ) [DecidableEq σ] (x : σ → R) (p : MvPolynomial σ R) : Polynomial R :=
  eval₂Hom Polynomial.C (fun j ↦ if j = i then Polynomial.X else Polynomial.C (x j)) p

Used by 10

Used byPartial derivatives under univariate specialization · Evaluating a univariate specialization · Real-rootedness of univariate specializations of real stable polynomials · Univariate specialization at real values preserves real coefficients · Roots of specializations of stable polynomials lie in the closed lower half-plane · Subtracting a partial derivative preserves stability · Mixed characteristic polynomials of positive semidefinite matrices are real-rooted · Marcus--Spielman--Srivastava barrier bound · Mixed characteristic polynomials are monic · Degree of a mixed characteristic polynomial

TheoremPartial derivatives under univariate specialization#✓fully proved

Let \(R\) be a commutative ring, let \(p\) be a multivariate polynomial over \(R\) in variables \(X_j\) indexed by \(j \in \sigma\), let \(i \in \sigma\) and \(x : \sigma \to R\), and for a polynomial \(q\) write \(q_{i,x} \in R[X]\) for its univariate specialization that keeps \(X_i\) as the variable \(X\) and sets every other \(X_j\) to \(x_j\). Then \((\partial p / \partial X_i)_{i,x} = (p_{i,x})'\), the derivative of \(p_{i,x}\).

public theorem derivative_univariateSpecialization {σ R : Type*} [CommRing R]
    (i : σ) [DecidableEq σ] (x : σ → R) (p : MvPolynomial σ R) :
    univariateSpecialization i x (pderiv i p) =
      Polynomial.derivative (univariateSpecialization i x p)

Uses 1 · Used by 2

Statement usesUnivariate specialization

Used bySubtracting a partial derivative preserves stability · Marcus--Spielman--Srivastava barrier bound

TheoremEvaluating a univariate specialization#✓fully proved

Let \(R\) be a commutative ring, let \(p\) be a multivariate polynomial over \(R\) in variables \(X_j\) indexed by \(j \in \sigma\), and let \(i \in \sigma\), \(x : \sigma \to R\) and \(t \in R\). Evaluating at \(t\) the univariate specialization of \(p\) that keeps \(X_i\) as the variable and sets every other \(X_j\) to \(x_j\) gives \(p(y)\), where \(y_i = t\) and \(y_j = x_j\) for \(j \ne i\).

public theorem eval_univariateSpecialization {σ R : Type*} [CommRing R]
    (i : σ) [DecidableEq σ] (x : σ → R) (t : R) (p : MvPolynomial σ R) :
    Polynomial.eval t (univariateSpecialization i x p) =
      MvPolynomial.eval (Function.update x i t) p

Uses 1 · Used by 4

Statement usesUnivariate specialization

Used byReal-rootedness of univariate specializations of real stable polynomials · Roots of specializations of stable polynomials lie in the closed lower half-plane · Subtracting a partial derivative preserves stability · Marcus--Spielman--Srivastava barrier bound

TheoremUnivariate specialization at real values preserves real coefficients#✓fully proved

Let \(p\) be a complex multivariate polynomial with real coefficients in variables \(X_j\) indexed by \(j \in \sigma\), let \(i \in \sigma\), and let \(a : \sigma \to \mathbb{C}\) with \(a_j\) real for every \(j \ne i\). Then the univariate specialization of \(p\) that keeps \(X_i\) as the variable and sets every other \(X_j\) to \(a_j\) has real coefficients.

public theorem map_star_univariateSpecialization {σ : Type*} [DecidableEq σ]
    (i : σ) (a : σ → ℂ) (p : MvPolynomial σ ℂ)
    (hp : MvPolynomial.map (starRingEnd ℂ) p = p)
    (ha : ∀ j, j ≠ i → (starRingEnd ℂ) (a j) = a j) :
    Polynomial.map (starRingEnd ℂ) (univariateSpecialization i a p) =
      univariateSpecialization i a p

Uses 1 · Used by 2

Statement usesUnivariate specialization

Used byReal-rootedness of univariate specializations of real stable polynomials · Marcus--Spielman--Srivastava barrier bound

Mv Polynomial Stable

TheoremRoots of specializations of stable polynomials lie in the closed lower half-plane#✓fully proved

Let \(p\) be a stable complex multivariate polynomial in variables \(X_j\) indexed by \(j \in \sigma\), let \(i \in \sigma\), and let \(a : \sigma \to \mathbb{C}\) with \(\operatorname{Im} a_j \ge 0\) for every \(j \ne i\). If the univariate specialization of \(p\) that keeps \(X_i\) as the variable and sets every other \(X_j\) to \(a_j\) is nonzero, then every root \(w\) of it satisfies \(\operatorname{Im} w \le 0\).

public theorem _root_.MvPolynomial.IsStable.roots_im_nonpos_univariateSpecialization
    {σ : Type*} [DecidableEq σ] {p : MvPolynomial σ ℂ} (hp : p.IsStable)
    (i : σ) (a : σ → ℂ) (ha : ∀ j, j ≠ i → 0 ≤ (a j).im)
    (hq : univariateSpecialization i a p ≠ 0) :
    ∀ w ∈ (univariateSpecialization i a p).roots, w.im ≤ 0

Uses 3 · Used by 1

Statement usesStable polynomials · Univariate specialization

Proof usesEvaluating a univariate specialization

Used byMarcus--Spielman--Srivastava barrier bound

TheoremReal-rootedness of univariate specializations of real stable polynomials#✓fully proved

Let \(p\) be a real stable complex multivariate polynomial in variables \(X_j\) indexed by \(j \in \sigma\), let \(i \in \sigma\), and for \(x : \sigma \to \mathbb{C}\) write \(p_{i,x} \in \mathbb{C}[X]\) for the univariate specialization of \(p\) that keeps \(X_i\) as the variable \(X\) and sets every other \(X_j\) to \(x_j\). Suppose there is a natural number \(d\) such that for every \(x : \sigma \to \mathbb{C}\) the polynomial \(p_{i,x}\) is monic of degree \(d\). Then for every \(a : \sigma \to \mathbb{C}\) with \(a_j\) real for all \(j \ne i\), the polynomial \(p_{i,a}\) is real-rooted.

public theorem _root_.MvPolynomial.isRealRooted_univariateSpecialization_of_isRealStable
    {σ : Type*} [DecidableEq σ] (i : σ) (p : MvPolynomial σ ℂ)
    (hp : p.IsRealStable) (d : ℕ)
    (hmonic : ∀ x, (univariateSpecialization i x p).Monic)
    (hdegree : ∀ x, (univariateSpecialization i x p).natDegree = d)
    (a : σ → ℂ) (ha : ∀ j, j ≠ i → (a j).im = 0) :
    (univariateSpecialization i a p).IsRealRooted

Uses 7 · Used by 1

Statement usesReal stable polynomials · Univariate specialization · Real-rooted polynomials

Proof usesStable polynomials · Evaluating a univariate specialization · Univariate specialization at real values preserves real coefficients · Conjugation-invariant polynomials with roots in the closed lower half-plane are real-rooted

Used byMixed characteristic polynomials of positive semidefinite matrices are real-rooted

TheoremSubtracting a partial derivative preserves stability#✓fully proved

Let \(p\) be a stable complex multivariate polynomial in variables \(X_j\) indexed by \(j \in \sigma\), let \(i \in \sigma\), and write \(\partial_i p\) for the partial derivative of \(p\) with respect to \(X_i\). Then \(p - \partial_i p\) is stable.

public theorem _root_.MvPolynomial.IsStable.sub_pderiv {σ : Type*}
    {p : MvPolynomial σ ℂ} (hp : p.IsStable) (i : σ) :
    (p - pderiv i p).IsStable

Uses 4 · Used by 2

Statement usesStable polynomials

Proof usesPartial derivatives under univariate specialization · Evaluating a univariate specialization · Univariate specialization

Used byThe mixed differential preserves stability · Subtracting a partial derivative preserves real stability

TheoremSubtracting a partial derivative preserves real stability#✓fully proved

Let \(p\) be a real stable complex multivariate polynomial in variables \(X_j\) indexed by \(j \in \sigma\), let \(i \in \sigma\), and write \(\partial_i p\) for the partial derivative of \(p\) with respect to \(X_i\). Then \(p - \partial_i p\) is real stable.

public theorem _root_.MvPolynomial.IsRealStable.sub_pderiv {σ : Type*}
    {p : MvPolynomial σ ℂ} (hp : p.IsRealStable) (i : σ) :
    (p - pderiv i p).IsRealStable

Uses 3 · Used by 2

Statement usesReal stable polynomials

Proof usesStable polynomials · Subtracting a partial derivative preserves stability

Used byThe mixed differential preserves real stability · Marcus--Spielman--Srivastava barrier bound

TheoremThe mixed differential preserves stability#✓fully proved

Let \(p\) be a stable complex multivariate polynomial in variables \(X_s\) indexed by \(s \in \sigma\), and write \(\partial_s\) for the partial derivative with respect to \(X_s\). For every finite list \((i_1, \dots, i_k)\) of indices in \(\sigma\) (repetitions allowed, possibly empty), the mixed differential of \(p\) along the list, \((1 - \partial_{i_k}) \cdots (1 - \partial_{i_1})\, p\), is stable.

public theorem _root_.MvPolynomial.IsStable.mixedDifferential {σ : Type*}
    {p : MvPolynomial σ ℂ} (hp : p.IsStable) (indices : List σ) :
    (MvPolynomial.mixedDifferential indices p).IsStable

Uses 5

Statement usesStable polynomials · Mixed differential operator

Proof usesSubtracting a partial derivative preserves stability · Mixed differential along a list with a given first index · Mixed differential along the empty list

TheoremThe mixed differential preserves real stability#✓fully proved

Let \(p\) be a real stable complex multivariate polynomial in variables \(X_s\) indexed by \(s \in \sigma\), and write \(\partial_s\) for the partial derivative with respect to \(X_s\). For every finite list \((i_1, \dots, i_k)\) of indices in \(\sigma\) (repetitions allowed, possibly empty), the mixed differential of \(p\) along the list, \((1 - \partial_{i_k}) \cdots (1 - \partial_{i_1})\, p\), is real stable.

public theorem _root_.MvPolynomial.IsRealStable.mixedDifferential {σ : Type*}
    {p : MvPolynomial σ ℂ} (hp : p.IsRealStable) (indices : List σ) :
    (MvPolynomial.mixedDifferential indices p).IsRealStable

Uses 5 · Used by 1

Statement usesReal stable polynomials · Mixed differential operator

Proof usesSubtracting a partial derivative preserves real stability · Mixed differential along a list with a given first index · Mixed differential along the empty list

Used byMixed characteristic polynomials of positive semidefinite matrices are real-rooted

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.