src/HOL/Library/Inner_Product.thy
author nipkow
Tue Sep 22 14:31:22 2015 +0200 (2015-09-22)
changeset 61225 1a690dce8cfc
parent 60679 ade12ef2773c
child 61518 ff12606337e9
permissions -rw-r--r--
tuned references
     1 (*  Title:      HOL/Library/Inner_Product.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section \<open>Inner Product Spaces and the Gradient Derivative\<close>
     6 
     7 theory Inner_Product
     8 imports "~~/src/HOL/Complex_Main"
     9 begin
    10 
    11 subsection \<open>Real inner product spaces\<close>
    12 
    13 text \<open>
    14   Temporarily relax type constraints for @{term "open"},
    15   @{term dist}, and @{term norm}.
    16 \<close>
    17 
    18 setup \<open>Sign.add_const_constraint
    19   (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"})\<close>
    20 
    21 setup \<open>Sign.add_const_constraint
    22   (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
    23 
    24 setup \<open>Sign.add_const_constraint
    25   (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
    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   using inner_add_left [of x "- y" z] by simp
    45 
    46 lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
    47   by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
    48 
    49 text \<open>Transfer distributivity rules to right argument.\<close>
    50 
    51 lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    52   using inner_add_left [of y z x] by (simp only: inner_commute)
    53 
    54 lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"
    55   using inner_scaleR_left [of r y x] by (simp only: inner_commute)
    56 
    57 lemma inner_zero_right [simp]: "inner x 0 = 0"
    58   using inner_zero_left [of x] by (simp only: inner_commute)
    59 
    60 lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
    61   using inner_minus_left [of y x] by (simp only: inner_commute)
    62 
    63 lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    64   using inner_diff_left [of y z x] by (simp only: inner_commute)
    65 
    66 lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
    67   using inner_setsum_left [of f A x] by (simp only: inner_commute)
    68 
    69 lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
    70 lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
    71 lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    72 
    73 text \<open>Legacy theorem names\<close>
    74 lemmas inner_left_distrib = inner_add_left
    75 lemmas inner_right_distrib = inner_add_right
    76 lemmas inner_distrib = inner_left_distrib inner_right_distrib
    77 
    78 lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
    79   by (simp add: order_less_le)
    80 
    81 lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
    82   by (simp add: norm_eq_sqrt_inner)
    83 
    84 lemma Cauchy_Schwarz_ineq:
    85   "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
    86 proof (cases)
    87   assume "y = 0"
    88   thus ?thesis by simp
    89 next
    90   assume y: "y \<noteq> 0"
    91   let ?r = "inner x y / inner y y"
    92   have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
    93     by (rule inner_ge_zero)
    94   also have "\<dots> = inner x x - inner y x * ?r"
    95     by (simp add: inner_diff)
    96   also have "\<dots> = inner x x - (inner x y)\<^sup>2 / inner y y"
    97     by (simp add: power2_eq_square inner_commute)
    98   finally have "0 \<le> inner x x - (inner x y)\<^sup>2 / inner y y" .
    99   hence "(inner x y)\<^sup>2 / inner y y \<le> inner x x"
   100     by (simp add: le_diff_eq)
   101   thus "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   102     by (simp add: pos_divide_le_eq y)
   103 qed
   104 
   105 lemma Cauchy_Schwarz_ineq2:
   106   "\<bar>inner x y\<bar> \<le> norm x * norm y"
   107 proof (rule power2_le_imp_le)
   108   have "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   109     using Cauchy_Schwarz_ineq .
   110   thus "\<bar>inner x y\<bar>\<^sup>2 \<le> (norm x * norm y)\<^sup>2"
   111     by (simp add: power_mult_distrib power2_norm_eq_inner)
   112   show "0 \<le> norm x * norm y"
   113     unfolding norm_eq_sqrt_inner
   114     by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
   115 qed
   116 
   117 lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y"
   118   using Cauchy_Schwarz_ineq2 [of x y] by auto
   119 
   120 subclass real_normed_vector
   121 proof
   122   fix a :: real and x y :: 'a
   123   show "norm x = 0 \<longleftrightarrow> x = 0"
   124     unfolding norm_eq_sqrt_inner by simp
   125   show "norm (x + y) \<le> norm x + norm y"
   126     proof (rule power2_le_imp_le)
   127       have "inner x y \<le> norm x * norm y"
   128         by (rule norm_cauchy_schwarz)
   129       thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
   130         unfolding power2_sum power2_norm_eq_inner
   131         by (simp add: inner_add inner_commute)
   132       show "0 \<le> norm x + norm y"
   133         unfolding norm_eq_sqrt_inner by simp
   134     qed
   135   have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
   136     by (simp add: real_sqrt_mult_distrib)
   137   then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
   138     unfolding norm_eq_sqrt_inner
   139     by (simp add: power2_eq_square mult.assoc)
   140 qed
   141 
   142 end
   143 
   144 text \<open>
   145   Re-enable constraints for @{term "open"},
   146   @{term dist}, and @{term norm}.
   147 \<close>
   148 
   149 setup \<open>Sign.add_const_constraint
   150   (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
   151 
   152 setup \<open>Sign.add_const_constraint
   153   (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
   154 
   155 setup \<open>Sign.add_const_constraint
   156   (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
   157 
   158 lemma bounded_bilinear_inner:
   159   "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
   160 proof
   161   fix x y z :: 'a and r :: real
   162   show "inner (x + y) z = inner x z + inner y z"
   163     by (rule inner_add_left)
   164   show "inner x (y + z) = inner x y + inner x z"
   165     by (rule inner_add_right)
   166   show "inner (scaleR r x) y = scaleR r (inner x y)"
   167     unfolding real_scaleR_def by (rule inner_scaleR_left)
   168   show "inner x (scaleR r y) = scaleR r (inner x y)"
   169     unfolding real_scaleR_def by (rule inner_scaleR_right)
   170   show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
   171   proof
   172     show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
   173       by (simp add: Cauchy_Schwarz_ineq2)
   174   qed
   175 qed
   176 
   177 lemmas tendsto_inner [tendsto_intros] =
   178   bounded_bilinear.tendsto [OF bounded_bilinear_inner]
   179 
   180 lemmas isCont_inner [simp] =
   181   bounded_bilinear.isCont [OF bounded_bilinear_inner]
   182 
   183 lemmas has_derivative_inner [derivative_intros] =
   184   bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
   185 
   186 lemmas bounded_linear_inner_left =
   187   bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
   188 
   189 lemmas bounded_linear_inner_right =
   190   bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
   191 
   192 lemmas has_derivative_inner_right [derivative_intros] =
   193   bounded_linear.has_derivative [OF bounded_linear_inner_right]
   194 
   195 lemmas has_derivative_inner_left [derivative_intros] =
   196   bounded_linear.has_derivative [OF bounded_linear_inner_left]
   197 
   198 lemma differentiable_inner [simp]:
   199   "f differentiable (at x within s) \<Longrightarrow> g differentiable at x within s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable at x within s"
   200   unfolding differentiable_def by (blast intro: has_derivative_inner)
   201 
   202 
   203 subsection \<open>Class instances\<close>
   204 
   205 instantiation real :: real_inner
   206 begin
   207 
   208 definition inner_real_def [simp]: "inner = op *"
   209 
   210 instance
   211 proof
   212   fix x y z r :: real
   213   show "inner x y = inner y x"
   214     unfolding inner_real_def by (rule mult.commute)
   215   show "inner (x + y) z = inner x z + inner y z"
   216     unfolding inner_real_def by (rule distrib_right)
   217   show "inner (scaleR r x) y = r * inner x y"
   218     unfolding inner_real_def real_scaleR_def by (rule mult.assoc)
   219   show "0 \<le> inner x x"
   220     unfolding inner_real_def by simp
   221   show "inner x x = 0 \<longleftrightarrow> x = 0"
   222     unfolding inner_real_def by simp
   223   show "norm x = sqrt (inner x x)"
   224     unfolding inner_real_def by simp
   225 qed
   226 
   227 end
   228 
   229 instantiation complex :: real_inner
   230 begin
   231 
   232 definition inner_complex_def:
   233   "inner x y = Re x * Re y + Im x * Im y"
   234 
   235 instance
   236 proof
   237   fix x y z :: complex and r :: real
   238   show "inner x y = inner y x"
   239     unfolding inner_complex_def by (simp add: mult.commute)
   240   show "inner (x + y) z = inner x z + inner y z"
   241     unfolding inner_complex_def by (simp add: distrib_right)
   242   show "inner (scaleR r x) y = r * inner x y"
   243     unfolding inner_complex_def by (simp add: distrib_left)
   244   show "0 \<le> inner x x"
   245     unfolding inner_complex_def by simp
   246   show "inner x x = 0 \<longleftrightarrow> x = 0"
   247     unfolding inner_complex_def
   248     by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
   249   show "norm x = sqrt (inner x x)"
   250     unfolding inner_complex_def complex_norm_def
   251     by (simp add: power2_eq_square)
   252 qed
   253 
   254 end
   255 
   256 lemma complex_inner_1 [simp]: "inner 1 x = Re x"
   257   unfolding inner_complex_def by simp
   258 
   259 lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
   260   unfolding inner_complex_def by simp
   261 
   262 lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
   263   unfolding inner_complex_def by simp
   264 
   265 lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
   266   unfolding inner_complex_def by simp
   267 
   268 
   269 subsection \<open>Gradient derivative\<close>
   270 
   271 definition
   272   gderiv ::
   273     "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
   274           ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   275 where
   276   "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
   277 
   278 lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
   279   by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)
   280 
   281 lemma GDERIV_DERIV_compose:
   282     "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
   283      \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
   284   unfolding gderiv_def has_field_derivative_def
   285   apply (drule (1) has_derivative_compose)
   286   apply (simp add: ac_simps)
   287   done
   288 
   289 lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   290   by simp
   291 
   292 lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
   293   by simp
   294 
   295 lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
   296   unfolding gderiv_def inner_zero_right by (rule has_derivative_const)
   297 
   298 lemma GDERIV_add:
   299     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   300      \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
   301   unfolding gderiv_def inner_add_right by (rule has_derivative_add)
   302 
   303 lemma GDERIV_minus:
   304     "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
   305   unfolding gderiv_def inner_minus_right by (rule has_derivative_minus)
   306 
   307 lemma GDERIV_diff:
   308     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   309      \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
   310   unfolding gderiv_def inner_diff_right by (rule has_derivative_diff)
   311 
   312 lemma GDERIV_scaleR:
   313     "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   314      \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
   315       :> (scaleR (f x) dg + scaleR df (g x))"
   316   unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
   317   apply (rule has_derivative_subst)
   318   apply (erule (1) has_derivative_scaleR)
   319   apply (simp add: ac_simps)
   320   done
   321 
   322 lemma GDERIV_mult:
   323     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   324      \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
   325   unfolding gderiv_def
   326   apply (rule has_derivative_subst)
   327   apply (erule (1) has_derivative_mult)
   328   apply (simp add: inner_add ac_simps)
   329   done
   330 
   331 lemma GDERIV_inverse:
   332     "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
   333      \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
   334   apply (erule GDERIV_DERIV_compose)
   335   apply (erule DERIV_inverse [folded numeral_2_eq_2])
   336   done
   337 
   338 lemma GDERIV_norm:
   339   assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
   340 proof -
   341   have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   342     by (intro has_derivative_inner has_derivative_ident)
   343   have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   344     by (simp add: fun_eq_iff inner_commute)
   345   have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp
   346   then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
   347     by (rule DERIV_real_sqrt)
   348   have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
   349     by (simp add: sgn_div_norm norm_eq_sqrt_inner)
   350   show ?thesis
   351     unfolding norm_eq_sqrt_inner
   352     apply (rule GDERIV_subst [OF _ 4])
   353     apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
   354     apply (subst gderiv_def)
   355     apply (rule has_derivative_subst [OF _ 2])
   356     apply (rule 1)
   357     apply (rule 3)
   358     done
   359 qed
   360 
   361 lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
   362 
   363 end