Skip to content

Special counting sequences

DefinitionLattice paths with prescribed steps#✓fully proved

Let \(d \in \mathbb{N}\), let \(D \subseteq \mathbb{Z}^d\) and let \(p, q \in \mathbb{Z}^d\). A lattice path from \(p\) to \(q\) with step set \(D\) is a finite sequence \((v_0, v_1, \dots, v_m)\) of points of \(\mathbb{Z}^d\), for some \(m \in \mathbb{N}\), such that \(v_0 = p\), \(v_m = q\), and \(v_i - v_{i-1} \in D\) for \(1 \le i \le m\).

The case \(m = 0\) is the path of length zero, which is a lattice path from \(p\) to \(q\) exactly when \(p = q\).

def LatticePath (d : ℕ)
    (D : Set (Fin d → ℤ))
    (p q : Fin d → ℤ) :=
  { l : List (Fin d → ℤ) //
    l.head? = some p ∧
    l.getLast? = some q ∧
    List.IsChain
      (fun a b => b - a ∈ D) l
  }

DefinitionFixed-length necklaces#✓fully proved

Let \(A\) be a set and let \(n \in \mathbb{N}\). For \(n \ge 1\), a word of length \(n\) over \(A\) is a tuple \((a_0, a_1, \dots, a_{n-1})\) of elements of \(A\), and two words \((a_0, \dots, a_{n-1})\) and \((b_0, \dots, b_{n-1})\) are rotationally equivalent if there is an integer \(r\) with \(0 \le r < n\) such that \(b_i = a_{(i+r) \bmod n}\) for \(0 \le i < n\). A necklace of length \(n\) over \(A\) is an equivalence class of words of length \(n\) under rotational equivalence. For \(n = 0\) there is exactly one necklace over \(A\), represented by the empty word.

Reflections are not identified.

def Necklace (A : Type*) (n : ℕ) :=
  {c : Cycle A // c.length = n}

DefinitionLucas number sequence#✓fully proved

The Lucas numbers \((L_n)_{n \ge 0}\) are the natural numbers defined by \(L_0 = 2\), \(L_1 = 1\), and \(L_{n+2} = L_{n+1} + L_n\) for every \(n \in \mathbb{N}\).

def Nat.lucas : ℕ → ℕ
  | 0 => 2
  | 1 => 1
  | n + 2 => Nat.lucas (n + 1) + Nat.lucas n

DefinitionMotzkin number sequence#✓fully proved

The Motzkin numbers \((M_n)_{n \ge 0}\) are the natural numbers defined by \(M_0 = 1\) and, for every \(n \in \mathbb{N}\), \(M_{n+1} = M_n + \sum_{k=0}^{n-1} M_k M_{n-1-k}\), where the sum is empty when \(n = 0\). Thus \(M_0, M_1, M_2, M_3 = 1, 1, 2, 4\).

def Nat.motzkin : ℕ → ℕ
  | 0 => 1
  | n + 1 =>
    Nat.motzkin n +
      Finset.sum Finset.univ fun k : Fin n =>
        Nat.motzkin k.val *
          Nat.motzkin (n - 1 - k.val)

DefinitionDelannoy numbers#✓fully proved

The Delannoy numbers \(D(m,n)\), for \(m, n \in \mathbb{N}\), are defined by \(D(0,n) = 1\) and \(D(m,0) = 1\) for all \(m, n \in \mathbb{N}\), and \(D(m+1,n+1) = D(m,n+1) + D(m+1,n) + D(m,n)\) for all \(m, n \in \mathbb{N}\).

Equivalently, \(D(m,n)\) is the number of lattice paths from \((0,0)\) to \((m,n)\) with steps \((1,0)\), \((0,1)\) and \((1,1)\).

def Nat.delannoy : ℕ → ℕ → ℕ
  | 0, _ => 1
  | _, 0 => 1
  | m + 1, n + 1 =>
    Nat.delannoy m (n + 1) +
      Nat.delannoy (m + 1) n +
        Nat.delannoy m n
9 fully proved

Southeast paths

DefinitionSoutheast paths#✓fully proved

A point of the quarter plane is a pair \((a, b) \in \mathbb{N}^2\), with \(a\) the horizontal coordinate and \(b\) the height. Let \(p\) and \(q\) be points of the quarter plane. A southeast path from \(p\) to \(q\) is a list \(v = [v_0, v_1, \dots, v_m]\) of points of the quarter plane, for some \(m \in \mathbb{N}\), with \(v_0 = p\), \(v_m = q\), and, for each \(1 \le t \le m\), either \(v_t = v_{t-1} + (1, 0)\) (an east step) or \(v_{t-1} = v_t + (0, 1)\) (a south step).

For \(m = 0\) the path is the single point \([p]\), which is a southeast path from \(p\) to \(q\) exactly when \(p = q\). The empty list is not a southeast path. Writing \(p = (a, b)\) and \(q = (c, d)\), a southeast path from \(p\) to \(q\) exists exactly when \(a \le c\) and \(d \le b\), and then \(m = (c - a) + (b - d)\).

def SoutheastPath (p q : ℕ × ℕ) :=
  { l : List (ℕ × ℕ) //
    l.head? = some p ∧ l.getLast? = some q ∧
    l.IsChain fun a b =>
      b = (a.1 + 1, a.2) ∨ a = (b.1, b.2 + 1) }
Used by 3
Used byNonintersecting families of southeast paths · Weighted sum over nonintersecting path families · Weight of a southeast path

DefinitionWeight of a southeast path#✓fully proved

Let \(R\) be a commutative monoid, written multiplicatively, let \(x = (x_j)_{j \in \mathbb{N}}\) be a family of elements of \(R\), let \(p, q \in \mathbb{N}^2\), and let \(v = [v_0, \dots, v_m]\) be a southeast path from \(p\) to \(q\). For \(1 \le t \le m\), the step from \(v_{t-1}\) to \(v_t\) has weight \(w_t = x_j\) if it is an east step at height \(j\), that is, \(v_{t-1} = (a, j)\) and \(v_t = (a+1, j)\), and weight \(w_t = 1\) if it is a south step. The weight of \(v\) is \(\operatorname{wt}(v) = \prod_{t=1}^{m} w_t\).

For \(m = 0\) the product is empty, so the one-point path \([p]\) has weight \(1\); so does every path all of whose steps are south steps. The weight depends only on the list \(v\).

def SoutheastPath.weight {p q : ℕ × ℕ} {R : Type*}
    [CommMonoid R] (x : ℕ → R)
    (l : SoutheastPath p q) : R :=
  ((l.1.zip l.1.tail).map fun c =>
    if c.2 = (c.1.1 + 1, c.1.2) then x c.1.2 else 1).prod
Uses 1 · Used by 1
Statement usesSoutheast paths
Used byWeighted sum over nonintersecting path families

Nonintersecting path families

DefinitionNonintersecting families of southeast paths#✓fully proved

Let \(n \in \mathbb{N}\) and let \(p_1, \dots, p_n\) and \(q_1, \dots, q_n\) be points of \(\mathbb{N}^2\). A family \(L = (L_1, \dots, L_n)\), in which \(L_i\) is a southeast path from \(p_i\) to \(q_i\) for each \(i\), is nonintersecting when for all \(i \ne j\) no point occurs both in \(L_i\) and in \(L_j\).

Endpoints count as points of a path, so two paths that meet only at a common endpoint do not form a nonintersecting family. Distinctness is of indices, not of paths: if \(i \ne j\) and \(L_i = L_j\), the family is not nonintersecting. For \(n \le 1\) every family is nonintersecting.

def IsNonintersectingPathFamily {n : ℕ}
    {p q : Fin n → ℕ × ℕ}
    (L : (i : Fin n) → SoutheastPath (p i) (q i)) :
    Prop :=
  Pairwise fun i j => ∀ v ∈ (L i).1, v ∉ (L j).1
Uses 1 · Used by 1
Statement usesSoutheast paths
Used byWeighted sum over nonintersecting path families

Weighted sums over nonintersecting families

DefinitionWeighted sum over nonintersecting path families#✓fully proved

Let \(R\) be a commutative semiring, let \(x = (x_j)_{j \in \mathbb{N}}\) be a family of elements of \(R\), let \(n \in \mathbb{N}\), and let \(p = (p_1, \dots, p_n)\) and \(q = (q_1, \dots, q_n)\) be tuples of points of \(\mathbb{N}^2\). The nonintersecting path weight sum of type \((p, q)\) is \(W(p, q) = \sum_L \prod_{i=1}^{n} \operatorname{wt}(L_i)\), the sum taken over all nonintersecting families \(L = (L_1, \dots, L_n)\) in which \(L_i\) is a southeast path from \(p_i\) to \(q_i\) for each \(i\), where \(\operatorname{wt}(L_i)\) is the weight of \(L_i\) with respect to \(x\).

There are only finitely many such families. If for some \(i\) there is no southeast path from \(p_i\) to \(q_i\), then \(W(p, q) = 0\). For \(n = 0\) the empty family is the only one, and \(W(p, q) = 1\).

noncomputable def nonintersectingPathWeightSum {n : ℕ}
    {R : Type*} [CommSemiring R] (x : ℕ → R)
    (p q : Fin n → ℕ × ℕ) : R :=
  ∑ᶠ L : {L : (i : Fin n) → SoutheastPath (p i) (q i) //
      IsNonintersectingPathFamily L},
    ∏ i, (L.1 i).weight x
Uses 3
Statement usesNonintersecting families of southeast paths · Southeast paths · Weight of a southeast path

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.