Sum of Stirling numbers of the first kind

Using Pólya's enumeration theorem, we prove a formula for the sum of the Stirling numbers of the first kind multiplied by powers of a natural number.

For additional information, refer to https://en.wikipedia.org/wiki/Stirling_numbers_of_the_first_kind.

@[reducible, inline]

abbrev StirlingFirstKindSum.stirlingFirstKind (n i : ℕ) : ℕ

The Stirling number of the first kind stirlingFirstKind n i represents the number of permutations of Fin n with exactly i cycles.

Equations

• StirlingFirstKindSum.stirlingFirstKind n i = CyclesOfGroupElements.numGroupOfNumCycles (Fin n) (Equiv.Perm (Fin n)) i

theorem StirlingFirstKindSum.sum_stirlingFirstKind_mul_pow_eq_choose_mul_factorial {n m : ℕ} : ∑ i : Fin (n + 1), StirlingFirstKindSum.stirlingFirstKind n ↑i * (m + 1) ^ ↑i = (n + m).choose m * n.factorial

Formula for the sum of Stirling numbers of the first kind multiplied by powers of a positive natural number. The sum of (stirlingFirstKind n i) * (m + 1)ⁱ over i ∈ {0, ..., n} is equal to ((n + m).choose m) * n!.

theorem StirlingFirstKindSum.sum_stirlingFirstKind_of_succ_mul_zero_pow_eq_zero {n : ℕ} : ∑ i : Fin (n + 1 + 1), StirlingFirstKindSum.stirlingFirstKind (n + 1) ↑i * 0 ^ ↑i = 0

The sum of (stirlingFirstKind (n + 1) i) * 0ⁱ over i ∈ {0, ..., n + 1} equals 0.

theorem StirlingFirstKindSum.sum_stirlingFirstKind_of_zero_mul_zero_pow_eq_one : ∑ i : Fin 1, StirlingFirstKindSum.stirlingFirstKind 0 ↑i * 0 ^ ↑i = 1

The sum of (stirlingFirstKind 0 i) * 0ⁱ over i ∈ {0} equals 1.