src/HOL/Series.thy
changeset 67167 88d1c9d86f48
parent 66456 621897f47fab
child 67268 bdf25939a550
     1.1 --- a/src/HOL/Series.thy	Mon Dec 11 17:28:32 2017 +0100
     1.2 +++ b/src/HOL/Series.thy	Tue Dec 12 10:01:14 2017 +0100
     1.3 @@ -1223,4 +1223,32 @@
     1.4    ultimately show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +lemma summable_bounded_partials:
     1.8 +  fixes f :: "nat \<Rightarrow> 'a :: {real_normed_vector,complete_space}"
     1.9 +  assumes bound: "eventually (\<lambda>x0. \<forall>a\<ge>x0. \<forall>b>a. norm (sum f {a<..b}) \<le> g a) sequentially"
    1.10 +  assumes g: "g \<longlonglongrightarrow> 0"
    1.11 +  shows   "summable f" unfolding summable_iff_convergent'
    1.12 +proof (intro Cauchy_convergent CauchyI', goal_cases)
    1.13 +  case (1 \<epsilon>)
    1.14 +  with g have "eventually (\<lambda>x. \<bar>g x\<bar> < \<epsilon>) sequentially"
    1.15 +    by (auto simp: tendsto_iff)
    1.16 +  from eventually_conj[OF this bound] obtain x0 where x0:
    1.17 +    "\<And>x. x \<ge> x0 \<Longrightarrow> \<bar>g x\<bar> < \<epsilon>" "\<And>a b. x0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> norm (sum f {a<..b}) \<le> g a" 
    1.18 +    unfolding eventually_at_top_linorder by auto
    1.19 +
    1.20 +  show ?case
    1.21 +  proof (intro exI[of _ x0] allI impI)
    1.22 +    fix m n assume mn: "x0 \<le> m" "m < n"
    1.23 +    have "dist (sum f {..m}) (sum f {..n}) = norm (sum f {..n} - sum f {..m})"
    1.24 +      by (simp add: dist_norm norm_minus_commute)
    1.25 +    also have "sum f {..n} - sum f {..m} = sum f ({..n} - {..m})"
    1.26 +      using mn by (intro Groups_Big.sum_diff [symmetric]) auto
    1.27 +    also have "{..n} - {..m} = {m<..n}" using mn by auto
    1.28 +    also have "norm (sum f {m<..n}) \<le> g m" using mn by (intro x0) auto
    1.29 +    also have "\<dots> \<le> \<bar>g m\<bar>" by simp
    1.30 +    also have "\<dots> < \<epsilon>" using mn by (intro x0) auto
    1.31 +    finally show "dist (sum f {..m}) (sum f {..n}) < \<epsilon>" .
    1.32 +  qed
    1.33 +qed
    1.34 +
    1.35  end