Families
Eulerian polynomials
Let $A_n(t) = \sum_{\sigma \in \mathfrak{S}_n} t^{\operatorname{des}(\sigma)}$ be the Eulerian polynomial. The library uses the shifted version eulerianTilde n $= t A_{n+1}(t)$, which satisfies $P_0 = t$ and $P_{n+1} = t\bigl((n+2) P_n + (1-t) P_n'\bigr)$. The type $B$ Eulerian polynomials satisfy $B_0 = 1$ and $B_{n+1} = \bigl(1 + (2n+1)t\bigr) B_n + 2t(1-t) B_n'$.
Both families are real-rooted, and consecutive polynomials interlace.
References
The ordinary Eulerian recurrence and its real-rootedness go back to F. G. Frobenius, “Über die Bernoullischen Zahlen und die Eulerschen Polynome,” Sitzungsberichte der Königlich Preussischen Akademie der Wissenschaften (1910), 809–847. For type $B$, see F. Brenti, “q-Eulerian polynomials arising from Coxeter groups,” European Journal of Combinatorics 15 (1994), 417–441. See also the Eulerian polynomials on symmetricfunctions.com.
≔ Definitions
Eulerian polynomials
def eulerianTilde : Nat → ℝ[X]
| 0 => X
| n + 1 =>
X * (C (n + 2 : ℝ) * eulerianTilde n +
(1 - X) * (eulerianTilde n).derivative)
Type B Eulerian polynomials
def typeBEulerian : Nat → ℝ[X]
| 0 => 1
| n + 1 =>
typeBEulerianCoeffA n * typeBEulerian n +
typeBEulerianCoeffB * (typeBEulerian n).derivative
⊢ Theorems
Eulerian polynomials are real-rootedMain result
theorem realRooted :
∀ n : Nat, eulerianTilde n ≠ 0 ∧ (eulerianTilde n).Splits
Consecutive Eulerian polynomials interlace
theorem interlaces_succ :
∀ n : Nat, Interlaces (eulerianTilde n) (eulerianTilde (n + 1))
Type B Eulerian polynomials are real-rootedMain result
theorem typeB_realRooted :
∀ n : Nat, typeBEulerian n ≠ 0 ∧ (typeBEulerian n).Splits
Consecutive type B Eulerian polynomials interlace
theorem typeB_interlaces_succ :
∀ n : Nat, Interlaces (typeBEulerian n) (typeBEulerian (n + 1))
Lean source RealRooted/Challenges/Eulerian.lean at revision 5827550b.