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