Compositions avoiding parts 2, 3 and 4

DefinitionOctagonal pyramidal numbers#✓fully proved

For a natural number \(k\), the \(k\)-th octagonal pyramidal number is \(k(k+1)(2k-1)/2\).

def octagonalPyramidalNumber (k : ℕ) : ℕ :=
  k * (k + 1) * (2 * k - 1) / 2
Used by 1

DefinitionCompositions avoiding parts 2, 3 and 4#✓fully proved

For a natural number \(k\), the restricted compositions of \(k + 14\) are the ordered compositions of \(k + 14\) into \(k\) positive parts with no part equal to \(2\), \(3\) or \(4\), that is, the tuples \((c_1, \dots, c_k)\) of positive integers with \(c_1 + \dots + c_k = k + 14\) and \(c_i \notin \{2, 3, 4\}\) for every \(i\).

def octagonalPyramidalCompositions (k : ℕ) : Finset (Fin k → ℕ) :=
  (Fintype.piFinset fun _ : Fin k => Finset.Icc 1 (k + 14) \ {2, 3, 4}).filter
    fun c => ∑ i, c i = k + 14
Used by 1

TheoremOctagonal pyramidal numbers count restricted compositions#✓fully proved

For every positive integer \(k\), the number of ordered compositions of \(k + 14\) into \(k\) positive parts with no part equal to \(2\), \(3\) or \(4\) is the \(k\)-th octagonal pyramidal number \(k(k+1)(2k-1)/2\).

theorem octagonalPyramidalNumber_eq_composition_card (k : ℕ) (hk : 0 < k) :
    (octagonalPyramidalCompositions k).card = octagonalPyramidalNumber k
Sources
  • Milan Janjić, Binomial Coefficients and Enumeration of Restricted Words, Journal of Integer Sequences 19 (2016), Article 16.7.3, the corollary.
Uses 2
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.