author | wenzelm |
Fri, 22 Oct 1999 20:14:31 +0200 | |
changeset 7917 | 5e5b9813cce7 |
parent 7808 | fd019ac3485f |
child 7927 | b50446a33c16 |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/NormedSpace.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
5 |
|
7808 | 6 |
header {* Normed vector spaces *}; |
7 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
8 |
theory NormedSpace = Subspace:; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
9 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
10 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
11 |
|
7808 | 12 |
subsection {* Quasinorms *}; |
13 |
||
7917 | 14 |
text{* A \emph{quasinorm} $\norm{\cdot}$ is a function on a real vector space into the reals |
15 |
that has the following properties: *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
16 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
17 |
constdefs |
7917 | 18 |
is_quasinorm :: "['a::{plus, minus} set, 'a => real] => bool" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
19 |
"is_quasinorm V norm == ALL x: V. ALL y:V. ALL a. |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
20 |
0r <= norm x |
7917 | 21 |
& norm (a <*> x) = (rabs a) * (norm x) |
22 |
& norm (x + y) <= norm x + norm y"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
23 |
|
7808 | 24 |
lemma is_quasinormI [intro]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
25 |
"[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x; |
7917 | 26 |
!! x a. x:V ==> norm (a <*> x) = (rabs a) * (norm x); |
27 |
!! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] |
|
28 |
==> is_quasinorm V norm"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
29 |
by (unfold is_quasinorm_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
30 |
|
7566 | 31 |
lemma quasinorm_ge_zero [intro!!]: |
32 |
"[| is_quasinorm V norm; x:V |] ==> 0r <= norm x"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
33 |
by (unfold is_quasinorm_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
34 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
35 |
lemma quasinorm_mult_distrib: |
7808 | 36 |
"[| is_quasinorm V norm; x:V |] |
7917 | 37 |
==> norm (a <*> x) = (rabs a) * (norm x)"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
38 |
by (unfold is_quasinorm_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
39 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
40 |
lemma quasinorm_triangle_ineq: |
7808 | 41 |
"[| is_quasinorm V norm; x:V; y:V |] |
7917 | 42 |
==> norm (x + y) <= norm x + norm y"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
43 |
by (unfold is_quasinorm_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
44 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
45 |
lemma quasinorm_diff_triangle_ineq: |
7808 | 46 |
"[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |] |
7917 | 47 |
==> norm (x - y) <= norm x + norm y"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
48 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
49 |
assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V"; |
7917 | 50 |
have "norm (x - y) = norm (x + - 1r <*> y)"; |
51 |
by (simp! add: diff_eq2 negate_eq2); |
|
52 |
also; have "... <= norm x + norm (- 1r <*> y)"; |
|
7808 | 53 |
by (simp! add: quasinorm_triangle_ineq); |
7917 | 54 |
also; have "norm (- 1r <*> y) = rabs (- 1r) * norm y"; |
7808 | 55 |
by (rule quasinorm_mult_distrib); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
56 |
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one); |
7917 | 57 |
finally; show "norm (x - y) <= norm x + norm y"; by simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
58 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
59 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
60 |
lemma quasinorm_minus: |
7808 | 61 |
"[| is_quasinorm V norm; x:V; is_vectorspace V |] |
7917 | 62 |
==> norm (- x) = norm x"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
63 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
64 |
assume "is_quasinorm V norm" "x:V" "is_vectorspace V"; |
7917 | 65 |
have "norm (- x) = norm (-1r <*> x)"; by (simp! only: negate_eq1); |
7808 | 66 |
also; have "... = rabs (-1r) * norm x"; |
67 |
by (rule quasinorm_mult_distrib); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
68 |
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one); |
7917 | 69 |
finally; show "norm (- x) = norm x"; by simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
70 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
71 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
72 |
|
7808 | 73 |
subsection {* Norms *}; |
74 |
||
7917 | 75 |
text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only $\zero$ to $0$. *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
76 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
77 |
constdefs |
7917 | 78 |
is_norm :: "['a::{minus, plus} set, 'a => real] => bool" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
79 |
"is_norm V norm == ALL x: V. is_quasinorm V norm |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
80 |
& (norm x = 0r) = (x = <0>)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
81 |
|
7566 | 82 |
lemma is_normI [intro]: |
7808 | 83 |
"ALL x: V. is_quasinorm V norm & (norm x = 0r) = (x = <0>) |
7917 | 84 |
==> is_norm V norm"; by (simp only: is_norm_def); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
85 |
|
7808 | 86 |
lemma norm_is_quasinorm [intro!!]: |
87 |
"[| is_norm V norm; x:V |] ==> is_quasinorm V norm"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
88 |
by (unfold is_norm_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
89 |
|
7808 | 90 |
lemma norm_zero_iff: |
91 |
"[| is_norm V norm; x:V |] ==> (norm x = 0r) = (x = <0>)"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
92 |
by (unfold is_norm_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
93 |
|
7566 | 94 |
lemma norm_ge_zero [intro!!]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
95 |
"[|is_norm V norm; x:V |] ==> 0r <= norm x"; |
7566 | 96 |
by (unfold is_norm_def is_quasinorm_def, force); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
97 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
98 |
|
7808 | 99 |
subsection {* Normed vector spaces *}; |
100 |
||
7917 | 101 |
text{* A vector space together with a norm is called |
102 |
a \emph{normed space}. *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
103 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
104 |
constdefs |
7917 | 105 |
is_normed_vectorspace :: |
106 |
"['a::{plus, minus} set, 'a => real] => bool" |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
107 |
"is_normed_vectorspace V norm == |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
108 |
is_vectorspace V & |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
109 |
is_norm V norm"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
110 |
|
7566 | 111 |
lemma normed_vsI [intro]: |
7808 | 112 |
"[| is_vectorspace V; is_norm V norm |] |
113 |
==> is_normed_vectorspace V norm"; |
|
7566 | 114 |
by (unfold is_normed_vectorspace_def) blast; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
115 |
|
7808 | 116 |
lemma normed_vs_vs [intro!!]: |
117 |
"is_normed_vectorspace V norm ==> is_vectorspace V"; |
|
7566 | 118 |
by (unfold is_normed_vectorspace_def) force; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
119 |
|
7808 | 120 |
lemma normed_vs_norm [intro!!]: |
121 |
"is_normed_vectorspace V norm ==> is_norm V norm"; |
|
7566 | 122 |
by (unfold is_normed_vectorspace_def, elim conjE); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
123 |
|
7808 | 124 |
lemma normed_vs_norm_ge_zero [intro!!]: |
125 |
"[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x"; |
|
7566 | 126 |
by (unfold is_normed_vectorspace_def, rule, elim conjE); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
127 |
|
7566 | 128 |
lemma normed_vs_norm_gt_zero [intro!!]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
129 |
"[| is_normed_vectorspace V norm; x:V; x ~= <0> |] ==> 0r < norm x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
130 |
proof (unfold is_normed_vectorspace_def, elim conjE); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
131 |
assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm"; |
7566 | 132 |
have "0r <= norm x"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
133 |
also; have "0r ~= norm x"; |
7566 | 134 |
proof; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
135 |
presume "norm x = 0r"; |
7566 | 136 |
also; have "?this = (x = <0>)"; by (rule norm_zero_iff); |
137 |
finally; have "x = <0>"; .; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
138 |
thus "False"; by contradiction; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
139 |
qed (rule sym); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
140 |
finally; show "0r < norm x"; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
141 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
142 |
|
7566 | 143 |
lemma normed_vs_norm_mult_distrib [intro!!]: |
7808 | 144 |
"[| is_normed_vectorspace V norm; x:V |] |
7917 | 145 |
==> norm (a <*> x) = (rabs a) * (norm x)"; |
7808 | 146 |
by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, |
147 |
rule normed_vs_norm); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
148 |
|
7566 | 149 |
lemma normed_vs_norm_triangle_ineq [intro!!]: |
7808 | 150 |
"[| is_normed_vectorspace V norm; x:V; y:V |] |
7917 | 151 |
==> norm (x + y) <= norm x + norm y"; |
7808 | 152 |
by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, |
153 |
rule normed_vs_norm); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
154 |
|
7917 | 155 |
text{* Any subspace of a normed vector space is again a |
156 |
normed vectorspace.*}; |
|
157 |
||
7566 | 158 |
lemma subspace_normed_vs [intro!!]: |
7917 | 159 |
"[| is_subspace F E; is_vectorspace E; |
160 |
is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
161 |
proof (rule normed_vsI); |
7808 | 162 |
assume "is_subspace F E" "is_vectorspace E" |
163 |
"is_normed_vectorspace E norm"; |
|
7566 | 164 |
show "is_vectorspace F"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
165 |
show "is_norm F norm"; |
7566 | 166 |
proof (intro is_normI ballI conjI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
167 |
show "is_quasinorm F norm"; |
7566 | 168 |
proof; |
169 |
fix x y a; presume "x : E"; |
|
170 |
show "0r <= norm x"; ..; |
|
7917 | 171 |
show "norm (a <*> x) = rabs a * norm x"; ..; |
7566 | 172 |
presume "y : E"; |
7917 | 173 |
show "norm (x + y) <= norm x + norm y"; ..; |
7566 | 174 |
qed (simp!)+; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
175 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
176 |
fix x; assume "x : F"; |
7566 | 177 |
show "(norm x = 0r) = (x = <0>)"; |
178 |
proof (rule norm_zero_iff); |
|
179 |
show "is_norm E norm"; ..; |
|
180 |
qed (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
181 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
182 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
183 |
|
7808 | 184 |
end; |