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?;
 wenzelm@7566  1 (* Title: HOL/Real/HahnBanach/FunctionNorm.thy  wenzelm@7566  2  ID: $Id$  wenzelm@7566  3  Author: Gertrud Bauer, TU Munich  wenzelm@7566  4 *)  wenzelm@7535  5 wenzelm@9035  6 header {* The norm of a function *}  wenzelm@7808  7 wenzelm@9035  8 theory FunctionNorm = NormedSpace + FunctionOrder:  wenzelm@7535  9 wenzelm@9035  10 subsection {* Continuous linear forms*}  wenzelm@7917  11 wenzelm@7978  12 text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$  wenzelm@7978  13 is \emph{continuous}, iff it is bounded, i.~e.  wenzelm@7978  14 $\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}$  wenzelm@7978  15 In our application no other functions than linear forms are considered,  wenzelm@7978  16 so we can define continuous linear forms as bounded linear forms:  wenzelm@9035  17 *}  wenzelm@7535  18 wenzelm@7535  19 constdefs  wenzelm@7978  20  is_continuous ::  bauerg@9374  21  "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool"  wenzelm@7978  22  "is_continuous V norm f ==  bauerg@9379  23  is_linearform V f \\ (\\c. \\x \\ V. |f x| <= c * norm x)"  wenzelm@7535  24 wenzelm@7978  25 lemma continuousI [intro]:  bauerg@9379  26  "[| is_linearform V f; !! x. x \\ V ==> |f x| <= c * norm x |]  wenzelm@9035  27  ==> is_continuous V norm f"  wenzelm@9035  28 proof (unfold is_continuous_def, intro exI conjI ballI)  bauerg@9379  29  assume r: "!! x. x \\ V ==> |f x| <= c * norm x"  bauerg@9379  30  fix x assume "x \\ V" show "|f x| <= c * norm x" by (rule r)  wenzelm@9035  31 qed  wenzelm@7535  32   wenzelm@9408  33 lemma continuous_linearform [intro?]:  wenzelm@9035  34  "is_continuous V norm f ==> is_linearform V f"  wenzelm@9035  35  by (unfold is_continuous_def) force  wenzelm@7535  36 wenzelm@9408  37 lemma continuous_bounded [intro?]:  wenzelm@7978  38  "is_continuous V norm f  bauerg@9379  39  ==> \\c. \\x \\ V. |f x| <= c * norm x"  wenzelm@9035  40  by (unfold is_continuous_def) force  wenzelm@7535  41 wenzelm@9035  42 subsection{* The norm of a linear form *}  wenzelm@7917  43 wenzelm@7917  44 wenzelm@7917  45 text{* The least real number $c$ for which holds  wenzelm@7978  46 $\All {x\in V}{|f\ap x| \leq c \cdot \norm x}$  wenzelm@7917  47 is called the \emph{norm} of $f$.  wenzelm@7917  48 wenzelm@7978  49 For non-trivial vector spaces $V \neq \{\zero\}$ the norm can be defined as  wenzelm@7927  50 $\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}$  wenzelm@7917  51 wenzelm@7978  52 For the case $V = \{\zero\}$ the supremum would be taken from an  wenzelm@7978  53 empty set. Since $\bbbR$ is unbounded, there would be no supremum. To  wenzelm@7978  54 avoid this situation it must be guaranteed that there is an element in  wenzelm@7978  55 this set. This element must be ${} \ge 0$ so that  wenzelm@7927  56 $\idt{function{\dsh}norm}$ has the norm properties. Furthermore it  wenzelm@7927  57 does not have to change the norm in all other cases, so it must be  wenzelm@7978  58 $0$, as all other elements of are ${} \ge 0$.  wenzelm@7917  59 wenzelm@7978  60 Thus we define the set $B$ the supremum is taken from as  wenzelm@7978  61 $ bauerg@9374  62 \{ 0 \} \Union \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}  wenzelm@7978  63 $  wenzelm@9035  64 *}  wenzelm@7917  65 wenzelm@7535  66 constdefs  bauerg@9374  67  B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"  wenzelm@7808  68  "B V norm f ==  bauerg@9379  69  {#0} \\ {|f x| * rinv (norm x) | x. x \\ 0 \\ x \\ V}"  wenzelm@7535  70 wenzelm@7978  71 text{* $n$ is the function norm of $f$, iff  wenzelm@7978  72 $n$ is the supremum of $B$.  wenzelm@9035  73 *}  wenzelm@7535  74 wenzelm@7535  75 constdefs  wenzelm@7917  76  is_function_norm ::  bauerg@9374  77  " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real => bool"  bauerg@9374  78  "is_function_norm f V norm fn == is_Sup UNIV (B V norm f) fn"  wenzelm@7535  79 wenzelm@7978  80 text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$,  wenzelm@9035  81 if the supremum exists. Otherwise it is undefined. *}  wenzelm@7978  82 wenzelm@7978  83 constdefs  bauerg@9374  84  function_norm :: " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real"  bauerg@9374  85  "function_norm f V norm == Sup UNIV (B V norm f)"  wenzelm@7978  86 bauerg@9374  87 syntax  bauerg@9379  88  function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\\_\\_,_")  bauerg@9374  89 bauerg@9379  90 lemma B_not_empty: "#0 \\ B V norm f"  wenzelm@9035  91  by (unfold B_def, force)  wenzelm@7535  92 wenzelm@7978  93 text {* The following lemma states that every continuous linear form  wenzelm@9035  94 on a normed space $(V, \norm{\cdot})$ has a function norm. *}  wenzelm@7917  95 wenzelm@9408  96 lemma ex_fnorm [intro?]:  wenzelm@7978  97  "[| is_normed_vectorspace V norm; is_continuous V norm f|]  bauerg@9379  98  ==> is_function_norm f V norm \\f\\V,norm"  wenzelm@7917  99 proof (unfold function_norm_def is_function_norm_def  wenzelm@9035  100  is_continuous_def Sup_def, elim conjE, rule selectI2EX)  wenzelm@9035  101  assume "is_normed_vectorspace V norm"  wenzelm@7808  102  assume "is_linearform V f"  bauerg@9379  103  and e: "\\c. \\x \\ V. |f x| <= c * norm x"  wenzelm@7917  104 wenzelm@7917  105  txt {* The existence of the supremum is shown using the  wenzelm@7917  106  completeness of the reals. Completeness means, that  wenzelm@7978  107  every non-empty bounded set of reals has a  wenzelm@9035  108  supremum. *}  bauerg@9379  109  show "\\a. is_Sup UNIV (B V norm f) a"  wenzelm@9035  110  proof (unfold is_Sup_def, rule reals_complete)  wenzelm@7917  111 wenzelm@9035  112  txt {* First we have to show that $B$ is non-empty: *}  wenzelm@7917  113 bauerg@9379  114  show "\\X. X \\ B V norm f"  wenzelm@9035  115  proof (intro exI)  bauerg@9379  116  show "#0 \\ (B V norm f)" by (unfold B_def, force)  wenzelm@9035  117  qed  wenzelm@7535  118 wenzelm@9035  119  txt {* Then we have to show that $B$ is bounded: *}  wenzelm@7917  120 bauerg@9379  121  from e show "\\Y. isUb UNIV (B V norm f) Y"  wenzelm@9035  122  proof  wenzelm@7917  123 wenzelm@9035  124  txt {* We know that $f$ is bounded by some value $c$. *}  wenzelm@7917  125   bauerg@9379  126  fix c assume a: "\\x \\ V. |f x| <= c * norm x"  wenzelm@9035  127  def b == "max c #0"  wenzelm@7535  128 wenzelm@9035  129  show "?thesis"  wenzelm@7535  130  proof (intro exI isUbI setleI ballI, unfold B_def,  wenzelm@9035  131  elim UnE CollectE exE conjE singletonE)  wenzelm@7917  132 wenzelm@7917  133  txt{* To proof the thesis, we have to show that there is  wenzelm@7978  134  some constant $b$, such that $y \leq b$ for all $y\in B$.  wenzelm@7917  135  Due to the definition of $B$ there are two cases for  bauerg@9379  136  $y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}  wenzelm@7917  137 wenzelm@9035  138  fix y assume "y = (#0::real)"  wenzelm@9394  139  show "y <= b" by (simp! add: le_maxI2)  wenzelm@7917  140 wenzelm@7917  141  txt{* The second case is  wenzelm@7978  142  $y = {|f\ap x|}/{\norm x}$ for some  wenzelm@9035  143  $x\in V$ with $x \neq \zero$. *}  wenzelm@7917  144 wenzelm@9035  145  next  wenzelm@9035  146  fix x y  bauerg@9379  147  assume "x \\ V" "x \\ 0" (***  wenzelm@7917  148 wenzelm@9035  149  have ge: "#0 <= rinv (norm x)";  wenzelm@7917  150  by (rule real_less_imp_le, rule real_rinv_gt_zero,  wenzelm@9035  151  rule normed_vs_norm_gt_zero); ( ***  wenzelm@7656  152  proof (rule real_less_imp_le);  wenzelm@9035  153  show "#0 < rinv (norm x)";  wenzelm@7566  154  proof (rule real_rinv_gt_zero);  wenzelm@9035  155  show "#0 < norm x"; ..;  wenzelm@7566  156  qed;  wenzelm@9035  157  qed; *** )  bauerg@9379  158  have nz: "norm x \\ #0"  wenzelm@7917  159  by (rule not_sym, rule lt_imp_not_eq,  wenzelm@9035  160  rule normed_vs_norm_gt_zero) (***  wenzelm@7917  161  proof (rule not_sym);  bauerg@9379  162  show "#0 \\ norm x";  wenzelm@7917  163  proof (rule lt_imp_not_eq);  wenzelm@9035  164  show "#0 < norm x"; ..;  wenzelm@7917  165  qed;  wenzelm@7917  166  qed; ***)***)  wenzelm@7917  167 wenzelm@7917  168  txt {* The thesis follows by a short calculation using the  wenzelm@9035  169  fact that $f$ is bounded. *}  wenzelm@7917  170   bauerg@9374  171  assume "y = |f x| * rinv (norm x)"  wenzelm@9035  172  also have "... <= c * norm x * rinv (norm x)"  wenzelm@9035  173  proof (rule real_mult_le_le_mono2)  wenzelm@9035  174  show "#0 <= rinv (norm x)"  fleuriot@9013  175  by (rule real_less_imp_le, rule real_rinv_gt_zero1,  wenzelm@9035  176  rule normed_vs_norm_gt_zero)  bauerg@9374  177  from a show "|f x| <= c * norm x" ..  wenzelm@9035  178  qed  wenzelm@9035  179  also have "... = c * (norm x * rinv (norm x))"  wenzelm@9035  180  by (rule real_mult_assoc)  wenzelm@9035  181  also have "(norm x * rinv (norm x)) = (#1::real)"  wenzelm@9035  182  proof (rule real_mult_inv_right1)  bauerg@9379  183  show nz: "norm x \\ #0"  wenzelm@7917  184  by (rule not_sym, rule lt_imp_not_eq,  wenzelm@9035  185  rule normed_vs_norm_gt_zero)  wenzelm@9035  186  qed  wenzelm@9394  187  also have "c * ... <= b " by (simp! add: le_maxI1)  wenzelm@9035  188  finally show "y <= b" .  wenzelm@9035  189  qed simp  wenzelm@9035  190  qed  wenzelm@9035  191  qed  wenzelm@9035  192 qed  wenzelm@7535  193 wenzelm@9035  194 text {* The norm of a continuous function is always $\geq 0$. *}  wenzelm@7917  195 wenzelm@9408  196 lemma fnorm_ge_zero [intro?]:  bauerg@9374  197  "[| is_continuous V norm f; is_normed_vectorspace V norm |]  bauerg@9379  198  ==> #0 <= \\f\\V,norm"  wenzelm@9035  199 proof -  wenzelm@7978  200  assume c: "is_continuous V norm f"  wenzelm@9035  201  and n: "is_normed_vectorspace V norm"  wenzelm@7917  202 wenzelm@7917  203  txt {* The function norm is defined as the supremum of $B$.  wenzelm@7917  204  So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided  wenzelm@9035  205  the supremum exists and $B$ is not empty. *}  wenzelm@7917  206 wenzelm@9035  207  show ?thesis  wenzelm@9035  208  proof (unfold function_norm_def, rule sup_ub1)  bauerg@9379  209  show "\\x \\ (B V norm f). #0 <= x"  wenzelm@7978  210  proof (intro ballI, unfold B_def,  wenzelm@9035  211  elim UnE singletonE CollectE exE conjE)  wenzelm@9035  212  fix x r  bauerg@9379  213  assume "x \\ V" "x \\ 0"  bauerg@9374  214  and r: "r = |f x| * rinv (norm x)"  wenzelm@7917  215 bauerg@9374  216  have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)  wenzelm@9035  217  have "#0 <= rinv (norm x)"  wenzelm@9035  218  by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(***  wenzelm@7656  219  proof (rule real_less_imp_le);  wenzelm@9035  220  show "#0 < rinv (norm x)";  wenzelm@7566  221  proof (rule real_rinv_gt_zero);  wenzelm@9035  222  show "#0 < norm x"; ..;  wenzelm@7566  223  qed;  wenzelm@7917  224  qed; ***)  wenzelm@9035  225  with ge show "#0 <= r"  wenzelm@9035  226  by (simp only: r, rule real_le_mult_order1a)  wenzelm@9035  227  qed (simp!)  wenzelm@7917  228 wenzelm@9035  229  txt {* Since $f$ is continuous the function norm exists: *}  wenzelm@7917  230 bauerg@9379  231  have "is_function_norm f V norm \\f\\V,norm" ..  wenzelm@9035  232  thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"  wenzelm@9035  233  by (unfold is_function_norm_def function_norm_def)  wenzelm@7917  234 wenzelm@9035  235  txt {* $B$ is non-empty by construction: *}  wenzelm@7917  236 bauerg@9379  237  show "#0 \\ B V norm f" by (rule B_not_empty)  wenzelm@9035  238  qed  wenzelm@9035  239 qed  wenzelm@7535  240   wenzelm@7978  241 text{* \medskip The fundamental property of function norms is:  wenzelm@7917  242 \begin{matharray}{l}  wenzelm@7917  243 | f\ap x | \leq {\fnorm {f}} \cdot {\norm x}  wenzelm@7917  244 \end{matharray}  wenzelm@9035  245 *}  wenzelm@7917  246 wenzelm@7535  247 lemma norm_fx_le_norm_f_norm_x:  bauerg@9379  248  "[| is_continuous V norm f; is_normed_vectorspace V norm; x \\ V |]  bauerg@9379  249  ==> |f x| <= \\f\\V,norm * norm x"  wenzelm@9035  250 proof -  bauerg@9379  251  assume "is_normed_vectorspace V norm" "x \\ V"  wenzelm@9035  252  and c: "is_continuous V norm f"  wenzelm@9035  253  have v: "is_vectorspace V" ..  wenzelm@7917  254 wenzelm@9035  255  txt{* The proof is by case analysis on $x$. *}  wenzelm@7917  256   wenzelm@9035  257  show ?thesis  wenzelm@9035  258  proof cases  wenzelm@7917  259 wenzelm@7917  260  txt {* For the case $x = \zero$ the thesis follows  wenzelm@7917  261  from the linearity of $f$: for every linear function  wenzelm@9035  262  holds $f\ap \zero = 0$. *}  wenzelm@7917  263 bauerg@9374  264  assume "x = 0"  bauerg@9374  265  have "|f x| = |f 0|" by (simp!)  bauerg@9374  266  also from v continuous_linearform have "f 0 = #0" ..  wenzelm@9035  267  also note abs_zero  bauerg@9379  268  also have "#0 <= \\f\\V,norm * norm x"  wenzelm@9035  269  proof (rule real_le_mult_order1a)  bauerg@9379  270  show "#0 <= \\f\\V,norm" ..  wenzelm@9035  271  show "#0 <= norm x" ..  wenzelm@9035  272  qed  wenzelm@9035  273  finally  bauerg@9379  274  show "|f x| <= \\f\\V,norm * norm x" .  wenzelm@7917  275 wenzelm@9035  276  next  bauerg@9379  277  assume "x \\ 0"  bauerg@9379  278  have n: "#0 < norm x" ..  bauerg@9379  279  hence nz: "norm x \\ #0"  bauerg@9379  280  by (simp only: lt_imp_not_eq)  wenzelm@7917  281 wenzelm@7917  282  txt {* For the case $x\neq \zero$ we derive the following  wenzelm@9035  283  fact from the definition of the function norm:*}  wenzelm@7917  284 bauerg@9379  285  have l: "|f x| * rinv (norm x) <= \\f\\V,norm"  wenzelm@9035  286  proof (unfold function_norm_def, rule sup_ub)  wenzelm@9035  287  from ex_fnorm [OF _ c]  wenzelm@9035  288  show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"  wenzelm@9035  289  by (simp! add: is_function_norm_def function_norm_def)  bauerg@9379  290  show "|f x| * rinv (norm x) \\ B V norm f"  wenzelm@7978  291  by (unfold B_def, intro UnI2 CollectI exI [of _ x]  wenzelm@9035  292  conjI, simp)  wenzelm@9035  293  qed  wenzelm@7917  294 wenzelm@9035  295  txt {* The thesis now follows by a short calculation: *}  wenzelm@7917  296 bauerg@9374  297  have "|f x| = |f x| * #1" by (simp!)  bauerg@9374  298  also from nz have "#1 = rinv (norm x) * norm x"  bauerg@9379  299  by (simp add: real_mult_inv_left1)  bauerg@9379  300  also have "|f x| * ... = |f x| * rinv (norm x) * norm x"  bauerg@9374  301  by (simp! add: real_mult_assoc)  bauerg@9379  302  also from n l have "... <= \\f\\V,norm * norm x"  bauerg@9379  303  by (simp add: real_mult_le_le_mono2)  bauerg@9379  304  finally show "|f x| <= \\f\\V,norm * norm x" .  wenzelm@9035  305  qed  wenzelm@9035  306 qed  wenzelm@7535  307 wenzelm@7978  308 text{* \medskip The function norm is the least positive real number for  wenzelm@7978  309 which the following inequation holds:  wenzelm@7917  310 \begin{matharray}{l}  wenzelm@7917  311 | f\ap x | \leq c \cdot {\norm x}  wenzelm@7917  312 \end{matharray}  wenzelm@9035  313 *}  wenzelm@7917  314 wenzelm@7535  315 lemma fnorm_le_ub:  bauerg@9374  316  "[| is_continuous V norm f; is_normed_vectorspace V norm;  bauerg@9379  317  \\x \\ V. |f x| <= c * norm x; #0 <= c |]  bauerg@9379  318  ==> \\f\\V,norm <= c"  wenzelm@9035  319 proof (unfold function_norm_def)  wenzelm@9035  320  assume "is_normed_vectorspace V norm"  wenzelm@9035  321  assume c: "is_continuous V norm f"  bauerg@9379  322  assume fb: "\\x \\ V. |f x| <= c * norm x"  bauerg@9379  323  and "#0 <= c"  wenzelm@7917  324 wenzelm@7917  325  txt {* Suppose the inequation holds for some $c\geq 0$.  wenzelm@7917  326  If $c$ is an upper bound of $B$, then $c$ is greater  wenzelm@7917  327  than the function norm since the function norm is the  wenzelm@7917  328  least upper bound.  wenzelm@9035  329  *}  wenzelm@7917  330 wenzelm@9035  331  show "Sup UNIV (B V norm f) <= c"  wenzelm@9035  332  proof (rule sup_le_ub)  wenzelm@9035  333  from ex_fnorm [OF _ c]  wenzelm@9035  334  show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"  wenzelm@9035  335  by (simp! add: is_function_norm_def function_norm_def)  wenzelm@7917  336   bauerg@9374  337  txt {* $c$ is an upper bound of $B$, i.e. every  wenzelm@9035  338  $y\in B$ is less than $c$. *}  wenzelm@7917  339 wenzelm@9035  340  show "isUb UNIV (B V norm f) c"  wenzelm@9035  341  proof (intro isUbI setleI ballI)  bauerg@9379  342  fix y assume "y \\ B V norm f"  wenzelm@9035  343  thus le: "y <= c"  wenzelm@9035  344  proof (unfold B_def, elim UnE CollectE exE conjE singletonE)  wenzelm@7917  345 wenzelm@9035  346  txt {* The first case for $y\in B$ is $y=0$. *}  wenzelm@7917  347 wenzelm@9035  348  assume "y = #0"  wenzelm@9035  349  show "y <= c" by (force!)  wenzelm@7917  350 wenzelm@7917  351  txt{* The second case is  wenzelm@7978  352  $y = {|f\ap x|}/{\norm x}$ for some  wenzelm@9035  353  $x\in V$ with $x \neq \zero$. *}  wenzelm@7917  354 wenzelm@9035  355  next  wenzelm@9035  356  fix x  bauerg@9379  357  assume "x \\ V" "x \\ 0"  wenzelm@7917  358 wenzelm@9035  359  have lz: "#0 < norm x"  wenzelm@9035  360  by (simp! add: normed_vs_norm_gt_zero)  wenzelm@7566  361   bauerg@9379  362  have nz: "norm x \\ #0"  wenzelm@9035  363  proof (rule not_sym)  bauerg@9379  364  from lz show "#0 \\ norm x"  wenzelm@9035  365  by (simp! add: order_less_imp_not_eq)  wenzelm@9035  366  qed  wenzelm@7566  367   wenzelm@9035  368  from lz have "#0 < rinv (norm x)"  wenzelm@9035  369  by (simp! add: real_rinv_gt_zero1)  wenzelm@9035  370  hence rinv_gez: "#0 <= rinv (norm x)"  wenzelm@9035  371  by (rule real_less_imp_le)  wenzelm@7535  372 bauerg@9374  373  assume "y = |f x| * rinv (norm x)"  wenzelm@9035  374  also from rinv_gez have "... <= c * norm x * rinv (norm x)"  wenzelm@9035  375  proof (rule real_mult_le_le_mono2)  bauerg@9374  376  show "|f x| <= c * norm x" by (rule bspec)  wenzelm@9035  377  qed  wenzelm@9035  378  also have "... <= c" by (simp add: nz real_mult_assoc)  wenzelm@9035  379  finally show ?thesis .  wenzelm@9035  380  qed  wenzelm@9035  381  qed force  wenzelm@9035  382  qed  wenzelm@9035  383 qed  wenzelm@7535  384 wenzelm@9035  385 end