Vandermonde vs Pochhammer; Hypergeometric series - very basic facts
authorchaieb
Thu Jul 23 21:12:57 2009 +0200 (2009-07-23)
changeset 3216063686057cbe8
parent 32159 4082bd9824c9
child 32161 abda97d2deea
Vandermonde vs Pochhammer; Hypergeometric series - very basic facts
src/HOL/Library/Formal_Power_Series.thy
     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.21    by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
    1.22  
    1.23 -lemma assumes r: "r (Suc k) 1 = 1" 
    1.24 +lemma radical_E:
    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.103 +	  by (simp add: field_simps power_add[symmetric])}
   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.190 +    by (simp add: field_simps power_add[symmetric])
   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.222    by (simp add: mult_ac)
   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 [1] [] 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.306 +  by (auto simp add: not_less setsum_head_Suc)
   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