src/HOL/Real_Vector_Spaces.thy
changeset 56369 2704ca85be98
parent 56194 9ffbb4004c81
child 56409 36489d77c484
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Apr 02 17:47:56 2014 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Apr 02 18:35:01 2014 +0200
     1.3 @@ -752,6 +752,12 @@
     1.4    shows "norm (setsum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
     1.5    by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono)
     1.6  
     1.7 +lemma setsum_norm_le:
     1.8 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     1.9 +  assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
    1.10 +  shows "norm (setsum f S) \<le> setsum g S"
    1.11 +  by (rule order_trans [OF norm_setsum setsum_mono]) (simp add: fg)
    1.12 +
    1.13  lemma abs_norm_cancel [simp]:
    1.14    fixes a :: "'a::real_normed_vector"
    1.15    shows "\<bar>norm a\<bar> = norm a"
    1.16 @@ -1158,6 +1164,8 @@
    1.17    show ?thesis by (auto intro: order_less_imp_le)
    1.18  qed
    1.19  
    1.20 +lemma linear: "linear f" ..
    1.21 +
    1.22  end
    1.23  
    1.24  lemma bounded_linear_intro: