src/HOL/Library/Product_Vector.thy
 author huffman Fri Feb 20 08:02:11 2009 -0800 (2009-02-20) changeset 30019 a2f19e0a28b2 child 30729 461ee3e49ad3 permissions -rw-r--r--
add theory of products as real vector spaces to Library
 huffman@30019 ` 1` ```(* Title: HOL/Library/Product_Vector.thy ``` huffman@30019 ` 2` ``` Author: Brian Huffman ``` huffman@30019 ` 3` ```*) ``` huffman@30019 ` 4` huffman@30019 ` 5` ```header {* Cartesian Products as Vector Spaces *} ``` huffman@30019 ` 6` huffman@30019 ` 7` ```theory Product_Vector ``` huffman@30019 ` 8` ```imports Inner_Product Product_plus ``` huffman@30019 ` 9` ```begin ``` huffman@30019 ` 10` huffman@30019 ` 11` ```subsection {* Product is a real vector space *} ``` huffman@30019 ` 12` huffman@30019 ` 13` ```instantiation "*" :: (real_vector, real_vector) real_vector ``` huffman@30019 ` 14` ```begin ``` huffman@30019 ` 15` huffman@30019 ` 16` ```definition scaleR_prod_def: ``` huffman@30019 ` 17` ``` "scaleR r A = (scaleR r (fst A), scaleR r (snd A))" ``` huffman@30019 ` 18` huffman@30019 ` 19` ```lemma fst_scaleR [simp]: "fst (scaleR r A) = scaleR r (fst A)" ``` huffman@30019 ` 20` ``` unfolding scaleR_prod_def by simp ``` huffman@30019 ` 21` huffman@30019 ` 22` ```lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)" ``` huffman@30019 ` 23` ``` unfolding scaleR_prod_def by simp ``` huffman@30019 ` 24` huffman@30019 ` 25` ```lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)" ``` huffman@30019 ` 26` ``` unfolding scaleR_prod_def by simp ``` huffman@30019 ` 27` huffman@30019 ` 28` ```instance proof ``` huffman@30019 ` 29` ``` fix a b :: real and x y :: "'a \ 'b" ``` huffman@30019 ` 30` ``` show "scaleR a (x + y) = scaleR a x + scaleR a y" ``` huffman@30019 ` 31` ``` by (simp add: expand_prod_eq scaleR_right_distrib) ``` huffman@30019 ` 32` ``` show "scaleR (a + b) x = scaleR a x + scaleR b x" ``` huffman@30019 ` 33` ``` by (simp add: expand_prod_eq scaleR_left_distrib) ``` huffman@30019 ` 34` ``` show "scaleR a (scaleR b x) = scaleR (a * b) x" ``` huffman@30019 ` 35` ``` by (simp add: expand_prod_eq) ``` huffman@30019 ` 36` ``` show "scaleR 1 x = x" ``` huffman@30019 ` 37` ``` by (simp add: expand_prod_eq) ``` huffman@30019 ` 38` ```qed ``` huffman@30019 ` 39` huffman@30019 ` 40` ```end ``` huffman@30019 ` 41` huffman@30019 ` 42` ```subsection {* Product is a normed vector space *} ``` huffman@30019 ` 43` huffman@30019 ` 44` ```instantiation ``` huffman@30019 ` 45` ``` "*" :: (real_normed_vector, real_normed_vector) real_normed_vector ``` huffman@30019 ` 46` ```begin ``` huffman@30019 ` 47` huffman@30019 ` 48` ```definition norm_prod_def: ``` huffman@30019 ` 49` ``` "norm x = sqrt ((norm (fst x))\ + (norm (snd x))\)" ``` huffman@30019 ` 50` huffman@30019 ` 51` ```definition sgn_prod_def: ``` huffman@30019 ` 52` ``` "sgn (x::'a \ 'b) = scaleR (inverse (norm x)) x" ``` huffman@30019 ` 53` huffman@30019 ` 54` ```lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\ + (norm b)\)" ``` huffman@30019 ` 55` ``` unfolding norm_prod_def by simp ``` huffman@30019 ` 56` huffman@30019 ` 57` ```instance proof ``` huffman@30019 ` 58` ``` fix r :: real and x y :: "'a \ 'b" ``` huffman@30019 ` 59` ``` show "0 \ norm x" ``` huffman@30019 ` 60` ``` unfolding norm_prod_def by simp ``` huffman@30019 ` 61` ``` show "norm x = 0 \ x = 0" ``` huffman@30019 ` 62` ``` unfolding norm_prod_def ``` huffman@30019 ` 63` ``` by (simp add: expand_prod_eq) ``` huffman@30019 ` 64` ``` show "norm (x + y) \ norm x + norm y" ``` huffman@30019 ` 65` ``` unfolding norm_prod_def ``` huffman@30019 ` 66` ``` apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]) ``` huffman@30019 ` 67` ``` apply (simp add: add_mono power_mono norm_triangle_ineq) ``` huffman@30019 ` 68` ``` done ``` huffman@30019 ` 69` ``` show "norm (scaleR r x) = \r\ * norm x" ``` huffman@30019 ` 70` ``` unfolding norm_prod_def ``` huffman@30019 ` 71` ``` apply (simp add: norm_scaleR power_mult_distrib) ``` huffman@30019 ` 72` ``` apply (simp add: right_distrib [symmetric]) ``` huffman@30019 ` 73` ``` apply (simp add: real_sqrt_mult_distrib) ``` huffman@30019 ` 74` ``` done ``` huffman@30019 ` 75` ``` show "sgn x = scaleR (inverse (norm x)) x" ``` huffman@30019 ` 76` ``` by (rule sgn_prod_def) ``` huffman@30019 ` 77` ```qed ``` huffman@30019 ` 78` huffman@30019 ` 79` ```end ``` huffman@30019 ` 80` huffman@30019 ` 81` ```subsection {* Product is an inner product space *} ``` huffman@30019 ` 82` huffman@30019 ` 83` ```instantiation "*" :: (real_inner, real_inner) real_inner ``` huffman@30019 ` 84` ```begin ``` huffman@30019 ` 85` huffman@30019 ` 86` ```definition inner_prod_def: ``` huffman@30019 ` 87` ``` "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)" ``` huffman@30019 ` 88` huffman@30019 ` 89` ```lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d" ``` huffman@30019 ` 90` ``` unfolding inner_prod_def by simp ``` huffman@30019 ` 91` huffman@30019 ` 92` ```instance proof ``` huffman@30019 ` 93` ``` fix r :: real ``` huffman@30019 ` 94` ``` fix x y z :: "'a::real_inner * 'b::real_inner" ``` huffman@30019 ` 95` ``` show "inner x y = inner y x" ``` huffman@30019 ` 96` ``` unfolding inner_prod_def ``` huffman@30019 ` 97` ``` by (simp add: inner_commute) ``` huffman@30019 ` 98` ``` show "inner (x + y) z = inner x z + inner y z" ``` huffman@30019 ` 99` ``` unfolding inner_prod_def ``` huffman@30019 ` 100` ``` by (simp add: inner_left_distrib) ``` huffman@30019 ` 101` ``` show "inner (scaleR r x) y = r * inner x y" ``` huffman@30019 ` 102` ``` unfolding inner_prod_def ``` huffman@30019 ` 103` ``` by (simp add: inner_scaleR_left right_distrib) ``` huffman@30019 ` 104` ``` show "0 \ inner x x" ``` huffman@30019 ` 105` ``` unfolding inner_prod_def ``` huffman@30019 ` 106` ``` by (intro add_nonneg_nonneg inner_ge_zero) ``` huffman@30019 ` 107` ``` show "inner x x = 0 \ x = 0" ``` huffman@30019 ` 108` ``` unfolding inner_prod_def expand_prod_eq ``` huffman@30019 ` 109` ``` by (simp add: add_nonneg_eq_0_iff) ``` huffman@30019 ` 110` ``` show "norm x = sqrt (inner x x)" ``` huffman@30019 ` 111` ``` unfolding norm_prod_def inner_prod_def ``` huffman@30019 ` 112` ``` by (simp add: power2_norm_eq_inner) ``` huffman@30019 ` 113` ```qed ``` huffman@30019 ` 114` huffman@30019 ` 115` ```end ``` huffman@30019 ` 116` huffman@30019 ` 117` ```subsection {* Pair operations are linear and continuous *} ``` huffman@30019 ` 118` huffman@30019 ` 119` ```interpretation fst!: bounded_linear fst ``` huffman@30019 ` 120` ``` apply (unfold_locales) ``` huffman@30019 ` 121` ``` apply (rule fst_add) ``` huffman@30019 ` 122` ``` apply (rule fst_scaleR) ``` huffman@30019 ` 123` ``` apply (rule_tac x="1" in exI, simp add: norm_Pair) ``` huffman@30019 ` 124` ``` done ``` huffman@30019 ` 125` huffman@30019 ` 126` ```interpretation snd!: bounded_linear snd ``` huffman@30019 ` 127` ``` apply (unfold_locales) ``` huffman@30019 ` 128` ``` apply (rule snd_add) ``` huffman@30019 ` 129` ``` apply (rule snd_scaleR) ``` huffman@30019 ` 130` ``` apply (rule_tac x="1" in exI, simp add: norm_Pair) ``` huffman@30019 ` 131` ``` done ``` huffman@30019 ` 132` huffman@30019 ` 133` ```text {* TODO: move to NthRoot *} ``` huffman@30019 ` 134` ```lemma sqrt_add_le_add_sqrt: ``` huffman@30019 ` 135` ``` assumes x: "0 \ x" and y: "0 \ y" ``` huffman@30019 ` 136` ``` shows "sqrt (x + y) \ sqrt x + sqrt y" ``` huffman@30019 ` 137` ```apply (rule power2_le_imp_le) ``` huffman@30019 ` 138` ```apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y) ``` huffman@30019 ` 139` ```apply (simp add: mult_nonneg_nonneg x y) ``` huffman@30019 ` 140` ```apply (simp add: add_nonneg_nonneg x y) ``` huffman@30019 ` 141` ```done ``` huffman@30019 ` 142` huffman@30019 ` 143` ```lemma bounded_linear_Pair: ``` huffman@30019 ` 144` ``` assumes f: "bounded_linear f" ``` huffman@30019 ` 145` ``` assumes g: "bounded_linear g" ``` huffman@30019 ` 146` ``` shows "bounded_linear (\x. (f x, g x))" ``` huffman@30019 ` 147` ```proof ``` huffman@30019 ` 148` ``` interpret f: bounded_linear f by fact ``` huffman@30019 ` 149` ``` interpret g: bounded_linear g by fact ``` huffman@30019 ` 150` ``` fix x y and r :: real ``` huffman@30019 ` 151` ``` show "(f (x + y), g (x + y)) = (f x, g x) + (f y, g y)" ``` huffman@30019 ` 152` ``` by (simp add: f.add g.add) ``` huffman@30019 ` 153` ``` show "(f (r *\<^sub>R x), g (r *\<^sub>R x)) = r *\<^sub>R (f x, g x)" ``` huffman@30019 ` 154` ``` by (simp add: f.scaleR g.scaleR) ``` huffman@30019 ` 155` ``` obtain Kf where "0 < Kf" and norm_f: "\x. norm (f x) \ norm x * Kf" ``` huffman@30019 ` 156` ``` using f.pos_bounded by fast ``` huffman@30019 ` 157` ``` obtain Kg where "0 < Kg" and norm_g: "\x. norm (g x) \ norm x * Kg" ``` huffman@30019 ` 158` ``` using g.pos_bounded by fast ``` huffman@30019 ` 159` ``` have "\x. norm (f x, g x) \ norm x * (Kf + Kg)" ``` huffman@30019 ` 160` ``` apply (rule allI) ``` huffman@30019 ` 161` ``` apply (simp add: norm_Pair) ``` huffman@30019 ` 162` ``` apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp) ``` huffman@30019 ` 163` ``` apply (simp add: right_distrib) ``` huffman@30019 ` 164` ``` apply (rule add_mono [OF norm_f norm_g]) ``` huffman@30019 ` 165` ``` done ``` huffman@30019 ` 166` ``` then show "\K. \x. norm (f x, g x) \ norm x * K" .. ``` huffman@30019 ` 167` ```qed ``` huffman@30019 ` 168` huffman@30019 ` 169` ```text {* ``` huffman@30019 ` 170` ``` TODO: The next three proofs are nearly identical to each other. ``` huffman@30019 ` 171` ``` Is there a good way to factor out the common parts? ``` huffman@30019 ` 172` ```*} ``` huffman@30019 ` 173` huffman@30019 ` 174` ```lemma LIMSEQ_Pair: ``` huffman@30019 ` 175` ``` assumes "X ----> a" and "Y ----> b" ``` huffman@30019 ` 176` ``` shows "(\n. (X n, Y n)) ----> (a, b)" ``` huffman@30019 ` 177` ```proof (rule LIMSEQ_I) ``` huffman@30019 ` 178` ``` fix r :: real assume "0 < r" ``` huffman@30019 ` 179` ``` then have "0 < r / sqrt 2" (is "0 < ?s") ``` huffman@30019 ` 180` ``` by (simp add: divide_pos_pos) ``` huffman@30019 ` 181` ``` obtain M where M: "\n\M. norm (X n - a) < ?s" ``` huffman@30019 ` 182` ``` using LIMSEQ_D [OF `X ----> a` `0 < ?s`] .. ``` huffman@30019 ` 183` ``` obtain N where N: "\n\N. norm (Y n - b) < ?s" ``` huffman@30019 ` 184` ``` using LIMSEQ_D [OF `Y ----> b` `0 < ?s`] .. ``` huffman@30019 ` 185` ``` have "\n\max M N. norm ((X n, Y n) - (a, b)) < r" ``` huffman@30019 ` 186` ``` using M N by (simp add: real_sqrt_sum_squares_less norm_Pair) ``` huffman@30019 ` 187` ``` then show "\n0. \n\n0. norm ((X n, Y n) - (a, b)) < r" .. ``` huffman@30019 ` 188` ```qed ``` huffman@30019 ` 189` huffman@30019 ` 190` ```lemma Cauchy_Pair: ``` huffman@30019 ` 191` ``` assumes "Cauchy X" and "Cauchy Y" ``` huffman@30019 ` 192` ``` shows "Cauchy (\n. (X n, Y n))" ``` huffman@30019 ` 193` ```proof (rule CauchyI) ``` huffman@30019 ` 194` ``` fix r :: real assume "0 < r" ``` huffman@30019 ` 195` ``` then have "0 < r / sqrt 2" (is "0 < ?s") ``` huffman@30019 ` 196` ``` by (simp add: divide_pos_pos) ``` huffman@30019 ` 197` ``` obtain M where M: "\m\M. \n\M. norm (X m - X n) < ?s" ``` huffman@30019 ` 198` ``` using CauchyD [OF `Cauchy X` `0 < ?s`] .. ``` huffman@30019 ` 199` ``` obtain N where N: "\m\N. \n\N. norm (Y m - Y n) < ?s" ``` huffman@30019 ` 200` ``` using CauchyD [OF `Cauchy Y` `0 < ?s`] .. ``` huffman@30019 ` 201` ``` have "\m\max M N. \n\max M N. norm ((X m, Y m) - (X n, Y n)) < r" ``` huffman@30019 ` 202` ``` using M N by (simp add: real_sqrt_sum_squares_less norm_Pair) ``` huffman@30019 ` 203` ``` then show "\n0. \m\n0. \n\n0. norm ((X m, Y m) - (X n, Y n)) < r" .. ``` huffman@30019 ` 204` ```qed ``` huffman@30019 ` 205` huffman@30019 ` 206` ```lemma LIM_Pair: ``` huffman@30019 ` 207` ``` assumes "f -- x --> a" and "g -- x --> b" ``` huffman@30019 ` 208` ``` shows "(\x. (f x, g x)) -- x --> (a, b)" ``` huffman@30019 ` 209` ```proof (rule LIM_I) ``` huffman@30019 ` 210` ``` fix r :: real assume "0 < r" ``` huffman@30019 ` 211` ``` then have "0 < r / sqrt 2" (is "0 < ?e") ``` huffman@30019 ` 212` ``` by (simp add: divide_pos_pos) ``` huffman@30019 ` 213` ``` obtain s where s: "0 < s" ``` huffman@30019 ` 214` ``` "\z. z \ x \ norm (z - x) < s \ norm (f z - a) < ?e" ``` huffman@30019 ` 215` ``` using LIM_D [OF `f -- x --> a` `0 < ?e`] by fast ``` huffman@30019 ` 216` ``` obtain t where t: "0 < t" ``` huffman@30019 ` 217` ``` "\z. z \ x \ norm (z - x) < t \ norm (g z - b) < ?e" ``` huffman@30019 ` 218` ``` using LIM_D [OF `g -- x --> b` `0 < ?e`] by fast ``` huffman@30019 ` 219` ``` have "0 < min s t \ ``` huffman@30019 ` 220` ``` (\z. z \ x \ norm (z - x) < min s t \ norm ((f z, g z) - (a, b)) < r)" ``` huffman@30019 ` 221` ``` using s t by (simp add: real_sqrt_sum_squares_less norm_Pair) ``` huffman@30019 ` 222` ``` then show ``` huffman@30019 ` 223` ``` "\s>0. \z. z \ x \ norm (z - x) < s \ norm ((f z, g z) - (a, b)) < r" .. ``` huffman@30019 ` 224` ```qed ``` huffman@30019 ` 225` huffman@30019 ` 226` ```lemma isCont_Pair [simp]: ``` huffman@30019 ` 227` ``` "\isCont f x; isCont g x\ \ isCont (\x. (f x, g x)) x" ``` huffman@30019 ` 228` ``` unfolding isCont_def by (rule LIM_Pair) ``` huffman@30019 ` 229` huffman@30019 ` 230` huffman@30019 ` 231` ```subsection {* Product is a complete vector space *} ``` huffman@30019 ` 232` huffman@30019 ` 233` ```instance "*" :: (banach, banach) banach ``` huffman@30019 ` 234` ```proof ``` huffman@30019 ` 235` ``` fix X :: "nat \ 'a \ 'b" assume "Cauchy X" ``` huffman@30019 ` 236` ``` have 1: "(\n. fst (X n)) ----> lim (\n. fst (X n))" ``` huffman@30019 ` 237` ``` using fst.Cauchy [OF `Cauchy X`] ``` huffman@30019 ` 238` ``` by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) ``` huffman@30019 ` 239` ``` have 2: "(\n. snd (X n)) ----> lim (\n. snd (X n))" ``` huffman@30019 ` 240` ``` using snd.Cauchy [OF `Cauchy X`] ``` huffman@30019 ` 241` ``` by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) ``` huffman@30019 ` 242` ``` have "X ----> (lim (\n. fst (X n)), lim (\n. snd (X n)))" ``` huffman@30019 ` 243` ``` using LIMSEQ_Pair [OF 1 2] by simp ``` huffman@30019 ` 244` ``` then show "convergent X" ``` huffman@30019 ` 245` ``` by (rule convergentI) ``` huffman@30019 ` 246` ```qed ``` huffman@30019 ` 247` huffman@30019 ` 248` ```subsection {* Frechet derivatives involving pairs *} ``` huffman@30019 ` 249` huffman@30019 ` 250` ```lemma FDERIV_Pair: ``` huffman@30019 ` 251` ``` assumes f: "FDERIV f x :> f'" and g: "FDERIV g x :> g'" ``` huffman@30019 ` 252` ``` shows "FDERIV (\x. (f x, g x)) x :> (\h. (f' h, g' h))" ``` huffman@30019 ` 253` ```apply (rule FDERIV_I) ``` huffman@30019 ` 254` ```apply (rule bounded_linear_Pair) ``` huffman@30019 ` 255` ```apply (rule FDERIV_bounded_linear [OF f]) ``` huffman@30019 ` 256` ```apply (rule FDERIV_bounded_linear [OF g]) ``` huffman@30019 ` 257` ```apply (simp add: norm_Pair) ``` huffman@30019 ` 258` ```apply (rule real_LIM_sandwich_zero) ``` huffman@30019 ` 259` ```apply (rule LIM_add_zero) ``` huffman@30019 ` 260` ```apply (rule FDERIV_D [OF f]) ``` huffman@30019 ` 261` ```apply (rule FDERIV_D [OF g]) ``` huffman@30019 ` 262` ```apply (rename_tac h) ``` huffman@30019 ` 263` ```apply (simp add: divide_nonneg_pos) ``` huffman@30019 ` 264` ```apply (rename_tac h) ``` huffman@30019 ` 265` ```apply (subst add_divide_distrib [symmetric]) ``` huffman@30019 ` 266` ```apply (rule divide_right_mono [OF _ norm_ge_zero]) ``` huffman@30019 ` 267` ```apply (rule order_trans [OF sqrt_add_le_add_sqrt]) ``` huffman@30019 ` 268` ```apply simp ``` huffman@30019 ` 269` ```apply simp ``` huffman@30019 ` 270` ```apply simp ``` huffman@30019 ` 271` ```done ``` huffman@30019 ` 272` huffman@30019 ` 273` ```end ```