src/HOL/Transcendental.thy
changeset 56213 e5720d3c18f0
parent 56193 c726ecfb22b6
child 56217 dc429a5b13c4
     1.1 --- a/src/HOL/Transcendental.thy	Tue Mar 18 22:11:46 2014 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Wed Mar 19 15:34:57 2014 +0100
     1.3 @@ -552,7 +552,7 @@
     1.4    hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
     1.5      by (rule summable_norm)
     1.6    also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
     1.7 -    by (rule summable_le)
     1.8 +    by (rule suminf_le)
     1.9    also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
    1.10      by (rule suminf_mult2 [symmetric])
    1.11    finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
    1.12 @@ -737,7 +737,7 @@
    1.13          using `x \<noteq> 0` by auto }
    1.14      note 1 = this and 2 = summable_rabs_comparison_test[OF _ ign[OF `summable L`]]
    1.15      then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))"
    1.16 -      by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] summable_le[OF _ 2 ign[OF `summable L`]]])
    1.17 +      by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF `summable L`]]])
    1.18      then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3")
    1.19        using L_estimate by auto
    1.20  
    1.21 @@ -1006,22 +1006,17 @@
    1.22    shows "(\<Sum>n. f n * 0 ^ n) = f 0"
    1.23  proof -
    1.24    have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
    1.25 -    by (rule sums_unique [OF series_zero], simp add: power_0_left)
    1.26 +    by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
    1.27    thus ?thesis unfolding One_nat_def by simp
    1.28  qed
    1.29  
    1.30  lemma exp_zero [simp]: "exp 0 = 1"
    1.31    unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
    1.32  
    1.33 -lemma setsum_cl_ivl_Suc2:
    1.34 -  "(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))"
    1.35 -  by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl
    1.36 -           del: setsum_cl_ivl_Suc)
    1.37 -
    1.38  lemma exp_series_add:
    1.39    fixes x y :: "'a::{real_field}"
    1.40    defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
    1.41 -  shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
    1.42 +  shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
    1.43  proof (induct n)
    1.44    case 0
    1.45    show ?case
    1.46 @@ -1035,32 +1030,32 @@
    1.47  
    1.48    have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
    1.49      by (simp only: times_S)
    1.50 -  also have "\<dots> = (x + y) * (\<Sum>i=0..n. S x i * S y (n-i))"
    1.51 +  also have "\<dots> = (x + y) * (\<Sum>i\<le>n. S x i * S y (n-i))"
    1.52      by (simp only: Suc)
    1.53 -  also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (n-i))
    1.54 -                + y * (\<Sum>i=0..n. S x i * S y (n-i))"
    1.55 +  also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (n-i))
    1.56 +                + y * (\<Sum>i\<le>n. S x i * S y (n-i))"
    1.57      by (rule distrib_right)
    1.58 -  also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
    1.59 -                + (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
    1.60 +  also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (n-i))
    1.61 +                + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
    1.62      by (simp only: setsum_right_distrib mult_ac)
    1.63 -  also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
    1.64 -                + (\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
    1.65 +  also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
    1.66 +                + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
    1.67      by (simp add: times_S Suc_diff_le)
    1.68 -  also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
    1.69 -             (\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
    1.70 -    by (subst setsum_cl_ivl_Suc2, simp)
    1.71 -  also have "(\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
    1.72 -             (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
    1.73 -    by (subst setsum_cl_ivl_Suc, simp)
    1.74 -  also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
    1.75 -             (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
    1.76 -             (\<Sum>i=0..Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
    1.77 +  also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
    1.78 +             (\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
    1.79 +    by (subst setsum_atMost_Suc_shift) simp
    1.80 +  also have "(\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
    1.81 +             (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
    1.82 +    by simp
    1.83 +  also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
    1.84 +             (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
    1.85 +             (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
    1.86      by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
    1.87 -              real_of_nat_add [symmetric], simp)
    1.88 -  also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
    1.89 +                   real_of_nat_add [symmetric]) simp
    1.90 +  also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n-i))"
    1.91      by (simp only: scaleR_right.setsum)
    1.92    finally show
    1.93 -    "S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
    1.94 +    "S (x + y) (Suc n) = (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"
    1.95      by (simp del: setsum_cl_ivl_Suc)
    1.96  qed
    1.97  
    1.98 @@ -1128,7 +1123,7 @@
    1.99    have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
   1.100      by (auto simp add: numeral_2_eq_2)
   1.101    also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
   1.102 -    apply (rule series_pos_le [OF summable_exp])
   1.103 +    apply (rule setsum_le_suminf [OF summable_exp])
   1.104      using `0 < x`
   1.105      apply (auto  simp add:  zero_le_mult_iff)
   1.106      done
   1.107 @@ -1412,7 +1407,7 @@
   1.108    proof -
   1.109      have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <=
   1.110          suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
   1.111 -      apply (rule summable_le)
   1.112 +      apply (rule suminf_le)
   1.113        apply (rule allI, rule aux1)
   1.114        apply (rule summable_exp [THEN summable_ignore_initial_segment])
   1.115        by (rule sums_summable, rule aux2)
   1.116 @@ -2388,7 +2383,7 @@
   1.117    show "0 < sin x"
   1.118      unfolding sums_unique [OF sums]
   1.119      using sums_summable [OF sums] pos
   1.120 -    by (rule suminf_gt_zero)
   1.121 +    by (rule suminf_pos)
   1.122  qed
   1.123  
   1.124  lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
   1.125 @@ -2427,7 +2422,7 @@
   1.126  apply (frule sums_unique)
   1.127  apply (drule sums_summable)
   1.128  apply simp
   1.129 -apply (erule suminf_gt_zero)
   1.130 +apply (erule suminf_pos)
   1.131  apply (simp add: add_ac)
   1.132  done
   1.133