src/HOL/Library/Inner_Product.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 44902 9ba11d41cd1f
child 49962 a8cc904a6820
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     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 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 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 {* Transfer distributivity rules to right argument. *}
    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 {* Legacy theorem names *}
    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)\<twosuperior> = inner x x"
    82   by (simp add: norm_eq_sqrt_inner)
    83 
    84 lemma Cauchy_Schwarz_ineq:
    85   "(inner x y)\<twosuperior> \<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)\<twosuperior> / inner y y"
    97     by (simp add: power2_eq_square inner_commute)
    98   finally have "0 \<le> inner x x - (inner x y)\<twosuperior> / inner y y" .
    99   hence "(inner x y)\<twosuperior> / inner y y \<le> inner x x"
   100     by (simp add: le_diff_eq)
   101   thus "(inner x y)\<twosuperior> \<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)\<twosuperior> \<le> inner x x * inner y y"
   109     using Cauchy_Schwarz_ineq .
   110   thus "\<bar>inner x y\<bar>\<twosuperior> \<le> (norm x * norm y)\<twosuperior>"
   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 subclass real_normed_vector
   118 proof
   119   fix a :: real and x y :: 'a
   120   show "0 \<le> norm x"
   121     unfolding norm_eq_sqrt_inner by simp
   122   show "norm x = 0 \<longleftrightarrow> x = 0"
   123     unfolding norm_eq_sqrt_inner by simp
   124   show "norm (x + y) \<le> norm x + norm y"
   125     proof (rule power2_le_imp_le)
   126       have "inner x y \<le> norm x * norm y"
   127         by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2])
   128       thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>"
   129         unfolding power2_sum power2_norm_eq_inner
   130         by (simp add: inner_add inner_commute)
   131       show "0 \<le> norm x + norm y"
   132         unfolding norm_eq_sqrt_inner by simp
   133     qed
   134   have "sqrt (a\<twosuperior> * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
   135     by (simp add: real_sqrt_mult_distrib)
   136   then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
   137     unfolding norm_eq_sqrt_inner
   138     by (simp add: power2_eq_square mult_assoc)
   139 qed
   140 
   141 end
   142 
   143 text {*
   144   Re-enable constraints for @{term "open"},
   145   @{term dist}, and @{term norm}.
   146 *}
   147 
   148 setup {* Sign.add_const_constraint
   149   (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}
   150 
   151 setup {* Sign.add_const_constraint
   152   (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
   153 
   154 setup {* Sign.add_const_constraint
   155   (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
   156 
   157 lemma bounded_bilinear_inner:
   158   "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
   159 proof
   160   fix x y z :: 'a and r :: real
   161   show "inner (x + y) z = inner x z + inner y z"
   162     by (rule inner_add_left)
   163   show "inner x (y + z) = inner x y + inner x z"
   164     by (rule inner_add_right)
   165   show "inner (scaleR r x) y = scaleR r (inner x y)"
   166     unfolding real_scaleR_def by (rule inner_scaleR_left)
   167   show "inner x (scaleR r y) = scaleR r (inner x y)"
   168     unfolding real_scaleR_def by (rule inner_scaleR_right)
   169   show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
   170   proof
   171     show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
   172       by (simp add: Cauchy_Schwarz_ineq2)
   173   qed
   174 qed
   175 
   176 lemmas tendsto_inner [tendsto_intros] =
   177   bounded_bilinear.tendsto [OF bounded_bilinear_inner]
   178 
   179 lemmas isCont_inner [simp] =
   180   bounded_bilinear.isCont [OF bounded_bilinear_inner]
   181 
   182 lemmas FDERIV_inner =
   183   bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
   184 
   185 lemmas bounded_linear_inner_left =
   186   bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
   187 
   188 lemmas bounded_linear_inner_right =
   189   bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
   190 
   191 
   192 subsection {* Class instances *}
   193 
   194 instantiation real :: real_inner
   195 begin
   196 
   197 definition inner_real_def [simp]: "inner = op *"
   198 
   199 instance proof
   200   fix x y z r :: real
   201   show "inner x y = inner y x"
   202     unfolding inner_real_def by (rule mult_commute)
   203   show "inner (x + y) z = inner x z + inner y z"
   204     unfolding inner_real_def by (rule left_distrib)
   205   show "inner (scaleR r x) y = r * inner x y"
   206     unfolding inner_real_def real_scaleR_def by (rule mult_assoc)
   207   show "0 \<le> inner x x"
   208     unfolding inner_real_def by simp
   209   show "inner x x = 0 \<longleftrightarrow> x = 0"
   210     unfolding inner_real_def by simp
   211   show "norm x = sqrt (inner x x)"
   212     unfolding inner_real_def by simp
   213 qed
   214 
   215 end
   216 
   217 instantiation complex :: real_inner
   218 begin
   219 
   220 definition inner_complex_def:
   221   "inner x y = Re x * Re y + Im x * Im y"
   222 
   223 instance proof
   224   fix x y z :: complex and r :: real
   225   show "inner x y = inner y x"
   226     unfolding inner_complex_def by (simp add: mult_commute)
   227   show "inner (x + y) z = inner x z + inner y z"
   228     unfolding inner_complex_def by (simp add: left_distrib)
   229   show "inner (scaleR r x) y = r * inner x y"
   230     unfolding inner_complex_def by (simp add: right_distrib)
   231   show "0 \<le> inner x x"
   232     unfolding inner_complex_def by simp
   233   show "inner x x = 0 \<longleftrightarrow> x = 0"
   234     unfolding inner_complex_def
   235     by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
   236   show "norm x = sqrt (inner x x)"
   237     unfolding inner_complex_def complex_norm_def
   238     by (simp add: power2_eq_square)
   239 qed
   240 
   241 end
   242 
   243 lemma complex_inner_1 [simp]: "inner 1 x = Re x"
   244   unfolding inner_complex_def by simp
   245 
   246 lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
   247   unfolding inner_complex_def by simp
   248 
   249 lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
   250   unfolding inner_complex_def by simp
   251 
   252 lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
   253   unfolding inner_complex_def by simp
   254 
   255 
   256 subsection {* Gradient derivative *}
   257 
   258 definition
   259   gderiv ::
   260     "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
   261           ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   262 where
   263   "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
   264 
   265 lemma deriv_fderiv: "DERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. h * D)"
   266   by (simp only: deriv_def field_fderiv_def)
   267 
   268 lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
   269   by (simp only: gderiv_def deriv_fderiv inner_real_def)
   270 
   271 lemma GDERIV_DERIV_compose:
   272     "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
   273      \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
   274   unfolding gderiv_def deriv_fderiv
   275   apply (drule (1) FDERIV_compose)
   276   apply (simp add: mult_ac)
   277   done
   278 
   279 lemma FDERIV_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   280   by simp
   281 
   282 lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
   283   by simp
   284 
   285 lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
   286   unfolding gderiv_def inner_zero_right by (rule FDERIV_const)
   287 
   288 lemma GDERIV_add:
   289     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   290      \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
   291   unfolding gderiv_def inner_add_right by (rule FDERIV_add)
   292 
   293 lemma GDERIV_minus:
   294     "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
   295   unfolding gderiv_def inner_minus_right by (rule FDERIV_minus)
   296 
   297 lemma GDERIV_diff:
   298     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   299      \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
   300   unfolding gderiv_def inner_diff_right by (rule FDERIV_diff)
   301 
   302 lemma GDERIV_scaleR:
   303     "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   304      \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
   305       :> (scaleR (f x) dg + scaleR df (g x))"
   306   unfolding gderiv_def deriv_fderiv inner_add_right inner_scaleR_right
   307   apply (rule FDERIV_subst)
   308   apply (erule (1) FDERIV_scaleR)
   309   apply (simp add: mult_ac)
   310   done
   311 
   312 lemma GDERIV_mult:
   313     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   314      \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
   315   unfolding gderiv_def
   316   apply (rule FDERIV_subst)
   317   apply (erule (1) FDERIV_mult)
   318   apply (simp add: inner_add mult_ac)
   319   done
   320 
   321 lemma GDERIV_inverse:
   322     "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
   323      \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<twosuperior> *\<^sub>R df"
   324   apply (erule GDERIV_DERIV_compose)
   325   apply (erule DERIV_inverse [folded numeral_2_eq_2])
   326   done
   327 
   328 lemma GDERIV_norm:
   329   assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
   330 proof -
   331   have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   332     by (intro FDERIV_inner FDERIV_ident)
   333   have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   334     by (simp add: fun_eq_iff inner_commute)
   335   have "0 < inner x x" using `x \<noteq> 0` by simp
   336   then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
   337     by (rule DERIV_real_sqrt)
   338   have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
   339     by (simp add: sgn_div_norm norm_eq_sqrt_inner)
   340   show ?thesis
   341     unfolding norm_eq_sqrt_inner
   342     apply (rule GDERIV_subst [OF _ 4])
   343     apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
   344     apply (subst gderiv_def)
   345     apply (rule FDERIV_subst [OF _ 2])
   346     apply (rule 1)
   347     apply (rule 3)
   348     done
   349 qed
   350 
   351 lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def]
   352 
   353 end