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.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.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.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.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.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.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.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.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.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
```