author  wenzelm 
Fri, 15 Sep 2000 20:22:00 +0200  
changeset 9998  09bf8fcd1c6e 
parent 9969  4753185f1dd2 
child 10606  e3229a37d53f 
permissions  rwrr 
7566  1 
(* Title: HOL/Real/HahnBanach/FunctionNorm.thy 
2 
ID: $Id$ 

3 
Author: Gertrud Bauer, TU Munich 

4 
*) 

7535
599d3414b51d
The HahnBanach 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 HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

9 

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

7978  12 
text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$ 
13 
is \emph{continuous}, iff it is bounded, i.~e. 

14 
\[\Ex {c\in R}{\All {x\in V} {f\ap x \leq c \cdot \norm x}}\] 

15 
In our application no other functions than linear forms are considered, 

16 
so we can define continuous linear forms as bounded linear forms: 

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

18 

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

19 
constdefs 
7978  20 
is_continuous :: 
9374  21 
"['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool" 
7978  22 
"is_continuous V norm f == 
9503  23 
is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. f x <= c * norm x)" 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

24 

7978  25 
lemma continuousI [intro]: 
9503  26 
"[ is_linearform V f; !! x. x \<in> V ==> f x <= c * norm x ] 
9035  27 
==> is_continuous V norm f" 
28 
proof (unfold is_continuous_def, intro exI conjI ballI) 

9503  29 
assume r: "!! x. x \<in> V ==> f x <= c * norm x" 
30 
fix x assume "x \<in> V" show "f x <= c * norm x" by (rule r) 

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

32 

9408  33 
lemma continuous_linearform [intro?]: 
9035  34 
"is_continuous V norm f ==> is_linearform V f" 
35 
by (unfold is_continuous_def) force 

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

36 

9408  37 
lemma continuous_bounded [intro?]: 
7978  38 
"is_continuous V norm f 
9503  39 
==> \<exists>c. \<forall>x \<in> V. f x <= c * norm x" 
9035  40 
by (unfold is_continuous_def) force 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

41 

9035  42 
subsection{* The norm of a linear form *} 
7917  43 

44 

45 
text{* The least real number $c$ for which holds 

7978  46 
\[\All {x\in V}{f\ap x \leq c \cdot \norm x}\] 
7917  47 
is called the \emph{norm} of $f$. 
48 

7978  49 
For nontrivial vector spaces $V \neq \{\zero\}$ the norm can be defined as 
7927  50 
\[\fnorm {f} =\sup_{x\neq\zero}\frac{f\ap x}{\norm x} \] 
7917  51 

7978  52 
For the case $V = \{\zero\}$ the supremum would be taken from an 
53 
empty set. Since $\bbbR$ is unbounded, there would be no supremum. To 

54 
avoid this situation it must be guaranteed that there is an element in 

55 
this set. This element must be ${} \ge 0$ so that 

7927  56 
$\idt{function{\dsh}norm}$ has the norm properties. Furthermore it 
57 
does not have to change the norm in all other cases, so it must be 

7978  58 
$0$, as all other elements of are ${} \ge 0$. 
7917  59 

7978  60 
Thus we define the set $B$ the supremum is taken from as 
61 
\[ 

9374  62 
\{ 0 \} \Union \left\{ \frac{f\ap x}{\norm x} \dt x\neq \zero \And x\in F\right\} 
7978  63 
\] 
9035  64 
*} 
7917  65 

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

66 
constdefs 
9374  67 
B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set" 
7808  68 
"B V norm f == 
9503  69 
{#0} \<union> {f x * rinv (norm x)  x. x \<noteq> 0 \<and> x \<in> V}" 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

70 

7978  71 
text{* $n$ is the function norm of $f$, iff 
72 
$n$ is the supremum of $B$. 

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

74 

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

75 
constdefs 
7917  76 
is_function_norm :: 
9374  77 
" ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real => bool" 
78 
"is_function_norm f V norm fn == is_Sup UNIV (B V norm f) fn" 

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

79 

7978  80 
text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
9035  81 
if the supremum exists. Otherwise it is undefined. *} 
7978  82 

83 
constdefs 

9374  84 
function_norm :: " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real" 
85 
"function_norm f V norm == Sup UNIV (B V norm f)" 

7978  86 

9374  87 
syntax 
9503  88 
function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\<parallel>_\<parallel>_,_") 
9374  89 

9503  90 
lemma B_not_empty: "#0 \<in> B V norm f" 
9035  91 
by (unfold B_def, force) 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

92 

7978  93 
text {* The following lemma states that every continuous linear form 
9035  94 
on a normed space $(V, \norm{\cdot})$ has a function norm. *} 
7917  95 

9408  96 
lemma ex_fnorm [intro?]: 
7978  97 
"[ is_normed_vectorspace V norm; is_continuous V norm f] 
9503  98 
==> is_function_norm f V norm \<parallel>f\<parallel>V,norm" 
7917  99 
proof (unfold function_norm_def is_function_norm_def 
9998  100 
is_continuous_def Sup_def, elim conjE, rule someI2_ex) 
9035  101 
assume "is_normed_vectorspace V norm" 
7808  102 
assume "is_linearform V f" 
9503  103 
and e: "\<exists>c. \<forall>x \<in> V. f x <= c * norm x" 
7917  104 

105 
txt {* The existence of the supremum is shown using the 

106 
completeness of the reals. Completeness means, that 

7978  107 
every nonempty bounded set of reals has a 
9035  108 
supremum. *} 
9503  109 
show "\<exists>a. is_Sup UNIV (B V norm f) a" 
9035  110 
proof (unfold is_Sup_def, rule reals_complete) 
7917  111 

9035  112 
txt {* First we have to show that $B$ is nonempty: *} 
7917  113 

9503  114 
show "\<exists>X. X \<in> B V norm f" 
9035  115 
proof (intro exI) 
9503  116 
show "#0 \<in> (B V norm f)" by (unfold B_def, force) 
9035  117 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

118 

9035  119 
txt {* Then we have to show that $B$ is bounded: *} 
7917  120 

9503  121 
from e show "\<exists>Y. isUb UNIV (B V norm f) Y" 
9035  122 
proof 
7917  123 

9035  124 
txt {* We know that $f$ is bounded by some value $c$. *} 
7917  125 

9503  126 
fix c assume a: "\<forall>x \<in> V. f x <= c * norm x" 
9035  127 
def b == "max c #0" 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

128 

9035  129 
show "?thesis" 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

130 
proof (intro exI isUbI setleI ballI, unfold B_def, 
9035  131 
elim UnE CollectE exE conjE singletonE) 
7917  132 

133 
txt{* To proof the thesis, we have to show that there is 

7978  134 
some constant $b$, such that $y \leq b$ for all $y\in B$. 
7917  135 
Due to the definition of $B$ there are two cases for 
9379  136 
$y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *} 
7917  137 

9035  138 
fix y assume "y = (#0::real)" 
9394  139 
show "y <= b" by (simp! add: le_maxI2) 
7917  140 

141 
txt{* The second case is 

7978  142 
$y = {f\ap x}/{\norm x}$ for some 
9035  143 
$x\in V$ with $x \neq \zero$. *} 
7917  144 

9035  145 
next 
146 
fix x y 

9503  147 
assume "x \<in> V" "x \<noteq> 0" (*** 
7917  148 

9035  149 
have ge: "#0 <= rinv (norm x)"; 
7917  150 
by (rule real_less_imp_le, rule real_rinv_gt_zero, 
9035  151 
rule normed_vs_norm_gt_zero); ( *** 
7656  152 
proof (rule real_less_imp_le); 
9035  153 
show "#0 < rinv (norm x)"; 
7566  154 
proof (rule real_rinv_gt_zero); 
9035  155 
show "#0 < norm x"; ..; 
7566  156 
qed; 
9035  157 
qed; *** ) 
9503  158 
have nz: "norm x \<noteq> #0" 
7917  159 
by (rule not_sym, rule lt_imp_not_eq, 
9035  160 
rule normed_vs_norm_gt_zero) (*** 
7917  161 
proof (rule not_sym); 
9503  162 
show "#0 \<noteq> norm x"; 
7917  163 
proof (rule lt_imp_not_eq); 
9035  164 
show "#0 < norm x"; ..; 
7917  165 
qed; 
166 
qed; ***)***) 

167 

168 
txt {* The thesis follows by a short calculation using the 

9035  169 
fact that $f$ is bounded. *} 
7917  170 

9374  171 
assume "y = f x * rinv (norm x)" 
9035  172 
also have "... <= c * norm x * rinv (norm x)" 
173 
proof (rule real_mult_le_le_mono2) 

174 
show "#0 <= rinv (norm x)" 

9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8838
diff
changeset

175 
by (rule real_less_imp_le, rule real_rinv_gt_zero1, 
9035  176 
rule normed_vs_norm_gt_zero) 
9374  177 
from a show "f x <= c * norm x" .. 
9035  178 
qed 
179 
also have "... = c * (norm x * rinv (norm x))" 

180 
by (rule real_mult_assoc) 

181 
also have "(norm x * rinv (norm x)) = (#1::real)" 

182 
proof (rule real_mult_inv_right1) 

9503  183 
show nz: "norm x \<noteq> #0" 
7917  184 
by (rule not_sym, rule lt_imp_not_eq, 
9035  185 
rule normed_vs_norm_gt_zero) 
186 
qed 

9394  187 
also have "c * ... <= b " by (simp! add: le_maxI1) 
9035  188 
finally show "y <= b" . 
189 
qed simp 

190 
qed 

191 
qed 

192 
qed 

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

193 

9035  194 
text {* The norm of a continuous function is always $\geq 0$. *} 
7917  195 

9408  196 
lemma fnorm_ge_zero [intro?]: 
9374  197 
"[ is_continuous V norm f; is_normed_vectorspace V norm ] 
9503  198 
==> #0 <= \<parallel>f\<parallel>V,norm" 
9035  199 
proof  
7978  200 
assume c: "is_continuous V norm f" 
9035  201 
and n: "is_normed_vectorspace V norm" 
7917  202 

203 
txt {* The function norm is defined as the supremum of $B$. 

204 
So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided 

9035  205 
the supremum exists and $B$ is not empty. *} 
7917  206 

9035  207 
show ?thesis 
208 
proof (unfold function_norm_def, rule sup_ub1) 

9503  209 
show "\<forall>x \<in> (B V norm f). #0 <= x" 
7978  210 
proof (intro ballI, unfold B_def, 
9035  211 
elim UnE singletonE CollectE exE conjE) 
212 
fix x r 

9503  213 
assume "x \<in> V" "x \<noteq> 0" 
9374  214 
and r: "r = f x * rinv (norm x)" 
7917  215 

9374  216 
have ge: "#0 <= f x" by (simp! only: abs_ge_zero) 
9035  217 
have "#0 <= rinv (norm x)" 
218 
by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(*** 

7656  219 
proof (rule real_less_imp_le); 
9035  220 
show "#0 < rinv (norm x)"; 
7566  221 
proof (rule real_rinv_gt_zero); 
9035  222 
show "#0 < norm x"; ..; 
7566  223 
qed; 
7917  224 
qed; ***) 
9035  225 
with ge show "#0 <= r" 
226 
by (simp only: r, rule real_le_mult_order1a) 

227 
qed (simp!) 

7917  228 

9035  229 
txt {* Since $f$ is continuous the function norm exists: *} 
7917  230 

9503  231 
have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" .. 
9035  232 
thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" 
233 
by (unfold is_function_norm_def function_norm_def) 

7917  234 

9035  235 
txt {* $B$ is nonempty by construction: *} 
7917  236 

9503  237 
show "#0 \<in> B V norm f" by (rule B_not_empty) 
9035  238 
qed 
239 
qed 

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

240 

7978  241 
text{* \medskip The fundamental property of function norms is: 
7917  242 
\begin{matharray}{l} 
243 
 f\ap x  \leq {\fnorm {f}} \cdot {\norm x} 

244 
\end{matharray} 

9035  245 
*} 
7917  246 

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

247 
lemma norm_fx_le_norm_f_norm_x: 
9503  248 
"[ is_continuous V norm f; is_normed_vectorspace V norm; x \<in> V ] 
249 
==> f x <= \<parallel>f\<parallel>V,norm * norm x" 

9035  250 
proof  
9503  251 
assume "is_normed_vectorspace V norm" "x \<in> V" 
9035  252 
and c: "is_continuous V norm f" 
253 
have v: "is_vectorspace V" .. 

7917  254 

9035  255 
txt{* The proof is by case analysis on $x$. *} 
7917  256 

9035  257 
show ?thesis 
258 
proof cases 

7917  259 

260 
txt {* For the case $x = \zero$ the thesis follows 

261 
from the linearity of $f$: for every linear function 

9035  262 
holds $f\ap \zero = 0$. *} 
7917  263 

9374  264 
assume "x = 0" 
265 
have "f x = f 0" by (simp!) 

266 
also from v continuous_linearform have "f 0 = #0" .. 

9035  267 
also note abs_zero 
9503  268 
also have "#0 <= \<parallel>f\<parallel>V,norm * norm x" 
9035  269 
proof (rule real_le_mult_order1a) 
9503  270 
show "#0 <= \<parallel>f\<parallel>V,norm" .. 
9035  271 
show "#0 <= norm x" .. 
272 
qed 

273 
finally 

9503  274 
show "f x <= \<parallel>f\<parallel>V,norm * norm x" . 
7917  275 

9035  276 
next 
9503  277 
assume "x \<noteq> 0" 
9379  278 
have n: "#0 < norm x" .. 
9503  279 
hence nz: "norm x \<noteq> #0" 
9379  280 
by (simp only: lt_imp_not_eq) 
7917  281 

282 
txt {* For the case $x\neq \zero$ we derive the following 

9035  283 
fact from the definition of the function norm:*} 
7917  284 

9503  285 
have l: "f x * rinv (norm x) <= \<parallel>f\<parallel>V,norm" 
9035  286 
proof (unfold function_norm_def, rule sup_ub) 
287 
from ex_fnorm [OF _ c] 

288 
show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" 

289 
by (simp! add: is_function_norm_def function_norm_def) 

9503  290 
show "f x * rinv (norm x) \<in> B V norm f" 
7978  291 
by (unfold B_def, intro UnI2 CollectI exI [of _ x] 
9035  292 
conjI, simp) 
293 
qed 

7917  294 

9035  295 
txt {* The thesis now follows by a short calculation: *} 
7917  296 

9374  297 
have "f x = f x * #1" by (simp!) 
298 
also from nz have "#1 = rinv (norm x) * norm x" 

9379  299 
by (simp add: real_mult_inv_left1) 
300 
also have "f x * ... = f x * rinv (norm x) * norm x" 

9374  301 
by (simp! add: real_mult_assoc) 
9503  302 
also from n l have "... <= \<parallel>f\<parallel>V,norm * norm x" 
9379  303 
by (simp add: real_mult_le_le_mono2) 
9503  304 
finally show "f x <= \<parallel>f\<parallel>V,norm * norm x" . 
9035  305 
qed 
306 
qed 

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

307 

7978  308 
text{* \medskip The function norm is the least positive real number for 
309 
which the following inequation holds: 

7917  310 
\begin{matharray}{l} 
311 
 f\ap x  \leq c \cdot {\norm x} 

312 
\end{matharray} 

9035  313 
*} 
7917  314 

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

315 
lemma fnorm_le_ub: 
9374  316 
"[ is_continuous V norm f; is_normed_vectorspace V norm; 
9503  317 
\<forall>x \<in> V. f x <= c * norm x; #0 <= c ] 
318 
==> \<parallel>f\<parallel>V,norm <= c" 

9035  319 
proof (unfold function_norm_def) 
320 
assume "is_normed_vectorspace V norm" 

321 
assume c: "is_continuous V norm f" 

9503  322 
assume fb: "\<forall>x \<in> V. f x <= c * norm x" 
9379  323 
and "#0 <= c" 
7917  324 

325 
txt {* Suppose the inequation holds for some $c\geq 0$. 

326 
If $c$ is an upper bound of $B$, then $c$ is greater 

327 
than the function norm since the function norm is the 

328 
least upper bound. 

9035  329 
*} 
7917  330 

9035  331 
show "Sup UNIV (B V norm f) <= c" 
332 
proof (rule sup_le_ub) 

333 
from ex_fnorm [OF _ c] 

334 
show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" 

335 
by (simp! add: is_function_norm_def function_norm_def) 

7917  336 

9374  337 
txt {* $c$ is an upper bound of $B$, i.e. every 
9035  338 
$y\in B$ is less than $c$. *} 
7917  339 

9035  340 
show "isUb UNIV (B V norm f) c" 
341 
proof (intro isUbI setleI ballI) 

9503  342 
fix y assume "y \<in> B V norm f" 
9035  343 
thus le: "y <= c" 
344 
proof (unfold B_def, elim UnE CollectE exE conjE singletonE) 

7917  345 

9035  346 
txt {* The first case for $y\in B$ is $y=0$. *} 
7917  347 

9035  348 
assume "y = #0" 
349 
show "y <= c" by (force!) 

7917  350 

351 
txt{* The second case is 

7978  352 
$y = {f\ap x}/{\norm x}$ for some 
9035  353 
$x\in V$ with $x \neq \zero$. *} 
7917  354 

9035  355 
next 
356 
fix x 

9503  357 
assume "x \<in> V" "x \<noteq> 0" 
7917  358 

9035  359 
have lz: "#0 < norm x" 
360 
by (simp! add: normed_vs_norm_gt_zero) 

7566  361 

9503  362 
have nz: "norm x \<noteq> #0" 
9035  363 
proof (rule not_sym) 
9503  364 
from lz show "#0 \<noteq> norm x" 
9035  365 
by (simp! add: order_less_imp_not_eq) 
366 
qed 

7566  367 

9035  368 
from lz have "#0 < rinv (norm x)" 
369 
by (simp! add: real_rinv_gt_zero1) 

370 
hence rinv_gez: "#0 <= rinv (norm x)" 

371 
by (rule real_less_imp_le) 

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

372 

9374  373 
assume "y = f x * rinv (norm x)" 
9035  374 
also from rinv_gez have "... <= c * norm x * rinv (norm x)" 
375 
proof (rule real_mult_le_le_mono2) 

9374  376 
show "f x <= c * norm x" by (rule bspec) 
9035  377 
qed 
378 
also have "... <= c" by (simp add: nz real_mult_assoc) 

379 
finally show ?thesis . 

380 
qed 

381 
qed force 

382 
qed 

383 
qed 

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

384 

9035  385 
end 