equal
deleted
inserted
replaced
559 apply simp |
559 apply simp |
560 apply simp |
560 apply simp |
561 apply (erule order_trans [OF norm_triangle_ineq add_left_mono]) |
561 apply (erule order_trans [OF norm_triangle_ineq add_left_mono]) |
562 apply simp |
562 apply simp |
563 done |
563 done |
|
564 |
|
565 lemma norm_bound_subset: |
|
566 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
|
567 assumes "finite s" "t \<subseteq> s" |
|
568 assumes le: "(\<And>x. x \<in> s \<Longrightarrow> norm(f x) \<le> g x)" |
|
569 shows "norm (setsum f t) \<le> setsum g s" |
|
570 proof - |
|
571 have "norm (setsum f t) \<le> (\<Sum>i\<in>t. norm (f i))" |
|
572 by (rule norm_setsum) |
|
573 also have "\<dots> \<le> (\<Sum>i\<in>t. g i)" |
|
574 using assms by (auto intro!: setsum_mono) |
|
575 also have "\<dots> \<le> setsum g s" |
|
576 using assms order.trans[OF norm_ge_zero le] |
|
577 by (auto intro!: setsum_mono3) |
|
578 finally show ?thesis . |
|
579 qed |
564 |
580 |
565 lemma summable_comparison_test: |
581 lemma summable_comparison_test: |
566 fixes f :: "nat \<Rightarrow> 'a::banach" |
582 fixes f :: "nat \<Rightarrow> 'a::banach" |
567 shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f" |
583 shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable f" |
568 apply (simp add: summable_Cauchy, safe) |
584 apply (simp add: summable_Cauchy, safe) |