Narayana numbers and polynomials

DefinitionNarayana number#✓fully proved

For positive integers \(n\) and \(k\), the Narayana number \(N(n, k)\) is the natural number \(\lfloor \binom{n}{k}\binom{n}{k-1} / n \rfloor\).

def narayana (n k : {n : ℕ // 0 < n}) : ℕ :=
  (Nat.choose n.val k.val * Nat.choose n.val (k.val - 1)) / n.val

Used by 4

Used byDefining formula for the Narayana number · Second formula for the Narayana number · Narayana polynomial coefficients · Narayana polynomial coefficients at positive indices

TheoremDefining formula for the Narayana number#✓fully proved

For positive integers \(n\) and \(k\), the Narayana number \(N(n, k)\) satisfies \(N(n, k) = \lfloor \binom{n}{k}\binom{n}{k-1} / n \rfloor\).

theorem narayana_eq (n k : {n : ℕ // 0 < n}) :
    narayana n k
      = (Nat.choose n.val k.val * Nat.choose n.val (k.val - 1)) / n.val

Uses 1

Statement usesNarayana number

TheoremSecond formula for the Narayana number#✓fully proved

For positive integers \(n\) and \(k\), the Narayana number \(N(n, k)\) satisfies \(N(n, k) = \lfloor \binom{n-1}{k-1}\binom{n}{k-1} / k \rfloor\).

theorem narayana_eq_second (n k : {n : ℕ // 0 < n}) :
    narayana n k
      = (Nat.choose (n.val - 1) (k.val - 1) * Nat.choose n.val (k.val - 1))
        / k.val

Uses 1

Statement usesNarayana number

DefinitionNarayana polynomial coefficients#✓fully proved

The Narayana polynomial coefficients are the natural numbers \(a(n, k)\), for natural numbers \(n\) and \(k\), given by \(a(0, 0) = 1\), \(a(0, k) = 0\) for \(k \ge 1\), \(a(n, 0) = 0\) for \(n \ge 1\), and \(a(n, k) = N(n, k)\) for \(n, k \ge 1\), where \(N(n, k)\) is the Narayana number. So row zero is \(1\) and every positive row has zero constant term.

def narayanaPolynomialCoeff : ℕ → ℕ → ℕ
  | 0, 0 => 1
  | 0, _ + 1 => 0
  | _ + 1, 0 => 0
  | n + 1, k + 1 => narayana ⟨n + 1, Nat.succ_pos n⟩ ⟨k + 1, Nat.succ_pos k⟩

Uses 1 · Used by 2

Statement usesNarayana number

Used byNarayana polynomials · Narayana polynomial coefficients at positive indices

TheoremNarayana polynomial coefficients at positive indices#✓fully proved

For all natural numbers \(n\) and \(k\), the Narayana polynomial coefficient in row \(n + 1\) and degree \(k + 1\) equals the Narayana number \(N(n + 1, k + 1)\).

This holds by definition.

theorem narayanaPolynomialCoeff_succ_succ (n k : ℕ) :
    narayanaPolynomialCoeff (n + 1) (k + 1) =
      narayana ⟨n + 1, Nat.succ_pos n⟩ ⟨k + 1, Nat.succ_pos k⟩

Uses 2

Statement usesNarayana number · Narayana polynomial coefficients

DefinitionNarayana polynomials#✓fully proved

For a semiring \(R\) and a natural number \(n\), the \(n\)-th Narayana polynomial is

\[N_n(X) = \sum_{k=0}^{n} a(n, k)\, X^k \in R[X],\]

where \(a(n, k)\) is the Narayana polynomial coefficient, taken in \(R\). Since \(a(0, 0) = 1\) and, for \(n \ge 1\), \(a(n, 0) = 0\) and \(a(n, k)\) is the Narayana number \(N(n, k)\) for \(k \ge 1\), the first polynomials are \(N_0 = 1\), \(N_1 = X\), \(N_2 = X^2 + X\) and \(N_3 = X^3 + 3X^2 + X\).

noncomputable def narayanaPolynomial (R : Type*) [Semiring R] (n : ℕ) : Polynomial R :=
  ∑ k ∈ Finset.range (n + 1),
    Polynomial.C (narayanaPolynomialCoeff n k : R) * Polynomial.X ^ k

Uses 1

Statement usesNarayana polynomial coefficients

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.