src/HOL/Real/HahnBanach/FunctionNorm.thy
 author wenzelm Sun Jul 23 12:01:05 2000 +0200 (2000-07-23) changeset 9408 d3d56e1d2ec1 parent 9394 1ff8a6234c6a child 9503 3324cbbecef8 permissions -rw-r--r--
classical atts now intro! / intro / intro?;
1 (*  Title:      HOL/Real/HahnBanach/FunctionNorm.thy
2     ID:         $Id$
3     Author:     Gertrud Bauer, TU Munich
4 *)
6 header {* The norm of a function *}
8 theory FunctionNorm = NormedSpace + FunctionOrder:
10 subsection {* Continuous linear forms*}
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:
17 *}
19 constdefs
20   is_continuous ::
21   "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool"
22   "is_continuous V norm f ==
23     is_linearform V f \\<and> (\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x)"
25 lemma continuousI [intro]:
26   "[| is_linearform V f; !! x. x \\<in> V ==> |f x| <= c * norm x |]
27   ==> is_continuous V norm f"
28 proof (unfold is_continuous_def, intro exI conjI ballI)
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)
31 qed
33 lemma continuous_linearform [intro?]:
34   "is_continuous V norm f ==> is_linearform V f"
35   by (unfold is_continuous_def) force
37 lemma continuous_bounded [intro?]:
38   "is_continuous V norm f
39   ==> \\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
40   by (unfold is_continuous_def) force
42 subsection{* The norm of a linear form *}
45 text{* The least real number $c$ for which holds
46 $\All {x\in V}{|f\ap x| \leq c \cdot \norm x}$
47 is called the \emph{norm} of $f$.
49 For non-trivial vector spaces $V \neq \{\zero\}$ the norm can be defined as
50 $\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}$
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
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
58 $0$, as all other elements of are ${} \ge 0$.
60 Thus we define the set $B$ the supremum is taken from as
61 $62 \{ 0 \} \Union \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\} 63$
64 *}
66 constdefs
67   B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"
68   "B V norm f ==
69   {#0} \\<union> {|f x| * rinv (norm x) | x. x \\<noteq> 0 \\<and> x \\<in> V}"
71 text{* $n$ is the function norm of $f$, iff
72 $n$ is the supremum of $B$.
73 *}
75 constdefs
76   is_function_norm ::
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"
80 text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$,
81 if the supremum exists. Otherwise it is undefined. *}
83 constdefs
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)"
87 syntax
88   function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\\<parallel>_\\<parallel>_,_")
90 lemma B_not_empty: "#0 \\<in> B V norm f"
91   by (unfold B_def, force)
93 text {* The following lemma states that every continuous linear form
94 on a normed space $(V, \norm{\cdot})$ has a function norm. *}
96 lemma ex_fnorm [intro?]:
97   "[| is_normed_vectorspace V norm; is_continuous V norm f|]
98      ==> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm"
99 proof (unfold function_norm_def is_function_norm_def
100   is_continuous_def Sup_def, elim conjE, rule selectI2EX)
101   assume "is_normed_vectorspace V norm"
102   assume "is_linearform V f"
103   and e: "\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
105   txt {* The existence of the supremum is shown using the
106   completeness of the reals. Completeness means, that
107   every non-empty bounded set of reals has a
108   supremum. *}
109   show  "\\<exists>a. is_Sup UNIV (B V norm f) a"
110   proof (unfold is_Sup_def, rule reals_complete)
112     txt {* First we have to show that $B$ is non-empty: *}
114     show "\\<exists>X. X \\<in> B V norm f"
115     proof (intro exI)
116       show "#0 \\<in> (B V norm f)" by (unfold B_def, force)
117     qed
119     txt {* Then we have to show that $B$ is bounded: *}
121     from e show "\\<exists>Y. isUb UNIV (B V norm f) Y"
122     proof
124       txt {* We know that $f$ is bounded by some value $c$. *}
126       fix c assume a: "\\<forall>x \\<in> V. |f x| <= c * norm x"
127       def b == "max c #0"
129       show "?thesis"
130       proof (intro exI isUbI setleI ballI, unfold B_def,
131 	elim UnE CollectE exE conjE singletonE)
133         txt{* To proof the thesis, we have to show that there is
134         some constant $b$, such that $y \leq b$ for all $y\in B$.
135         Due to the definition of $B$ there are two cases for
136         $y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}
138 	fix y assume "y = (#0::real)"
139         show "y <= b" by (simp! add: le_maxI2)
141         txt{* The second case is
142         $y = {|f\ap x|}/{\norm x}$ for some
143         $x\in V$ with $x \neq \zero$. *}
145       next
146 	fix x y
147         assume "x \\<in> V" "x \\<noteq> 0" (***
149          have ge: "#0 <= rinv (norm x)";
150           by (rule real_less_imp_le, rule real_rinv_gt_zero,
151                 rule normed_vs_norm_gt_zero); ( ***
152           proof (rule real_less_imp_le);
153             show "#0 < rinv (norm x)";
154             proof (rule real_rinv_gt_zero);
155               show "#0 < norm x"; ..;
156             qed;
157           qed; *** )
158         have nz: "norm x \\<noteq> #0"
159           by (rule not_sym, rule lt_imp_not_eq,
160               rule normed_vs_norm_gt_zero) (***
161           proof (rule not_sym);
162             show "#0 \\<noteq> norm x";
163             proof (rule lt_imp_not_eq);
164               show "#0 < norm x"; ..;
165             qed;
166           qed; ***)***)
168         txt {* The thesis follows by a short calculation using the
169         fact that $f$ is bounded. *}
171         assume "y = |f x| * rinv (norm x)"
172         also have "... <= c * norm x * rinv (norm x)"
173         proof (rule real_mult_le_le_mono2)
174           show "#0 <= rinv (norm x)"
175             by (rule real_less_imp_le, rule real_rinv_gt_zero1,
176                 rule normed_vs_norm_gt_zero)
177           from a show "|f x| <= c * norm x" ..
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)
183           show nz: "norm x \\<noteq> #0"
184             by (rule not_sym, rule lt_imp_not_eq,
185               rule normed_vs_norm_gt_zero)
186         qed
187         also have "c * ... <= b " by (simp! add: le_maxI1)
188 	finally show "y <= b" .
189       qed simp
190     qed
191   qed
192 qed
194 text {* The norm of a continuous function is always $\geq 0$. *}
196 lemma fnorm_ge_zero [intro?]:
197   "[| is_continuous V norm f; is_normed_vectorspace V norm |]
198    ==> #0 <= \\<parallel>f\\<parallel>V,norm"
199 proof -
200   assume c: "is_continuous V norm f"
201      and n: "is_normed_vectorspace V norm"
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
205   the supremum exists and $B$ is not empty. *}
207   show ?thesis
208   proof (unfold function_norm_def, rule sup_ub1)
209     show "\\<forall>x \\<in> (B V norm f). #0 <= x"
210     proof (intro ballI, unfold B_def,
211            elim UnE singletonE CollectE exE conjE)
212       fix x r
213       assume "x \\<in> V" "x \\<noteq> 0"
214         and r: "r = |f x| * rinv (norm x)"
216       have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)
217       have "#0 <= rinv (norm x)"
218         by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(***
219         proof (rule real_less_imp_le);
220           show "#0 < rinv (norm x)";
221           proof (rule real_rinv_gt_zero);
222             show "#0 < norm x"; ..;
223           qed;
224         qed; ***)
225       with ge show "#0 <= r"
226        by (simp only: r, rule real_le_mult_order1a)
227     qed (simp!)
229     txt {* Since $f$ is continuous the function norm exists: *}
231     have "is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" ..
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)
235     txt {* $B$ is non-empty by construction: *}
237     show "#0 \\<in> B V norm f" by (rule B_not_empty)
238   qed
239 qed
241 text{* \medskip The fundamental property of function norms is:
242 \begin{matharray}{l}
243 | f\ap x | \leq {\fnorm {f}} \cdot {\norm x}
244 \end{matharray}
245 *}
247 lemma norm_fx_le_norm_f_norm_x:
248   "[| is_continuous V norm f; is_normed_vectorspace V norm; x \\<in> V |]
249     ==> |f x| <= \\<parallel>f\\<parallel>V,norm * norm x"
250 proof -
251   assume "is_normed_vectorspace V norm" "x \\<in> V"
252   and c: "is_continuous V norm f"
253   have v: "is_vectorspace V" ..
255  txt{* The proof is by case analysis on $x$. *}
257   show ?thesis
258   proof cases
260     txt {* For the case $x = \zero$ the thesis follows
261     from the linearity of $f$: for every linear function
262     holds $f\ap \zero = 0$. *}
264     assume "x = 0"
265     have "|f x| = |f 0|" by (simp!)
266     also from v continuous_linearform have "f 0 = #0" ..
267     also note abs_zero
268     also have "#0 <= \\<parallel>f\\<parallel>V,norm * norm x"
269     proof (rule real_le_mult_order1a)
270       show "#0 <= \\<parallel>f\\<parallel>V,norm" ..
271       show "#0 <= norm x" ..
272     qed
273     finally
274     show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .
276   next
277     assume "x \\<noteq> 0"
278     have n: "#0 < norm x" ..
279     hence nz: "norm x \\<noteq> #0"
280       by (simp only: lt_imp_not_eq)
282     txt {* For the case $x\neq \zero$ we derive the following
283     fact from the definition of the function norm:*}
285     have l: "|f x| * rinv (norm x) <= \\<parallel>f\\<parallel>V,norm"
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)
290       show "|f x| * rinv (norm x) \\<in> B V norm f"
291         by (unfold B_def, intro UnI2 CollectI exI [of _ x]
292             conjI, simp)
293     qed
295     txt {* The thesis now follows by a short calculation: *}
297     have "|f x| = |f x| * #1" by (simp!)
298     also from nz have "#1 = rinv (norm x) * norm x"
299       by (simp add: real_mult_inv_left1)
300     also have "|f x| * ... = |f x| * rinv (norm x) * norm x"
301       by (simp! add: real_mult_assoc)
302     also from n l have "... <= \\<parallel>f\\<parallel>V,norm * norm x"
303       by (simp add: real_mult_le_le_mono2)
304     finally show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .
305   qed
306 qed
308 text{* \medskip The function norm is the least positive real number for
309 which the following inequation holds:
310 \begin{matharray}{l}
311 | f\ap x | \leq c \cdot {\norm x}
312 \end{matharray}
313 *}
315 lemma fnorm_le_ub:
316   "[| is_continuous V norm f; is_normed_vectorspace V norm;
317      \\<forall>x \\<in> V. |f x| <= c * norm x; #0 <= c |]
318   ==> \\<parallel>f\\<parallel>V,norm <= c"
319 proof (unfold function_norm_def)
320   assume "is_normed_vectorspace V norm"
321   assume c: "is_continuous V norm f"
322   assume fb: "\\<forall>x \\<in> V. |f x| <= c * norm x"
323     and "#0 <= c"
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.
329   *}
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)
337     txt {* $c$ is an upper bound of $B$, i.e. every
338     $y\in B$ is less than $c$. *}
340     show "isUb UNIV (B V norm f) c"
341     proof (intro isUbI setleI ballI)
342       fix y assume "y \\<in> B V norm f"
343       thus le: "y <= c"
344       proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
346        txt {* The first case for $y\in B$ is $y=0$. *}
348         assume "y = #0"
349         show "y <= c" by (force!)
351         txt{* The second case is
352         $y = {|f\ap x|}/{\norm x}$ for some
353         $x\in V$ with $x \neq \zero$. *}
355       next
356 	fix x
357         assume "x \\<in> V" "x \\<noteq> 0"
359         have lz: "#0 < norm x"
360           by (simp! add: normed_vs_norm_gt_zero)
362         have nz: "norm x \\<noteq> #0"
363         proof (rule not_sym)
364           from lz show "#0 \\<noteq> norm x"
365             by (simp! add: order_less_imp_not_eq)
366         qed
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)
373 	assume "y = |f x| * rinv (norm x)"
374 	also from rinv_gez have "... <= c * norm x * rinv (norm x)"
375 	  proof (rule real_mult_le_le_mono2)
376 	    show "|f x| <= c * norm x" by (rule bspec)
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
385 end