Partition-sum expansion of binomial coefficients

TheoremPartition-sum expansion of \(\binom{nm}{l}\), unconditional form#✓fully proved

For all natural numbers \(n\), \(m\) and \(l\), let \(P\) be the set of tuples \(s = (s_1, \dots, s_m)\) of natural numbers with \(\sum_{j=1}^{m} j\,s_j = l\), and for \(s \in P\) write \(T_j(s) = s_{j+1} + \dots + s_m\). Then

\[\binom{nm}{l} = \sum_{s \in P} \prod_{j=1}^{m} \binom{n - T_j(s)}{s_j} \binom{m}{j}^{s_j},\]

where \(n - T_j(s)\) is read as \(0\) when \(T_j(s) > n\). No positivity or range conditions on \(n\), \(m\) and \(l\) are needed.

theorem choose_mul_eq_partition_sum_unconditional
    (n m l : ℕ) :
    Nat.choose (n * m) l =
      ∑ s : {s : Fin m → Fin (l + 1) //
          ∑ k : Fin m, ((k : ℕ) + 1) * (s k : ℕ) = l},
        ∏ k : Fin m,
          Nat.choose
              (n - ∑ i : Fin m, if k < i then (s.1 i : ℕ) else 0)
              (s.1 k : ℕ) *
            Nat.choose m ((k : ℕ) + 1) ^ (s.1 k : ℕ)
Used by 1
Used byPartition-sum expansion of \(\binom{nm}{l}\)

TheoremPartition-sum expansion of \(\binom{nm}{l}\)#✓fully proved

Let \(n\) and \(m\) be positive natural numbers and let \(l\) be a natural number with \(1 \le l \le nm\). Let \(P\) be the set of tuples \(s = (s_1, \dots, s_m)\) of natural numbers with \(\sum_{j=1}^{m} j\,s_j = l\), and for \(s \in P\) write \(T_j(s) = s_{j+1} + \dots + s_m\). Then

\[\binom{nm}{l} = \sum_{s \in P} \prod_{j=1}^{m} \binom{n - T_j(s)}{s_j} \binom{m}{j}^{s_j},\]

where \(n - T_j(s)\) is read as \(0\) when \(T_j(s) > n\).

theorem choose_mul_eq_partition_sum
    (n m l : ℕ) (hn : 0 < n) (hm : 0 < m) (hl : 0 < l)
    (hl_lower : 1 ≤ l) (hl_upper : l ≤ n * m) :
    Nat.choose (n * m) l =
      ∑ s : {s : Fin m → Fin (l + 1) //
          ∑ k : Fin m, ((k : ℕ) + 1) * (s k : ℕ) = l},
        ∏ k : Fin m,
          Nat.choose
              (n - ∑ i : Fin m, if k < i then (s.1 i : ℕ) else 0)
              (s.1 k : ℕ) *
            Nat.choose m ((k : ℕ) + 1) ^ (s.1 k : ℕ)
Sources
Uses 1
Proof usesPartition-sum expansion of \(\binom{nm}{l}\), unconditional form
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.