Theory Falling_Factorial_Sum_Vandermonde

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Proving Falling Factorial of a Sum with Vandermonde Identity›

theory Falling_Factorial_Sum_Vandermonde
imports
  "Discrete_Summation.Factorials"
begin

text ‹Note the potentially special copyright license condition of the following proof.›

lemma ffact_add_nat:
  shows "ffact k (n + m) = (∑i≤k. (k choose i) * ffact i n * ffact (k - i) m)"
proof -
  have "ffact k (n + m) = fact k * ((n + m) choose k)"
    by (simp only: ffact_eq_fact_mult_binomial)
  also have "… = fact k * (∑i≤k. (n choose i) * (m choose (k - i)))"
    by (simp only: vandermonde)
  also have "… = (∑i≤k. fact k * (n choose i) * (m choose (k - i)))"
    by (simp add: sum_distrib_left field_simps)
  also have "… = (∑i≤k. (fact i * fact (k - i) * (k choose i)) * (n choose i) * (m choose (k - i)))"
    by (simp add: binomial_fact_lemma)
  also have "… = (∑i≤k. (k choose i) * (fact i * (n choose i)) * (fact (k - i) * (m choose (k - i))))"
    by (auto intro: sum.cong)
  also have "… = (∑i≤k. (k choose i) * ffact i n * ffact (k - i) m)"
    by (simp only: ffact_eq_fact_mult_binomial)
  finally show ?thesis .
qed

end