author  huffman 
Sun, 07 Jun 2009 17:59:54 0700  
changeset 31492  5400beeddb55 
parent 31446  2d91b2416de8 
child 31590  776d6a4c1327 
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" 

30 
and inner_left_distrib: "inner (x + y) z = inner x z + inner y z" 

31 
and inner_scaleR_left: "inner (scaleR r x) y = r * (inner x y)" 

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" 

30067  38 
using inner_left_distrib [of 0 0 x] by simp 
29993  39 

40 
lemma inner_minus_left [simp]: "inner ( x) y =  inner x y" 

30067  41 
using inner_left_distrib [of x " x" y] by simp 
29993  42 

43 
lemma inner_diff_left: "inner (x  y) z = inner x z  inner y z" 

44 
by (simp add: diff_minus inner_left_distrib) 

45 

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

47 

48 
lemma inner_right_distrib: "inner x (y + z) = inner x y + inner x z" 

49 
using inner_left_distrib [of y z x] by (simp only: inner_commute) 

50 

51 
lemma inner_scaleR_right: "inner x (scaleR r y) = r * (inner x y)" 

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 

63 
lemmas inner_distrib = inner_left_distrib inner_right_distrib 

64 
lemmas inner_diff = inner_diff_left inner_diff_right 

65 
lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right 

66 

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

68 
by (simp add: order_less_le) 

69 

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

71 
by (simp add: norm_eq_sqrt_inner) 

72 

30046  73 
lemma Cauchy_Schwarz_ineq: 
29993  74 
"(inner x y)\<twosuperior> \<le> inner x x * inner y y" 
75 
proof (cases) 

76 
assume "y = 0" 

77 
thus ?thesis by simp 

78 
next 

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

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

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

82 
by (rule inner_ge_zero) 

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

84 
by (simp add: inner_diff inner_scaleR) 

85 
also have "\<dots> = inner x x  (inner x y)\<twosuperior> / inner y y" 

86 
by (simp add: power2_eq_square inner_commute) 

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

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

89 
by (simp add: le_diff_eq) 

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

91 
by (simp add: pos_divide_le_eq y) 

92 
qed 

93 

30046  94 
lemma Cauchy_Schwarz_ineq2: 
29993  95 
"\<bar>inner x y\<bar> \<le> norm x * norm y" 
96 
proof (rule power2_le_imp_le) 

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

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

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

102 
unfolding norm_eq_sqrt_inner 

103 
by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero) 

104 
qed 

105 

106 
subclass real_normed_vector 

107 
proof 

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

109 
show "0 \<le> norm x" 

110 
unfolding norm_eq_sqrt_inner by simp 

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

112 
unfolding norm_eq_sqrt_inner by simp 

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

114 
proof (rule power2_le_imp_le) 

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

30046  116 
by (rule order_trans [OF abs_ge_self Cauchy_Schwarz_ineq2]) 
29993  117 
thus "(norm (x + y))\<twosuperior> \<le> (norm x + norm y)\<twosuperior>" 
118 
unfolding power2_sum power2_norm_eq_inner 

119 
by (simp add: inner_distrib inner_commute) 

120 
show "0 \<le> norm x + norm y" 

121 
unfolding norm_eq_sqrt_inner 

122 
by (simp add: add_nonneg_nonneg) 

123 
qed 

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

125 
by (simp add: real_sqrt_mult_distrib) 

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

127 
unfolding norm_eq_sqrt_inner 

128 
by (simp add: inner_scaleR power2_eq_square mult_assoc) 

129 
qed 

130 

131 
end 

132 

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

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

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

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

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

137 

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

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

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

141 
setup {* Sign.add_const_constraint 

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

143 

144 
setup {* Sign.add_const_constraint 

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

146 

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

147 
interpretation inner: 
29993  148 
bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real" 
149 
proof 

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

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

152 
by (rule inner_left_distrib) 

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

154 
by (rule inner_right_distrib) 

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

156 
unfolding real_scaleR_def by (rule inner_scaleR_left) 

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

158 
unfolding real_scaleR_def by (rule inner_scaleR_right) 

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

160 
proof 

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

30046  162 
by (simp add: Cauchy_Schwarz_ineq2) 
29993  163 
qed 
164 
qed 

165 

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

166 
interpretation inner_left: 
29993  167 
bounded_linear "\<lambda>x::'a::real_inner. inner x y" 
168 
by (rule inner.bounded_linear_left) 

169 

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

170 
interpretation inner_right: 
29993  171 
bounded_linear "\<lambda>y::'a::real_inner. inner x y" 
172 
by (rule inner.bounded_linear_right) 

173 

174 

175 
subsection {* Class instances *} 

176 

177 
instantiation real :: real_inner 

178 
begin 

179 

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

181 

182 
instance proof 

183 
fix x y z r :: real 

184 
show "inner x y = inner y x" 

185 
unfolding inner_real_def by (rule mult_commute) 

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

187 
unfolding inner_real_def by (rule left_distrib) 

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

189 
unfolding inner_real_def real_scaleR_def by (rule mult_assoc) 

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

191 
unfolding inner_real_def by simp 

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

193 
unfolding inner_real_def by simp 

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

195 
unfolding inner_real_def by simp 

196 
qed 

197 

198 
end 

199 

200 
instantiation complex :: real_inner 

201 
begin 

202 

203 
definition inner_complex_def: 

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

205 

206 
instance proof 

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

208 
show "inner x y = inner y x" 

209 
unfolding inner_complex_def by (simp add: mult_commute) 

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

211 
unfolding inner_complex_def by (simp add: left_distrib) 

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

213 
unfolding inner_complex_def by (simp add: right_distrib) 

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

215 
unfolding inner_complex_def by (simp add: add_nonneg_nonneg) 

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

217 
unfolding inner_complex_def 

218 
by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff) 

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

220 
unfolding inner_complex_def complex_norm_def 

221 
by (simp add: power2_eq_square) 

222 
qed 

223 

224 
end 

225 

226 

227 
subsection {* Gradient derivative *} 

228 

229 
definition 

230 
gderiv :: 

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

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

233 
where 

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

235 

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

237 
by (simp only: deriv_def field_fderiv_def) 

238 

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

240 
by (simp only: gderiv_def deriv_fderiv inner_real_def) 

241 

242 
lemma GDERIV_DERIV_compose: 

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

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

245 
unfolding gderiv_def deriv_fderiv 

246 
apply (drule (1) FDERIV_compose) 

247 
apply (simp add: inner_scaleR_right mult_ac) 

248 
done 

249 

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

251 
by simp 

252 

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

254 
by simp 

255 

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

257 
unfolding gderiv_def inner_right.zero by (rule FDERIV_const) 

258 

259 
lemma GDERIV_add: 

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

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

262 
unfolding gderiv_def inner_right.add by (rule FDERIV_add) 

263 

264 
lemma GDERIV_minus: 

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

266 
unfolding gderiv_def inner_right.minus by (rule FDERIV_minus) 

267 

268 
lemma GDERIV_diff: 

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

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

271 
unfolding gderiv_def inner_right.diff by (rule FDERIV_diff) 

272 

273 
lemma GDERIV_scaleR: 

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

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

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

277 
unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR 

278 
apply (rule FDERIV_subst) 

279 
apply (erule (1) scaleR.FDERIV) 

280 
apply (simp add: mult_ac) 

281 
done 

282 

283 
lemma GDERIV_mult: 

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

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

286 
unfolding gderiv_def 

287 
apply (rule FDERIV_subst) 

288 
apply (erule (1) FDERIV_mult) 

289 
apply (simp add: inner_distrib inner_scaleR mult_ac) 

290 
done 

291 

292 
lemma GDERIV_inverse: 

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

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

295 
apply (erule GDERIV_DERIV_compose) 

296 
apply (erule DERIV_inverse [folded numeral_2_eq_2]) 

297 
done 

298 

299 
lemma GDERIV_norm: 

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

301 
proof  

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

303 
by (intro inner.FDERIV FDERIV_ident) 

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

305 
by (simp add: expand_fun_eq inner_scaleR inner_commute) 

306 
have "0 < inner x x" using `x \<noteq> 0` by simp 

307 
then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)" 

308 
by (rule DERIV_real_sqrt) 

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

310 
by (simp add: sgn_div_norm norm_eq_sqrt_inner) 

311 
show ?thesis 

312 
unfolding norm_eq_sqrt_inner 

313 
apply (rule GDERIV_subst [OF _ 4]) 

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

315 
apply (subst gderiv_def) 

316 
apply (rule FDERIV_subst [OF _ 2]) 

317 
apply (rule 1) 

318 
apply (rule 3) 

319 
done 

320 
qed 

321 

322 
lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def] 

323 

324 
end 