Lucky cars in parking functions

TheoremExpected number of lucky cars in weakly increasing parking functions#✓fully proved

Let \(n \ge 1\). Number cars and spots from \(0\), and encode a weakly increasing parking function of length \(n\) as a nondecreasing map \(a : \{0, \dots, n-1\} \to \{0, \dots, n-1\}\) with \(a(i) \le i\) for every \(i\). The average, over all such maps \(a\), of the number of indices \(i\) with \(a(i) = i\) equals \(\frac{3n}{n+2}\). Here car \(i\) parks in spot \(i\) and is lucky exactly when \(a(i) = i\), so this number counts both the lucky cars and the lucky spots.

theorem expected_lucky_spots_weakly_increasing_parking_functions
    (n : ℕ) (hn : 0 < n) :
    let parkingFunctions := Finset.univ.filter fun a : Fin n → Fin n =>
      Monotone a ∧ ∀ i, (a i).val ≤ i.val
    (∑ a ∈ parkingFunctions,
        ((Finset.univ.filter fun i : Fin n => a i = i).card : ℚ)) /
      (parkingFunctions.card : ℚ) = ((3 : ℚ) * n) / (n + 2)

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, Corollary, lines 631–633 (supporting lemma lines 619–629), https://cs.uwaterloo.ca/journals/JIS/VOL29/Hadaway/had3.tex The corollary attributes the Dyck-path expectation value to Deutsch.

DefinitionNext free spot#✓fully proved

Number the \(n\) spots \(0, \dots, n-1\). Given a set \(S\) of occupied spots and a spot \(a\), the next free spot is the least spot \(s \ge a\) with \(s \notin S\); when every spot \(s \ge a\) is occupied, it is \(a\) itself.

def nextFreeSpot {n : ℕ} (occ : Finset (Fin n)) (a : Fin n) : Fin n :=
  if h : (Finset.univ.filter (fun s : Fin n => a ≤ s ∧ s ∉ occ)).Nonempty then
    (Finset.univ.filter (fun s : Fin n => a ≤ s ∧ s ∉ occ)).min' h
  else a

Used by 1

Used byGreedy parking from an occupied set

DefinitionGreedy parking from an occupied set#✓fully proved

Number the \(n\) spots \(0, \dots, n-1\). Given a list \(a_1, \dots, a_m\) of preferred spots and a set \(S\) of occupied spots, cars \(1, \dots, m\) arrive in order and car \(k\) takes the least spot at or after \(a_k\) that is neither in \(S\) nor taken by cars \(1, \dots, k-1\) (or \(a_k\) itself if there is none). The result is the list of spots taken, in arrival order.

def parkSpotsFrom {n : ℕ} : List (Fin n) → Finset (Fin n) → List (Fin n)
  | [], _ => []
  | a :: rest, occ =>
      nextFreeSpot occ a ::
        parkSpotsFrom rest (insert (nextFreeSpot occ a) occ)

Uses 1 · Used by 1

Statement usesNext free spot

Used byGreedy parking outcome

DefinitionGreedy parking outcome#✓fully proved

Let \(f : \{0, \dots, n-1\} \to \{0, \dots, n-1\}\) give the preferred spot of each of \(n\) cars. Starting from an empty lot with spots \(0, \dots, n-1\), cars \(0, 1, \dots, n-1\) arrive in order, and each takes the least free spot at or after its preference (or its preference itself if there is none). The outcome sends each car \(i\) to the spot it takes.

def parkSpots {n : ℕ} (f : Fin n → Fin n) : Fin n → Fin n :=
  fun i => (parkSpotsFrom (List.ofFn f) ∅).getD i.val i

Uses 1 · Used by 3

Statement usesGreedy parking from an occupied set

Used byParking spot of a car · Lucky car under greedy parking · Number of lucky cars

DefinitionLucky car under greedy parking#✓fully proved

Let \(f : \{0, \dots, n-1\} \to \{0, \dots, n-1\}\) give the preferred spot of each of \(n\) cars. Cars \(0, 1, \dots, n-1\) arrive in order, and each takes the least spot at or after its preference not taken by an earlier car, or its preferred spot itself when there is no such spot. Car \(i\) is lucky if the spot it takes is its preferred spot \(f(i)\).

For a parking function a free spot always exists.

def IsLuckyCar {n : ℕ} (f : Fin n → Fin n) (i : Fin n) : Prop :=
  parkSpots f i = f i

Uses 1 · Used by 4

Statement usesGreedy parking outcome

Used byParking functions with prescribed lucky and unlucky cars · Lucky-car counts · Decreasing lucky-car counts · Increasing lucky-car counts

DefinitionNumber of lucky cars#✓fully proved

Let \(f : \{0, \dots, n-1\} \to \{0, \dots, n-1\}\) give the preferred spot of each of \(n\) cars, and let cars \(0, 1, \dots, n-1\) arrive in order, each taking the least spot at or after its preference not taken by an earlier car, or its preferred spot itself when there is no such spot. The number of lucky cars of \(f\) is the number of cars \(i\) whose spot is \(f(i)\).

def luckyCount {n : ℕ} (f : Fin n → Fin n) : ℕ :=
  (Finset.univ.filter (fun i => decide (parkSpots f i = f i))).card

Uses 1 · Used by 3

Statement usesGreedy parking outcome

Used byFactorial moments of the number of lucky cars · Expected number of lucky cars in weakly decreasing parking functions · Generating polynomial of lucky cars

DefinitionLucky-car counts#✓fully proved

Number the cars and spots \(0, \dots, n-1\). For \(i, j \in \{0, \dots, n-1\}\), \(q_n(i, j)\) is the number of parking functions \(f : \{0, \dots, n-1\} \to \{0, \dots, n-1\}\) with \(f(i) = j\) in which car \(i\) is lucky, that is, parks in spot \(f(i)\).

In the one-based indexing of Butler et al. this is \(q_n(i+1, j+1)\).

noncomputable def q (n : ℕ) (i j : Fin n) : ℕ :=
  Nat.card { f : Fin n → Fin n //
    IsParkingFunction n f ∧ f i = j ∧ IsLuckyCar f i }

Uses 2 · Used by 3

Statement usesLucky car under greedy parking · Parking function

Used byBoundary values of lucky-car counts (Lemma 9) · Number of parking functions in which a given car is lucky · Number of parking functions in which the second spot is lucky

DefinitionIncreasing lucky-car counts#✓fully proved

Number the cars and spots \(0, \dots, n-1\). For \(i, j \in \{0, \dots, n-1\}\), \(q^{\mathrm{inc}}_n(i, j)\) is the number of weakly increasing parking functions \(f : \{0, \dots, n-1\} \to \{0, \dots, n-1\}\) with \(f(i) = j\) in which car \(i\) is lucky, that is, parks in spot \(f(i)\).

In the one-based indexing of Butler et al. this is \(q^i_n(i+1, j+1)\).

noncomputable def qInc (n : ℕ) (i j : Fin n) : ℕ :=
  Nat.card { f : Fin n → Fin n //
    IsParkingFunction n f ∧ Monotone f ∧ f i = j ∧
      IsLuckyCar f i }

Uses 2 · Used by 1

Statement usesLucky car under greedy parking · Parking function

Used byIncreasing lucky-car counts (Lemma 18)

DefinitionDecreasing lucky-car counts#✓fully proved

Number the cars and spots \(0, \dots, n-1\). For \(i, j \in \{0, \dots, n-1\}\), \(q^{\mathrm{dec}}_n(i, j)\) is the number of weakly decreasing parking functions \(f : \{0, \dots, n-1\} \to \{0, \dots, n-1\}\) with \(f(i) = j\) in which car \(i\) is lucky, that is, parks in spot \(f(i)\).

In the one-based indexing of Butler et al. this is \(q^d_n(i+1, j+1)\).

noncomputable def qDec (n : ℕ) (i j : Fin n) : ℕ :=
  Nat.card { f : Fin n → Fin n //
    IsParkingFunction n f ∧ Antitone f ∧ f i = j ∧
      IsLuckyCar f i }

Uses 2 · Used by 3

Statement usesLucky car under greedy parking · Parking function

Used byLucky spots of weakly decreasing parking functions as a sum · Lucky spots of weakly decreasing parking functions as a Catalan convolution · Decreasing lucky-car counts (Lemma 22)

DefinitionLucky-car polynomial#✓fully proved

For \(n \in \mathbb{N}\), \(f_n \in \mathbb{Q}[x]\) is the polynomial

\[f_n(x) = \frac{1}{n+1} \prod_{i=0}^{n-1} \bigl((n+1-i)\,x + i\bigr).\]

Equivalently, \(f_n(x) = \frac{1}{n+1} \prod_{i=1}^{n} \bigl((n+2-i)\,x + (i-1)\bigr)\).

noncomputable def luckyGenPoly (n : ℕ) : Polynomial ℚ :=
  C (1 / (n + 1 : ℚ)) *
    ∏ i : Fin n, (C ((n + 1 - i.val : ℕ) : ℚ) * X + C (i.val : ℚ))

Used by 2

Used byFactorial moments of the number of lucky cars · Generating polynomial of lucky cars

TheoremParking functions with prescribed lucky and unlucky cars#●ready to prove

Number the cars and spots \(0, \dots, n-1\), and let \(L\) and \(U\) be disjoint sets of cars. The number of parking functions of length \(n\) in which every car in \(L\) is lucky and no car in \(U\) is lucky equals

\[\prod_{i \in L} (n + 1 - i) \cdot \prod_{i \in U} i \cdot (n + 1)^{n - |L| - |U| - 1},\]

where the power is taken in \(\mathbb{Q}\), so the exponent may be negative.

In the paper's numbering of cars from \(1\), the factors are \(n + 2 - i\) and \(i - 1\).

theorem_wanted card_parking_lucky_on (n : ℕ) (L U : Finset (Fin n))
    (hLU : Disjoint L U) :
    (Nat.card { f : Fin n → Fin n // IsParkingFunction n f ∧
        (∀ i ∈ L, IsLuckyCar f i) ∧
          (∀ i ∈ U, ¬ IsLuckyCar f i) } : ℚ) =
      (∏ i ∈ L, ((n + 1 - i.val : ℕ) : ℚ)) *
        (∏ i ∈ U, (i.val : ℚ)) *
        ((n + 1 : ℚ)) ^ ((n : ℤ) - L.card - U.card - 1)

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Theorem 4.

Uses 2

Statement usesLucky car under greedy parking · Parking function

TheoremGenerating polynomial of lucky cars#●ready to prove

For \(n \in \mathbb{N}\) and \(0 \le k \le n\), let \(c_k\) be the number of parking functions of length \(n\) with exactly \(k\) lucky cars. Then in \(\mathbb{Q}[x]\),

\[\frac{1}{n+1} \prod_{i=0}^{n-1} \bigl((n+1-i)x + i\bigr) = \sum_{k=0}^{n} c_k x^k.\]

theorem_wanted luckyGenPoly_eq_sum (n : ℕ) :
    luckyGenPoly n =
      ∑ k ∈ Finset.range (n + 1),
        C ((Nat.card { f : Fin n → Fin n //
          IsParkingFunction n f ∧ luckyCount f = k } : ℕ) : ℚ) *
          X ^ k

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Corollary 5.

Uses 3

Statement usesNumber of lucky cars · Lucky-car polynomial · Parking function

TheoremFactorial moments of the number of lucky cars#●ready to prove

Let \(n \ge 1\) and \(\ell \in \mathbb{N}\), let \(X(f)\) be the number of lucky cars of a parking function \(f\) of length \(n\), and let \(P_n(x) = \frac{1}{n+1} \prod_{i=0}^{n-1} \bigl((n+1-i)x + i\bigr) \in \mathbb{Q}[x]\). Then

\[\frac{1}{(n+1)^{n-1}} \sum_f X(f)\bigl(X(f)-1\bigr)\cdots\bigl(X(f)-\ell+1\bigr) = \frac{P_n^{(\ell)}(1)}{(n+1)^{n-1}},\]

where \(f\) runs over the parking functions of length \(n\) and \(P_n^{(\ell)}\) is the \(\ell\)-th derivative of \(P_n\). Since there are \((n+1)^{n-1}\) parking functions of length \(n\), the left side is the \(\ell\)-th falling-factorial moment of \(X\) for a uniformly random parking function.

theorem_wanted expected_descFactorial_luckyCount (n ℓ : ℕ)
    (hn : 1 ≤ n) :
    ((∑ f ∈ Finset.univ.filter (fun f : Fin n → Fin n =>
        IsParkingFunction n f),
      ((luckyCount f).descFactorial ℓ : ℚ)) /
        (n + 1 : ℚ) ^ (n - 1) =
      (Polynomial.derivative^[ℓ] (luckyGenPoly n)).eval 1 /
        (n + 1 : ℚ) ^ (n - 1))

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Proposition 6.

Uses 4

Statement usesNumber of lucky cars · Lucky-car polynomial · Parking function · Partial parking function

TheoremBoundary values of lucky-car counts (Lemma 9)#●ready to prove

Let \(n \ge 1\), number the cars and spots \(0, \dots, n-1\), and let \(q_n(i, j)\) be the number of parking functions of length \(n\) in which car \(i\) prefers spot \(j\) and is lucky. Then for all \(i, j \in \{0, \dots, n-1\}\), with powers taken in \(\mathbb{Q}\) (the integer exponents may be negative),

\[q_n(n-1, j) = \binom{n-1}{j} (j+1)^{j-1} (n-j)^{n-j-2},\]

\[q_n(0, j) = \sum_{k=j+1}^{n} \binom{n-1}{k-1} k^{k-2} (n-k+1)^{n-k-1},\]

\[q_n(i, n-1) = n^{n-2},\]

\[q_n(i, 0) = (n+1)^{n-i-2}\, n^{i-1}\, (2n-i).\]

In the one-based indexing of the source, car \(i\) and spot \(j\) here are car \(i+1\) and spot \(j+1\).

theorem_wanted q_boundary_values (n : ℕ) (hn : 1 ≤ n)
    (i j : Fin n) :
    (q n ⟨n - 1, by omega⟩ j : ℚ) =
        Nat.choose (n - 1) j.val * ((j.val + 1 : ℚ)) ^ ((j.val : ℤ) - 1) *
          ((n - j.val : ℚ)) ^ ((n : ℤ) - j.val - 2) ∧
      (q n ⟨0, hn⟩ j : ℚ) =
        ∑ k ∈ Finset.Icc (j.val + 1) n,
          Nat.choose (n - 1) (k - 1) * ((k : ℚ)) ^ ((k : ℤ) - 2) *
            ((n - k + 1 : ℚ)) ^ ((n : ℤ) - k - 1) ∧
      (q n i ⟨n - 1, by omega⟩ : ℚ) = ((n : ℚ)) ^ ((n : ℤ) - 2) ∧
      (q n i ⟨0, hn⟩ : ℚ) =
        ((n + 1 : ℚ)) ^ ((n : ℤ) - i.val - 2) *
          ((n : ℚ)) ^ ((i.val : ℤ) - 1) * (2 * n - i.val)

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Lemma 9.

Uses 1

Statement usesLucky-car counts

TheoremNumber of parking functions in which a given car is lucky#●ready to prove

Number cars and spots \(0, \dots, n-1\), and let \(q_n(i, j)\) be the number of parking functions of length \(n\) in which car \(i\) prefers spot \(j\) and parks there. Then for every \(n\) and every car \(i < n\),

\[\sum_{j=0}^{n-1} q_n(i, j) = (n + 1 - i)(n + 1)^{n-2},\]

an identity in \(\mathbb{Q}\) (for \(n = 1\) the exponent is \(-1\)). The left side is the number of parking functions of length \(n\) in which car \(i\) is lucky; in the paper's one-based numbering the count for the \(i\)-th car is \((n + 2 - i)(n + 1)^{n-2}\).

theorem_wanted sum_q_eq (n : ℕ) (i : Fin n) :
    (∑ j : Fin n, (q n i j : ℚ)) =
      (n + 1 - i.val : ℚ) * ((n + 1 : ℚ)) ^ ((n : ℤ) - 2)

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Corollary 10.

Uses 1

Statement usesLucky-car counts

TheoremNumber of parking functions in which the second spot is lucky#●ready to prove

Number cars and spots \(0, \dots, n-1\), and let \(q_n(i, j)\) be the number of parking functions of length \(n\) in which car \(i\) prefers spot \(j\) and parks there. Then for every \(n \ge 2\), in \(\mathbb{Q}\),

\[\sum_{i=0}^{n-1} q_n(i, 1) = \frac{3}{4}(n + 1)^{n-1} - \frac{1}{4}(n - 1)^{n-1}.\]

Since at most one car parks in spot \(1\), the left side is the number of parking functions of length \(n\) in which the second spot is lucky, that is, the car parking there preferred it.

theorem_wanted sum_q_second_spot (n : ℕ) (hn : 2 ≤ n) :
    (∑ i : Fin n, (q n i ⟨1, hn⟩ : ℚ)) =
      3 / 4 * ((n + 1 : ℚ)) ^ (n - 1) -
        1 / 4 * ((n : ℚ) - 1) ^ (n - 1)

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Theorem 12.

Uses 1

Statement usesLucky-car counts

TheoremIncreasing lucky-car counts (Lemma 18)#●ready to prove

Number the cars and spots \(0, \dots, n-1\), let \(q^{\mathrm{inc}}_n(i, j)\) be the number of weakly increasing parking functions of length \(n\) in which car \(i\) prefers spot \(j\) and is lucky, and let \(C_m\) be the \(m\)-th Catalan number. For all \(i, j \in \{0, \dots, n-1\}\), \(q^{\mathrm{inc}}_n(i, j) = C_i \, C_{n-i}\) if \(i = j\), and \(q^{\mathrm{inc}}_n(i, j) = 0\) otherwise.

In the one-based indexing of the source the diagonal value reads \(C_{i-1} C_{n-i+1}\).

theorem_wanted qInc_eq (n : ℕ) (i j : Fin n) :
    qInc n i j =
      if i = j then catalan i.val * catalan (n - i.val)
      else 0

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Lemma 18.

Uses 1

Statement usesIncreasing lucky-car counts

DefinitionBallot paths#✓fully proved

For \(k, \ell \in \mathbb{N}\), a ballot path to \((k, \ell)\) is a word of length \(k + \ell\) in up steps and right steps with exactly \(\ell\) up steps such that every prefix has at least as many up steps as right steps; equivalently, a lattice path from \((0,0)\) to \((k, \ell)\) with unit up and right steps that stays on or above the line \(y = x\).

def BallotPath (k ℓ : ℕ) : Type :=
  { w : List Bool // w.length = k + ℓ ∧ w.count true = ℓ ∧
    ∀ m : ℕ, m ≤ w.length →
      (w.take m).count false ≤ (w.take m).count true }

Used by 1

Used byNumber of ballot paths

TheoremNumber of ballot paths#●ready to prove

For natural numbers \(k \le \ell\), the number of lattice paths from \((0,0)\) to \((k, \ell)\) with unit up and right steps that stay on or above the line \(y = x\) is \(\frac{\ell - k + 1}{\ell + 1} \binom{k + \ell}{k}\).

theorem_wanted card_ballotPath (k ℓ : ℕ) (h : k ≤ ℓ) :
    (Nat.card (BallotPath k ℓ) : ℚ) =
      ((ℓ - k + 1 : ℚ) / (ℓ + 1)) * Nat.choose (k + ℓ) k

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Lemma 21.

Uses 1

Statement usesBallot paths

TheoremDecreasing lucky-car counts (Lemma 22)#●ready to prove

Number the cars and spots \(0, \dots, n-1\), and let \(q^{\mathrm{dec}}_n(i, j)\) be the number of weakly decreasing parking functions of length \(n\) in which car \(i\) prefers spot \(j\) and is lucky. For all \(i, j \in \{0, \dots, n-1\}\), if \(i + j < n\) then

\[q^{\mathrm{dec}}_n(i, j) = \frac{(n-i-j)^2}{(n-i)(n-j)} \binom{n-i+j-1}{j} \binom{n-j+i-1}{i},\]

and \(q^{\mathrm{dec}}_n(i, j) = 0\) otherwise.

In the one-based indexing of the source the condition reads \(i + j \le n + 1\).

theorem_wanted qDec_eq (n : ℕ) (i j : Fin n) :
    (qDec n i j : ℚ) =
      if i.val + j.val < n then
        ((n - i.val - j.val : ℚ)) ^ 2 /
            ((n - i.val) * (n - j.val)) *
          Nat.choose (n - i.val + j.val - 1) j.val *
          Nat.choose (n - j.val + i.val - 1) i.val
      else 0

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Lemma 22.

Uses 1

Statement usesDecreasing lucky-car counts

TheoremLucky spots of weakly decreasing parking functions as a sum#●ready to prove

Number the cars and spots \(0, \dots, n-1\). For cars \(i\) and spots \(j\), let \(q^d_n(i, j)\) be the number of weakly decreasing parking functions \(f\) of length \(n\) (that is, \(f(0) \ge f(1) \ge \dots \ge f(n-1)\)) with \(f(i) = j\) in which car \(i\) is lucky. Then for every spot \(j\),

\[\sum_{i=0}^{n-1} q^d_n(i, j) = \sum_{i=1}^{n-j} \frac{(n-i-j+1)^2}{(n+1-i)(n-j)} \binom{n-i+j}{j} \binom{n-j+i-2}{i-1}.\]

The left side counts the weakly decreasing parking functions in which spot \(j\) is lucky, that is, taken by a car that prefers it.

theorem_wanted card_dec_lucky_spot_eq_sum (n : ℕ) (j : Fin n) :
    (∑ i : Fin n, (qDec n i j : ℚ)) =
      ∑ i ∈ Finset.Icc 1 (n - j.val),
        ((n : ℚ) - i - j.val + 1) ^ 2 /
            ((n + 1 - i) * (n - j.val)) *
          Nat.choose (n - i + j.val) j.val *
          Nat.choose (n - j.val + i - 2) (i - 1)

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Corollary 23.

Uses 1

Statement usesDecreasing lucky-car counts

TheoremLucky spots of weakly decreasing parking functions as a Catalan convolution#●ready to prove

Number the cars and spots \(0, \dots, n-1\). For cars \(i\) and spots \(j\), let \(q^d_n(i, j)\) be the number of weakly decreasing parking functions \(f\) of length \(n\) (that is, \(f(0) \ge f(1) \ge \dots \ge f(n-1)\)) with \(f(i) = j\) in which car \(i\) is lucky. Then for every spot \(j\),

\[\sum_{i=0}^{n-1} q^d_n(i, j) = \sum_{k=0}^{n-j-1} C_{n-1-k} \, C_k,\]

where \(C_m\) is the \(m\)-th Catalan number.

The left side counts the weakly decreasing parking functions in which spot \(j\) is lucky, that is, taken by a car that prefers it.

theorem_wanted card_dec_lucky_spot_eq_sum_catalan (n : ℕ)
    (j : Fin n) :
    (∑ i : Fin n, (qDec n i j : ℚ)) =
      ∑ k ∈ Finset.range (n - j.val),
        ((catalan (n - 1 - k) * catalan k : ℕ) : ℚ)

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Theorem 24.

Uses 1

Statement usesDecreasing lucky-car counts

TheoremExpected number of lucky cars in weakly decreasing parking functions#●ready to prove

For \(n \ge 1\), the sum of the numbers of lucky cars over all weakly decreasing parking functions \(f\) of length \(n\) (those with \(f(0) \ge f(1) \ge \dots \ge f(n-1)\)), divided by the Catalan number \(C_n\), equals \(\frac{n+1}{2}\).

There are \(C_n\) weakly decreasing parking functions of length \(n\), so this is the expected number of lucky cars, which equals the expected number of lucky spots.

theorem_wanted expected_lucky_dec (n : ℕ) (hn : 1 ≤ n) :
    ((∑ f ∈ Finset.univ.filter (fun f : Fin n → Fin n =>
        IsParkingFunction n f ∧ Antitone f),
      (luckyCount f : ℚ)) / (catalan n : ℚ)) =
      ((n : ℚ) + 1) / 2

Sources

• Steve Butler et al., "Lucky Cars and Lucky Spots in Parking Functions", Theorem 25.

Uses 3

Statement usesNumber of lucky cars · Parking function · Partial parking function

11 fully proved12 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.