Theorems

Matrices preserving interlacing sequences

A nonnegative polynomial matrix preserves interlacing sequences when every ordered $2 \times 2$ submatrix satisfies the affine interlacing condition. A zero-aware form allows output rows to vanish.

References

S. Fisk, Polynomials, roots, and interlacing, 2006, Chapter 3, develops matrices preserving interlacing. P. Brändén gives the exact nonnegative polynomial characterization in “Unimodality, log-concavity, real-rootedness and beyond,” Handbook of Enumerative Combinatorics, 2015, Theorem 7.8.5. See the matrix criterion on symmetricfunctions.com.

Definitions

  • A polynomial matrix acting on a sequence

    RealRooted.matPolyActionsource
    def matPolyAction (G : List (List ℝ[X])) (fs : List ℝ[X]) : List ℝ[X] :=
  G.map (fun row => (row.zipWith (· * ·) fs).sum)

  • 2 × 2 interlacing condition

    RealRooted.Has2x2InterlacingPropertysource
    def Has2x2InterlacingProperty (a b c d : ℝ[X]) : Prop :=
  ∀ (s t : ℝ), 0 < s → 0 < t →
    StrictInterl ((C s * X + C t) * b + d) ((C s * X + C t) * a + c)

  • 2 × 2 interlacing condition, allowing zeros

    RealRooted.Has2x2InterlacingProperty0source
    def Has2x2InterlacingProperty0 (a b c d : ℝ[X]) : Prop :=
  ∀ (s t : ℝ), 0 < s → 0 < t →
    Interl ((C s * X + C t) * b + d) ((C s * X + C t) * a + c)

Theorems

  • Such matrices preserve interlacing sequences

    RealRooted.Challenges.MatrixInterlacing.preserves_interlacing_sequencessource
    theorem preserves_interlacing_sequences :
    ∀ {n : Nat} (_hn : 0 < n) (G : List (List ℝ[X]))
      (hG_rect : ∀ row ∈ G, row.length = n)
      (_hG_nonneg : ∀ row ∈ G, ∀ p ∈ row, HasNonnegCoeffs p)
      (_hG_affine : ∀ (i₁ i₂ : Fin G.length) (j₁ j₂ : Fin n),
        i₁ ≤ i₂ → j₁ ≤ j₂ →
        Has2x2InterlacingProperty
          ((G.get i₁).get ⟨j₁, by simp_all⟩)
          ((G.get i₁).get ⟨j₂, by simp_all⟩)
          ((G.get i₂).get ⟨j₁, by simp_all⟩)
          ((G.get i₂).get ⟨j₂, by simp_all⟩))
      (fs : List ℝ[X]) (_hfs_len : fs.length = n)
      (_hfs : IsInterlacingSeqNonneg fs),
        IsInterlacingSeqNonneg (matPolyAction G fs)

  • The same, allowing zero rows

    RealRooted.Challenges.MatrixInterlacing.preserves_interlacing_sequences_zeroAwaresource
    theorem preserves_interlacing_sequences_zeroAware :
    ∀ {n : Nat} (G : List (List ℝ[X]))
      (hG_rect : ∀ row ∈ G, row.length = n)
      (_hG_nonneg : ∀ row ∈ G, ∀ p ∈ row, HasNonnegCoeffs p)
      (_hG_affine : ∀ (i₁ i₂ : Fin G.length) (j₁ j₂ : Fin n),
        i₁ ≤ i₂ → j₁ ≤ j₂ →
        Has2x2InterlacingProperty0
          ((G.get i₁).get ⟨j₁, by simp_all⟩)
          ((G.get i₁).get ⟨j₂, by simp_all⟩)
          ((G.get i₂).get ⟨j₁, by simp_all⟩)
          ((G.get i₂).get ⟨j₂, by simp_all⟩))
      (fs : List ℝ[X]) (_hfs_len : fs.length = n)
      (_hfs : IsInterlacingSeqNonneg fs),
        IsInterlacingSeq0Nonneg (matPolyAction G fs)

Lean source RealRooted/Challenges/MatrixInterlacing.lean at revision 5827550b.