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.36 -           del: setsum_cl_ivl_Suc)
1.37 -
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.88 -  also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
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)