Integer compositions

Ordered sums of positive integers: compositions with restricted, palindromic, colored or n-color parts, Arndt compositions, perfect compositions, shade, symmetric peaks and valleys, and convolution identities for weighted compositions.

• Arndt compositions
• Colored compositions, Dyck paths and polygon dissections
• Compositions avoiding parts 2, 3 and 4
• Compositions with an odd number of parts
• Compositions with parts 1, 2 and 3
• Even and odd compositions
• Perfect compositions
• Positional colored compositions
• Restricted n-color compositions
• Restricted weighted compositions
• Shade of integer compositions
• Symmetric peaks and valleys in compositions

TheoremMunagi's theorem on restricted compositions#✓fully proved

For positive integers \(n\) and \(k\), the number of compositions of \(n\) all of whose parts are congruent to \(1\) modulo \(k\) equals the number of compositions of \(n + k - 1\) all of whose parts are at least \(k\).

theorem munagi_restricted_compositions
    (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :
    Fintype.card {c : Composition n // ∀ a ∈ c.blocks, a % k = 1 % k} =
      Fintype.card {c : Composition (n + k - 1) // ∀ a ∈ c.blocks, k ≤ a}

Sources

• Jia Huang, "Even and Odd Compositions with Restricted Parts", Journal of Integer Sequences 27 (2024), Article 24.6.5, Theorem thm:comp2 (Munagi), lines 160-162, https://cs.uwaterloo.ca/journals/JIS/VOL27/Huang/huang9.tex.

TheoremPalindromic compositions without 2's#✓fully proved

For an integer \(m \ge 0\), let \(C(m)\) be the number of compositions of \(m\) (finite sequences of positive integers with sum \(m\)) with no part equal to \(2\), so that \(C(0) = 1\) counts the empty composition, and set \(C(m) = 0\) for \(m < 0\). For a natural number \(n\), let \(P(n)\) be the number of such compositions of \(n\) that are palindromes. Then for every natural number \(k\), \(P(2k) = C(k+1)\) and \(P(2k+1) = C(k+1) + C(k-1)\), and the generating function \(G_P(x) = \sum_{n \ge 0} P(n)\, x^n\) satisfies \((1 - x^2 - x^3)\, G_P(x) = 1 + x\) as formal power series with integer coefficients.

The generating-function identity is the source's \(G_P(z) = (1 + z)/(1 - z^2 - z^3)\) cleared of denominators.

theorem palindromic_compositions_without_two :
    let C : ℤ → ℕ := fun m => if 0 ≤ m then
      Set.ncard {c : List ℕ | (∀ a ∈ c, 0 < a ∧ a ≠ 2) ∧ c.sum = m.toNat} else 0
    let P : ℕ → ℕ := fun n => Set.ncard {c : List ℕ |
      (∀ a ∈ c, 0 < a ∧ a ≠ 2) ∧ c.sum = n ∧ c.reverse = c}
    (∀ k : ℕ, P (2 * k) = C ((k : ℤ) + 1)) ∧
      (∀ k : ℕ, P (2 * k + 1) = C ((k : ℤ) + 1) + C ((k : ℤ) - 1)) ∧
      (1 - PowerSeries.X ^ 2 - PowerSeries.X ^ 3) *
          PowerSeries.mk (fun n : ℕ => (P n : ℤ)) = 1 + PowerSeries.X

Sources

• Phyllis Chinn and Silvia Heubach, "Integer Sequences Related to Compositions without 2's," Journal of Integer Sequences 6 (2003), Article 03.2.3, Theorem 10, lines 462–471, https://cs.uwaterloo.ca/journals/JIS/VOL6/Heubach/heubach5.tex.

TheoremRoots-of-unity partial fraction identity#●ready to prove

Let \(\alpha < \beta\) be natural numbers and let \(\zeta = e^{2 \pi i / \beta}\). For every complex number \(u\) with \(1 - u^\beta \ne 0\),

\[\frac{u^\alpha}{1 - u^\beta} = \frac{1}{\beta} \sum_{k=0}^{\beta - 1} \frac{\zeta^{-k \alpha}}{1 - \zeta^k u}.\]

public theorem_wanted pow_div_one_sub_pow_eq_sum (α β : ℕ) (hα : α < β)
    (u : ℂ) (hu : 1 - u ^ β ≠ 0) :
    u ^ α / (1 - u ^ β)
      = (1 / (β : ℂ)) * ∑ k ∈ Finset.range β,
          (Complex.exp (2 * (Real.pi : ℂ) * Complex.I / (β : ℂ)))
              ^ (-((k : ℤ) * (α : ℤ)))
            / (1 - (Complex.exp (2 * (Real.pi : ℂ) * Complex.I / (β : ℂ)))
              ^ k * u)

Sources

• Bowman, Compositions with an Odd Number of Parts, and Other Congruences, Journal of Integer Sequences 27 (2024), Article 24.3.6, Lemma 7 (jis-2024-24.3.6-lem-7).

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.