src/HOL/Transcendental.thy
changeset 56193 c726ecfb22b6
parent 56181 2aa0b19e74f3
child 56213 e5720d3c18f0
     1.1 --- a/src/HOL/Transcendental.thy	Tue Mar 18 14:32:23 2014 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Tue Mar 18 15:53:48 2014 +0100
     1.3 @@ -21,66 +21,55 @@
     1.4    thus ?thesis by (simp add: power_commutes)
     1.5  qed
     1.6  
     1.7 -lemma lemma_realpow_diff_sumr:
     1.8 -  fixes y :: "'a::{comm_semiring_0,monoid_mult}"
     1.9 -  shows
    1.10 -    "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =
    1.11 -      y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
    1.12 -  by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac del: setsum_op_ivl_Suc)
    1.13 -
    1.14  lemma lemma_realpow_diff_sumr2:
    1.15    fixes y :: "'a::{comm_ring,monoid_mult}"
    1.16    shows
    1.17      "x ^ (Suc n) - y ^ (Suc n) =
    1.18 -      (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
    1.19 +      (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
    1.20  proof (induct n)
    1.21 -  case 0 show ?case
    1.22 -    by simp
    1.23 -next
    1.24    case (Suc n)
    1.25    have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x ^ n) - y * (y * y ^ n)"
    1.26      by simp
    1.27    also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x ^ n)"
    1.28      by (simp add: algebra_simps)
    1.29 -  also have "... = y * ((x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    1.30 +  also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    1.31      by (simp only: Suc)
    1.32 -  also have "... = (x - y) * (y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    1.33 +  also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
    1.34      by (simp only: mult_left_commute)
    1.35 -  also have "... = (x - y) * (\<Sum>p = 0..<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
    1.36 -    by (simp add: setsum_op_ivl_Suc [where n = "Suc n"] distrib_left lemma_realpow_diff_sumr
    1.37 -             del: setsum_op_ivl_Suc)
    1.38 +  also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
    1.39 +    by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
    1.40    finally show ?case .
    1.41 -qed
    1.42 +qed simp
    1.43  
    1.44  corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
    1.45    fixes x :: "'a::{comm_ring,monoid_mult}"
    1.46 -  shows   "x^n - y^n = (x - y) * (\<Sum>i=0..<n. y^(n - Suc i) * x^i)"
    1.47 +  shows   "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
    1.48  using lemma_realpow_diff_sumr2[of x "n - 1" y]
    1.49  by (cases "n = 0") (simp_all add: field_simps)
    1.50  
    1.51  lemma lemma_realpow_rev_sumr:
    1.52 -   "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
    1.53 -    (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
    1.54 +   "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
    1.55 +    (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
    1.56    apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
    1.57 -  apply (rule inj_onI, auto)
    1.58 -  apply (metis atLeastLessThan_iff diff_diff_cancel diff_less_Suc imageI le0 less_Suc_eq_le)
    1.59 +  apply (auto simp: image_iff Bex_def intro!: inj_onI)
    1.60 +  apply arith
    1.61    done
    1.62  
    1.63  lemma power_diff_1_eq:
    1.64    fixes x :: "'a::{comm_ring,monoid_mult}"
    1.65 -  shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i=0..<n. (x^i))"
    1.66 +  shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
    1.67  using lemma_realpow_diff_sumr2 [of x _ 1] 
    1.68    by (cases n) auto
    1.69  
    1.70  lemma one_diff_power_eq':
    1.71    fixes x :: "'a::{comm_ring,monoid_mult}"
    1.72 -  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i=0..<n. x^(n - Suc i))"
    1.73 +  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
    1.74  using lemma_realpow_diff_sumr2 [of 1 _ x] 
    1.75    by (cases n) auto
    1.76  
    1.77  lemma one_diff_power_eq:
    1.78    fixes x :: "'a::{comm_ring,monoid_mult}"
    1.79 -  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i=0..<n. x^i)"
    1.80 +  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
    1.81  by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
    1.82  
    1.83  text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
    1.84 @@ -149,17 +138,17 @@
    1.85  lemma sum_split_even_odd:
    1.86    fixes f :: "nat \<Rightarrow> real"
    1.87    shows
    1.88 -    "(\<Sum> i = 0 ..< 2 * n. if even i then f i else g i) =
    1.89 -     (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1))"
    1.90 +    "(\<Sum>i<2 * n. if even i then f i else g i) =
    1.91 +     (\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1))"
    1.92  proof (induct n)
    1.93    case 0
    1.94    then show ?case by simp
    1.95  next
    1.96    case (Suc n)
    1.97 -  have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) =
    1.98 -    (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
    1.99 +  have "(\<Sum>i<2 * Suc n. if even i then f i else g i) =
   1.100 +    (\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
   1.101      using Suc.hyps unfolding One_nat_def by auto
   1.102 -  also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))"
   1.103 +  also have "\<dots> = (\<Sum>i<Suc n. f (2 * i)) + (\<Sum>i<Suc n. g (2 * i + 1))"
   1.104      by auto
   1.105    finally show ?case .
   1.106  qed
   1.107 @@ -173,14 +162,14 @@
   1.108    fix r :: real
   1.109    assume "0 < r"
   1.110    from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this]
   1.111 -  obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g { 0..<n } - x) < r)" by blast
   1.112 -
   1.113 -  let ?SUM = "\<lambda> m. \<Sum> i = 0 ..< m. if even i then 0 else g ((i - 1) div 2)"
   1.114 +  obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g {..<n} - x) < r)" by blast
   1.115 +
   1.116 +  let ?SUM = "\<lambda> m. \<Sum>i<m. if even i then 0 else g ((i - 1) div 2)"
   1.117    {
   1.118      fix m
   1.119      assume "m \<ge> 2 * no"
   1.120      hence "m div 2 \<ge> no" by auto
   1.121 -    have sum_eq: "?SUM (2 * (m div 2)) = setsum g { 0 ..< m div 2 }"
   1.122 +    have sum_eq: "?SUM (2 * (m div 2)) = setsum g {..< m div 2}"
   1.123        using sum_split_even_odd by auto
   1.124      hence "(norm (?SUM (2 * (m div 2)) - x) < r)"
   1.125        using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto
   1.126 @@ -220,16 +209,12 @@
   1.127    have g_sums: "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
   1.128      using sums_if'[OF `g sums x`] .
   1.129    {
   1.130 -    have "?s 0 = 0" by auto
   1.131 -    have Suc_m1: "\<And> n. Suc n - 1 = n" by auto
   1.132      have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" by auto
   1.133  
   1.134      have "?s sums y" using sums_if'[OF `f sums y`] .
   1.135      from this[unfolded sums_def, THEN LIMSEQ_Suc]
   1.136      have "(\<lambda> n. if even n then f (n div 2) else 0) sums y"
   1.137 -      unfolding sums_def setsum_shift_lb_Suc0_0_upt[where f="?s", OF `?s 0 = 0`, symmetric]
   1.138 -                image_Suc_atLeastLessThan[symmetric] setsum_reindex[OF inj_Suc, unfolded comp_def]
   1.139 -                even_Suc Suc_m1 if_eq .
   1.140 +      by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum_reindex if_eq sums_def cong del: if_cong)
   1.141    }
   1.142    from sums_add[OF g_sums this] show ?thesis unfolding if_sum .
   1.143  qed
   1.144 @@ -239,8 +224,8 @@
   1.145  lemma sums_alternating_upper_lower:
   1.146    fixes a :: "nat \<Rightarrow> real"
   1.147    assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
   1.148 -  shows "\<exists>l. ((\<forall>n. (\<Sum>i=0..<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i=0..<2*n. -1^i*a i) ----> l) \<and>
   1.149 -             ((\<forall>n. l \<le> (\<Sum>i=0..<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i=0..<2*n + 1. -1^i*a i) ----> l)"
   1.150 +  shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. -1^i*a i) ----> l) \<and>
   1.151 +             ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. -1^i*a i) ----> l)"
   1.152    (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
   1.153  proof (rule nested_sequence_unique)
   1.154    have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
   1.155 @@ -279,13 +264,13 @@
   1.156      and a_pos: "\<And> n. 0 \<le> a n"
   1.157      and a_monotone: "\<And> n. a (Suc n) \<le> a n"
   1.158    shows summable: "summable (\<lambda> n. (-1)^n * a n)"
   1.159 -    and "\<And>n. (\<Sum>i=0..<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)"
   1.160 -    and "(\<lambda>n. \<Sum>i=0..<2*n. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
   1.161 -    and "\<And>n. (\<Sum>i. (-1)^i*a i) \<le> (\<Sum>i=0..<2*n+1. (-1)^i*a i)"
   1.162 -    and "(\<lambda>n. \<Sum>i=0..<2*n+1. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
   1.163 +    and "\<And>n. (\<Sum>i<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)"
   1.164 +    and "(\<lambda>n. \<Sum>i<2*n. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
   1.165 +    and "\<And>n. (\<Sum>i. (-1)^i*a i) \<le> (\<Sum>i<2*n+1. (-1)^i*a i)"
   1.166 +    and "(\<lambda>n. \<Sum>i<2*n+1. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
   1.167  proof -
   1.168    let ?S = "\<lambda>n. (-1)^n * a n"
   1.169 -  let ?P = "\<lambda>n. \<Sum>i=0..<n. ?S i"
   1.170 +  let ?P = "\<lambda>n. \<Sum>i<n. ?S i"
   1.171    let ?f = "\<lambda>n. ?P (2 * n)"
   1.172    let ?g = "\<lambda>n. ?P (2 * n + 1)"
   1.173    obtain l :: real
   1.174 @@ -295,7 +280,7 @@
   1.175        and "?g ----> l"
   1.176      using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast
   1.177  
   1.178 -  let ?Sa = "\<lambda>m. \<Sum> n = 0..<m. ?S n"
   1.179 +  let ?Sa = "\<lambda>m. \<Sum>n<m. ?S n"
   1.180    have "?Sa ----> l"
   1.181    proof (rule LIMSEQ_I)
   1.182      fix r :: real
   1.183 @@ -332,13 +317,13 @@
   1.184          from n_eq `n \<ge> 2 * g_no` have "(n - 1) div 2 \<ge> g_no"
   1.185            by auto
   1.186          from g[OF this] show ?thesis
   1.187 -          unfolding n_eq atLeastLessThanSuc_atLeastAtMost range_eq .
   1.188 +          unfolding n_eq range_eq .
   1.189        qed
   1.190      }
   1.191      thus "\<exists>no. \<forall>n \<ge> no. norm (?Sa n - l) < r" by blast
   1.192    qed
   1.193    hence sums_l: "(\<lambda>i. (-1)^i * a i) sums l"
   1.194 -    unfolding sums_def atLeastLessThanSuc_atLeastAtMost[symmetric] .
   1.195 +    unfolding sums_def .
   1.196    thus "summable ?S" using summable_def by auto
   1.197  
   1.198    have "l = suminf ?S" using sums_unique[OF sums_l] .
   1.199 @@ -359,11 +344,11 @@
   1.200    assumes a_zero: "a ----> 0" and "monoseq a"
   1.201    shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
   1.202      and "0 < a 0 \<longrightarrow>
   1.203 -      (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i=0..<2*n. -1^i * a i .. \<Sum>i=0..<2*n+1. -1^i * a i})" (is "?pos")
   1.204 +      (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i<2*n. -1^i * a i .. \<Sum>i<2*n+1. -1^i * a i})" (is "?pos")
   1.205      and "a 0 < 0 \<longrightarrow>
   1.206 -      (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i=0..<2*n+1. -1^i * a i .. \<Sum>i=0..<2*n. -1^i * a i})" (is "?neg")
   1.207 -    and "(\<lambda>n. \<Sum>i=0..<2*n. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?f")
   1.208 -    and "(\<lambda>n. \<Sum>i=0..<2*n+1. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?g")
   1.209 +      (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i<2*n+1. -1^i * a i .. \<Sum>i<2*n. -1^i * a i})" (is "?neg")
   1.210 +    and "(\<lambda>n. \<Sum>i<2*n. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?f")
   1.211 +    and "(\<lambda>n. \<Sum>i<2*n+1. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?g")
   1.212  proof -
   1.213    have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
   1.214    proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
   1.215 @@ -424,38 +409,32 @@
   1.216  
   1.217  subsection {* Term-by-Term Differentiability of Power Series *}
   1.218  
   1.219 -definition diffs :: "(nat => 'a::ring_1) => nat => 'a"
   1.220 -  where "diffs c = (\<lambda>n. of_nat (Suc n) * c(Suc n))"
   1.221 +definition diffs :: "(nat \<Rightarrow> 'a::ring_1) \<Rightarrow> nat \<Rightarrow> 'a"
   1.222 +  where "diffs c = (\<lambda>n. of_nat (Suc n) * c (Suc n))"
   1.223  
   1.224  text{*Lemma about distributing negation over it*}
   1.225  lemma diffs_minus: "diffs (\<lambda>n. - c n) = (\<lambda>n. - diffs c n)"
   1.226    by (simp add: diffs_def)
   1.227  
   1.228  lemma sums_Suc_imp:
   1.229 -  assumes f: "f 0 = 0"
   1.230 -  shows "(\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
   1.231 -  unfolding sums_def
   1.232 -  apply (rule LIMSEQ_imp_Suc)
   1.233 -  apply (subst setsum_shift_lb_Suc0_0_upt [where f=f, OF f, symmetric])
   1.234 -  apply (simp only: setsum_shift_bounds_Suc_ivl)
   1.235 -  done
   1.236 +  "(f::nat \<Rightarrow> 'a::real_normed_vector) 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
   1.237 +  using sums_Suc_iff[of f] by simp
   1.238  
   1.239  lemma diffs_equiv:
   1.240    fixes x :: "'a::{real_normed_vector, ring_1}"
   1.241 -  shows "summable (\<lambda>n. (diffs c)(n) * (x ^ n)) \<Longrightarrow>
   1.242 -      (\<lambda>n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums
   1.243 -         (\<Sum>n. (diffs c)(n) * (x ^ n))"
   1.244 +  shows "summable (\<lambda>n. diffs c n * x^n) \<Longrightarrow>
   1.245 +      (\<lambda>n. of_nat n * c n * x^(n - Suc 0)) sums (\<Sum>n. diffs c n * x^n)"
   1.246    unfolding diffs_def
   1.247    by (simp add: summable_sums sums_Suc_imp)
   1.248  
   1.249  lemma lemma_termdiff1:
   1.250    fixes z :: "'a :: {monoid_mult,comm_ring}" shows
   1.251 -  "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
   1.252 -   (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
   1.253 +  "(\<Sum>p<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
   1.254 +   (\<Sum>p<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
   1.255    by (auto simp add: algebra_simps power_add [symmetric])
   1.256  
   1.257  lemma sumr_diff_mult_const2:
   1.258 -  "setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)"
   1.259 +  "setsum f {..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i<n. f i - r)"
   1.260    by (simp add: setsum_subtractf)
   1.261  
   1.262  lemma lemma_termdiff2:
   1.263 @@ -463,7 +442,7 @@
   1.264    assumes h: "h \<noteq> 0"
   1.265    shows
   1.266      "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
   1.267 -     h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p.
   1.268 +     h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p.
   1.269            (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
   1.270    apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
   1.271    apply (simp add: right_diff_distrib diff_divide_distrib h)
   1.272 @@ -471,7 +450,7 @@
   1.273    apply (cases "n", simp)
   1.274    apply (simp add: lemma_realpow_diff_sumr2 h
   1.275                     right_diff_distrib [symmetric] mult_assoc
   1.276 -              del: power_Suc setsum_op_ivl_Suc of_nat_Suc)
   1.277 +              del: power_Suc setsum_lessThan_Suc of_nat_Suc)
   1.278    apply (subst lemma_realpow_rev_sumr)
   1.279    apply (subst sumr_diff_mult_const2)
   1.280    apply simp
   1.281 @@ -480,7 +459,7 @@
   1.282    apply (simp add: less_iff_Suc_add)
   1.283    apply (clarify)
   1.284    apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
   1.285 -              del: setsum_op_ivl_Suc power_Suc)
   1.286 +              del: setsum_lessThan_Suc power_Suc)
   1.287    apply (subst mult_assoc [symmetric], subst power_add [symmetric])
   1.288    apply (simp add: mult_ac)
   1.289    done
   1.290 @@ -489,7 +468,7 @@
   1.291    fixes K :: "'a::linordered_semidom"
   1.292    assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
   1.293      and K: "0 \<le> K"
   1.294 -  shows "setsum f {0..<n-k} \<le> of_nat n * K"
   1.295 +  shows "setsum f {..<n-k} \<le> of_nat n * K"
   1.296    apply (rule order_trans [OF setsum_mono])
   1.297    apply (rule f, simp)
   1.298    apply (simp add: mult_right_mono K)
   1.299 @@ -504,7 +483,7 @@
   1.300            \<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
   1.301  proof -
   1.302    have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
   1.303 -        norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
   1.304 +        norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p.
   1.305            (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
   1.306      by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult_commute norm_mult)
   1.307    also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
   1.308 @@ -516,7 +495,7 @@
   1.309        apply (simp only: norm_mult norm_power power_add)
   1.310        apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
   1.311        done
   1.312 -    show "norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))
   1.313 +    show "norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))
   1.314            \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
   1.315        apply (intro
   1.316           order_trans [OF norm_setsum]
   1.317 @@ -712,16 +691,16 @@
   1.318    from divide_pos_pos[OF `0 < r` this]
   1.319    have "0 < ?r" .
   1.320  
   1.321 -  let "?s n" = "SOME s. 0 < s \<and> (\<forall> x. x \<noteq> 0 \<and> \<bar> x \<bar> < s \<longrightarrow> \<bar> ?diff n x - f' x0 n \<bar> < ?r)"
   1.322 -  def S' \<equiv> "Min (?s ` { 0 ..< ?N })"
   1.323 +  let ?s = "\<lambda>n. SOME s. 0 < s \<and> (\<forall> x. x \<noteq> 0 \<and> \<bar> x \<bar> < s \<longrightarrow> \<bar> ?diff n x - f' x0 n \<bar> < ?r)"
   1.324 +  def S' \<equiv> "Min (?s ` {..< ?N })"
   1.325  
   1.326    have "0 < S'" unfolding S'_def
   1.327    proof (rule iffD2[OF Min_gr_iff])
   1.328 -    show "\<forall>x \<in> (?s ` { 0 ..< ?N }). 0 < x"
   1.329 +    show "\<forall>x \<in> (?s ` {..< ?N }). 0 < x"
   1.330      proof
   1.331        fix x
   1.332 -      assume "x \<in> ?s ` {0..<?N}"
   1.333 -      then obtain n where "x = ?s n" and "n \<in> {0..<?N}"
   1.334 +      assume "x \<in> ?s ` {..<?N}"
   1.335 +      then obtain n where "x = ?s n" and "n \<in> {..<?N}"
   1.336          using image_iff[THEN iffD1] by blast
   1.337        from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def]
   1.338        obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)"
   1.339 @@ -750,32 +729,30 @@
   1.340      note div_shft_smbl = summable_divide[OF diff_shft_smbl]
   1.341      note all_shft_smbl = summable_diff[OF div_smbl ign[OF `summable (f' x0)`]]
   1.342  
   1.343 -    {
   1.344 -      fix n
   1.345 +    { fix n
   1.346        have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x) - x0 \<bar> / \<bar> x \<bar>"
   1.347          using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero]
   1.348          unfolding abs_divide .
   1.349        hence "\<bar> (\<bar>?diff (n + ?N) x \<bar>) \<bar> \<le> L (n + ?N)"
   1.350 -        using `x \<noteq> 0` by auto
   1.351 -    } note L_ge = summable_le2[OF allI[OF this] ign[OF `summable L`]]
   1.352 -    from order_trans[OF summable_rabs[OF conjunct1[OF L_ge]] L_ge[THEN conjunct2]]
   1.353 -    have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))" .
   1.354 -    hence "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3")
   1.355 +        using `x \<noteq> 0` by auto }
   1.356 +    note 1 = this and 2 = summable_rabs_comparison_test[OF _ ign[OF `summable L`]]
   1.357 +    then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))"
   1.358 +      by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] summable_le[OF _ 2 ign[OF `summable L`]]])
   1.359 +    then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3")
   1.360        using L_estimate by auto
   1.361  
   1.362 -    have "\<bar>\<Sum>n \<in> { 0 ..< ?N}. ?diff n x - f' x0 n \<bar> \<le>
   1.363 -      (\<Sum>n \<in> { 0 ..< ?N}. \<bar>?diff n x - f' x0 n \<bar>)" ..
   1.364 -    also have "\<dots> < (\<Sum>n \<in> { 0 ..< ?N}. ?r)"
   1.365 +    have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> \<le> (\<Sum>n<?N. \<bar>?diff n x - f' x0 n \<bar>)" ..
   1.366 +    also have "\<dots> < (\<Sum>n<?N. ?r)"
   1.367      proof (rule setsum_strict_mono)
   1.368        fix n
   1.369 -      assume "n \<in> { 0 ..< ?N}"
   1.370 +      assume "n \<in> {..< ?N}"
   1.371        have "\<bar>x\<bar> < S" using `\<bar>x\<bar> < S` .
   1.372        also have "S \<le> S'" using `S \<le> S'` .
   1.373        also have "S' \<le> ?s n" unfolding S'_def
   1.374        proof (rule Min_le_iff[THEN iffD2])
   1.375 -        have "?s n \<in> (?s ` {0..<?N}) \<and> ?s n \<le> ?s n"
   1.376 -          using `n \<in> { 0 ..< ?N}` by auto
   1.377 -        thus "\<exists> a \<in> (?s ` {0..<?N}). a \<le> ?s n" by blast
   1.378 +        have "?s n \<in> (?s ` {..<?N}) \<and> ?s n \<le> ?s n"
   1.379 +          using `n \<in> {..< ?N}` by auto
   1.380 +        thus "\<exists> a \<in> (?s ` {..<?N}). a \<le> ?s n" by blast
   1.381        qed auto
   1.382        finally have "\<bar>x\<bar> < ?s n" .
   1.383  
   1.384 @@ -784,12 +761,12 @@
   1.385        with `x \<noteq> 0` and `\<bar>x\<bar> < ?s n` show "\<bar>?diff n x - f' x0 n\<bar> < ?r"
   1.386          by blast
   1.387      qed auto
   1.388 -    also have "\<dots> = of_nat (card {0 ..< ?N}) * ?r"
   1.389 +    also have "\<dots> = of_nat (card {..<?N}) * ?r"
   1.390        by (rule setsum_constant)
   1.391      also have "\<dots> = real ?N * ?r"
   1.392        unfolding real_eq_of_nat by auto
   1.393      also have "\<dots> = r/3" by auto
   1.394 -    finally have "\<bar>\<Sum>n \<in> { 0 ..< ?N}. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
   1.395 +    finally have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
   1.396  
   1.397      from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
   1.398      have "\<bar>(suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0)\<bar> =
   1.399 @@ -799,6 +776,7 @@
   1.400      also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N)) \<bar>"
   1.401        unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"]
   1.402        unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]]
   1.403 +      apply (subst (5) add_commute)
   1.404        by (rule abs_triangle_ineq)
   1.405      also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part"
   1.406        using abs_triangle_ineq4 by auto
   1.407 @@ -844,17 +822,17 @@
   1.408          show "\<bar>?f x n - ?f y n\<bar> \<le> \<bar>f n * real (Suc n) * R'^n\<bar> * \<bar>x-y\<bar>"
   1.409          proof -
   1.410            have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> =
   1.411 -            (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar>"
   1.412 +            (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar>"
   1.413              unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult
   1.414              by auto
   1.415            also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>x-y\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)"
   1.416            proof (rule mult_left_mono)
   1.417 -            have "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> (\<Sum>p = 0..<Suc n. \<bar>x ^ p * y ^ (n - p)\<bar>)"
   1.418 +            have "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> (\<Sum>p<Suc n. \<bar>x ^ p * y ^ (n - p)\<bar>)"
   1.419                by (rule setsum_abs)
   1.420 -            also have "\<dots> \<le> (\<Sum>p = 0..<Suc n. R' ^ n)"
   1.421 +            also have "\<dots> \<le> (\<Sum>p<Suc n. R' ^ n)"
   1.422              proof (rule setsum_mono)
   1.423                fix p
   1.424 -              assume "p \<in> {0..<Suc n}"
   1.425 +              assume "p \<in> {..<Suc n}"
   1.426                hence "p \<le> n" by auto
   1.427                {
   1.428                  fix n
   1.429 @@ -872,7 +850,7 @@
   1.430              qed
   1.431              also have "\<dots> = real (Suc n) * R' ^ n"
   1.432                unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto
   1.433 -            finally show "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>"
   1.434 +            finally show "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>"
   1.435                unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] .
   1.436              show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>"
   1.437                unfolding abs_mult[symmetric] by auto
   1.438 @@ -893,14 +871,14 @@
   1.439          hence "R' \<in> {-R <..< R}" and "norm x < norm R'"
   1.440            using assms `R' < R` by auto
   1.441          have "summable (\<lambda> n. f n * x^n)"
   1.442 -        proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`]], rule allI)
   1.443 +        proof (rule summable_comparison_test, intro exI allI impI)
   1.444            fix n
   1.445            have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)"
   1.446              by (rule mult_left_mono) auto
   1.447 -          show "\<bar>f n * x ^ n\<bar> \<le> norm (f n * real (Suc n) * x ^ n)"
   1.448 +          show "norm (f n * x ^ n) \<le> norm (f n * real (Suc n) * x ^ n)"
   1.449              unfolding real_norm_def abs_mult
   1.450              by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
   1.451 -        qed
   1.452 +        qed (rule powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`])
   1.453          from this[THEN summable_mult2[where c=x], unfolded mult_assoc, unfolded mult_commute]
   1.454          show "summable (?f x)" by auto
   1.455        }
   1.456 @@ -947,7 +925,7 @@
   1.457    obtain N :: nat where N: "norm x < real N * r"
   1.458      using reals_Archimedean3 [OF r0] by fast
   1.459    from r1 show ?thesis
   1.460 -  proof (rule ratio_test [rule_format])
   1.461 +  proof (rule summable_ratio_test [rule_format])
   1.462      fix n :: nat
   1.463      assume n: "N \<le> n"
   1.464      have "norm x \<le> real N * r"
   1.465 @@ -1027,7 +1005,7 @@
   1.466    fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
   1.467    shows "(\<Sum>n. f n * 0 ^ n) = f 0"
   1.468  proof -
   1.469 -  have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
   1.470 +  have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
   1.471      by (rule sums_unique [OF series_zero], simp add: power_0_left)
   1.472    thus ?thesis unfolding One_nat_def by simp
   1.473  qed
   1.474 @@ -1147,7 +1125,7 @@
   1.475  using order_le_imp_less_or_eq [OF assms]
   1.476  proof 
   1.477    assume "0 < x"
   1.478 -  have "1+x \<le> (\<Sum>n = 0..<2. inverse (real (fact n)) * x ^ n)"
   1.479 +  have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
   1.480      by (auto simp add: numeral_2_eq_2)
   1.481    also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
   1.482      apply (rule series_pos_le [OF summable_exp])
   1.483 @@ -1395,12 +1373,13 @@
   1.484  proof -
   1.485    have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
   1.486      by (simp add: exp_def)
   1.487 -  also from summable_exp have "... = (\<Sum> n::nat = 0 ..< 2. inverse(fact n) * (x ^ n)) +
   1.488 -      (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _")
   1.489 +  also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) + 
   1.490 +    (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
   1.491      by (rule suminf_split_initial_segment)
   1.492    also have "?a = 1 + x"
   1.493      by (simp add: numeral_2_eq_2)
   1.494 -  finally show ?thesis .
   1.495 +  finally show ?thesis
   1.496 +    by simp
   1.497  qed
   1.498  
   1.499  lemma exp_bound: "0 <= (x::real) \<Longrightarrow> x <= 1 \<Longrightarrow> exp x <= 1 + x + x\<^sup>2"
   1.500 @@ -2433,6 +2412,25 @@
   1.501  
   1.502  lemmas realpow_num_eq_if = power_eq_if
   1.503  
   1.504 +lemma sumr_pos_lt_pair:
   1.505 +  fixes f :: "nat \<Rightarrow> real"
   1.506 +  shows "\<lbrakk>summable f;
   1.507 +        \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
   1.508 +      \<Longrightarrow> setsum f {..<k} < suminf f"
   1.509 +unfolding One_nat_def
   1.510 +apply (subst suminf_split_initial_segment [where k="k"])
   1.511 +apply assumption
   1.512 +apply simp
   1.513 +apply (drule_tac k="k" in summable_ignore_initial_segment)
   1.514 +apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)
   1.515 +apply simp
   1.516 +apply (frule sums_unique)
   1.517 +apply (drule sums_summable)
   1.518 +apply simp
   1.519 +apply (erule suminf_gt_zero)
   1.520 +apply (simp add: add_ac)
   1.521 +done
   1.522 +
   1.523  lemma cos_two_less_zero [simp]:
   1.524    "cos 2 < 0"
   1.525  proof -
   1.526 @@ -2444,9 +2442,9 @@
   1.527      by simp
   1.528    then have **: "summable (\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.529      by (rule sums_summable)
   1.530 -  have "0 < (\<Sum>n = 0..<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.531 +  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.532      by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
   1.533 -  moreover have "(\<Sum>n = 0..<Suc (Suc (Suc 0)). - (-1 ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
   1.534 +  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
   1.535      < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   1.536    proof -
   1.537      { fix d
   1.538 @@ -3807,7 +3805,7 @@
   1.539      case False
   1.540      hence "\<bar>x\<bar> = 1" using `\<bar>x\<bar> \<le> 1` by auto
   1.541      let ?a = "\<lambda>x n. \<bar>1 / real (n*2+1) * x^(n*2+1)\<bar>"
   1.542 -    let ?diff = "\<lambda> x n. \<bar> arctan x - (\<Sum> i = 0..<n. ?c x i)\<bar>"
   1.543 +    let ?diff = "\<lambda> x n. \<bar> arctan x - (\<Sum> i<n. ?c x i)\<bar>"
   1.544      {
   1.545        fix n :: nat
   1.546        have "0 < (1 :: real)" by auto
   1.547 @@ -3830,7 +3828,7 @@
   1.548            from `even n` obtain m where "2 * m = n"
   1.549              unfolding even_mult_two_ex by auto
   1.550            from bounds[of m, unfolded this atLeastAtMost_iff]
   1.551 -          have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n + 1. (?c x i)) - (\<Sum>i = 0..<n. (?c x i))"
   1.552 +          have "\<bar>arctan x - (\<Sum>i<n. (?c x i))\<bar> \<le> (\<Sum>i<n + 1. (?c x i)) - (\<Sum>i<n. (?c x i))"
   1.553              by auto
   1.554            also have "\<dots> = ?c x n" unfolding One_nat_def by auto
   1.555            also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
   1.556 @@ -3842,7 +3840,7 @@
   1.557              unfolding odd_Suc_mult_two_ex by auto
   1.558            hence m_plus: "2 * (m + 1) = n + 1" by auto
   1.559            from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
   1.560 -          have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n. (?c x i)) - (\<Sum>i = 0..<n+1. (?c x i))"
   1.561 +          have "\<bar>arctan x - (\<Sum>i<n. (?c x i))\<bar> \<le> (\<Sum>i<n. (?c x i)) - (\<Sum>i<n+1. (?c x i))"
   1.562              by auto
   1.563            also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
   1.564            also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto