new theory of real inner product spaces
authorhuffman
Thu Feb 19 09:42:23 2009 -0800 (2009-02-19)
changeset 2999384b2c432b94a
parent 29992 5deee36e33c4
child 29994 6ca6b6bd6e15
new theory of real inner product spaces
src/HOL/IsaMakefile
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Library.thy
     1.1 --- a/src/HOL/IsaMakefile	Thu Feb 19 09:39:49 2009 -0800
     1.2 +++ b/src/HOL/IsaMakefile	Thu Feb 19 09:42:23 2009 -0800
     1.3 @@ -315,6 +315,7 @@
     1.4    Library/Finite_Cartesian_Product.thy \
     1.5    Library/FrechetDeriv.thy \
     1.6    Library/Fundamental_Theorem_Algebra.thy \
     1.7 +  Library/Inner_Product.thy \
     1.8    Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
     1.9    Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
    1.10    Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Inner_Product.thy	Thu Feb 19 09:42:23 2009 -0800
     2.3 @@ -0,0 +1,305 @@
     2.4 +(* Title:      Inner_Product.thy
     2.5 +   Author:     Brian Huffman
     2.6 +*)
     2.7 +
     2.8 +header {* Inner Product Spaces and the Gradient Derivative *}
     2.9 +
    2.10 +theory Inner_Product
    2.11 +imports Complex FrechetDeriv
    2.12 +begin
    2.13 +
    2.14 +subsection {* Real inner product spaces *}
    2.15 +
    2.16 +class real_inner = real_vector + sgn_div_norm +
    2.17 +  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    2.18 +  assumes inner_commute: "inner x y = inner y x"
    2.19 +  and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
    2.20 +  and inner_scaleR_left: "inner (scaleR r x) y = r * (inner x y)"
    2.21 +  and inner_ge_zero [simp]: "0 \<le> inner x x"
    2.22 +  and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"
    2.23 +  and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"
    2.24 +begin
    2.25 +
    2.26 +lemma inner_zero_left [simp]: "inner 0 x = 0"
    2.27 +proof -
    2.28 +  have "inner 0 x = inner (0 + 0) x" by simp
    2.29 +  also have "\<dots> = inner 0 x + inner 0 x" by (rule inner_left_distrib)
    2.30 +  finally show "inner 0 x = 0" by simp
    2.31 +qed
    2.32 +
    2.33 +lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
    2.34 +proof -
    2.35 +  have "inner (- x) y + inner x y = inner (- x + x) y"
    2.36 +    by (rule inner_left_distrib [symmetric])
    2.37 +  also have "\<dots> = - inner x y + inner x y" by simp
    2.38 +  finally show "inner (- x) y = - inner x y" by simp
    2.39 +qed
    2.40 +
    2.41 +lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    2.42 +  by (simp add: diff_minus inner_left_distrib)
    2.43 +
    2.44 +text {* Transfer distributivity rules to right argument. *}
    2.45 +
    2.46 +lemma inner_right_distrib: "inner x (y + z) = inner x y + inner x z"
    2.47 +  using inner_left_distrib [of y z x] by (simp only: inner_commute)
    2.48 +
    2.49 +lemma inner_scaleR_right: "inner x (scaleR r y) = r * (inner x y)"
    2.50 +  using inner_scaleR_left [of r y x] by (simp only: inner_commute)
    2.51 +
    2.52 +lemma inner_zero_right [simp]: "inner x 0 = 0"
    2.53 +  using inner_zero_left [of x] by (simp only: inner_commute)
    2.54 +
    2.55 +lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
    2.56 +  using inner_minus_left [of y x] by (simp only: inner_commute)
    2.57 +
    2.58 +lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    2.59 +  using inner_diff_left [of y z x] by (simp only: inner_commute)
    2.60 +
    2.61 +lemmas inner_distrib = inner_left_distrib inner_right_distrib
    2.62 +lemmas inner_diff = inner_diff_left inner_diff_right
    2.63 +lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    2.64 +
    2.65 +lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
    2.66 +  by (simp add: order_less_le)
    2.67 +
    2.68 +lemma power2_norm_eq_inner: "(norm x)\<twosuperior> = inner x x"
    2.69 +  by (simp add: norm_eq_sqrt_inner)
    2.70 +
    2.71 +lemma Cauchy_Schwartz_ineq:
    2.72 +  "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
    2.73 +proof (cases)
    2.74 +  assume "y = 0"
    2.75 +  thus ?thesis by simp
    2.76 +next
    2.77 +  assume y: "y \<noteq> 0"
    2.78 +  let ?r = "inner x y / inner y y"
    2.79 +  have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
    2.80 +    by (rule inner_ge_zero)
    2.81 +  also have "\<dots> = inner x x - inner y x * ?r"
    2.82 +    by (simp add: inner_diff inner_scaleR)
    2.83 +  also have "\<dots> = inner x x - (inner x y)\<twosuperior> / inner y y"
    2.84 +    by (simp add: power2_eq_square inner_commute)
    2.85 +  finally have "0 \<le> inner x x - (inner x y)\<twosuperior> / inner y y" .
    2.86 +  hence "(inner x y)\<twosuperior> / inner y y \<le> inner x x"
    2.87 +    by (simp add: le_diff_eq)
    2.88 +  thus "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
    2.89 +    by (simp add: pos_divide_le_eq y)
    2.90 +qed
    2.91 +
    2.92 +lemma Cauchy_Schwartz_ineq2:
    2.93 +  "\<bar>inner x y\<bar> \<le> norm x * norm y"
    2.94 +proof (rule power2_le_imp_le)
    2.95 +  have "(inner x y)\<twosuperior> \<le> inner x x * inner y y"
    2.96 +    using Cauchy_Schwartz_ineq .
    2.97 +  thus "\<bar>inner x y\<bar>\<twosuperior> \<le> (norm x * norm y)\<twosuperior>"
    2.98 +    by (simp add: power_mult_distrib power2_norm_eq_inner)
    2.99 +  show "0 \<le> norm x * norm y"
   2.100 +    unfolding norm_eq_sqrt_inner
   2.101 +    by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
   2.102 +qed
   2.103 +
   2.104 +subclass real_normed_vector
   2.105 +proof
   2.106 +  fix a :: real and x y :: 'a
   2.107 +  show "0 \<le> norm x"
   2.108 +    unfolding norm_eq_sqrt_inner by simp
   2.109 +  show "norm x = 0 \<longleftrightarrow> x = 0"
   2.110 +    unfolding norm_eq_sqrt_inner by simp
   2.111 +  show "norm (x + y) \<le> norm x + norm y"
   2.112 +    proof (rule power2_le_imp_le)
   2.113 +      have "inner x y \<le> norm x * norm y"
   2.114 +        by (rule order_trans [OF abs_ge_self Cauchy_Schwartz_ineq2])
   2.115 +      thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"
   2.116 +        unfolding power2_sum power2_norm_eq_inner
   2.117 +        by (simp add: inner_distrib inner_commute)
   2.118 +      show "0 \<le> norm x + norm y"
   2.119 +        unfolding norm_eq_sqrt_inner
   2.120 +        by (simp add: add_nonneg_nonneg)
   2.121 +    qed
   2.122 +  have "sqrt (a\<twosuperior> * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
   2.123 +    by (simp add: real_sqrt_mult_distrib)
   2.124 +  then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
   2.125 +    unfolding norm_eq_sqrt_inner
   2.126 +    by (simp add: inner_scaleR power2_eq_square mult_assoc)
   2.127 +qed
   2.128 +
   2.129 +end
   2.130 +
   2.131 +interpretation inner!:
   2.132 +  bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
   2.133 +proof
   2.134 +  fix x y z :: 'a and r :: real
   2.135 +  show "inner (x + y) z = inner x z + inner y z"
   2.136 +    by (rule inner_left_distrib)
   2.137 +  show "inner x (y + z) = inner x y + inner x z"
   2.138 +    by (rule inner_right_distrib)
   2.139 +  show "inner (scaleR r x) y = scaleR r (inner x y)"
   2.140 +    unfolding real_scaleR_def by (rule inner_scaleR_left)
   2.141 +  show "inner x (scaleR r y) = scaleR r (inner x y)"
   2.142 +    unfolding real_scaleR_def by (rule inner_scaleR_right)
   2.143 +  show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
   2.144 +  proof
   2.145 +    show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
   2.146 +      by (simp add: Cauchy_Schwartz_ineq2)
   2.147 +  qed
   2.148 +qed
   2.149 +
   2.150 +interpretation inner_left!:
   2.151 +  bounded_linear "\<lambda>x::'a::real_inner. inner x y"
   2.152 +  by (rule inner.bounded_linear_left)
   2.153 +
   2.154 +interpretation inner_right!:
   2.155 +  bounded_linear "\<lambda>y::'a::real_inner. inner x y"
   2.156 +  by (rule inner.bounded_linear_right)
   2.157 +
   2.158 +
   2.159 +subsection {* Class instances *}
   2.160 +
   2.161 +instantiation real :: real_inner
   2.162 +begin
   2.163 +
   2.164 +definition inner_real_def [simp]: "inner = op *"
   2.165 +
   2.166 +instance proof
   2.167 +  fix x y z r :: real
   2.168 +  show "inner x y = inner y x"
   2.169 +    unfolding inner_real_def by (rule mult_commute)
   2.170 +  show "inner (x + y) z = inner x z + inner y z"
   2.171 +    unfolding inner_real_def by (rule left_distrib)
   2.172 +  show "inner (scaleR r x) y = r * inner x y"
   2.173 +    unfolding inner_real_def real_scaleR_def by (rule mult_assoc)
   2.174 +  show "0 \<le> inner x x"
   2.175 +    unfolding inner_real_def by simp
   2.176 +  show "inner x x = 0 \<longleftrightarrow> x = 0"
   2.177 +    unfolding inner_real_def by simp
   2.178 +  show "norm x = sqrt (inner x x)"
   2.179 +    unfolding inner_real_def by simp
   2.180 +qed
   2.181 +
   2.182 +end
   2.183 +
   2.184 +instantiation complex :: real_inner
   2.185 +begin
   2.186 +
   2.187 +definition inner_complex_def:
   2.188 +  "inner x y = Re x * Re y + Im x * Im y"
   2.189 +
   2.190 +instance proof
   2.191 +  fix x y z :: complex and r :: real
   2.192 +  show "inner x y = inner y x"
   2.193 +    unfolding inner_complex_def by (simp add: mult_commute)
   2.194 +  show "inner (x + y) z = inner x z + inner y z"
   2.195 +    unfolding inner_complex_def by (simp add: left_distrib)
   2.196 +  show "inner (scaleR r x) y = r * inner x y"
   2.197 +    unfolding inner_complex_def by (simp add: right_distrib)
   2.198 +  show "0 \<le> inner x x"
   2.199 +    unfolding inner_complex_def by (simp add: add_nonneg_nonneg)
   2.200 +  show "inner x x = 0 \<longleftrightarrow> x = 0"
   2.201 +    unfolding inner_complex_def
   2.202 +    by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
   2.203 +  show "norm x = sqrt (inner x x)"
   2.204 +    unfolding inner_complex_def complex_norm_def
   2.205 +    by (simp add: power2_eq_square)
   2.206 +qed
   2.207 +
   2.208 +end
   2.209 +
   2.210 +
   2.211 +subsection {* Gradient derivative *}
   2.212 +
   2.213 +definition
   2.214 +  gderiv ::
   2.215 +    "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
   2.216 +          ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   2.217 +where
   2.218 +  "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
   2.219 +
   2.220 +lemma deriv_fderiv: "DERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. h * D)"
   2.221 +  by (simp only: deriv_def field_fderiv_def)
   2.222 +
   2.223 +lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
   2.224 +  by (simp only: gderiv_def deriv_fderiv inner_real_def)
   2.225 +
   2.226 +lemma GDERIV_DERIV_compose:
   2.227 +    "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
   2.228 +     \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
   2.229 +  unfolding gderiv_def deriv_fderiv
   2.230 +  apply (drule (1) FDERIV_compose)
   2.231 +  apply (simp add: inner_scaleR_right mult_ac)
   2.232 +  done
   2.233 +
   2.234 +lemma FDERIV_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   2.235 +  by simp
   2.236 +
   2.237 +lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
   2.238 +  by simp
   2.239 +
   2.240 +lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
   2.241 +  unfolding gderiv_def inner_right.zero by (rule FDERIV_const)
   2.242 +
   2.243 +lemma GDERIV_add:
   2.244 +    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   2.245 +     \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
   2.246 +  unfolding gderiv_def inner_right.add by (rule FDERIV_add)
   2.247 +
   2.248 +lemma GDERIV_minus:
   2.249 +    "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
   2.250 +  unfolding gderiv_def inner_right.minus by (rule FDERIV_minus)
   2.251 +
   2.252 +lemma GDERIV_diff:
   2.253 +    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   2.254 +     \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
   2.255 +  unfolding gderiv_def inner_right.diff by (rule FDERIV_diff)
   2.256 +
   2.257 +lemma GDERIV_scaleR:
   2.258 +    "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   2.259 +     \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
   2.260 +      :> (scaleR (f x) dg + scaleR df (g x))"
   2.261 +  unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR
   2.262 +  apply (rule FDERIV_subst)
   2.263 +  apply (erule (1) scaleR.FDERIV)
   2.264 +  apply (simp add: mult_ac)
   2.265 +  done
   2.266 +
   2.267 +lemma GDERIV_mult:
   2.268 +    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   2.269 +     \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
   2.270 +  unfolding gderiv_def
   2.271 +  apply (rule FDERIV_subst)
   2.272 +  apply (erule (1) FDERIV_mult)
   2.273 +  apply (simp add: inner_distrib inner_scaleR mult_ac)
   2.274 +  done
   2.275 +
   2.276 +lemma GDERIV_inverse:
   2.277 +    "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
   2.278 +     \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<twosuperior> *\<^sub>R df"
   2.279 +  apply (erule GDERIV_DERIV_compose)
   2.280 +  apply (erule DERIV_inverse [folded numeral_2_eq_2])
   2.281 +  done
   2.282 +
   2.283 +lemma GDERIV_norm:
   2.284 +  assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
   2.285 +proof -
   2.286 +  have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   2.287 +    by (intro inner.FDERIV FDERIV_ident)
   2.288 +  have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   2.289 +    by (simp add: expand_fun_eq inner_scaleR inner_commute)
   2.290 +  have "0 < inner x x" using `x \<noteq> 0` by simp
   2.291 +  then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
   2.292 +    by (rule DERIV_real_sqrt)
   2.293 +  have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
   2.294 +    by (simp add: sgn_div_norm norm_eq_sqrt_inner)
   2.295 +  show ?thesis
   2.296 +    unfolding norm_eq_sqrt_inner
   2.297 +    apply (rule GDERIV_subst [OF _ 4])
   2.298 +    apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
   2.299 +    apply (subst gderiv_def)
   2.300 +    apply (rule FDERIV_subst [OF _ 2])
   2.301 +    apply (rule 1)
   2.302 +    apply (rule 3)
   2.303 +    done
   2.304 +qed
   2.305 +
   2.306 +lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def]
   2.307 +
   2.308 +end
     3.1 --- a/src/HOL/Library/Library.thy	Thu Feb 19 09:39:49 2009 -0800
     3.2 +++ b/src/HOL/Library/Library.thy	Thu Feb 19 09:42:23 2009 -0800
     3.3 @@ -26,6 +26,7 @@
     3.4    FuncSet
     3.5    Fundamental_Theorem_Algebra
     3.6    Infinite_Set
     3.7 +  Inner_Product
     3.8    ListVector
     3.9    Mapping
    3.10    Multiset