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
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
MathlibExt/Combinatorics/Enumerative/OctagonalPyramidalNumber.lean:40
def octagonalPyramidalNumber (k : ℕ) : ℕ :=
k * (k + 1) * (2 * k - 1) / 2
MathlibExt/Combinatorics/Enumerative/OctagonalPyramidalNumber.lean:31
Sources
- Milan Janjić, Binomial Coefficients and Enumeration of Restricted Words, Journal of Integer Sequences 19 (2016), Article 16.7.3, the corollary.
Uses 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.