k-Naples parking functions

DefinitionThe \(k\)-Naples rule#✓fully proved

On the spots \(1, \dots, n\), when the spots in a list \(O\) of natural numbers are occupied, a car preferring \(a\) parks in \(a\) if \(a\) is free; otherwise in the first free spot among those of \(a - 1, \dots, a - k\) that are at least \(1\), checked in decreasing order; otherwise in the first free spot among \(a + 1, \dots, n\), checked in increasing order. The car cannot park if none of these is free, or if \(a\) is not one of the spots \(1, \dots, n\).

public def naplesSpot (n k : ℕ) (occ : List ℕ) (a : ℕ) : Option ℕ :=
  if ¬ (1 ≤ a ∧ a ≤ n) then none else
  if a ∉ occ then some a else
    match ((List.range k).map fun j => a - (j + 1)).find? (fun s => decide (1 ≤ s ∧ s ∉ occ)) with
    | some s => some s
    | none => (List.range' (a + 1) (n - a)).find? (fun s => decide (s ∉ occ))

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 1.

Used by 1

Used byNaples parking

DefinitionNaples parking#✓fully proved

Starting from a list of occupied spots, cars with preferences \(a_1, \dots, a_m \in \mathbb{N}\) arrive in order, and each takes the spot given by the \(k\)-Naples rule on the spots \(1, \dots, n\) for the spots occupied when it arrives. If every car parks, the result is the final list of occupied spots: the spots of the cars, most recent first, followed by the initially occupied spots. If some car cannot park, there is no result.

public def naplesPark (n k : ℕ) : List ℕ → List ℕ → Option (List ℕ)
  | occ, [] => some occ
  | occ, a :: as => (naplesSpot n k occ a).bind fun s => naplesPark n k (s :: occ) as

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 1.

Uses 1 · Used by 8

Statement usesThe \(k\)-Naples rule

Used byNumber of ascending \(k\)-Naples parking functions · Number of ascending \(k\)-Naples parking functions starting with \(1\) · Number of descending \(k\)-Naples parking functions · Number of descending strictly \(k\)-Naples parking functions · \(k\)-Naples parking function · A \(2\)-Naples parking function that is not \(1\)-Naples · Remaining cars still park after moving a car to an earlier spot · A \(2\)-Naples parking example

Definition\(k\)-Naples parking function#✓fully proved

A preference \(\alpha = (a_1, \dots, a_n)\) of length \(n\) is a \(k\)-Naples parking function if \(1 \le a_i \le n\) for every \(i\) and all \(n\) cars park on the spots \(1, \dots, n\) when they arrive in order and follow the \(k\)-Naples rule: car \(i\) takes spot \(a_i\) if it is free; otherwise the first free spot among \(a_i - 1, \dots, a_i - k\), checked in decreasing order and only among spots at least \(1\); otherwise the first free spot after \(a_i\), if there is one. For \(k = 0\) these are the ordinary parking functions.

public def IsNaplesParkingFunction (k : ℕ) {n : ℕ} (α : Fin n → ℕ) : Prop :=
  (∀ i, 1 ≤ α i ∧ α i ≤ n) ∧ (naplesPark n k [] (List.ofFn α)).isSome

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 1.

Uses 1 · Used by 8

Statement usesNaples parking

Used byNumber of ascending \(k\)-Naples parking functions · Number of ascending \(k\)-Naples parking functions starting with \(1\) · Number of descending \(k\)-Naples parking functions · Number of descending strictly \(k\)-Naples parking functions · When every rearrangement of a preference is \(k\)-Naples · A \(2\)-Naples parking function that is not \(1\)-Naples · Lattice-path criterion for ascending \(k\)-Naples parking functions · Every \(k\)-Naples parking function is \((k + 1)\)-Naples

TheoremA \(2\)-Naples parking example#✓fully proved

Under the \(2\)-Naples rule on the spots \(1, \dots, 7\), the cars with preferences \((6, 6, 6, 5, 5, 2, 1)\), arriving in order into an empty lot, all park, in the spots \(6, 5, 4, 3, 7, 2, 1\) respectively.

public theorem naplesPark_example :
    naplesPark 7 2 [] [6, 6, 6, 5, 5, 2, 1] = some [1, 2, 7, 3, 4, 5, 6]

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 1.

Uses 1

Statement usesNaples parking

TheoremA \(2\)-Naples parking function that is not \(1\)-Naples#✓fully proved

The preference \((6, 6, 6, 5, 5, 2, 1)\) of length \(7\) is a \(2\)-Naples parking function but not a \(1\)-Naples parking function.

public theorem isNaplesParkingFunction_example :
    IsNaplesParkingFunction 2 ![6, 6, 6, 5, 5, 2, 1] ∧
      ¬ IsNaplesParkingFunction 1 ![6, 6, 6, 5, 5, 2, 1]

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 1.

Uses 2

Statement uses\(k\)-Naples parking function

Proof usesNaples parking

DefinitionNumber of ascending \(k\)-Naples parking functions#✓fully proved

For natural numbers \(n\) and \(k\), \(I_{n,k}\) is the number of \(k\)-Naples parking functions \((a_1, \dots, a_n)\) of length \(n\) that are weakly increasing, that is, \(a_1 \le a_2 \le \dots \le a_n\).

public def ascendingNaplesCount (n k : ℕ) : ℕ :=
  ((Fintype.piFinset fun _ : Fin n => Finset.Icc 1 n).filter fun α =>
    (∀ i j : Fin n, i ≤ j → α i ≤ α j) ∧ IsNaplesParkingFunction k α).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Theorem 3.

Uses 2 · Used by 5

Statement uses\(k\)-Naples parking function · Naples parking

Used byAscending \(k\)-Naples parking functions and Dyck paths · Counting ascending \(1\)-Naples parking functions · Recurrence for ascending \(k\)-Naples parking functions · Generating functions for ascending \(k\)-Naples parking functions · Naples counts for \(n = 2\) and \(k = 1\)

DefinitionNumber of ascending \(k\)-Naples parking functions starting with \(1\)#✓fully proved

For natural numbers \(n\) and \(k\), \(U_{n,k}\) is the number of weakly increasing \(k\)-Naples parking functions \((a_1, \dots, a_n)\) of length \(n\) with \(a_1 = 1\); in particular \(U_{0,k} = 0\).

public def ascendingNaplesOneCount (n k : ℕ) : ℕ :=
  ((Fintype.piFinset fun _ : Fin n => Finset.Icc 1 n).filter fun α =>
    (∀ i j : Fin n, i ≤ j → α i ≤ α j) ∧ IsNaplesParkingFunction k α ∧
      ∃ i : Fin n, i.val = 0 ∧ α i = 1).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Theorem 3.

Uses 2 · Used by 4

Statement uses\(k\)-Naples parking function · Naples parking

Used byRecurrence for ascending \(k\)-Naples parking functions · Generating functions for ascending \(k\)-Naples parking functions · Ascending \(1\)-Naples parking functions starting with \(1\) and Fine numbers · Naples counts for \(n = 2\) and \(k = 1\)

DefinitionNumber of descending \(k\)-Naples parking functions#✓fully proved

For natural numbers \(n\) and \(k\), this is the number of \(k\)-Naples parking functions \(\alpha = (a_1, \dots, a_n)\) of length \(n\) (so \(a_i \in \{1, \dots, n\}\) for all \(i\)) that are descending, that is, weakly decreasing: \(a_1 \ge a_2 \ge \dots \ge a_n\).

public def descendingNaplesCount (n k : ℕ) : ℕ :=
  ((Fintype.piFinset fun _ : Fin n => Finset.Icc 1 n).filter fun α =>
    (∀ i j : Fin n, i ≤ j → α j ≤ α i) ∧ IsNaplesParkingFunction k α).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Proposition 2.

Uses 2 · Used by 4

Statement uses\(k\)-Naples parking function · Naples parking

Used byDescending \(k\)-Naples parking functions and Dyck paths · Descending \(k\)-Naples parking functions and \(k\)-Dyck paths · Counting descending \(k\)-Naples parking functions · Naples counts for \(n = 2\) and \(k = 1\)

DefinitionNumber of descending strictly \(k\)-Naples parking functions#✓fully proved

For natural numbers \(n\) and \(k\), this is the number of preferences \(\alpha = (a_1, \dots, a_n) \in \{1, \dots, n\}^n\) that are descending (\(a_1 \ge a_2 \ge \dots \ge a_n\)), are \(k\)-Naples parking functions, and are not \((k - 1)\)-Naples parking functions. It is used for \(k \ge 1\); for \(k = 0\), where \(k - 1\) is read as \(0\), the count is \(0\).

public def descendingStrictNaplesCount (n k : ℕ) : ℕ :=
  ((Fintype.piFinset fun _ : Fin n => Finset.Icc 1 n).filter fun α =>
    (∀ i j : Fin n, i ≤ j → α j ≤ α i) ∧ IsNaplesParkingFunction k α ∧
      ¬ IsNaplesParkingFunction (k - 1) α).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Proposition 4.

Uses 2 · Used by 6

Statement uses\(k\)-Naples parking function · Naples parking

Used byCounting descending \(k\)-Naples parking functions · Descending strictly \(k\)-Naples parking functions and binary trees · Descending strictly \(k\)-Naples parking functions and Dyck paths with an early return · Descending strictly \(k\)-Naples parking functions and noncrossing partitions · Descending strictly \(k\)-Naples parking functions and polygon dissections · Naples counts for \(n = 2\) and \(k = 1\)

TheoremNaples counts for \(n = 2\) and \(k = 1\)#✓fully proved

Among the preferences of length \(2\) with entries in \(\{1, 2\}\), exactly \(3\) are weakly increasing \(1\)-Naples parking functions (\(I_{2,1} = 3\)), and exactly \(2\) of these start with \(1\) (\(U_{2,1} = 2\)); exactly \(3\) are weakly decreasing \(1\)-Naples parking functions, and exactly \(1\) is weakly decreasing, \(1\)-Naples and not \(0\)-Naples.

public theorem naplesCount_two_one :
    ascendingNaplesCount 2 1 = 3 ∧ ascendingNaplesOneCount 2 1 = 2 ∧
      descendingNaplesCount 2 1 = 3 ∧ descendingStrictNaplesCount 2 1 = 1

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 4.

Uses 4

Statement usesNumber of ascending \(k\)-Naples parking functions · Number of ascending \(k\)-Naples parking functions starting with \(1\) · Number of descending \(k\)-Naples parking functions · Number of descending strictly \(k\)-Naples parking functions

DefinitionHeight of a lattice path#✓fully proved

For a lattice path \(p\) of \(m\) steps, each an Up step \((1, 1)\) or a Down step \((1, -1)\), and a natural number \(j\), the height of \(p\) after \(j\) steps is the number of Up steps minus the number of Down steps among the first \(\min(j, m)\) steps of \(p\).

public def latticeHeight {m : ℕ} (p : Fin m → Bool) (j : ℕ) : ℤ :=
  ∑ i : Fin m, if i.val < j then (if p i then 1 else -1) else 0

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 3.

Used by 5

Used byDescending \(k\)-Naples parking functions and \(k\)-Dyck paths · When every rearrangement of a preference is \(k\)-Naples · \(k\)-Dyck path · A \(1\)-Dyck path that is not a \(0\)-Dyck path · Lattice-path criterion for ascending \(k\)-Naples parking functions

DefinitionHeight of a sequence of Dyck steps#✓fully proved

For a finite sequence \(l\) of Up steps \(U\) and Down steps \(D\) and a natural number \(j\), the height of \(l\) after \(j\) steps is the integer obtained as the number of \(U\) minus the number of \(D\) among the first \(j\) steps of \(l\) (among all of \(l\) when \(j\) exceeds its length).

public def dyckStepHeight (l : List DyckStep) (j : ℕ) : ℤ :=
  ((l.take j).count DyckStep.U : ℤ) - ((l.take j).count DyckStep.D : ℤ)

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 3.

Used by 3

Used byAscending \(k\)-Naples parking functions and Dyck paths · Descending strictly \(k\)-Naples parking functions and Dyck paths with an early return · A \(1\)-Dyck path that is not a \(0\)-Dyck path

Definition\(k\)-Dyck path#✓fully proved

Let \(n\) and \(k\) be natural numbers. A lattice path of \(2n\) steps, each an Up step \((1, 1)\) or a Down step \((1, -1)\), is a \(k\)-Dyck path of semilength \(n\) if its height after all \(2n\) steps is \(0\), its height after its first \(j\) steps is at least \(-k\) for every \(j \le 2n\), and, when \(n \ge 1\), its last step is a Down step.

public def IsKDyckPath (n k : ℕ) (p : Fin (2 * n) → Bool) : Prop :=
  latticeHeight p (2 * n) = 0 ∧ (∀ j ≤ 2 * n, -(k : ℤ) ≤ latticeHeight p j) ∧
    ∀ i : Fin (2 * n), i.val + 1 = 2 * n → p i = false

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 3.

Uses 1 · Used by 2

Statement usesHeight of a lattice path

Used byDescending \(k\)-Naples parking functions and \(k\)-Dyck paths · A \(1\)-Dyck path that is not a \(0\)-Dyck path

TheoremA \(1\)-Dyck path that is not a \(0\)-Dyck path#✓fully proved

Write \(U\) for an Up step \((1, 1)\) and \(D\) for a Down step \((1, -1)\). The path \(DUUD\) is a \(1\)-Dyck path of semilength \(2\) but not a \(0\)-Dyck path, and the path \(UUD\) has height \(1\) after its three steps.

public theorem isKDyckPath_example :
    IsKDyckPath 2 1 ![false, true, true, false] ∧ ¬ IsKDyckPath 2 0 ![false, true, true, false] ∧
      dyckStepHeight [DyckStep.U, DyckStep.U, DyckStep.D] 3 = 1

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 3.

Uses 3

Statement uses\(k\)-Dyck path · Height of a sequence of Dyck steps

Proof usesHeight of a lattice path

TheoremEvery \(k\)-Naples parking function is \((k + 1)\)-Naples#●ready to prove

For all natural numbers \(k\) and \(n\), every \(k\)-Naples parking function \(\alpha\) of length \(n\) is also a \((k + 1)\)-Naples parking function.

public theorem_wanted IsNaplesParkingFunction.succ {k n : ℕ} {α : Fin n → ℕ}
    (h : IsNaplesParkingFunction k α) : IsNaplesParkingFunction (k + 1) α

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Proposition 1.

Uses 1

Statement uses\(k\)-Naples parking function

DefinitionThe \(k\)-Naples rule on \(\mathbb{Z}\)#✓fully proved

When the spots in a finite list \(O\) of integers are occupied, a car preferring \(a \in \mathbb{Z}\) parks in \(a\) if \(a\) is free; otherwise in the first free spot among \(a - 1, \dots, a - k\), checked in decreasing order with no lower bound; otherwise in the first free spot among \(a + 1, \dots, a + |O| + 1\), checked in increasing order (one of them is free, so this is the first free spot after \(a\)).

public def naplesSpotInt (k : ℕ) (occ : List ℤ) (a : ℤ) : ℤ :=
  if a ∉ occ then a else
    match ((List.range k).map fun j => a - ((j + 1 : ℕ) : ℤ)).find? (fun s => decide (s ∉ occ)) with
    | some s => s
    | none => (((List.range (occ.length + 1)).map fun j => a + ((j + 1 : ℕ) : ℤ)).find?
        (fun s => decide (s ∉ occ))).getD a

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 2 (parking on ℤ).

Used by 1

Used byNaples parking on \(\mathbb{Z}\)

DefinitionNaples parking on \(\mathbb{Z}\)#✓fully proved

Starting from a list of occupied spots in \(\mathbb{Z}\), cars with integer preferences \(a_1, \dots, a_m\) arrive in order, and each takes the spot given by the \(k\)-Naples rule on \(\mathbb{Z}\) for the spots occupied when it arrives. The result is the final list of occupied spots: the spots of the cars, most recent first, followed by the initially occupied spots.

public def naplesParkInt (k : ℕ) : List ℤ → List ℤ → List ℤ
  | occ, [] => occ
  | occ, a :: as => naplesParkInt k (naplesSpotInt k occ a :: occ) as

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 2 (parking on ℤ).

Uses 1 · Used by 3

Statement usesThe \(k\)-Naples rule on \(\mathbb{Z}\)

Used byA \(2\)-Naples parking example on \(\mathbb{Z}\) · A \(3\)-Naples parking example on \(\mathbb{Z}\) · One more backward step keeps the cars in \(\{0, \dots, n\}\)

TheoremA \(2\)-Naples parking example on \(\mathbb{Z}\)#✓fully proved

Under the \(2\)-Naples rule on \(\mathbb{Z}\), the cars with preferences \((4, 2, 2, 2)\), arriving in order with no spot occupied, park in the spots \(4, 2, 1, 0\) respectively.

public theorem naplesParkInt_example :
    naplesParkInt 2 [] [4, 2, 2, 2] = [0, 1, 2, 4]

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 2, Figure 1.

Uses 1

Statement usesNaples parking on \(\mathbb{Z}\)

TheoremA \(3\)-Naples parking example on \(\mathbb{Z}\)#✓fully proved

Under the \(3\)-Naples rule on \(\mathbb{Z}\), the cars with preferences \((1, 2, 2, 5, 7, 7, 7, 3)\), arriving in order with no spot occupied, park in the spots \(1, 2, 0, 5, 7, 6, 4, 3\) respectively.

public theorem naplesParkInt_example_three :
    naplesParkInt 3 [] [1, 2, 2, 5, 7, 7, 7, 3] = [3, 4, 6, 7, 5, 0, 2, 1]

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 2, Remark 2.

Uses 1

Statement usesNaples parking on \(\mathbb{Z}\)

TheoremOne more backward step keeps the cars in \(\{0, \dots, n\}\)#●ready to prove

Let \((a_1, \dots, a_n)\) be integers with \(1 \le a_j \le n\) for every \(j\). If, under the \(k\)-Naples rule on \(\mathbb{Z}\), the cars with these preferences, arriving in order with no spot occupied, occupy exactly the spots \(1, \dots, n\), then under the \((k + 1)\)-Naples rule on \(\mathbb{Z}\) every car parks in a spot \(s\) with \(0 \le s \le n\).

Every \(k \ge 0\) is admitted (the source's proof treats any \(k \ge 0\)).

public theorem_wanted naplesParkInt_succ_mem_Icc {k n : ℕ} {α : List ℤ} (hlen : α.length = n)
    (hα : ∀ a ∈ α, 1 ≤ a ∧ a ≤ n)
    (hpark : ∀ s : ℤ, s ∈ naplesParkInt k [] α ↔ 1 ≤ s ∧ s ≤ n) :
    ∀ s ∈ naplesParkInt (k + 1) [] α, 0 ≤ s ∧ s ≤ n

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Lemma 1.

Uses 1

Statement usesNaples parking on \(\mathbb{Z}\)

TheoremDescending \(k\)-Naples parking functions and \(k\)-Dyck paths#●ready to prove

For all natural numbers \(n \ge 1\) and \(k \ge 1\), the number of weakly decreasing \(k\)-Naples parking functions of length \(n\) equals the number of \(k\)-Dyck paths of length \(n\): sequences of \(2n\) Up and Down steps that end at height \(0\), never go below height \(-k\), and end with a Down step.

public theorem_wanted descendingNaplesCount_eq_card_kDyckPath {n k : ℕ} (hn : 1 ≤ n)
    (hk : 1 ≤ k) :
    descendingNaplesCount n k = (Finset.univ.filter (IsKDyckPath n k)).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Proposition 2 (citing Christensen et al., Theorem 1.3).

Uses 3

Statement uses\(k\)-Dyck path · Number of descending \(k\)-Naples parking functions · Height of a lattice path

TheoremDescending \(k\)-Naples parking functions and Dyck paths#●ready to prove

For all natural numbers \(n \ge 1\) and \(k \ge 1\), the number of weakly decreasing \(k\)-Naples parking functions of length \(n\) equals the number of Dyck paths of semilength \(n + k\) (that is, with \(2(n + k)\) steps) whose first \(k\) steps are Up and whose last \(k + 1\) steps are Down.

public theorem_wanted descendingNaplesCount_eq_card_dyckPath {n k : ℕ} (hn : 1 ≤ n)
    (hk : 1 ≤ k) :
    descendingNaplesCount n k = (Finset.univ.filter fun p : {p : DyckWord // p.semilength = n + k} =>
      List.replicate k DyckStep.U <+: p.1.toList ∧
        List.replicate (k + 1) DyckStep.D <:+ p.1.toList).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Proposition 3.

Uses 1

Statement usesNumber of descending \(k\)-Naples parking functions

TheoremDescending strictly \(k\)-Naples parking functions and Dyck paths with an early return#●ready to prove

For \(n \ge 1\) and \(k \ge 1\), the number of descending strictly \(k\)-Naples parking functions of length \(n\) (descending preferences that are \(k\)-Naples but not \((k - 1)\)-Naples) equals the number of Dyck paths of semilength \(n + k\), that is, with \(2(n + k)\) Up and Down steps, whose first \(k\) steps are Up, whose last \(k + 1\) steps are Down, and whose height after \(j\) steps is \(0\) for some \(j\) with \(0 < j < 2(n + k)\).

public theorem_wanted descendingStrictNaplesCount_eq_card_dyckPath {n k : ℕ} (hn : 1 ≤ n)
    (hk : 1 ≤ k) :
    descendingStrictNaplesCount n k = (Finset.univ.filter fun p : {p : DyckWord // p.semilength = n + k} =>
      List.replicate k DyckStep.U <+: p.1.toList ∧
        List.replicate (k + 1) DyckStep.D <:+ p.1.toList ∧
        ∃ j < 2 * (n + k), 0 < j ∧ dyckStepHeight p.1.toList j = 0).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Proposition 4.

Uses 2

Statement usesNumber of descending strictly \(k\)-Naples parking functions · Height of a sequence of Dyck steps

TheoremRecurrence for ascending \(k\)-Naples parking functions#●ready to prove

Let \(I_{n,k}\) be the number of weakly increasing \(k\)-Naples parking functions of length \(n\), let \(U_{n,k}\) be the number of those whose first entry is \(1\), and let \(C_k\) be the \(k\)-th Catalan number. For all natural numbers \(n\) and \(k\) with \(1 \le k \le n - 1\),

\[I_{n,k} = I_{n,k-1} + C_k \sum_{i=0}^{n-k} I_{i,k-1} \, U_{n-k-i,k}\]

and

\[U_{n,k} = U_{n,k-1} + C_k \sum_{i=0}^{n-k} U_{i,k-1} \, U_{n-k-i,k}.\]

public theorem_wanted ascendingNaplesCount_recurrence {n k : ℕ} (hk : 1 ≤ k) (hkn : k + 1 ≤ n) :
    ascendingNaplesCount n k = ascendingNaplesCount n (k - 1) + catalan k *
        ∑ i ∈ Finset.range (n - k + 1),
          ascendingNaplesCount i (k - 1) * ascendingNaplesOneCount (n - k - i) k ∧
      ascendingNaplesOneCount n k = ascendingNaplesOneCount n (k - 1) + catalan k *
        ∑ i ∈ Finset.range (n - k + 1),
          ascendingNaplesOneCount i (k - 1) * ascendingNaplesOneCount (n - k - i) k

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Theorem 3.

Uses 2

Statement usesNumber of ascending \(k\)-Naples parking functions · Number of ascending \(k\)-Naples parking functions starting with \(1\)

TheoremAscending \(1\)-Naples parking functions starting with \(1\) and Fine numbers#●ready to prove

For every natural number \(n\), the number \(U_{n,1}\) of weakly increasing \(1\)-Naples parking functions of length \(n\) whose first entry is \(1\) equals the Fine number \(F(n + 1)\), where the Fine numbers \(1, 0, 1, 2, 6, 18, \dots\) are indexed so that \(F(0) = 1\) and \(F(1) = 0\) (OEIS A000957).

public theorem_wanted ascendingNaplesOneCount_one_eq_fineNumber (n : ℕ) :
    (ascendingNaplesOneCount n 1 : ℚ) = fineNumber (n + 1)

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Theorem 4.

Uses 2

Statement usesNumber of ascending \(k\)-Naples parking functions starting with \(1\) · Fine numbers

TheoremCounting ascending \(1\)-Naples parking functions#●ready to prove

For every natural number \(n\), let \(I_{n,1}\) be the number of weakly increasing \(1\)-Naples parking functions of length \(n\). Then

\[I_{n,1} = \sum_{i=0}^{n} C_i \, F(n - i),\]

where \(C_i\) is the \(i\)-th Catalan number and \(F\) is the sequence of Fine numbers, indexed so that \(F(0) = 1\) and \(F(1) = 0\). This is the convolution of the Catalan and Fine numbers (OEIS A000958).

public theorem_wanted ascendingNaplesCount_one_eq_sum (n : ℕ) :
    (ascendingNaplesCount n 1 : ℚ) =
      ∑ i ∈ Finset.range (n + 1), (catalan i : ℚ) * fineNumber (n - i)

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Theorem 5.

Uses 2

Statement usesNumber of ascending \(k\)-Naples parking functions · Fine numbers

TheoremGenerating functions for ascending \(k\)-Naples parking functions#●ready to prove

Let \(I_{n,k}\) be the number of weakly increasing \(k\)-Naples parking functions of length \(n\), let \(U_{n,k}\) be the number of those whose first entry is \(1\), and let \(C_k\) be the \(k\)-th Catalan number. Write \(I_k(x) = \sum_{n \ge 0} I_{n,k} x^n\) and \(U_k(x) = \sum_{n \ge 0} U_{n,k} x^n\), formal power series with natural number coefficients. For every natural number \(k \ge 1\),

\[I_k(x) = I_{k-1}(x) + C_k x^k I_{k-1}(x) U_k(x)\]

and

\[U_k(x) = U_{k-1}(x) + C_k x^k U_{k-1}(x) U_k(x).\]

public theorem_wanted ascendingNaples_generatingFunction {k : ℕ} (hk : 1 ≤ k) :
    PowerSeries.mk (fun n => ascendingNaplesCount n k) =
        PowerSeries.mk (fun n => ascendingNaplesCount n (k - 1)) +
          (catalan k : PowerSeries ℕ) * PowerSeries.X ^ k *
            PowerSeries.mk (fun n => ascendingNaplesCount n (k - 1)) *
            PowerSeries.mk (fun n => ascendingNaplesOneCount n k) ∧
      PowerSeries.mk (fun n => ascendingNaplesOneCount n k) =
        PowerSeries.mk (fun n => ascendingNaplesOneCount n (k - 1)) +
          (catalan k : PowerSeries ℕ) * PowerSeries.X ^ k *
            PowerSeries.mk (fun n => ascendingNaplesOneCount n (k - 1)) *
            PowerSeries.mk (fun n => ascendingNaplesOneCount n k)

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Theorem 6.

Uses 2

Statement usesNumber of ascending \(k\)-Naples parking functions · Number of ascending \(k\)-Naples parking functions starting with \(1\)

TheoremCounting descending \(k\)-Naples parking functions#●ready to prove

For all natural numbers \(n \ge 1\) and \(k \ge 1\), the number of weakly decreasing \(k\)-Naples parking functions of length \(n\) is \(\binom{2n-1}{n} - \binom{2n-1}{n+k+1}\), and the number of weakly decreasing strictly \(k\)-Naples parking functions of length \(n\) (those that are \(k\)-Naples but not \((k-1)\)-Naples) is \(\frac{k+1}{n} \binom{2n}{n+k+1}\).

public theorem_wanted descendingNaplesCount_eq_choose {n k : ℕ} (hn : 1 ≤ n) (hk : 1 ≤ k) :
    descendingNaplesCount n k = Nat.choose (2 * n - 1) n - Nat.choose (2 * n - 1) (n + k + 1) ∧
      (descendingStrictNaplesCount n k : ℚ) =
        ((k : ℚ) + 1) / n * Nat.choose (2 * n) (n + k + 1)

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Theorem 7.

Uses 2

Statement usesNumber of descending \(k\)-Naples parking functions · Number of descending strictly \(k\)-Naples parking functions

DefinitionLattice path of a parking preference#✓fully proved

Let \(\alpha = (a_1, \dots, a_n)\) be a sequence of natural numbers. Its lattice path is the sequence of \(2n\) steps, each an Up step \((1, 1)\) or a Down step \((1, -1)\), obtained by taking, for each spot \(s = 1, \dots, n\) in turn, one Up step for every index \(i\) with \(a_i = s\) followed by one Down step, and then appending Down steps until there are \(2n\) steps. When every \(a_i\) lies in \(\{1, \dots, n\}\) this gives exactly \(2n\) steps and nothing is appended; if moreover \(\alpha\) is weakly increasing, the \(i\)-th Up step is preceded by exactly \(a_i - 1\) Down steps.

public def preferencePath {n : ℕ} (α : Fin n → ℕ) : Fin (2 * n) → Bool := fun j =>
  ((List.range n).flatMap fun s =>
    List.replicate (Finset.univ.filter fun i => α i = s + 1).card true ++ [false]).getD j false

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 3 (Remark 3.3).

Used by 3

Used byWhen every rearrangement of a preference is \(k\)-Naples · Lattice-path criterion for ascending \(k\)-Naples parking functions · The lattice path of \((1, 3, 3, 5, 6, 6)\)

TheoremThe lattice path of \((1, 3, 3, 5, 6, 6)\)#✓fully proved

The lattice path of the parking preference \((1, 3, 3, 5, 6, 6)\) is \(\mathrm{UDDUUDDUDUUD}\), where \(\mathrm{U}\) is an Up step and \(\mathrm{D}\) a Down step.

public theorem preferencePath_example :
    preferencePath ![1, 3, 3, 5, 6, 6] =
      ![true, false, false, true, true, false, false, true, false, true, true, false]

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 3 (Figure 3).

Uses 1

Statement usesLattice path of a parking preference

TheoremRemaining cars still park after moving a car to an earlier spot#●ready to prove

Let \((a_1, \dots, a_n)\) be a parking preference with \(1 \le a_j \le n\) for every \(j\), with which all \(n\) cars, arriving in order into an empty lot, park under the \(k\)-Naples rule on the spots \(1, \dots, n\), car \(j\) in spot \(d_j\). Let \(1 \le l \le i \le n\), and let \(q\) be a spot with \(1 \le q < d_l\) and \(q \ne d_j\) for every \(j \le i\) with \(j \ne l\). If exactly the spots \(d_1, \dots, d_i\), with \(d_l\) replaced by \(q\), are occupied, then the remaining cars \(a_{i+1}, \dots, a_n\), arriving in order, all park under the \(k\)-Naples rule.

public theorem_wanted naplesPark_drop_set_isSome {n k i l q : ℕ} {α : Fin n → ℕ}
    {d : List ℕ} (hα : ∀ j, 1 ≤ α j ∧ α j ≤ n)
    (hd : naplesPark n k [] (List.ofFn α) = some d.reverse) (hl : l < i) (hi : i ≤ n)
    (hq : 1 ≤ q) (hql : q < d.getD l 0) (hqd : ∀ j < i, j ≠ l → d.getD j 0 ≠ q) :
    (naplesPark n k ((d.take i).set l q) ((List.ofFn α).drop i)).isSome

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Lemma 2.3.

Uses 1

Statement usesNaples parking

TheoremLattice-path criterion for ascending \(k\)-Naples parking functions#●ready to prove

Let \(\alpha = (a_1, \dots, a_n)\) be a weakly increasing preference with \(1 \le a_i \le n\) for every \(i\), and let \(h_j\) be the height after the first \(j\) steps of the lattice path of \(\alpha\), which has \(2n\) steps. Then \(\alpha\) is a \(k\)-Naples parking function if and only if for every \(j\) with \(1 \le j \le 2n\) and \(h_j < 0\) there is a \(j'\) with \(j < j' \le j + 2k\), \(j' \le 2n\) and \(h_{j'} > 0\).

public theorem_wanted isNaplesParkingFunction_iff_of_monotone {n k : ℕ} {α : Fin n → ℕ}
    (hα : ∀ i, 1 ≤ α i ∧ α i ≤ n) (hmono : Monotone α) :
    IsNaplesParkingFunction k α ↔
      ∀ i < 2 * n, latticeHeight (preferencePath α) (i + 1) < 0 →
        ∃ j, i + 1 < j ∧ j ≤ i + 1 + 2 * k ∧ j ≤ 2 * n ∧
          0 < latticeHeight (preferencePath α) j

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Theorem 2.6 (published as Theorem 2).

Uses 3

Statement uses\(k\)-Naples parking function · Height of a lattice path · Lattice path of a parking preference

TheoremWhen every rearrangement of a preference is \(k\)-Naples#●ready to prove

Let \(\alpha = (a_1, \dots, a_n) \in \{1, \dots, n\}^n\) and let \(P\) be its lattice path: for each spot \(s = 1, \dots, n\) in turn, one Up step for every car preferring \(s\), then one Down step (this is also the lattice path of the ascending rearrangement of \(\alpha\)). The height of \(P\) after \(m\) steps is the number of Up steps minus the number of Down steps among its first \(m\) steps. Then every rearrangement of \(\alpha\) is a \(k\)-Naples parking function if and only if, for every \(i\) with \(1 \le i \le 2n\) such that the height of \(P\) after \(i\) steps is negative, there is a \(j\) with \(i < j \le i + 2k\) and \(j \le 2n\) such that the height of \(P\) after \(j\) steps is positive.

public theorem_wanted forall_perm_isNaplesParkingFunction_iff {n k : ℕ} {α : Fin n → ℕ}
    (hα : ∀ i, 1 ≤ α i ∧ α i ≤ n) :
    (∀ σ : Equiv.Perm (Fin n), IsNaplesParkingFunction k (α ∘ σ)) ↔
      ∀ i < 2 * n, latticeHeight (preferencePath α) (i + 1) < 0 →
        ∃ j, i + 1 < j ∧ j ≤ i + 1 + 2 * k ∧ j ≤ 2 * n ∧
          0 < latticeHeight (preferencePath α) j

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Corollary 2.7 (published as Corollary 1).

Uses 3

Statement uses\(k\)-Naples parking function · Height of a lattice path · Lattice path of a parking preference

TheoremAscending \(k\)-Naples parking functions and Dyck paths#●ready to prove

For all natural numbers \(n \ge 1\) and \(k\), the number of weakly increasing \(k\)-Naples parking functions of length \(n\) equals the number of Dyck paths of semilength \(n + k\) (that is, with \(2(n + k)\) steps) whose first \(k\) steps are Up, whose last \(k + 1\) steps are Down, and which satisfy the following condition. Writing \(h_j\) for the height after the first \(j\) steps, whenever the \(m\)-th step is a Down step that is not among the last \(k + 1\) steps and \(h_m < k\), there is a \(j\) with \(m < j \le m + 2k\) and \(j \le 2(n + k)\) such that \(h_j > k\).

public theorem_wanted ascendingNaplesCount_eq_card_dyckPath {n k : ℕ} (hn : 1 ≤ n) :
    ascendingNaplesCount n k = (Finset.univ.filter fun p : {p : DyckWord // p.semilength = n + k} =>
      List.replicate k DyckStep.U <+: p.1.toList ∧
        List.replicate (k + 1) DyckStep.D <:+ p.1.toList ∧
        ∀ i, i + (k + 1) < 2 * (n + k) → p.1.toList[i]? = some DyckStep.D →
          dyckStepHeight p.1.toList (i + 1) < k →
            ∃ j, i + 1 < j ∧ j ≤ i + 1 + 2 * k ∧ j ≤ 2 * (n + k) ∧
              (k : ℤ) < dyckStepHeight p.1.toList j).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Corollary 2.12 (published as Corollary 3).

Uses 2

Statement usesNumber of ascending \(k\)-Naples parking functions · Height of a sequence of Dyck steps

DefinitionLeft spine length of a binary tree#✓fully proved

The number of nodes on the left spine of a binary tree: the root, its left child, that child's left child, and so on (0 for the empty tree).

public def leftSpineLength {α : Type*} : BinaryTree α → ℕ
  | .nil => 0
  | .node _ l _ => leftSpineLength l + 1

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 4 (Proposition 4.12).

Used by 2

Used byDescending strictly \(k\)-Naples parking functions and binary trees · Left spine lengths of small binary trees

TheoremLeft spine lengths of small binary trees#✓fully proved

The empty binary tree has left spine length \(0\), and the binary tree with three nodes, a root whose left child and right child have no children, has left spine length \(2\).

public theorem leftSpineLength_examples :
    leftSpineLength (BinaryTree.nil : BinaryTree Unit) = 0 ∧
      leftSpineLength (BinaryTree.node () (BinaryTree.node () .nil .nil)
        (BinaryTree.node () .nil .nil)) = 2

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 4 (Proposition 4.12).

Uses 1

Statement usesLeft spine length of a binary tree

TheoremDescending strictly \(k\)-Naples parking functions and binary trees#●ready to prove

For every \(n\) and every \(k \ge 1\), the number of descending strictly \(k\)-Naples parking functions of length \(n\) (descending preferences that are \(k\)-Naples but not \((k - 1)\)-Naples) equals the number of binary trees \(t\) with \(n + k\) nodes such that the left spine of \(t\) (the root, its left child, that child's left child, and so on) has at least \(k\) nodes and the left spine of the right subtree of \(t\) has at least \(k + 1\) nodes.

public theorem_wanted descendingStrictNaplesCount_eq_card_binaryTree {n k : ℕ} (hk : 1 ≤ k) :
    descendingStrictNaplesCount n k = ((BinaryTree.treesOfNumNodesEq (n + k)).filter fun t =>
      k ≤ leftSpineLength t ∧ k + 1 ≤ leftSpineLength t.right).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Proposition 4.12 (published as Proposition 5).

Uses 2

Statement usesNumber of descending strictly \(k\)-Naples parking functions · Left spine length of a binary tree

DefinitionEdges of an inscribed polygon#✓fully proved

Let \(R\) be a set of vertices of the convex \(s\)-gon with vertices \(0, 1, \dots, s - 1\). The edges of the polygon with vertex set \(R\) are the pairs \((a, b)\) of elements of \(R\) with \(a < b\) such that either no element of \(R\) lies strictly between \(a\) and \(b\), or \(a\) is the least and \(b\) the greatest element of \(R\).

public def inscribedPolygonEdges {s : ℕ} (R : Finset (Fin s)) : Finset (Fin s × Fin s) :=
  (R ×ˢ R).filter fun e => e.1 < e.2 ∧
    ((∀ c ∈ R, ¬ (e.1 < c ∧ c < e.2)) ∨ ∀ c ∈ R, e.1 ≤ c ∧ c ≤ e.2)

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 6 (Theorem 6.3).

Used by 3

Used by\(r\)-in-\(s\) dissection · Examples of \(r\)-in-\(s\) dissections · Descending strictly \(k\)-Naples parking functions and polygon dissections

Definition\(r\)-in-\(s\) dissection#✓fully proved

Let \(D\) be a set of pairs \((a, b)\) of vertices of the convex \(s\)-gon with vertices \(0, 1, \dots, s - 1\), and let \(R\) be a set of its vertices. Then \(D\) is an \(r\)-in-\(s\) dissection with inner polygon \(R\) when all of the following hold: the number of elements of \(D\) plus \(r\) equals \(s\), and \(R\) has \(r\) elements; every \((a, b) \in D\) is a diagonal, that is, \(a + 2 \le b\) and \((a, b) \ne (0, s - 1)\); no \((a, b)\) and \((c, d)\) in \(D\) cross, that is, \(a < c < b < d\) never holds; every edge of the polygon with vertex set \(R\) is a side of the \(s\)-gon, \((a, a + 1)\) or \((0, s - 1)\), or lies in \(D\); and every element of \(D\) with both endpoints in \(R\) is an edge of the polygon with vertex set \(R\).

The remaining \(s - r\) faces of such a dissection are triangles.

public def IsInnerPolygonDissection (s r : ℕ) (D : Finset (Fin s × Fin s))
    (R : Finset (Fin s)) : Prop :=
  D.card + r = s ∧ R.card = r ∧
    (∀ e ∈ D, e.1.val + 2 ≤ e.2.val ∧ ¬ (e.1.val = 0 ∧ e.2.val + 1 = s)) ∧
    (∀ e ∈ D, ∀ f ∈ D, ¬ (e.1 < f.1 ∧ f.1 < e.2 ∧ e.2 < f.2)) ∧
    (∀ e ∈ inscribedPolygonEdges R,
      e.2.val = e.1.val + 1 ∨ (e.1.val = 0 ∧ e.2.val + 1 = s) ∨ e ∈ D) ∧
    ∀ e ∈ D, e.1 ∈ R → e.2 ∈ R → e ∈ inscribedPolygonEdges R

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 6 (Definition 6.1).

Uses 1 · Used by 2

Statement usesEdges of an inscribed polygon

Used byExamples of \(r\)-in-\(s\) dissections · Descending strictly \(k\)-Naples parking functions and polygon dissections

TheoremExamples of \(r\)-in-\(s\) dissections#✓fully proved

For the convex polygons with vertices \(0, 1, \dots, s - 1\): the square (\(s = 4\)) with no diagonals is a \(4\)-in-\(4\) dissection whose quadrilateral has all four vertices; the pentagon (\(s = 5\)) with the single diagonal \((0, 2)\) is a \(4\)-in-\(5\) dissection with quadrilateral on the vertices \(0, 2, 3, 4\), but not with quadrilateral on the vertices \(0, 1, 2, 3\).

public theorem isInnerPolygonDissection_examples :
    IsInnerPolygonDissection 4 4 ∅ Finset.univ ∧
      IsInnerPolygonDissection 5 4 {(0, 2)} {0, 2, 3, 4} ∧
      ¬ IsInnerPolygonDissection 5 4 {(0, 2)} {0, 1, 2, 3}

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Section 6 (Definition 6.1).

Uses 2

Statement uses\(r\)-in-\(s\) dissection

Proof usesEdges of an inscribed polygon

TheoremDescending strictly \(k\)-Naples parking functions and polygon dissections#●ready to prove

Let \(n\) and \(k \ge 1\) be natural numbers and let \(s = n + k + 1\). Then \(s\) times the number of weakly decreasing preferences of length \(n\) that are \(k\)-Naples but not \((k - 1)\)-Naples parking functions equals the number of triples \((D, R, e)\) such that the set of diagonals \(D\) and the vertex set \(R\) form a \((2k + 2)\)-in-\(s\) dissection of the convex \(s\)-gon with vertices \(0, \dots, s - 1\), and \(e\) is an edge of the inscribed polygon with vertex set \(R\).

Rotations of the \(s\)-gon act freely on these triples, so this says that descending strictly \(k\)-Naples parking functions of length \(n\) are in bijection with \((2k + 2)\)-in-\(s\) dissections up to rotation with a distinguished edge on the \((2k + 2)\)-gon.

public theorem_wanted mul_descendingStrictNaplesCount_eq_card_dissection {n k : ℕ}
    (hk : 1 ≤ k) :
    (n + k + 1) * descendingStrictNaplesCount n k =
      (Finset.univ.filter fun x : Finset (Fin (n + k + 1) × Fin (n + k + 1)) ×
          Finset (Fin (n + k + 1)) × (Fin (n + k + 1) × Fin (n + k + 1)) =>
        IsInnerPolygonDissection (n + k + 1) (2 * k + 2) x.1 x.2.1 ∧
          x.2.2 ∈ inscribedPolygonEdges x.2.1).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Theorem 6.3 (published as Proposition 6).

Uses 3

Statement uses\(r\)-in-\(s\) dissection · Number of descending strictly \(k\)-Naples parking functions · Edges of an inscribed polygon

TheoremDescending strictly \(k\)-Naples parking functions and noncrossing partitions#●ready to prove

For every \(n\) and every \(k \ge 1\), the number of descending strictly \(k\)-Naples parking functions of length \(n\) (descending preferences that are \(k\)-Naples but not \((k - 1)\)-Naples) equals the number of noncrossing partitions of \(\{0, 1, \dots, n + k\}\) in which the block containing \(0\) has exactly \(2k + 2\) elements.

public theorem_wanted descendingStrictNaplesCount_eq_card_noncrossingPartition {n k : ℕ}
    (hk : 1 ≤ k) :
    descendingStrictNaplesCount n k = (Finset.univ.filter fun P : NoncrossingPartition (n + k + 1) =>
      (NoncrossingPartition.block P 0).card = 2 * k + 2).card

Sources

• J. P. Carvalho, P. E. Harris, G. Rojas Kirby, N. Tripeny and A. R. Vindas Meléndez, Enumerating k-Naples Parking Functions through Catalan Objects, INTEGERS 24 (2024), Article A44, Theorem 6.4 (published as Proposition 7).

Uses 6

Statement usesNumber of descending strictly \(k\)-Naples parking functions · Noncrossing partition · Crossing in a set partition · Noncrossing set partition · Set partition · Block of a noncrossing partition

25 fully proved17 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.