src/HOL/Analysis/Inner_Product.thy
author immler
Thu May 03 15:07:14 2018 +0200 (15 months ago)
changeset 68073 fad29d2a17a5
parent 68072 493b818e8e10
child 68499 d4312962161a
permissions -rw-r--r--
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
     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 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%important 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_sum_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 lemma all_zero_iff [simp]: "(\<forall>u. inner x u = 0) \<longleftrightarrow> (x = 0)"
    53   by auto (use inner_eq_zero_iff in blast)
    54 
    55 text \<open>Transfer distributivity rules to right argument.\<close>
    56 
    57 lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
    58   using inner_add_left [of y z x] by (simp only: inner_commute)
    59 
    60 lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"
    61   using inner_scaleR_left [of r y x] by (simp only: inner_commute)
    62 
    63 lemma inner_zero_right [simp]: "inner x 0 = 0"
    64   using inner_zero_left [of x] by (simp only: inner_commute)
    65 
    66 lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
    67   using inner_minus_left [of y x] by (simp only: inner_commute)
    68 
    69 lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
    70   using inner_diff_left [of y z x] by (simp only: inner_commute)
    71 
    72 lemma inner_sum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
    73   using inner_sum_left [of f A x] by (simp only: inner_commute)
    74 
    75 lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
    76 lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
    77 lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
    78 
    79 text \<open>Legacy theorem names\<close>
    80 lemmas inner_left_distrib = inner_add_left
    81 lemmas inner_right_distrib = inner_add_right
    82 lemmas inner_distrib = inner_left_distrib inner_right_distrib
    83 
    84 lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
    85   by (simp add: order_less_le)
    86 
    87 lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
    88   by (simp add: norm_eq_sqrt_inner)
    89 
    90 text \<open>Identities involving real multiplication and division.\<close>
    91 
    92 lemma inner_mult_left: "inner (of_real m * a) b = m * (inner a b)"
    93   by (metis real_inner_class.inner_scaleR_left scaleR_conv_of_real)
    94 
    95 lemma inner_mult_right: "inner a (of_real m * b) = m * (inner a b)"
    96   by (metis real_inner_class.inner_scaleR_right scaleR_conv_of_real)
    97 
    98 lemma inner_mult_left': "inner (a * of_real m) b = m * (inner a b)"
    99   by (simp add: of_real_def)
   100 
   101 lemma inner_mult_right': "inner a (b * of_real m) = (inner a b) * m"
   102   by (simp add: of_real_def real_inner_class.inner_scaleR_right)
   103 
   104 lemma Cauchy_Schwarz_ineq:
   105   "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   106 proof (cases)
   107   assume "y = 0"
   108   thus ?thesis by simp
   109 next
   110   assume y: "y \<noteq> 0"
   111   let ?r = "inner x y / inner y y"
   112   have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
   113     by (rule inner_ge_zero)
   114   also have "\<dots> = inner x x - inner y x * ?r"
   115     by (simp add: inner_diff)
   116   also have "\<dots> = inner x x - (inner x y)\<^sup>2 / inner y y"
   117     by (simp add: power2_eq_square inner_commute)
   118   finally have "0 \<le> inner x x - (inner x y)\<^sup>2 / inner y y" .
   119   hence "(inner x y)\<^sup>2 / inner y y \<le> inner x x"
   120     by (simp add: le_diff_eq)
   121   thus "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   122     by (simp add: pos_divide_le_eq y)
   123 qed
   124 
   125 lemma Cauchy_Schwarz_ineq2:
   126   "\<bar>inner x y\<bar> \<le> norm x * norm y"
   127 proof (rule power2_le_imp_le)
   128   have "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
   129     using Cauchy_Schwarz_ineq .
   130   thus "\<bar>inner x y\<bar>\<^sup>2 \<le> (norm x * norm y)\<^sup>2"
   131     by (simp add: power_mult_distrib power2_norm_eq_inner)
   132   show "0 \<le> norm x * norm y"
   133     unfolding norm_eq_sqrt_inner
   134     by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
   135 qed
   136 
   137 lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y"
   138   using Cauchy_Schwarz_ineq2 [of x y] by auto
   139 
   140 subclass real_normed_vector
   141 proof
   142   fix a :: real and x y :: 'a
   143   show "norm x = 0 \<longleftrightarrow> x = 0"
   144     unfolding norm_eq_sqrt_inner by simp
   145   show "norm (x + y) \<le> norm x + norm y"
   146     proof (rule power2_le_imp_le)
   147       have "inner x y \<le> norm x * norm y"
   148         by (rule norm_cauchy_schwarz)
   149       thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
   150         unfolding power2_sum power2_norm_eq_inner
   151         by (simp add: inner_add inner_commute)
   152       show "0 \<le> norm x + norm y"
   153         unfolding norm_eq_sqrt_inner by simp
   154     qed
   155   have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
   156     by (simp add: real_sqrt_mult_distrib)
   157   then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
   158     unfolding norm_eq_sqrt_inner
   159     by (simp add: power2_eq_square mult.assoc)
   160 qed
   161 
   162 end
   163 
   164 lemma square_bound_lemma:
   165   fixes x :: real
   166   shows "x < (1 + x) * (1 + x)"
   167 proof -
   168   have "(x + 1/2)\<^sup>2 + 3/4 > 0"
   169     using zero_le_power2[of "x+1/2"] by arith
   170   then show ?thesis
   171     by (simp add: field_simps power2_eq_square)
   172 qed
   173 
   174 lemma square_continuous:
   175   fixes e :: real
   176   shows "e > 0 \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> \<bar>y * y - x * x\<bar> < e)"
   177   using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
   178   by (force simp add: power2_eq_square)
   179 
   180 lemma norm_triangle_sub:
   181   fixes x y :: "'a::real_normed_vector"
   182   shows "norm x \<le> norm y + norm (x - y)"
   183   using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
   184 
   185 lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
   186   by (simp add: norm_eq_sqrt_inner)
   187 
   188 lemma norm_lt: "norm x < norm y \<longleftrightarrow> inner x x < inner y y"
   189   by (simp add: norm_eq_sqrt_inner)
   190 
   191 lemma norm_eq: "norm x = norm y \<longleftrightarrow> inner x x = inner y y"
   192   apply (subst order_eq_iff)
   193   apply (auto simp: norm_le)
   194   done
   195 
   196 lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> inner x x = 1"
   197   by (simp add: norm_eq_sqrt_inner)
   198 
   199 lemma inner_divide_left:
   200   fixes a :: "'a :: {real_inner,real_div_algebra}"
   201   shows "inner (a / of_real m) b = (inner a b) / m"
   202   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)
   203 
   204 lemma inner_divide_right:
   205   fixes a :: "'a :: {real_inner,real_div_algebra}"
   206   shows "inner a (b / of_real m) = (inner a b) / m"
   207   by (metis inner_commute inner_divide_left)
   208 
   209 text \<open>
   210   Re-enable constraints for @{term "open"}, @{term "uniformity"},
   211   @{term dist}, and @{term norm}.
   212 \<close>
   213 
   214 setup \<open>Sign.add_const_constraint
   215   (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
   216 
   217 setup \<open>Sign.add_const_constraint
   218   (@{const_name uniformity}, SOME @{typ "('a::uniform_space \<times> 'a) filter"})\<close>
   219 
   220 setup \<open>Sign.add_const_constraint
   221   (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
   222 
   223 setup \<open>Sign.add_const_constraint
   224   (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
   225 
   226 lemma bounded_bilinear_inner:
   227   "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
   228 proof
   229   fix x y z :: 'a and r :: real
   230   show "inner (x + y) z = inner x z + inner y z"
   231     by (rule inner_add_left)
   232   show "inner x (y + z) = inner x y + inner x z"
   233     by (rule inner_add_right)
   234   show "inner (scaleR r x) y = scaleR r (inner x y)"
   235     unfolding real_scaleR_def by (rule inner_scaleR_left)
   236   show "inner x (scaleR r y) = scaleR r (inner x y)"
   237     unfolding real_scaleR_def by (rule inner_scaleR_right)
   238   show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
   239   proof
   240     show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
   241       by (simp add: Cauchy_Schwarz_ineq2)
   242   qed
   243 qed
   244 
   245 lemmas tendsto_inner [tendsto_intros] =
   246   bounded_bilinear.tendsto [OF bounded_bilinear_inner]
   247 
   248 lemmas isCont_inner [simp] =
   249   bounded_bilinear.isCont [OF bounded_bilinear_inner]
   250 
   251 lemmas has_derivative_inner [derivative_intros] =
   252   bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
   253 
   254 lemmas bounded_linear_inner_left =
   255   bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
   256 
   257 lemmas bounded_linear_inner_right =
   258   bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
   259 
   260 lemmas bounded_linear_inner_left_comp = bounded_linear_inner_left[THEN bounded_linear_compose]
   261 
   262 lemmas bounded_linear_inner_right_comp = bounded_linear_inner_right[THEN bounded_linear_compose]
   263 
   264 lemmas has_derivative_inner_right [derivative_intros] =
   265   bounded_linear.has_derivative [OF bounded_linear_inner_right]
   266 
   267 lemmas has_derivative_inner_left [derivative_intros] =
   268   bounded_linear.has_derivative [OF bounded_linear_inner_left]
   269 
   270 lemma differentiable_inner [simp]:
   271   "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"
   272   unfolding differentiable_def by (blast intro: has_derivative_inner)
   273 
   274 
   275 subsection \<open>Class instances\<close>
   276 
   277 instantiation%important real :: real_inner
   278 begin
   279 
   280 definition inner_real_def [simp]: "inner = ( * )"
   281 
   282 instance
   283 proof
   284   fix x y z r :: real
   285   show "inner x y = inner y x"
   286     unfolding inner_real_def by (rule mult.commute)
   287   show "inner (x + y) z = inner x z + inner y z"
   288     unfolding inner_real_def by (rule distrib_right)
   289   show "inner (scaleR r x) y = r * inner x y"
   290     unfolding inner_real_def real_scaleR_def by (rule mult.assoc)
   291   show "0 \<le> inner x x"
   292     unfolding inner_real_def by simp
   293   show "inner x x = 0 \<longleftrightarrow> x = 0"
   294     unfolding inner_real_def by simp
   295   show "norm x = sqrt (inner x x)"
   296     unfolding inner_real_def by simp
   297 qed
   298 
   299 end
   300 
   301 lemma
   302   shows real_inner_1_left[simp]: "inner 1 x = x"
   303     and real_inner_1_right[simp]: "inner x 1 = x"
   304   by simp_all
   305 
   306 instantiation%important complex :: real_inner
   307 begin
   308 
   309 definition inner_complex_def:
   310   "inner x y = Re x * Re y + Im x * Im y"
   311 
   312 instance
   313 proof
   314   fix x y z :: complex and r :: real
   315   show "inner x y = inner y x"
   316     unfolding inner_complex_def by (simp add: mult.commute)
   317   show "inner (x + y) z = inner x z + inner y z"
   318     unfolding inner_complex_def by (simp add: distrib_right)
   319   show "inner (scaleR r x) y = r * inner x y"
   320     unfolding inner_complex_def by (simp add: distrib_left)
   321   show "0 \<le> inner x x"
   322     unfolding inner_complex_def by simp
   323   show "inner x x = 0 \<longleftrightarrow> x = 0"
   324     unfolding inner_complex_def
   325     by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
   326   show "norm x = sqrt (inner x x)"
   327     unfolding inner_complex_def complex_norm_def
   328     by (simp add: power2_eq_square)
   329 qed
   330 
   331 end
   332 
   333 lemma complex_inner_1 [simp]: "inner 1 x = Re x"
   334   unfolding inner_complex_def by simp
   335 
   336 lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
   337   unfolding inner_complex_def by simp
   338 
   339 lemma complex_inner_i_left [simp]: "inner \<i> x = Im x"
   340   unfolding inner_complex_def by simp
   341 
   342 lemma complex_inner_i_right [simp]: "inner x \<i> = Im x"
   343   unfolding inner_complex_def by simp
   344 
   345 
   346 lemma dot_square_norm: "inner x x = (norm x)\<^sup>2"
   347   by (simp only: power2_norm_eq_inner) (* TODO: move? *)
   348 
   349 lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> inner x x = a\<^sup>2"
   350   by (auto simp add: norm_eq_sqrt_inner)
   351 
   352 lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> inner x x \<le> a\<^sup>2"
   353   apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
   354   using norm_ge_zero[of x]
   355   apply arith
   356   done
   357 
   358 lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> inner x x \<ge> a\<^sup>2"
   359   apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
   360   using norm_ge_zero[of x]
   361   apply arith
   362   done
   363 
   364 lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> inner x x < a\<^sup>2"
   365   by (metis not_le norm_ge_square)
   366 
   367 lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> inner x x > a\<^sup>2"
   368   by (metis norm_le_square not_less)
   369 
   370 text\<open>Dot product in terms of the norm rather than conversely.\<close>
   371 
   372 lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
   373   inner_scaleR_left inner_scaleR_right
   374 
   375 lemma dot_norm: "inner x y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
   376   by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
   377 
   378 lemma dot_norm_neg: "inner x y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
   379   by (simp only: power2_norm_eq_inner inner_simps inner_commute)
   380     (auto simp add: algebra_simps)
   381 
   382 lemma of_real_inner_1 [simp]: 
   383   "inner (of_real x) (1 :: 'a :: {real_inner, real_normed_algebra_1}) = x"
   384   by (simp add: of_real_def dot_square_norm)
   385   
   386 lemma summable_of_real_iff: 
   387   "summable (\<lambda>x. of_real (f x) :: 'a :: {real_normed_algebra_1,real_inner}) \<longleftrightarrow> summable f"
   388 proof
   389   assume *: "summable (\<lambda>x. of_real (f x) :: 'a)"
   390   interpret bounded_linear "\<lambda>x::'a. inner x 1"
   391     by (rule bounded_linear_inner_left)
   392   from summable [OF *] show "summable f" by simp
   393 qed (auto intro: summable_of_real)
   394 
   395 
   396 subsection \<open>Gradient derivative\<close>
   397 
   398 definition%important
   399   gderiv ::
   400     "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
   401           ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
   402 where
   403   "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
   404 
   405 lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
   406   by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)
   407 
   408 lemma GDERIV_DERIV_compose:
   409     "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
   410      \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
   411   unfolding gderiv_def has_field_derivative_def
   412   apply (drule (1) has_derivative_compose)
   413   apply (simp add: ac_simps)
   414   done
   415 
   416 lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
   417   by simp
   418 
   419 lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
   420   by simp
   421 
   422 lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
   423   unfolding gderiv_def inner_zero_right by (rule has_derivative_const)
   424 
   425 lemma GDERIV_add:
   426     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   427      \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
   428   unfolding gderiv_def inner_add_right by (rule has_derivative_add)
   429 
   430 lemma GDERIV_minus:
   431     "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
   432   unfolding gderiv_def inner_minus_right by (rule has_derivative_minus)
   433 
   434 lemma GDERIV_diff:
   435     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   436      \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
   437   unfolding gderiv_def inner_diff_right by (rule has_derivative_diff)
   438 
   439 lemma GDERIV_scaleR:
   440     "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   441      \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
   442       :> (scaleR (f x) dg + scaleR df (g x))"
   443   unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
   444   apply (rule has_derivative_subst)
   445   apply (erule (1) has_derivative_scaleR)
   446   apply (simp add: ac_simps)
   447   done
   448 
   449 lemma GDERIV_mult:
   450     "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
   451      \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
   452   unfolding gderiv_def
   453   apply (rule has_derivative_subst)
   454   apply (erule (1) has_derivative_mult)
   455   apply (simp add: inner_add ac_simps)
   456   done
   457 
   458 lemma GDERIV_inverse:
   459     "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
   460      \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
   461   by (metis DERIV_inverse GDERIV_DERIV_compose numerals(2))
   462   
   463 lemma GDERIV_norm:
   464   assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
   465     unfolding gderiv_def norm_eq_sqrt_inner
   466     by (rule derivative_eq_intros | force simp add: inner_commute sgn_div_norm norm_eq_sqrt_inner assms)+
   467 
   468 lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
   469 
   470 end