author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46867  0883804b67bb 
child 50918  3b6417e9f73e 
permissions  rwrr 
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset

1 
(* Title: HOL/Hahn_Banach/Function_Norm.thy 
7566  2 
Author: Gertrud Bauer, TU Munich 
3 
*) 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

4 

9035  5 
header {* The norm of a function *} 
7808  6 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset

7 
theory Function_Norm 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29291
diff
changeset

8 
imports Normed_Space Function_Order 
27612  9 
begin 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

10 

9035  11 
subsection {* Continuous linear forms*} 
7917  12 

10687  13 
text {* 
11472  14 
A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"} 
13515  15 
is \emph{continuous}, iff it is bounded, i.e. 
10687  16 
\begin{center} 
11472  17 
@{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} 
10687  18 
\end{center} 
19 
In our application no other functions than linear forms are 

20 
considered, so we can define continuous linear forms as bounded 

21 
linear forms: 

9035  22 
*} 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

23 

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

24 
locale continuous = linearform + 
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

25 
fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>") 
13515  26 
assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" 
7535
599d3414b51d
The HahnBanach 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>" 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

34 
shows "continuous V f norm" 
13515  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 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

38 
then show "continuous_axioms V f norm" .. 
13515  39 
qed 
7535
599d3414b51d
The HahnBanach 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 nontrivial 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 

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

75 
locale fn_norm = 
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

76 
fixes norm :: "_ \<Rightarrow> real" ("\<parallel>_\<parallel>") 
13547  77 
fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>  x. x \<noteq> 0 \<and> x \<in> V}" 
78 
fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999) 

13515  79 
defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)" 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

80 

27611  81 
locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm 
82 

13547  83 
lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f" 
84 
by (simp add: B_def) 

7917  85 

10687  86 
text {* 
87 
The following lemma states that every continuous linear form on a 

11472  88 
normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm. 
10687  89 
*} 
90 

27611  91 
lemma (in normed_vectorspace_with_fn_norm) fn_norm_works: 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

92 
assumes "continuous V f norm" 
13515  93 
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 
94 
proof  

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

95 
interpret continuous V f norm by fact 
10687  96 
txt {* The existence of the supremum is shown using the 
13515  97 
completeness of the reals. Completeness means, that every 
98 
nonempty bounded set of reals has a supremum. *} 

99 
have "\<exists>a. lub (B V f) a" 

100 
proof (rule real_complete) 

10687  101 
txt {* First we have to show that @{text B} is nonempty: *} 
13515  102 
have "0 \<in> B V f" .. 
27612  103 
then show "\<exists>x. x \<in> B V f" .. 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

104 

10687  105 
txt {* Then we have to show that @{text B} is bounded: *} 
13515  106 
show "\<exists>c. \<forall>y \<in> B V f. y \<le> c" 
107 
proof  

10687  108 
txt {* We know that @{text f} is bounded by some value @{text c}. *} 
13515  109 
from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

110 

13515  111 
txt {* To prove the thesis, we have to show that there is some 
112 
@{text b}, such that @{text "y \<le> b"} for all @{text "y \<in> 

113 
B"}. Due to the definition of @{text B} there are two cases. *} 

7917  114 

13515  115 
def b \<equiv> "max c 0" 
116 
have "\<forall>y \<in> B V f. y \<le> b" 

117 
proof 

118 
fix y assume y: "y \<in> B V f" 

119 
show "y \<le> b" 

120 
proof cases 

121 
assume "y = 0" 

27612  122 
then show ?thesis unfolding b_def by arith 
13515  123 
next 
124 
txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some 

125 
@{text "x \<in> V"} with @{text "x \<noteq> 0"}. *} 

126 
assume "y \<noteq> 0" 

127 
with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" 

128 
and x: "x \<in> V" and neq: "x \<noteq> 0" 

36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
32960
diff
changeset

129 
by (auto simp add: B_def divide_inverse) 
13515  130 
from x neq have gt: "0 < \<parallel>x\<parallel>" .. 
7917  131 

13515  132 
txt {* The thesis follows by a short calculation using the 
133 
fact that @{text f} is bounded. *} 

134 

135 
note y_rep 

136 
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" 

14334  137 
proof (rule mult_right_mono) 
23378  138 
from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. 
14334  139 
from gt have "0 < inverse \<parallel>x\<parallel>" 
140 
by (rule positive_imp_inverse_positive) 

27612  141 
then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le) 
13515  142 
qed 
143 
also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)" 

36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
32960
diff
changeset

144 
by (rule Groups.mult_assoc) 
13515  145 
also 
146 
from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp 

27612  147 
then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 
44887  148 
also have "c * 1 \<le> b" by (simp add: b_def) 
13515  149 
finally show "y \<le> b" . 
9035  150 
qed 
13515  151 
qed 
27612  152 
then show ?thesis .. 
9035  153 
qed 
154 
qed 

27612  155 
then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex) 
13515  156 
qed 
157 

27611  158 
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]: 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

159 
assumes "continuous V f norm" 
13515  160 
assumes b: "b \<in> B V f" 
161 
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V" 

162 
proof  

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

163 
interpret continuous V f norm by fact 
13547  164 
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

165 
using `continuous V f norm` by (rule fn_norm_works) 
13515  166 
from this and b show ?thesis .. 
167 
qed 

168 

27611  169 
lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB: 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

170 
assumes "continuous V f norm" 
13515  171 
assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y" 
172 
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y" 

173 
proof  

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

174 
interpret continuous V f norm by fact 
13547  175 
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

176 
using `continuous V f norm` by (rule fn_norm_works) 
13515  177 
from this and b show ?thesis .. 
9035  178 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

179 

11472  180 
text {* The norm of a continuous function is always @{text "\<ge> 0"}. *} 
7917  181 

27611  182 
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]: 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

183 
assumes "continuous V f norm" 
13515  184 
shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V" 
9035  185 
proof  
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

186 
interpret continuous V f norm by fact 
10687  187 
txt {* The function norm is defined as the supremum of @{text B}. 
13515  188 
So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge> 
189 
0"}, provided the supremum exists and @{text B} is not empty. *} 

13547  190 
have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

191 
using `continuous V f norm` by (rule fn_norm_works) 
13515  192 
moreover have "0 \<in> B V f" .. 
193 
ultimately show ?thesis .. 

9035  194 
qed 
10687  195 

196 
text {* 

197 
\medskip The fundamental property of function norms is: 

198 
\begin{center} 

11472  199 
@{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} 
10687  200 
\end{center} 
9035  201 
*} 
7917  202 

27611  203 
lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong: 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

204 
assumes "continuous V f norm" "linearform V f" 
13515  205 
assumes x: "x \<in> V" 
206 
shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" 

27611  207 
proof  
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

208 
interpret continuous V f norm by fact 
29291  209 
interpret linearform V f by fact 
27612  210 
show ?thesis 
211 
proof cases 

27611  212 
assume "x = 0" 
213 
then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp 

214 
also have "f 0 = 0" by rule unfold_locales 

215 
also have "\<bar>\<dots>\<bar> = 0" by simp 

216 
also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V" 

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

217 
using `continuous V f norm` by (rule fn_norm_ge_zero) 
27611  218 
from x have "0 \<le> norm x" .. 
219 
with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff) 

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>" 

226 
proof (rule mult_right_mono) 

227 
from x show "0 \<le> \<parallel>x\<parallel>" .. 

228 
from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f" 

36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
32960
diff
changeset

229 
by (auto simp add: B_def divide_inverse) 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

230 
with `continuous V f norm` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

231 
by (rule fn_norm_ub) 
27611  232 
qed 
233 
finally show ?thesis . 

9035  234 
qed 
235 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

236 

10687  237 
text {* 
238 
\medskip The function norm is the least positive real number for 

239 
which the following inequation holds: 

240 
\begin{center} 

13515  241 
@{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"} 
10687  242 
\end{center} 
9035  243 
*} 
7917  244 

27611  245 
lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]: 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

246 
assumes "continuous V f norm" 
13515  247 
assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c" 
248 
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c" 

27611  249 
proof  
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

250 
interpret continuous V f norm by fact 
27612  251 
show ?thesis 
252 
proof (rule fn_norm_leastB [folded B_def fn_norm_def]) 

27611  253 
fix b assume b: "b \<in> B V f" 
254 
show "b \<le> c" 

255 
proof cases 

256 
assume "b = 0" 

257 
with ge show ?thesis by simp 

258 
next 

259 
assume "b \<noteq> 0" 

260 
with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>" 

13515  261 
and x_neq: "x \<noteq> 0" and x: "x \<in> V" 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
32960
diff
changeset

262 
by (auto simp add: B_def divide_inverse) 
27611  263 
note b_rep 
264 
also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>" 

265 
proof (rule mult_right_mono) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

266 
have "0 < \<parallel>x\<parallel>" using x x_neq .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

267 
then show "0 \<le> inverse \<parallel>x\<parallel>" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

268 
from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" .. 
27611  269 
qed 
270 
also have "\<dots> = c" 

271 
proof  

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

272 
from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

273 
then show ?thesis by simp 
27611  274 
qed 
275 
finally show ?thesis . 

13515  276 
qed 
46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

277 
qed (insert `continuous V f norm`, simp_all add: continuous_def) 
27611  278 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

279 

10687  280 
end 