author | wenzelm |
Mon, 25 Oct 1999 19:24:43 +0200 | |
changeset 7927 | b50446a33c16 |
parent 7917 | 5e5b9813cce7 |
child 7978 | 1b99ee57d131 |
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 |
||
7927 | 75 |
text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only the |
76 |
$\zero$ vector to $0$. *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
77 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
78 |
constdefs |
7917 | 79 |
is_norm :: "['a::{minus, plus} set, 'a => real] => bool" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
80 |
"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
|
81 |
& (norm x = 0r) = (x = <0>)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
82 |
|
7566 | 83 |
lemma is_normI [intro]: |
7808 | 84 |
"ALL x: V. is_quasinorm V norm & (norm x = 0r) = (x = <0>) |
7917 | 85 |
==> 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
|
86 |
|
7808 | 87 |
lemma norm_is_quasinorm [intro!!]: |
88 |
"[| 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
|
89 |
by (unfold is_norm_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
90 |
|
7808 | 91 |
lemma norm_zero_iff: |
92 |
"[| 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
|
93 |
by (unfold is_norm_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
94 |
|
7566 | 95 |
lemma norm_ge_zero [intro!!]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
96 |
"[|is_norm V norm; x:V |] ==> 0r <= norm x"; |
7566 | 97 |
by (unfold is_norm_def is_quasinorm_def, force); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
98 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
99 |
|
7808 | 100 |
subsection {* Normed vector spaces *}; |
101 |
||
7917 | 102 |
text{* A vector space together with a norm is called |
103 |
a \emph{normed space}. *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
104 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
105 |
constdefs |
7917 | 106 |
is_normed_vectorspace :: |
107 |
"['a::{plus, minus} set, 'a => real] => bool" |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
108 |
"is_normed_vectorspace V norm == |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
109 |
is_vectorspace V & |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
110 |
is_norm V norm"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
111 |
|
7566 | 112 |
lemma normed_vsI [intro]: |
7808 | 113 |
"[| is_vectorspace V; is_norm V norm |] |
114 |
==> is_normed_vectorspace V norm"; |
|
7566 | 115 |
by (unfold is_normed_vectorspace_def) blast; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
116 |
|
7808 | 117 |
lemma normed_vs_vs [intro!!]: |
118 |
"is_normed_vectorspace V norm ==> is_vectorspace V"; |
|
7566 | 119 |
by (unfold is_normed_vectorspace_def) force; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
120 |
|
7808 | 121 |
lemma normed_vs_norm [intro!!]: |
122 |
"is_normed_vectorspace V norm ==> is_norm V norm"; |
|
7566 | 123 |
by (unfold is_normed_vectorspace_def, elim conjE); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
124 |
|
7808 | 125 |
lemma normed_vs_norm_ge_zero [intro!!]: |
126 |
"[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x"; |
|
7566 | 127 |
by (unfold is_normed_vectorspace_def, rule, elim conjE); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
128 |
|
7566 | 129 |
lemma normed_vs_norm_gt_zero [intro!!]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
130 |
"[| 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
|
131 |
proof (unfold is_normed_vectorspace_def, elim conjE); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
132 |
assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm"; |
7566 | 133 |
have "0r <= norm x"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
134 |
also; have "0r ~= norm x"; |
7566 | 135 |
proof; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
136 |
presume "norm x = 0r"; |
7566 | 137 |
also; have "?this = (x = <0>)"; by (rule norm_zero_iff); |
138 |
finally; have "x = <0>"; .; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
139 |
thus "False"; by contradiction; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
140 |
qed (rule sym); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
141 |
finally; show "0r < norm x"; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
142 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
143 |
|
7566 | 144 |
lemma normed_vs_norm_mult_distrib [intro!!]: |
7808 | 145 |
"[| is_normed_vectorspace V norm; x:V |] |
7917 | 146 |
==> norm (a <*> x) = (rabs a) * (norm x)"; |
7808 | 147 |
by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, |
148 |
rule normed_vs_norm); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
149 |
|
7566 | 150 |
lemma normed_vs_norm_triangle_ineq [intro!!]: |
7808 | 151 |
"[| is_normed_vectorspace V norm; x:V; y:V |] |
7917 | 152 |
==> norm (x + y) <= norm x + norm y"; |
7808 | 153 |
by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, |
154 |
rule normed_vs_norm); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
155 |
|
7917 | 156 |
text{* Any subspace of a normed vector space is again a |
157 |
normed vectorspace.*}; |
|
158 |
||
7566 | 159 |
lemma subspace_normed_vs [intro!!]: |
7917 | 160 |
"[| is_subspace F E; is_vectorspace E; |
161 |
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
|
162 |
proof (rule normed_vsI); |
7808 | 163 |
assume "is_subspace F E" "is_vectorspace E" |
164 |
"is_normed_vectorspace E norm"; |
|
7566 | 165 |
show "is_vectorspace F"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
166 |
show "is_norm F norm"; |
7566 | 167 |
proof (intro is_normI ballI conjI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
168 |
show "is_quasinorm F norm"; |
7566 | 169 |
proof; |
170 |
fix x y a; presume "x : E"; |
|
171 |
show "0r <= norm x"; ..; |
|
7917 | 172 |
show "norm (a <*> x) = rabs a * norm x"; ..; |
7566 | 173 |
presume "y : E"; |
7917 | 174 |
show "norm (x + y) <= norm x + norm y"; ..; |
7566 | 175 |
qed (simp!)+; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
176 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
177 |
fix x; assume "x : F"; |
7566 | 178 |
show "(norm x = 0r) = (x = <0>)"; |
179 |
proof (rule norm_zero_iff); |
|
180 |
show "is_norm E norm"; ..; |
|
181 |
qed (simp!); |
|
7535
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 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
184 |
|
7808 | 185 |
end; |