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