src/HOL/Library/Inner_Product.thy
author wenzelm
Wed, 17 Jun 2015 11:03:05 +0200
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60679 ade12ef2773c
permissions -rw-r--r--
isabelle update_cartouches;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 39302
diff changeset
     1
(*  Title:      HOL/Library/Inner_Product.thy
b460124855b8 tuned headers;
wenzelm
parents: 39302
diff changeset
     2
    Author:     Brian Huffman
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
     3
*)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     5
section \<open>Inner Product Spaces and the Gradient Derivative\<close>
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
     6
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
     7
theory Inner_Product
51642
400ec5ae7f8f move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents: 51002
diff changeset
     8
imports "~~/src/HOL/Complex_Main"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
     9
begin
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    10
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    11
subsection \<open>Real inner product spaces\<close>
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    12
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    13
text \<open>
31492
5400beeddb55 replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents: 31446
diff changeset
    14
  Temporarily relax type constraints for @{term "open"},
5400beeddb55 replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents: 31446
diff changeset
    15
  @{term dist}, and @{term norm}.
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    16
\<close>
31492
5400beeddb55 replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents: 31446
diff changeset
    17
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    18
setup \<open>Sign.add_const_constraint
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    19
  (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"})\<close>
31446
2d91b2416de8 add extra type constraints for dist, norm
huffman
parents: 31417
diff changeset
    20
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    21
setup \<open>Sign.add_const_constraint
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    22
  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
31446
2d91b2416de8 add extra type constraints for dist, norm
huffman
parents: 31417
diff changeset
    23
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    24
setup \<open>Sign.add_const_constraint
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    25
  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
31446
2d91b2416de8 add extra type constraints for dist, norm
huffman
parents: 31417
diff changeset
    26
31492
5400beeddb55 replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents: 31446
diff changeset
    27
class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    28
  fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    29
  assumes inner_commute: "inner x y = inner y x"
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    30
  and inner_add_left: "inner (x + y) z = inner x z + inner y z"
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    31
  and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    32
  and inner_ge_zero [simp]: "0 \<le> inner x x"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    33
  and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    34
  and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    35
begin
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    36
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    37
lemma inner_zero_left [simp]: "inner 0 x = 0"
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    38
  using inner_add_left [of 0 0 x] by simp
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    39
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    40
lemma inner_minus_left [simp]: "inner (- x) y = - inner x y"
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    41
  using inner_add_left [of x "- x" y] by simp
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    42
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    43
lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53938
diff changeset
    44
  using inner_add_left [of x "- y" z] by simp
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    45
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
    46
lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
    47
  by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
    48
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    49
text \<open>Transfer distributivity rules to right argument.\<close>
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    50
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    51
lemma inner_add_right: "inner x (y + z) = inner x y + inner x z"
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    52
  using inner_add_left [of y z x] by (simp only: inner_commute)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    53
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    54
lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    55
  using inner_scaleR_left [of r y x] by (simp only: inner_commute)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    56
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    57
lemma inner_zero_right [simp]: "inner x 0 = 0"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    58
  using inner_zero_left [of x] by (simp only: inner_commute)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    59
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    60
lemma inner_minus_right [simp]: "inner x (- y) = - inner x y"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    61
  using inner_minus_left [of y x] by (simp only: inner_commute)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    62
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    63
lemma inner_diff_right: "inner x (y - z) = inner x y - inner x z"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    64
  using inner_diff_left [of y z x] by (simp only: inner_commute)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    65
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
    66
lemma inner_setsum_right: "inner x (\<Sum>y\<in>A. f y) = (\<Sum>y\<in>A. inner x (f y))"
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
    67
  using inner_setsum_left [of f A x] by (simp only: inner_commute)
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
    68
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    69
lemmas inner_add [algebra_simps] = inner_add_left inner_add_right
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    70
lemmas inner_diff [algebra_simps]  = inner_diff_left inner_diff_right
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    71
lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    72
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    73
text \<open>Legacy theorem names\<close>
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    74
lemmas inner_left_distrib = inner_add_left
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    75
lemmas inner_right_distrib = inner_add_right
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    76
lemmas inner_distrib = inner_left_distrib inner_right_distrib
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    77
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    78
lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    79
  by (simp add: order_less_le)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    80
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
    81
lemma power2_norm_eq_inner: "(norm x)\<^sup>2 = inner x x"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    82
  by (simp add: norm_eq_sqrt_inner)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    83
30046
49f603f92c47 fix spelling
huffman
parents: 29993
diff changeset
    84
lemma Cauchy_Schwarz_ineq:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
    85
  "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    86
proof (cases)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    87
  assume "y = 0"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    88
  thus ?thesis by simp
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    89
next
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    90
  assume y: "y \<noteq> 0"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    91
  let ?r = "inner x y / inner y y"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    92
  have "0 \<le> inner (x - scaleR ?r y) (x - scaleR ?r y)"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    93
    by (rule inner_ge_zero)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    94
  also have "\<dots> = inner x x - inner y x * ?r"
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
    95
    by (simp add: inner_diff)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
    96
  also have "\<dots> = inner x x - (inner x y)\<^sup>2 / inner y y"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
    97
    by (simp add: power2_eq_square inner_commute)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
    98
  finally have "0 \<le> inner x x - (inner x y)\<^sup>2 / inner y y" .
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
    99
  hence "(inner x y)\<^sup>2 / inner y y \<le> inner x x"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   100
    by (simp add: le_diff_eq)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
   101
  thus "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   102
    by (simp add: pos_divide_le_eq y)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   103
qed
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   104
30046
49f603f92c47 fix spelling
huffman
parents: 29993
diff changeset
   105
lemma Cauchy_Schwarz_ineq2:
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   106
  "\<bar>inner x y\<bar> \<le> norm x * norm y"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   107
proof (rule power2_le_imp_le)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
   108
  have "(inner x y)\<^sup>2 \<le> inner x x * inner y y"
30046
49f603f92c47 fix spelling
huffman
parents: 29993
diff changeset
   109
    using Cauchy_Schwarz_ineq .
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
   110
  thus "\<bar>inner x y\<bar>\<^sup>2 \<le> (norm x * norm y)\<^sup>2"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   111
    by (simp add: power_mult_distrib power2_norm_eq_inner)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   112
  show "0 \<le> norm x * norm y"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   113
    unfolding norm_eq_sqrt_inner
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   114
    by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   115
qed
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   116
53938
eb93cca4589a moved lemma
huffman
parents: 53015
diff changeset
   117
lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y"
eb93cca4589a moved lemma
huffman
parents: 53015
diff changeset
   118
  using Cauchy_Schwarz_ineq2 [of x y] by auto
eb93cca4589a moved lemma
huffman
parents: 53015
diff changeset
   119
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   120
subclass real_normed_vector
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   121
proof
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   122
  fix a :: real and x y :: 'a
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   123
  show "norm x = 0 \<longleftrightarrow> x = 0"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   124
    unfolding norm_eq_sqrt_inner by simp
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   125
  show "norm (x + y) \<le> norm x + norm y"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   126
    proof (rule power2_le_imp_le)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   127
      have "inner x y \<le> norm x * norm y"
53938
eb93cca4589a moved lemma
huffman
parents: 53015
diff changeset
   128
        by (rule norm_cauchy_schwarz)
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
   129
      thus "(norm (x + y))\<^sup>2 \<le> (norm x + norm y)\<^sup>2"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   130
        unfolding power2_sum power2_norm_eq_inner
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
   131
        by (simp add: inner_add inner_commute)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   132
      show "0 \<le> norm x + norm y"
44126
ce44e70d0c47 avoid duplicate rewrite warnings
huffman
parents: 41959
diff changeset
   133
        unfolding norm_eq_sqrt_inner by simp
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   134
    qed
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
   135
  have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   136
    by (simp add: real_sqrt_mult_distrib)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   137
  then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   138
    unfolding norm_eq_sqrt_inner
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56381
diff changeset
   139
    by (simp add: power2_eq_square mult.assoc)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   140
qed
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   141
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   142
end
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   143
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   144
text \<open>
31492
5400beeddb55 replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents: 31446
diff changeset
   145
  Re-enable constraints for @{term "open"},
5400beeddb55 replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents: 31446
diff changeset
   146
  @{term dist}, and @{term norm}.
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   147
\<close>
31492
5400beeddb55 replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents: 31446
diff changeset
   148
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   149
setup \<open>Sign.add_const_constraint
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   150
  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
31446
2d91b2416de8 add extra type constraints for dist, norm
huffman
parents: 31417
diff changeset
   151
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   152
setup \<open>Sign.add_const_constraint
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   153
  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
31446
2d91b2416de8 add extra type constraints for dist, norm
huffman
parents: 31417
diff changeset
   154
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   155
setup \<open>Sign.add_const_constraint
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   156
  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close>
31446
2d91b2416de8 add extra type constraints for dist, norm
huffman
parents: 31417
diff changeset
   157
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   158
lemma bounded_bilinear_inner:
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   159
  "bounded_bilinear (inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real)"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   160
proof
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   161
  fix x y z :: 'a and r :: real
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   162
  show "inner (x + y) z = inner x z + inner y z"
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
   163
    by (rule inner_add_left)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   164
  show "inner x (y + z) = inner x y + inner x z"
31590
776d6a4c1327 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents: 31492
diff changeset
   165
    by (rule inner_add_right)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   166
  show "inner (scaleR r x) y = scaleR r (inner x y)"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   167
    unfolding real_scaleR_def by (rule inner_scaleR_left)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   168
  show "inner x (scaleR r y) = scaleR r (inner x y)"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   169
    unfolding real_scaleR_def by (rule inner_scaleR_right)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   170
  show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   171
  proof
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   172
    show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1"
30046
49f603f92c47 fix spelling
huffman
parents: 29993
diff changeset
   173
      by (simp add: Cauchy_Schwarz_ineq2)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   174
  qed
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   175
qed
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   176
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   177
lemmas tendsto_inner [tendsto_intros] =
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   178
  bounded_bilinear.tendsto [OF bounded_bilinear_inner]
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   179
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   180
lemmas isCont_inner [simp] =
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   181
  bounded_bilinear.isCont [OF bounded_bilinear_inner]
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   182
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56181
diff changeset
   183
lemmas has_derivative_inner [derivative_intros] =
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   184
  bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   185
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   186
lemmas bounded_linear_inner_left =
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   187
  bounded_bilinear.bounded_linear_left [OF bounded_bilinear_inner]
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   188
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   189
lemmas bounded_linear_inner_right =
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44233
diff changeset
   190
  bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
44233
aa74ce315bae add simp rules for isCont
huffman
parents: 44126
diff changeset
   191
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56181
diff changeset
   192
lemmas has_derivative_inner_right [derivative_intros] =
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   193
  bounded_linear.has_derivative [OF bounded_linear_inner_right]
51642
400ec5ae7f8f move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents: 51002
diff changeset
   194
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56181
diff changeset
   195
lemmas has_derivative_inner_left [derivative_intros] =
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   196
  bounded_linear.has_derivative [OF bounded_linear_inner_left]
51642
400ec5ae7f8f move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents: 51002
diff changeset
   197
400ec5ae7f8f move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
hoelzl
parents: 51002
diff changeset
   198
lemma differentiable_inner [simp]:
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   199
  "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"
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   200
  unfolding differentiable_def by (blast intro: has_derivative_inner)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   201
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   202
subsection \<open>Class instances\<close>
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   203
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   204
instantiation real :: real_inner
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   205
begin
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   206
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   207
definition inner_real_def [simp]: "inner = op *"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   208
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   209
instance proof
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   210
  fix x y z r :: real
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   211
  show "inner x y = inner y x"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56381
diff changeset
   212
    unfolding inner_real_def by (rule mult.commute)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   213
  show "inner (x + y) z = inner x z + inner y z"
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44902
diff changeset
   214
    unfolding inner_real_def by (rule distrib_right)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   215
  show "inner (scaleR r x) y = r * inner x y"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56381
diff changeset
   216
    unfolding inner_real_def real_scaleR_def by (rule mult.assoc)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   217
  show "0 \<le> inner x x"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   218
    unfolding inner_real_def by simp
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   219
  show "inner x x = 0 \<longleftrightarrow> x = 0"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   220
    unfolding inner_real_def by simp
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   221
  show "norm x = sqrt (inner x x)"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   222
    unfolding inner_real_def by simp
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   223
qed
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   224
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   225
end
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   226
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   227
instantiation complex :: real_inner
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   228
begin
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   229
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   230
definition inner_complex_def:
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   231
  "inner x y = Re x * Re y + Im x * Im y"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   232
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   233
instance proof
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   234
  fix x y z :: complex and r :: real
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   235
  show "inner x y = inner y x"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56381
diff changeset
   236
    unfolding inner_complex_def by (simp add: mult.commute)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   237
  show "inner (x + y) z = inner x z + inner y z"
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44902
diff changeset
   238
    unfolding inner_complex_def by (simp add: distrib_right)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   239
  show "inner (scaleR r x) y = r * inner x y"
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 44902
diff changeset
   240
    unfolding inner_complex_def by (simp add: distrib_left)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   241
  show "0 \<le> inner x x"
44126
ce44e70d0c47 avoid duplicate rewrite warnings
huffman
parents: 41959
diff changeset
   242
    unfolding inner_complex_def by simp
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   243
  show "inner x x = 0 \<longleftrightarrow> x = 0"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   244
    unfolding inner_complex_def
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   245
    by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   246
  show "norm x = sqrt (inner x x)"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   247
    unfolding inner_complex_def complex_norm_def
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   248
    by (simp add: power2_eq_square)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   249
qed
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   250
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   251
end
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   252
44902
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   253
lemma complex_inner_1 [simp]: "inner 1 x = Re x"
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   254
  unfolding inner_complex_def by simp
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   255
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   256
lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   257
  unfolding inner_complex_def by simp
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   258
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   259
lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   260
  unfolding inner_complex_def by simp
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   261
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   262
lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   263
  unfolding inner_complex_def by simp
9ba11d41cd1f move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
huffman
parents: 44282
diff changeset
   264
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   265
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   266
subsection \<open>Gradient derivative\<close>
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   267
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   268
definition
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   269
  gderiv ::
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   270
    "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   271
          ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   272
where
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   273
  "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   274
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   275
lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   276
  by (simp only: gderiv_def has_field_derivative_def inner_real_def mult_commute_abs)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   277
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   278
lemma GDERIV_DERIV_compose:
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   279
    "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk>
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   280
     \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   281
  unfolding gderiv_def has_field_derivative_def
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   282
  apply (drule (1) has_derivative_compose)
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   283
  apply (simp add: ac_simps)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   284
  done
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   285
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   286
lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   287
  by simp
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   288
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   289
lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   290
  by simp
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   291
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   292
lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   293
  unfolding gderiv_def inner_zero_right by (rule has_derivative_const)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   294
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   295
lemma GDERIV_add:
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   296
    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   297
     \<Longrightarrow> GDERIV (\<lambda>x. f x + g x) x :> df + dg"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   298
  unfolding gderiv_def inner_add_right by (rule has_derivative_add)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   299
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   300
lemma GDERIV_minus:
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   301
    "GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x. - f x) x :> - df"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   302
  unfolding gderiv_def inner_minus_right by (rule has_derivative_minus)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   303
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   304
lemma GDERIV_diff:
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   305
    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   306
     \<Longrightarrow> GDERIV (\<lambda>x. f x - g x) x :> df - dg"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   307
  unfolding gderiv_def inner_diff_right by (rule has_derivative_diff)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   308
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   309
lemma GDERIV_scaleR:
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   310
    "\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk>
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   311
     \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   312
      :> (scaleR (f x) dg + scaleR df (g x))"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   313
  unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   314
  apply (rule has_derivative_subst)
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   315
  apply (erule (1) has_derivative_scaleR)
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   316
  apply (simp add: ac_simps)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   317
  done
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   318
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   319
lemma GDERIV_mult:
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   320
    "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk>
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   321
     \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   322
  unfolding gderiv_def
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   323
  apply (rule has_derivative_subst)
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   324
  apply (erule (1) has_derivative_mult)
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   325
  apply (simp add: inner_add ac_simps)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   326
  done
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   327
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   328
lemma GDERIV_inverse:
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   329
    "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk>
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 51642
diff changeset
   330
     \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df"
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   331
  apply (erule GDERIV_DERIV_compose)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   332
  apply (erule DERIV_inverse [folded numeral_2_eq_2])
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   333
  done
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   334
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   335
lemma GDERIV_norm:
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   336
  assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   337
proof -
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   338
  have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   339
    by (intro has_derivative_inner has_derivative_ident)
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   340
  have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   341
    by (simp add: fun_eq_iff inner_commute)
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   342
  have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   343
  then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   344
    by (rule DERIV_real_sqrt)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   345
  have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x"
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   346
    by (simp add: sgn_div_norm norm_eq_sqrt_inner)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   347
  show ?thesis
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   348
    unfolding norm_eq_sqrt_inner
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   349
    apply (rule GDERIV_subst [OF _ 4])
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   350
    apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"])
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   351
    apply (subst gderiv_def)
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   352
    apply (rule has_derivative_subst [OF _ 2])
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   353
    apply (rule 1)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   354
    apply (rule 3)
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   355
    done
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   356
qed
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   357
56181
2aa0b19e74f3 unify syntax for has_derivative and differentiable
hoelzl
parents: 54230
diff changeset
   358
lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
29993
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   359
84b2c432b94a new theory of real inner product spaces
huffman
parents:
diff changeset
   360
end