author | wenzelm |
Tue, 27 Aug 2002 11:03:05 +0200 | |
changeset 13524 | 604d0f3622d6 |
parent 13515 | a6a7025fd7e8 |
child 13547 | bf399f3bd7dc |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/FunctionNorm.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 |
|
9035 | 6 |
header {* The norm of a function *} |
7808 | 7 |
|
9035 | 8 |
theory FunctionNorm = NormedSpace + FunctionOrder: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
9 |
|
9035 | 10 |
subsection {* Continuous linear forms*} |
7917 | 11 |
|
10687 | 12 |
text {* |
11472 | 13 |
A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"} |
13515 | 14 |
is \emph{continuous}, iff it is bounded, i.e. |
10687 | 15 |
\begin{center} |
11472 | 16 |
@{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
10687 | 17 |
\end{center} |
18 |
In our application no other functions than linear forms are |
|
19 |
considered, so we can define continuous linear forms as bounded |
|
20 |
linear forms: |
|
9035 | 21 |
*} |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
|
13515 | 23 |
locale continuous = var V + norm_syntax + linearform + |
24 |
assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
25 |
|
10687 | 26 |
lemma continuousI [intro]: |
13515 | 27 |
includes norm_syntax + linearform |
28 |
assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
|
29 |
shows "continuous V norm f" |
|
30 |
proof |
|
31 |
show "linearform V f" . |
|
32 |
from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast |
|
33 |
then show "continuous_axioms V norm f" .. |
|
34 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
35 |
|
11472 | 36 |
|
13515 | 37 |
subsection {* The norm of a linear form *} |
7917 | 38 |
|
10687 | 39 |
text {* |
40 |
The least real number @{text c} for which holds |
|
41 |
\begin{center} |
|
11472 | 42 |
@{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
10687 | 43 |
\end{center} |
44 |
is called the \emph{norm} of @{text f}. |
|
7917 | 45 |
|
11472 | 46 |
For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be |
10687 | 47 |
defined as |
48 |
\begin{center} |
|
11472 | 49 |
@{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"} |
10687 | 50 |
\end{center} |
7917 | 51 |
|
10687 | 52 |
For the case @{text "V = {0}"} the supremum would be taken from an |
11472 | 53 |
empty set. Since @{text \<real>} is unbounded, there would be no supremum. |
10687 | 54 |
To avoid this situation it must be guaranteed that there is an |
11472 | 55 |
element in this set. This element must be @{text "{} \<ge> 0"} so that |
10687 | 56 |
@{text function_norm} has the norm properties. Furthermore |
57 |
it does not have to change the norm in all other cases, so it must |
|
13515 | 58 |
be @{text 0}, as all other elements are @{text "{} \<ge> 0"}. |
7917 | 59 |
|
13515 | 60 |
Thus we define the set @{text B} where the supremum is taken from as |
61 |
follows: |
|
10687 | 62 |
\begin{center} |
11472 | 63 |
@{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"} |
10687 | 64 |
\end{center} |
65 |
||
13515 | 66 |
@{text function_norm} is equal to the supremum of @{text B}, if the |
67 |
supremum exists (otherwise it is undefined). |
|
9035 | 68 |
*} |
7917 | 69 |
|
13515 | 70 |
locale function_norm = norm_syntax + |
71 |
fixes B |
|
72 |
defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}" |
|
73 |
fixes function_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999) |
|
74 |
defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)" |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
75 |
|
13515 | 76 |
lemma (in function_norm) B_not_empty [intro]: "0 \<in> B V f" |
77 |
by (unfold B_def) simp |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
78 |
|
13515 | 79 |
locale (open) functional_vectorspace = |
80 |
normed_vectorspace + function_norm + |
|
81 |
fixes cont |
|
82 |
defines "cont f \<equiv> continuous V norm f" |
|
7917 | 83 |
|
10687 | 84 |
text {* |
85 |
The following lemma states that every continuous linear form on a |
|
11472 | 86 |
normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm. |
10687 | 87 |
*} |
88 |
||
13515 | 89 |
lemma (in functional_vectorspace) function_norm_works: |
90 |
includes continuous |
|
91 |
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
|
92 |
proof - |
|
10687 | 93 |
txt {* The existence of the supremum is shown using the |
13515 | 94 |
completeness of the reals. Completeness means, that every |
95 |
non-empty bounded set of reals has a supremum. *} |
|
96 |
have "\<exists>a. lub (B V f) a" |
|
97 |
proof (rule real_complete) |
|
10687 | 98 |
txt {* First we have to show that @{text B} is non-empty: *} |
13515 | 99 |
have "0 \<in> B V f" .. |
100 |
thus "\<exists>x. x \<in> B V f" .. |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
101 |
|
10687 | 102 |
txt {* Then we have to show that @{text B} is bounded: *} |
13515 | 103 |
show "\<exists>c. \<forall>y \<in> B V f. y \<le> c" |
104 |
proof - |
|
10687 | 105 |
txt {* We know that @{text f} is bounded by some value @{text c}. *} |
13515 | 106 |
from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
107 |
|
13515 | 108 |
txt {* To prove the thesis, we have to show that there is some |
109 |
@{text b}, such that @{text "y \<le> b"} for all @{text "y \<in> |
|
110 |
B"}. Due to the definition of @{text B} there are two cases. *} |
|
7917 | 111 |
|
13515 | 112 |
def b \<equiv> "max c 0" |
113 |
have "\<forall>y \<in> B V f. y \<le> b" |
|
114 |
proof |
|
115 |
fix y assume y: "y \<in> B V f" |
|
116 |
show "y \<le> b" |
|
117 |
proof cases |
|
118 |
assume "y = 0" |
|
119 |
thus ?thesis by (unfold b_def) arith |
|
120 |
next |
|
121 |
txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some |
|
122 |
@{text "x \<in> V"} with @{text "x \<noteq> 0"}. *} |
|
123 |
assume "y \<noteq> 0" |
|
124 |
with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" |
|
125 |
and x: "x \<in> V" and neq: "x \<noteq> 0" |
|
126 |
by (auto simp add: B_def real_divide_def) |
|
127 |
from x neq have gt: "0 < \<parallel>x\<parallel>" .. |
|
7917 | 128 |
|
13515 | 129 |
txt {* The thesis follows by a short calculation using the |
130 |
fact that @{text f} is bounded. *} |
|
131 |
||
132 |
note y_rep |
|
133 |
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" |
|
134 |
proof (rule real_mult_le_le_mono2) |
|
135 |
from c show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
|
136 |
from gt have "0 < inverse \<parallel>x\<parallel>" by (rule real_inverse_gt_0) |
|
137 |
thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le) |
|
138 |
qed |
|
139 |
also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)" |
|
140 |
by (rule real_mult_assoc) |
|
141 |
also |
|
142 |
from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
143 |
hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by (simp add: real_mult_inv_right1) |
|
144 |
also have "c * 1 \<le> b" by (simp add: b_def le_maxI1) |
|
145 |
finally show "y \<le> b" . |
|
9035 | 146 |
qed |
13515 | 147 |
qed |
148 |
thus ?thesis .. |
|
9035 | 149 |
qed |
150 |
qed |
|
13515 | 151 |
then show ?thesis |
152 |
by (unfold function_norm_def) (rule the_lubI_ex) |
|
153 |
qed |
|
154 |
||
155 |
lemma (in functional_vectorspace) function_norm_ub [intro?]: |
|
156 |
includes continuous |
|
157 |
assumes b: "b \<in> B V f" |
|
158 |
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
159 |
proof - |
|
160 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works) |
|
161 |
from this and b show ?thesis .. |
|
162 |
qed |
|
163 |
||
13524 | 164 |
lemma (in functional_vectorspace) function_norm_least' [intro?]: |
13515 | 165 |
includes continuous |
166 |
assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y" |
|
167 |
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y" |
|
168 |
proof - |
|
169 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works) |
|
170 |
from this and b show ?thesis .. |
|
9035 | 171 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
172 |
|
11472 | 173 |
text {* The norm of a continuous function is always @{text "\<ge> 0"}. *} |
7917 | 174 |
|
13515 | 175 |
lemma (in functional_vectorspace) function_norm_ge_zero [iff]: |
176 |
includes continuous |
|
177 |
shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
9035 | 178 |
proof - |
10687 | 179 |
txt {* The function norm is defined as the supremum of @{text B}. |
13515 | 180 |
So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge> |
181 |
0"}, provided the supremum exists and @{text B} is not empty. *} |
|
182 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works) |
|
183 |
moreover have "0 \<in> B V f" .. |
|
184 |
ultimately show ?thesis .. |
|
9035 | 185 |
qed |
10687 | 186 |
|
187 |
text {* |
|
188 |
\medskip The fundamental property of function norms is: |
|
189 |
\begin{center} |
|
11472 | 190 |
@{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} |
10687 | 191 |
\end{center} |
9035 | 192 |
*} |
7917 | 193 |
|
13515 | 194 |
lemma (in functional_vectorspace) function_norm_le_cong: |
195 |
includes continuous + vectorspace_linearform |
|
196 |
assumes x: "x \<in> V" |
|
197 |
shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
198 |
proof cases |
|
199 |
assume "x = 0" |
|
200 |
then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp |
|
201 |
also have "f 0 = 0" .. |
|
202 |
also have "\<bar>\<dots>\<bar> = 0" by simp |
|
203 |
also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
204 |
proof (rule real_le_mult_order1a) |
|
205 |
show "0 \<le> \<parallel>f\<parallel>\<hyphen>V" .. |
|
206 |
show "0 \<le> norm x" .. |
|
207 |
qed |
|
208 |
finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" . |
|
209 |
next |
|
210 |
assume "x \<noteq> 0" |
|
211 |
with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
212 |
then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp |
|
213 |
also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
214 |
proof (rule real_mult_le_le_mono2) |
|
215 |
from x show "0 \<le> \<parallel>x\<parallel>" .. |
|
216 |
show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
217 |
proof |
|
218 |
from x and neq show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f" |
|
219 |
by (auto simp add: B_def real_divide_def) |
|
9035 | 220 |
qed |
221 |
qed |
|
13515 | 222 |
finally show ?thesis . |
9035 | 223 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
224 |
|
10687 | 225 |
text {* |
226 |
\medskip The function norm is the least positive real number for |
|
227 |
which the following inequation holds: |
|
228 |
\begin{center} |
|
13515 | 229 |
@{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
10687 | 230 |
\end{center} |
9035 | 231 |
*} |
7917 | 232 |
|
13515 | 233 |
lemma (in functional_vectorspace) function_norm_least [intro?]: |
234 |
includes continuous |
|
235 |
assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c" |
|
236 |
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c" |
|
13524 | 237 |
proof (rule function_norm_least') |
13515 | 238 |
fix b assume b: "b \<in> B V f" |
239 |
show "b \<le> c" |
|
240 |
proof cases |
|
241 |
assume "b = 0" |
|
242 |
with ge show ?thesis by simp |
|
243 |
next |
|
244 |
assume "b \<noteq> 0" |
|
245 |
with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" |
|
246 |
and x_neq: "x \<noteq> 0" and x: "x \<in> V" |
|
247 |
by (auto simp add: B_def real_divide_def) |
|
248 |
note b_rep |
|
249 |
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" |
|
250 |
proof (rule real_mult_le_le_mono2) |
|
251 |
have "0 < \<parallel>x\<parallel>" .. |
|
252 |
then show "0 \<le> inverse \<parallel>x\<parallel>" by simp |
|
253 |
from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
|
254 |
qed |
|
255 |
also have "\<dots> = c" |
|
256 |
proof - |
|
257 |
from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
258 |
then show ?thesis by simp |
|
259 |
qed |
|
260 |
finally show ?thesis . |
|
9035 | 261 |
qed |
262 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
263 |
|
13515 | 264 |
lemmas [iff?] = |
265 |
functional_vectorspace.function_norm_ge_zero |
|
266 |
functional_vectorspace.function_norm_le_cong |
|
267 |
functional_vectorspace.function_norm_least |
|
268 |
||
10687 | 269 |
end |