|
1 (* Title: HOL/Real_Vector_Spaces.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Vector Spaces and Algebras over the Reals *} |
|
6 |
|
7 theory Real_Vector_Spaces |
|
8 imports Metric_Spaces |
|
9 begin |
|
10 |
|
11 subsection {* Locale for additive functions *} |
|
12 |
|
13 locale additive = |
|
14 fixes f :: "'a::ab_group_add \<Rightarrow> 'b::ab_group_add" |
|
15 assumes add: "f (x + y) = f x + f y" |
|
16 begin |
|
17 |
|
18 lemma zero: "f 0 = 0" |
|
19 proof - |
|
20 have "f 0 = f (0 + 0)" by simp |
|
21 also have "\<dots> = f 0 + f 0" by (rule add) |
|
22 finally show "f 0 = 0" by simp |
|
23 qed |
|
24 |
|
25 lemma minus: "f (- x) = - f x" |
|
26 proof - |
|
27 have "f (- x) + f x = f (- x + x)" by (rule add [symmetric]) |
|
28 also have "\<dots> = - f x + f x" by (simp add: zero) |
|
29 finally show "f (- x) = - f x" by (rule add_right_imp_eq) |
|
30 qed |
|
31 |
|
32 lemma diff: "f (x - y) = f x - f y" |
|
33 by (simp add: add minus diff_minus) |
|
34 |
|
35 lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))" |
|
36 apply (cases "finite A") |
|
37 apply (induct set: finite) |
|
38 apply (simp add: zero) |
|
39 apply (simp add: add) |
|
40 apply (simp add: zero) |
|
41 done |
|
42 |
|
43 end |
|
44 |
|
45 subsection {* Vector spaces *} |
|
46 |
|
47 locale vector_space = |
|
48 fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" |
|
49 assumes scale_right_distrib [algebra_simps]: |
|
50 "scale a (x + y) = scale a x + scale a y" |
|
51 and scale_left_distrib [algebra_simps]: |
|
52 "scale (a + b) x = scale a x + scale b x" |
|
53 and scale_scale [simp]: "scale a (scale b x) = scale (a * b) x" |
|
54 and scale_one [simp]: "scale 1 x = x" |
|
55 begin |
|
56 |
|
57 lemma scale_left_commute: |
|
58 "scale a (scale b x) = scale b (scale a x)" |
|
59 by (simp add: mult_commute) |
|
60 |
|
61 lemma scale_zero_left [simp]: "scale 0 x = 0" |
|
62 and scale_minus_left [simp]: "scale (- a) x = - (scale a x)" |
|
63 and scale_left_diff_distrib [algebra_simps]: |
|
64 "scale (a - b) x = scale a x - scale b x" |
|
65 and scale_setsum_left: "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)" |
|
66 proof - |
|
67 interpret s: additive "\<lambda>a. scale a x" |
|
68 proof qed (rule scale_left_distrib) |
|
69 show "scale 0 x = 0" by (rule s.zero) |
|
70 show "scale (- a) x = - (scale a x)" by (rule s.minus) |
|
71 show "scale (a - b) x = scale a x - scale b x" by (rule s.diff) |
|
72 show "scale (setsum f A) x = (\<Sum>a\<in>A. scale (f a) x)" by (rule s.setsum) |
|
73 qed |
|
74 |
|
75 lemma scale_zero_right [simp]: "scale a 0 = 0" |
|
76 and scale_minus_right [simp]: "scale a (- x) = - (scale a x)" |
|
77 and scale_right_diff_distrib [algebra_simps]: |
|
78 "scale a (x - y) = scale a x - scale a y" |
|
79 and scale_setsum_right: "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))" |
|
80 proof - |
|
81 interpret s: additive "\<lambda>x. scale a x" |
|
82 proof qed (rule scale_right_distrib) |
|
83 show "scale a 0 = 0" by (rule s.zero) |
|
84 show "scale a (- x) = - (scale a x)" by (rule s.minus) |
|
85 show "scale a (x - y) = scale a x - scale a y" by (rule s.diff) |
|
86 show "scale a (setsum f A) = (\<Sum>x\<in>A. scale a (f x))" by (rule s.setsum) |
|
87 qed |
|
88 |
|
89 lemma scale_eq_0_iff [simp]: |
|
90 "scale a x = 0 \<longleftrightarrow> a = 0 \<or> x = 0" |
|
91 proof cases |
|
92 assume "a = 0" thus ?thesis by simp |
|
93 next |
|
94 assume anz [simp]: "a \<noteq> 0" |
|
95 { assume "scale a x = 0" |
|
96 hence "scale (inverse a) (scale a x) = 0" by simp |
|
97 hence "x = 0" by simp } |
|
98 thus ?thesis by force |
|
99 qed |
|
100 |
|
101 lemma scale_left_imp_eq: |
|
102 "\<lbrakk>a \<noteq> 0; scale a x = scale a y\<rbrakk> \<Longrightarrow> x = y" |
|
103 proof - |
|
104 assume nonzero: "a \<noteq> 0" |
|
105 assume "scale a x = scale a y" |
|
106 hence "scale a (x - y) = 0" |
|
107 by (simp add: scale_right_diff_distrib) |
|
108 hence "x - y = 0" by (simp add: nonzero) |
|
109 thus "x = y" by (simp only: right_minus_eq) |
|
110 qed |
|
111 |
|
112 lemma scale_right_imp_eq: |
|
113 "\<lbrakk>x \<noteq> 0; scale a x = scale b x\<rbrakk> \<Longrightarrow> a = b" |
|
114 proof - |
|
115 assume nonzero: "x \<noteq> 0" |
|
116 assume "scale a x = scale b x" |
|
117 hence "scale (a - b) x = 0" |
|
118 by (simp add: scale_left_diff_distrib) |
|
119 hence "a - b = 0" by (simp add: nonzero) |
|
120 thus "a = b" by (simp only: right_minus_eq) |
|
121 qed |
|
122 |
|
123 lemma scale_cancel_left [simp]: |
|
124 "scale a x = scale a y \<longleftrightarrow> x = y \<or> a = 0" |
|
125 by (auto intro: scale_left_imp_eq) |
|
126 |
|
127 lemma scale_cancel_right [simp]: |
|
128 "scale a x = scale b x \<longleftrightarrow> a = b \<or> x = 0" |
|
129 by (auto intro: scale_right_imp_eq) |
|
130 |
|
131 end |
|
132 |
|
133 subsection {* Real vector spaces *} |
|
134 |
|
135 class scaleR = |
|
136 fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75) |
|
137 begin |
|
138 |
|
139 abbreviation |
|
140 divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "'/\<^sub>R" 70) |
|
141 where |
|
142 "x /\<^sub>R r == scaleR (inverse r) x" |
|
143 |
|
144 end |
|
145 |
|
146 class real_vector = scaleR + ab_group_add + |
|
147 assumes scaleR_add_right: "scaleR a (x + y) = scaleR a x + scaleR a y" |
|
148 and scaleR_add_left: "scaleR (a + b) x = scaleR a x + scaleR b x" |
|
149 and scaleR_scaleR: "scaleR a (scaleR b x) = scaleR (a * b) x" |
|
150 and scaleR_one: "scaleR 1 x = x" |
|
151 |
|
152 interpretation real_vector: |
|
153 vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector" |
|
154 apply unfold_locales |
|
155 apply (rule scaleR_add_right) |
|
156 apply (rule scaleR_add_left) |
|
157 apply (rule scaleR_scaleR) |
|
158 apply (rule scaleR_one) |
|
159 done |
|
160 |
|
161 text {* Recover original theorem names *} |
|
162 |
|
163 lemmas scaleR_left_commute = real_vector.scale_left_commute |
|
164 lemmas scaleR_zero_left = real_vector.scale_zero_left |
|
165 lemmas scaleR_minus_left = real_vector.scale_minus_left |
|
166 lemmas scaleR_diff_left = real_vector.scale_left_diff_distrib |
|
167 lemmas scaleR_setsum_left = real_vector.scale_setsum_left |
|
168 lemmas scaleR_zero_right = real_vector.scale_zero_right |
|
169 lemmas scaleR_minus_right = real_vector.scale_minus_right |
|
170 lemmas scaleR_diff_right = real_vector.scale_right_diff_distrib |
|
171 lemmas scaleR_setsum_right = real_vector.scale_setsum_right |
|
172 lemmas scaleR_eq_0_iff = real_vector.scale_eq_0_iff |
|
173 lemmas scaleR_left_imp_eq = real_vector.scale_left_imp_eq |
|
174 lemmas scaleR_right_imp_eq = real_vector.scale_right_imp_eq |
|
175 lemmas scaleR_cancel_left = real_vector.scale_cancel_left |
|
176 lemmas scaleR_cancel_right = real_vector.scale_cancel_right |
|
177 |
|
178 text {* Legacy names *} |
|
179 |
|
180 lemmas scaleR_left_distrib = scaleR_add_left |
|
181 lemmas scaleR_right_distrib = scaleR_add_right |
|
182 lemmas scaleR_left_diff_distrib = scaleR_diff_left |
|
183 lemmas scaleR_right_diff_distrib = scaleR_diff_right |
|
184 |
|
185 lemma scaleR_minus1_left [simp]: |
|
186 fixes x :: "'a::real_vector" |
|
187 shows "scaleR (-1) x = - x" |
|
188 using scaleR_minus_left [of 1 x] by simp |
|
189 |
|
190 class real_algebra = real_vector + ring + |
|
191 assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)" |
|
192 and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)" |
|
193 |
|
194 class real_algebra_1 = real_algebra + ring_1 |
|
195 |
|
196 class real_div_algebra = real_algebra_1 + division_ring |
|
197 |
|
198 class real_field = real_div_algebra + field |
|
199 |
|
200 instantiation real :: real_field |
|
201 begin |
|
202 |
|
203 definition |
|
204 real_scaleR_def [simp]: "scaleR a x = a * x" |
|
205 |
|
206 instance proof |
|
207 qed (simp_all add: algebra_simps) |
|
208 |
|
209 end |
|
210 |
|
211 interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)" |
|
212 proof qed (rule scaleR_left_distrib) |
|
213 |
|
214 interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)" |
|
215 proof qed (rule scaleR_right_distrib) |
|
216 |
|
217 lemma nonzero_inverse_scaleR_distrib: |
|
218 fixes x :: "'a::real_div_algebra" shows |
|
219 "\<lbrakk>a \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> inverse (scaleR a x) = scaleR (inverse a) (inverse x)" |
|
220 by (rule inverse_unique, simp) |
|
221 |
|
222 lemma inverse_scaleR_distrib: |
|
223 fixes x :: "'a::{real_div_algebra, division_ring_inverse_zero}" |
|
224 shows "inverse (scaleR a x) = scaleR (inverse a) (inverse x)" |
|
225 apply (case_tac "a = 0", simp) |
|
226 apply (case_tac "x = 0", simp) |
|
227 apply (erule (1) nonzero_inverse_scaleR_distrib) |
|
228 done |
|
229 |
|
230 |
|
231 subsection {* Embedding of the Reals into any @{text real_algebra_1}: |
|
232 @{term of_real} *} |
|
233 |
|
234 definition |
|
235 of_real :: "real \<Rightarrow> 'a::real_algebra_1" where |
|
236 "of_real r = scaleR r 1" |
|
237 |
|
238 lemma scaleR_conv_of_real: "scaleR r x = of_real r * x" |
|
239 by (simp add: of_real_def) |
|
240 |
|
241 lemma of_real_0 [simp]: "of_real 0 = 0" |
|
242 by (simp add: of_real_def) |
|
243 |
|
244 lemma of_real_1 [simp]: "of_real 1 = 1" |
|
245 by (simp add: of_real_def) |
|
246 |
|
247 lemma of_real_add [simp]: "of_real (x + y) = of_real x + of_real y" |
|
248 by (simp add: of_real_def scaleR_left_distrib) |
|
249 |
|
250 lemma of_real_minus [simp]: "of_real (- x) = - of_real x" |
|
251 by (simp add: of_real_def) |
|
252 |
|
253 lemma of_real_diff [simp]: "of_real (x - y) = of_real x - of_real y" |
|
254 by (simp add: of_real_def scaleR_left_diff_distrib) |
|
255 |
|
256 lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y" |
|
257 by (simp add: of_real_def mult_commute) |
|
258 |
|
259 lemma nonzero_of_real_inverse: |
|
260 "x \<noteq> 0 \<Longrightarrow> of_real (inverse x) = |
|
261 inverse (of_real x :: 'a::real_div_algebra)" |
|
262 by (simp add: of_real_def nonzero_inverse_scaleR_distrib) |
|
263 |
|
264 lemma of_real_inverse [simp]: |
|
265 "of_real (inverse x) = |
|
266 inverse (of_real x :: 'a::{real_div_algebra, division_ring_inverse_zero})" |
|
267 by (simp add: of_real_def inverse_scaleR_distrib) |
|
268 |
|
269 lemma nonzero_of_real_divide: |
|
270 "y \<noteq> 0 \<Longrightarrow> of_real (x / y) = |
|
271 (of_real x / of_real y :: 'a::real_field)" |
|
272 by (simp add: divide_inverse nonzero_of_real_inverse) |
|
273 |
|
274 lemma of_real_divide [simp]: |
|
275 "of_real (x / y) = |
|
276 (of_real x / of_real y :: 'a::{real_field, field_inverse_zero})" |
|
277 by (simp add: divide_inverse) |
|
278 |
|
279 lemma of_real_power [simp]: |
|
280 "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n" |
|
281 by (induct n) simp_all |
|
282 |
|
283 lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)" |
|
284 by (simp add: of_real_def) |
|
285 |
|
286 lemma inj_of_real: |
|
287 "inj of_real" |
|
288 by (auto intro: injI) |
|
289 |
|
290 lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified] |
|
291 |
|
292 lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)" |
|
293 proof |
|
294 fix r |
|
295 show "of_real r = id r" |
|
296 by (simp add: of_real_def) |
|
297 qed |
|
298 |
|
299 text{*Collapse nested embeddings*} |
|
300 lemma of_real_of_nat_eq [simp]: "of_real (of_nat n) = of_nat n" |
|
301 by (induct n) auto |
|
302 |
|
303 lemma of_real_of_int_eq [simp]: "of_real (of_int z) = of_int z" |
|
304 by (cases z rule: int_diff_cases, simp) |
|
305 |
|
306 lemma of_real_numeral: "of_real (numeral w) = numeral w" |
|
307 using of_real_of_int_eq [of "numeral w"] by simp |
|
308 |
|
309 lemma of_real_neg_numeral: "of_real (neg_numeral w) = neg_numeral w" |
|
310 using of_real_of_int_eq [of "neg_numeral w"] by simp |
|
311 |
|
312 text{*Every real algebra has characteristic zero*} |
|
313 |
|
314 instance real_algebra_1 < ring_char_0 |
|
315 proof |
|
316 from inj_of_real inj_of_nat have "inj (of_real \<circ> of_nat)" by (rule inj_comp) |
|
317 then show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: comp_def) |
|
318 qed |
|
319 |
|
320 instance real_field < field_char_0 .. |
|
321 |
|
322 |
|
323 subsection {* The Set of Real Numbers *} |
|
324 |
|
325 definition Reals :: "'a::real_algebra_1 set" where |
|
326 "Reals = range of_real" |
|
327 |
|
328 notation (xsymbols) |
|
329 Reals ("\<real>") |
|
330 |
|
331 lemma Reals_of_real [simp]: "of_real r \<in> Reals" |
|
332 by (simp add: Reals_def) |
|
333 |
|
334 lemma Reals_of_int [simp]: "of_int z \<in> Reals" |
|
335 by (subst of_real_of_int_eq [symmetric], rule Reals_of_real) |
|
336 |
|
337 lemma Reals_of_nat [simp]: "of_nat n \<in> Reals" |
|
338 by (subst of_real_of_nat_eq [symmetric], rule Reals_of_real) |
|
339 |
|
340 lemma Reals_numeral [simp]: "numeral w \<in> Reals" |
|
341 by (subst of_real_numeral [symmetric], rule Reals_of_real) |
|
342 |
|
343 lemma Reals_neg_numeral [simp]: "neg_numeral w \<in> Reals" |
|
344 by (subst of_real_neg_numeral [symmetric], rule Reals_of_real) |
|
345 |
|
346 lemma Reals_0 [simp]: "0 \<in> Reals" |
|
347 apply (unfold Reals_def) |
|
348 apply (rule range_eqI) |
|
349 apply (rule of_real_0 [symmetric]) |
|
350 done |
|
351 |
|
352 lemma Reals_1 [simp]: "1 \<in> Reals" |
|
353 apply (unfold Reals_def) |
|
354 apply (rule range_eqI) |
|
355 apply (rule of_real_1 [symmetric]) |
|
356 done |
|
357 |
|
358 lemma Reals_add [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a + b \<in> Reals" |
|
359 apply (auto simp add: Reals_def) |
|
360 apply (rule range_eqI) |
|
361 apply (rule of_real_add [symmetric]) |
|
362 done |
|
363 |
|
364 lemma Reals_minus [simp]: "a \<in> Reals \<Longrightarrow> - a \<in> Reals" |
|
365 apply (auto simp add: Reals_def) |
|
366 apply (rule range_eqI) |
|
367 apply (rule of_real_minus [symmetric]) |
|
368 done |
|
369 |
|
370 lemma Reals_diff [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a - b \<in> Reals" |
|
371 apply (auto simp add: Reals_def) |
|
372 apply (rule range_eqI) |
|
373 apply (rule of_real_diff [symmetric]) |
|
374 done |
|
375 |
|
376 lemma Reals_mult [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a * b \<in> Reals" |
|
377 apply (auto simp add: Reals_def) |
|
378 apply (rule range_eqI) |
|
379 apply (rule of_real_mult [symmetric]) |
|
380 done |
|
381 |
|
382 lemma nonzero_Reals_inverse: |
|
383 fixes a :: "'a::real_div_algebra" |
|
384 shows "\<lbrakk>a \<in> Reals; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Reals" |
|
385 apply (auto simp add: Reals_def) |
|
386 apply (rule range_eqI) |
|
387 apply (erule nonzero_of_real_inverse [symmetric]) |
|
388 done |
|
389 |
|
390 lemma Reals_inverse [simp]: |
|
391 fixes a :: "'a::{real_div_algebra, division_ring_inverse_zero}" |
|
392 shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals" |
|
393 apply (auto simp add: Reals_def) |
|
394 apply (rule range_eqI) |
|
395 apply (rule of_real_inverse [symmetric]) |
|
396 done |
|
397 |
|
398 lemma nonzero_Reals_divide: |
|
399 fixes a b :: "'a::real_field" |
|
400 shows "\<lbrakk>a \<in> Reals; b \<in> Reals; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Reals" |
|
401 apply (auto simp add: Reals_def) |
|
402 apply (rule range_eqI) |
|
403 apply (erule nonzero_of_real_divide [symmetric]) |
|
404 done |
|
405 |
|
406 lemma Reals_divide [simp]: |
|
407 fixes a b :: "'a::{real_field, field_inverse_zero}" |
|
408 shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals" |
|
409 apply (auto simp add: Reals_def) |
|
410 apply (rule range_eqI) |
|
411 apply (rule of_real_divide [symmetric]) |
|
412 done |
|
413 |
|
414 lemma Reals_power [simp]: |
|
415 fixes a :: "'a::{real_algebra_1}" |
|
416 shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals" |
|
417 apply (auto simp add: Reals_def) |
|
418 apply (rule range_eqI) |
|
419 apply (rule of_real_power [symmetric]) |
|
420 done |
|
421 |
|
422 lemma Reals_cases [cases set: Reals]: |
|
423 assumes "q \<in> \<real>" |
|
424 obtains (of_real) r where "q = of_real r" |
|
425 unfolding Reals_def |
|
426 proof - |
|
427 from `q \<in> \<real>` have "q \<in> range of_real" unfolding Reals_def . |
|
428 then obtain r where "q = of_real r" .. |
|
429 then show thesis .. |
|
430 qed |
|
431 |
|
432 lemma Reals_induct [case_names of_real, induct set: Reals]: |
|
433 "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q" |
|
434 by (rule Reals_cases) auto |
|
435 |
|
436 |
|
437 subsection {* Real normed vector spaces *} |
|
438 |
|
439 class norm = |
|
440 fixes norm :: "'a \<Rightarrow> real" |
|
441 |
|
442 class sgn_div_norm = scaleR + norm + sgn + |
|
443 assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x" |
|
444 |
|
445 class dist_norm = dist + norm + minus + |
|
446 assumes dist_norm: "dist x y = norm (x - y)" |
|
447 |
|
448 class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist + |
|
449 assumes norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0" |
|
450 and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y" |
|
451 and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x" |
|
452 begin |
|
453 |
|
454 lemma norm_ge_zero [simp]: "0 \<le> norm x" |
|
455 proof - |
|
456 have "0 = norm (x + -1 *\<^sub>R x)" |
|
457 using scaleR_add_left[of 1 "-1" x] norm_scaleR[of 0 x] by (simp add: scaleR_one) |
|
458 also have "\<dots> \<le> norm x + norm (-1 *\<^sub>R x)" by (rule norm_triangle_ineq) |
|
459 finally show ?thesis by simp |
|
460 qed |
|
461 |
|
462 end |
|
463 |
|
464 class real_normed_algebra = real_algebra + real_normed_vector + |
|
465 assumes norm_mult_ineq: "norm (x * y) \<le> norm x * norm y" |
|
466 |
|
467 class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra + |
|
468 assumes norm_one [simp]: "norm 1 = 1" |
|
469 |
|
470 class real_normed_div_algebra = real_div_algebra + real_normed_vector + |
|
471 assumes norm_mult: "norm (x * y) = norm x * norm y" |
|
472 |
|
473 class real_normed_field = real_field + real_normed_div_algebra |
|
474 |
|
475 instance real_normed_div_algebra < real_normed_algebra_1 |
|
476 proof |
|
477 fix x y :: 'a |
|
478 show "norm (x * y) \<le> norm x * norm y" |
|
479 by (simp add: norm_mult) |
|
480 next |
|
481 have "norm (1 * 1::'a) = norm (1::'a) * norm (1::'a)" |
|
482 by (rule norm_mult) |
|
483 thus "norm (1::'a) = 1" by simp |
|
484 qed |
|
485 |
|
486 lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0" |
|
487 by simp |
|
488 |
|
489 lemma zero_less_norm_iff [simp]: |
|
490 fixes x :: "'a::real_normed_vector" |
|
491 shows "(0 < norm x) = (x \<noteq> 0)" |
|
492 by (simp add: order_less_le) |
|
493 |
|
494 lemma norm_not_less_zero [simp]: |
|
495 fixes x :: "'a::real_normed_vector" |
|
496 shows "\<not> norm x < 0" |
|
497 by (simp add: linorder_not_less) |
|
498 |
|
499 lemma norm_le_zero_iff [simp]: |
|
500 fixes x :: "'a::real_normed_vector" |
|
501 shows "(norm x \<le> 0) = (x = 0)" |
|
502 by (simp add: order_le_less) |
|
503 |
|
504 lemma norm_minus_cancel [simp]: |
|
505 fixes x :: "'a::real_normed_vector" |
|
506 shows "norm (- x) = norm x" |
|
507 proof - |
|
508 have "norm (- x) = norm (scaleR (- 1) x)" |
|
509 by (simp only: scaleR_minus_left scaleR_one) |
|
510 also have "\<dots> = \<bar>- 1\<bar> * norm x" |
|
511 by (rule norm_scaleR) |
|
512 finally show ?thesis by simp |
|
513 qed |
|
514 |
|
515 lemma norm_minus_commute: |
|
516 fixes a b :: "'a::real_normed_vector" |
|
517 shows "norm (a - b) = norm (b - a)" |
|
518 proof - |
|
519 have "norm (- (b - a)) = norm (b - a)" |
|
520 by (rule norm_minus_cancel) |
|
521 thus ?thesis by simp |
|
522 qed |
|
523 |
|
524 lemma norm_triangle_ineq2: |
|
525 fixes a b :: "'a::real_normed_vector" |
|
526 shows "norm a - norm b \<le> norm (a - b)" |
|
527 proof - |
|
528 have "norm (a - b + b) \<le> norm (a - b) + norm b" |
|
529 by (rule norm_triangle_ineq) |
|
530 thus ?thesis by simp |
|
531 qed |
|
532 |
|
533 lemma norm_triangle_ineq3: |
|
534 fixes a b :: "'a::real_normed_vector" |
|
535 shows "\<bar>norm a - norm b\<bar> \<le> norm (a - b)" |
|
536 apply (subst abs_le_iff) |
|
537 apply auto |
|
538 apply (rule norm_triangle_ineq2) |
|
539 apply (subst norm_minus_commute) |
|
540 apply (rule norm_triangle_ineq2) |
|
541 done |
|
542 |
|
543 lemma norm_triangle_ineq4: |
|
544 fixes a b :: "'a::real_normed_vector" |
|
545 shows "norm (a - b) \<le> norm a + norm b" |
|
546 proof - |
|
547 have "norm (a + - b) \<le> norm a + norm (- b)" |
|
548 by (rule norm_triangle_ineq) |
|
549 thus ?thesis |
|
550 by (simp only: diff_minus norm_minus_cancel) |
|
551 qed |
|
552 |
|
553 lemma norm_diff_ineq: |
|
554 fixes a b :: "'a::real_normed_vector" |
|
555 shows "norm a - norm b \<le> norm (a + b)" |
|
556 proof - |
|
557 have "norm a - norm (- b) \<le> norm (a - - b)" |
|
558 by (rule norm_triangle_ineq2) |
|
559 thus ?thesis by simp |
|
560 qed |
|
561 |
|
562 lemma norm_diff_triangle_ineq: |
|
563 fixes a b c d :: "'a::real_normed_vector" |
|
564 shows "norm ((a + b) - (c + d)) \<le> norm (a - c) + norm (b - d)" |
|
565 proof - |
|
566 have "norm ((a + b) - (c + d)) = norm ((a - c) + (b - d))" |
|
567 by (simp add: diff_minus add_ac) |
|
568 also have "\<dots> \<le> norm (a - c) + norm (b - d)" |
|
569 by (rule norm_triangle_ineq) |
|
570 finally show ?thesis . |
|
571 qed |
|
572 |
|
573 lemma abs_norm_cancel [simp]: |
|
574 fixes a :: "'a::real_normed_vector" |
|
575 shows "\<bar>norm a\<bar> = norm a" |
|
576 by (rule abs_of_nonneg [OF norm_ge_zero]) |
|
577 |
|
578 lemma norm_add_less: |
|
579 fixes x y :: "'a::real_normed_vector" |
|
580 shows "\<lbrakk>norm x < r; norm y < s\<rbrakk> \<Longrightarrow> norm (x + y) < r + s" |
|
581 by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono]) |
|
582 |
|
583 lemma norm_mult_less: |
|
584 fixes x y :: "'a::real_normed_algebra" |
|
585 shows "\<lbrakk>norm x < r; norm y < s\<rbrakk> \<Longrightarrow> norm (x * y) < r * s" |
|
586 apply (rule order_le_less_trans [OF norm_mult_ineq]) |
|
587 apply (simp add: mult_strict_mono') |
|
588 done |
|
589 |
|
590 lemma norm_of_real [simp]: |
|
591 "norm (of_real r :: 'a::real_normed_algebra_1) = \<bar>r\<bar>" |
|
592 unfolding of_real_def by simp |
|
593 |
|
594 lemma norm_numeral [simp]: |
|
595 "norm (numeral w::'a::real_normed_algebra_1) = numeral w" |
|
596 by (subst of_real_numeral [symmetric], subst norm_of_real, simp) |
|
597 |
|
598 lemma norm_neg_numeral [simp]: |
|
599 "norm (neg_numeral w::'a::real_normed_algebra_1) = numeral w" |
|
600 by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp) |
|
601 |
|
602 lemma norm_of_int [simp]: |
|
603 "norm (of_int z::'a::real_normed_algebra_1) = \<bar>of_int z\<bar>" |
|
604 by (subst of_real_of_int_eq [symmetric], rule norm_of_real) |
|
605 |
|
606 lemma norm_of_nat [simp]: |
|
607 "norm (of_nat n::'a::real_normed_algebra_1) = of_nat n" |
|
608 apply (subst of_real_of_nat_eq [symmetric]) |
|
609 apply (subst norm_of_real, simp) |
|
610 done |
|
611 |
|
612 lemma nonzero_norm_inverse: |
|
613 fixes a :: "'a::real_normed_div_algebra" |
|
614 shows "a \<noteq> 0 \<Longrightarrow> norm (inverse a) = inverse (norm a)" |
|
615 apply (rule inverse_unique [symmetric]) |
|
616 apply (simp add: norm_mult [symmetric]) |
|
617 done |
|
618 |
|
619 lemma norm_inverse: |
|
620 fixes a :: "'a::{real_normed_div_algebra, division_ring_inverse_zero}" |
|
621 shows "norm (inverse a) = inverse (norm a)" |
|
622 apply (case_tac "a = 0", simp) |
|
623 apply (erule nonzero_norm_inverse) |
|
624 done |
|
625 |
|
626 lemma nonzero_norm_divide: |
|
627 fixes a b :: "'a::real_normed_field" |
|
628 shows "b \<noteq> 0 \<Longrightarrow> norm (a / b) = norm a / norm b" |
|
629 by (simp add: divide_inverse norm_mult nonzero_norm_inverse) |
|
630 |
|
631 lemma norm_divide: |
|
632 fixes a b :: "'a::{real_normed_field, field_inverse_zero}" |
|
633 shows "norm (a / b) = norm a / norm b" |
|
634 by (simp add: divide_inverse norm_mult norm_inverse) |
|
635 |
|
636 lemma norm_power_ineq: |
|
637 fixes x :: "'a::{real_normed_algebra_1}" |
|
638 shows "norm (x ^ n) \<le> norm x ^ n" |
|
639 proof (induct n) |
|
640 case 0 show "norm (x ^ 0) \<le> norm x ^ 0" by simp |
|
641 next |
|
642 case (Suc n) |
|
643 have "norm (x * x ^ n) \<le> norm x * norm (x ^ n)" |
|
644 by (rule norm_mult_ineq) |
|
645 also from Suc have "\<dots> \<le> norm x * norm x ^ n" |
|
646 using norm_ge_zero by (rule mult_left_mono) |
|
647 finally show "norm (x ^ Suc n) \<le> norm x ^ Suc n" |
|
648 by simp |
|
649 qed |
|
650 |
|
651 lemma norm_power: |
|
652 fixes x :: "'a::{real_normed_div_algebra}" |
|
653 shows "norm (x ^ n) = norm x ^ n" |
|
654 by (induct n) (simp_all add: norm_mult) |
|
655 |
|
656 text {* Every normed vector space is a metric space. *} |
|
657 |
|
658 instance real_normed_vector < metric_space |
|
659 proof |
|
660 fix x y :: 'a show "dist x y = 0 \<longleftrightarrow> x = y" |
|
661 unfolding dist_norm by simp |
|
662 next |
|
663 fix x y z :: 'a show "dist x y \<le> dist x z + dist y z" |
|
664 unfolding dist_norm |
|
665 using norm_triangle_ineq4 [of "x - z" "y - z"] by simp |
|
666 qed |
|
667 |
|
668 subsection {* Class instances for real numbers *} |
|
669 |
|
670 instantiation real :: real_normed_field |
|
671 begin |
|
672 |
|
673 definition real_norm_def [simp]: |
|
674 "norm r = \<bar>r\<bar>" |
|
675 |
|
676 instance |
|
677 apply (intro_classes, unfold real_norm_def real_scaleR_def) |
|
678 apply (rule dist_real_def) |
|
679 apply (simp add: sgn_real_def) |
|
680 apply (rule abs_eq_0) |
|
681 apply (rule abs_triangle_ineq) |
|
682 apply (rule abs_mult) |
|
683 apply (rule abs_mult) |
|
684 done |
|
685 |
|
686 end |
|
687 |
|
688 instance real :: linear_continuum_topology .. |
|
689 |
|
690 subsection {* Extra type constraints *} |
|
691 |
|
692 text {* Only allow @{term "open"} in class @{text topological_space}. *} |
|
693 |
|
694 setup {* Sign.add_const_constraint |
|
695 (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *} |
|
696 |
|
697 text {* Only allow @{term dist} in class @{text metric_space}. *} |
|
698 |
|
699 setup {* Sign.add_const_constraint |
|
700 (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *} |
|
701 |
|
702 text {* Only allow @{term norm} in class @{text real_normed_vector}. *} |
|
703 |
|
704 setup {* Sign.add_const_constraint |
|
705 (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *} |
|
706 |
|
707 subsection {* Sign function *} |
|
708 |
|
709 lemma norm_sgn: |
|
710 "norm (sgn(x::'a::real_normed_vector)) = (if x = 0 then 0 else 1)" |
|
711 by (simp add: sgn_div_norm) |
|
712 |
|
713 lemma sgn_zero [simp]: "sgn(0::'a::real_normed_vector) = 0" |
|
714 by (simp add: sgn_div_norm) |
|
715 |
|
716 lemma sgn_zero_iff: "(sgn(x::'a::real_normed_vector) = 0) = (x = 0)" |
|
717 by (simp add: sgn_div_norm) |
|
718 |
|
719 lemma sgn_minus: "sgn (- x) = - sgn(x::'a::real_normed_vector)" |
|
720 by (simp add: sgn_div_norm) |
|
721 |
|
722 lemma sgn_scaleR: |
|
723 "sgn (scaleR r x) = scaleR (sgn r) (sgn(x::'a::real_normed_vector))" |
|
724 by (simp add: sgn_div_norm mult_ac) |
|
725 |
|
726 lemma sgn_one [simp]: "sgn (1::'a::real_normed_algebra_1) = 1" |
|
727 by (simp add: sgn_div_norm) |
|
728 |
|
729 lemma sgn_of_real: |
|
730 "sgn (of_real r::'a::real_normed_algebra_1) = of_real (sgn r)" |
|
731 unfolding of_real_def by (simp only: sgn_scaleR sgn_one) |
|
732 |
|
733 lemma sgn_mult: |
|
734 fixes x y :: "'a::real_normed_div_algebra" |
|
735 shows "sgn (x * y) = sgn x * sgn y" |
|
736 by (simp add: sgn_div_norm norm_mult mult_commute) |
|
737 |
|
738 lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>" |
|
739 by (simp add: sgn_div_norm divide_inverse) |
|
740 |
|
741 lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1" |
|
742 unfolding real_sgn_eq by simp |
|
743 |
|
744 lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1" |
|
745 unfolding real_sgn_eq by simp |
|
746 |
|
747 lemma norm_conv_dist: "norm x = dist x 0" |
|
748 unfolding dist_norm by simp |
|
749 |
|
750 subsection {* Bounded Linear and Bilinear Operators *} |
|
751 |
|
752 locale bounded_linear = additive f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" + |
|
753 assumes scaleR: "f (scaleR r x) = scaleR r (f x)" |
|
754 assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K" |
|
755 begin |
|
756 |
|
757 lemma pos_bounded: |
|
758 "\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K" |
|
759 proof - |
|
760 obtain K where K: "\<And>x. norm (f x) \<le> norm x * K" |
|
761 using bounded by fast |
|
762 show ?thesis |
|
763 proof (intro exI impI conjI allI) |
|
764 show "0 < max 1 K" |
|
765 by (rule order_less_le_trans [OF zero_less_one le_maxI1]) |
|
766 next |
|
767 fix x |
|
768 have "norm (f x) \<le> norm x * K" using K . |
|
769 also have "\<dots> \<le> norm x * max 1 K" |
|
770 by (rule mult_left_mono [OF le_maxI2 norm_ge_zero]) |
|
771 finally show "norm (f x) \<le> norm x * max 1 K" . |
|
772 qed |
|
773 qed |
|
774 |
|
775 lemma nonneg_bounded: |
|
776 "\<exists>K\<ge>0. \<forall>x. norm (f x) \<le> norm x * K" |
|
777 proof - |
|
778 from pos_bounded |
|
779 show ?thesis by (auto intro: order_less_imp_le) |
|
780 qed |
|
781 |
|
782 end |
|
783 |
|
784 lemma bounded_linear_intro: |
|
785 assumes "\<And>x y. f (x + y) = f x + f y" |
|
786 assumes "\<And>r x. f (scaleR r x) = scaleR r (f x)" |
|
787 assumes "\<And>x. norm (f x) \<le> norm x * K" |
|
788 shows "bounded_linear f" |
|
789 by default (fast intro: assms)+ |
|
790 |
|
791 locale bounded_bilinear = |
|
792 fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector] |
|
793 \<Rightarrow> 'c::real_normed_vector" |
|
794 (infixl "**" 70) |
|
795 assumes add_left: "prod (a + a') b = prod a b + prod a' b" |
|
796 assumes add_right: "prod a (b + b') = prod a b + prod a b'" |
|
797 assumes scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)" |
|
798 assumes scaleR_right: "prod a (scaleR r b) = scaleR r (prod a b)" |
|
799 assumes bounded: "\<exists>K. \<forall>a b. norm (prod a b) \<le> norm a * norm b * K" |
|
800 begin |
|
801 |
|
802 lemma pos_bounded: |
|
803 "\<exists>K>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K" |
|
804 apply (cut_tac bounded, erule exE) |
|
805 apply (rule_tac x="max 1 K" in exI, safe) |
|
806 apply (rule order_less_le_trans [OF zero_less_one le_maxI1]) |
|
807 apply (drule spec, drule spec, erule order_trans) |
|
808 apply (rule mult_left_mono [OF le_maxI2]) |
|
809 apply (intro mult_nonneg_nonneg norm_ge_zero) |
|
810 done |
|
811 |
|
812 lemma nonneg_bounded: |
|
813 "\<exists>K\<ge>0. \<forall>a b. norm (a ** b) \<le> norm a * norm b * K" |
|
814 proof - |
|
815 from pos_bounded |
|
816 show ?thesis by (auto intro: order_less_imp_le) |
|
817 qed |
|
818 |
|
819 lemma additive_right: "additive (\<lambda>b. prod a b)" |
|
820 by (rule additive.intro, rule add_right) |
|
821 |
|
822 lemma additive_left: "additive (\<lambda>a. prod a b)" |
|
823 by (rule additive.intro, rule add_left) |
|
824 |
|
825 lemma zero_left: "prod 0 b = 0" |
|
826 by (rule additive.zero [OF additive_left]) |
|
827 |
|
828 lemma zero_right: "prod a 0 = 0" |
|
829 by (rule additive.zero [OF additive_right]) |
|
830 |
|
831 lemma minus_left: "prod (- a) b = - prod a b" |
|
832 by (rule additive.minus [OF additive_left]) |
|
833 |
|
834 lemma minus_right: "prod a (- b) = - prod a b" |
|
835 by (rule additive.minus [OF additive_right]) |
|
836 |
|
837 lemma diff_left: |
|
838 "prod (a - a') b = prod a b - prod a' b" |
|
839 by (rule additive.diff [OF additive_left]) |
|
840 |
|
841 lemma diff_right: |
|
842 "prod a (b - b') = prod a b - prod a b'" |
|
843 by (rule additive.diff [OF additive_right]) |
|
844 |
|
845 lemma bounded_linear_left: |
|
846 "bounded_linear (\<lambda>a. a ** b)" |
|
847 apply (cut_tac bounded, safe) |
|
848 apply (rule_tac K="norm b * K" in bounded_linear_intro) |
|
849 apply (rule add_left) |
|
850 apply (rule scaleR_left) |
|
851 apply (simp add: mult_ac) |
|
852 done |
|
853 |
|
854 lemma bounded_linear_right: |
|
855 "bounded_linear (\<lambda>b. a ** b)" |
|
856 apply (cut_tac bounded, safe) |
|
857 apply (rule_tac K="norm a * K" in bounded_linear_intro) |
|
858 apply (rule add_right) |
|
859 apply (rule scaleR_right) |
|
860 apply (simp add: mult_ac) |
|
861 done |
|
862 |
|
863 lemma prod_diff_prod: |
|
864 "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)" |
|
865 by (simp add: diff_left diff_right) |
|
866 |
|
867 end |
|
868 |
|
869 lemma bounded_bilinear_mult: |
|
870 "bounded_bilinear (op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)" |
|
871 apply (rule bounded_bilinear.intro) |
|
872 apply (rule distrib_right) |
|
873 apply (rule distrib_left) |
|
874 apply (rule mult_scaleR_left) |
|
875 apply (rule mult_scaleR_right) |
|
876 apply (rule_tac x="1" in exI) |
|
877 apply (simp add: norm_mult_ineq) |
|
878 done |
|
879 |
|
880 lemma bounded_linear_mult_left: |
|
881 "bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)" |
|
882 using bounded_bilinear_mult |
|
883 by (rule bounded_bilinear.bounded_linear_left) |
|
884 |
|
885 lemma bounded_linear_mult_right: |
|
886 "bounded_linear (\<lambda>y::'a::real_normed_algebra. x * y)" |
|
887 using bounded_bilinear_mult |
|
888 by (rule bounded_bilinear.bounded_linear_right) |
|
889 |
|
890 lemma bounded_linear_divide: |
|
891 "bounded_linear (\<lambda>x::'a::real_normed_field. x / y)" |
|
892 unfolding divide_inverse by (rule bounded_linear_mult_left) |
|
893 |
|
894 lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR" |
|
895 apply (rule bounded_bilinear.intro) |
|
896 apply (rule scaleR_left_distrib) |
|
897 apply (rule scaleR_right_distrib) |
|
898 apply simp |
|
899 apply (rule scaleR_left_commute) |
|
900 apply (rule_tac x="1" in exI, simp) |
|
901 done |
|
902 |
|
903 lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)" |
|
904 using bounded_bilinear_scaleR |
|
905 by (rule bounded_bilinear.bounded_linear_left) |
|
906 |
|
907 lemma bounded_linear_scaleR_right: "bounded_linear (\<lambda>x. scaleR r x)" |
|
908 using bounded_bilinear_scaleR |
|
909 by (rule bounded_bilinear.bounded_linear_right) |
|
910 |
|
911 lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)" |
|
912 unfolding of_real_def by (rule bounded_linear_scaleR_left) |
|
913 |
|
914 instance real_normed_algebra_1 \<subseteq> perfect_space |
|
915 proof |
|
916 fix x::'a |
|
917 show "\<not> open {x}" |
|
918 unfolding open_dist dist_norm |
|
919 by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp) |
|
920 qed |
|
921 |
|
922 end |