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