Theory Discrete_Summation.Factorials

```
(* Authors: Amine Chaieb & Florian Haftmann, TU Muenchen with contributions by Lukas Bulwahn *)

section ‹Falling factorials›

theory Factorials
imports Complex_Main "HOL-Combinatorics.Stirling"
begin

lemma pochhammer_0 [simp]: ― ‹TODO move›
"pochhammer 0 n = (0::nat)" if "n > 0"
using that by (simp add: pochhammer_prod)

definition ffact :: "nat ⇒ 'a::comm_semiring_1_cancel ⇒ 'a"
where "ffact n a = pochhammer (a + 1 - of_nat n) n"

lemma ffact_0 [simp]:
"ffact 0 = (λx. 1)"

lemma ffact_Suc:
"ffact (Suc n) a = a * ffact n (a - 1)"
for a :: "'a :: comm_ring_1"
by (simp add: ffact_def pochhammer_prod prod.atLeast0_lessThan_Suc algebra_simps)

(* TODO: what's the right class here? *)
lemma ffact_Suc_rev:
"ffact (Suc n) m = (m - of_nat n) * ffact n m"
for m :: "'a :: {comm_semiring_1_cancel, ab_group_add}"

lemma ffact_nat_triv:
"ffact n m = 0" if "m < n"
using that by (simp add: ffact_def)

lemma ffact_Suc_nat:
"ffact (Suc n) m = m * ffact n (m - 1)"
for m :: nat
proof (cases "n ≤ m")
case True
then show ?thesis
by (simp add: ffact_def pochhammer_prod algebra_simps prod.atLeast0_lessThan_Suc)
next
case False
then have "m < n"
by simp
then show ?thesis
qed

lemma ffact_Suc_rev_nat:
"ffact (Suc n) m = (m - n) * ffact n m"
proof (cases "n ≤ m")
case True
then show ?thesis
by (simp add: ffact_def pochhammer_rec Suc_diff_le)
next
case False
then have "m < n" by simp
then show ?thesis by (simp add: ffact_nat_triv)
qed

lemma fact_div_fact_ffact:
"fact n div fact m = ffact (n - m) n" if "m ≤ n"
proof -
from that have "fact n = ffact (n - m) n * fact m"
by (simp add: ffact_def pochhammer_product pochhammer_fact)
moreover have "fact m dvd (fact n :: nat)"
using that by (rule fact_dvd)
ultimately show ?thesis
by simp
qed

lemma fact_div_fact_ffact_nat:
"fact n div fact (n - k) = ffact k n" if "k ≤ n"
using that by (simp add: fact_div_fact_ffact)

lemma ffact_fact:
"ffact n (of_nat n) = (of_nat (fact n) :: 'a :: comm_ring_1)"
by (induct n) (simp_all add: algebra_simps ffact_Suc)

"(a - of_nat n) * ffact n a + of_nat n * ffact n a = a * ffact n a"
for a :: "'a :: comm_ring_1"

lemma mult_ffact:
"a * ffact n a = ffact (Suc n) a + of_nat n * ffact n a"
for a :: "'a :: comm_ring_1"
proof -
have "ffact (Suc n) a + of_nat n * (ffact n a) = (a - of_nat n) * (ffact n a) + of_nat n * (ffact n a)"
using ffact_Suc_rev [of n] by auto
also have "… = a * ffact n a" using ffact_add_diff_assoc by (simp add: algebra_simps)
finally show ?thesis by simp
qed

(* TODO: what's the right class here? *)
lemma prod_ffact:
fixes m :: "'a :: {ord, ring_1, comm_monoid_mult, comm_semiring_1_cancel}"
shows "(∏i = 0..<n. m - of_nat i) = ffact n m"
proof -
have "inj_on (λj. j - 1) {1..n}"
by (force intro: inj_on_diff_nat)
moreover have "{0..<n} = (λj. j - 1) ` {1..n}"
proof -
have "i ∈ (λj. j - 1) ` {1..n}" if "i ∈ {0..<n}" for i
using that by (auto intro: image_eqI[where x="i + 1"])
from this show ?thesis by auto
qed
moreover have "m - of_nat (i - 1) = m + 1 - of_nat n + of_nat (n - i)" if "i ∈ {1..n}" for i
using that by (simp add: of_nat_diff)
ultimately have "(∏i = 0..<n. m - of_nat i) = (∏i = 1..n. m + 1 - of_nat n + of_nat (n - i))"
by (rule prod.reindex_cong)
from this show ?thesis
unfolding ffact_def by (simp only: pochhammer_prod_rev)
qed

lemma prod_ffact_nat:
fixes m :: nat
shows "(∏i = 0..<n. m - i) = ffact n m"
proof cases
assume "n ≤ m"
have "inj_on (λj. j - 1) {1..n}" by (force intro: inj_on_diff_nat)
moreover have "{0..<n} = (λj. j - 1) ` {1..n}"
proof -
have "i ∈ (λj. j - 1) ` {1..n}" if "i ∈ {0..<n}" for i
using that by (auto intro: image_eqI[where x="i + 1"])
from this show ?thesis by auto
qed
ultimately have "(∏i = 0..<n. m - i) = (∏i = 1..n. (m + 1) - i)"
by (auto intro: prod.reindex_cong[where l="λi. i - 1"])
from this ‹n ≤ m› show ?thesis
unfolding ffact_def by (simp add: pochhammer_prod_rev)
next
assume "¬ n ≤ m"
from this show ?thesis by (auto simp add: ffact_nat_triv)
qed

(* TODO: what's the right class here? *)
lemma prod_rev_ffact:
fixes m :: "'a :: {ord, ring_1, comm_monoid_mult, comm_semiring_1_cancel}"
shows "(∏i = 1..n. m - of_nat n + of_nat i) = ffact n m"
proof -
have "inj_on (λi. i + 1) {0..<n}" by simp
moreover have "{1..n} = (λi. i + 1) ` {0..<n}" by auto
moreover have "m - of_nat n + of_nat (i + 1) = m + 1 - of_nat n + of_nat i" for i by simp
ultimately have "(∏i = 1..n. m - of_nat n + of_nat i) = (∏i = 0..<n. m + 1 - of_nat n + of_nat i)"
by (rule prod.reindex_cong[where l="λi. i + 1"])
from this show ?thesis
unfolding ffact_def by (simp only: pochhammer_prod)
qed

lemma prod_rev_ffact_nat:
fixes m :: nat
assumes "n ≤ m"
shows "(∏i = 1..n. m - n + i) = ffact n m"
proof -
have "inj_on (λi. i + 1) {0..<n}" by simp
moreover have "{1..n} = (λi. i + 1) ` {0..<n}" by auto
moreover have "m - n + (i + 1) = m + 1 - n + i" for i
using  ‹n ≤ m› by auto
ultimately have "(∏i = 1..n. m - n + i) = (∏i = 0..<n. m + 1 - n + i)"
by (rule prod.reindex_cong)
from this show ?thesis
unfolding ffact_def by (simp only: pochhammer_prod of_nat_id)
qed

lemma prod_rev_ffact_nat':
fixes m :: nat
assumes "n ≤ m"
shows "∏{m - n + 1..m} = ffact n m"
proof -
have "inj_on (λi. m - n + i) {1::nat..n}" by (auto intro: inj_onI)
moreover have "{m - n + 1..m} = (λi. m - n + i) ` {1::nat..n}"
proof -
have "i ∈ (λi. m + i - n) ` {Suc 0..n}" if "i ∈ {m - n + 1..m}" for i
using that ‹n ≤ m› by (auto intro!: image_eqI[where x="i - (m - n)"])
with ‹n ≤ m› show ?thesis by auto
qed
moreover have "m - n + i = m - n + i" for i ..
ultimately have "∏{m - n + (1::nat)..m} = (∏i = 1..n. m - n + i)"
by (rule prod.reindex_cong)
from this show ?thesis
using ‹n ≤ m› by (simp only: prod_rev_ffact_nat)
qed

lemma ffact_eq_fact_mult_binomial:
"ffact k n = fact k * (n choose k)"
proof cases
assume "k ≤ n"
have "ffact k n = fact n div fact (n - k)"
using ‹k ≤ n› by (simp add: fact_div_fact_ffact_nat)
also have "… = fact k * (n choose k)"
using ‹k ≤ n› by (simp add: binomial_fact_lemma[symmetric])
finally show ?thesis .
next
assume "¬ k ≤ n"
from this ffact_nat_triv show ?thesis by force
qed

lemma of_nat_ffact:
"of_nat (ffact n m) = ffact n (of_nat m :: 'a :: comm_ring_1)"
proof (induct n arbitrary: m)
case 0
then show ?case
by simp
next
case (Suc n)
show ?case
proof (cases m)
case 0
then show ?thesis
next
case (Suc m)
with Suc.hyps show ?thesis
by (simp add: algebra_simps ffact_Suc_nat ffact_Suc)
qed
qed

lemma of_int_ffact:
"of_int (ffact n k) = ffact n (of_int k :: 'a :: comm_ring_1)"
proof (induct n arbitrary: k)
case 0 then show ?case by simp
next
case (Suc n k)
then have "of_int (ffact n (k - 1)) = ffact n (of_int (k - 1) :: 'a)" .
then show ?case
qed

lemma ffact_minus:
fixes x :: "'a :: comm_ring_1"
shows "ffact n (- x) = (- 1) ^ n * pochhammer x n"
proof -
have "ffact n (- x) = pochhammer (- x + 1 - of_nat n) n"
unfolding ffact_def ..
also have "… = pochhammer (- x - of_nat n + 1) n"
also have "… = (- 1) ^ n * pochhammer (- (- x)) n"
by (rule pochhammer_minus')
also have "… = (- 1) ^ n * pochhammer x n" by simp
finally show ?thesis .
qed

text ‹Conversion of natural potences into falling factorials and back›

lemma monomial_ffact:
"a ^ n = (∑k = 0..n. of_nat (Stirling n k) * ffact k a)"
for a :: "'a :: comm_ring_1"
proof (induct n)
case 0 then show ?case by simp
next
case (Suc n)
then have "a ^ Suc n = a * (∑k = 0..n. of_nat (Stirling n k) * ffact k a)"
by simp
also have "… = (∑k = 0..n. of_nat (Stirling n k) * (a * ffact k a))"
also have "… = (∑k = 0..n. of_nat (Stirling n k) * ffact (Suc k) a) +
(∑k = 0..n. of_nat (Stirling n k) * (of_nat k * ffact k a))"
by (simp add: sum.distrib algebra_simps mult_ffact)
also have "… = (∑k = 0.. Suc n. of_nat (Stirling n k) * ffact (Suc k) a) +
(∑k = 0..Suc n. of_nat ((Suc k) * (Stirling n (Suc k))) * (ffact (Suc k) a))"
proof -
have "(∑k = 0..n. of_nat (Stirling n k) * (of_nat k * ffact k a)) =
(∑k = 0..n+2. of_nat (Stirling n k) * (of_nat k * ffact k a))" by simp
also have "… = (∑k = Suc 0 .. Suc (Suc n). of_nat (Stirling n k) * (of_nat k * ffact k a)) "
by (simp only: sum.atLeast_Suc_atMost [of 0 "n + 2"]) simp
also have "… = (∑k = 0 .. Suc n. of_nat (Stirling n (Suc k)) * (of_nat (Suc k) * ffact (Suc k) a))"
by (simp only: image_Suc_atLeastAtMost sum.shift_bounds_cl_Suc_ivl)
also have "… = (∑k = 0 .. Suc n. of_nat ((Suc k) * Stirling n (Suc k)) * ffact (Suc k) a)"
by (simp only: of_nat_mult algebra_simps)
finally have "(∑k = 0..n. of_nat (Stirling n k) * (of_nat k * ffact k a)) =
(∑k = 0..Suc n. of_nat (Suc k * Stirling n (Suc k)) * ffact (Suc k) a)"
by simp
then show ?thesis by simp
qed
also have "… = (∑k = 0..n. of_nat (Stirling (Suc n) (Suc k)) * ffact (Suc k) a)"
also have "… = (∑k = Suc 0..Suc n. of_nat (Stirling (Suc n) k) * ffact k a)"
by (simp only: image_Suc_atLeastAtMost sum.shift_bounds_cl_Suc_ivl)
also have "… = (∑k = 0..Suc n. of_nat (Stirling (Suc n) k) * ffact k a)"
by (simp only: sum.atLeast_Suc_atMost [of "0" "Suc n"]) simp
finally show ?case by simp
qed

lemma ffact_monomial:
"ffact n a = (∑k = 0..n. (- 1) ^ (n - k) * of_nat (stirling n k) * a ^ k)"
for a :: "'a :: comm_ring_1"
proof (induct n)
case 0 show ?case by simp
next
case (Suc n)
then have "ffact (Suc n) a = (a - of_nat n) * (∑k = 0..n. (- 1) ^ (n - k) * of_nat (stirling n k) * a ^ k)"
also have "… = (∑k = 0..n. (- 1) ^ (n - k) * of_nat (stirling n k) * a ^ (Suc k)) +
(∑k = 0..n. (- 1) * (- 1) ^ (n - k) * of_nat (n * (stirling n k)) * a ^ k)"
also have "… = (∑k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (stirling n k) * a ^ Suc k) +
(∑k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (n * stirling n (Suc k)) * a ^ Suc k)"
proof -
have "(∑k = 0..n. (- 1) * (- 1) ^ (n - k) * of_nat (n * stirling n k) * a ^ k) =
(∑k = 0..n. (- 1) ^ (Suc n - k) * of_nat (n * stirling n k) * a ^ k)"
also have "… = (∑k = Suc 0..Suc n. (- 1) ^ (Suc n - k) * of_nat (n * stirling n k) * a ^ k)"
by (simp add: sum.atLeast_Suc_atMost) (cases n; simp)
also have "… = (∑k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (n * stirling n (Suc k)) * a ^ Suc k)"
by (simp only: sum.shift_bounds_cl_Suc_ivl)
finally show ?thesis by simp
qed
also have "… = (∑k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (n * stirling n (Suc k) + stirling n k) * a ^ Suc k)"