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