author  huffman 
Fri, 12 Jun 2009 16:23:07 0700  
changeset 31590  776d6a4c1327 
parent 31492  5400beeddb55 
child 39198  f967a16dfcdd 
permissions  rwrr 
29993  1 
(* Title: Inner_Product.thy 
2 
Author: Brian Huffman 

3 
*) 

4 

5 
header {* Inner Product Spaces and the Gradient Derivative *} 

6 

7 
theory Inner_Product 

30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
30067
diff
changeset

8 
imports Complex_Main FrechetDeriv 
29993  9 
begin 
10 

11 
subsection {* Real inner product spaces *} 

12 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

13 
text {* 
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}. 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

16 
*} 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

17 

5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

18 
setup {* Sign.add_const_constraint 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

19 
(@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"}) *} 
31446  20 

21 
setup {* Sign.add_const_constraint 

22 
(@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *} 

23 

24 
setup {* Sign.add_const_constraint 

25 
(@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *} 

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" 

31590
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

44 
by (simp add: diff_minus inner_add_left) 
29993  45 

46 
text {* Transfer distributivity rules to right argument. *} 

47 

31590
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

48 
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

49 
using inner_add_left [of y z x] by (simp only: inner_commute) 
29993  50 

31590
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

51 
lemma inner_scaleR_right [simp]: "inner x (scaleR r y) = r * (inner x y)" 
29993  52 
using inner_scaleR_left [of r y x] by (simp only: inner_commute) 
53 

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

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

56 

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

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

59 

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

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

62 

31590
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

63 
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

64 
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

65 
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

66 

776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

67 
text {* Legacy theorem names *} 
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

68 
lemmas inner_left_distrib = inner_add_left 
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

69 
lemmas inner_right_distrib = inner_add_right 
29993  70 
lemmas inner_distrib = inner_left_distrib inner_right_distrib 
71 

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

73 
by (simp add: order_less_le) 

74 

75 
lemma power2_norm_eq_inner: "(norm x)\<twosuperior> = inner x x" 

76 
by (simp add: norm_eq_sqrt_inner) 

77 

30046  78 
lemma Cauchy_Schwarz_ineq: 
29993  79 
"(inner x y)\<twosuperior> \<le> inner x x * inner y y" 
80 
proof (cases) 

81 
assume "y = 0" 

82 
thus ?thesis by simp 

83 
next 

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

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

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

87 
by (rule inner_ge_zero) 

88 
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

89 
by (simp add: inner_diff) 
29993  90 
also have "\<dots> = inner x x  (inner x y)\<twosuperior> / inner y y" 
91 
by (simp add: power2_eq_square inner_commute) 

92 
finally have "0 \<le> inner x x  (inner x y)\<twosuperior> / inner y y" . 

93 
hence "(inner x y)\<twosuperior> / inner y y \<le> inner x x" 

94 
by (simp add: le_diff_eq) 

95 
thus "(inner x y)\<twosuperior> \<le> inner x x * inner y y" 

96 
by (simp add: pos_divide_le_eq y) 

97 
qed 

98 

30046  99 
lemma Cauchy_Schwarz_ineq2: 
29993  100 
"\<bar>inner x y\<bar> \<le> norm x * norm y" 
101 
proof (rule power2_le_imp_le) 

102 
have "(inner x y)\<twosuperior> \<le> inner x x * inner y y" 

30046  103 
using Cauchy_Schwarz_ineq . 
29993  104 
thus "\<bar>inner x y\<bar>\<twosuperior> \<le> (norm x * norm y)\<twosuperior>" 
105 
by (simp add: power_mult_distrib power2_norm_eq_inner) 

106 
show "0 \<le> norm x * norm y" 

107 
unfolding norm_eq_sqrt_inner 

108 
by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero) 

109 
qed 

110 

111 
subclass real_normed_vector 

112 
proof 

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

114 
show "0 \<le> norm x" 

115 
unfolding norm_eq_sqrt_inner by simp 

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

117 
unfolding norm_eq_sqrt_inner by simp 

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

119 
proof (rule power2_le_imp_le) 

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

30046  121 
by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2]) 
29993  122 
thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>" 
123 
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

124 
by (simp add: inner_add inner_commute) 
29993  125 
show "0 \<le> norm x + norm y" 
126 
unfolding norm_eq_sqrt_inner 

127 
by (simp add: add_nonneg_nonneg) 

128 
qed 

129 
have "sqrt (a\<twosuperior> * inner x x) = \<bar>a\<bar> * sqrt (inner x x)" 

130 
by (simp add: real_sqrt_mult_distrib) 

131 
then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x" 

132 
unfolding norm_eq_sqrt_inner 

31590
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

133 
by (simp add: power2_eq_square mult_assoc) 
29993  134 
qed 
135 

136 
end 

137 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

138 
text {* 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

139 
Reenable constraints for @{term "open"}, 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

140 
@{term dist}, and @{term norm}. 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

141 
*} 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

142 

5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

143 
setup {* Sign.add_const_constraint 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31446
diff
changeset

144 
(@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *} 
31446  145 

146 
setup {* Sign.add_const_constraint 

147 
(@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *} 

148 

149 
setup {* Sign.add_const_constraint 

150 
(@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *} 

151 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset

152 
interpretation inner: 
29993  153 
bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real" 
154 
proof 

155 
fix x y z :: 'a and r :: real 

156 
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

157 
by (rule inner_add_left) 
29993  158 
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

159 
by (rule inner_add_right) 
29993  160 
show "inner (scaleR r x) y = scaleR r (inner x y)" 
161 
unfolding real_scaleR_def by (rule inner_scaleR_left) 

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

163 
unfolding real_scaleR_def by (rule inner_scaleR_right) 

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

165 
proof 

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

30046  167 
by (simp add: Cauchy_Schwarz_ineq2) 
29993  168 
qed 
169 
qed 

170 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset

171 
interpretation inner_left: 
29993  172 
bounded_linear "\<lambda>x::'a::real_inner. inner x y" 
173 
by (rule inner.bounded_linear_left) 

174 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30663
diff
changeset

175 
interpretation inner_right: 
29993  176 
bounded_linear "\<lambda>y::'a::real_inner. inner x y" 
177 
by (rule inner.bounded_linear_right) 

178 

179 

180 
subsection {* Class instances *} 

181 

182 
instantiation real :: real_inner 

183 
begin 

184 

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

186 

187 
instance proof 

188 
fix x y z r :: real 

189 
show "inner x y = inner y x" 

190 
unfolding inner_real_def by (rule mult_commute) 

191 
show "inner (x + y) z = inner x z + inner y z" 

192 
unfolding inner_real_def by (rule left_distrib) 

193 
show "inner (scaleR r x) y = r * inner x y" 

194 
unfolding inner_real_def real_scaleR_def by (rule mult_assoc) 

195 
show "0 \<le> inner x x" 

196 
unfolding inner_real_def by simp 

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

198 
unfolding inner_real_def by simp 

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

200 
unfolding inner_real_def by simp 

201 
qed 

202 

203 
end 

204 

205 
instantiation complex :: real_inner 

206 
begin 

207 

208 
definition inner_complex_def: 

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

210 

211 
instance proof 

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

213 
show "inner x y = inner y x" 

214 
unfolding inner_complex_def by (simp add: mult_commute) 

215 
show "inner (x + y) z = inner x z + inner y z" 

216 
unfolding inner_complex_def by (simp add: left_distrib) 

217 
show "inner (scaleR r x) y = r * inner x y" 

218 
unfolding inner_complex_def by (simp add: right_distrib) 

219 
show "0 \<le> inner x x" 

220 
unfolding inner_complex_def by (simp add: add_nonneg_nonneg) 

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

222 
unfolding inner_complex_def 

223 
by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff) 

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

225 
unfolding inner_complex_def complex_norm_def 

226 
by (simp add: power2_eq_square) 

227 
qed 

228 

229 
end 

230 

231 

232 
subsection {* Gradient derivative *} 

233 

234 
definition 

235 
gderiv :: 

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

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

238 
where 

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

240 

241 
lemma deriv_fderiv: "DERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. h * D)" 

242 
by (simp only: deriv_def field_fderiv_def) 

243 

244 
lemma gderiv_deriv [simp]: "GDERIV f x :> D \<longleftrightarrow> DERIV f x :> D" 

245 
by (simp only: gderiv_def deriv_fderiv inner_real_def) 

246 

247 
lemma GDERIV_DERIV_compose: 

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

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

250 
unfolding gderiv_def deriv_fderiv 

251 
apply (drule (1) FDERIV_compose) 

31590
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

252 
apply (simp add: mult_ac) 
29993  253 
done 
254 

255 
lemma FDERIV_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d" 

256 
by simp 

257 

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

259 
by simp 

260 

261 
lemma GDERIV_const: "GDERIV (\<lambda>x. k) x :> 0" 

262 
unfolding gderiv_def inner_right.zero by (rule FDERIV_const) 

263 

264 
lemma GDERIV_add: 

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

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

267 
unfolding gderiv_def inner_right.add by (rule FDERIV_add) 

268 

269 
lemma GDERIV_minus: 

270 
"GDERIV f x :> df \<Longrightarrow> GDERIV (\<lambda>x.  f x) x :>  df" 

271 
unfolding gderiv_def inner_right.minus by (rule FDERIV_minus) 

272 

273 
lemma GDERIV_diff: 

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

275 
\<Longrightarrow> GDERIV (\<lambda>x. f x  g x) x :> df  dg" 

276 
unfolding gderiv_def inner_right.diff by (rule FDERIV_diff) 

277 

278 
lemma GDERIV_scaleR: 

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

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

281 
:> (scaleR (f x) dg + scaleR df (g x))" 

282 
unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR 

283 
apply (rule FDERIV_subst) 

284 
apply (erule (1) scaleR.FDERIV) 

285 
apply (simp add: mult_ac) 

286 
done 

287 

288 
lemma GDERIV_mult: 

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

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

291 
unfolding gderiv_def 

292 
apply (rule FDERIV_subst) 

293 
apply (erule (1) FDERIV_mult) 

31590
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

294 
apply (simp add: inner_add mult_ac) 
29993  295 
done 
296 

297 
lemma GDERIV_inverse: 

298 
"\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk> 

299 
\<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :>  (inverse (f x))\<twosuperior> *\<^sub>R df" 

300 
apply (erule GDERIV_DERIV_compose) 

301 
apply (erule DERIV_inverse [folded numeral_2_eq_2]) 

302 
done 

303 

304 
lemma GDERIV_norm: 

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

306 
proof  

307 
have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)" 

308 
by (intro inner.FDERIV FDERIV_ident) 

309 
have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))" 

31590
776d6a4c1327
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
huffman
parents:
31492
diff
changeset

310 
by (simp add: expand_fun_eq inner_commute) 
29993  311 
have "0 < inner x x" using `x \<noteq> 0` by simp 
312 
then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)" 

313 
by (rule DERIV_real_sqrt) 

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

315 
by (simp add: sgn_div_norm norm_eq_sqrt_inner) 

316 
show ?thesis 

317 
unfolding norm_eq_sqrt_inner 

318 
apply (rule GDERIV_subst [OF _ 4]) 

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

320 
apply (subst gderiv_def) 

321 
apply (rule FDERIV_subst [OF _ 2]) 

322 
apply (rule 1) 

323 
apply (rule 3) 

324 
done 

325 
qed 

326 

327 
lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def] 

328 

329 
end 