Theorems

Operators preserving interlacing

A real-linear operator that preserves real-rootedness up to zero also preserves interlacing, up to reversing the orientation.

References

P. Brändén, “Iterated sequences and the geometry of zeros,” Journal für die reine und angewandte Mathematik 658 (2011), 115–131. See also the operator-preserver overview on symmetricfunctions.com.

Definitions

  • Real-rootedness preserver

    RealRooted.PreservesRealRootedOrZerosource
    def PreservesRealRootedOrZero (T : ℝ[X] →ₗ[ℝ] ℝ[X]) : Prop :=
  ∀ p : ℝ[X], (p ≠ 0 ∧ p.Splits) → T p = 0 ∨ (T p).Splits

  • Interlacing preserver, up to orientation

    RealRooted.PreservesInterlacingPairsUpToOrder0source
    def PreservesInterlacingPairsUpToOrder0 (T : ℝ[X] →ₗ[ℝ] ℝ[X]) : Prop :=
  ∀ ⦃f g : ℝ[X]⦄, StrictInterl f g → Interl (T f) (T g) ∨ Interl (T g) (T f)

Theorems

  • Real-rootedness preservers preserve interlacing

    RealRooted.Challenges.OperatorPreservers.realRootedPreserver_preservesInterlacingsource
    theorem realRootedPreserver_preservesInterlacing :
    ∀ T : ℝ[X] →ₗ[ℝ] ℝ[X],
      PreservesRealRootedOrZero T →
      PreservesInterlacingPairsUpToOrder0 T

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