Refined Eulerian polynomials

TheoremMarginals of the refined Eulerian polynomial#✓fully proved

Let \(n \ge 1\). For a permutation \(\sigma\) of \(\{1, \dots, n\}\), let \(\mathrm{odes}(\sigma)\) (resp. \(\mathrm{edes}(\sigma)\)) be the number of odd (resp. even) positions \(i \in \{1, \dots, n-1\}\) with \(\sigma(i) > \sigma(i+1)\), and let \(A_n(p, q) = \sum_{\sigma} p^{\mathrm{odes}(\sigma)} q^{\mathrm{edes}(\sigma)}\), the sum over all permutations \(\sigma\) of \(\{1, \dots, n\}\). Then for all real numbers \(p\) and \(q\),

\[A_n(p, 1) = \frac{n!}{2^{\lfloor n/2 \rfloor}} (1+p)^{\lfloor n/2 \rfloor}\]

and

\[A_n(1, q) = \frac{n!}{2^{\lfloor (n-1)/2 \rfloor}} (1+q)^{\lfloor (n-1)/2 \rfloor}.\]
MetaMathlibExt.sun_refined_eulerian_marginals · 15 lines 
theorem sun_refined_eulerian_marginals (n : ℕ) (hn : 0 < n) (p q : ℝ) :
    let odes : Equiv.Perm (Fin n) → ℕ := fun σ =>
      (Finset.univ.filter (fun i : Fin (n - 1) =>
        Odd (i.val + 1) ∧
        (σ ⟨i.val, by have := i.isLt; omega⟩).val >
          (σ ⟨i.val + 1, by have := i.isLt; omega⟩).val)).card;
    let edes : Equiv.Perm (Fin n) → ℕ := fun σ =>
      (Finset.univ.filter (fun i : Fin (n - 1) =>
        Even (i.val + 1) ∧
        (σ ⟨i.val, by have := i.isLt; omega⟩).val >
          (σ ⟨i.val + 1, by have := i.isLt; omega⟩).val)).card;
    let genA : ℝ → ℝ → ℝ := fun p q =>
      ∑ σ : Equiv.Perm (Fin n), p ^ odes σ * q ^ edes σ;
    genA p 1 = (Nat.factorial n : ℝ) / 2 ^ (n / 2) * (1 + p) ^ (n / 2) ∧
      genA 1 q = (Nat.factorial n : ℝ) / 2 ^ ((n - 1) / 2) * (1 + q) ^ ((n - 1) / 2)
Sources

TheoremPalindromicity of the refined Eulerian polynomials#✓fully proved

Let \(n \ge 1\). For a permutation \(\sigma\) of \(\{1, \dots, n\}\), let \(\mathrm{odes}(\sigma)\) (resp. \(\mathrm{edes}(\sigma)\)) be the number of odd (resp. even) positions \(i \in \{1, \dots, n-1\}\) with \(\sigma(i) > \sigma(i+1)\), and let \(A_n(p, q) = \sum_{\sigma} p^{\mathrm{odes}(\sigma)} q^{\mathrm{edes}(\sigma)}\), the sum over all permutations \(\sigma\) of \(\{1, \dots, n\}\), be the refined Eulerian polynomial with real coefficients. Let \(P_n = (1+q) A_n\) if \(n\) is even and \(P_n = A_n\) if \(n\) is odd. Then \(P_n\) is palindromic of darga \(\lfloor n/2 \rfloor\): it is a nonzero polynomial, \(P_n(p, q) = P_n(q, p)\) for all real \(p\) and \(q\), and \(P_n(p, q) = (pq)^{\lfloor n/2 \rfloor} P_n(1/p, 1/q)\) for all nonzero real \(p\) and \(q\).

MetaMathlibExt.refinedEulerianPolynomial_palindromic · 28 lines 
theorem refinedEulerianPolynomial_palindromic
    (n : ℕ) (hn : 1 ≤ n) :
    let oddDescentCount : Equiv.Perm (Fin n) → ℕ := fun σ =>
      (Finset.univ.filter fun i : Fin n =>
        if h : i.val + 1 < n then
          (i.val + 1) % 2 = 1 ∧ σ i > σ ⟨i.val + 1, h⟩
        else False).card
    let evenDescentCount : Equiv.Perm (Fin n) → ℕ := fun σ =>
      (Finset.univ.filter fun i : Fin n =>
        if h : i.val + 1 < n then
          (i.val + 1) % 2 = 0 ∧ σ i > σ ⟨i.val + 1, h⟩
        else False).card
    let refinedEulerian : Polynomial (Polynomial ℝ) :=
      ∑ σ : Equiv.Perm (Fin n),
        Polynomial.C (Polynomial.X ^ evenDescentCount σ) *
          Polynomial.X ^ oddDescentCount σ
    let palindromicRefinement : Polynomial (Polynomial ℝ) :=
      if n % 2 = 0 then Polynomial.C (1 + Polynomial.X) * refinedEulerian
      else refinedEulerian
    palindromicRefinement ≠ 0 ∧
      (∀ p q : ℝ,
        Polynomial.eval q (Polynomial.eval (Polynomial.C p) palindromicRefinement) =
          Polynomial.eval p (Polynomial.eval (Polynomial.C q) palindromicRefinement)) ∧
      ∀ p q : ℝ, p ≠ 0 → q ≠ 0 →
        Polynomial.eval q (Polynomial.eval (Polynomial.C p) palindromicRefinement) =
          (p * q) ^ (n / 2) *
            Polynomial.eval q⁻¹
              (Polynomial.eval (Polynomial.C p⁻¹) palindromicRefinement)
Sources
  • Hua Sun, "A New Class of Refined Eulerian Polynomials," Journal of Integer Sequences 21 (2018), Article 18.5.5, Theorem, lines 160–162 (polynomial definition lines 135–136, palindromic-darga definition lines 105–110). https://cs.uwaterloo.ca/journals/JIS/VOL21/Sun/sun2.tex
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.