author | bauerg |
Fri, 07 May 2004 12:16:57 +0200 | |
changeset 14710 | 247615bfffb8 |
parent 14334 | 6137d24eef79 |
child 15206 | 09d78ec709c7 |
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 |
|
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 |
|
33 |
show "linearform V f" . |
|
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 |
||
13547 | 85 |
lemma (in normed_vectorspace) fn_norm_works: (* FIXME bug with "(in fn_norm)" !? *) |
86 |
includes fn_norm + continuous |
|
13515 | 87 |
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
88 |
proof - |
|
10687 | 89 |
txt {* The existence of the supremum is shown using the |
13515 | 90 |
completeness of the reals. Completeness means, that every |
91 |
non-empty bounded set of reals has a supremum. *} |
|
92 |
have "\<exists>a. lub (B V f) a" |
|
93 |
proof (rule real_complete) |
|
10687 | 94 |
txt {* First we have to show that @{text B} is non-empty: *} |
13515 | 95 |
have "0 \<in> B V f" .. |
96 |
thus "\<exists>x. x \<in> B V f" .. |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
97 |
|
10687 | 98 |
txt {* Then we have to show that @{text B} is bounded: *} |
13515 | 99 |
show "\<exists>c. \<forall>y \<in> B V f. y \<le> c" |
100 |
proof - |
|
10687 | 101 |
txt {* We know that @{text f} is bounded by some value @{text c}. *} |
13515 | 102 |
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
|
103 |
|
13515 | 104 |
txt {* To prove the thesis, we have to show that there is some |
105 |
@{text b}, such that @{text "y \<le> b"} for all @{text "y \<in> |
|
106 |
B"}. Due to the definition of @{text B} there are two cases. *} |
|
7917 | 107 |
|
13515 | 108 |
def b \<equiv> "max c 0" |
109 |
have "\<forall>y \<in> B V f. y \<le> b" |
|
110 |
proof |
|
111 |
fix y assume y: "y \<in> B V f" |
|
112 |
show "y \<le> b" |
|
113 |
proof cases |
|
114 |
assume "y = 0" |
|
115 |
thus ?thesis by (unfold b_def) arith |
|
116 |
next |
|
117 |
txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some |
|
118 |
@{text "x \<in> V"} with @{text "x \<noteq> 0"}. *} |
|
119 |
assume "y \<noteq> 0" |
|
120 |
with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" |
|
121 |
and x: "x \<in> V" and neq: "x \<noteq> 0" |
|
122 |
by (auto simp add: B_def real_divide_def) |
|
123 |
from x neq have gt: "0 < \<parallel>x\<parallel>" .. |
|
7917 | 124 |
|
13515 | 125 |
txt {* The thesis follows by a short calculation using the |
126 |
fact that @{text f} is bounded. *} |
|
127 |
||
128 |
note y_rep |
|
129 |
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" |
|
14334 | 130 |
proof (rule mult_right_mono) |
13515 | 131 |
from c show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
14334 | 132 |
from gt have "0 < inverse \<parallel>x\<parallel>" |
133 |
by (rule positive_imp_inverse_positive) |
|
13515 | 134 |
thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le) |
135 |
qed |
|
136 |
also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)" |
|
137 |
by (rule real_mult_assoc) |
|
138 |
also |
|
139 |
from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
14710 | 140 |
hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp |
13515 | 141 |
also have "c * 1 \<le> b" by (simp add: b_def le_maxI1) |
142 |
finally show "y \<le> b" . |
|
9035 | 143 |
qed |
13515 | 144 |
qed |
145 |
thus ?thesis .. |
|
9035 | 146 |
qed |
147 |
qed |
|
13547 | 148 |
then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex) |
13515 | 149 |
qed |
150 |
||
13547 | 151 |
lemma (in normed_vectorspace) fn_norm_ub [iff?]: |
152 |
includes fn_norm + continuous |
|
13515 | 153 |
assumes b: "b \<in> B V f" |
154 |
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
155 |
proof - |
|
13547 | 156 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
157 |
by (unfold B_def fn_norm_def) (rule fn_norm_works [OF _ continuous.intro]) |
13515 | 158 |
from this and b show ?thesis .. |
159 |
qed |
|
160 |
||
13547 | 161 |
lemma (in normed_vectorspace) fn_norm_leastB: |
162 |
includes fn_norm + continuous |
|
13515 | 163 |
assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y" |
164 |
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y" |
|
165 |
proof - |
|
13547 | 166 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
167 |
by (unfold B_def fn_norm_def) (rule fn_norm_works [OF _ continuous.intro]) |
13515 | 168 |
from this and b show ?thesis .. |
9035 | 169 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
170 |
|
11472 | 171 |
text {* The norm of a continuous function is always @{text "\<ge> 0"}. *} |
7917 | 172 |
|
13547 | 173 |
lemma (in normed_vectorspace) fn_norm_ge_zero [iff]: |
174 |
includes fn_norm + continuous |
|
13515 | 175 |
shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V" |
9035 | 176 |
proof - |
10687 | 177 |
txt {* The function norm is defined as the supremum of @{text B}. |
13515 | 178 |
So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge> |
179 |
0"}, provided the supremum exists and @{text B} is not empty. *} |
|
13547 | 180 |
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" |
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
181 |
by (unfold B_def fn_norm_def) (rule fn_norm_works [OF _ continuous.intro]) |
13515 | 182 |
moreover have "0 \<in> B V f" .. |
183 |
ultimately show ?thesis .. |
|
9035 | 184 |
qed |
10687 | 185 |
|
186 |
text {* |
|
187 |
\medskip The fundamental property of function norms is: |
|
188 |
\begin{center} |
|
11472 | 189 |
@{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} |
10687 | 190 |
\end{center} |
9035 | 191 |
*} |
7917 | 192 |
|
13547 | 193 |
lemma (in normed_vectorspace) fn_norm_le_cong: |
194 |
includes fn_norm + continuous + linearform |
|
13515 | 195 |
assumes x: "x \<in> V" |
196 |
shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
197 |
proof cases |
|
198 |
assume "x = 0" |
|
199 |
then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp |
|
200 |
also have "f 0 = 0" .. |
|
201 |
also have "\<bar>\<dots>\<bar> = 0" by simp |
|
14710 | 202 |
also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V" |
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
203 |
by (unfold B_def fn_norm_def) |
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
204 |
(rule fn_norm_ge_zero [OF _ continuous.intro]) |
14710 | 205 |
have "0 \<le> norm x" .. |
206 |
with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff) |
|
13515 | 207 |
finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" . |
208 |
next |
|
209 |
assume "x \<noteq> 0" |
|
210 |
with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
211 |
then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp |
|
212 |
also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" |
|
14334 | 213 |
proof (rule mult_right_mono) |
13515 | 214 |
from x show "0 \<le> \<parallel>x\<parallel>" .. |
13547 | 215 |
from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f" |
216 |
by (auto simp add: B_def real_divide_def) |
|
217 |
then show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V" |
|
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
218 |
by (unfold B_def fn_norm_def) (rule fn_norm_ub [OF _ continuous.intro]) |
9035 | 219 |
qed |
13515 | 220 |
finally show ?thesis . |
9035 | 221 |
qed |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
222 |
|
10687 | 223 |
text {* |
224 |
\medskip The function norm is the least positive real number for |
|
225 |
which the following inequation holds: |
|
226 |
\begin{center} |
|
13515 | 227 |
@{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} |
10687 | 228 |
\end{center} |
9035 | 229 |
*} |
7917 | 230 |
|
13547 | 231 |
lemma (in normed_vectorspace) fn_norm_least [intro?]: |
232 |
includes fn_norm + continuous |
|
13515 | 233 |
assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c" |
234 |
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c" |
|
13547 | 235 |
proof (rule fn_norm_leastB [folded B_def fn_norm_def]) |
13515 | 236 |
fix b assume b: "b \<in> B V f" |
237 |
show "b \<le> c" |
|
238 |
proof cases |
|
239 |
assume "b = 0" |
|
240 |
with ge show ?thesis by simp |
|
241 |
next |
|
242 |
assume "b \<noteq> 0" |
|
243 |
with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" |
|
244 |
and x_neq: "x \<noteq> 0" and x: "x \<in> V" |
|
245 |
by (auto simp add: B_def real_divide_def) |
|
246 |
note b_rep |
|
247 |
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" |
|
14334 | 248 |
proof (rule mult_right_mono) |
13515 | 249 |
have "0 < \<parallel>x\<parallel>" .. |
250 |
then show "0 \<le> inverse \<parallel>x\<parallel>" by simp |
|
251 |
from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. |
|
252 |
qed |
|
253 |
also have "\<dots> = c" |
|
254 |
proof - |
|
255 |
from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp |
|
256 |
then show ?thesis by simp |
|
257 |
qed |
|
258 |
finally show ?thesis . |
|
9035 | 259 |
qed |
14214
5369d671f100
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
13547
diff
changeset
|
260 |
qed (simp_all! add: continuous_def) |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
261 |
|
10687 | 262 |
end |