Real-rooted polynomials

DefinitionReal-rooted polynomials#✓fully proved

A complex polynomial \(p\) is real-rooted if every element \(z\) of its multiset of roots is real, that is, \(\operatorname{Im} z = 0\).

public def IsRealRooted (p : Polynomial ℂ) : Prop :=
  ∀ z ∈ p.roots, z.im = 0

Used by 16

Used byNonpositivity between an upper interlacing point and the largest root · Common upper interlacing bounds some member's largest root by a weighted sum's · Some member's largest root is at most that of a weighted sum, via real-rooted segments · For a real-rooted polynomial, the largest real part of a root is a root · Monic real-rooted polynomials have nonnegative real part from the largest root on · Monic real-rooted polynomials have positive real part right of the largest root · Conjugation-invariant polynomials with roots in the closed lower half-plane are real-rooted · Real-rootedness of univariate specializations of real stable polynomials · An outcome bounded by the mixed characteristic polynomial · Mixed characteristic polynomials of positive semidefinite matrices are real-rooted · Marcus--Spielman--Srivastava barrier bound · Stanley's Problem 20' on chain polynomials of distributive lattices · Neggers' conjecture · Real-rootedness of the minuscule polynomials · The Haglund–Ono–Wagner monotone column permanent conjecture · Hermitian matrices have real-rooted characteristic polynomials

TheoremConjugation-invariant polynomials with roots in the closed lower half-plane are real-rooted#✓fully proved

Let \(p\) be a nonzero complex polynomial that is unchanged when complex conjugation is applied to each of its coefficients. If every root \(z\) of \(p\) satisfies \(\operatorname{Im} z \le 0\), then \(p\) is real-rooted.

public theorem isRealRooted_of_map_star_eq_self_of_roots_im_nonpos
    (p : Polynomial ℂ) (hp0 : p ≠ 0)
    (hreal : Polynomial.map (starRingEnd ℂ) p = p)
    (hupper : ∀ z ∈ p.roots, z.im ≤ 0) : p.IsRealRooted

Uses 1 · Used by 2

Statement usesReal-rooted polynomials

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

DefinitionLargest real part of a root#✓fully proved

For a complex polynomial \(p\), let \(\rho(p)\) be the largest real part \(\operatorname{Re} z\) of an element \(z\) of the multiset of roots of \(p\), with \(\rho(p) = 0\) when that multiset is empty (as it is for nonzero constants and for \(p = 0\)).

public noncomputable def maxRealRoot (p : Polynomial ℂ) : ℝ :=
  if h : (p.roots.map Complex.re).toFinset.Nonempty then
    (p.roots.map Complex.re).toFinset.max' h
  else 0

Used by 13

Used byNonpositivity between an upper interlacing point and the largest root · Common upper interlacing bounds some member's largest root by a weighted sum's · Some member's largest root is at most that of a weighted sum, via real-rooted segments · Upper interlacing point · For a real-rooted polynomial, the largest real part of a root is a root · Monic real-rooted polynomials have nonnegative real part from the largest root on · Monic real-rooted polynomials have positive real part right of the largest root · The largest real part of a root is attained · Real parts of roots are bounded by the largest one · An outcome bounded by the mixed characteristic polynomial · Marcus--Spielman--Srivastava bound, finite-support form · Marcus--Spielman--Srivastava barrier bound · Spectral norm of a positive semidefinite matrix

TheoremReal parts of roots are bounded by the largest one#✓fully proved

Let \(p\) be a complex polynomial and let \(\rho(p)\) be the largest real part of an element of its multiset of roots, or \(0\) if that multiset is empty. Then every element \(z\) of the multiset of roots of \(p\) satisfies \(\operatorname{Re} z \le \rho(p)\).

public theorem root_re_le_maxRealRoot {p : Polynomial ℂ} {z : ℂ} (hz : z ∈ p.roots) :
    z.re ≤ p.maxRealRoot

Uses 1 · Used by 4

Statement usesLargest real part of a root

Used bySome member's largest root is at most that of a weighted sum, via real-rooted segments · Monic real-rooted polynomials have nonnegative real part from the largest root on · Monic real-rooted polynomials have positive real part right of the largest root · Spectral norm of a positive semidefinite matrix

TheoremThe largest real part of a root is attained#✓fully proved

Let \(p\) be a complex polynomial whose multiset of roots is nonempty, and let \(\rho(p)\) be the largest real part of a root of \(p\). Then some root \(z\) of \(p\) satisfies \(\operatorname{Re} z = \rho(p)\).

public theorem exists_root_re_eq_maxRealRoot {p : Polynomial ℂ} (hp : p.roots ≠ 0) :
    ∃ z ∈ p.roots, z.re = p.maxRealRoot

Uses 1 · Used by 1

Statement usesLargest real part of a root

Used byFor a real-rooted polynomial, the largest real part of a root is a root

TheoremNonconstant complex polynomials have a root#✓fully proved

Every complex polynomial of positive degree has at least one root.

public theorem roots_ne_zero_of_natDegree_pos {p : Polynomial ℂ} (hp : 0 < p.natDegree) :
    p.roots ≠ 0

Used by 1

Used byFor a real-rooted polynomial, the largest real part of a root is a root

TheoremFor a real-rooted polynomial, the largest real part of a root is a root#✓fully proved

Let \(p\) be a real-rooted complex polynomial of positive degree, and let \(\rho(p)\) be the largest real part of a root of \(p\). Then the real number \(\rho(p)\), viewed as a complex number, is a root of \(p\).

public theorem coe_maxRealRoot_mem_roots {p : Polynomial ℂ} (hp : p.IsRealRooted)
    (hdegree : 0 < p.natDegree) : (p.maxRealRoot : ℂ) ∈ p.roots

Uses 4 · Used by 4

Statement usesReal-rooted polynomials · Largest real part of a root

Proof usesThe largest real part of a root is attained · Nonconstant complex polynomials have a root

Used byNonpositivity between an upper interlacing point and the largest root · Some member's largest root is at most that of a weighted sum, via real-rooted segments · Marcus--Spielman--Srivastava barrier bound · Spectral norm of a positive semidefinite matrix

TheoremMonic real-rooted polynomials have positive real part right of the largest root#✓fully proved

Let \(p\) be a monic real-rooted complex polynomial, and let \(\rho(p)\) be the largest real part of a root of \(p\), or \(0\) if \(p\) has no roots. Then \(\operatorname{Re} p(x) > 0\) for every real number \(x > \rho(p)\).

public theorem eval_re_pos_of_maxRealRoot_lt {p : Polynomial ℂ} (hmonic : p.Monic)
    (hrooted : p.IsRealRooted) {x : ℝ} (hx : p.maxRealRoot < x) :
    0 < (p.eval (x : ℂ)).re

Uses 3 · Used by 2

Statement usesReal-rooted polynomials · Largest real part of a root

Proof usesReal parts of roots are bounded by the largest one

Used byCommon upper interlacing bounds some member's largest root by a weighted sum's · Some member's largest root is at most that of a weighted sum, via real-rooted segments

TheoremMonic real-rooted polynomials have nonnegative real part from the largest root on#✓fully proved

Let \(p\) be a monic real-rooted complex polynomial, and let \(\rho(p)\) be the largest real part of a root of \(p\), or \(0\) if \(p\) has no roots. Then \(\operatorname{Re} p(x) \ge 0\) for every real number \(x \ge \rho(p)\).

public theorem eval_re_nonneg_of_maxRealRoot_le {p : Polynomial ℂ} (hmonic : p.Monic)
    (hrooted : p.IsRealRooted) {x : ℝ} (hx : p.maxRealRoot ≤ x) :
    0 ≤ (p.eval (x : ℂ)).re

Uses 3

Statement usesReal-rooted polynomials · Largest real part of a root

Proof usesReal parts of roots are bounded by the largest one

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.