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"