author | wenzelm |
Thu, 14 Jun 2007 00:22:45 +0200 | |
changeset 23378 | 1d138d6bb461 |
parent 22931 | 11cc1ccad58e |
child 27611 | 2c01c0bdb385 |
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 |
|
16417 | 8 |
theory FunctionNorm imports NormedSpace FunctionOrder begin |
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 |
|
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14214
diff
changeset
|
26 |
declare continuous.intro [intro?] continuous_axioms.intro [intro?] |
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
14214
diff
changeset
|
27 |
|
10687 | 28 |
lemma continuousI [intro]: |
13515 | 29 |
includes norm_syntax + linearform |
30 |
assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" |
|
31 |
shows "continuous V norm f" |
|
32 |
proof |
|
23378 | 33 |
show "linearform V f" by fact |
13515 | 34 |
from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast |
35 |
then show "continuous_axioms V norm f" .. |
|
36 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
37 |
|
11472 | 38 |
|
13515 | 39 |
subsection {* The norm of a linear form *} |
7917 | 40 |
|
10687 | 41 |
text {* |
42 |
The least real number @{text c} for which holds |
|
43 |
\begin{center} |
|
11472 | 44 |
@{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
10687 | 45 |
\end{center} |
46 |
is called the \emph{norm} of @{text f}. |
|
7917 | 47 |
|
11472 | 48 |
For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be |
10687 | 49 |
defined as |
50 |
\begin{center} |
|
11472 | 51 |
@{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"} |
10687 | 52 |
\end{center} |
7917 | 53 |
|
10687 | 54 |
For the case @{text "V = {0}"} the supremum would be taken from an |
11472 | 55 |
empty set. Since @{text \<real>} is unbounded, there would be no supremum. |
10687 | 56 |
To avoid this situation it must be guaranteed that there is an |
11472 | 57 |
element in this set. This element must be @{text "{} \<ge> 0"} so that |
13547 | 58 |
@{text fn_norm} has the norm properties. Furthermore it does not |
59 |
have to change the norm in all other cases, so it must be @{text 0}, |
|
60 |
as all other elements are @{text "{} \<ge> 0"}. |
|
7917 | 61 |
|
13515 | 62 |
Thus we define the set @{text B} where the supremum is taken from as |
63 |
follows: |
|
10687 | 64 |
\begin{center} |
11472 | 65 |
@{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"} |
10687 | 66 |
\end{center} |
67 |
||
13547 | 68 |
@{text fn_norm} is equal to the supremum of @{text B}, if the |
13515 | 69 |
supremum exists (otherwise it is undefined). |
9035 | 70 |
*} |
7917 | 71 |
|
13547 | 72 |
locale fn_norm = norm_syntax + |
73 |
fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}" |
|
74 |
fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999) |
|
13515 | 75 |
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
|
76 |
|
13547 | 77 |
lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f" |
78 |
by (simp add: B_def) |
|
7917 | 79 |
|
10687 | 80 |
text {* |
81 |
The following lemma states that every continuous linear form on a |
|
11472 | 82 |
normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm. |
10687 | 83 |
*} |
84 |
||
15206
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
85 |
(* Alternative statement of the lemma as |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
86 |
lemma (in fn_norm) |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
87 |
includes normed_vectorspace + continuous |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
88 |
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
89 |
is not possible: |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
90 |
fn_norm contrains parameter norm to type "'a::zero => real", |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
91 |
normed_vectorspace and continuous contrain this parameter to |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
92 |
"'a::{minus, plus, zero} => real, which is less general. |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
93 |
*) |
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
94 |
|
09d78ec709c7
Modified locales: improved implementation of "includes".
ballarin
parents:
14710
diff
changeset
|
95 |
lemma (in normed_vectorspace) fn_norm_works: |
13547 | 96 |
includes fn_norm + continuous |
13515 | 97 |
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
98 |
proof - |
|
10687 | 99 |
txt {* The existence of the supremum is shown using the |
13515 | 100 |
completeness of the reals. Completeness means, that every |
101 |
non-empty bounded set of reals has a supremum. *} |
|
102 |
have "\<exists>a. lub (B V f) a" |
|
103 |
proof (rule real_complete) |
|
10687 | 104 |
txt {* First we have to show that @{text B} is non-empty: *} |
13515 | 105 |
have "0 \<in> B V f" .. |
106 |
thus "\<exists>x. x \<in> B V f" .. |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
107 |
|
10687 | 108 |
txt {* Then we have to show that @{text B} is bounded: *} |
13515 | 109 |
show "\<exists>c. \<forall>y \<in> B V f. y \<le> c" |
110 |
proof - |
|
10687 | 111 |
txt {* We know that @{text f} is bounded by some value @{text c}. *} |
13515 | 112 |
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
|
113 |
|
13515 | 114 |
txt {* To prove the thesis, we have to show that there is some |
115 |
@{text b}, such that @{text "y \<le> b"} for all @{text "y \<in> |
|
116 |
B"}. Due to the definition of @{text B} there are two cases. *} |
|
7917 | 117 |
|
13515 | 118 |
def b \<equiv> "max c 0" |
119 |
have "\<forall>y \<in> B V f. y \<le> b" |
|
120 |
proof |
|
121 |
fix y assume y: "y \<in> B V f" |
|
122 |
show "y \<le> b" |
|
123 |
proof cases |
|
124 |
assume "y = 0" |
|
125 |
thus ?thesis by (unfold b_def) arith |
|
126 |
next |
|
127 |
txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some |
|
128 |
@{text "x \<in> V"} with @{text "x \<noteq> 0"}. *} |
|
129 |
assume "y \<noteq> 0" |
|
130 |
with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" |
|
131 |
and x: "x \<in> V" and neq: "x \<noteq> 0" |
|
132 |
by (auto simp add: B_def real_divide_def) |
|
133 |
from x neq have gt: "0 < \<parallel>x\<parallel>" .. |
|
7917 | 134 |
|
13515 | 135 |
txt {* The thesis follows by a short calculation using the |
136 |
fact that @{text f} is bounded. *} |
|
137 |
||
138 |
note y_rep |
|
139 |
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" |
|
14334 | 140 |
proof (rule mult_right_mono) |
23378 | 141 |
from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
14334 | 142 |
from gt have "0 < inverse \<parallel>x\<parallel>" |
143 |
by (rule positive_imp_inverse_positive) |
|
13515 | 144 |
thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le) |
145 |
qed |
|
146 |
also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)" |
|
147 |
by (rule real_mult_assoc) |
|
148 |
also |
|
149 |
from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
14710 | 150 |
hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp |
13515 | 151 |
also have "c * 1 \<le> b" by (simp add: b_def le_maxI1) |
152 |
finally show "y \<le> b" . |
|
9035 | 153 |
qed |
13515 | 154 |
qed |
155 |
thus ?thesis .. |
|
9035 | 156 |
qed |
157 |
qed |
|
13547 | 158 |
then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex) |
13515 | 159 |
qed |
160 |
||
13547 | 161 |
lemma (in normed_vectorspace) fn_norm_ub [iff?]: |
162 |
includes fn_norm + continuous |
|
13515 | 163 |
assumes b: "b \<in> B V f" |
164 |
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
165 |
proof - |
|
13547 | 166 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
23378 | 167 |
unfolding B_def fn_norm_def |
168 |
using `continuous V norm f` by (rule fn_norm_works) |
|
13515 | 169 |
from this and b show ?thesis .. |
170 |
qed |
|
171 |
||
13547 | 172 |
lemma (in normed_vectorspace) fn_norm_leastB: |
173 |
includes fn_norm + continuous |
|
13515 | 174 |
assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y" |
175 |
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y" |
|
176 |
proof - |
|
13547 | 177 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
23378 | 178 |
unfolding B_def fn_norm_def |
179 |
using `continuous V norm f` by (rule fn_norm_works) |
|
13515 | 180 |
from this and b show ?thesis .. |
9035 | 181 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
182 |
|
11472 | 183 |
text {* The norm of a continuous function is always @{text "\<ge> 0"}. *} |
7917 | 184 |
|
13547 | 185 |
lemma (in normed_vectorspace) fn_norm_ge_zero [iff]: |
186 |
includes fn_norm + continuous |
|
13515 | 187 |
shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V" |
9035 | 188 |
proof - |
10687 | 189 |
txt {* The function norm is defined as the supremum of @{text B}. |
13515 | 190 |
So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge> |
191 |
0"}, provided the supremum exists and @{text B} is not empty. *} |
|
13547 | 192 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
23378 | 193 |
unfolding B_def fn_norm_def |
194 |
using `continuous V norm f` by (rule fn_norm_works) |
|
13515 | 195 |
moreover have "0 \<in> B V f" .. |
196 |
ultimately show ?thesis .. |
|
9035 | 197 |
qed |
10687 | 198 |
|
199 |
text {* |
|
200 |
\medskip The fundamental property of function norms is: |
|
201 |
\begin{center} |
|
11472 | 202 |
@{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} |
10687 | 203 |
\end{center} |
9035 | 204 |
*} |
7917 | 205 |
|
13547 | 206 |
lemma (in normed_vectorspace) fn_norm_le_cong: |
207 |
includes fn_norm + continuous + linearform |
|
13515 | 208 |
assumes x: "x \<in> V" |
209 |
shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
210 |
proof cases |
|
211 |
assume "x = 0" |
|
212 |
then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp |
|
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
213 |
also have "f 0 = 0" by rule unfold_locales |
13515 | 214 |
also have "\<bar>\<dots>\<bar> = 0" by simp |
14710 | 215 |
also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V" |
23378 | 216 |
unfolding B_def fn_norm_def |
217 |
using `continuous V norm f` by (rule fn_norm_ge_zero) |
|
218 |
from x have "0 \<le> norm x" .. |
|
14710 | 219 |
with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff) |
13515 | 220 |
finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" . |
221 |
next |
|
222 |
assume "x \<noteq> 0" |
|
223 |
with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
224 |
then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp |
|
225 |
also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
14334 | 226 |
proof (rule mult_right_mono) |
13515 | 227 |
from x show "0 \<le> \<parallel>x\<parallel>" .. |
13547 | 228 |
from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f" |
229 |
by (auto simp add: B_def real_divide_def) |
|
23378 | 230 |
with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V" |
231 |
unfolding B_def fn_norm_def by (rule fn_norm_ub) |
|
9035 | 232 |
qed |
13515 | 233 |
finally show ?thesis . |
9035 | 234 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
235 |
|
10687 | 236 |
text {* |
237 |
\medskip The function norm is the least positive real number for |
|
238 |
which the following inequation holds: |
|
239 |
\begin{center} |
|
13515 | 240 |
@{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
10687 | 241 |
\end{center} |
9035 | 242 |
*} |
7917 | 243 |
|
13547 | 244 |
lemma (in normed_vectorspace) fn_norm_least [intro?]: |
245 |
includes fn_norm + continuous |
|
13515 | 246 |
assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c" |
247 |
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c" |
|
13547 | 248 |
proof (rule fn_norm_leastB [folded B_def fn_norm_def]) |
13515 | 249 |
fix b assume b: "b \<in> B V f" |
250 |
show "b \<le> c" |
|
251 |
proof cases |
|
252 |
assume "b = 0" |
|
253 |
with ge show ?thesis by simp |
|
254 |
next |
|
255 |
assume "b \<noteq> 0" |
|
256 |
with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" |
|
257 |
and x_neq: "x \<noteq> 0" and x: "x \<in> V" |
|
258 |
by (auto simp add: B_def real_divide_def) |
|
259 |
note b_rep |
|
260 |
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" |
|
14334 | 261 |
proof (rule mult_right_mono) |
23378 | 262 |
have "0 < \<parallel>x\<parallel>" using x x_neq .. |
13515 | 263 |
then show "0 \<le> inverse \<parallel>x\<parallel>" by simp |
264 |
from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
|
265 |
qed |
|
266 |
also have "\<dots> = c" |
|
267 |
proof - |
|
268 |
from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
269 |
then show ?thesis by simp |
|
270 |
qed |
|
271 |
finally show ?thesis . |
|
9035 | 272 |
qed |
22931 | 273 |
qed (insert `continuous V norm f`, simp_all add: continuous_def) |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
274 |
|
10687 | 275 |
end |