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