misc tuning and modernization;
authorwenzelm
Tue Jul 26 10:33:39 2016 +0200 (2016-07-26)
changeset 635503a0f40a6fa42
parent 63549 b0d31c7def86
child 63551 679402a894ae
child 63557 e506baad44fa
misc tuning and modernization;
src/HOL/Series.thy
     1.1 --- a/src/HOL/Series.thy	Mon Jul 25 21:50:04 2016 +0200
     1.2 +++ b/src/HOL/Series.thy	Tue Jul 26 10:33:39 2016 +0200
     1.3 @@ -15,20 +15,16 @@
     1.4  
     1.5  subsection \<open>Definition of infinite summability\<close>
     1.6  
     1.7 -definition
     1.8 -  sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
     1.9 -  (infixr "sums" 80)
    1.10 -where
    1.11 -  "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> s"
    1.12 +definition sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
    1.13 +    (infixr "sums" 80)
    1.14 +  where "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> s"
    1.15  
    1.16 -definition summable :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> bool" where
    1.17 -   "summable f \<longleftrightarrow> (\<exists>s. f sums s)"
    1.18 +definition summable :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> bool"
    1.19 +  where "summable f \<longleftrightarrow> (\<exists>s. f sums s)"
    1.20  
    1.21 -definition
    1.22 -  suminf :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a"
    1.23 -  (binder "\<Sum>" 10)
    1.24 -where
    1.25 -  "suminf f = (THE s. f sums s)"
    1.26 +definition suminf :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a"
    1.27 +    (binder "\<Sum>" 10)
    1.28 +  where "suminf f = (THE s. f sums s)"
    1.29  
    1.30  lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
    1.31    apply (simp add: sums_def)
    1.32 @@ -36,6 +32,7 @@
    1.33    apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
    1.34    done
    1.35  
    1.36 +
    1.37  subsection \<open>Infinite summability on topological monoids\<close>
    1.38  
    1.39  lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
    1.40 @@ -50,8 +47,7 @@
    1.41  lemma summable_iff_convergent: "summable f \<longleftrightarrow> convergent (\<lambda>n. \<Sum>i<n. f i)"
    1.42    by (simp add: summable_def sums_def convergent_def)
    1.43  
    1.44 -lemma summable_iff_convergent':
    1.45 -  "summable f \<longleftrightarrow> convergent (\<lambda>n. setsum f {..n})"
    1.46 +lemma summable_iff_convergent': "summable f \<longleftrightarrow> convergent (\<lambda>n. setsum f {..n})"
    1.47    by (simp_all only: summable_iff_convergent convergent_def
    1.48          lessThan_Suc_atMost [symmetric] LIMSEQ_Suc_iff[of "\<lambda>n. setsum f {..<n}"])
    1.49  
    1.50 @@ -80,24 +76,29 @@
    1.51    by (rule arg_cong[of f g], rule ext) simp
    1.52  
    1.53  lemma summable_cong:
    1.54 -  assumes "eventually (\<lambda>x. f x = (g x :: 'a :: real_normed_vector)) sequentially"
    1.55 -  shows   "summable f = summable g"
    1.56 +  fixes f g :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.57 +  assumes "eventually (\<lambda>x. f x = g x) sequentially"
    1.58 +  shows "summable f = summable g"
    1.59  proof -
    1.60 -  from assms obtain N where N: "\<forall>n\<ge>N. f n = g n" by (auto simp: eventually_at_top_linorder)
    1.61 +  from assms obtain N where N: "\<forall>n\<ge>N. f n = g n"
    1.62 +    by (auto simp: eventually_at_top_linorder)
    1.63    define C where "C = (\<Sum>k<N. f k - g k)"
    1.64    from eventually_ge_at_top[of N]
    1.65 -    have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially"
    1.66 +  have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially"
    1.67    proof eventually_elim
    1.68 -    fix n assume n: "n \<ge> N"
    1.69 -    from n have "{..<n} = {..<N} \<union> {N..<n}" by auto
    1.70 +    case (elim n)
    1.71 +    then have "{..<n} = {..<N} \<union> {N..<n}"
    1.72 +      by auto
    1.73      also have "setsum f ... = setsum f {..<N} + setsum f {N..<n}"
    1.74        by (intro setsum.union_disjoint) auto
    1.75 -    also from N have "setsum f {N..<n} = setsum g {N..<n}" by (intro setsum.cong) simp_all
    1.76 +    also from N have "setsum f {N..<n} = setsum g {N..<n}"
    1.77 +      by (intro setsum.cong) simp_all
    1.78      also have "setsum f {..<N} + setsum g {N..<n} = C + (setsum g {..<N} + setsum g {N..<n})"
    1.79        unfolding C_def by (simp add: algebra_simps setsum_subtractf)
    1.80      also have "setsum g {..<N} + setsum g {N..<n} = setsum g ({..<N} \<union> {N..<n})"
    1.81        by (intro setsum.union_disjoint [symmetric]) auto
    1.82 -    also from n have "{..<N} \<union> {N..<n} = {..<n}" by auto
    1.83 +    also from elim have "{..<N} \<union> {N..<n} = {..<n}"
    1.84 +      by auto
    1.85      finally show "setsum f {..<n} = C + setsum g {..<n}" .
    1.86    qed
    1.87    from convergent_cong[OF this] show ?thesis
    1.88 @@ -105,32 +106,32 @@
    1.89  qed
    1.90  
    1.91  lemma sums_finite:
    1.92 -  assumes [simp]: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
    1.93 +  assumes [simp]: "finite N"
    1.94 +    and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
    1.95    shows "f sums (\<Sum>n\<in>N. f n)"
    1.96  proof -
    1.97 -  { fix n
    1.98 -    have "setsum f {..<n + Suc (Max N)} = setsum f N"
    1.99 -    proof cases
   1.100 -      assume "N = {}"
   1.101 -      with f have "f = (\<lambda>x. 0)" by auto
   1.102 -      then show ?thesis by simp
   1.103 -    next
   1.104 -      assume [simp]: "N \<noteq> {}"
   1.105 -      show ?thesis
   1.106 -      proof (safe intro!: setsum.mono_neutral_right f)
   1.107 -        fix i assume "i \<in> N"
   1.108 -        then have "i \<le> Max N" by simp
   1.109 -        then show "i < n + Suc (Max N)" by simp
   1.110 -      qed
   1.111 -    qed }
   1.112 -  note eq = this
   1.113 -  show ?thesis unfolding sums_def
   1.114 +  have eq: "setsum f {..<n + Suc (Max N)} = setsum f N" for n
   1.115 +  proof (cases "N = {}")
   1.116 +    case True
   1.117 +    with f have "f = (\<lambda>x. 0)" by auto
   1.118 +    then show ?thesis by simp
   1.119 +  next
   1.120 +    case [simp]: False
   1.121 +    show ?thesis
   1.122 +    proof (safe intro!: setsum.mono_neutral_right f)
   1.123 +      fix i
   1.124 +      assume "i \<in> N"
   1.125 +      then have "i \<le> Max N" by simp
   1.126 +      then show "i < n + Suc (Max N)" by simp
   1.127 +    qed
   1.128 +  qed
   1.129 +  show ?thesis
   1.130 +    unfolding sums_def
   1.131      by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
   1.132         (simp add: eq atLeast0LessThan del: add_Suc_right)
   1.133  qed
   1.134  
   1.135 -corollary sums_0:
   1.136 -   "(\<And>n. f n = 0) \<Longrightarrow> (f sums 0)"
   1.137 +corollary sums_0: "(\<And>n. f n = 0) \<Longrightarrow> (f sums 0)"
   1.138      by (metis (no_types) finite.emptyI setsum.empty sums_finite)
   1.139  
   1.140  lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
   1.141 @@ -155,7 +156,7 @@
   1.142    by (rule sums_summable) (rule sums_single)
   1.143  
   1.144  context
   1.145 -  fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}"
   1.146 +  fixes f :: "nat \<Rightarrow> 'a::{t2_space,comm_monoid_add}"
   1.147  begin
   1.148  
   1.149  lemma summable_sums[intro]: "summable f \<Longrightarrow> f sums (suminf f)"
   1.150 @@ -168,20 +169,19 @@
   1.151  lemma sums_unique: "f sums s \<Longrightarrow> s = suminf f"
   1.152    by (metis limI suminf_eq_lim sums_def)
   1.153  
   1.154 -lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
   1.155 +lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> suminf f = x"
   1.156    by (metis summable_sums sums_summable sums_unique)
   1.157  
   1.158 -lemma summable_sums_iff:
   1.159 -  "summable (f :: nat \<Rightarrow> 'a :: {comm_monoid_add,t2_space}) \<longleftrightarrow> f sums suminf f"
   1.160 +lemma summable_sums_iff: "summable f \<longleftrightarrow> f sums suminf f"
   1.161    by (auto simp: sums_iff summable_sums)
   1.162  
   1.163 -lemma sums_unique2:
   1.164 -  fixes a b :: "'a::{comm_monoid_add,t2_space}"
   1.165 -  shows "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b"
   1.166 -by (simp add: sums_iff)
   1.167 +lemma sums_unique2: "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b"
   1.168 +  for a b :: 'a
   1.169 +  by (simp add: sums_iff)
   1.170  
   1.171  lemma suminf_finite:
   1.172 -  assumes N: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
   1.173 +  assumes N: "finite N"
   1.174 +    and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
   1.175    shows "suminf f = (\<Sum>n\<in>N. f n)"
   1.176    using sums_finite[OF assms, THEN sums_unique] by simp
   1.177  
   1.178 @@ -193,16 +193,15 @@
   1.179  
   1.180  subsection \<open>Infinite summability on ordered, topological monoids\<close>
   1.181  
   1.182 -lemma sums_le:
   1.183 -  fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
   1.184 -  shows "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
   1.185 +lemma sums_le: "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
   1.186 +  for f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology}"
   1.187    by (rule LIMSEQ_le) (auto intro: setsum_mono simp: sums_def)
   1.188  
   1.189  context
   1.190 -  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
   1.191 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology}"
   1.192  begin
   1.193  
   1.194 -lemma suminf_le: "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
   1.195 +lemma suminf_le: "\<forall>n. f n \<le> g n \<Longrightarrow> summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f \<le> suminf g"
   1.196    by (auto dest: sums_summable intro: sums_le)
   1.197  
   1.198  lemma setsum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f"
   1.199 @@ -221,15 +220,14 @@
   1.200      using summable_LIMSEQ[of f] by simp
   1.201    then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
   1.202    proof (rule LIMSEQ_le_const)
   1.203 -    fix i show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}"
   1.204 +    show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}" for i
   1.205        using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto
   1.206    qed
   1.207    with pos show "\<forall>n. f n = 0"
   1.208      by (auto intro!: antisym)
   1.209  qed (metis suminf_zero fun_eq_iff)
   1.210  
   1.211 -lemma suminf_pos_iff:
   1.212 -  "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
   1.213 +lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
   1.214    using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
   1.215  
   1.216  lemma suminf_pos2:
   1.217 @@ -249,14 +247,14 @@
   1.218  end
   1.219  
   1.220  context
   1.221 -  fixes f :: "nat \<Rightarrow> 'a::{ordered_cancel_comm_monoid_add, linorder_topology}"
   1.222 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_cancel_comm_monoid_add,linorder_topology}"
   1.223  begin
   1.224  
   1.225 -lemma setsum_less_suminf2: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> setsum f {..<n} < suminf f"
   1.226 -  using
   1.227 -    setsum_le_suminf[of f "Suc i"]
   1.228 -    add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
   1.229 -    setsum_mono2[of "{..<i}" "{..<n}" f]
   1.230 +lemma setsum_less_suminf2:
   1.231 +  "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> setsum f {..<n} < suminf f"
   1.232 +  using setsum_le_suminf[of f "Suc i"]
   1.233 +    and add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
   1.234 +    and setsum_mono2[of "{..<i}" "{..<n}" f]
   1.235    by (auto simp: less_imp_le ac_simps)
   1.236  
   1.237  lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
   1.238 @@ -265,10 +263,11 @@
   1.239  end
   1.240  
   1.241  lemma summableI_nonneg_bounded:
   1.242 -  fixes f:: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology, conditionally_complete_linorder}"
   1.243 -  assumes pos[simp]: "\<And>n. 0 \<le> f n" and le: "\<And>n. (\<Sum>i<n. f i) \<le> x"
   1.244 +  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology,conditionally_complete_linorder}"
   1.245 +  assumes pos[simp]: "\<And>n. 0 \<le> f n"
   1.246 +    and le: "\<And>n. (\<Sum>i<n. f i) \<le> x"
   1.247    shows "summable f"
   1.248 -  unfolding summable_def sums_def[abs_def]
   1.249 +  unfolding summable_def sums_def [abs_def]
   1.250  proof (rule exI LIMSEQ_incseq_SUP)+
   1.251    show "bdd_above (range (\<lambda>n. setsum f {..<n}))"
   1.252      using le by (auto simp: bdd_above_def)
   1.253 @@ -276,27 +275,28 @@
   1.254      by (auto simp: mono_def intro!: setsum_mono2)
   1.255  qed
   1.256  
   1.257 -lemma summableI[intro, simp]:
   1.258 -  fixes f:: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add, linorder_topology, complete_linorder}"
   1.259 -  shows "summable f"
   1.260 +lemma summableI[intro, simp]: "summable f"
   1.261 +  for f :: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add,linorder_topology,complete_linorder}"
   1.262    by (intro summableI_nonneg_bounded[where x=top] zero_le top_greatest)
   1.263  
   1.264 +
   1.265  subsection \<open>Infinite summability on topological monoids\<close>
   1.266  
   1.267  context
   1.268 -  fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
   1.269 +  fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_comm_monoid_add}"
   1.270  begin
   1.271  
   1.272  lemma sums_Suc:
   1.273 -  assumes "(\<lambda>n. f (Suc n)) sums l" shows "f sums (l + f 0)"
   1.274 +  assumes "(\<lambda>n. f (Suc n)) sums l"
   1.275 +  shows "f sums (l + f 0)"
   1.276  proof  -
   1.277    have "(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0"
   1.278      using assms by (auto intro!: tendsto_add simp: sums_def)
   1.279    moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
   1.280      unfolding lessThan_Suc_eq_insert_0
   1.281 -      by (simp add: ac_simps setsum_atLeast1_atMost_eq image_Suc_lessThan)
   1.282 +    by (simp add: ac_simps setsum_atLeast1_atMost_eq image_Suc_lessThan)
   1.283    ultimately show ?thesis
   1.284 -    by (auto simp add: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
   1.285 +    by (auto simp: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
   1.286  qed
   1.287  
   1.288  lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
   1.289 @@ -311,7 +311,8 @@
   1.290  end
   1.291  
   1.292  context
   1.293 -  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{t2_space, topological_comm_monoid_add}" and I :: "'i set"
   1.294 +  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{t2_space,topological_comm_monoid_add}"
   1.295 +    and I :: "'i set"
   1.296  begin
   1.297  
   1.298  lemma sums_setsum: "(\<And>i. i \<in> I \<Longrightarrow> (f i) sums (x i)) \<Longrightarrow> (\<lambda>n. \<Sum>i\<in>I. f i n) sums (\<Sum>i\<in>I. x i)"
   1.299 @@ -340,8 +341,7 @@
   1.300    also have "\<dots> \<longleftrightarrow> (\<lambda>n. f (Suc n)) sums s"
   1.301    proof
   1.302      assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
   1.303 -    with tendsto_add[OF this tendsto_const, of "- f 0"]
   1.304 -    show "(\<lambda>i. f (Suc i)) sums s"
   1.305 +    with tendsto_add[OF this tendsto_const, of "- f 0"] show "(\<lambda>i. f (Suc i)) sums s"
   1.306        by (simp add: sums_def)
   1.307    qed (auto intro: tendsto_add simp: sums_def)
   1.308    finally show ?thesis ..
   1.309 @@ -350,9 +350,12 @@
   1.310  lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n)) = summable f"
   1.311  proof
   1.312    assume "summable f"
   1.313 -  hence "f sums suminf f" by (rule summable_sums)
   1.314 -  hence "(\<lambda>n. f (Suc n)) sums (suminf f - f 0)" by (simp add: sums_Suc_iff)
   1.315 -  thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast
   1.316 +  then have "f sums suminf f"
   1.317 +    by (rule summable_sums)
   1.318 +  then have "(\<lambda>n. f (Suc n)) sums (suminf f - f 0)"
   1.319 +    by (simp add: sums_Suc_iff)
   1.320 +  then show "summable (\<lambda>n. f (Suc n))"
   1.321 +    unfolding summable_def by blast
   1.322  qed (auto simp: sums_Suc_iff summable_def)
   1.323  
   1.324  lemma sums_Suc_imp: "f 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
   1.325 @@ -360,7 +363,7 @@
   1.326  
   1.327  end
   1.328  
   1.329 -context \<comment>\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
   1.330 +context (* Separate contexts are necessary to allow general use of the results above, here. *)
   1.331    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   1.332  begin
   1.333  
   1.334 @@ -384,12 +387,15 @@
   1.335  
   1.336  lemma sums_iff_shift: "(\<lambda>i. f (i + n)) sums s \<longleftrightarrow> f sums (s + (\<Sum>i<n. f i))"
   1.337  proof (induct n arbitrary: s)
   1.338 +  case 0
   1.339 +  then show ?case by simp
   1.340 +next
   1.341    case (Suc n)
   1.342 -  moreover have "(\<lambda>i. f (Suc i + n)) sums s \<longleftrightarrow> (\<lambda>i. f (i + n)) sums (s + f n)"
   1.343 +  then have "(\<lambda>i. f (Suc i + n)) sums s \<longleftrightarrow> (\<lambda>i. f (i + n)) sums (s + f n)"
   1.344      by (subst sums_Suc_iff) simp
   1.345 -  ultimately show ?case
   1.346 +  with Suc show ?case
   1.347      by (simp add: ac_simps)
   1.348 -qed simp
   1.349 +qed
   1.350  
   1.351  corollary sums_iff_shift': "(\<lambda>i. f (i + n)) sums (s - (\<Sum>i<n. f i)) \<longleftrightarrow> f sums s"
   1.352    by (simp add: sums_iff_shift)
   1.353 @@ -397,10 +403,10 @@
   1.354  lemma sums_zero_iff_shift:
   1.355    assumes "\<And>i. i < n \<Longrightarrow> f i = 0"
   1.356    shows "(\<lambda>i. f (i+n)) sums s \<longleftrightarrow> (\<lambda>i. f i) sums s"
   1.357 -by (simp add: assms sums_iff_shift)
   1.358 +  by (simp add: assms sums_iff_shift)
   1.359  
   1.360  lemma summable_iff_shift: "summable (\<lambda>n. f (n + k)) \<longleftrightarrow> summable f"
   1.361 -  by (metis diff_add_cancel summable_def sums_iff_shift[abs_def])
   1.362 +  by (metis diff_add_cancel summable_def sums_iff_shift [abs_def])
   1.363  
   1.364  lemma sums_split_initial_segment: "f sums s \<Longrightarrow> (\<lambda>i. f (i + n)) sums (s - (\<Sum>i<n. f i))"
   1.365    by (simp add: sums_iff_shift)
   1.366 @@ -418,23 +424,30 @@
   1.367    using suminf_split_initial_segment[of 1] by simp
   1.368  
   1.369  lemma suminf_exist_split:
   1.370 -  fixes r :: real assumes "0 < r" and "summable f"
   1.371 +  fixes r :: real
   1.372 +  assumes "0 < r" and "summable f"
   1.373    shows "\<exists>N. \<forall>n\<ge>N. norm (\<Sum>i. f (i + n)) < r"
   1.374  proof -
   1.375    from LIMSEQ_D[OF summable_LIMSEQ[OF \<open>summable f\<close>] \<open>0 < r\<close>]
   1.376 -  obtain N :: nat where "\<forall> n \<ge> N. norm (setsum f {..<n} - suminf f) < r" by auto
   1.377 -  thus ?thesis
   1.378 +  obtain N :: nat where "\<forall> n \<ge> N. norm (setsum f {..<n} - suminf f) < r"
   1.379 +    by auto
   1.380 +  then show ?thesis
   1.381      by (auto simp: norm_minus_commute suminf_minus_initial_segment[OF \<open>summable f\<close>])
   1.382  qed
   1.383  
   1.384  lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f \<longlonglongrightarrow> 0"
   1.385    apply (drule summable_iff_convergent [THEN iffD1])
   1.386    apply (drule convergent_Cauchy)
   1.387 -  apply (simp only: Cauchy_iff LIMSEQ_iff, safe)
   1.388 -  apply (drule_tac x="r" in spec, safe)
   1.389 -  apply (rule_tac x="M" in exI, safe)
   1.390 -  apply (drule_tac x="Suc n" in spec, simp)
   1.391 -  apply (drule_tac x="n" in spec, simp)
   1.392 +  apply (simp only: Cauchy_iff LIMSEQ_iff)
   1.393 +  apply safe
   1.394 +  apply (drule_tac x="r" in spec)
   1.395 +  apply safe
   1.396 +  apply (rule_tac x="M" in exI)
   1.397 +  apply safe
   1.398 +  apply (drule_tac x="Suc n" in spec)
   1.399 +  apply simp
   1.400 +  apply (drule_tac x="n" in spec)
   1.401 +  apply simp
   1.402    done
   1.403  
   1.404  lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f"
   1.405 @@ -445,13 +458,12 @@
   1.406  
   1.407  end
   1.408  
   1.409 -lemma summable_minus_iff:
   1.410 -  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   1.411 -  shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
   1.412 -  by (auto dest: summable_minus) \<comment>\<open>used two ways, hence must be outside the context above\<close>
   1.413 +lemma summable_minus_iff: "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
   1.414 +  for f :: "nat \<Rightarrow> 'a::real_normed_vector"
   1.415 +  by (auto dest: summable_minus)  (* used two ways, hence must be outside the context above *)
   1.416  
   1.417  lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
   1.418 -  unfolding sums_def by (drule tendsto, simp only: setsum)
   1.419 +  unfolding sums_def by (drule tendsto) (simp only: setsum)
   1.420  
   1.421  lemma (in bounded_linear) summable: "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))"
   1.422    unfolding summable_def by (auto intro: sums)
   1.423 @@ -471,19 +483,21 @@
   1.424  lemmas summable_scaleR_right = bounded_linear.summable[OF bounded_linear_scaleR_right]
   1.425  lemmas suminf_scaleR_right = bounded_linear.suminf[OF bounded_linear_scaleR_right]
   1.426  
   1.427 -lemma summable_const_iff: "summable (\<lambda>_. c) \<longleftrightarrow> (c :: 'a :: real_normed_vector) = 0"
   1.428 +lemma summable_const_iff: "summable (\<lambda>_. c) \<longleftrightarrow> c = 0"
   1.429 +  for c :: "'a::real_normed_vector"
   1.430  proof -
   1.431 -  {
   1.432 -    assume "c \<noteq> 0"
   1.433 -    hence "filterlim (\<lambda>n. of_nat n * norm c) at_top sequentially"
   1.434 +  have "\<not> summable (\<lambda>_. c)" if "c \<noteq> 0"
   1.435 +  proof -
   1.436 +    from that have "filterlim (\<lambda>n. of_nat n * norm c) at_top sequentially"
   1.437        by (subst mult.commute)
   1.438 -         (auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_real_sequentially)
   1.439 -    hence "\<not>convergent (\<lambda>n. norm (\<Sum>k<n. c))"
   1.440 +        (auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_real_sequentially)
   1.441 +    then have "\<not> convergent (\<lambda>n. norm (\<Sum>k<n. c))"
   1.442        by (intro filterlim_at_infinity_imp_not_convergent filterlim_at_top_imp_at_infinity)
   1.443 -         (simp_all add: setsum_constant_scaleR)
   1.444 -    hence "\<not>summable (\<lambda>_. c)" unfolding summable_iff_convergent using convergent_norm by blast
   1.445 -  }
   1.446 -  thus ?thesis by auto
   1.447 +        (simp_all add: setsum_constant_scaleR)
   1.448 +    then show ?thesis
   1.449 +      unfolding summable_iff_convergent using convergent_norm by blast
   1.450 +  qed
   1.451 +  then show ?thesis by auto
   1.452  qed
   1.453  
   1.454  
   1.455 @@ -514,18 +528,20 @@
   1.456  end
   1.457  
   1.458  lemma sums_mult_iff:
   1.459 +  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra,field}"
   1.460    assumes "c \<noteq> 0"
   1.461 -  shows   "(\<lambda>n. c * f n :: 'a :: {real_normed_algebra,field}) sums (c * d) \<longleftrightarrow> f sums d"
   1.462 +  shows "(\<lambda>n. c * f n) sums (c * d) \<longleftrightarrow> f sums d"
   1.463    using sums_mult[of f d c] sums_mult[of "\<lambda>n. c * f n" "c * d" "inverse c"]
   1.464    by (force simp: field_simps assms)
   1.465  
   1.466  lemma sums_mult2_iff:
   1.467 -  assumes "c \<noteq> (0 :: 'a :: {real_normed_algebra, field})"
   1.468 +  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra,field}"
   1.469 +  assumes "c \<noteq> 0"
   1.470    shows   "(\<lambda>n. f n * c) sums (d * c) \<longleftrightarrow> f sums d"
   1.471    using sums_mult_iff[OF assms, of f d] by (simp add: mult.commute)
   1.472  
   1.473  lemma sums_of_real_iff:
   1.474 -  "(\<lambda>n. of_real (f n) :: 'a :: real_normed_div_algebra) sums of_real c \<longleftrightarrow> f sums c"
   1.475 +  "(\<lambda>n. of_real (f n) :: 'a::real_normed_div_algebra) sums of_real c \<longleftrightarrow> f sums c"
   1.476    by (simp add: sums_def of_real_setsum[symmetric] tendsto_of_real_iff del: of_real_setsum)
   1.477  
   1.478  
   1.479 @@ -544,26 +560,28 @@
   1.480  lemma suminf_divide: "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
   1.481    by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
   1.482  
   1.483 -lemma sums_mult_D: "\<lbrakk>(\<lambda>n. c * f n) sums a; c \<noteq> 0\<rbrakk> \<Longrightarrow> f sums (a/c)"
   1.484 +lemma sums_mult_D: "(\<lambda>n. c * f n) sums a \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> f sums (a/c)"
   1.485    using sums_mult_iff by fastforce
   1.486  
   1.487 -lemma summable_mult_D: "\<lbrakk>summable (\<lambda>n. c * f n); c \<noteq> 0\<rbrakk> \<Longrightarrow> summable f"
   1.488 +lemma summable_mult_D: "summable (\<lambda>n. c * f n) \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> summable f"
   1.489    by (auto dest: summable_divide)
   1.490  
   1.491 -text\<open>Sum of a geometric progression.\<close>
   1.492 +
   1.493 +text \<open>Sum of a geometric progression.\<close>
   1.494  
   1.495 -lemma geometric_sums: "norm c < 1 \<Longrightarrow> (\<lambda>n. c^n) sums (1 / (1 - c))"
   1.496 +lemma geometric_sums:
   1.497 +  assumes less_1: "norm c < 1"
   1.498 +  shows "(\<lambda>n. c^n) sums (1 / (1 - c))"
   1.499  proof -
   1.500 -  assume less_1: "norm c < 1"
   1.501 -  hence neq_1: "c \<noteq> 1" by auto
   1.502 -  hence neq_0: "c - 1 \<noteq> 0" by simp
   1.503 +  from less_1 have neq_1: "c \<noteq> 1" by auto
   1.504 +  then have neq_0: "c - 1 \<noteq> 0" by simp
   1.505    from less_1 have lim_0: "(\<lambda>n. c^n) \<longlonglongrightarrow> 0"
   1.506      by (rule LIMSEQ_power_zero)
   1.507 -  hence "(\<lambda>n. c ^ n / (c - 1) - 1 / (c - 1)) \<longlonglongrightarrow> 0 / (c - 1) - 1 / (c - 1)"
   1.508 +  then have "(\<lambda>n. c ^ n / (c - 1) - 1 / (c - 1)) \<longlonglongrightarrow> 0 / (c - 1) - 1 / (c - 1)"
   1.509      using neq_0 by (intro tendsto_intros)
   1.510 -  hence "(\<lambda>n. (c ^ n - 1) / (c - 1)) \<longlonglongrightarrow> 1 / (1 - c)"
   1.511 +  then have "(\<lambda>n. (c ^ n - 1) / (c - 1)) \<longlonglongrightarrow> 1 / (1 - c)"
   1.512      by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
   1.513 -  thus "(\<lambda>n. c ^ n) sums (1 / (1 - c))"
   1.514 +  then show "(\<lambda>n. c ^ n) sums (1 / (1 - c))"
   1.515      by (simp add: sums_def geometric_sum neq_1)
   1.516  qed
   1.517  
   1.518 @@ -576,88 +594,106 @@
   1.519  lemma summable_geometric_iff: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
   1.520  proof
   1.521    assume "summable (\<lambda>n. c ^ n :: 'a :: real_normed_field)"
   1.522 -  hence "(\<lambda>n. norm c ^ n) \<longlonglongrightarrow> 0"
   1.523 +  then have "(\<lambda>n. norm c ^ n) \<longlonglongrightarrow> 0"
   1.524      by (simp add: norm_power [symmetric] tendsto_norm_zero_iff summable_LIMSEQ_zero)
   1.525    from order_tendstoD(2)[OF this zero_less_one] obtain n where "norm c ^ n < 1"
   1.526      by (auto simp: eventually_at_top_linorder)
   1.527 -  thus "norm c < 1" using one_le_power[of "norm c" n] by (cases "norm c \<ge> 1") (linarith, simp)
   1.528 +  then show "norm c < 1" using one_le_power[of "norm c" n]
   1.529 +    by (cases "norm c \<ge> 1") (linarith, simp)
   1.530  qed (rule summable_geometric)
   1.531  
   1.532  end
   1.533  
   1.534  lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
   1.535  proof -
   1.536 -  have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
   1.537 -    by auto
   1.538 +  have 2: "(\<lambda>n. (1/2::real)^n) sums 2"
   1.539 +    using geometric_sums [of "1/2::real"] by auto
   1.540    have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
   1.541      by (simp add: mult.commute)
   1.542 -  thus ?thesis using sums_divide [OF 2, of 2]
   1.543 -    by simp
   1.544 +  then show ?thesis
   1.545 +    using sums_divide [OF 2, of 2] by simp
   1.546  qed
   1.547  
   1.548  
   1.549  subsection \<open>Telescoping\<close>
   1.550  
   1.551  lemma telescope_sums:
   1.552 -  assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)"
   1.553 -  shows   "(\<lambda>n. f (Suc n) - f n) sums (c - f 0)"
   1.554 +  fixes c :: "'a::real_normed_vector"
   1.555 +  assumes "f \<longlonglongrightarrow> c"
   1.556 +  shows "(\<lambda>n. f (Suc n) - f n) sums (c - f 0)"
   1.557    unfolding sums_def
   1.558  proof (subst LIMSEQ_Suc_iff [symmetric])
   1.559    have "(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)"
   1.560      by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setsum_Suc_diff)
   1.561 -  also have "\<dots> \<longlonglongrightarrow> c - f 0" by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const)
   1.562 +  also have "\<dots> \<longlonglongrightarrow> c - f 0"
   1.563 +    by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const)
   1.564    finally show "(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0" .
   1.565  qed
   1.566  
   1.567  lemma telescope_sums':
   1.568 -  assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)"
   1.569 -  shows   "(\<lambda>n. f n - f (Suc n)) sums (f 0 - c)"
   1.570 +  fixes c :: "'a::real_normed_vector"
   1.571 +  assumes "f \<longlonglongrightarrow> c"
   1.572 +  shows "(\<lambda>n. f n - f (Suc n)) sums (f 0 - c)"
   1.573    using sums_minus[OF telescope_sums[OF assms]] by (simp add: algebra_simps)
   1.574  
   1.575  lemma telescope_summable:
   1.576 -  assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)"
   1.577 -  shows   "summable (\<lambda>n. f (Suc n) - f n)"
   1.578 +  fixes c :: "'a::real_normed_vector"
   1.579 +  assumes "f \<longlonglongrightarrow> c"
   1.580 +  shows "summable (\<lambda>n. f (Suc n) - f n)"
   1.581    using telescope_sums[OF assms] by (simp add: sums_iff)
   1.582  
   1.583  lemma telescope_summable':
   1.584 -  assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)"
   1.585 -  shows   "summable (\<lambda>n. f n - f (Suc n))"
   1.586 +  fixes c :: "'a::real_normed_vector"
   1.587 +  assumes "f \<longlonglongrightarrow> c"
   1.588 +  shows "summable (\<lambda>n. f n - f (Suc n))"
   1.589    using summable_minus[OF telescope_summable[OF assms]] by (simp add: algebra_simps)
   1.590  
   1.591  
   1.592  subsection \<open>Infinite summability on Banach spaces\<close>
   1.593  
   1.594 -text\<open>Cauchy-type criterion for convergence of series (c.f. Harrison)\<close>
   1.595 +text \<open>Cauchy-type criterion for convergence of series (c.f. Harrison).\<close>
   1.596  
   1.597 -lemma summable_Cauchy:
   1.598 -  fixes f :: "nat \<Rightarrow> 'a::banach"
   1.599 -  shows "summable f \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. norm (setsum f {m..<n}) < e)"
   1.600 -  apply (simp only: summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff, safe)
   1.601 -  apply (drule spec, drule (1) mp)
   1.602 -  apply (erule exE, rule_tac x="M" in exI, clarify)
   1.603 +lemma summable_Cauchy: "summable f \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. norm (setsum f {m..<n}) < e)"
   1.604 +  for f :: "nat \<Rightarrow> 'a::banach"
   1.605 +  apply (simp only: summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff)
   1.606 +  apply safe
   1.607 +   apply (drule spec)
   1.608 +   apply (drule (1) mp)
   1.609 +   apply (erule exE)
   1.610 +   apply (rule_tac x="M" in exI)
   1.611 +   apply clarify
   1.612 +   apply (rule_tac x="m" and y="n" in linorder_le_cases)
   1.613 +    apply (frule (1) order_trans)
   1.614 +    apply (drule_tac x="n" in spec)
   1.615 +    apply (drule (1) mp)
   1.616 +    apply (drule_tac x="m" in spec)
   1.617 +    apply (drule (1) mp)
   1.618 +    apply (simp_all add: setsum_diff [symmetric])
   1.619 +  apply (drule spec)
   1.620 +  apply (drule (1) mp)
   1.621 +  apply (erule exE)
   1.622 +  apply (rule_tac x="N" in exI)
   1.623 +  apply clarify
   1.624    apply (rule_tac x="m" and y="n" in linorder_le_cases)
   1.625 -  apply (frule (1) order_trans)
   1.626 -  apply (drule_tac x="n" in spec, drule (1) mp)
   1.627 -  apply (drule_tac x="m" in spec, drule (1) mp)
   1.628 -  apply (simp_all add: setsum_diff [symmetric])
   1.629 -  apply (drule spec, drule (1) mp)
   1.630 -  apply (erule exE, rule_tac x="N" in exI, clarify)
   1.631 -  apply (rule_tac x="m" and y="n" in linorder_le_cases)
   1.632 -  apply (subst norm_minus_commute)
   1.633 -  apply (simp_all add: setsum_diff [symmetric])
   1.634 +   apply (subst norm_minus_commute)
   1.635 +   apply (simp_all add: setsum_diff [symmetric])
   1.636    done
   1.637  
   1.638  context
   1.639    fixes f :: "nat \<Rightarrow> 'a::banach"
   1.640  begin
   1.641  
   1.642 -text\<open>Absolute convergence imples normal convergence\<close>
   1.643 +text \<open>Absolute convergence imples normal convergence.\<close>
   1.644  
   1.645  lemma summable_norm_cancel: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f"
   1.646 -  apply (simp only: summable_Cauchy, safe)
   1.647 -  apply (drule_tac x="e" in spec, safe)
   1.648 -  apply (rule_tac x="N" in exI, safe)
   1.649 -  apply (drule_tac x="m" in spec, safe)
   1.650 +  apply (simp only: summable_Cauchy)
   1.651 +  apply safe
   1.652 +  apply (drule_tac x="e" in spec)
   1.653 +  apply safe
   1.654 +  apply (rule_tac x="N" in exI)
   1.655 +  apply safe
   1.656 +  apply (drule_tac x="m" in spec)
   1.657 +  apply safe
   1.658    apply (rule order_le_less_trans [OF norm_setsum])
   1.659    apply (rule order_le_less_trans [OF abs_ge_self])
   1.660    apply simp
   1.661 @@ -666,99 +702,117 @@
   1.662  lemma summable_norm: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))"
   1.663    by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel summable_LIMSEQ norm_setsum)
   1.664  
   1.665 -text \<open>Comparison tests\<close>
   1.666 +text \<open>Comparison tests.\<close>
   1.667  
   1.668  lemma summable_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable f"
   1.669 -  apply (simp add: summable_Cauchy, safe)
   1.670 -  apply (drule_tac x="e" in spec, safe)
   1.671 -  apply (rule_tac x = "N + Na" in exI, safe)
   1.672 +  apply (simp add: summable_Cauchy)
   1.673 +  apply safe
   1.674 +  apply (drule_tac x="e" in spec)
   1.675 +  apply safe
   1.676 +  apply (rule_tac x = "N + Na" in exI)
   1.677 +  apply safe
   1.678    apply (rotate_tac 2)
   1.679    apply (drule_tac x = m in spec)
   1.680 -  apply (auto, rotate_tac 2, drule_tac x = n in spec)
   1.681 +  apply auto
   1.682 +  apply (rotate_tac 2)
   1.683 +  apply (drule_tac x = n in spec)
   1.684    apply (rule_tac y = "\<Sum>k=m..<n. norm (f k)" in order_le_less_trans)
   1.685 -  apply (rule norm_setsum)
   1.686 +   apply (rule norm_setsum)
   1.687    apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
   1.688 -  apply (auto intro: setsum_mono simp add: abs_less_iff)
   1.689 +   apply (auto intro: setsum_mono simp add: abs_less_iff)
   1.690    done
   1.691  
   1.692  lemma summable_comparison_test_ev:
   1.693 -  shows "eventually (\<lambda>n. norm (f n) \<le> g n) sequentially \<Longrightarrow> summable g \<Longrightarrow> summable f"
   1.694 +  "eventually (\<lambda>n. norm (f n) \<le> g n) sequentially \<Longrightarrow> summable g \<Longrightarrow> summable f"
   1.695    by (rule summable_comparison_test) (auto simp: eventually_at_top_linorder)
   1.696  
   1.697 -(*A better argument order*)
   1.698 -lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
   1.699 +text \<open>A better argument order.\<close>
   1.700 +lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm (f n) \<le> g n) \<Longrightarrow> summable f"
   1.701    by (rule summable_comparison_test) auto
   1.702  
   1.703 +
   1.704  subsection \<open>The Ratio Test\<close>
   1.705  
   1.706  lemma summable_ratio_test:
   1.707    assumes "c < 1" "\<And>n. n \<ge> N \<Longrightarrow> norm (f (Suc n)) \<le> c * norm (f n)"
   1.708    shows "summable f"
   1.709 -proof cases
   1.710 -  assume "0 < c"
   1.711 +proof (cases "0 < c")
   1.712 +  case True
   1.713    show "summable f"
   1.714    proof (rule summable_comparison_test)
   1.715      show "\<exists>N'. \<forall>n\<ge>N'. norm (f n) \<le> (norm (f N) / (c ^ N)) * c ^ n"
   1.716      proof (intro exI allI impI)
   1.717 -      fix n assume "N \<le> n" then show "norm (f n) \<le> (norm (f N) / (c ^ N)) * c ^ n"
   1.718 +      fix n
   1.719 +      assume "N \<le> n"
   1.720 +      then show "norm (f n) \<le> (norm (f N) / (c ^ N)) * c ^ n"
   1.721        proof (induct rule: inc_induct)
   1.722 +        case base
   1.723 +        with True show ?case by simp
   1.724 +      next
   1.725          case (step m)
   1.726 -        moreover have "norm (f (Suc m)) / c ^ Suc m * c ^ n \<le> norm (f m) / c ^ m * c ^ n"
   1.727 +        have "norm (f (Suc m)) / c ^ Suc m * c ^ n \<le> norm (f m) / c ^ m * c ^ n"
   1.728            using \<open>0 < c\<close> \<open>c < 1\<close> assms(2)[OF \<open>N \<le> m\<close>] by (simp add: field_simps)
   1.729 -        ultimately show ?case by simp
   1.730 -      qed (insert \<open>0 < c\<close>, simp)
   1.731 +        with step show ?case by simp
   1.732 +      qed
   1.733      qed
   1.734      show "summable (\<lambda>n. norm (f N) / c ^ N * c ^ n)"
   1.735        using \<open>0 < c\<close> \<open>c < 1\<close> by (intro summable_mult summable_geometric) simp
   1.736    qed
   1.737  next
   1.738 -  assume c: "\<not> 0 < c"
   1.739 -  { fix n assume "n \<ge> N"
   1.740 -    then have "norm (f (Suc n)) \<le> c * norm (f n)"
   1.741 -      by fact
   1.742 +  case False
   1.743 +  have "f (Suc n) = 0" if "n \<ge> N" for n
   1.744 +  proof -
   1.745 +    from that have "norm (f (Suc n)) \<le> c * norm (f n)"
   1.746 +      by (rule assms(2))
   1.747      also have "\<dots> \<le> 0"
   1.748 -      using c by (simp add: not_less mult_nonpos_nonneg)
   1.749 -    finally have "f (Suc n) = 0"
   1.750 -      by auto }
   1.751 +      using False by (simp add: not_less mult_nonpos_nonneg)
   1.752 +    finally show ?thesis
   1.753 +      by auto
   1.754 +  qed
   1.755    then show "summable f"
   1.756      by (intro sums_summable[OF sums_finite, of "{.. Suc N}"]) (auto simp: not_le Suc_less_eq2)
   1.757  qed
   1.758  
   1.759  end
   1.760  
   1.761 -text\<open>Relations among convergence and absolute convergence for power series.\<close>
   1.762 +
   1.763 +text \<open>Relations among convergence and absolute convergence for power series.\<close>
   1.764  
   1.765  lemma Abel_lemma:
   1.766    fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
   1.767 -  assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm (a n) * r0^n \<le> M"
   1.768 -    shows "summable (\<lambda>n. norm (a n) * r^n)"
   1.769 +  assumes r: "0 \<le> r"
   1.770 +    and r0: "r < r0"
   1.771 +    and M: "\<And>n. norm (a n) * r0^n \<le> M"
   1.772 +  shows "summable (\<lambda>n. norm (a n) * r^n)"
   1.773  proof (rule summable_comparison_test')
   1.774    show "summable (\<lambda>n. M * (r / r0) ^ n)"
   1.775      using assms
   1.776      by (auto simp add: summable_mult summable_geometric)
   1.777 -next
   1.778 -  fix n
   1.779 -  show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n"
   1.780 +  show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n" for n
   1.781      using r r0 M [of n]
   1.782      apply (auto simp add: abs_mult field_simps)
   1.783 -    apply (cases "r=0", simp)
   1.784 -    apply (cases n, auto)
   1.785 +    apply (cases "r = 0")
   1.786 +     apply simp
   1.787 +     apply (cases n)
   1.788 +      apply auto
   1.789      done
   1.790  qed
   1.791  
   1.792  
   1.793 -text\<open>Summability of geometric series for real algebras\<close>
   1.794 +text \<open>Summability of geometric series for real algebras.\<close>
   1.795  
   1.796  lemma complete_algebra_summable_geometric:
   1.797    fixes x :: "'a::{real_normed_algebra_1,banach}"
   1.798 -  shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)"
   1.799 +  assumes "norm x < 1"
   1.800 +  shows "summable (\<lambda>n. x ^ n)"
   1.801  proof (rule summable_comparison_test)
   1.802    show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n"
   1.803      by (simp add: norm_power_ineq)
   1.804 -  show "norm x < 1 \<Longrightarrow> summable (\<lambda>n. norm x ^ n)"
   1.805 +  from assms show "summable (\<lambda>n. norm x ^ n)"
   1.806      by (simp add: summable_geometric)
   1.807  qed
   1.808  
   1.809 +
   1.810  subsection \<open>Cauchy Product Formula\<close>
   1.811  
   1.812  text \<open>
   1.813 @@ -769,7 +823,7 @@
   1.814  lemma Cauchy_product_sums:
   1.815    fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   1.816    assumes a: "summable (\<lambda>k. norm (a k))"
   1.817 -  assumes b: "summable (\<lambda>k. norm (b k))"
   1.818 +    and b: "summable (\<lambda>k. norm (b k))"
   1.819    shows "(\<lambda>k. \<Sum>i\<le>k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))"
   1.820  proof -
   1.821    let ?S1 = "\<lambda>n::nat. {..<n} \<times> {..<n}"
   1.822 @@ -782,97 +836,103 @@
   1.823  
   1.824    let ?g = "\<lambda>(i,j). a i * b j"
   1.825    let ?f = "\<lambda>(i,j). norm (a i) * norm (b j)"
   1.826 -  have f_nonneg: "\<And>x. 0 \<le> ?f x" by (auto)
   1.827 -  hence norm_setsum_f: "\<And>A. norm (setsum ?f A) = setsum ?f A"
   1.828 +  have f_nonneg: "\<And>x. 0 \<le> ?f x" by auto
   1.829 +  then have norm_setsum_f: "\<And>A. norm (setsum ?f A) = setsum ?f A"
   1.830      unfolding real_norm_def
   1.831      by (simp only: abs_of_nonneg setsum_nonneg [rule_format])
   1.832  
   1.833    have "(\<lambda>n. (\<Sum>k<n. a k) * (\<Sum>k<n. b k)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.834      by (intro tendsto_mult summable_LIMSEQ summable_norm_cancel [OF a] summable_norm_cancel [OF b])
   1.835 -  hence 1: "(\<lambda>n. setsum ?g (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.836 +  then have 1: "(\<lambda>n. setsum ?g (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.837      by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan)
   1.838  
   1.839    have "(\<lambda>n. (\<Sum>k<n. norm (a k)) * (\<Sum>k<n. norm (b k))) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
   1.840      using a b by (intro tendsto_mult summable_LIMSEQ)
   1.841 -  hence "(\<lambda>n. setsum ?f (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
   1.842 +  then have "(\<lambda>n. setsum ?f (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))"
   1.843      by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan)
   1.844 -  hence "convergent (\<lambda>n. setsum ?f (?S1 n))"
   1.845 +  then have "convergent (\<lambda>n. setsum ?f (?S1 n))"
   1.846      by (rule convergentI)
   1.847 -  hence Cauchy: "Cauchy (\<lambda>n. setsum ?f (?S1 n))"
   1.848 +  then have Cauchy: "Cauchy (\<lambda>n. setsum ?f (?S1 n))"
   1.849      by (rule convergent_Cauchy)
   1.850    have "Zfun (\<lambda>n. setsum ?f (?S1 n - ?S2 n)) sequentially"
   1.851    proof (rule ZfunI, simp only: eventually_sequentially norm_setsum_f)
   1.852      fix r :: real
   1.853      assume r: "0 < r"
   1.854      from CauchyD [OF Cauchy r] obtain N
   1.855 -    where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (setsum ?f (?S1 m) - setsum ?f (?S1 n)) < r" ..
   1.856 -    hence "\<And>m n. \<lbrakk>N \<le> n; n \<le> m\<rbrakk> \<Longrightarrow> norm (setsum ?f (?S1 m - ?S1 n)) < r"
   1.857 +      where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (setsum ?f (?S1 m) - setsum ?f (?S1 n)) < r" ..
   1.858 +    then have "\<And>m n. N \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> norm (setsum ?f (?S1 m - ?S1 n)) < r"
   1.859        by (simp only: setsum_diff finite_S1 S1_mono)
   1.860 -    hence N: "\<And>m n. \<lbrakk>N \<le> n; n \<le> m\<rbrakk> \<Longrightarrow> setsum ?f (?S1 m - ?S1 n) < r"
   1.861 +    then have N: "\<And>m n. N \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> setsum ?f (?S1 m - ?S1 n) < r"
   1.862        by (simp only: norm_setsum_f)
   1.863      show "\<exists>N. \<forall>n\<ge>N. setsum ?f (?S1 n - ?S2 n) < r"
   1.864      proof (intro exI allI impI)
   1.865 -      fix n assume "2 * N \<le> n"
   1.866 -      hence n: "N \<le> n div 2" by simp
   1.867 +      fix n
   1.868 +      assume "2 * N \<le> n"
   1.869 +      then have n: "N \<le> n div 2" by simp
   1.870        have "setsum ?f (?S1 n - ?S2 n) \<le> setsum ?f (?S1 n - ?S1 (n div 2))"
   1.871 -        by (intro setsum_mono2 finite_Diff finite_S1 f_nonneg
   1.872 -                  Diff_mono subset_refl S1_le_S2)
   1.873 +        by (intro setsum_mono2 finite_Diff finite_S1 f_nonneg Diff_mono subset_refl S1_le_S2)
   1.874        also have "\<dots> < r"
   1.875          using n div_le_dividend by (rule N)
   1.876        finally show "setsum ?f (?S1 n - ?S2 n) < r" .
   1.877      qed
   1.878    qed
   1.879 -  hence "Zfun (\<lambda>n. setsum ?g (?S1 n - ?S2 n)) sequentially"
   1.880 +  then have "Zfun (\<lambda>n. setsum ?g (?S1 n - ?S2 n)) sequentially"
   1.881      apply (rule Zfun_le [rule_format])
   1.882      apply (simp only: norm_setsum_f)
   1.883      apply (rule order_trans [OF norm_setsum setsum_mono])
   1.884      apply (auto simp add: norm_mult_ineq)
   1.885      done
   1.886 -  hence 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) \<longlonglongrightarrow> 0"
   1.887 +  then have 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) \<longlonglongrightarrow> 0"
   1.888      unfolding tendsto_Zfun_iff diff_0_right
   1.889      by (simp only: setsum_diff finite_S1 S2_le_S1)
   1.890 -
   1.891    with 1 have "(\<lambda>n. setsum ?g (?S2 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
   1.892      by (rule Lim_transform2)
   1.893 -  thus ?thesis by (simp only: sums_def setsum_triangle_reindex)
   1.894 +  then show ?thesis
   1.895 +    by (simp only: sums_def setsum_triangle_reindex)
   1.896  qed
   1.897  
   1.898  lemma Cauchy_product:
   1.899    fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   1.900 -  assumes a: "summable (\<lambda>k. norm (a k))"
   1.901 -  assumes b: "summable (\<lambda>k. norm (b k))"
   1.902 +  assumes "summable (\<lambda>k. norm (a k))"
   1.903 +    and "summable (\<lambda>k. norm (b k))"
   1.904    shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i\<le>k. a i * b (k - i))"
   1.905 -  using a b
   1.906 -  by (rule Cauchy_product_sums [THEN sums_unique])
   1.907 +  using assms by (rule Cauchy_product_sums [THEN sums_unique])
   1.908  
   1.909  lemma summable_Cauchy_product:
   1.910 -  assumes "summable (\<lambda>k. norm (a k :: 'a :: {real_normed_algebra,banach}))"
   1.911 -          "summable (\<lambda>k. norm (b k))"
   1.912 -  shows   "summable (\<lambda>k. \<Sum>i\<le>k. a i * b (k - i))"
   1.913 +  fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   1.914 +  assumes "summable (\<lambda>k. norm (a k))"
   1.915 +    and "summable (\<lambda>k. norm (b k))"
   1.916 +  shows "summable (\<lambda>k. \<Sum>i\<le>k. a i * b (k - i))"
   1.917    using Cauchy_product_sums[OF assms] by (simp add: sums_iff)
   1.918  
   1.919 +
   1.920  subsection \<open>Series on @{typ real}s\<close>
   1.921  
   1.922 -lemma summable_norm_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))"
   1.923 +lemma summable_norm_comparison_test:
   1.924 +  "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))"
   1.925    by (rule summable_comparison_test) auto
   1.926  
   1.927 -lemma summable_rabs_comparison_test: "\<lbrakk>\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. \<bar>f n :: real\<bar>)"
   1.928 +lemma summable_rabs_comparison_test: "\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. \<bar>f n\<bar>)"
   1.929 +  for f :: "nat \<Rightarrow> real"
   1.930    by (rule summable_comparison_test) auto
   1.931  
   1.932 -lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
   1.933 +lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> summable f"
   1.934 +  for f :: "nat \<Rightarrow> real"
   1.935    by (rule summable_norm_cancel) simp
   1.936  
   1.937 -lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
   1.938 +lemma summable_rabs: "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
   1.939 +  for f :: "nat \<Rightarrow> real"
   1.940    by (fold real_norm_def) (rule summable_norm)
   1.941  
   1.942 -lemma summable_zero_power [simp]: "summable (\<lambda>n. 0 ^ n :: 'a :: {comm_ring_1,topological_space})"
   1.943 +lemma summable_zero_power [simp]: "summable (\<lambda>n. 0 ^ n :: 'a::{comm_ring_1,topological_space})"
   1.944  proof -
   1.945 -  have "(\<lambda>n. 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then 0^0 else 0)" by (intro ext) (simp add: zero_power)
   1.946 +  have "(\<lambda>n. 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then 0^0 else 0)"
   1.947 +    by (intro ext) (simp add: zero_power)
   1.948    moreover have "summable \<dots>" by simp
   1.949    ultimately show ?thesis by simp
   1.950  qed
   1.951  
   1.952 -lemma summable_zero_power' [simp]: "summable (\<lambda>n. f n * 0 ^ n :: 'a :: {ring_1,topological_space})"
   1.953 +lemma summable_zero_power' [simp]: "summable (\<lambda>n. f n * 0 ^ n :: 'a::{ring_1,topological_space})"
   1.954  proof -
   1.955    have "(\<lambda>n. f n * 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then f 0 * 0^0 else 0)"
   1.956      by (intro ext) (simp add: zero_power)
   1.957 @@ -882,33 +942,37 @@
   1.958  
   1.959  lemma summable_power_series:
   1.960    fixes z :: real
   1.961 -  assumes le_1: "\<And>i. f i \<le> 1" and nonneg: "\<And>i. 0 \<le> f i" and z: "0 \<le> z" "z < 1"
   1.962 +  assumes le_1: "\<And>i. f i \<le> 1"
   1.963 +    and nonneg: "\<And>i. 0 \<le> f i"
   1.964 +    and z: "0 \<le> z" "z < 1"
   1.965    shows "summable (\<lambda>i. f i * z^i)"
   1.966  proof (rule summable_comparison_test[OF _ summable_geometric])
   1.967 -  show "norm z < 1" using z by (auto simp: less_imp_le)
   1.968 +  show "norm z < 1"
   1.969 +    using z by (auto simp: less_imp_le)
   1.970    show "\<And>n. \<exists>N. \<forall>na\<ge>N. norm (f na * z ^ na) \<le> z ^ na"
   1.971 -    using z by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1)
   1.972 +    using z
   1.973 +    by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1)
   1.974  qed
   1.975  
   1.976 -lemma summable_0_powser:
   1.977 -  "summable (\<lambda>n. f n * 0 ^ n :: 'a :: real_normed_div_algebra)"
   1.978 +lemma summable_0_powser: "summable (\<lambda>n. f n * 0 ^ n :: 'a::real_normed_div_algebra)"
   1.979  proof -
   1.980    have A: "(\<lambda>n. f n * 0 ^ n) = (\<lambda>n. if n = 0 then f n else 0)"
   1.981      by (intro ext) auto
   1.982 -  thus ?thesis by (subst A) simp_all
   1.983 +  then show ?thesis
   1.984 +    by (subst A) simp_all
   1.985  qed
   1.986  
   1.987  lemma summable_powser_split_head:
   1.988 -  "summable (\<lambda>n. f (Suc n) * z ^ n :: 'a :: real_normed_div_algebra) = summable (\<lambda>n. f n * z ^ n)"
   1.989 +  "summable (\<lambda>n. f (Suc n) * z ^ n :: 'a::real_normed_div_algebra) = summable (\<lambda>n. f n * z ^ n)"
   1.990  proof -
   1.991    have "summable (\<lambda>n. f (Suc n) * z ^ n) \<longleftrightarrow> summable (\<lambda>n. f (Suc n) * z ^ Suc n)"
   1.992 +    (is "?lhs \<longleftrightarrow> ?rhs")
   1.993    proof
   1.994 -    assume "summable (\<lambda>n. f (Suc n) * z ^ n)"
   1.995 -    from summable_mult2[OF this, of z] show "summable (\<lambda>n. f (Suc n) * z ^ Suc n)"
   1.996 +    show ?rhs if ?lhs
   1.997 +      using summable_mult2[OF that, of z]
   1.998        by (simp add: power_commutes algebra_simps)
   1.999 -  next
  1.1000 -    assume "summable (\<lambda>n. f (Suc n) * z ^ Suc n)"
  1.1001 -    from summable_mult2[OF this, of "inverse z"] show "summable (\<lambda>n. f (Suc n) * z ^ n)"
  1.1002 +    show ?lhs if ?rhs
  1.1003 +      using summable_mult2[OF that, of "inverse z"]
  1.1004        by (cases "z \<noteq> 0", subst (asm) power_Suc2) (simp_all add: algebra_simps)
  1.1005    qed
  1.1006    also have "\<dots> \<longleftrightarrow> summable (\<lambda>n. f n * z ^ n)" by (rule summable_Suc_iff)
  1.1007 @@ -916,120 +980,133 @@
  1.1008  qed
  1.1009  
  1.1010  lemma powser_split_head:
  1.1011 -  assumes "summable (\<lambda>n. f n * z ^ n :: 'a :: {real_normed_div_algebra,banach})"
  1.1012 -  shows   "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z"
  1.1013 -          "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0"
  1.1014 -          "summable (\<lambda>n. f (Suc n) * z ^ n)"
  1.1015 +  fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
  1.1016 +  assumes "summable (\<lambda>n. f n * z ^ n)"
  1.1017 +  shows "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z"
  1.1018 +    and "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0"
  1.1019 +    and "summable (\<lambda>n. f (Suc n) * z ^ n)"
  1.1020  proof -
  1.1021 -  from assms show "summable (\<lambda>n. f (Suc n) * z ^ n)" by (subst summable_powser_split_head)
  1.1022 -
  1.1023 +  from assms show "summable (\<lambda>n. f (Suc n) * z ^ n)"
  1.1024 +    by (subst summable_powser_split_head)
  1.1025    from suminf_mult2[OF this, of z]
  1.1026      have "(\<Sum>n. f (Suc n) * z ^ n) * z = (\<Sum>n. f (Suc n) * z ^ Suc n)"
  1.1027      by (simp add: power_commutes algebra_simps)
  1.1028    also from assms have "\<dots> = suminf (\<lambda>n. f n * z ^ n) - f 0"
  1.1029      by (subst suminf_split_head) simp_all
  1.1030 -  finally show "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z" by simp
  1.1031 -  thus "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0" by simp
  1.1032 +  finally show "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z"
  1.1033 +    by simp
  1.1034 +  then show "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0"
  1.1035 +    by simp
  1.1036  qed
  1.1037  
  1.1038  lemma summable_partial_sum_bound:
  1.1039    fixes f :: "nat \<Rightarrow> 'a :: banach"
  1.1040 -  assumes summable: "summable f" and e: "e > (0::real)"
  1.1041 +    and e :: real
  1.1042 +  assumes summable: "summable f"
  1.1043 +    and e: "e > 0"
  1.1044    obtains N where "\<And>m n. m \<ge> N \<Longrightarrow> norm (\<Sum>k=m..n. f k) < e"
  1.1045  proof -
  1.1046    from summable have "Cauchy (\<lambda>n. \<Sum>k<n. f k)"
  1.1047      by (simp add: Cauchy_convergent_iff summable_iff_convergent)
  1.1048 -  from CauchyD[OF this e] obtain N
  1.1049 -    where N: "\<And>m n. m \<ge> N \<Longrightarrow> n \<ge> N \<Longrightarrow> norm ((\<Sum>k<m. f k) - (\<Sum>k<n. f k)) < e" by blast
  1.1050 -  {
  1.1051 -    fix m n :: nat assume m: "m \<ge> N"
  1.1052 -    have "norm (\<Sum>k=m..n. f k) < e"
  1.1053 -    proof (cases "n \<ge> m")
  1.1054 -      assume n: "n \<ge> m"
  1.1055 -      with m have "norm ((\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k)) < e" by (intro N) simp_all
  1.1056 -      also from n have "(\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k) = (\<Sum>k=m..n. f k)"
  1.1057 -        by (subst setsum_diff [symmetric]) (simp_all add: setsum_last_plus)
  1.1058 -      finally show ?thesis .
  1.1059 -    qed (insert e, simp_all)
  1.1060 -  }
  1.1061 -  thus ?thesis by (rule that)
  1.1062 +  from CauchyD [OF this e] obtain N
  1.1063 +    where N: "\<And>m n. m \<ge> N \<Longrightarrow> n \<ge> N \<Longrightarrow> norm ((\<Sum>k<m. f k) - (\<Sum>k<n. f k)) < e"
  1.1064 +    by blast
  1.1065 +  have "norm (\<Sum>k=m..n. f k) < e" if m: "m \<ge> N" for m n
  1.1066 +  proof (cases "n \<ge> m")
  1.1067 +    case True
  1.1068 +    with m have "norm ((\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k)) < e"
  1.1069 +      by (intro N) simp_all
  1.1070 +    also from True have "(\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k) = (\<Sum>k=m..n. f k)"
  1.1071 +      by (subst setsum_diff [symmetric]) (simp_all add: setsum_last_plus)
  1.1072 +    finally show ?thesis .
  1.1073 +  next
  1.1074 +    case False
  1.1075 +    with e show ?thesis by simp_all
  1.1076 +  qed
  1.1077 +  then show ?thesis by (rule that)
  1.1078  qed
  1.1079  
  1.1080  lemma powser_sums_if:
  1.1081 -  "(\<lambda>n. (if n = m then (1 :: 'a :: {ring_1,topological_space}) else 0) * z^n) sums z^m"
  1.1082 +  "(\<lambda>n. (if n = m then (1 :: 'a::{ring_1,topological_space}) else 0) * z^n) sums z^m"
  1.1083  proof -
  1.1084    have "(\<lambda>n. (if n = m then 1 else 0) * z^n) = (\<lambda>n. if n = m then z^n else 0)"
  1.1085      by (intro ext) auto
  1.1086 -  thus ?thesis by (simp add: sums_single)
  1.1087 +  then show ?thesis
  1.1088 +    by (simp add: sums_single)
  1.1089  qed
  1.1090  
  1.1091  lemma
  1.1092 -   fixes f :: "nat \<Rightarrow> real"
  1.1093 -   assumes "summable f"
  1.1094 -   and "inj g"
  1.1095 -   and pos: "\<And>x. 0 \<le> f x"
  1.1096 -   shows summable_reindex: "summable (f o g)"
  1.1097 -   and suminf_reindex_mono: "suminf (f o g) \<le> suminf f"
  1.1098 -   and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f"
  1.1099 +  fixes f :: "nat \<Rightarrow> real"
  1.1100 +  assumes "summable f"
  1.1101 +    and "inj g"
  1.1102 +    and pos: "\<And>x. 0 \<le> f x"
  1.1103 +  shows summable_reindex: "summable (f \<circ> g)"
  1.1104 +    and suminf_reindex_mono: "suminf (f \<circ> g) \<le> suminf f"
  1.1105 +    and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f"
  1.1106  proof -
  1.1107 -  from \<open>inj g\<close> have [simp]: "\<And>A. inj_on g A" by(rule subset_inj_on) simp
  1.1108 +  from \<open>inj g\<close> have [simp]: "\<And>A. inj_on g A"
  1.1109 +    by (rule subset_inj_on) simp
  1.1110  
  1.1111    have smaller: "\<forall>n. (\<Sum>i<n. (f \<circ> g) i) \<le> suminf f"
  1.1112    proof
  1.1113      fix n
  1.1114      have "\<forall> n' \<in> (g ` {..<n}). n' < Suc (Max (g ` {..<n}))"
  1.1115 -      by(metis Max_ge finite_imageI finite_lessThan not_le not_less_eq)
  1.1116 -    then obtain m where n: "\<And>n'. n' < n \<Longrightarrow> g n' < m" by blast
  1.1117 +      by (metis Max_ge finite_imageI finite_lessThan not_le not_less_eq)
  1.1118 +    then obtain m where n: "\<And>n'. n' < n \<Longrightarrow> g n' < m"
  1.1119 +      by blast
  1.1120  
  1.1121      have "(\<Sum>i<n. f (g i)) = setsum f (g ` {..<n})"
  1.1122        by (simp add: setsum.reindex)
  1.1123      also have "\<dots> \<le> (\<Sum>i<m. f i)"
  1.1124        by (rule setsum_mono3) (auto simp add: pos n[rule_format])
  1.1125      also have "\<dots> \<le> suminf f"
  1.1126 -      using \<open>summable f\<close>
  1.1127 -      by (rule setsum_le_suminf) (simp add: pos)
  1.1128 -    finally show "(\<Sum>i<n. (f \<circ>  g) i) \<le> suminf f" by simp
  1.1129 +      using \<open>summable f\<close> by (rule setsum_le_suminf) (simp add: pos)
  1.1130 +    finally show "(\<Sum>i<n. (f \<circ>  g) i) \<le> suminf f"
  1.1131 +      by simp
  1.1132    qed
  1.1133  
  1.1134    have "incseq (\<lambda>n. \<Sum>i<n. (f \<circ> g) i)"
  1.1135      by (rule incseq_SucI) (auto simp add: pos)
  1.1136    then obtain  L where L: "(\<lambda> n. \<Sum>i<n. (f \<circ> g) i) \<longlonglongrightarrow> L"
  1.1137      using smaller by(rule incseq_convergent)
  1.1138 -  hence "(f \<circ> g) sums L" by (simp add: sums_def)
  1.1139 -  thus "summable (f o g)" by (auto simp add: sums_iff)
  1.1140 +  then have "(f \<circ> g) sums L"
  1.1141 +    by (simp add: sums_def)
  1.1142 +  then show "summable (f \<circ> g)"
  1.1143 +    by (auto simp add: sums_iff)
  1.1144  
  1.1145 -  hence "(\<lambda>n. \<Sum>i<n. (f \<circ> g) i) \<longlonglongrightarrow> suminf (f \<circ> g)"
  1.1146 -    by(rule summable_LIMSEQ)
  1.1147 -  thus le: "suminf (f \<circ> g) \<le> suminf f"
  1.1148 +  then have "(\<lambda>n. \<Sum>i<n. (f \<circ> g) i) \<longlonglongrightarrow> suminf (f \<circ> g)"
  1.1149 +    by (rule summable_LIMSEQ)
  1.1150 +  then show le: "suminf (f \<circ> g) \<le> suminf f"
  1.1151      by(rule LIMSEQ_le_const2)(blast intro: smaller[rule_format])
  1.1152  
  1.1153    assume f: "\<And>x. x \<notin> range g \<Longrightarrow> f x = 0"
  1.1154  
  1.1155    from \<open>summable f\<close> have "suminf f \<le> suminf (f \<circ> g)"
  1.1156 -  proof(rule suminf_le_const)
  1.1157 +  proof (rule suminf_le_const)
  1.1158      fix n
  1.1159      have "\<forall> n' \<in> (g -` {..<n}). n' < Suc (Max (g -` {..<n}))"
  1.1160        by(auto intro: Max_ge simp add: finite_vimageI less_Suc_eq_le)
  1.1161 -    then obtain m where n: "\<And>n'. g n' < n \<Longrightarrow> n' < m" by blast
  1.1162 -
  1.1163 +    then obtain m where n: "\<And>n'. g n' < n \<Longrightarrow> n' < m"
  1.1164 +      by blast
  1.1165      have "(\<Sum>i<n. f i) = (\<Sum>i\<in>{..<n} \<inter> range g. f i)"
  1.1166        using f by(auto intro: setsum.mono_neutral_cong_right)
  1.1167      also have "\<dots> = (\<Sum>i\<in>g -` {..<n}. (f \<circ> g) i)"
  1.1168 -      by(rule setsum.reindex_cong[where l=g])(auto)
  1.1169 +      by (rule setsum.reindex_cong[where l=g])(auto)
  1.1170      also have "\<dots> \<le> (\<Sum>i<m. (f \<circ> g) i)"
  1.1171 -      by(rule setsum_mono3)(auto simp add: pos n)
  1.1172 +      by (rule setsum_mono3)(auto simp add: pos n)
  1.1173      also have "\<dots> \<le> suminf (f \<circ> g)"
  1.1174 -      using \<open>summable (f o g)\<close>
  1.1175 -      by(rule setsum_le_suminf)(simp add: pos)
  1.1176 +      using \<open>summable (f \<circ> g)\<close> by (rule setsum_le_suminf) (simp add: pos)
  1.1177      finally show "setsum f {..<n} \<le> suminf (f \<circ> g)" .
  1.1178    qed
  1.1179 -  with le show "suminf (f \<circ> g) = suminf f" by(rule antisym)
  1.1180 +  with le show "suminf (f \<circ> g) = suminf f"
  1.1181 +    by (rule antisym)
  1.1182  qed
  1.1183  
  1.1184  lemma sums_mono_reindex:
  1.1185 -  assumes subseq: "subseq g" and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
  1.1186 -  shows   "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c"
  1.1187 -unfolding sums_def
  1.1188 +  assumes subseq: "subseq g"
  1.1189 +    and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
  1.1190 +  shows "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c"
  1.1191 +  unfolding sums_def
  1.1192  proof
  1.1193    assume lim: "(\<lambda>n. \<Sum>k<n. f k) \<longlonglongrightarrow> c"
  1.1194    have "(\<lambda>n. \<Sum>k<n. f (g k)) = (\<lambda>n. \<Sum>k<g n. f k)"
  1.1195 @@ -1039,69 +1116,93 @@
  1.1196        by (subst setsum.reindex) (auto intro: subseq_imp_inj_on)
  1.1197      also from subseq have "\<dots> = (\<Sum>k<g n. f k)"
  1.1198        by (intro setsum.mono_neutral_left ballI zero)
  1.1199 -         (auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
  1.1200 +        (auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
  1.1201      finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" .
  1.1202    qed
  1.1203 -  also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c" unfolding o_def .
  1.1204 +  also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c"
  1.1205 +    by (simp only: o_def)
  1.1206    finally show "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c" .
  1.1207  next
  1.1208    assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c"
  1.1209    define g_inv where "g_inv n = (LEAST m. g m \<ge> n)" for n
  1.1210    from filterlim_subseq[OF subseq] have g_inv_ex: "\<exists>m. g m \<ge> n" for n
  1.1211      by (auto simp: filterlim_at_top eventually_at_top_linorder)
  1.1212 -  hence g_inv: "g (g_inv n) \<ge> n" for n unfolding g_inv_def by (rule LeastI_ex)
  1.1213 -  have g_inv_least: "m \<ge> g_inv n" if "g m \<ge> n" for m n using that
  1.1214 -    unfolding g_inv_def by (rule Least_le)
  1.1215 -  have g_inv_least': "g m < n" if "m < g_inv n" for m n using that g_inv_least[of n m] by linarith
  1.1216 +  then have g_inv: "g (g_inv n) \<ge> n" for n
  1.1217 +    unfolding g_inv_def by (rule LeastI_ex)
  1.1218 +  have g_inv_least: "m \<ge> g_inv n" if "g m \<ge> n" for m n
  1.1219 +    using that unfolding g_inv_def by (rule Least_le)
  1.1220 +  have g_inv_least': "g m < n" if "m < g_inv n" for m n
  1.1221 +    using that g_inv_least[of n m] by linarith
  1.1222    have "(\<lambda>n. \<Sum>k<n. f k) = (\<lambda>n. \<Sum>k<g_inv n. f (g k))"
  1.1223    proof
  1.1224      fix n :: nat
  1.1225      {
  1.1226 -      fix k assume k: "k \<in> {..<n} - g`{..<g_inv n}"
  1.1227 +      fix k
  1.1228 +      assume k: "k \<in> {..<n} - g`{..<g_inv n}"
  1.1229        have "k \<notin> range g"
  1.1230        proof (rule notI, elim imageE)
  1.1231 -        fix l assume l: "k = g l"
  1.1232 -        have "g l < g (g_inv n)" by (rule less_le_trans[OF _ g_inv]) (insert k l, simp_all)
  1.1233 -        with subseq have "l < g_inv n" by (simp add: subseq_strict_mono strict_mono_less)
  1.1234 -        with k l show False by simp
  1.1235 +        fix l
  1.1236 +        assume l: "k = g l"
  1.1237 +        have "g l < g (g_inv n)"
  1.1238 +          by (rule less_le_trans[OF _ g_inv]) (use k l in simp_all)
  1.1239 +        with subseq have "l < g_inv n"
  1.1240 +          by (simp add: subseq_strict_mono strict_mono_less)
  1.1241 +        with k l show False
  1.1242 +          by simp
  1.1243        qed
  1.1244 -      hence "f k = 0" by (rule zero)
  1.1245 +      then have "f k = 0"
  1.1246 +        by (rule zero)
  1.1247      }
  1.1248      with g_inv_least' g_inv have "(\<Sum>k<n. f k) = (\<Sum>k\<in>g`{..<g_inv n}. f k)"
  1.1249        by (intro setsum.mono_neutral_right) auto
  1.1250 -    also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))" using subseq_imp_inj_on
  1.1251 -      by (subst setsum.reindex) simp_all
  1.1252 +    also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))"
  1.1253 +      using subseq_imp_inj_on by (subst setsum.reindex) simp_all
  1.1254      finally show "(\<Sum>k<n. f k) = (\<Sum>k<g_inv n. f (g k))" .
  1.1255    qed
  1.1256    also {
  1.1257 -    fix K n :: nat assume "g K \<le> n"
  1.1258 -    also have "n \<le> g (g_inv n)" by (rule g_inv)
  1.1259 -    finally have "K \<le> g_inv n" using subseq by (simp add: strict_mono_less_eq subseq_strict_mono)
  1.1260 +    fix K n :: nat
  1.1261 +    assume "g K \<le> n"
  1.1262 +    also have "n \<le> g (g_inv n)"
  1.1263 +      by (rule g_inv)
  1.1264 +    finally have "K \<le> g_inv n"
  1.1265 +      using subseq by (simp add: strict_mono_less_eq subseq_strict_mono)
  1.1266    }
  1.1267 -  hence "filterlim g_inv at_top sequentially"
  1.1268 +  then have "filterlim g_inv at_top sequentially"
  1.1269      by (auto simp: filterlim_at_top eventually_at_top_linorder)
  1.1270 -  from lim and this have "(\<lambda>n. \<Sum>k<g_inv n. f (g k)) \<longlonglongrightarrow> c" by (rule filterlim_compose)
  1.1271 +  with lim have "(\<lambda>n. \<Sum>k<g_inv n. f (g k)) \<longlonglongrightarrow> c"
  1.1272 +    by (rule filterlim_compose)
  1.1273    finally show "(\<lambda>n. \<Sum>k<n. f k) \<longlonglongrightarrow> c" .
  1.1274  qed
  1.1275  
  1.1276  lemma summable_mono_reindex:
  1.1277 -  assumes subseq: "subseq g" and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
  1.1278 -  shows   "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f"
  1.1279 +  assumes subseq: "subseq g"
  1.1280 +    and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
  1.1281 +  shows "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f"
  1.1282    using sums_mono_reindex[of g f, OF assms] by (simp add: summable_def)
  1.1283  
  1.1284  lemma suminf_mono_reindex:
  1.1285 -  assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = (0 :: 'a :: {t2_space,comm_monoid_add})"
  1.1286 +  fixes f :: "nat \<Rightarrow> 'a::{t2_space,comm_monoid_add}"
  1.1287 +  assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
  1.1288    shows   "suminf (\<lambda>n. f (g n)) = suminf f"
  1.1289  proof (cases "summable f")
  1.1290 +  case True
  1.1291 +  with sums_mono_reindex [of g f, OF assms]
  1.1292 +    and summable_mono_reindex [of g f, OF assms]
  1.1293 +  show ?thesis
  1.1294 +    by (simp add: sums_iff)
  1.1295 +next
  1.1296    case False
  1.1297 -  hence "\<not>(\<exists>c. f sums c)" unfolding summable_def by blast
  1.1298 -  hence "suminf f = The (\<lambda>_. False)" by (simp add: suminf_def)
  1.1299 -  moreover from False have "\<not>summable (\<lambda>n. f (g n))"
  1.1300 +  then have "\<not>(\<exists>c. f sums c)"
  1.1301 +    unfolding summable_def by blast
  1.1302 +  then have "suminf f = The (\<lambda>_. False)"
  1.1303 +    by (simp add: suminf_def)
  1.1304 +  moreover from False have "\<not> summable (\<lambda>n. f (g n))"
  1.1305      using summable_mono_reindex[of g f, OF assms] by simp
  1.1306 -  hence "\<not>(\<exists>c. (\<lambda>n. f (g n)) sums c)" unfolding summable_def by blast
  1.1307 -  hence "suminf (\<lambda>n. f (g n)) = The (\<lambda>_. False)" by (simp add: suminf_def)
  1.1308 +  then have "\<not>(\<exists>c. (\<lambda>n. f (g n)) sums c)"
  1.1309 +    unfolding summable_def by blast
  1.1310 +  then have "suminf (\<lambda>n. f (g n)) = The (\<lambda>_. False)"
  1.1311 +    by (simp add: suminf_def)
  1.1312    ultimately show ?thesis by simp
  1.1313 -qed (insert sums_mono_reindex[of g f, OF assms] summable_mono_reindex[of g f, OF assms],
  1.1314 -     simp_all add: sums_iff)
  1.1315 +qed
  1.1316  
  1.1317  end