src/HOL/Series.thy
 changeset 56178 2a6f58938573 parent 54703 499f92dc6e45 child 56193 c726ecfb22b6
```     1.1 --- a/src/HOL/Series.thy	Mon Mar 17 14:40:59 2014 +0100
1.2 +++ b/src/HOL/Series.thy	Mon Mar 17 15:48:30 2014 +0000
1.3 @@ -562,6 +562,22 @@
1.4  apply simp
1.5  done
1.6
1.7 +lemma norm_bound_subset:
1.8 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.9 +  assumes "finite s" "t \<subseteq> s"
1.10 +  assumes le: "(\<And>x. x \<in> s \<Longrightarrow> norm(f x) \<le> g x)"
1.11 +  shows "norm (setsum f t) \<le> setsum g s"
1.12 +proof -
1.13 +  have "norm (setsum f t) \<le> (\<Sum>i\<in>t. norm (f i))"
1.14 +    by (rule norm_setsum)
1.15 +  also have "\<dots> \<le> (\<Sum>i\<in>t. g i)"
1.16 +    using assms by (auto intro!: setsum_mono)
1.17 +  also have "\<dots> \<le> setsum g s"
1.18 +    using assms order.trans[OF norm_ge_zero le]
1.19 +    by (auto intro!: setsum_mono3)
1.20 +  finally show ?thesis .
1.21 +qed
1.22 +
1.23  lemma summable_comparison_test:
1.24    fixes f :: "nat \<Rightarrow> 'a::banach"
1.25    shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f"
```