Interlacing families of polynomials

DefinitionUpper interlacing point#✓fully proved

Let \(p\) be a complex polynomial and let \(\operatorname{maxroot}(p)\) be the largest real part of an element of the multiset of roots of \(p\), with \(\operatorname{maxroot}(p) = 0\) when that multiset is empty (as it is for nonzero constants and for \(p = 0\)). A real number \(a\) is an upper interlacing point of \(p\) if \(a \le \operatorname{maxroot}(p)\) and, after removing one copy of \(\operatorname{maxroot}(p)\) from the multiset of roots of \(p\) (if it occurs there), every remaining root has real part at most \(a\).

public def HasUpperInterlacingPoint (p : Polynomial ℂ) (a : ℝ) : Prop :=
  a ≤ p.maxRealRoot ∧
    ∀ z ∈ p.roots.erase (p.maxRealRoot : ℂ), z.re ≤ a

Uses 1 · Used by 3

Statement usesLargest real part of a root

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 · Common upper interlacing point

DefinitionCommon upper interlacing point#✓fully proved

A family \((P_i)_{i \in I}\) of complex polynomials, indexed by an arbitrary type \(I\), has a common upper interlacing point if some real number \(a\) is an upper interlacing point of \(P_i\) for every \(i \in I\).

public def HasCommonUpperInterlacing {ι : Type*} (P : ι → Polynomial ℂ) : Prop :=
  ∃ a : ℝ, ∀ i, (P i).HasUpperInterlacingPoint a

Uses 1 · Used by 1

Statement usesUpper interlacing point

Used byCommon upper interlacing bounds some member's largest root by a weighted sum's

TheoremNonpositivity between an upper interlacing point and the largest root#✓fully proved

Let \(p\) be a monic complex polynomial of positive degree all of whose roots are real, let \(\operatorname{maxroot}(p)\) be its largest root, and let \(a\) be an upper interlacing point of \(p\). Then for every real \(x\) with \(a \le x \le \operatorname{maxroot}(p)\), the real part of \(p(x)\) is at most \(0\).

public theorem eval_re_nonpos_of_upperInterlacing
    {p : Polynomial ℂ} (hmonic : p.Monic) (hrooted : p.IsRealRooted)
    {a x : ℝ} (ha : p.HasUpperInterlacingPoint a) (hax : a ≤ x)
    (hx : x ≤ p.maxRealRoot) (hdegree : 0 < p.natDegree) :
    (p.eval (x : ℂ)).re ≤ 0

Uses 4 · Used by 1

Statement usesUpper interlacing point · Real-rooted polynomials · Largest real part of a root

Proof usesFor a real-rooted polynomial, the largest real part of a root is a root

Used byCommon upper interlacing bounds some member's largest root by a weighted sum's

TheoremCommon upper interlacing bounds some member's largest root by a weighted sum's#✓fully proved

Let \(I\) be a nonempty finite set and, for each \(i \in I\), let \(P_i\) be a monic complex polynomial of positive degree all of whose roots are real, such that the family \((P_i)_{i \in I}\) has a common upper interlacing point. Let \(w_i \ge 0\) be real weights such that \(Q = \sum_{i \in I} w_i P_i\) is monic and all of its roots are real. Then there is \(i \in I\) with \(\operatorname{maxroot}(P_i) \le \operatorname{maxroot}(Q)\), where \(\operatorname{maxroot}(f)\) denotes the largest root of a real-rooted polynomial \(f\).

public theorem exists_maxRealRoot_le_weightedSum_of_commonUpperInterlacing
    {ι : Type*} [Fintype ι] [Nonempty ι] (w : ι → ℝ) (P : ι → Polynomial ℂ)
    (hw : ∀ i, 0 ≤ w i) (hmonic : ∀ i, (P i).Monic)
    (hrooted : ∀ i, (P i).IsRealRooted) (hdegree : ∀ i, 0 < (P i).natDegree)
    (hcommon : Polynomial.HasCommonUpperInterlacing P)
    (hsumMonic : (∑ i, (w i : ℂ) • P i).Monic)
    (hsumRooted : (∑ i, (w i : ℂ) • P i).IsRealRooted) :
    ∃ i, (P i).maxRealRoot ≤ (∑ j, (w j : ℂ) • P j).maxRealRoot

Uses 6

Statement usesCommon upper interlacing point · Real-rooted polynomials · Largest real part of a root

Proof usesUpper interlacing point · Nonpositivity between an upper interlacing point and the largest root · Monic real-rooted polynomials have positive real part right of the largest root

TheoremSome member's largest root is at most that of a weighted sum, via real-rooted segments#✓fully proved

Let \(I\) be a nonempty finite set, let \(n \ge 1\), and for each \(i \in I\) let \(P_i\) be a monic complex polynomial of degree \(n\) and \(w_i \ge 0\) a real weight. Suppose that \(Q = \sum_{i \in I} w_i P_i\) is monic of degree \(n\) and that, for every \(i \in I\) and every \(t \in [0, 1]\), all roots of \((1 - t) Q + t P_i\) are real. Then there is \(i \in I\) with \(\operatorname{maxroot}(P_i) \le \operatorname{maxroot}(Q)\), where \(\operatorname{maxroot}(f)\) denotes the largest real part of a root of \(f\).

public theorem exists_maxRealRoot_le_weightedSum_of_segment_realRooted
    {ι : Type*} [Fintype ι] (hne : Nonempty ι) (w : ι → ℝ) (P : ι → Polynomial ℂ)
    {n : ℕ} (hn : 0 < n) (hw : ∀ i, 0 ≤ w i)
    (hfamily : ∀ i, (P i).IsMonicOfDegree n)
    (hsum : (∑ i, (w i : ℂ) • P i).IsMonicOfDegree n)
    (hsegments : ∀ i t, t ∈ Set.Icc (0 : ℝ) 1 →
      ((1 - (t : ℂ)) • (∑ j, (w j : ℂ) • P j) + (t : ℂ) • P i).IsRealRooted) :
    ∃ i, (P i).maxRealRoot ≤ (∑ j, (w j : ℂ) • P j).maxRealRoot

Uses 5 · Used by 1

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

Proof usesFor a real-rooted polynomial, the largest real part of a root is a root · Monic real-rooted polynomials have positive real part right of the largest root · Real parts of roots are bounded by the largest one

Used byAn outcome bounded by the mixed characteristic polynomial

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.