80177
|
1 |
section \<open>More facts about binomial coefficients\<close>
|
|
2 |
|
|
3 |
text \<open>
|
|
4 |
These facts could have been proven before, but having real numbers
|
|
5 |
makes the proofs a lot easier. Thanks to Alexander Maletzky among others.
|
|
6 |
\<close>
|
|
7 |
|
|
8 |
theory Binomial_Plus
|
|
9 |
imports Real
|
|
10 |
begin
|
|
11 |
|
|
12 |
subsection \<open>More facts about binomial coefficients\<close>
|
|
13 |
|
|
14 |
text \<open>
|
|
15 |
These facts could have been proven before, but having real numbers
|
|
16 |
makes the proofs a lot easier.
|
|
17 |
\<close>
|
|
18 |
|
|
19 |
lemma central_binomial_odd:
|
|
20 |
"odd n \<Longrightarrow> n choose (Suc (n div 2)) = n choose (n div 2)"
|
|
21 |
proof -
|
|
22 |
assume "odd n"
|
|
23 |
hence "Suc (n div 2) \<le> n" by presburger
|
|
24 |
hence "n choose (Suc (n div 2)) = n choose (n - Suc (n div 2))"
|
|
25 |
by (rule binomial_symmetric)
|
|
26 |
also from \<open>odd n\<close> have "n - Suc (n div 2) = n div 2" by presburger
|
|
27 |
finally show ?thesis .
|
|
28 |
qed
|
|
29 |
|
|
30 |
lemma binomial_less_binomial_Suc:
|
|
31 |
assumes k: "k < n div 2"
|
|
32 |
shows "n choose k < n choose (Suc k)"
|
|
33 |
proof -
|
|
34 |
from k have k': "k \<le> n" "Suc k \<le> n" by simp_all
|
|
35 |
from k' have "real (n choose k) = fact n / (fact k * fact (n - k))"
|
|
36 |
by (simp add: binomial_fact)
|
|
37 |
also from k' have "n - k = Suc (n - Suc k)" by simp
|
|
38 |
also from k' have "fact \<dots> = (real n - real k) * fact (n - Suc k)"
|
|
39 |
by (subst fact_Suc) (simp_all add: of_nat_diff)
|
|
40 |
also from k have "fact k = fact (Suc k) / (real k + 1)" by (simp add: field_simps)
|
|
41 |
also have "fact n / (fact (Suc k) / (real k + 1) * ((real n - real k) * fact (n - Suc k))) =
|
|
42 |
(n choose (Suc k)) * ((real k + 1) / (real n - real k))"
|
|
43 |
using k by (simp add: field_split_simps binomial_fact)
|
|
44 |
also from assms have "(real k + 1) / (real n - real k) < 1" by simp
|
|
45 |
finally show ?thesis using k by (simp add: mult_less_cancel_left)
|
|
46 |
qed
|
|
47 |
|
|
48 |
lemma binomial_strict_mono:
|
|
49 |
assumes "k < k'" "2*k' \<le> n"
|
|
50 |
shows "n choose k < n choose k'"
|
|
51 |
proof -
|
|
52 |
from assms have "k \<le> k' - 1" by simp
|
|
53 |
thus ?thesis
|
|
54 |
proof (induction rule: inc_induct)
|
|
55 |
case base
|
|
56 |
with assms binomial_less_binomial_Suc[of "k' - 1" n]
|
|
57 |
show ?case by simp
|
|
58 |
next
|
|
59 |
case (step k)
|
|
60 |
from step.prems step.hyps assms have "n choose k < n choose (Suc k)"
|
|
61 |
by (intro binomial_less_binomial_Suc) simp_all
|
|
62 |
also have "\<dots> < n choose k'" by (rule step.IH)
|
|
63 |
finally show ?case .
|
|
64 |
qed
|
|
65 |
qed
|
|
66 |
|
|
67 |
lemma binomial_mono:
|
|
68 |
assumes "k \<le> k'" "2*k' \<le> n"
|
|
69 |
shows "n choose k \<le> n choose k'"
|
|
70 |
using assms binomial_strict_mono[of k k' n] by (cases "k = k'") simp_all
|
|
71 |
|
|
72 |
lemma binomial_strict_antimono:
|
|
73 |
assumes "k < k'" "2 * k \<ge> n" "k' \<le> n"
|
|
74 |
shows "n choose k > n choose k'"
|
|
75 |
proof -
|
|
76 |
from assms have "n choose (n - k) > n choose (n - k')"
|
|
77 |
by (intro binomial_strict_mono) (simp_all add: algebra_simps)
|
|
78 |
with assms show ?thesis by (simp add: binomial_symmetric [symmetric])
|
|
79 |
qed
|
|
80 |
|
|
81 |
lemma binomial_antimono:
|
|
82 |
assumes "k \<le> k'" "k \<ge> n div 2" "k' \<le> n"
|
|
83 |
shows "n choose k \<ge> n choose k'"
|
|
84 |
proof (cases "k = k'")
|
|
85 |
case False
|
|
86 |
note not_eq = False
|
|
87 |
show ?thesis
|
|
88 |
proof (cases "k = n div 2 \<and> odd n")
|
|
89 |
case False
|
|
90 |
with assms(2) have "2*k \<ge> n" by presburger
|
|
91 |
with not_eq assms binomial_strict_antimono[of k k' n]
|
|
92 |
show ?thesis by simp
|
|
93 |
next
|
|
94 |
case True
|
|
95 |
have "n choose k' \<le> n choose (Suc (n div 2))"
|
|
96 |
proof (cases "k' = Suc (n div 2)")
|
|
97 |
case False
|
|
98 |
with assms True not_eq have "Suc (n div 2) < k'" by simp
|
|
99 |
with assms binomial_strict_antimono[of "Suc (n div 2)" k' n] True
|
|
100 |
show ?thesis by auto
|
|
101 |
qed simp_all
|
|
102 |
also from True have "\<dots> = n choose k" by (simp add: central_binomial_odd)
|
|
103 |
finally show ?thesis .
|
|
104 |
qed
|
|
105 |
qed simp_all
|
|
106 |
|
|
107 |
lemma binomial_maximum: "n choose k \<le> n choose (n div 2)"
|
|
108 |
proof -
|
|
109 |
have "k \<le> n div 2 \<longleftrightarrow> 2*k \<le> n" by linarith
|
|
110 |
consider "2*k \<le> n" | "2*k \<ge> n" "k \<le> n" | "k > n" by linarith
|
|
111 |
thus ?thesis
|
|
112 |
proof cases
|
|
113 |
case 1
|
|
114 |
thus ?thesis by (intro binomial_mono) linarith+
|
|
115 |
next
|
|
116 |
case 2
|
|
117 |
thus ?thesis by (intro binomial_antimono) simp_all
|
|
118 |
qed (simp_all add: binomial_eq_0)
|
|
119 |
qed
|
|
120 |
|
|
121 |
lemma binomial_maximum': "(2*n) choose k \<le> (2*n) choose n"
|
|
122 |
using binomial_maximum[of "2*n"] by simp
|
|
123 |
|
|
124 |
lemma central_binomial_lower_bound:
|
|
125 |
assumes "n > 0"
|
|
126 |
shows "4^n / (2*real n) \<le> real ((2*n) choose n)"
|
|
127 |
proof -
|
|
128 |
from binomial[of 1 1 "2*n"]
|
|
129 |
have "4 ^ n = (\<Sum>k\<le>2*n. (2*n) choose k)"
|
|
130 |
by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def)
|
|
131 |
also have "{..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto
|
|
132 |
also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) =
|
|
133 |
(\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
|
|
134 |
by (subst sum.union_disjoint) auto
|
|
135 |
also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)"
|
|
136 |
by (cases n) simp_all
|
|
137 |
also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)"
|
|
138 |
by (intro sum_mono2) auto
|
|
139 |
also have "\<dots> = (2*n) choose n" by (rule choose_square_sum)
|
|
140 |
also have "(\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) \<le> (\<Sum>k\<in>{0<..<2*n}. (2*n) choose n)"
|
|
141 |
by (intro sum_mono binomial_maximum')
|
|
142 |
also have "\<dots> = card {0<..<2*n} * ((2*n) choose n)" by simp
|
|
143 |
also have "card {0<..<2*n} \<le> 2*n - 1" by (cases n) simp_all
|
|
144 |
also have "(2 * n - 1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)"
|
|
145 |
using assms by (simp add: algebra_simps)
|
|
146 |
finally have "4 ^ n \<le> (2 * n choose n) * (2 * n)" by simp_all
|
|
147 |
hence "real (4 ^ n) \<le> real ((2 * n choose n) * (2 * n))"
|
|
148 |
by (subst of_nat_le_iff)
|
|
149 |
with assms show ?thesis by (simp add: field_simps)
|
|
150 |
qed
|
|
151 |
|
|
152 |
lemma upper_le_binomial:
|
|
153 |
assumes "0 < k" and "k < n"
|
|
154 |
shows "n \<le> n choose k"
|
|
155 |
proof -
|
|
156 |
from assms have "1 \<le> n" by simp
|
|
157 |
define k' where "k' = (if n div 2 \<le> k then k else n - k)"
|
|
158 |
from assms have 1: "k' \<le> n - 1" and 2: "n div 2 \<le> k'" by (auto simp: k'_def)
|
|
159 |
from assms(2) have "k \<le> n" by simp
|
|
160 |
have "n choose k = n choose k'" by (simp add: k'_def binomial_symmetric[OF \<open>k \<le> n\<close>])
|
|
161 |
have "n = n choose 1" by (simp only: choose_one)
|
|
162 |
also from \<open>1 \<le> n\<close> have "\<dots> = n choose (n - 1)" by (rule binomial_symmetric)
|
|
163 |
also from 1 2 have "\<dots> \<le> n choose k'" by (rule binomial_antimono) simp
|
|
164 |
also have "\<dots> = n choose k" by (simp add: k'_def binomial_symmetric[OF \<open>k \<le> n\<close>])
|
|
165 |
finally show ?thesis .
|
|
166 |
qed
|
|
167 |
|
|
168 |
subsection \<open>Results about binomials and integers, thanks to Alexander Maletzky\<close>
|
|
169 |
|
|
170 |
text \<open>Restore original sort constraints: semidom rather than field of char 0\<close>
|
|
171 |
setup \<open>Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a"})\<close>
|
|
172 |
|
|
173 |
lemma gbinomial_eq_0_int:
|
|
174 |
assumes "n < k"
|
|
175 |
shows "(int n) gchoose k = 0"
|
|
176 |
by (simp add: assms gbinomial_prod_rev prod_zero)
|
|
177 |
|
|
178 |
corollary gbinomial_eq_0: "0 \<le> a \<Longrightarrow> a < int k \<Longrightarrow> a gchoose k = 0"
|
|
179 |
by (metis nat_eq_iff2 nat_less_iff gbinomial_eq_0_int)
|
|
180 |
|
|
181 |
lemma int_binomial: "int (n choose k) = (int n) gchoose k"
|
|
182 |
proof (cases "k \<le> n")
|
|
183 |
case True
|
|
184 |
from refl have eq: "(\<Prod>i = 0..<k. int (n - i)) = (\<Prod>i = 0..<k. int n - int i)"
|
|
185 |
proof (rule prod.cong)
|
|
186 |
fix i
|
|
187 |
assume "i \<in> {0..<k}"
|
|
188 |
with True show "int (n - i) = int n - int i" by simp
|
|
189 |
qed
|
|
190 |
show ?thesis
|
|
191 |
by (simp add: gbinomial_binomial[symmetric] gbinomial_prod_rev zdiv_int eq)
|
|
192 |
next
|
|
193 |
case False
|
|
194 |
thus ?thesis by (simp add: gbinomial_eq_0_int)
|
|
195 |
qed
|
|
196 |
|
|
197 |
lemma falling_fact_pochhammer: "prod (\<lambda>i. a - int i) {0..<k} = (- 1) ^ k * pochhammer (- a) k"
|
|
198 |
proof -
|
|
199 |
have eq: "z ^ Suc n * prod f {0..n} = prod (\<lambda>x. z * f x) {0..n}" for z::int and n f
|
|
200 |
by (induct n) (simp_all add: ac_simps)
|
|
201 |
show ?thesis
|
|
202 |
proof (cases k)
|
|
203 |
case 0
|
|
204 |
thus ?thesis by (simp add: pochhammer_minus)
|
|
205 |
next
|
|
206 |
case (Suc n)
|
|
207 |
thus ?thesis
|
|
208 |
by (simp only: pochhammer_prod atLeastLessThanSuc_atLeastAtMost
|
|
209 |
prod.atLeast_Suc_atMost_Suc_shift eq flip: power_mult_distrib) (simp add: of_nat_diff)
|
|
210 |
qed
|
|
211 |
qed
|
|
212 |
|
|
213 |
lemma falling_fact_pochhammer': "prod (\<lambda>i. a - int i) {0..<k} = pochhammer (a - int k + 1) k"
|
|
214 |
by (simp add: falling_fact_pochhammer pochhammer_minus')
|
|
215 |
|
|
216 |
lemma gbinomial_int_pochhammer: "(a::int) gchoose k = (- 1) ^ k * pochhammer (- a) k div fact k"
|
|
217 |
by (simp only: gbinomial_prod_rev falling_fact_pochhammer)
|
|
218 |
|
|
219 |
lemma gbinomial_int_pochhammer': "a gchoose k = pochhammer (a - int k + 1) k div fact k"
|
|
220 |
by (simp only: gbinomial_prod_rev falling_fact_pochhammer')
|
|
221 |
|
|
222 |
lemma fact_dvd_pochhammer: "fact k dvd pochhammer (a::int) k"
|
|
223 |
proof -
|
|
224 |
have dvd: "y \<noteq> 0 \<Longrightarrow> ((of_int (x div y))::'a::field_char_0) = of_int x / of_int y \<Longrightarrow> y dvd x"
|
|
225 |
for x y :: int
|
|
226 |
by (smt dvd_triv_left mult.commute nonzero_eq_divide_eq of_int_eq_0_iff of_int_eq_iff of_int_mult)
|
|
227 |
show ?thesis
|
|
228 |
proof (cases "0 < a")
|
|
229 |
case True
|
|
230 |
moreover define n where "n = nat (a - 1) + k"
|
|
231 |
ultimately have a: "a = int n - int k + 1" by simp
|
|
232 |
from fact_nonzero show ?thesis unfolding a
|
|
233 |
proof (rule dvd)
|
|
234 |
have "of_int (pochhammer (int n - int k + 1) k div fact k) = (of_int (int n gchoose k)::rat)"
|
|
235 |
by (simp only: gbinomial_int_pochhammer')
|
|
236 |
also have "\<dots> = of_nat (n choose k)"
|
|
237 |
by (metis int_binomial of_int_of_nat_eq)
|
|
238 |
also have "\<dots> = (of_nat n) gchoose k" by (fact binomial_gbinomial)
|
|
239 |
also have "\<dots> = pochhammer (of_nat n - of_nat k + 1) k / fact k"
|
|
240 |
by (fact gbinomial_pochhammer')
|
|
241 |
also have "\<dots> = pochhammer (of_int (int n - int k + 1)) k / fact k" by simp
|
|
242 |
also have "\<dots> = (of_int (pochhammer (int n - int k + 1) k)) / (of_int (fact k))"
|
|
243 |
by (simp only: of_int_fact pochhammer_of_int)
|
|
244 |
finally show "of_int (pochhammer (int n - int k + 1) k div fact k) =
|
|
245 |
of_int (pochhammer (int n - int k + 1) k) / rat_of_int (fact k)" .
|
|
246 |
qed
|
|
247 |
next
|
|
248 |
case False
|
|
249 |
moreover define n where "n = nat (- a)"
|
|
250 |
ultimately have a: "a = - int n" by simp
|
|
251 |
from fact_nonzero have "fact k dvd (-1)^k * pochhammer (- int n) k"
|
|
252 |
proof (rule dvd)
|
|
253 |
have "of_int ((-1)^k * pochhammer (- int n) k div fact k) = (of_int (int n gchoose k)::rat)"
|
|
254 |
by (metis falling_fact_pochhammer gbinomial_prod_rev)
|
|
255 |
also have "\<dots> = of_int (int (n choose k))" by (simp only: int_binomial)
|
|
256 |
also have "\<dots> = of_nat (n choose k)" by simp
|
|
257 |
also have "\<dots> = (of_nat n) gchoose k" by (fact binomial_gbinomial)
|
|
258 |
also have "\<dots> = (-1)^k * pochhammer (- of_nat n) k / fact k"
|
|
259 |
by (fact gbinomial_pochhammer)
|
|
260 |
also have "\<dots> = (-1)^k * pochhammer (of_int (- int n)) k / fact k" by simp
|
|
261 |
also have "\<dots> = (-1)^k * (of_int (pochhammer (- int n) k)) / (of_int (fact k))"
|
|
262 |
by (simp only: of_int_fact pochhammer_of_int)
|
|
263 |
also have "\<dots> = (of_int ((-1)^k * pochhammer (- int n) k)) / (of_int (fact k))" by simp
|
|
264 |
finally show "of_int ((- 1) ^ k * pochhammer (- int n) k div fact k) =
|
|
265 |
of_int ((- 1) ^ k * pochhammer (- int n) k) / rat_of_int (fact k)" .
|
|
266 |
qed
|
|
267 |
thus ?thesis unfolding a by (metis dvdI dvd_mult_unit_iff' minus_one_mult_self)
|
|
268 |
qed
|
|
269 |
qed
|
|
270 |
|
|
271 |
lemma gbinomial_int_negated_upper: "(a gchoose k) = (-1) ^ k * ((int k - a - 1) gchoose k)"
|
|
272 |
by (simp add: gbinomial_int_pochhammer pochhammer_minus algebra_simps fact_dvd_pochhammer div_mult_swap)
|
|
273 |
|
|
274 |
lemma gbinomial_int_mult_fact: "fact k * (a gchoose k) = (\<Prod>i = 0..<k. a - int i)"
|
|
275 |
by (simp only: gbinomial_int_pochhammer' fact_dvd_pochhammer dvd_mult_div_cancel falling_fact_pochhammer')
|
|
276 |
|
|
277 |
corollary gbinomial_int_mult_fact': "(a gchoose k) * fact k = (\<Prod>i = 0..<k. a - int i)"
|
|
278 |
using gbinomial_int_mult_fact[of k a] by (simp add: ac_simps)
|
|
279 |
|
|
280 |
lemma gbinomial_int_binomial:
|
|
281 |
"a gchoose k = (if 0 \<le> a then int ((nat a) choose k) else (-1::int)^k * int ((k + (nat (- a)) - 1) choose k))"
|
|
282 |
by (auto simp: int_binomial gbinomial_int_negated_upper[of a] int_ops(6))
|
|
283 |
|
|
284 |
corollary gbinomial_nneg: "0 \<le> a \<Longrightarrow> a gchoose k = int ((nat a) choose k)"
|
|
285 |
by (simp add: gbinomial_int_binomial)
|
|
286 |
|
|
287 |
corollary gbinomial_neg: "a < 0 \<Longrightarrow> a gchoose k = (-1::int)^k * int ((k + (nat (- a)) - 1) choose k)"
|
|
288 |
by (simp add: gbinomial_int_binomial)
|
|
289 |
|
|
290 |
lemma of_int_gbinomial: "of_int (a gchoose k) = (of_int a :: 'a::field_char_0) gchoose k"
|
|
291 |
proof -
|
|
292 |
have of_int_div: "y dvd x \<Longrightarrow> of_int (x div y) = of_int x / (of_int y :: 'a)" for x y :: int by auto
|
|
293 |
show ?thesis
|
|
294 |
by (simp add: gbinomial_int_pochhammer' gbinomial_pochhammer' of_int_div fact_dvd_pochhammer
|
|
295 |
pochhammer_of_int[symmetric])
|
|
296 |
qed
|
|
297 |
|
|
298 |
lemma uminus_one_gbinomial [simp]: "(- 1::int) gchoose k = (- 1) ^ k"
|
|
299 |
by (simp add: gbinomial_int_binomial)
|
|
300 |
|
|
301 |
lemma gbinomial_int_Suc_Suc: "(x + 1::int) gchoose (Suc k) = (x gchoose k) + (x gchoose (Suc k))"
|
|
302 |
proof (rule linorder_cases)
|
|
303 |
assume 1: "x + 1 < 0"
|
|
304 |
hence 2: "x < 0" by simp
|
|
305 |
then obtain n where 3: "nat (- x) = Suc n" using not0_implies_Suc by fastforce
|
|
306 |
hence 4: "nat (- x - 1) = n" by simp
|
|
307 |
show ?thesis
|
|
308 |
proof (cases k)
|
|
309 |
case 0
|
|
310 |
show ?thesis by (simp add: \<open>k = 0\<close>)
|
|
311 |
next
|
|
312 |
case (Suc k')
|
|
313 |
from 1 2 3 4 show ?thesis by (simp add: \<open>k = Suc k'\<close> gbinomial_int_binomial int_distrib(2))
|
|
314 |
qed
|
|
315 |
next
|
|
316 |
assume "x + 1 = 0"
|
|
317 |
hence "x = - 1" by simp
|
|
318 |
thus ?thesis by simp
|
|
319 |
next
|
|
320 |
assume "0 < x + 1"
|
|
321 |
hence "0 \<le> x + 1" and "0 \<le> x" and "nat (x + 1) = Suc (nat x)" by simp_all
|
|
322 |
thus ?thesis by (simp add: gbinomial_int_binomial)
|
|
323 |
qed
|
|
324 |
|
|
325 |
corollary plus_Suc_gbinomial:
|
|
326 |
"(x + (1 + int k)) gchoose (Suc k) = ((x + int k) gchoose k) + ((x + int k) gchoose (Suc k))"
|
|
327 |
(is "?l = ?r")
|
|
328 |
proof -
|
|
329 |
have "?l = (x + int k + 1) gchoose (Suc k)" by (simp only: ac_simps)
|
|
330 |
also have "\<dots> = ?r" by (fact gbinomial_int_Suc_Suc)
|
|
331 |
finally show ?thesis .
|
|
332 |
qed
|
|
333 |
|
|
334 |
lemma gbinomial_int_n_n [simp]: "(int n) gchoose n = 1"
|
|
335 |
proof (induct n)
|
|
336 |
case 0
|
|
337 |
show ?case by simp
|
|
338 |
next
|
|
339 |
case (Suc n)
|
|
340 |
have "int (Suc n) gchoose Suc n = (int n + 1) gchoose Suc n" by (simp add: add.commute)
|
|
341 |
also have "\<dots> = (int n gchoose n) + (int n gchoose (Suc n))" by (fact gbinomial_int_Suc_Suc)
|
|
342 |
finally show ?case by (simp add: Suc gbinomial_eq_0)
|
|
343 |
qed
|
|
344 |
|
|
345 |
lemma gbinomial_int_Suc_n [simp]: "(1 + int n) gchoose n = 1 + int n"
|
|
346 |
proof (induct n)
|
|
347 |
case 0
|
|
348 |
show ?case by simp
|
|
349 |
next
|
|
350 |
case (Suc n)
|
|
351 |
have "1 + int (Suc n) gchoose Suc n = (1 + int n) + 1 gchoose Suc n" by simp
|
|
352 |
also have "\<dots> = (1 + int n gchoose n) + (1 + int n gchoose (Suc n))" by (fact gbinomial_int_Suc_Suc)
|
|
353 |
also have "\<dots> = 1 + int n + (int (Suc n) gchoose (Suc n))" by (simp add: Suc)
|
|
354 |
also have "\<dots> = 1 + int (Suc n)" by (simp only: gbinomial_int_n_n)
|
|
355 |
finally show ?case .
|
|
356 |
qed
|
|
357 |
|
|
358 |
lemma zbinomial_eq_0_iff [simp]: "a gchoose k = 0 \<longleftrightarrow> (0 \<le> a \<and> a < int k)"
|
|
359 |
proof
|
|
360 |
assume a: "a gchoose k = 0"
|
|
361 |
have 1: "b < int k" if "b gchoose k = 0" for b
|
|
362 |
proof (rule ccontr)
|
|
363 |
assume "\<not> b < int k"
|
|
364 |
hence "0 \<le> b" and "k \<le> nat b" by simp_all
|
|
365 |
from this(1) have "int ((nat b) choose k) = b gchoose k" by (simp add: gbinomial_int_binomial)
|
|
366 |
also have "\<dots> = 0" by (fact that)
|
|
367 |
finally show False using \<open>k \<le> nat b\<close> by simp
|
|
368 |
qed
|
|
369 |
show "0 \<le> a \<and> a < int k"
|
|
370 |
proof
|
|
371 |
show "0 \<le> a"
|
|
372 |
proof (rule ccontr)
|
|
373 |
assume "\<not> 0 \<le> a"
|
|
374 |
hence "(-1) ^ k * ((int k - a - 1) gchoose k) = a gchoose k"
|
|
375 |
by (simp add: gbinomial_int_negated_upper[of a])
|
|
376 |
also have "\<dots> = 0" by (fact a)
|
|
377 |
finally have "(int k - a - 1) gchoose k = 0" by simp
|
|
378 |
hence "int k - a - 1 < int k" by (rule 1)
|
|
379 |
with \<open>\<not> 0 \<le> a\<close> show False by simp
|
|
380 |
qed
|
|
381 |
next
|
|
382 |
from a show "a < int k" by (rule 1)
|
|
383 |
qed
|
|
384 |
qed (auto intro: gbinomial_eq_0)
|
|
385 |
|
|
386 |
subsection \<open>Sums\<close>
|
|
387 |
|
|
388 |
lemma gchoose_rising_sum_nat: "(\<Sum>j\<le>n. int j + int k gchoose k) = (int n + int k + 1) gchoose (Suc k)"
|
|
389 |
proof -
|
|
390 |
have "(\<Sum>j\<le>n. int j + int k gchoose k) = int (\<Sum>j\<le>n. k + j choose k)"
|
|
391 |
by (simp add: int_binomial add.commute)
|
|
392 |
also have "(\<Sum>j\<le>n. k + j choose k) = (k + n + 1) choose (k + 1)" by (fact choose_rising_sum(1))
|
|
393 |
also have "int \<dots> = (int n + int k + 1) gchoose (Suc k)"
|
|
394 |
by (simp add: int_binomial ac_simps del: binomial_Suc_Suc)
|
|
395 |
finally show ?thesis .
|
|
396 |
qed
|
|
397 |
|
|
398 |
lemma gchoose_rising_sum:
|
|
399 |
assumes "0 \<le> n" \<comment>\<open>Necessary condition.\<close>
|
|
400 |
shows "(\<Sum>j=0..n. j + int k gchoose k) = (n + int k + 1) gchoose (Suc k)"
|
|
401 |
proof -
|
|
402 |
from _ refl have "(\<Sum>j=0..n. j + int k gchoose k) = (\<Sum>j\<in>int ` {0..nat n}. j + int k gchoose k)"
|
|
403 |
proof (rule sum.cong)
|
|
404 |
from assms show "{0..n} = int ` {0..nat n}" by (simp add: image_int_atLeastAtMost)
|
|
405 |
qed
|
|
406 |
also have "\<dots> = (\<Sum>j\<le>nat n. int j + int k gchoose k)" by (simp add: sum.reindex atMost_atLeast0)
|
|
407 |
also have "\<dots> = (int (nat n) + int k + 1) gchoose (Suc k)" by (fact gchoose_rising_sum_nat)
|
|
408 |
also from assms have "\<dots> = (n + int k + 1) gchoose (Suc k)" by (simp add: add.assoc add.commute)
|
|
409 |
finally show ?thesis .
|
|
410 |
qed
|
|
411 |
|
|
412 |
end
|