The Falling Factorial of a Sum

Title:	The Falling Factorial of a Sum
Author:	Lukas Bulwahn (lukas /dot/ bulwahn /at/ gmail /dot/ com)
Submission date:	2017-12-22
Abstract:	This entry shows that the falling factorial of a sum can be computed with an expression using binomial coefficients and the falling factorial of its summands. The entry provides three different proofs: a combinatorial proof, an induction proof and an algebraic proof using the Vandermonde identity. The three formalizations try to follow their informal presentations from a Mathematics Stack Exchange page as close as possible. The induction and algebraic formalization end up to be very close to their informal presentation, whereas the combinatorial proof first requires the introduction of list interleavings, and significant more detail than its informal presentation.
BibTeX:	@article{Falling_Factorial_Sum-AFP, author = {Lukas Bulwahn}, title = {The Falling Factorial of a Sum}, journal = {Archive of Formal Proofs}, month = dec, year = 2017, note = {\url{http://isa-afp.org/entries/Falling_Factorial_Sum.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Card_Partitions, Discrete_Summation
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.