src/HOL/Real_Vector_Spaces.thy
changeset 55719 cdddd073bff8
parent 54890 cb892d835803
child 56194 9ffbb4004c81
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Feb 24 15:45:55 2014 +0000
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Feb 24 16:56:04 2014 +0000
     1.3 @@ -385,7 +385,7 @@
     1.4  apply (erule nonzero_of_real_inverse [symmetric])
     1.5  done
     1.6  
     1.7 -lemma Reals_inverse [simp]:
     1.8 +lemma Reals_inverse:
     1.9    fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}"
    1.10    shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
    1.11  apply (auto simp add: Reals_def)
    1.12 @@ -393,6 +393,11 @@
    1.13  apply (rule of_real_inverse [symmetric])
    1.14  done
    1.15  
    1.16 +lemma Reals_inverse_iff [simp]: 
    1.17 +  fixes x:: "'a :: {real_div_algebra, division_ring_inverse_zero}"
    1.18 +  shows "inverse x \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
    1.19 +by (metis Reals_inverse inverse_inverse_eq)
    1.20 +
    1.21  lemma nonzero_Reals_divide:
    1.22    fixes a b :: "'a::real_field"
    1.23    shows "\<lbrakk>a \<in> Reals; b \<in> Reals; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
    1.24 @@ -427,6 +432,24 @@
    1.25    then show thesis ..
    1.26  qed
    1.27  
    1.28 +lemma setsum_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
    1.29 +proof (cases "finite s")
    1.30 +  case True then show ?thesis using assms
    1.31 +    by (induct s rule: finite_induct) auto
    1.32 +next
    1.33 +  case False then show ?thesis using assms
    1.34 +    by (metis Reals_0 setsum_infinite)
    1.35 +qed
    1.36 +
    1.37 +lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
    1.38 +proof (cases "finite s")
    1.39 +  case True then show ?thesis using assms
    1.40 +    by (induct s rule: finite_induct) auto
    1.41 +next
    1.42 +  case False then show ?thesis using assms
    1.43 +    by (metis Reals_1 setprod_infinite)
    1.44 +qed
    1.45 +
    1.46  lemma Reals_induct [case_names of_real, induct set: Reals]:
    1.47    "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q"
    1.48    by (rule Reals_cases) auto
    1.49 @@ -719,6 +742,11 @@
    1.50    finally show ?thesis .
    1.51  qed
    1.52  
    1.53 +lemma norm_triangle_mono: 
    1.54 +  fixes a b :: "'a::real_normed_vector"
    1.55 +  shows "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> r + s"
    1.56 +by (metis add_mono_thms_linordered_semiring(1) norm_triangle_ineq order.trans)
    1.57 +
    1.58  lemma abs_norm_cancel [simp]:
    1.59    fixes a :: "'a::real_normed_vector"
    1.60    shows "\<bar>norm a\<bar> = norm a"
    1.61 @@ -802,6 +830,17 @@
    1.62    shows "norm (x ^ n) = norm x ^ n"
    1.63  by (induct n) (simp_all add: norm_mult)
    1.64  
    1.65 +lemma setprod_norm:
    1.66 +  fixes f :: "'a \<Rightarrow> 'b::{comm_semiring_1,real_normed_div_algebra}"
    1.67 +  shows "setprod (\<lambda>x. norm(f x)) A = norm (setprod f A)"
    1.68 +proof (cases "finite A")
    1.69 +  case True then show ?thesis 
    1.70 +    by (induct A rule: finite_induct) (auto simp: norm_mult)
    1.71 +next
    1.72 +  case False then show ?thesis
    1.73 +    by (metis norm_one setprod.infinite) 
    1.74 +qed
    1.75 +
    1.76  
    1.77  subsection {* Metric spaces *}
    1.78