Parking functions

Parking functions and their variants (partial, weakly increasing, k-Naples, metered) and statistics on them: lucky cars, descents, displacement, and lucky statistics of Stirling permutations read as parking preferences.

DefinitionPartial parking function#✓fully proved

Let \(s, t \in \mathbb{N}\) and number the \(t\) spots \(0, \dots, t-1\). A map \(f : \{0, \dots, s-1\} \to \{0, \dots, t-1\}\), giving the preferred spot of each of \(s\) cars, is a partial parking function if for every spot \(k \in \{0, \dots, t-1\}\), at most \(t - k\) cars \(i\) satisfy \(f(i) \ge k\).

def IsPartialParkingFunction (s t : ℕ) (f : Fin s → Fin t) : Prop :=
  ∀ k : Fin t,
    (Finset.univ.filter (fun i => k ≤ f i)).card ≤ t - (k : ℕ)

Used by 29

DefinitionParking function#✓fully proved

Let \(n \in \mathbb{N}\) and number the \(n\) spots \(0, \dots, n-1\). A map \(f : \{0, \dots, n-1\} \to \{0, \dots, n-1\}\), giving the preferred spot of each of \(n\) cars, is a parking function if it is a partial parking function with \(n\) cars and \(n\) spots, that is, if for every spot \(k\), at most \(n - k\) cars \(i\) satisfy \(f(i) \ge k\).

def IsParkingFunction (n : ℕ) (f : Fin n → Fin n) : Prop :=
  IsPartialParkingFunction n n f

def IsPartialParkingFunction (s t : ℕ) (f : Fin s → Fin t) : Prop :=
  ∀ k : Fin t,
    (Finset.univ.filter (fun i => k ≤ f i)).card ≤ t - (k : ℕ)

MathlibExt/Combinatorics/Enumerative/ParkingFunction.lean:29

Uses 1 · Used by 34

Statement usesPartial parking function

TheoremLower-tail characterization of parking functions#✓fully proved

Let \(n \in \mathbb{N}\), number the \(n\) spots \(0, \dots, n-1\), and let \(f : \{0, \dots, n-1\} \to \{0, \dots, n-1\}\) give the preferred spot of each of \(n\) cars. Then \(f\) is a parking function if and only if, for every spot \(k \in \{0, \dots, n-1\}\), at least \(k + 1\) cars \(i\) satisfy \(f(i) \le k\).

theorem isParkingFunction_iff_card_filter_le (n : ℕ) (f : Fin n → Fin n) :
    IsParkingFunction n f ↔
      ∀ k : Fin n,
        k.val + 1 ≤ (Finset.univ.filter (fun i : Fin n ↦ f i ≤ k)).card

Uses 2 · Used by 1

Statement usesParking function

Proof usesPartial parking function

Used byTotal number of descents over parking functions

TheoremNumber of partial parking functions#✓fully proved

Let \(s\) and \(t\) be natural numbers with \(0 < s \le t\). A partial parking function with \(s\) cars and \(t\) spots is a map \(f : \{0, \dots, s - 1\} \to \{0, \dots, t - 1\}\) such that for every spot \(k \in \{0, \dots, t - 1\}\) at most \(t - k\) cars \(i\) have \(f(i) \ge k\). The number of partial parking functions with \(s\) cars and \(t\) spots is \((t + 1 - s)(t + 1)^{s - 1}\).

The proof is Pollak's circle argument.

theorem pollak_partial_parking_functions_card
    (s t : ℕ) (hs : 0 < s) (hst : s ≤ t) :
    Nat.card {f : Fin s → Fin t // IsPartialParkingFunction s t f} =
    (t + 1 - s) * (t + 1) ^ (s - 1)

def IsPartialParkingFunction (s t : ℕ) (f : Fin s → Fin t) : Prop :=
  ∀ k : Fin t,
    (Finset.univ.filter (fun i => k ≤ f i)).card ≤ t - (k : ℕ)

MathlibExt/Combinatorics/Enumerative/ParkingFunction.lean:29

Sources

Steve Butler, Kimberly Hadaway, Victoria Lenius, Preston Martens, and Marshall Moats, “Lucky Cars and Lucky Spots in Parking Functions”, Journal of Integer Sequences 29 (2026), Article 26.1.1, proposition at lines 330–332 of https://cs.uwaterloo.ca/journals/JIS/VOL29/Hadaway/had3.tex.

Uses 1

Statement usesPartial parking function

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.