Fuss–Catalan numbers

TheoremIntegrality of the Fuss–Catalan numbers#✓fully proved

For natural numbers \(a \ge 2\) and \(n \ge 1\), the integer \((a-1)n + 1\) divides the binomial coefficient \(\binom{an}{n}\). Hence the Fuss–Catalan number \(\frac{1}{(a-1)n+1}\binom{an}{n}\) is an integer.

theorem fuss_catalan_dvd_choose
    (a n : ℕ) (ha : 2 ≤ a) (hn : 1 ≤ n) :
    (a - 1) * n + 1 ∣ Nat.choose (a * n) n
Sources
  • Christian Ballot, "Lucasnomial Fuss-Catalan Numbers and Related Divisibility Questions," Journal of Integer Sequences 21 (2018), Article 18.6.5, equation, lines 115–117 (classical definition), line 127 (classical integrality recorded as known), Theorem, lines 516–521 (Lucasnomial generalization), https://cs.uwaterloo.ca/journals/JIS/VOL21/Ballot/ballot30.tex
Used by 1
Used byPrime divisibility of generalized Catalan numbers

DefinitionFuss–Catalan numbers#✓fully proved

For natural numbers \(k \ge 1\) (the chord arity) and \(m\), the Fuss–Catalan number is the natural-number quotient of \(\binom{km}{m}\) by \((k-1)m+1\), that is \(\lfloor \binom{km}{m} / ((k-1)m+1) \rfloor\).

public def fussCatalanNumber (k m : ℕ) (_hk : 1 ≤ k) : ℕ :=
  Nat.choose (k * m) m / ((k - 1) * m + 1)
Sources

TheoremPrime divisibility of generalized Catalan numbers#✓fully proved

Let \(p\) be a prime and \(n\) a natural number. Then \(p\) divides the generalized Catalan number \(\frac{1}{(p-1)n+1}\binom{pn}{n}\) (an integer) if and only if \(n\) is not of the form \(\frac{p^k-1}{p-1}\) for any natural number \(k\).

The source theorem's "in particular" Mersenne-index clause is already recorded as catalan_odd_iff; this declaration keeps only the new general-p result.

theorem generalizedCatalan_prime_dvd_iff_not_geometric_sum
    (p n : ℕ) (hp : p.Prime) :
    p ∣ Nat.choose (p * n) n / ((p - 1) * n + 1) ↔
      ∀ k : ℕ, n ≠ (p ^ k - 1) / (p - 1)
Sources
  • B. Sury, "Generalized Catalan Numbers: Linear Recursion and Divisibility," Journal of Integer Sequences 12 (2009), Article 09.7.5, Theorem, lines 154–158, https://cs.uwaterloo.ca/journals/JIS/VOL12/Sury/sury31.tex
Uses 1
Proof usesIntegrality of the Fuss–Catalan numbers

DefinitionGeneralized Fuss–Catalan number#✓fully proved

For natural numbers \(m\), \(n\) and \(k\), the generalized Fuss–Catalan number \(F_m(n, k)\) is the quotient of \(k \binom{mn + k}{n}\) by \(mn + k\) in natural-number division, rounded down, with division by \(0\) giving \(0\).

The source considers \(m \ge 2\) and \(n, k \ge 1\). The definition is totalized over natural numbers.

def generalizedFussCatalanNumber (m n k : ℕ) : ℕ :=
  k * Nat.choose (m * n + k) n / (m * n + k)
Used by 7
Used byToeplitz–Hessenberg determinants of Fuss–Catalan numbers · Special Toeplitz–Hessenberg determinants of Fuss–Catalan numbers · Toeplitz–Hessenberg determinants of ternary Fuss–Catalan numbers · Small generalized Fuss–Catalan numbers · Trudi multi-sums of Fuss–Catalan numbers · Formula for the generalized Fuss–Catalan number · Generalized Fuss–Catalan numbers at \(n = 1\)

TheoremFormula for the generalized Fuss–Catalan number#✓fully proved

For all natural numbers \(m\), \(n\) and \(k\), the generalized Fuss–Catalan number \(F_m(n, k)\) equals the quotient of \(k \binom{mn + k}{n}\) by \(mn + k\) in natural-number division, rounded down, with division by \(0\) giving \(0\).

theorem generalizedFussCatalanNumber_eq (m n k : ℕ) :
    generalizedFussCatalanNumber m n k =
      k * Nat.choose (m * n + k) n / (m * n + k)
Uses 1
Statement usesGeneralized Fuss–Catalan number

TheoremGeneralized Fuss–Catalan numbers at \(n = 1\)#✓fully proved

For all natural numbers \(m\) and \(k\), the generalized Fuss–Catalan number \(F_m(1, k)\) equals \(k\).

theorem generalizedFussCatalanNumber_one (m k : ℕ) :
    generalizedFussCatalanNumber m 1 k = k
Sources
Uses 1
Statement usesGeneralized Fuss–Catalan number
6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.