Parking functions

A parking function of length $n$ is a word $w$ with letters in $\{0, \dotsc, n-1\}$ such that, for every $k \leq n$, at least $k$ of its letters are smaller than $k$. The following generating polynomials over parking functions of length $n$ are real-rooted:

Descents: $\sum_w x^{\operatorname{des}(w)}$. The proof passes through Pollak's cyclic action: $(n+1)$ times this polynomial equals the descent polynomial of all words of length $n$ over an alphabet of size $n+1$.
Tieless descents: the same count over parking functions with no two equal adjacent entries. $(n+1)$ times this polynomial equals a Brändén–Vecchi Chow polynomial of an elementary Toeplitz matrix.
Weak left peaks: $\sum_w x^{\operatorname{wlpk}(w)}$.

References

P. Diaconis and A. Hicks, “Probabilizing parking functions,” Adv. in Appl. Math. 89 (2017), 125–155. The Chow polynomials appear on the Brändén–Vecchi page.

Definitions

Parking functions

RealRooted.ParkingFunctions.IsParkingFunctionsource

def IsParkingFunction {n : ℕ} (w : Fin n → Fin n) : Prop :=
  ∀ k : ℕ, k ≤ n →
    k ≤ (Finset.univ.filter fun i => (w i).val < k).card

Descent polynomial of parking functions

RealRooted.ParkingFunctions.parkingDescentPolynomialsource

noncomputable def parkingDescentPolynomial : ℕ → ℝ[X]
  | 0 => 1
  | n + 1 => descentGeneratingPolynomial (R := ℝ) (parkingFunctions (n + 1))

Descent polynomial of tieless parking functions

RealRooted.ParkingFunctions.tielessParkingDescentPolynomialsource

def tielessParkingDescentPolynomial : ℕ → ℤ[X]
  | 0 => 1
  | n + 1 => descentGeneratingPolynomial (R := ℤ)
      (tielessParkingFunctions (n + 1))

Weak left peak polynomial of parking functions

RealRooted.ParkingFunctions.parkingWeakLeftPeakPolynomialIntsource

def parkingWeakLeftPeakPolynomialInt (n : ℕ) : ℤ[X] :=
  ∑ w ∈ parkingFunctions n, X ^ wordWeakLeftPeakNumber w

Theorems

Parking function descent polynomials are real-rootedMain result

RealRooted.ParkingFunctions.parkingDescentPolynomial_splitssource

theorem parkingDescentPolynomial_splits (n : ℕ) :
    (parkingDescentPolynomial n).Splits

Pollak's cyclic action: descents of parking functions and of words

RealRooted.ParkingFunctions.succ_nsmul_parkingDescentPolynomialInt_eq_literalWordDescentPolynomialIntsource

theorem succ_nsmul_parkingDescentPolynomialInt_eq_literalWordDescentPolynomialInt
    (n : ℕ) :
    (n + 1) • parkingDescentPolynomialInt n =
      literalWordDescentPolynomialInt (n + 1) n

Tieless parking function descent polynomials are real-rootedMain result

RealRooted.ParkingFunctions.map_tielessParkingDescentPolynomial_splitssource

theorem map_tielessParkingDescentPolynomial_splits (n : ℕ) :
    ((tielessParkingDescentPolynomial n).map
      (Int.castRingHom ℝ)).Splits

Tieless descents and a Brändén–Vecchi Chow polynomial

RealRooted.ParkingFunctions.succ_nsmul_tielessParkingDescentPolynomial_eq_chowPolynomialsource

theorem succ_nsmul_tielessParkingDescentPolynomial_eq_chowPolynomial
    (n : ℕ) :
    (n + 1) • tielessParkingDescentPolynomial n =
      BrandenVecchi.chowPolynomial
        (BrandenVecchi.finiteElementaryToeplitz
          (R := ℤ) (fun _ : Fin (n + 1) => 1)) n

Parking function weak left peak polynomials are real-rootedMain result

RealRooted.ParkingFunctions.map_parkingWeakLeftPeakPolynomialInt_splitssource

theorem map_parkingWeakLeftPeakPolynomialInt_splits (n : ℕ) :
    ((parkingWeakLeftPeakPolynomialInt n).map
      (Int.castRingHom ℝ)).Splits

Parking functions

References

≔ Definitions

⊢ Theorems

Definitions

Theorems