author chaieb Thu Jul 23 21:12:57 2009 +0200 (2009-07-23) changeset 32160 63686057cbe8 parent 32159 4082bd9824c9 child 32161 abda97d2deea
Vandermonde vs Pochhammer; Hypergeometric series - very basic facts
```     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Jul 23 21:12:57 2009 +0200
1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Thu Jul 23 21:12:57 2009 +0200
1.3 @@ -469,7 +469,6 @@
1.4
1.5  lemma dist_fps_sym: "dist (a::'a fps) b = dist b a"
1.6    apply (auto simp add: dist_fps_def)
1.7 -  thm cong[OF refl]
1.8    apply (rule cong[OF refl, where x="(\<lambda>n\<Colon>nat. a \$ n \<noteq> b \$ n)"])
1.9    apply (rule ext)
1.10    by auto
1.11 @@ -2333,7 +2332,6 @@
1.12
1.13  from a0 have ia0: "?ia \$ 0 \<noteq> 0" by (simp )
1.14  from a0 have ab0: "?ab \$ 0 \<noteq> 0" by (simp add: fps_compose_def)
1.15 -thm inverse_mult_eq_1[OF ab0]
1.16  have "(?ia oo b) *  (a oo b) = 1"
1.17  unfolding fps_compose_mult_distrib[OF b0, symmetric]
1.18  unfolding inverse_mult_eq_1[OF a0]
1.19 @@ -2606,7 +2604,8 @@
1.20  lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
1.22
1.23 -lemma assumes r: "r (Suc k) 1 = 1"
1.25 +  assumes r: "r (Suc k) 1 = 1"
1.26    shows "fps_radical r (Suc k) (E (c::'a::{field_char_0})) = E (c / of_nat (Suc k))"
1.27  proof-
1.28    let ?ck = "(c / of_nat (Suc k))"
1.29 @@ -2802,7 +2801,7 @@
1.30  qed
1.31
1.32  text{* Vandermonde's Identity as a consequence *}
1.33 -lemma gbinomial_Vandermond: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
1.34 +lemma gbinomial_Vandermonde: "setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
1.35  proof-
1.36    let ?ba = "fps_binomial a"
1.37    let ?bb = "fps_binomial b"
1.38 @@ -2811,27 +2810,168 @@
1.39    then show ?thesis by (simp add: fps_mult_nth)
1.40  qed
1.41
1.42 -lemma binomial_Vandermond: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
1.43 -  using gbinomial_Vandermond[of "(of_nat a)" "of_nat b" n]
1.44 +lemma binomial_Vandermonde: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
1.45 +  using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n]
1.46
1.47    apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
1.48    by simp
1.49 -
1.50 -lemma binomial_symmetric: assumes kn: "k \<le> n"
1.51 -  shows "n choose k = n choose (n - k)"
1.52 -proof-
1.53 -  from kn have kn': "n - k \<le> n" by arith
1.54 -  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
1.55 -  have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
1.56 -  then show ?thesis using kn by simp
1.57 -qed
1.58
1.59 -lemma binomial_Vandermond_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
1.60 -  using binomial_Vandermond[of n n n,symmetric]
1.61 +lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)^2) {0..n} = (2*n) choose n"
1.62 +  using binomial_Vandermonde[of n n n,symmetric]
1.63    unfolding nat_mult_2 apply (simp add: power2_eq_square)
1.64    apply (rule setsum_cong2)
1.65    by (auto intro:  binomial_symmetric)
1.66
1.67 +lemma Vandermonde_pochhammer_lemma:
1.68 +  fixes a :: "'a::field_char_0"
1.69 +  assumes b: "\<forall> j\<in>{0 ..<n}. b \<noteq> of_nat j"
1.70 +  shows "setsum (%k. (pochhammer (- a) k * pochhammer (- (of_nat n)) k) / (of_nat (fact k) * pochhammer (b - of_nat n + 1) k)) {0..n} = pochhammer (- (a+ b)) n / pochhammer (- b) n" (is "?l = ?r")
1.71 +proof-
1.72 +  let ?m1 = "%m. (- 1 :: 'a) ^ m"
1.73 +  let ?f = "%m. of_nat (fact m)"
1.74 +  let ?p = "%(x::'a). pochhammer (- x)"
1.75 +  from b have bn0: "?p b n \<noteq> 0" unfolding pochhammer_eq_0_iff by simp
1.76 +  {fix k assume kn: "k \<in> {0..n}"
1.77 +    {assume c:"pochhammer (b - of_nat n + 1) n = 0"
1.78 +      then obtain j where j: "j < n" "b - of_nat n + 1 = - of_nat j"
1.79 +	unfolding pochhammer_eq_0_iff by blast
1.80 +      from j have "b = of_nat n - of_nat j - of_nat 1"
1.81 +	by (simp add: algebra_simps)
1.82 +      then have "b = of_nat (n - j - 1)"
1.83 +	using j kn by (simp add: of_nat_diff)
1.84 +      with b have False using j by auto}
1.85 +    then have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0"
1.86 +      by (auto simp add: algebra_simps)
1.87 +
1.88 +    from nz kn have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0"
1.89 +      by (simp add: pochhammer_neq_0_mono)
1.90 +    {assume k0: "k = 0 \<or> n =0"
1.91 +      then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
1.92 +	using kn
1.93 +	by (cases "k=0", simp_all add: gbinomial_pochhammer)}
1.94 +    moreover
1.95 +    {assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0"
1.96 +      then obtain m where m: "n = Suc m" by (cases n, auto)
1.97 +      from k0 obtain h where h: "k = Suc h" by (cases k, auto)
1.98 +      {assume kn: "k = n"
1.99 +	then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
1.100 +	  using kn pochhammer_minus'[where k=k and n=n and b=b]
1.101 +	  apply (simp add:  pochhammer_same)
1.102 +	  using bn0
1.104 +      moreover
1.105 +      {assume nk: "k \<noteq> n"
1.106 +	have m1nk: "?m1 n = setprod (%i. - 1) {0..m}"
1.107 +	  "?m1 k = setprod (%i. - 1) {0..h}"
1.108 +	  by (simp_all add: setprod_constant m h)
1.109 +	from kn nk have kn': "k < n" by simp
1.110 +	have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0"
1.111 +	  using bn0 kn
1.112 +	  unfolding pochhammer_eq_0_iff
1.113 +	  apply auto
1.114 +	  apply (erule_tac x= "n - ka - 1" in allE)
1.115 +	  by (auto simp add: algebra_simps of_nat_diff)
1.116 +	have eq1: "setprod (%k. (1::'a) + of_nat m - of_nat k) {0 .. h} = setprod of_nat {Suc (m - h) .. Suc m}"
1.117 +	  apply (rule strong_setprod_reindex_cong[where f="%k. Suc m - k "])
1.118 +	  using kn' h m
1.119 +	  apply (auto simp add: inj_on_def image_def)
1.120 +	  apply (rule_tac x="Suc m - x" in bexI)
1.121 +	  apply (simp_all add: of_nat_diff)
1.122 +	  done
1.123 +
1.124 +	have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
1.125 +	  unfolding m1nk
1.126 +
1.127 +	  unfolding m h pochhammer_Suc_setprod
1.128 +	  apply (simp add: field_simps del: fact_Suc id_def)
1.129 +	  unfolding fact_setprod id_def
1.130 +	  unfolding of_nat_setprod
1.131 +	  unfolding setprod_timesf[symmetric]
1.132 +	  apply auto
1.133 +	  unfolding eq1
1.134 +	  apply (subst setprod_Un_disjoint[symmetric])
1.135 +	  apply (auto)
1.136 +	  apply (rule setprod_cong)
1.137 +	  apply auto
1.138 +	  done
1.139 +	have th20: "?m1 n * ?p b n = setprod (%i. b - of_nat i) {0..m}"
1.140 +	  unfolding m1nk
1.141 +	  unfolding m h pochhammer_Suc_setprod
1.142 +	  unfolding setprod_timesf[symmetric]
1.143 +	  apply (rule setprod_cong)
1.144 +	  apply auto
1.145 +	  done
1.146 +	have th21:"pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {n - k .. n - 1}"
1.147 +	  unfolding h m
1.148 +	  unfolding pochhammer_Suc_setprod
1.149 +	  apply (rule strong_setprod_reindex_cong[where f="%k. n - 1 - k"])
1.150 +	  using kn
1.151 +	  apply (auto simp add: inj_on_def m h image_def)
1.152 +	  apply (rule_tac x= "m - x" in bexI)
1.153 +	  by (auto simp add: of_nat_diff)
1.154 +
1.155 +	have "?m1 n * ?p b n = pochhammer (b - of_nat n + 1) k * setprod (%i. b - of_nat i) {0.. n - k - 1}"
1.156 +	  unfolding th20 th21
1.157 +	  unfolding h m
1.158 +	  apply (subst setprod_Un_disjoint[symmetric])
1.159 +	  using kn' h m
1.160 +	  apply auto
1.161 +	  apply (rule setprod_cong)
1.162 +	  apply auto
1.163 +	  done
1.164 +	then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {0.. n - k - 1}"
1.165 +	  using nz' by (simp add: field_simps)
1.166 +	have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) = ((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)"
1.167 +	  using bnz0
1.168 +	  by (simp add: field_simps)
1.169 +	also have "\<dots> = b gchoose (n - k)"
1.170 +	  unfolding th1 th2
1.171 +	  using kn' by (simp add: gbinomial_def)
1.172 +	finally have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" by simp}
1.173 +      ultimately have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
1.174 +	by (cases "k =n", auto)}
1.175 +    ultimately have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" "pochhammer (1 + b - of_nat n) k \<noteq> 0 "
1.176 +      using nz'
1.177 +      apply (cases "n=0", auto)
1.178 +      by (cases "k", auto)}
1.179 +  note th00 = this
1.180 +  have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))"
1.181 +    unfolding gbinomial_pochhammer
1.182 +    using bn0 by (auto simp add: field_simps)
1.183 +  also have "\<dots> = ?l"
1.184 +    unfolding gbinomial_Vandermonde[symmetric]
1.185 +    apply (simp add: th00)
1.186 +    unfolding gbinomial_pochhammer
1.187 +    using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps)
1.188 +    apply (rule setsum_cong2)
1.189 +    apply (drule th00(2))
1.191 +  finally show ?thesis by simp
1.192 +qed
1.193 +
1.194 +
1.195 +lemma Vandermonde_pochhammer:
1.196 +   fixes a :: "'a::field_char_0"
1.197 +  assumes c: "ALL i : {0..< n}. c \<noteq> - of_nat i"
1.198 +  shows "setsum (%k. (pochhammer a k * pochhammer (- (of_nat n)) k) / (of_nat (fact k) * pochhammer c k)) {0..n} = pochhammer (c - a) n / pochhammer c n"
1.199 +proof-
1.200 +  let ?a = "- a"
1.201 +  let ?b = "c + of_nat n - 1"
1.202 +  have h: "\<forall> j \<in>{0..< n}. ?b \<noteq> of_nat j" using c
1.203 +    apply (auto simp add: algebra_simps of_nat_diff)
1.204 +    apply (erule_tac x= "n - j - 1" in ballE)
1.205 +    by (auto simp add: of_nat_diff algebra_simps)
1.206 +  have th0: "pochhammer (- (?a + ?b)) n = (- 1)^n * pochhammer (c - a) n"
1.207 +    unfolding pochhammer_minus[OF le_refl]
1.208 +    by (simp add: algebra_simps)
1.209 +  have th1: "pochhammer (- ?b) n = (- 1)^n * pochhammer c n"
1.210 +    unfolding pochhammer_minus[OF le_refl]
1.211 +    by simp
1.212 +  have nz: "pochhammer c n \<noteq> 0" using c
1.213 +    by (simp add: pochhammer_eq_0_iff)
1.214 +  from Vandermonde_pochhammer_lemma[where a = "?a" and b="?b" and n=n, OF h, unfolded th0 th1]
1.215 +  show ?thesis using nz by (simp add: field_simps setsum_right_distrib)
1.216 +qed
1.217
1.218  subsubsection{* Formal trigonometric functions  *}
1.219
1.220 @@ -3090,4 +3230,104 @@
1.221    unfolding Eii_sin_cos[symmetric] E_power_mult
1.223
1.224 +subsection {* Hypergeometric series *}
1.225 +
1.226 +
1.227 +definition "F as bs (c::'a::{field_char_0, division_by_zero}) = Abs_fps (%n. (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
1.228 +
1.229 +lemma F_nth[simp]: "F as bs c \$ n =  (foldl (%r a. r* pochhammer a n) 1 as * c^n)/ (foldl (%r b. r * pochhammer b n) 1 bs * of_nat (fact n))"
1.230 +  by (simp add: F_def)
1.231 +
1.232 +lemma foldl_mult_start:
1.233 +  "foldl (%r x. r * f x) (v::'a::comm_ring_1) as * x = foldl (%r x. r * f x) (v * x) as "
1.234 +  by (induct as arbitrary: x v, auto simp add: algebra_simps)
1.235 +
1.236 +lemma foldr_mult_foldl: "foldr (%x r. r * f x) as v = foldl (%r x. r * f x) (v :: 'a::comm_ring_1) as"
1.237 +  by (induct as arbitrary: v, auto simp add: foldl_mult_start)
1.238 +
1.239 +lemma F_nth_alt: "F as bs c \$ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
1.240 +    foldr (\<lambda>b r. r * pochhammer b n) bs (of_nat (fact n))"
1.241 +  by (simp add: foldl_mult_start foldr_mult_foldl)
1.242 +
1.243 +lemma F_E[simp]: "F [] [] c = E c"
1.244 +  by (simp add: fps_eq_iff)
1.245 +
1.246 +lemma F_1_0[simp]: "F  [] c = 1/(1 - fps_const c * X)"
1.247 +proof-
1.248 +  let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)"
1.249 +  thm gp
1.250 +  have th0: "(fps_const c * X) \$ 0 = 0" by simp
1.251 +  show ?thesis unfolding gp[OF th0, symmetric]
1.252 +    by (auto simp add: fps_eq_iff pochhammer_fact[symmetric] fps_compose_nth power_mult_distrib cond_value_iff setsum_delta' cong del: if_weak_cong)
1.253 +qed
1.254 +
1.255 +lemma F_B[simp]: "F [-a] [] (- 1) = fps_binomial a"
1.256 +  by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps)
1.257 +
1.258 +lemma F_0[simp]: "F as bs c \$0 = 1"
1.259 +  apply simp
1.260 +  apply (subgoal_tac "ALL as. foldl (%(r::'a) (a::'a). r) 1 as = 1")
1.261 +  apply auto
1.262 +  apply (induct_tac as, auto)
1.263 +  done
1.264 +
1.265 +lemma foldl_prod_prod: "foldl (%(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (%r x. r * g x) w as = foldl (%r x. r * f x * g x) (v*w) as"
1.266 +  by (induct as arbitrary: v w, auto simp add: algebra_simps)
1.267 +
1.268 +
1.269 +lemma F_rec: "F as bs c \$ Suc n = ((foldl (%r a. r* (a + of_nat n)) c as)/ (foldl (%r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c \$ n"
1.270 +  apply (simp del: of_nat_Suc of_nat_add fact_Suc)
1.271 +  apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc)
1.272 +  unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc
1.273 +  by (simp add: algebra_simps of_nat_mult)
1.274 +
1.275 +lemma XD_nth[simp]: "XD a \$ n = (if n=0 then 0 else of_nat n * a\$n)"
1.276 +  by (simp add: XD_def)
1.277 +
1.278 +lemma XD_0th[simp]: "XD a \$ 0 = 0" by simp
1.279 +lemma XD_Suc[simp]:" XD a \$ Suc n = of_nat (Suc n) * a \$ Suc n" by simp
1.280 +
1.281 +definition "XDp c a = XD a + fps_const c * a"
1.282 +
1.283 +lemma XDp_nth[simp]: "XDp c a \$ n = (c + of_nat n) * a\$n"
1.284 +  by (simp add: XDp_def algebra_simps)
1.285 +
1.286 +lemma XDp_commute:
1.287 +  shows "XDp b o XDp (c::'a::comm_ring_1) = XDp c o XDp b"
1.288 +  by (auto simp add: XDp_def expand_fun_eq fps_eq_iff algebra_simps)
1.289 +
1.290 +lemma XDp0[simp]: "XDp 0 = XD"
1.291 +  by (simp add: expand_fun_eq fps_eq_iff)
1.292 +
1.293 +lemma XDp_fps_integral[simp]:"XDp 0 (fps_integral a c) = X * a"
1.294 +  by (simp add: fps_eq_iff fps_integral_def)
1.295 +
1.296 +lemma F_minus_nat:
1.297 +  "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, division_by_zero}) \$ k = (if k <= n then pochhammer (- of_nat n) k * c ^ k /
1.298 +    (pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)"
1.299 +  "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, division_by_zero}) \$ k = (if k <= m then pochhammer (- of_nat m) k * c ^ k /
1.300 +    (pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)"
1.301 +  by (auto simp add: pochhammer_eq_0_iff)
1.302 +
1.303 +lemma setsum_eq_if: "setsum f {(n::nat) .. m} = (if m < n then 0 else f n + setsum f {n+1 .. m})"
1.304 +  apply simp
1.305 +  apply (subst setsum_insert[symmetric])
1.307 +
1.308 +lemma pochhammer_rec_if:
1.309 +  "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))"
1.310 +  by (cases n, simp_all add: pochhammer_rec)
1.311 +
1.312 +lemma XDp_foldr_nth[simp]: "foldr (%c r. XDp c o r) cs (%c. XDp c a) c0 \$ n =
1.313 +  foldr (%c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a\$n"
1.314 +  by (induct cs arbitrary: c0, auto simp add: algebra_simps)
1.315 +
1.316 +lemma genric_XDp_foldr_nth:
1.317 +  assumes
1.318 +  f: "ALL n c a. f c a \$ n = (of_nat n + k c) * a\$n"
1.319 +
1.320 +  shows "foldr (%c r. f c o r) cs (%c. g c a) c0 \$ n =
1.321 +  foldr (%c r. (k c + of_nat n) * r) cs (g c0 a \$ n)"
1.322 +  by (induct cs arbitrary: c0, auto simp add: algebra_simps f )
1.323 +
1.324  end
```