author | wenzelm |
Mon, 07 Feb 2000 18:38:51 +0100 | |
changeset 8203 | 2fcc6017cb72 |
parent 7978 | 1b99ee57d131 |
child 8703 | 816d8f6513be |
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 |
||
7978 | 14 |
text{* A \emph{seminorm} $\norm{\cdot}$ is a function on a real vector |
15 |
space into the reals that has the following properties: It is positive |
|
16 |
definite, absolute homogenous and subadditive. *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
17 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
18 |
constdefs |
7978 | 19 |
is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool" |
20 |
"is_seminorm V norm == ALL x: V. ALL y:V. ALL a. |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
21 |
0r <= norm x |
7917 | 22 |
& norm (a <*> x) = (rabs a) * (norm x) |
23 |
& norm (x + y) <= norm x + norm y"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
24 |
|
7978 | 25 |
lemma is_seminormI [intro]: |
26 |
"[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x; |
|
7917 | 27 |
!! x a. x:V ==> norm (a <*> x) = (rabs a) * (norm x); |
28 |
!! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] |
|
7978 | 29 |
==> is_seminorm V norm"; |
30 |
by (unfold is_seminorm_def, force); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
31 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
32 |
lemma seminorm_ge_zero [intro??]: |
7978 | 33 |
"[| is_seminorm V norm; x:V |] ==> 0r <= norm x"; |
34 |
by (unfold is_seminorm_def, force); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
35 |
|
7978 | 36 |
lemma seminorm_rabs_homogenous: |
37 |
"[| is_seminorm V norm; x:V |] |
|
7917 | 38 |
==> norm (a <*> x) = (rabs a) * (norm x)"; |
7978 | 39 |
by (unfold is_seminorm_def, force); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
40 |
|
7978 | 41 |
lemma seminorm_subadditive: |
42 |
"[| is_seminorm V norm; x:V; y:V |] |
|
7917 | 43 |
==> norm (x + y) <= norm x + norm y"; |
7978 | 44 |
by (unfold is_seminorm_def, force); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
45 |
|
7978 | 46 |
lemma seminorm_diff_subadditive: |
47 |
"[| is_seminorm V norm; x:V; y:V; is_vectorspace V |] |
|
7917 | 48 |
==> norm (x - y) <= norm x + norm y"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
49 |
proof -; |
7978 | 50 |
assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V"; |
7917 | 51 |
have "norm (x - y) = norm (x + - 1r <*> y)"; |
52 |
by (simp! add: diff_eq2 negate_eq2); |
|
53 |
also; have "... <= norm x + norm (- 1r <*> y)"; |
|
7978 | 54 |
by (simp! add: seminorm_subadditive); |
7917 | 55 |
also; have "norm (- 1r <*> y) = rabs (- 1r) * norm y"; |
7978 | 56 |
by (rule seminorm_rabs_homogenous); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
57 |
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one); |
7917 | 58 |
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
|
59 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
60 |
|
7978 | 61 |
lemma seminorm_minus: |
62 |
"[| is_seminorm V norm; x:V; is_vectorspace V |] |
|
7917 | 63 |
==> norm (- x) = norm x"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
64 |
proof -; |
7978 | 65 |
assume "is_seminorm V norm" "x:V" "is_vectorspace V"; |
66 |
have "norm (- x) = norm (- 1r <*> x)"; by (simp! only: negate_eq1); |
|
67 |
also; have "... = rabs (- 1r) * norm x"; |
|
68 |
by (rule seminorm_rabs_homogenous); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
69 |
also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one); |
7917 | 70 |
finally; show "norm (- x) = norm x"; by simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
71 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
72 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
73 |
|
7808 | 74 |
subsection {* Norms *}; |
75 |
||
7978 | 76 |
text{* A \emph{norm} $\norm{\cdot}$ is a seminorm that maps only the |
7927 | 77 |
$\zero$ vector to $0$. *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
78 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
79 |
constdefs |
7917 | 80 |
is_norm :: "['a::{minus, plus} set, 'a => real] => bool" |
7978 | 81 |
"is_norm V norm == ALL x: V. is_seminorm V norm |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
82 |
& (norm x = 0r) = (x = <0>)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
83 |
|
7566 | 84 |
lemma is_normI [intro]: |
7978 | 85 |
"ALL x: V. is_seminorm V norm & (norm x = 0r) = (x = <0>) |
7917 | 86 |
==> 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
|
87 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
88 |
lemma norm_is_seminorm [intro??]: |
7978 | 89 |
"[| is_norm V norm; x:V |] ==> is_seminorm V norm"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
90 |
by (unfold is_norm_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
91 |
|
7808 | 92 |
lemma norm_zero_iff: |
93 |
"[| 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
|
94 |
by (unfold is_norm_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
95 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
96 |
lemma norm_ge_zero [intro??]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
97 |
"[|is_norm V norm; x:V |] ==> 0r <= norm x"; |
7978 | 98 |
by (unfold is_norm_def is_seminorm_def, force); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
99 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
100 |
|
7808 | 101 |
subsection {* Normed vector spaces *}; |
102 |
||
7917 | 103 |
text{* A vector space together with a norm is called |
104 |
a \emph{normed space}. *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
105 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
106 |
constdefs |
7917 | 107 |
is_normed_vectorspace :: |
108 |
"['a::{plus, minus} set, 'a => real] => bool" |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
109 |
"is_normed_vectorspace V norm == |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
110 |
is_vectorspace V & |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
111 |
is_norm V norm"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
112 |
|
7566 | 113 |
lemma normed_vsI [intro]: |
7808 | 114 |
"[| is_vectorspace V; is_norm V norm |] |
115 |
==> is_normed_vectorspace V norm"; |
|
7566 | 116 |
by (unfold is_normed_vectorspace_def) blast; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
117 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
118 |
lemma normed_vs_vs [intro??]: |
7808 | 119 |
"is_normed_vectorspace V norm ==> is_vectorspace V"; |
7566 | 120 |
by (unfold is_normed_vectorspace_def) force; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
121 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
122 |
lemma normed_vs_norm [intro??]: |
7808 | 123 |
"is_normed_vectorspace V norm ==> is_norm V norm"; |
7566 | 124 |
by (unfold is_normed_vectorspace_def, elim conjE); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
125 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
126 |
lemma normed_vs_norm_ge_zero [intro??]: |
7808 | 127 |
"[| is_normed_vectorspace V norm; x:V |] ==> 0r <= norm x"; |
7566 | 128 |
by (unfold is_normed_vectorspace_def, rule, elim conjE); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
129 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
130 |
lemma normed_vs_norm_gt_zero [intro??]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
131 |
"[| 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
|
132 |
proof (unfold is_normed_vectorspace_def, elim conjE); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
133 |
assume "x : V" "x ~= <0>" "is_vectorspace V" "is_norm V norm"; |
7566 | 134 |
have "0r <= norm x"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
135 |
also; have "0r ~= norm x"; |
7566 | 136 |
proof; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
137 |
presume "norm x = 0r"; |
7566 | 138 |
also; have "?this = (x = <0>)"; by (rule norm_zero_iff); |
139 |
finally; have "x = <0>"; .; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
140 |
thus "False"; by contradiction; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
141 |
qed (rule sym); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
142 |
finally; show "0r < norm x"; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
143 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
144 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
145 |
lemma normed_vs_norm_rabs_homogenous [intro??]: |
7808 | 146 |
"[| is_normed_vectorspace V norm; x:V |] |
7917 | 147 |
==> norm (a <*> x) = (rabs a) * (norm x)"; |
7978 | 148 |
by (rule seminorm_rabs_homogenous, rule norm_is_seminorm, |
7808 | 149 |
rule normed_vs_norm); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
150 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
151 |
lemma normed_vs_norm_subadditive [intro??]: |
7808 | 152 |
"[| is_normed_vectorspace V norm; x:V; y:V |] |
7917 | 153 |
==> norm (x + y) <= norm x + norm y"; |
7978 | 154 |
by (rule seminorm_subadditive, rule norm_is_seminorm, |
7808 | 155 |
rule normed_vs_norm); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
156 |
|
7917 | 157 |
text{* Any subspace of a normed vector space is again a |
158 |
normed vectorspace.*}; |
|
159 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
160 |
lemma subspace_normed_vs [intro??]: |
7917 | 161 |
"[| is_subspace F E; is_vectorspace E; |
162 |
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
|
163 |
proof (rule normed_vsI); |
7808 | 164 |
assume "is_subspace F E" "is_vectorspace E" |
165 |
"is_normed_vectorspace E norm"; |
|
7566 | 166 |
show "is_vectorspace F"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
167 |
show "is_norm F norm"; |
7566 | 168 |
proof (intro is_normI ballI conjI); |
7978 | 169 |
show "is_seminorm F norm"; |
7566 | 170 |
proof; |
171 |
fix x y a; presume "x : E"; |
|
172 |
show "0r <= norm x"; ..; |
|
7917 | 173 |
show "norm (a <*> x) = rabs a * norm x"; ..; |
7566 | 174 |
presume "y : E"; |
7917 | 175 |
show "norm (x + y) <= norm x + norm y"; ..; |
7566 | 176 |
qed (simp!)+; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
177 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
178 |
fix x; assume "x : F"; |
7566 | 179 |
show "(norm x = 0r) = (x = <0>)"; |
180 |
proof (rule norm_zero_iff); |
|
181 |
show "is_norm E norm"; ..; |
|
182 |
qed (simp!); |
|
7535
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 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
185 |
|
7808 | 186 |
end; |