src/HOL/Real/RealVector.thy
changeset 20533 49442b3024bb
parent 20504 6342e872e71d
child 20551 ba543692bfa1
equal deleted inserted replaced
20532:64181717e37c 20533:49442b3024bb
    86 
    86 
    87 
    87 
    88 subsection {* Real normed vector spaces *}
    88 subsection {* Real normed vector spaces *}
    89 
    89 
    90 axclass norm < type
    90 axclass norm < type
    91 consts norm :: "'a::norm \<Rightarrow> real" ("\<parallel>_\<parallel>")
    91 consts norm :: "'a::norm \<Rightarrow> real"
    92 
    92 
    93 axclass real_normed_vector < real_vector, norm
    93 axclass real_normed_vector < real_vector, norm
    94   norm_ge_zero [simp]: "0 \<le> \<parallel>x\<parallel>"
    94   norm_ge_zero [simp]: "0 \<le> norm x"
    95   norm_eq_zero [simp]: "(\<parallel>x\<parallel> = 0) = (x = 0)"
    95   norm_eq_zero [simp]: "(norm x = 0) = (x = 0)"
    96   norm_triangle_ineq: "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    96   norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
    97   norm_scaleR: "\<parallel>a *# x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
    97   norm_scaleR: "norm (a *# x) = \<bar>a\<bar> * norm x"
    98 
    98 
    99 axclass real_normed_algebra < real_normed_vector, real_algebra
    99 axclass real_normed_algebra < real_normed_vector, real_algebra
   100   norm_mult_ineq: "\<parallel>x * y\<parallel> \<le> \<parallel>x\<parallel> * \<parallel>y\<parallel>"
   100   norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
   101 
   101 
   102 axclass real_normed_div_algebra
   102 axclass real_normed_div_algebra
   103           < real_normed_vector, real_algebra, division_ring
   103           < real_normed_vector, real_algebra, division_ring
   104   norm_mult: "\<parallel>x * y\<parallel> = \<parallel>x\<parallel> * \<parallel>y\<parallel>"
   104   norm_mult: "norm (x * y) = norm x * norm y"
   105   norm_one [simp]: "\<parallel>1\<parallel> = 1"
   105   norm_one [simp]: "norm 1 = 1"
   106 
   106 
   107 instance real_normed_div_algebra < real_normed_algebra
   107 instance real_normed_div_algebra < real_normed_algebra
   108 by (intro_classes, simp add: norm_mult)
   108 by (intro_classes, simp add: norm_mult)
   109 
   109 
   110 lemma norm_zero [simp]: "\<parallel>0::'a::real_normed_vector\<parallel> = 0"
   110 lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0"
   111 by simp
   111 by simp
   112 
   112 
   113 lemma zero_less_norm_iff [simp]:
   113 lemma zero_less_norm_iff [simp]:
   114   fixes x :: "'a::real_normed_vector" shows "(0 < \<parallel>x\<parallel>) = (x \<noteq> 0)"
   114   fixes x :: "'a::real_normed_vector" shows "(0 < norm x) = (x \<noteq> 0)"
   115 by (simp add: order_less_le)
   115 by (simp add: order_less_le)
   116 
   116 
   117 lemma norm_minus_cancel [simp]:
   117 lemma norm_minus_cancel [simp]:
   118   fixes x :: "'a::real_normed_vector" shows "\<parallel>- x\<parallel> = \<parallel>x\<parallel>"
   118   fixes x :: "'a::real_normed_vector" shows "norm (- x) = norm x"
   119 proof -
   119 proof -
   120   have "\<parallel>- x\<parallel> = \<parallel>- 1 *# x\<parallel>"
   120   have "norm (- x) = norm (- 1 *# x)"
   121     by (simp only: scaleR_minus_left scaleR_one)
   121     by (simp only: scaleR_minus_left scaleR_one)
   122   also have "\<dots> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
   122   also have "\<dots> = \<bar>- 1\<bar> * norm x"
   123     by (rule norm_scaleR)
   123     by (rule norm_scaleR)
   124   finally show ?thesis by simp
   124   finally show ?thesis by simp
   125 qed
   125 qed
   126 
   126 
   127 lemma norm_minus_commute:
   127 lemma norm_minus_commute:
   128   fixes a b :: "'a::real_normed_vector" shows "\<parallel>a - b\<parallel> = \<parallel>b - a\<parallel>"
   128   fixes a b :: "'a::real_normed_vector" shows "norm (a - b) = norm (b - a)"
   129 proof -
   129 proof -
   130   have "\<parallel>a - b\<parallel> = \<parallel>-(a - b)\<parallel>" by (simp only: norm_minus_cancel)
   130   have "norm (a - b) = norm (- (a - b))"
   131   also have "\<dots> = \<parallel>b - a\<parallel>" by simp
   131     by (simp only: norm_minus_cancel)
       
   132   also have "\<dots> = norm (b - a)" by simp
   132   finally show ?thesis .
   133   finally show ?thesis .
   133 qed
   134 qed
   134 
   135 
   135 lemma norm_triangle_ineq2:
   136 lemma norm_triangle_ineq2:
   136   fixes a :: "'a::real_normed_vector" shows "\<parallel>a\<parallel> - \<parallel>b\<parallel> \<le> \<parallel>a - b\<parallel>"
   137   fixes a :: "'a::real_normed_vector"
   137 proof -
   138   shows "norm a - norm b \<le> norm (a - b)"
   138   have "\<parallel>a - b + b\<parallel> \<le> \<parallel>a - b\<parallel> + \<parallel>b\<parallel>"
   139 proof -
       
   140   have "norm (a - b + b) \<le> norm (a - b) + norm b"
   139     by (rule norm_triangle_ineq)
   141     by (rule norm_triangle_ineq)
   140   also have "(a - b + b) = a"
   142   also have "(a - b + b) = a"
   141     by simp
   143     by simp
   142   finally show ?thesis
   144   finally show ?thesis
   143     by (simp add: compare_rls)
   145     by (simp add: compare_rls)
   144 qed
   146 qed
   145 
   147 
   146 lemma norm_triangle_ineq4:
   148 lemma norm_triangle_ineq4:
   147   fixes a :: "'a::real_normed_vector" shows "\<parallel>a - b\<parallel> \<le> \<parallel>a\<parallel> + \<parallel>b\<parallel>"
   149   fixes a :: "'a::real_normed_vector"
   148 proof -
   150   shows "norm (a - b) \<le> norm a + norm b"
   149   have "\<parallel>a - b\<parallel> = \<parallel>a + - b\<parallel>"
   151 proof -
       
   152   have "norm (a - b) = norm (a + - b)"
   150     by (simp only: diff_minus)
   153     by (simp only: diff_minus)
   151   also have "\<dots> \<le> \<parallel>a\<parallel> + \<parallel>- b\<parallel>"
   154   also have "\<dots> \<le> norm a + norm (- b)"
   152     by (rule norm_triangle_ineq)
   155     by (rule norm_triangle_ineq)
   153   finally show ?thesis
   156   finally show ?thesis
   154     by simp
   157     by simp
   155 qed
   158 qed
   156 
   159 
   157 lemma nonzero_norm_inverse:
   160 lemma nonzero_norm_inverse:
   158   fixes a :: "'a::real_normed_div_algebra"
   161   fixes a :: "'a::real_normed_div_algebra"
   159   shows "a \<noteq> 0 \<Longrightarrow> \<parallel>inverse a\<parallel> = inverse \<parallel>a\<parallel>"
   162   shows "a \<noteq> 0 \<Longrightarrow> norm (inverse a) = inverse (norm a)"
   160 apply (rule inverse_unique [symmetric])
   163 apply (rule inverse_unique [symmetric])
   161 apply (simp add: norm_mult [symmetric])
   164 apply (simp add: norm_mult [symmetric])
   162 done
   165 done
   163 
   166 
   164 lemma norm_inverse:
   167 lemma norm_inverse:
   165   fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
   168   fixes a :: "'a::{real_normed_div_algebra,division_by_zero}"
   166   shows "\<parallel>inverse a\<parallel> = inverse \<parallel>a\<parallel>"
   169   shows "norm (inverse a) = inverse (norm a)"
   167 apply (case_tac "a = 0", simp)
   170 apply (case_tac "a = 0", simp)
   168 apply (erule nonzero_norm_inverse)
   171 apply (erule nonzero_norm_inverse)
   169 done
   172 done
   170 
   173 
   171 
   174 
   187 done
   190 done
   188 
   191 
   189 instance real :: norm ..
   192 instance real :: norm ..
   190 
   193 
   191 defs (overloaded)
   194 defs (overloaded)
   192   real_norm_def: "\<parallel>r\<parallel> \<equiv> \<bar>r\<bar>"
   195   real_norm_def: "norm r \<equiv> \<bar>r\<bar>"
   193 
   196 
   194 instance real :: real_normed_div_algebra
   197 instance real :: real_normed_div_algebra
   195 apply (intro_classes, unfold real_norm_def real_scaleR_def)
   198 apply (intro_classes, unfold real_norm_def real_scaleR_def)
   196 apply (rule abs_ge_zero)
   199 apply (rule abs_ge_zero)
   197 apply (rule abs_eq_0)
   200 apply (rule abs_eq_0)