author  wenzelm 
Wed, 17 Jun 2015 11:03:05 +0200  
changeset 60500  903bb1495239 
parent 58881  b9556a055632 
child 60679  ade12ef2773c 
permissions  rwrr 
41959  1 
(* Title: HOL/Library/Inner_Product.thy 
2 
Author: Brian Huffman 

29993  3 
*) 
4 

60500  5 
section \<open>Inner Product Spaces and the Gradient Derivative\<close> 
29993  6 

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  9 
begin 
10 

60500  11 
subsection \<open>Real inner product spaces\<close> 
29993  12 

60500  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  16 
\<close> 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

17 

60500  18 
setup \<open>Sign.add_const_constraint 
19 
(@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"})\<close> 

31446  20 

60500  21 
setup \<open>Sign.add_const_constraint 
22 
(@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close> 

31446  23 

60500  24 
setup \<open>Sign.add_const_constraint 
25 
(@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close> 

31446  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  28 
fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real" 
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  32 
and inner_ge_zero [simp]: "0 \<le> inner x x" 
33 
and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0" 

34 
and norm_eq_sqrt_inner: "norm x = sqrt (inner x x)" 

35 
begin 

36 

37 
lemma inner_zero_left [simp]: "inner 0 x = 0" 

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  39 

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  42 

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  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  49 
text \<open>Transfer distributivity rules to right argument.\<close> 
29993  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  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  55 
using inner_scaleR_left [of r y x] by (simp only: inner_commute) 
56 

57 
lemma inner_zero_right [simp]: "inner x 0 = 0" 

58 
using inner_zero_left [of x] by (simp only: inner_commute) 

59 

60 
lemma inner_minus_right [simp]: "inner x ( y) =  inner x y" 

61 
using inner_minus_left [of y x] by (simp only: inner_commute) 

62 

63 
lemma inner_diff_right: "inner x (y  z) = inner x y  inner x z" 

64 
using inner_diff_left [of y z x] by (simp only: inner_commute) 

65 

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  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  76 
lemmas inner_distrib = inner_left_distrib inner_right_distrib 
77 

78 
lemma inner_gt_zero_iff [simp]: "0 < inner x x \<longleftrightarrow> x \<noteq> 0" 

79 
by (simp add: order_less_le) 

80 

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  82 
by (simp add: norm_eq_sqrt_inner) 
83 

30046  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  86 
proof (cases) 
87 
assume "y = 0" 

88 
thus ?thesis by simp 

89 
next 

90 
assume y: "y \<noteq> 0" 

91 
let ?r = "inner x y / inner y y" 

92 
have "0 \<le> inner (x  scaleR ?r y) (x  scaleR ?r y)" 

93 
by (rule inner_ge_zero) 

94 
also have "\<dots> = inner x x  inner y x * ?r" 

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  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  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  102 
by (simp add: pos_divide_le_eq y) 
103 
qed 

104 

30046  105 
lemma Cauchy_Schwarz_ineq2: 
29993  106 
"\<bar>inner x y\<bar> \<le> norm x * norm y" 
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  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  111 
by (simp add: power_mult_distrib power2_norm_eq_inner) 
112 
show "0 \<le> norm x * norm y" 

113 
unfolding norm_eq_sqrt_inner 

114 
by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero) 

115 
qed 

116 

53938  117 
lemma norm_cauchy_schwarz: "inner x y \<le> norm x * norm y" 
118 
using Cauchy_Schwarz_ineq2 [of x y] by auto 

119 

29993  120 
subclass real_normed_vector 
121 
proof 

122 
fix a :: real and x y :: 'a 

123 
show "norm x = 0 \<longleftrightarrow> x = 0" 

124 
unfolding norm_eq_sqrt_inner by simp 

125 
show "norm (x + y) \<le> norm x + norm y" 

126 
proof (rule power2_le_imp_le) 

127 
have "inner x y \<le> norm x * norm y" 

53938  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  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  132 
show "0 \<le> norm x + norm y" 
44126  133 
unfolding norm_eq_sqrt_inner by simp 
29993  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  136 
by (simp add: real_sqrt_mult_distrib) 
137 
then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x" 

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  140 
qed 
141 

142 
end 

143 

60500  144 
text \<open> 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

145 
Reenable 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  147 
\<close> 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

148 

60500  149 
setup \<open>Sign.add_const_constraint 
150 
(@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close> 

31446  151 

60500  152 
setup \<open>Sign.add_const_constraint 
153 
(@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close> 

31446  154 

60500  155 
setup \<open>Sign.add_const_constraint 
156 
(@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"})\<close> 

31446  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  160 
proof 
161 
fix x y z :: 'a and r :: real 

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  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  166 
show "inner (scaleR r x) y = scaleR r (inner x y)" 
167 
unfolding real_scaleR_def by (rule inner_scaleR_left) 

168 
show "inner x (scaleR r y) = scaleR r (inner x y)" 

169 
unfolding real_scaleR_def by (rule inner_scaleR_right) 

170 
show "\<exists>K. \<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * K" 

171 
proof 

172 
show "\<forall>x y::'a. norm (inner x y) \<le> norm x * norm y * 1" 

30046  173 
by (simp add: Cauchy_Schwarz_ineq2) 
29993  174 
qed 
175 
qed 

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  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  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  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  201 

60500  202 
subsection \<open>Class instances\<close> 
29993  203 

204 
instantiation real :: real_inner 

205 
begin 

206 

207 
definition inner_real_def [simp]: "inner = op *" 

208 

209 
instance proof 

210 
fix x y z r :: real 

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  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  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  217 
show "0 \<le> inner x x" 
218 
unfolding inner_real_def by simp 

219 
show "inner x x = 0 \<longleftrightarrow> x = 0" 

220 
unfolding inner_real_def by simp 

221 
show "norm x = sqrt (inner x x)" 

222 
unfolding inner_real_def by simp 

223 
qed 

224 

225 
end 

226 

227 
instantiation complex :: real_inner 

228 
begin 

229 

230 
definition inner_complex_def: 

231 
"inner x y = Re x * Re y + Im x * Im y" 

232 

233 
instance proof 

234 
fix x y z :: complex and r :: real 

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  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  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  241 
show "0 \<le> inner x x" 
44126  242 
unfolding inner_complex_def by simp 
29993  243 
show "inner x x = 0 \<longleftrightarrow> x = 0" 
244 
unfolding inner_complex_def 

245 
by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff) 

246 
show "norm x = sqrt (inner x x)" 

247 
unfolding inner_complex_def complex_norm_def 

248 
by (simp add: power2_eq_square) 

249 
qed 

250 

251 
end 

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  265 

60500  266 
subsection \<open>Gradient derivative\<close> 
29993  267 

268 
definition 

269 
gderiv :: 

270 
"['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool" 

271 
("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) 

272 
where 

273 
"GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)" 

274 

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  277 

278 
lemma GDERIV_DERIV_compose: 

279 
"\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk> 

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  284 
done 
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  287 
by simp 
288 

289 
lemma GDERIV_subst: "\<lbrakk>GDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> GDERIV f x :> d" 

290 
by simp 

291 

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  294 

295 
lemma GDERIV_add: 

296 
"\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk> 

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  299 

300 
lemma GDERIV_minus: 

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  303 

304 
lemma GDERIV_diff: 

305 
"\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk> 

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  308 

309 
lemma GDERIV_scaleR: 

310 
"\<lbrakk>DERIV f x :> df; GDERIV g x :> dg\<rbrakk> 

311 
\<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x 

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  317 
done 
318 

319 
lemma GDERIV_mult: 

320 
"\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk> 

321 
\<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df" 

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  326 
done 
327 

328 
lemma GDERIV_inverse: 

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  331 
apply (erule GDERIV_DERIV_compose) 
332 
apply (erule DERIV_inverse [folded numeral_2_eq_2]) 

333 
done 

334 

335 
lemma GDERIV_norm: 

336 
assumes "x \<noteq> 0" shows "GDERIV (\<lambda>x. norm x) x :> sgn x" 

337 
proof  

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  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  342 
have "0 < inner x x" using \<open>x \<noteq> 0\<close> by simp 
29993  343 
then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)" 
344 
by (rule DERIV_real_sqrt) 

345 
have 4: "(inverse (sqrt (inner x x)) / 2) *\<^sub>R 2 *\<^sub>R x = sgn x" 

346 
by (simp add: sgn_div_norm norm_eq_sqrt_inner) 

347 
show ?thesis 

348 
unfolding norm_eq_sqrt_inner 

349 
apply (rule GDERIV_subst [OF _ 4]) 

350 
apply (rule GDERIV_DERIV_compose [where g=sqrt and df="scaleR 2 x"]) 

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  353 
apply (rule 1) 
354 
apply (rule 3) 

355 
done 

356 
qed 

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  359 

360 
end 