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