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 *)
     5 
     6 header {* The norm of a function *}
     7 
     8 theory FunctionNorm = NormedSpace + FunctionOrder:
     9 
    10 subsection {* Continuous linear forms*}
    11 
    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 *}
    18 
    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)"
    24 
    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
    32   
    33 lemma continuous_linearform [intro?]: 
    34   "is_continuous V norm f ==> is_linearform V f"
    35   by (unfold is_continuous_def) force
    36 
    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
    41 
    42 subsection{* The norm of a linear form *}
    43 
    44 
    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$.
    48 
    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} \] 
    51 
    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$.
    59 
    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 *}
    65 
    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}"
    70 
    71 text{* $n$ is the function norm of $f$, iff 
    72 $n$ is the supremum of $B$. 
    73 *}
    74 
    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"
    79 
    80 text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
    81 if the supremum exists. Otherwise it is undefined. *}
    82 
    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)"
    86 
    87 syntax   
    88   function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\\<parallel>_\\<parallel>_,_")
    89 
    90 lemma B_not_empty: "#0 \\<in> B V norm f"
    91   by (unfold B_def, force)
    92 
    93 text {* The following lemma states that every continuous linear form
    94 on a normed space $(V, \norm{\cdot})$ has a function norm. *}
    95 
    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"
   104 
   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)
   111 
   112     txt {* First we have to show that $B$ is non-empty: *} 
   113 
   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
   118 
   119     txt {* Then we have to show that $B$ is bounded: *}
   120 
   121     from e show "\\<exists>Y. isUb UNIV (B V norm f) Y"
   122     proof
   123 
   124       txt {* We know that $f$ is bounded by some value $c$. *}  
   125   
   126       fix c assume a: "\\<forall>x \\<in> V. |f x| <= c * norm x"
   127       def b == "max c #0"
   128 
   129       show "?thesis"
   130       proof (intro exI isUbI setleI ballI, unfold B_def, 
   131 	elim UnE CollectE exE conjE singletonE)
   132 
   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$: *}
   137 
   138 	fix y assume "y = (#0::real)"
   139         show "y <= b" by (simp! add: le_maxI2)
   140 
   141         txt{* The second case is 
   142         $y = {|f\ap x|}/{\norm x}$ for some 
   143         $x\in V$ with $x \neq \zero$. *}
   144 
   145       next
   146 	fix x y
   147         assume "x \\<in> V" "x \\<noteq> 0" (***
   148 
   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; ***)***)
   167 
   168         txt {* The thesis follows by a short calculation using the 
   169         fact that $f$ is bounded. *}
   170     
   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
   193 
   194 text {* The norm of a continuous function is always $\geq 0$. *}
   195 
   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"
   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
   205   the supremum exists and $B$ is not empty. *}
   206 
   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)"
   215 
   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!)
   228 
   229     txt {* Since $f$ is continuous the function norm exists: *}
   230 
   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)
   234 
   235     txt {* $B$ is non-empty by construction: *}
   236 
   237     show "#0 \\<in> B V norm f" by (rule B_not_empty)
   238   qed
   239 qed
   240   
   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 *}
   246 
   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" ..
   254 
   255  txt{* The proof is by case analysis on $x$. *}
   256  
   257   show ?thesis
   258   proof cases
   259 
   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$. *}
   263 
   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" .
   275 
   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)
   281 
   282     txt {* For the case $x\neq \zero$ we derive the following
   283     fact from the definition of the function norm:*}
   284 
   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
   294 
   295     txt {* The thesis now follows by a short calculation: *}
   296 
   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
   307 
   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 *}
   314 
   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"
   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.
   329   *}
   330 
   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) 
   336   
   337     txt {* $c$ is an upper bound of $B$, i.e. every
   338     $y\in B$ is less than $c$. *}
   339 
   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)
   345 
   346        txt {* The first case for $y\in B$ is $y=0$. *}
   347 
   348         assume "y = #0"
   349         show "y <= c" by (force!)
   350 
   351         txt{* The second case is 
   352         $y = {|f\ap x|}/{\norm x}$ for some 
   353         $x\in V$ with $x \neq \zero$. *}  
   354 
   355       next
   356 	fix x 
   357         assume "x \\<in> V" "x \\<noteq> 0" 
   358 
   359         have lz: "#0 < norm x" 
   360           by (simp! add: normed_vs_norm_gt_zero)
   361           
   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
   367             
   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)
   372 
   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
   384 
   385 end