src/HOL/Real_Vector_Spaces.thy
changeset 60800 7d04351c795a
parent 60762 bf0c76ccee8d
child 61070 b72a990adfe2
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Jul 27 16:35:12 2015 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jul 27 16:52:57 2015 +0100
     1.3 @@ -228,6 +228,29 @@
     1.4  apply (erule (1) nonzero_inverse_scaleR_distrib)
     1.5  done
     1.6  
     1.7 +lemma real_vector_affinity_eq:
     1.8 +  fixes x :: "'a :: real_vector"
     1.9 +  assumes m0: "m \<noteq> 0"
    1.10 +  shows "m *\<^sub>R x + c = y \<longleftrightarrow> x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)"
    1.11 +proof
    1.12 +  assume h: "m *\<^sub>R x + c = y"
    1.13 +  hence "m *\<^sub>R x = y - c" by (simp add: field_simps)
    1.14 +  hence "inverse m *\<^sub>R (m *\<^sub>R x) = inverse m *\<^sub>R (y - c)" by simp
    1.15 +  then show "x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)"
    1.16 +    using m0
    1.17 +  by (simp add: real_vector.scale_right_diff_distrib)
    1.18 +next
    1.19 +  assume h: "x = inverse m *\<^sub>R y - (inverse m *\<^sub>R c)"
    1.20 +  show "m *\<^sub>R x + c = y" unfolding h
    1.21 +    using m0  by (simp add: real_vector.scale_right_diff_distrib)
    1.22 +qed
    1.23 +
    1.24 +lemma real_vector_eq_affinity:
    1.25 +  fixes x :: "'a :: real_vector"
    1.26 +  shows "m \<noteq> 0 ==> (y = m *\<^sub>R x + c \<longleftrightarrow> inverse m *\<^sub>R y - (inverse m *\<^sub>R c) = x)"
    1.27 +  using real_vector_affinity_eq[where m=m and x=x and y=y and c=c]
    1.28 +  by metis
    1.29 +
    1.30  
    1.31  subsection \<open>Embedding of the Reals into any @{text real_algebra_1}:
    1.32  @{term of_real}\<close>
    1.33 @@ -763,6 +786,18 @@
    1.34    finally show ?thesis .
    1.35  qed
    1.36  
    1.37 +lemma norm_diff_triangle_le:
    1.38 +  fixes x y z :: "'a::real_normed_vector"
    1.39 +  assumes "norm (x - y) \<le> e1"  "norm (y - z) \<le> e2"
    1.40 +    shows "norm (x - z) \<le> e1 + e2"
    1.41 +  using norm_diff_triangle_ineq [of x y y z] assms by simp
    1.42 +
    1.43 +lemma norm_diff_triangle_less:
    1.44 +  fixes x y z :: "'a::real_normed_vector"
    1.45 +  assumes "norm (x - y) < e1"  "norm (y - z) < e2"
    1.46 +    shows "norm (x - z) < e1 + e2"
    1.47 +  using norm_diff_triangle_ineq [of x y y z] assms by simp
    1.48 +
    1.49  lemma norm_triangle_mono:
    1.50    fixes a b :: "'a::real_normed_vector"
    1.51    shows "\<lbrakk>norm a \<le> r; norm b \<le> s\<rbrakk> \<Longrightarrow> norm (a + b) \<le> r + s"
    1.52 @@ -1123,6 +1158,11 @@
    1.53  
    1.54  end
    1.55  
    1.56 +lemma dist_of_real [simp]:
    1.57 +  fixes a :: "'a::real_normed_div_algebra"
    1.58 +  shows "dist (of_real x :: 'a) (of_real y) = dist x y"
    1.59 +by (metis dist_norm norm_of_real of_real_diff real_norm_def)
    1.60 +
    1.61  declare [[code abort: "open :: real set \<Rightarrow> bool"]]
    1.62  
    1.63  instance real :: linorder_topology
    1.64 @@ -1249,6 +1289,10 @@
    1.65  locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
    1.66    assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
    1.67  
    1.68 +lemma linear_imp_scaleR:
    1.69 +  assumes "linear D" obtains d where "D = (\<lambda>x. x *\<^sub>R d)"
    1.70 +  by (metis assms linear.scaleR mult.commute mult.left_neutral real_scaleR_def)
    1.71 +
    1.72  lemma linearI:
    1.73    assumes "\<And>x y. f (x + y) = f x + f y"
    1.74    assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
    1.75 @@ -1503,6 +1547,11 @@
    1.76      by (auto intro: exI[of _ "f 1"] bounded_linear_mult_left)
    1.77  qed
    1.78  
    1.79 +lemma bij_linear_imp_inv_linear:
    1.80 +  assumes "linear f" "bij f" shows "linear (inv f)"
    1.81 +  using assms unfolding linear_def linear_axioms_def additive_def
    1.82 +  by (auto simp: bij_is_surj bij_is_inj surj_f_inv_f intro!:  Hilbert_Choice.inv_f_eq)
    1.83 +    
    1.84  instance real_normed_algebra_1 \<subseteq> perfect_space
    1.85  proof
    1.86    fix x::'a