author  huffman 
Wed, 03 Jun 2009 08:43:01 0700  
changeset 31414  8514775606e0 
parent 31289  847f00f435d4 
child 31417  c12b25b7f015 
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 

31414  13 
class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist + 
29993  14 
fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real" 
15 
assumes inner_commute: "inner x y = inner y x" 

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

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

18 
and inner_ge_zero [simp]: "0 \<le> inner x x" 

19 
and inner_eq_zero_iff [simp]: "inner x x = 0 \<longleftrightarrow> x = 0" 

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

21 
begin 

22 

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

30067  24 
using inner_left_distrib [of 0 0 x] by simp 
29993  25 

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

30067  27 
using inner_left_distrib [of x " x" y] by simp 
29993  28 

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

30 
by (simp add: diff_minus inner_left_distrib) 

31 

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

33 

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

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

36 

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

38 
using inner_scaleR_left [of r y x] by (simp only: inner_commute) 

39 

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

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

42 

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

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

45 

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

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

48 

49 
lemmas inner_distrib = inner_left_distrib inner_right_distrib 

50 
lemmas inner_diff = inner_diff_left inner_diff_right 

51 
lemmas inner_scaleR = inner_scaleR_left inner_scaleR_right 

52 

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

54 
by (simp add: order_less_le) 

55 

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

57 
by (simp add: norm_eq_sqrt_inner) 

58 

30046  59 
lemma Cauchy_Schwarz_ineq: 
29993  60 
"(inner x y)\<twosuperior> \<le> inner x x * inner y y" 
61 
proof (cases) 

62 
assume "y = 0" 

63 
thus ?thesis by simp 

64 
next 

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

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

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

68 
by (rule inner_ge_zero) 

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

70 
by (simp add: inner_diff inner_scaleR) 

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

72 
by (simp add: power2_eq_square inner_commute) 

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

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

75 
by (simp add: le_diff_eq) 

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

77 
by (simp add: pos_divide_le_eq y) 

78 
qed 

79 

30046  80 
lemma Cauchy_Schwarz_ineq2: 
29993  81 
"\<bar>inner x y\<bar> \<le> norm x * norm y" 
82 
proof (rule power2_le_imp_le) 

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

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

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

88 
unfolding norm_eq_sqrt_inner 

89 
by (intro mult_nonneg_nonneg real_sqrt_ge_zero inner_ge_zero) 

90 
qed 

91 

92 
subclass real_normed_vector 

93 
proof 

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

95 
show "0 \<le> norm x" 

96 
unfolding norm_eq_sqrt_inner by simp 

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

98 
unfolding norm_eq_sqrt_inner by simp 

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

100 
proof (rule power2_le_imp_le) 

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

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

105 
by (simp add: inner_distrib inner_commute) 

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

107 
unfolding norm_eq_sqrt_inner 

108 
by (simp add: add_nonneg_nonneg) 

109 
qed 

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

111 
by (simp add: real_sqrt_mult_distrib) 

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

113 
unfolding norm_eq_sqrt_inner 

114 
by (simp add: inner_scaleR power2_eq_square mult_assoc) 

115 
qed 

116 

117 
end 

118 

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

119 
interpretation inner: 
29993  120 
bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real" 
121 
proof 

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

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

124 
by (rule inner_left_distrib) 

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

126 
by (rule inner_right_distrib) 

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

128 
unfolding real_scaleR_def by (rule inner_scaleR_left) 

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

130 
unfolding real_scaleR_def by (rule inner_scaleR_right) 

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

132 
proof 

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

30046  134 
by (simp add: Cauchy_Schwarz_ineq2) 
29993  135 
qed 
136 
qed 

137 

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

138 
interpretation inner_left: 
29993  139 
bounded_linear "\<lambda>x::'a::real_inner. inner x y" 
140 
by (rule inner.bounded_linear_left) 

141 

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

142 
interpretation inner_right: 
29993  143 
bounded_linear "\<lambda>y::'a::real_inner. inner x y" 
144 
by (rule inner.bounded_linear_right) 

145 

146 

147 
subsection {* Class instances *} 

148 

149 
instantiation real :: real_inner 

150 
begin 

151 

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

153 

154 
instance proof 

155 
fix x y z r :: real 

156 
show "inner x y = inner y x" 

157 
unfolding inner_real_def by (rule mult_commute) 

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

159 
unfolding inner_real_def by (rule left_distrib) 

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

161 
unfolding inner_real_def real_scaleR_def by (rule mult_assoc) 

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

163 
unfolding inner_real_def by simp 

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

165 
unfolding inner_real_def by simp 

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

167 
unfolding inner_real_def by simp 

168 
qed 

169 

170 
end 

171 

172 
instantiation complex :: real_inner 

173 
begin 

174 

175 
definition inner_complex_def: 

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

177 

178 
instance proof 

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

180 
show "inner x y = inner y x" 

181 
unfolding inner_complex_def by (simp add: mult_commute) 

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

183 
unfolding inner_complex_def by (simp add: left_distrib) 

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

185 
unfolding inner_complex_def by (simp add: right_distrib) 

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

187 
unfolding inner_complex_def by (simp add: add_nonneg_nonneg) 

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

189 
unfolding inner_complex_def 

190 
by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff) 

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

192 
unfolding inner_complex_def complex_norm_def 

193 
by (simp add: power2_eq_square) 

194 
qed 

195 

196 
end 

197 

198 

199 
subsection {* Gradient derivative *} 

200 

201 
definition 

202 
gderiv :: 

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

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

205 
where 

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

207 

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

209 
by (simp only: deriv_def field_fderiv_def) 

210 

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

212 
by (simp only: gderiv_def deriv_fderiv inner_real_def) 

213 

214 
lemma GDERIV_DERIV_compose: 

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

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

217 
unfolding gderiv_def deriv_fderiv 

218 
apply (drule (1) FDERIV_compose) 

219 
apply (simp add: inner_scaleR_right mult_ac) 

220 
done 

221 

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

223 
by simp 

224 

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

226 
by simp 

227 

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

229 
unfolding gderiv_def inner_right.zero by (rule FDERIV_const) 

230 

231 
lemma GDERIV_add: 

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

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

234 
unfolding gderiv_def inner_right.add by (rule FDERIV_add) 

235 

236 
lemma GDERIV_minus: 

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

238 
unfolding gderiv_def inner_right.minus by (rule FDERIV_minus) 

239 

240 
lemma GDERIV_diff: 

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

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

243 
unfolding gderiv_def inner_right.diff by (rule FDERIV_diff) 

244 

245 
lemma GDERIV_scaleR: 

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

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

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

249 
unfolding gderiv_def deriv_fderiv inner_right.add inner_right.scaleR 

250 
apply (rule FDERIV_subst) 

251 
apply (erule (1) scaleR.FDERIV) 

252 
apply (simp add: mult_ac) 

253 
done 

254 

255 
lemma GDERIV_mult: 

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

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

258 
unfolding gderiv_def 

259 
apply (rule FDERIV_subst) 

260 
apply (erule (1) FDERIV_mult) 

261 
apply (simp add: inner_distrib inner_scaleR mult_ac) 

262 
done 

263 

264 
lemma GDERIV_inverse: 

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

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

267 
apply (erule GDERIV_DERIV_compose) 

268 
apply (erule DERIV_inverse [folded numeral_2_eq_2]) 

269 
done 

270 

271 
lemma GDERIV_norm: 

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

273 
proof  

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

275 
by (intro inner.FDERIV FDERIV_ident) 

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

277 
by (simp add: expand_fun_eq inner_scaleR inner_commute) 

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

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

280 
by (rule DERIV_real_sqrt) 

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

282 
by (simp add: sgn_div_norm norm_eq_sqrt_inner) 

283 
show ?thesis 

284 
unfolding norm_eq_sqrt_inner 

285 
apply (rule GDERIV_subst [OF _ 4]) 

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

287 
apply (subst gderiv_def) 

288 
apply (rule FDERIV_subst [OF _ 2]) 

289 
apply (rule 1) 

290 
apply (rule 3) 

291 
done 

292 
qed 

293 

294 
lemmas FDERIV_norm = GDERIV_norm [unfolded gderiv_def] 

295 

296 
end 