Dyck paths and lattice walks

Statistics on Dyck paths (peaks, valleys, marked steps, subwords) and their variants (skew, rational, k-box Dyck paths), lattice walks with unit or diagonal steps, Delannoy numbers, Sulanke arrays, colored Dyck paths, and nonintersecting paths via the Lindström–Gessel–Viennot lemma.

• Generalized Delannoy numbers
• Gessel words
• k-box paths and skew Dyck paths
• Marked Dyck paths
• Peak descents of Dyck paths
• Rational Dyck paths
• Subwords in non-decreasing Dyck paths
• Sulanke arrays

TheoremLindström–Gessel–Viennot lemma#✓fully proved

Let \(R\) be a commutative ring, let \(n\) be a natural number, and let \(E\) be a relation on a type \(V\), read as a directed graph on \(V\) with an edge from \(u\) to \(v\) whenever \(E(u, v)\). Suppose there is a function \(r : V \to \mathbb{N}\) with \(r(u) < r(v)\) whenever \(E(u, v)\), so the graph is acyclic. A path from \(u\) to \(w\) is a nonempty list of vertices that starts at \(u\), ends at \(w\), and in which there is an edge from each vertex to the next one. Let \(A_0, \dots, A_{n-1}\) and \(B_0, \dots, B_{n-1}\) be vertices, and suppose that for all \(i, j < n\) the paths from \(A_i\) to \(B_j\) form a finite set \(P_{ij}\). Let \(e\) be the \(n \times n\) matrix over \(R\) with \(e_{ij} = |P_{ij}|\). Suppose further that whenever \(i < j\) and \(l < k\), every path from \(A_i\) to \(B_k\) shares a vertex with every path from \(A_j\) to \(B_l\). Let \(S\) be the finite set of families \((F_0, \dots, F_{n-1})\) in which each \(F_i\) is a path from \(A_i\) to \(B_i\) and \(F_i\) and \(F_j\) share no vertex whenever \(i \ne j\). Then the number of elements of \(S\), taken in \(R\), equals \(\det e\).

MetaMathlibExt.lindstrom_gessel_viennot · 21 lines

theorem lindstrom_gessel_viennot
    {V : Type*} [DecidableEq V]
    {R : Type*} [CommRing R]
    (n : ℕ)
    (E : V → V → Prop)
    (A B : Fin n → V)
    (rank : V → ℕ)
    (hAcyc : ∀ u v : V, E u v → rank u < rank v)
    (P : Fin n → Fin n → Finset (List V))
    (hPath : ∀ i j : Fin n, ∀ p : List V, p ∈ P i j ↔
      (p.head? = some (A i) ∧ p.getLast? = some (B j) ∧
        p.IsChain (fun u v => E u v)))
    (e : Fin n → Fin n → R)
    (he : ∀ i j : Fin n, e i j = ((P i j).card : R))
    (hPlanar : ∀ i j k l : Fin n, i < j → l < k →
      ∀ p ∈ P i k, ∀ q ∈ P j l, ∃ v : V, v ∈ p ∧ v ∈ q)
    (S : Finset (Fin n → List V))
    (hSys : ∀ F : Fin n → List V, F ∈ S ↔
      ((∀ i : Fin n, F i ∈ P i i) ∧
        ∀ i j : Fin n, i ≠ j → Disjoint (F i).toFinset (F j).toFinset)) :
    (S.card : R) = Matrix.det e

Sources

• https://en.wikipedia.org/wiki/Lindstr%C3%B6m%E2%80%93Gessel%E2%80%93Viennot_lemma

TheoremMinimal lattice walks with unit and diagonal steps#✓fully proved

For all natural numbers \(a\) and \(b\), the number of sequences of \(\max(a, b)\) steps, each taken from \(\{(1,0), (0,1), (1,1)\}\), whose sum is \((a, b)\) equals \(\binom{\max(a, b)}{\min(a, b)}\).

Every walk from the origin to \((a, b)\) with these steps has at least \(\max(a, b)\) steps, since each step raises each coordinate by at most \(1\), and walks of exactly that length exist; so the sequences counted are the minimal-length walks from the origin to \((a, b)\).

theorem minimal_lattice_walk_count (a b : ℕ) :
    Finset.card (Finset.univ.filter (fun f : Fin (max a b) → Fin 3 =>
      (∑ i, (![1, 0, 1] : Fin 3 → ℕ) (f i)) = a ∧
      (∑ i, (![0, 1, 1] : Fin 3 → ℕ) (f i)) = b)) =
    Nat.choose (max a b) (min a b)

Sources

• Jackson Evoniuk, Steven Klee, and Van Magnan, "Enumerating Minimal Length Lattice Paths," Journal of Integer Sequences 21 (2018), Article 18.3.6, Theorem (section Minimal walks for S = {(1,0),(0,1),(1,1)}, label sec2), lines 273–275, https://cs.uwaterloo.ca/journals/JIS/VOL21/Klee/klee2.tex

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.