src/HOL/Analysis/Inner_Product.thy
author hoelzl
Fri Sep 30 15:35:37 2016 +0200 (2016-09-30)
changeset 63971 da89140186e2
parent 63886 src/HOL/Library/Inner_Product.thy@685fb01256af
child 64267 b9a1486e79be
permissions -rw-r--r--
HOL-Analysis: move Product_Vector and Inner_Product from Library
     1 (*  Title:      HOL/Analysis/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"}, @{term "uniformity"},
    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 uniformity}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
    26 
    27 setup \<open>Sign.add_const_constraint
    28   (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
    29 
    30 class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
    31   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    32   assumes inner_commute: "inner x y = inner y x"
    33   and inner_add_left: "inner (x + y) z = inner x z + inner y z"
    34   and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)"
    35   and inner_ge_zero [simp]: "0 \<le> inner x x"
    36   and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"
    37   and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"
    38 begin
    39 
    40 lemma inner_zero_left [simp]: "inner 0 x = 0"
    41   using inner_add_left [of 0 0 x] by simp
    42 
    43 lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
    44   using inner_add_left [of x "- x" y] by simp
    45 
    46 lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
    47   using inner_add_left [of x "- y" z] by simp
    48 
    49 lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
    50   by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
    51 
    52 text \<open>Transfer distributivity rules to right argument.\<close>
    53 
    54 lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    55   using inner_add_left [of y z x] by (simp only: inner_commute)
    56 
    57 lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"
    58   using inner_scaleR_left [of r y x] by (simp only: inner_commute)
    59 
    60 lemma inner_zero_right [simp]: "inner x 0 = 0"
    61   using inner_zero_left [of x] by (simp only: inner_commute)
    62 
    63 lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
    64   using inner_minus_left [of y x] by (simp only: inner_commute)
    65 
    66 lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    67   using inner_diff_left [of y z x] by (simp only: inner_commute)
    68 
    69 lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
    70   using inner_setsum_left [of f A x] by (simp only: inner_commute)
    71 
    72 lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
    73 lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
    74 lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    75 
    76 text \<open>Legacy theorem names\<close>
    77 lemmas inner_left_distrib = inner_add_left
    78 lemmas inner_right_distrib = inner_add_right
    79 lemmas inner_distrib = inner_left_distrib inner_right_distrib
    80 
    81 lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
    82   by (simp add: order_less_le)
    83 
    84 lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
    85   by (simp add: norm_eq_sqrt_inner)
    86 
    87 text \<open>Identities involving real multiplication and division.\<close>
    88 
    89 lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
    90   by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real)
    91 
    92 lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)"
    93   by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real)
    94 
    95 lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)"
    96   by (simp add: of_real_def)
    97 
    98 lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m"
    99   by (simp add: of_real_def real_inner_class.inner_scaleR_right)
   100 
   101 lemma Cauchy_Schwarz_ineq:
   102   "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   103 proof (cases)
   104   assume "y = 0"
   105   thus ?thesis by simp
   106 next
   107   assume y: "y \<noteq> 0"
   108   let ?r = "inner x y / inner y y"
   109   have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
   110     by (rule inner_ge_zero)
   111   also have "\<dots> = inner x x - inner y x * ?r"
   112     by (simp add: inner_diff)
   113   also have "\<dots> = inner x x - (inner x y)\<^sup>2 / inner y y"
   114     by (simp add: power2_eq_square inner_commute)
   115   finally have "0 \<le> inner x x - (inner x y)\<^sup>2 / inner y y" .
   116   hence "(inner x y)\<^sup>2 / inner y y \<le> inner x x"
   117     by (simp add: le_diff_eq)
   118   thus "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   119     by (simp add: pos_divide_le_eq y)
   120 qed
   121 
   122 lemma Cauchy_Schwarz_ineq2:
   123   "\<bar>inner x y\<bar> \<le> norm x * norm y"
   124 proof (rule power2_le_imp_le)
   125   have "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   126     using Cauchy_Schwarz_ineq .
   127   thus "\<bar>inner x y\<bar>\<^sup>2 \<le> (norm x * norm y)\<^sup>2"
   128     by (simp add: power_mult_distrib power2_norm_eq_inner)
   129   show "0 \<le> norm x * norm y"
   130     unfolding norm_eq_sqrt_inner
   131     by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
   132 qed
   133 
   134 lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y"
   135   using Cauchy_Schwarz_ineq2 [of x y] by auto
   136 
   137 subclass real_normed_vector
   138 proof
   139   fix a :: real and x y :: 'a
   140   show "norm x = 0 \<longleftrightarrow> x = 0"
   141     unfolding norm_eq_sqrt_inner by simp
   142   show "norm (x + y) \<le> norm x + norm y"
   143     proof (rule power2_le_imp_le)
   144       have "inner x y \<le> norm x * norm y"
   145         by (rule norm_cauchy_schwarz)
   146       thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
   147         unfolding power2_sum power2_norm_eq_inner
   148         by (simp add: inner_add inner_commute)
   149       show "0 \<le> norm x + norm y"
   150         unfolding norm_eq_sqrt_inner by simp
   151     qed
   152   have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
   153     by (simp add: real_sqrt_mult_distrib)
   154   then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
   155     unfolding norm_eq_sqrt_inner
   156     by (simp add: power2_eq_square mult.assoc)
   157 qed
   158 
   159 end
   160 
   161 lemma inner_divide_left:
   162   fixes a :: "'a :: {real_inner,real_div_algebra}"
   163   shows "inner (a / of_real m) b = (inner a b) / m"
   164   by (metis (no_types) divide_inverse inner_commute inner_scaleR_right mult.left_neutral mult.right_neutral mult_scaleR_right of_real_inverse scaleR_conv_of_real times_divide_eq_left)
   165 
   166 lemma inner_divide_right:
   167   fixes a :: "'a :: {real_inner,real_div_algebra}"
   168   shows "inner a (b / of_real m) = (inner a b) / m"
   169   by (metis inner_commute inner_divide_left)
   170 
   171 text \<open>
   172   Re-enable constraints for @{term "open"}, @{term "uniformity"},
   173   @{term dist}, and @{term norm}.
   174 \<close>
   175 
   176 setup \<open>Sign.add_const_constraint
   177   (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
   178 
   179 setup \<open>Sign.add_const_constraint
   180   (@{const_name uniformity}, SOME @{typ "('a::uniform_space \<times> 'a) filter"})\<close>
   181 
   182 setup \<open>Sign.add_const_constraint
   183   (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
   184 
   185 setup \<open>Sign.add_const_constraint
   186   (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
   187 
   188 lemma bounded_bilinear_inner:
   189   "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
   190 proof
   191   fix x y z :: 'a and r :: real
   192   show "inner (x + y) z = inner x z + inner y z"
   193     by (rule inner_add_left)
   194   show "inner x (y + z) = inner x y + inner x z"
   195     by (rule inner_add_right)
   196   show "inner (scaleR r x) y = scaleR r (inner x y)"
   197     unfolding real_scaleR_def by (rule inner_scaleR_left)
   198   show "inner x (scaleR r y) = scaleR r (inner x y)"
   199     unfolding real_scaleR_def by (rule inner_scaleR_right)
   200   show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
   201   proof
   202     show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
   203       by (simp add: Cauchy_Schwarz_ineq2)
   204   qed
   205 qed
   206 
   207 lemmas tendsto_inner [tendsto_intros] =
   208   bounded_bilinear.tendsto [OF bounded_bilinear_inner]
   209 
   210 lemmas isCont_inner [simp] =
   211   bounded_bilinear.isCont [OF bounded_bilinear_inner]
   212 
   213 lemmas has_derivative_inner [derivative_intros] =
   214   bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
   215 
   216 lemmas bounded_linear_inner_left =
   217   bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
   218 
   219 lemmas bounded_linear_inner_right =
   220   bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
   221 
   222 lemmas bounded_linear_inner_left_comp = bounded_linear_inner_left[THEN bounded_linear_compose]
   223 
   224 lemmas bounded_linear_inner_right_comp = bounded_linear_inner_right[THEN bounded_linear_compose]
   225 
   226 lemmas has_derivative_inner_right [derivative_intros] =
   227   bounded_linear.has_derivative [OF bounded_linear_inner_right]
   228 
   229 lemmas has_derivative_inner_left [derivative_intros] =
   230   bounded_linear.has_derivative [OF bounded_linear_inner_left]
   231 
   232 lemma differentiable_inner [simp]:
   233   "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"
   234   unfolding differentiable_def by (blast intro: has_derivative_inner)
   235 
   236 
   237 subsection \<open>Class instances\<close>
   238 
   239 instantiation real :: real_inner
   240 begin
   241 
   242 definition inner_real_def [simp]: "inner = op *"
   243 
   244 instance
   245 proof
   246   fix x y z r :: real
   247   show "inner x y = inner y x"
   248     unfolding inner_real_def by (rule mult.commute)
   249   show "inner (x + y) z = inner x z + inner y z"
   250     unfolding inner_real_def by (rule distrib_right)
   251   show "inner (scaleR r x) y = r * inner x y"
   252     unfolding inner_real_def real_scaleR_def by (rule mult.assoc)
   253   show "0 \<le> inner x x"
   254     unfolding inner_real_def by simp
   255   show "inner x x = 0 \<longleftrightarrow> x = 0"
   256     unfolding inner_real_def by simp
   257   show "norm x = sqrt (inner x x)"
   258     unfolding inner_real_def by simp
   259 qed
   260 
   261 end
   262 
   263 lemma
   264   shows real_inner_1_left[simp]: "inner 1 x = x"
   265     and real_inner_1_right[simp]: "inner x 1 = x"
   266   by simp_all
   267 
   268 instantiation complex :: real_inner
   269 begin
   270 
   271 definition inner_complex_def:
   272   "inner x y = Re x * Re y + Im x * Im y"
   273 
   274 instance
   275 proof
   276   fix x y z :: complex and r :: real
   277   show "inner x y = inner y x"
   278     unfolding inner_complex_def by (simp add: mult.commute)
   279   show "inner (x + y) z = inner x z + inner y z"
   280     unfolding inner_complex_def by (simp add: distrib_right)
   281   show "inner (scaleR r x) y = r * inner x y"
   282     unfolding inner_complex_def by (simp add: distrib_left)
   283   show "0 \<le> inner x x"
   284     unfolding inner_complex_def by simp
   285   show "inner x x = 0 \<longleftrightarrow> x = 0"
   286     unfolding inner_complex_def
   287     by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
   288   show "norm x = sqrt (inner x x)"
   289     unfolding inner_complex_def complex_norm_def
   290     by (simp add: power2_eq_square)
   291 qed
   292 
   293 end
   294 
   295 lemma complex_inner_1 [simp]: "inner 1 x = Re x"
   296   unfolding inner_complex_def by simp
   297 
   298 lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
   299   unfolding inner_complex_def by simp
   300 
   301 lemma complex_inner_ii_left [simp]: "inner \<i> x = Im x"
   302   unfolding inner_complex_def by simp
   303 
   304 lemma complex_inner_ii_right [simp]: "inner x \<i> = Im x"
   305   unfolding inner_complex_def by simp
   306 
   307 
   308 subsection \<open>Gradient derivative\<close>
   309 
   310 definition
   311   gderiv ::
   312     "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
   313           ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   314 where
   315   "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
   316 
   317 lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
   318   by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)
   319 
   320 lemma GDERIV_DERIV_compose:
   321     "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
   322      \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
   323   unfolding gderiv_def has_field_derivative_def
   324   apply (drule (1) has_derivative_compose)
   325   apply (simp add: ac_simps)
   326   done
   327 
   328 lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   329   by simp
   330 
   331 lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
   332   by simp
   333 
   334 lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
   335   unfolding gderiv_def inner_zero_right by (rule has_derivative_const)
   336 
   337 lemma GDERIV_add:
   338     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   339      \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
   340   unfolding gderiv_def inner_add_right by (rule has_derivative_add)
   341 
   342 lemma GDERIV_minus:
   343     "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
   344   unfolding gderiv_def inner_minus_right by (rule has_derivative_minus)
   345 
   346 lemma GDERIV_diff:
   347     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   348      \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
   349   unfolding gderiv_def inner_diff_right by (rule has_derivative_diff)
   350 
   351 lemma GDERIV_scaleR:
   352     "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   353      \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
   354       :> (scaleR (f x) dg + scaleR df (g x))"
   355   unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
   356   apply (rule has_derivative_subst)
   357   apply (erule (1) has_derivative_scaleR)
   358   apply (simp add: ac_simps)
   359   done
   360 
   361 lemma GDERIV_mult:
   362     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   363      \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
   364   unfolding gderiv_def
   365   apply (rule has_derivative_subst)
   366   apply (erule (1) has_derivative_mult)
   367   apply (simp add: inner_add ac_simps)
   368   done
   369 
   370 lemma GDERIV_inverse:
   371     "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
   372      \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
   373   apply (erule GDERIV_DERIV_compose)
   374   apply (erule DERIV_inverse [folded numeral_2_eq_2])
   375   done
   376 
   377 lemma GDERIV_norm:
   378   assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
   379 proof -
   380   have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
   381     by (intro has_derivative_inner has_derivative_ident)
   382   have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
   383     by (simp add: fun_eq_iff inner_commute)
   384   have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp
   385   then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
   386     by (rule DERIV_real_sqrt)
   387   have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
   388     by (simp add: sgn_div_norm norm_eq_sqrt_inner)
   389   show ?thesis
   390     unfolding norm_eq_sqrt_inner
   391     apply (rule GDERIV_subst [OF _ 4])
   392     apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
   393     apply (subst gderiv_def)
   394     apply (rule has_derivative_subst [OF _ 2])
   395     apply (rule 1)
   396     apply (rule 3)
   397     done
   398 qed
   399 
   400 lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
   401 
   402 end