9 |
9 |
10 |
10 |
11 |
11 |
12 subsection {* Quasinorms *}; |
12 subsection {* Quasinorms *}; |
13 |
13 |
|
14 text{* A \emph{quasinorm} $\norm{\cdot}$ is a function on a real vector space into the reals |
|
15 that has the following properties: *}; |
14 |
16 |
15 constdefs |
17 constdefs |
16 is_quasinorm :: "['a set, 'a => real] => bool" |
18 is_quasinorm :: "['a::{plus, minus} set, 'a => real] => bool" |
17 "is_quasinorm V norm == ALL x: V. ALL y:V. ALL a. |
19 "is_quasinorm V norm == ALL x: V. ALL y:V. ALL a. |
18 0r <= norm x |
20 0r <= norm x |
19 & norm (a [*] x) = (rabs a) * (norm x) |
21 & norm (a <*> x) = (rabs a) * (norm x) |
20 & norm (x [+] y) <= norm x + norm y"; |
22 & norm (x + y) <= norm x + norm y"; |
21 |
23 |
22 lemma is_quasinormI [intro]: |
24 lemma is_quasinormI [intro]: |
23 "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x; |
25 "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x; |
24 !! x a. x:V ==> norm (a [*] x) = (rabs a) * (norm x); |
26 !! x a. x:V ==> norm (a <*> x) = (rabs a) * (norm x); |
25 !! x y. [|x:V; y:V |] ==> norm (x [+] y) <= norm x + norm y |] |
27 !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] |
26 ==> is_quasinorm V norm"; |
28 ==> is_quasinorm V norm"; |
27 by (unfold is_quasinorm_def, force); |
29 by (unfold is_quasinorm_def, force); |
28 |
30 |
29 lemma quasinorm_ge_zero [intro!!]: |
31 lemma quasinorm_ge_zero [intro!!]: |
30 "[| is_quasinorm V norm; x:V |] ==> 0r <= norm x"; |
32 "[| is_quasinorm V norm; x:V |] ==> 0r <= norm x"; |
31 by (unfold is_quasinorm_def, force); |
33 by (unfold is_quasinorm_def, force); |
32 |
34 |
33 lemma quasinorm_mult_distrib: |
35 lemma quasinorm_mult_distrib: |
34 "[| is_quasinorm V norm; x:V |] |
36 "[| is_quasinorm V norm; x:V |] |
35 ==> norm (a [*] x) = (rabs a) * (norm x)"; |
37 ==> norm (a <*> x) = (rabs a) * (norm x)"; |
36 by (unfold is_quasinorm_def, force); |
38 by (unfold is_quasinorm_def, force); |
37 |
39 |
38 lemma quasinorm_triangle_ineq: |
40 lemma quasinorm_triangle_ineq: |
39 "[| is_quasinorm V norm; x:V; y:V |] |
41 "[| is_quasinorm V norm; x:V; y:V |] |
40 ==> norm (x [+] y) <= norm x + norm y"; |
42 ==> norm (x + y) <= norm x + norm y"; |
41 by (unfold is_quasinorm_def, force); |
43 by (unfold is_quasinorm_def, force); |
42 |
44 |
43 lemma quasinorm_diff_triangle_ineq: |
45 lemma quasinorm_diff_triangle_ineq: |
44 "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |] |
46 "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |] |
45 ==> norm (x [-] y) <= norm x + norm y"; |
47 ==> norm (x - y) <= norm x + norm y"; |
46 proof -; |
48 proof -; |
47 assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V"; |
49 assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V"; |
48 have "norm (x [-] y) = norm (x [+] - 1r [*] y)"; |
50 have "norm (x - y) = norm (x + - 1r <*> y)"; |
49 by (simp add: diff_def negate_def); |
51 by (simp! add: diff_eq2 negate_eq2); |
50 also; have "... <= norm x + norm (- 1r [*] y)"; |
52 also; have "... <= norm x + norm (- 1r <*> y)"; |
51 by (simp! add: quasinorm_triangle_ineq); |
53 by (simp! add: quasinorm_triangle_ineq); |
52 also; have "norm (- 1r [*] y) = rabs (- 1r) * norm y"; |
54 also; have "norm (- 1r <*> y) = rabs (- 1r) * norm y"; |
53 by (rule quasinorm_mult_distrib); |
55 by (rule quasinorm_mult_distrib); |
54 also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one); |
56 also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one); |
55 finally; show "norm (x [-] y) <= norm x + norm y"; by simp; |
57 finally; show "norm (x - y) <= norm x + norm y"; by simp; |
56 qed; |
58 qed; |
57 |
59 |
58 lemma quasinorm_minus: |
60 lemma quasinorm_minus: |
59 "[| is_quasinorm V norm; x:V; is_vectorspace V |] |
61 "[| is_quasinorm V norm; x:V; is_vectorspace V |] |
60 ==> norm ([-] x) = norm x"; |
62 ==> norm (- x) = norm x"; |
61 proof -; |
63 proof -; |
62 assume "is_quasinorm V norm" "x:V" "is_vectorspace V"; |
64 assume "is_quasinorm V norm" "x:V" "is_vectorspace V"; |
63 have "norm ([-] x) = norm (-1r [*] x)"; by (unfold negate_def) force; |
65 have "norm (- x) = norm (-1r <*> x)"; by (simp! only: negate_eq1); |
64 also; have "... = rabs (-1r) * norm x"; |
66 also; have "... = rabs (-1r) * norm x"; |
65 by (rule quasinorm_mult_distrib); |
67 by (rule quasinorm_mult_distrib); |
66 also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one); |
68 also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one); |
67 finally; show "norm ([-] x) = norm x"; by simp; |
69 finally; show "norm (- x) = norm x"; by simp; |
68 qed; |
70 qed; |
69 |
|
70 |
71 |
71 |
72 |
72 subsection {* Norms *}; |
73 subsection {* Norms *}; |
73 |
74 |
|
75 text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only $\zero$ to $0$. *}; |
74 |
76 |
75 constdefs |
77 constdefs |
76 is_norm :: "['a set, 'a => real] => bool" |
78 is_norm :: "['a::{minus, plus} set, 'a => real] => bool" |
77 "is_norm V norm == ALL x: V. is_quasinorm V norm |
79 "is_norm V norm == ALL x: V. is_quasinorm V norm |
78 & (norm x = 0r) = (x = <0>)"; |
80 & (norm x = 0r) = (x = <0>)"; |
79 |
81 |
80 lemma is_normI [intro]: |
82 lemma is_normI [intro]: |
81 "ALL x: V. is_quasinorm V norm & (norm x = 0r) = (x = <0>) |
83 "ALL x: V. is_quasinorm V norm & (norm x = 0r) = (x = <0>) |
82 ==> is_norm V norm"; |
84 ==> is_norm V norm"; by (simp only: is_norm_def); |
83 by (unfold is_norm_def, force); |
|
84 |
85 |
85 lemma norm_is_quasinorm [intro!!]: |
86 lemma norm_is_quasinorm [intro!!]: |
86 "[| is_norm V norm; x:V |] ==> is_quasinorm V norm"; |
87 "[| is_norm V norm; x:V |] ==> is_quasinorm V norm"; |
87 by (unfold is_norm_def, force); |
88 by (unfold is_norm_def, force); |
88 |
89 |
136 finally; show "0r < norm x"; .; |
140 finally; show "0r < norm x"; .; |
137 qed; |
141 qed; |
138 |
142 |
139 lemma normed_vs_norm_mult_distrib [intro!!]: |
143 lemma normed_vs_norm_mult_distrib [intro!!]: |
140 "[| is_normed_vectorspace V norm; x:V |] |
144 "[| is_normed_vectorspace V norm; x:V |] |
141 ==> norm (a [*] x) = (rabs a) * (norm x)"; |
145 ==> norm (a <*> x) = (rabs a) * (norm x)"; |
142 by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, |
146 by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, |
143 rule normed_vs_norm); |
147 rule normed_vs_norm); |
144 |
148 |
145 lemma normed_vs_norm_triangle_ineq [intro!!]: |
149 lemma normed_vs_norm_triangle_ineq [intro!!]: |
146 "[| is_normed_vectorspace V norm; x:V; y:V |] |
150 "[| is_normed_vectorspace V norm; x:V; y:V |] |
147 ==> norm (x [+] y) <= norm x + norm y"; |
151 ==> norm (x + y) <= norm x + norm y"; |
148 by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, |
152 by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, |
149 rule normed_vs_norm); |
153 rule normed_vs_norm); |
150 |
154 |
|
155 text{* Any subspace of a normed vector space is again a |
|
156 normed vectorspace.*}; |
|
157 |
151 lemma subspace_normed_vs [intro!!]: |
158 lemma subspace_normed_vs [intro!!]: |
152 "[| is_subspace F E; is_vectorspace E; is_normed_vectorspace E norm |] |
159 "[| is_subspace F E; is_vectorspace E; |
153 ==> is_normed_vectorspace F norm"; |
160 is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"; |
154 proof (rule normed_vsI); |
161 proof (rule normed_vsI); |
155 assume "is_subspace F E" "is_vectorspace E" |
162 assume "is_subspace F E" "is_vectorspace E" |
156 "is_normed_vectorspace E norm"; |
163 "is_normed_vectorspace E norm"; |
157 show "is_vectorspace F"; ..; |
164 show "is_vectorspace F"; ..; |
158 show "is_norm F norm"; |
165 show "is_norm F norm"; |
159 proof (intro is_normI ballI conjI); |
166 proof (intro is_normI ballI conjI); |
160 show "is_quasinorm F norm"; |
167 show "is_quasinorm F norm"; |
161 proof; |
168 proof; |
162 fix x y a; presume "x : E"; |
169 fix x y a; presume "x : E"; |
163 show "0r <= norm x"; ..; |
170 show "0r <= norm x"; ..; |
164 show "norm (a [*] x) = rabs a * norm x"; ..; |
171 show "norm (a <*> x) = rabs a * norm x"; ..; |
165 presume "y : E"; |
172 presume "y : E"; |
166 show "norm (x [+] y) <= norm x + norm y"; ..; |
173 show "norm (x + y) <= norm x + norm y"; ..; |
167 qed (simp!)+; |
174 qed (simp!)+; |
168 |
175 |
169 fix x; assume "x : F"; |
176 fix x; assume "x : F"; |
170 show "(norm x = 0r) = (x = <0>)"; |
177 show "(norm x = 0r) = (x = <0>)"; |
171 proof (rule norm_zero_iff); |
178 proof (rule norm_zero_iff); |