Restricted weighted compositions

DefinitionRestricted weighted composition count#✓fully proved

Let \(R\) be a commutative ring, \(S\) a finite set of natural numbers and \(f \colon \mathbb{N} \to R\) a weight function. For natural numbers \(n\) and \(k\), \(d_{S,f}(n, k)\) is the sum, over all \(k\)-tuples \((\pi_1, \dots, \pi_k)\) of natural numbers with every \(\pi_i \in S\) and \(\pi_1 + \dots + \pi_k = n\), of the weight \(f(\pi_1) \cdots f(\pi_k)\).

Since every part of a composition of \(n\) is at most \(n\), the tuples range over the finite set of maps from \(\{0, \dots, k-1\}\) to \(\{0, \dots, n\}\).

noncomputable def sRestrictedWeightedCompositionCount {R : Type*} [CommRing R]
    (S : Finset ℕ) (f : ℕ → R) (n k : ℕ) : R := by
  classical
  exact ∑ π ∈ Finset.univ.filter
    (fun π : Fin k → Fin (n + 1) => (∀ i, (π i : ℕ) ∈ S) ∧ ∑ i, (π i : ℕ) = n),
      ∏ i, f (π i)

Used by 1

Used byVandermonde convolution for restricted weighted compositions

TheoremVandermonde convolution for restricted weighted compositions#✓fully proved

Let \(R\) be a commutative ring, \(S\) a finite set of natural numbers and \(f \colon \mathbb{N} \to R\) a weight function, and write \(d_{S,f}(n, k)\) for the weighted count of \(S\)-restricted \(f\)-weighted compositions of \(n\) with \(k\) parts. Then for all natural numbers \(n\), \(k\) and \(j\) with \(j \le k\),

\[d_{S,f}(n, k) = \sum_{m=0}^{n} d_{S,f}(m, j) \, d_{S,f}(n - m, k - j).\]

public theorem vandermondeTypeConvolutionForSRestrictedWeightedCompositions
    {R : Type*} [CommRing R]
    (S : Finset ℕ) (f : ℕ → R) (n k j : ℕ) (hj : j ≤ k) :
    sRestrictedWeightedCompositionCount S f n k =
      ∑ m ∈ Finset.range (n + 1),
        sRestrictedWeightedCompositionCount S f m j *
          sRestrictedWeightedCompositionCount S f (n - m) (k - j)

Uses 1

Statement usesRestricted weighted composition count

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.