src/HOL/Library/Inner_Product.thy
 author haftmann Wed Apr 22 19:09:21 2009 +0200 (2009-04-22) changeset 30960 fec1a04b7220 parent 30729 461ee3e49ad3 child 31289 847f00f435d4 permissions -rw-r--r--
power operation defined generic
 huffman@29993 ` 1` ```(* Title: Inner_Product.thy ``` huffman@29993 ` 2` ``` Author: Brian Huffman ``` huffman@29993 ` 3` ```*) ``` huffman@29993 ` 4` huffman@29993 ` 5` ```header {* Inner Product Spaces and the Gradient Derivative *} ``` huffman@29993 ` 6` huffman@29993 ` 7` ```theory Inner_Product ``` haftmann@30663 ` 8` ```imports Complex_Main FrechetDeriv ``` huffman@29993 ` 9` ```begin ``` huffman@29993 ` 10` huffman@29993 ` 11` ```subsection {* Real inner product spaces *} ``` huffman@29993 ` 12` huffman@29993 ` 13` ```class real_inner = real_vector + sgn_div_norm + ``` huffman@29993 ` 14` ``` fixes inner :: "'a \ 'a \ real" ``` huffman@29993 ` 15` ``` assumes inner_commute: "inner x y = inner y x" ``` huffman@29993 ` 16` ``` and inner_left_distrib: "inner (x + y) z = inner x z + inner y z" ``` huffman@29993 ` 17` ``` and inner_scaleR_left: "inner (scaleR r x) y = r * (inner x y)" ``` huffman@29993 ` 18` ``` and inner_ge_zero [simp]: "0 \ inner x x" ``` huffman@29993 ` 19` ``` and inner_eq_zero_iff [simp]: "inner x x = 0 \ x = 0" ``` huffman@29993 ` 20` ``` and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)" ``` huffman@29993 ` 21` ```begin ``` huffman@29993 ` 22` huffman@29993 ` 23` ```lemma inner_zero_left [simp]: "inner 0 x = 0" ``` huffman@30067 ` 24` ``` using inner_left_distrib [of 0 0 x] by simp ``` huffman@29993 ` 25` huffman@29993 ` 26` ```lemma inner_minus_left [simp]: "inner (- x) y = - inner x y" ``` huffman@30067 ` 27` ``` using inner_left_distrib [of x "- x" y] by simp ``` huffman@29993 ` 28` huffman@29993 ` 29` ```lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z" ``` huffman@29993 ` 30` ``` by (simp add: diff_minus inner_left_distrib) ``` huffman@29993 ` 31` huffman@29993 ` 32` ```text {* Transfer distributivity rules to right argument. *} ``` huffman@29993 ` 33` huffman@29993 ` 34` ```lemma inner_right_distrib: "inner x (y + z) = inner x y + inner x z" ``` huffman@29993 ` 35` ``` using inner_left_distrib [of y z x] by (simp only: inner_commute) ``` huffman@29993 ` 36` huffman@29993 ` 37` ```lemma inner_scaleR_right: "inner x (scaleR r y) = r * (inner x y)" ``` huffman@29993 ` 38` ``` using inner_scaleR_left [of r y x] by (simp only: inner_commute) ``` huffman@29993 ` 39` huffman@29993 ` 40` ```lemma inner_zero_right [simp]: "inner x 0 = 0" ``` huffman@29993 ` 41` ``` using inner_zero_left [of x] by (simp only: inner_commute) ``` huffman@29993 ` 42` huffman@29993 ` 43` ```lemma inner_minus_right [simp]: "inner x (- y) = - inner x y" ``` huffman@29993 ` 44` ``` using inner_minus_left [of y x] by (simp only: inner_commute) ``` huffman@29993 ` 45` huffman@29993 ` 46` ```lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z" ``` huffman@29993 ` 47` ``` using inner_diff_left [of y z x] by (simp only: inner_commute) ``` huffman@29993 ` 48` huffman@29993 ` 49` ```lemmas inner_distrib = inner_left_distrib inner_right_distrib ``` huffman@29993 ` 50` ```lemmas inner_diff = inner_diff_left inner_diff_right ``` huffman@29993 ` 51` ```lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right ``` huffman@29993 ` 52` huffman@29993 ` 53` ```lemma inner_gt_zero_iff [simp]: "0 < inner x x \ x \ 0" ``` huffman@29993 ` 54` ``` by (simp add: order_less_le) ``` huffman@29993 ` 55` huffman@29993 ` 56` ```lemma power2_norm_eq_inner: "(norm x)\ = inner x x" ``` huffman@29993 ` 57` ``` by (simp add: norm_eq_sqrt_inner) ``` huffman@29993 ` 58` huffman@30046 ` 59` ```lemma Cauchy_Schwarz_ineq: ``` huffman@29993 ` 60` ``` "(inner x y)\ \ inner x x * inner y y" ``` huffman@29993 ` 61` ```proof (cases) ``` huffman@29993 ` 62` ``` assume "y = 0" ``` huffman@29993 ` 63` ``` thus ?thesis by simp ``` huffman@29993 ` 64` ```next ``` huffman@29993 ` 65` ``` assume y: "y \ 0" ``` huffman@29993 ` 66` ``` let ?r = "inner x y / inner y y" ``` huffman@29993 ` 67` ``` have "0 \ inner (x - scaleR ?r y) (x - scaleR ?r y)" ``` huffman@29993 ` 68` ``` by (rule inner_ge_zero) ``` huffman@29993 ` 69` ``` also have "\ = inner x x - inner y x * ?r" ``` huffman@29993 ` 70` ``` by (simp add: inner_diff inner_scaleR) ``` huffman@29993 ` 71` ``` also have "\ = inner x x - (inner x y)\ / inner y y" ``` huffman@29993 ` 72` ``` by (simp add: power2_eq_square inner_commute) ``` huffman@29993 ` 73` ``` finally have "0 \ inner x x - (inner x y)\ / inner y y" . ``` huffman@29993 ` 74` ``` hence "(inner x y)\ / inner y y \ inner x x" ``` huffman@29993 ` 75` ``` by (simp add: le_diff_eq) ``` huffman@29993 ` 76` ``` thus "(inner x y)\ \ inner x x * inner y y" ``` huffman@29993 ` 77` ``` by (simp add: pos_divide_le_eq y) ``` huffman@29993 ` 78` ```qed ``` huffman@29993 ` 79` huffman@30046 ` 80` ```lemma Cauchy_Schwarz_ineq2: ``` huffman@29993 ` 81` ``` "\inner x y\ \ norm x * norm y" ``` huffman@29993 ` 82` ```proof (rule power2_le_imp_le) ``` huffman@29993 ` 83` ``` have "(inner x y)\ \ inner x x * inner y y" ``` huffman@30046 ` 84` ``` using Cauchy_Schwarz_ineq . ``` huffman@29993 ` 85` ``` thus "\inner x y\\ \ (norm x * norm y)\" ``` huffman@29993 ` 86` ``` by (simp add: power_mult_distrib power2_norm_eq_inner) ``` huffman@29993 ` 87` ``` show "0 \ norm x * norm y" ``` huffman@29993 ` 88` ``` unfolding norm_eq_sqrt_inner ``` huffman@29993 ` 89` ``` by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero) ``` huffman@29993 ` 90` ```qed ``` huffman@29993 ` 91` huffman@29993 ` 92` ```subclass real_normed_vector ``` huffman@29993 ` 93` ```proof ``` huffman@29993 ` 94` ``` fix a :: real and x y :: 'a ``` huffman@29993 ` 95` ``` show "0 \ norm x" ``` huffman@29993 ` 96` ``` unfolding norm_eq_sqrt_inner by simp ``` huffman@29993 ` 97` ``` show "norm x = 0 \ x = 0" ``` huffman@29993 ` 98` ``` unfolding norm_eq_sqrt_inner by simp ``` huffman@29993 ` 99` ``` show "norm (x + y) \ norm x + norm y" ``` huffman@29993 ` 100` ``` proof (rule power2_le_imp_le) ``` huffman@29993 ` 101` ``` have "inner x y \ norm x * norm y" ``` huffman@30046 ` 102` ``` by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2]) ``` huffman@29993 ` 103` ``` thus "(norm (x + y))\ \ (norm x + norm y)\" ``` huffman@29993 ` 104` ``` unfolding power2_sum power2_norm_eq_inner ``` huffman@29993 ` 105` ``` by (simp add: inner_distrib inner_commute) ``` huffman@29993 ` 106` ``` show "0 \ norm x + norm y" ``` huffman@29993 ` 107` ``` unfolding norm_eq_sqrt_inner ``` huffman@29993 ` 108` ``` by (simp add: add_nonneg_nonneg) ``` huffman@29993 ` 109` ``` qed ``` huffman@29993 ` 110` ``` have "sqrt (a\ * inner x x) = \a\ * sqrt (inner x x)" ``` huffman@29993 ` 111` ``` by (simp add: real_sqrt_mult_distrib) ``` huffman@29993 ` 112` ``` then show "norm (a *\<^sub>R x) = \a\ * norm x" ``` huffman@29993 ` 113` ``` unfolding norm_eq_sqrt_inner ``` huffman@29993 ` 114` ``` by (simp add: inner_scaleR power2_eq_square mult_assoc) ``` huffman@29993 ` 115` ```qed ``` huffman@29993 ` 116` huffman@29993 ` 117` ```end ``` huffman@29993 ` 118` wenzelm@30729 ` 119` ```interpretation inner: ``` huffman@29993 ` 120` ``` bounded_bilinear "inner::'a::real_inner \ 'a \ real" ``` huffman@29993 ` 121` ```proof ``` huffman@29993 ` 122` ``` fix x y z :: 'a and r :: real ``` huffman@29993 ` 123` ``` show "inner (x + y) z = inner x z + inner y z" ``` huffman@29993 ` 124` ``` by (rule inner_left_distrib) ``` huffman@29993 ` 125` ``` show "inner x (y + z) = inner x y + inner x z" ``` huffman@29993 ` 126` ``` by (rule inner_right_distrib) ``` huffman@29993 ` 127` ``` show "inner (scaleR r x) y = scaleR r (inner x y)" ``` huffman@29993 ` 128` ``` unfolding real_scaleR_def by (rule inner_scaleR_left) ``` huffman@29993 ` 129` ``` show "inner x (scaleR r y) = scaleR r (inner x y)" ``` huffman@29993 ` 130` ``` unfolding real_scaleR_def by (rule inner_scaleR_right) ``` huffman@29993 ` 131` ``` show "\K. \x y::'a. norm (inner x y) \ norm x * norm y * K" ``` huffman@29993 ` 132` ``` proof ``` huffman@29993 ` 133` ``` show "\x y::'a. norm (inner x y) \ norm x * norm y * 1" ``` huffman@30046 ` 134` ``` by (simp add: Cauchy_Schwarz_ineq2) ``` huffman@29993 ` 135` ``` qed ``` huffman@29993 ` 136` ```qed ``` huffman@29993 ` 137` wenzelm@30729 ` 138` ```interpretation inner_left: ``` huffman@29993 ` 139` ``` bounded_linear "\x::'a::real_inner. inner x y" ``` huffman@29993 ` 140` ``` by (rule inner.bounded_linear_left) ``` huffman@29993 ` 141` wenzelm@30729 ` 142` ```interpretation inner_right: ``` huffman@29993 ` 143` ``` bounded_linear "\y::'a::real_inner. inner x y" ``` huffman@29993 ` 144` ``` by (rule inner.bounded_linear_right) ``` huffman@29993 ` 145` huffman@29993 ` 146` huffman@29993 ` 147` ```subsection {* Class instances *} ``` huffman@29993 ` 148` huffman@29993 ` 149` ```instantiation real :: real_inner ``` huffman@29993 ` 150` ```begin ``` huffman@29993 ` 151` huffman@29993 ` 152` ```definition inner_real_def [simp]: "inner = op *" ``` huffman@29993 ` 153` huffman@29993 ` 154` ```instance proof ``` huffman@29993 ` 155` ``` fix x y z r :: real ``` huffman@29993 ` 156` ``` show "inner x y = inner y x" ``` huffman@29993 ` 157` ``` unfolding inner_real_def by (rule mult_commute) ``` huffman@29993 ` 158` ``` show "inner (x + y) z = inner x z + inner y z" ``` huffman@29993 ` 159` ``` unfolding inner_real_def by (rule left_distrib) ``` huffman@29993 ` 160` ``` show "inner (scaleR r x) y = r * inner x y" ``` huffman@29993 ` 161` ``` unfolding inner_real_def real_scaleR_def by (rule mult_assoc) ``` huffman@29993 ` 162` ``` show "0 \ inner x x" ``` huffman@29993 ` 163` ``` unfolding inner_real_def by simp ``` huffman@29993 ` 164` ``` show "inner x x = 0 \ x = 0" ``` huffman@29993 ` 165` ``` unfolding inner_real_def by simp ``` huffman@29993 ` 166` ``` show "norm x = sqrt (inner x x)" ``` huffman@29993 ` 167` ``` unfolding inner_real_def by simp ``` huffman@29993 ` 168` ```qed ``` huffman@29993 ` 169` huffman@29993 ` 170` ```end ``` huffman@29993 ` 171` huffman@29993 ` 172` ```instantiation complex :: real_inner ``` huffman@29993 ` 173` ```begin ``` huffman@29993 ` 174` huffman@29993 ` 175` ```definition inner_complex_def: ``` huffman@29993 ` 176` ``` "inner x y = Re x * Re y + Im x * Im y" ``` huffman@29993 ` 177` huffman@29993 ` 178` ```instance proof ``` huffman@29993 ` 179` ``` fix x y z :: complex and r :: real ``` huffman@29993 ` 180` ``` show "inner x y = inner y x" ``` huffman@29993 ` 181` ``` unfolding inner_complex_def by (simp add: mult_commute) ``` huffman@29993 ` 182` ``` show "inner (x + y) z = inner x z + inner y z" ``` huffman@29993 ` 183` ``` unfolding inner_complex_def by (simp add: left_distrib) ``` huffman@29993 ` 184` ``` show "inner (scaleR r x) y = r * inner x y" ``` huffman@29993 ` 185` ``` unfolding inner_complex_def by (simp add: right_distrib) ``` huffman@29993 ` 186` ``` show "0 \ inner x x" ``` huffman@29993 ` 187` ``` unfolding inner_complex_def by (simp add: add_nonneg_nonneg) ``` huffman@29993 ` 188` ``` show "inner x x = 0 \ x = 0" ``` huffman@29993 ` 189` ``` unfolding inner_complex_def ``` huffman@29993 ` 190` ``` by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff) ``` huffman@29993 ` 191` ``` show "norm x = sqrt (inner x x)" ``` huffman@29993 ` 192` ``` unfolding inner_complex_def complex_norm_def ``` huffman@29993 ` 193` ``` by (simp add: power2_eq_square) ``` huffman@29993 ` 194` ```qed ``` huffman@29993 ` 195` huffman@29993 ` 196` ```end ``` huffman@29993 ` 197` huffman@29993 ` 198` huffman@29993 ` 199` ```subsection {* Gradient derivative *} ``` huffman@29993 ` 200` huffman@29993 ` 201` ```definition ``` huffman@29993 ` 202` ``` gderiv :: ``` huffman@29993 ` 203` ``` "['a::real_inner \ real, 'a, 'a] \ bool" ``` huffman@29993 ` 204` ``` ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) ``` huffman@29993 ` 205` ```where ``` huffman@29993 ` 206` ``` "GDERIV f x :> D \ FDERIV f x :> (\h. inner h D)" ``` huffman@29993 ` 207` huffman@29993 ` 208` ```lemma deriv_fderiv: "DERIV f x :> D \ FDERIV f x :> (\h. h * D)" ``` huffman@29993 ` 209` ``` by (simp only: deriv_def field_fderiv_def) ``` huffman@29993 ` 210` huffman@29993 ` 211` ```lemma gderiv_deriv [simp]: "GDERIV f x :> D \ DERIV f x :> D" ``` huffman@29993 ` 212` ``` by (simp only: gderiv_def deriv_fderiv inner_real_def) ``` huffman@29993 ` 213` huffman@29993 ` 214` ```lemma GDERIV_DERIV_compose: ``` huffman@29993 ` 215` ``` "\GDERIV f x :> df; DERIV g (f x) :> dg\ ``` huffman@29993 ` 216` ``` \ GDERIV (\x. g (f x)) x :> scaleR dg df" ``` huffman@29993 ` 217` ``` unfolding gderiv_def deriv_fderiv ``` huffman@29993 ` 218` ``` apply (drule (1) FDERIV_compose) ``` huffman@29993 ` 219` ``` apply (simp add: inner_scaleR_right mult_ac) ``` huffman@29993 ` 220` ``` done ``` huffman@29993 ` 221` huffman@29993 ` 222` ```lemma FDERIV_subst: "\FDERIV f x :> df; df = d\ \ FDERIV f x :> d" ``` huffman@29993 ` 223` ``` by simp ``` huffman@29993 ` 224` huffman@29993 ` 225` ```lemma GDERIV_subst: "\GDERIV f x :> df; df = d\ \ GDERIV f x :> d" ``` huffman@29993 ` 226` ``` by simp ``` huffman@29993 ` 227` huffman@29993 ` 228` ```lemma GDERIV_const: "GDERIV (\x. k) x :> 0" ``` huffman@29993 ` 229` ``` unfolding gderiv_def inner_right.zero by (rule FDERIV_const) ``` huffman@29993 ` 230` huffman@29993 ` 231` ```lemma GDERIV_add: ``` huffman@29993 ` 232` ``` "\GDERIV f x :> df; GDERIV g x :> dg\ ``` huffman@29993 ` 233` ``` \ GDERIV (\x. f x + g x) x :> df + dg" ``` huffman@29993 ` 234` ``` unfolding gderiv_def inner_right.add by (rule FDERIV_add) ``` huffman@29993 ` 235` huffman@29993 ` 236` ```lemma GDERIV_minus: ``` huffman@29993 ` 237` ``` "GDERIV f x :> df \ GDERIV (\x. - f x) x :> - df" ``` huffman@29993 ` 238` ``` unfolding gderiv_def inner_right.minus by (rule FDERIV_minus) ``` huffman@29993 ` 239` huffman@29993 ` 240` ```lemma GDERIV_diff: ``` huffman@29993 ` 241` ``` "\GDERIV f x :> df; GDERIV g x :> dg\ ``` huffman@29993 ` 242` ``` \ GDERIV (\x. f x - g x) x :> df - dg" ``` huffman@29993 ` 243` ``` unfolding gderiv_def inner_right.diff by (rule FDERIV_diff) ``` huffman@29993 ` 244` huffman@29993 ` 245` ```lemma GDERIV_scaleR: ``` huffman@29993 ` 246` ``` "\DERIV f x :> df; GDERIV g x :> dg\ ``` huffman@29993 ` 247` ``` \ GDERIV (\x. scaleR (f x) (g x)) x ``` huffman@29993 ` 248` ``` :> (scaleR (f x) dg + scaleR df (g x))" ``` huffman@29993 ` 249` ``` unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR ``` huffman@29993 ` 250` ``` apply (rule FDERIV_subst) ``` huffman@29993 ` 251` ``` apply (erule (1) scaleR.FDERIV) ``` huffman@29993 ` 252` ``` apply (simp add: mult_ac) ``` huffman@29993 ` 253` ``` done ``` huffman@29993 ` 254` huffman@29993 ` 255` ```lemma GDERIV_mult: ``` huffman@29993 ` 256` ``` "\GDERIV f x :> df; GDERIV g x :> dg\ ``` huffman@29993 ` 257` ``` \ GDERIV (\x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df" ``` huffman@29993 ` 258` ``` unfolding gderiv_def ``` huffman@29993 ` 259` ``` apply (rule FDERIV_subst) ``` huffman@29993 ` 260` ``` apply (erule (1) FDERIV_mult) ``` huffman@29993 ` 261` ``` apply (simp add: inner_distrib inner_scaleR mult_ac) ``` huffman@29993 ` 262` ``` done ``` huffman@29993 ` 263` huffman@29993 ` 264` ```lemma GDERIV_inverse: ``` huffman@29993 ` 265` ``` "\GDERIV f x :> df; f x \ 0\ ``` huffman@29993 ` 266` ``` \ GDERIV (\x. inverse (f x)) x :> - (inverse (f x))\ *\<^sub>R df" ``` huffman@29993 ` 267` ``` apply (erule GDERIV_DERIV_compose) ``` huffman@29993 ` 268` ``` apply (erule DERIV_inverse [folded numeral_2_eq_2]) ``` huffman@29993 ` 269` ``` done ``` huffman@29993 ` 270` huffman@29993 ` 271` ```lemma GDERIV_norm: ``` huffman@29993 ` 272` ``` assumes "x \ 0" shows "GDERIV (\x. norm x) x :> sgn x" ``` huffman@29993 ` 273` ```proof - ``` huffman@29993 ` 274` ``` have 1: "FDERIV (\x. inner x x) x :> (\h. inner x h + inner h x)" ``` huffman@29993 ` 275` ``` by (intro inner.FDERIV FDERIV_ident) ``` huffman@29993 ` 276` ``` have 2: "(\h. inner x h + inner h x) = (\h. inner h (scaleR 2 x))" ``` huffman@29993 ` 277` ``` by (simp add: expand_fun_eq inner_scaleR inner_commute) ``` huffman@29993 ` 278` ``` have "0 < inner x x" using `x \ 0` by simp ``` huffman@29993 ` 279` ``` then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)" ``` huffman@29993 ` 280` ``` by (rule DERIV_real_sqrt) ``` huffman@29993 ` 281` ``` have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x" ``` huffman@29993 ` 282` ``` by (simp add: sgn_div_norm norm_eq_sqrt_inner) ``` huffman@29993 ` 283` ``` show ?thesis ``` huffman@29993 ` 284` ``` unfolding norm_eq_sqrt_inner ``` huffman@29993 ` 285` ``` apply (rule GDERIV_subst [OF _ 4]) ``` huffman@29993 ` 286` ``` apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"]) ``` huffman@29993 ` 287` ``` apply (subst gderiv_def) ``` huffman@29993 ` 288` ``` apply (rule FDERIV_subst [OF _ 2]) ``` huffman@29993 ` 289` ``` apply (rule 1) ``` huffman@29993 ` 290` ``` apply (rule 3) ``` huffman@29993 ` 291` ``` done ``` huffman@29993 ` 292` ```qed ``` huffman@29993 ` 293` huffman@29993 ` 294` ```lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def] ``` huffman@29993 ` 295` huffman@29993 ` 296` ```end ```