src/HOL/Hahn_Banach/Function_Norm.thy
 author hoelzl Thu Sep 02 10:14:32 2010 +0200 (2010-09-02) changeset 39072 1030b1a166ef parent 36778 739a9379e29b child 44887 7ca82df6e951 permissions -rw-r--r--
 wenzelm@31795  1 (* Title: HOL/Hahn_Banach/Function_Norm.thy  wenzelm@7566  2  Author: Gertrud Bauer, TU Munich  wenzelm@7566  3 *)  wenzelm@7535  4 wenzelm@9035  5 header {* The norm of a function *}  wenzelm@7808  6 wenzelm@31795  7 theory Function_Norm  wenzelm@31795  8 imports Normed_Space Function_Order  wenzelm@27612  9 begin  wenzelm@7535  10 wenzelm@9035  11 subsection {* Continuous linear forms*}  wenzelm@7917  12 wenzelm@10687  13 text {*  wenzelm@11472  14  A linear form @{text f} on a normed vector space @{text "(V, \\\)"}  wenzelm@13515  15  is \emph{continuous}, iff it is bounded, i.e.  wenzelm@10687  16  \begin{center}  wenzelm@11472  17  @{text "\c \ R. \x \ V. \f x\ \ c \ \x\"}  wenzelm@10687  18  \end{center}  wenzelm@10687  19  In our application no other functions than linear forms are  wenzelm@10687  20  considered, so we can define continuous linear forms as bounded  wenzelm@10687  21  linear forms:  wenzelm@9035  22 *}  wenzelm@7535  23 ballarin@29234  24 locale continuous = var_V + norm_syntax + linearform +  wenzelm@13515  25  assumes bounded: "\c. \x \ V. \f x\ \ c * \x\"  wenzelm@7535  26 ballarin@14254  27 declare continuous.intro [intro?] continuous_axioms.intro [intro?]  ballarin@14254  28 wenzelm@10687  29 lemma continuousI [intro]:  ballarin@27611  30  fixes norm :: "_ \ real" ("\_\")  ballarin@27611  31  assumes "linearform V f"  wenzelm@13515  32  assumes r: "\x. x \ V \ \f x\ \ c * \x\"  wenzelm@13515  33  shows "continuous V norm f"  wenzelm@13515  34 proof  wenzelm@23378  35  show "linearform V f" by fact  wenzelm@13515  36  from r have "\c. \x\V. \f x\ \ c * \x\" by blast  wenzelm@13515  37  then show "continuous_axioms V norm f" ..  wenzelm@13515  38 qed  wenzelm@7535  39 wenzelm@11472  40 wenzelm@13515  41 subsection {* The norm of a linear form *}  wenzelm@7917  42 wenzelm@10687  43 text {*  wenzelm@10687  44  The least real number @{text c} for which holds  wenzelm@10687  45  \begin{center}  wenzelm@11472  46  @{text "\x \ V. \f x\ \ c \ \x\"}  wenzelm@10687  47  \end{center}  wenzelm@10687  48  is called the \emph{norm} of @{text f}.  wenzelm@7917  49 wenzelm@11472  50  For non-trivial vector spaces @{text "V \ {0}"} the norm can be  wenzelm@10687  51  defined as  wenzelm@10687  52  \begin{center}  wenzelm@11472  53  @{text "\f\ = \x \ 0. \f x\ / \x\"}  wenzelm@10687  54  \end{center}  wenzelm@7917  55 wenzelm@10687  56  For the case @{text "V = {0}"} the supremum would be taken from an  wenzelm@11472  57  empty set. Since @{text \} is unbounded, there would be no supremum.  wenzelm@10687  58  To avoid this situation it must be guaranteed that there is an  wenzelm@11472  59  element in this set. This element must be @{text "{} \ 0"} so that  wenzelm@13547  60  @{text fn_norm} has the norm properties. Furthermore it does not  wenzelm@13547  61  have to change the norm in all other cases, so it must be @{text 0},  wenzelm@13547  62  as all other elements are @{text "{} \ 0"}.  wenzelm@7917  63 wenzelm@13515  64  Thus we define the set @{text B} where the supremum is taken from as  wenzelm@13515  65  follows:  wenzelm@10687  66  \begin{center}  wenzelm@11472  67  @{text "{0} \ {\f x\ / \x\. x \ 0 \ x \ F}"}  wenzelm@10687  68  \end{center}  wenzelm@10687  69 wenzelm@13547  70  @{text fn_norm} is equal to the supremum of @{text B}, if the  wenzelm@13515  71  supremum exists (otherwise it is undefined).  wenzelm@9035  72 *}  wenzelm@7917  73 wenzelm@13547  74 locale fn_norm = norm_syntax +  wenzelm@13547  75  fixes B defines "B V f \ {0} \ {\f x\ / \x\ | x. x \ 0 \ x \ V}"  wenzelm@13547  76  fixes fn_norm ("\_\\_" [0, 1000] 999)  wenzelm@13515  77  defines "\f\\V \ $$B V f)"  wenzelm@7535  78 ballarin@27611  79 locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm  ballarin@27611  80 wenzelm@13547  81 lemma (in fn_norm) B_not_empty [intro]: "0 \ B V f"  wenzelm@13547  82  by (simp add: B_def)  wenzelm@7917  83 wenzelm@10687  84 text {*  wenzelm@10687  85  The following lemma states that every continuous linear form on a  wenzelm@11472  86  normed space @{text "(V, \\$$"} has a function norm.  wenzelm@10687  87 *}  wenzelm@10687  88 ballarin@27611  89 lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:  ballarin@27611  90  assumes "continuous V norm f"  wenzelm@13515  91  shows "lub (B V f) (\f\\V)"  wenzelm@13515  92 proof -  ballarin@29234  93  interpret continuous V norm f by fact  wenzelm@10687  94  txt {* The existence of the supremum is shown using the  wenzelm@13515  95  completeness of the reals. Completeness means, that every  wenzelm@13515  96  non-empty bounded set of reals has a supremum. *}  wenzelm@13515  97  have "\a. lub (B V f) a"  wenzelm@13515  98  proof (rule real_complete)  wenzelm@10687  99  txt {* First we have to show that @{text B} is non-empty: *}  wenzelm@13515  100  have "0 \ B V f" ..  wenzelm@27612  101  then show "\x. x \ B V f" ..  wenzelm@7535  102 wenzelm@10687  103  txt {* Then we have to show that @{text B} is bounded: *}  wenzelm@13515  104  show "\c. \y \ B V f. y \ c"  wenzelm@13515  105  proof -  wenzelm@10687  106  txt {* We know that @{text f} is bounded by some value @{text c}. *}  wenzelm@13515  107  from bounded obtain c where c: "\x \ V. \f x\ \ c * \x\" ..  wenzelm@7535  108 wenzelm@13515  109  txt {* To prove the thesis, we have to show that there is some  wenzelm@13515  110  @{text b}, such that @{text "y \ b"} for all @{text "y \  wenzelm@13515  111  B"}. Due to the definition of @{text B} there are two cases. *}  wenzelm@7917  112 wenzelm@13515  113  def b \ "max c 0"  wenzelm@13515  114  have "\y \ B V f. y \ b"  wenzelm@13515  115  proof  wenzelm@13515  116  fix y assume y: "y \ B V f"  wenzelm@13515  117  show "y \ b"  wenzelm@13515  118  proof cases  wenzelm@13515  119  assume "y = 0"  wenzelm@27612  120  then show ?thesis unfolding b_def by arith  wenzelm@13515  121  next  wenzelm@13515  122  txt {* The second case is @{text "y = \f x\ / \x\"} for some  wenzelm@13515  123  @{text "x \ V"} with @{text "x \ 0"}. *}  wenzelm@13515  124  assume "y \ 0"  wenzelm@13515  125  with y obtain x where y_rep: "y = \f x\ * inverse \x\"  wenzelm@13515  126  and x: "x \ V" and neq: "x \ 0"  huffman@36778  127  by (auto simp add: B_def divide_inverse)  wenzelm@13515  128  from x neq have gt: "0 < \x\" ..  wenzelm@7917  129 wenzelm@13515  130  txt {* The thesis follows by a short calculation using the  wenzelm@13515  131  fact that @{text f} is bounded. *}  wenzelm@13515  132 wenzelm@13515  133  note y_rep  wenzelm@13515  134  also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\"  paulson@14334  135  proof (rule mult_right_mono)  wenzelm@23378  136  from c x show "\f x\ \ c * \x\" ..  paulson@14334  137  from gt have "0 < inverse \x\"  paulson@14334  138  by (rule positive_imp_inverse_positive)  wenzelm@27612  139  then show "0 \ inverse \x\" by (rule order_less_imp_le)  wenzelm@13515  140  qed  wenzelm@13515  141  also have "\ = c * (\x\ * inverse \x\)"  huffman@36778  142  by (rule Groups.mult_assoc)  wenzelm@13515  143  also  wenzelm@13515  144  from gt have "\x\ \ 0" by simp  wenzelm@27612  145  then have "\x\ * inverse \x\ = 1" by simp  wenzelm@13515  146  also have "c * 1 \ b" by (simp add: b_def le_maxI1)  wenzelm@13515  147  finally show "y \ b" .  wenzelm@9035  148  qed  wenzelm@13515  149  qed  wenzelm@27612  150  then show ?thesis ..  wenzelm@9035  151  qed  wenzelm@9035  152  qed  wenzelm@27612  153  then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)  wenzelm@13515  154 qed  wenzelm@13515  155 ballarin@27611  156 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:  ballarin@27611  157  assumes "continuous V norm f"  wenzelm@13515  158  assumes b: "b \ B V f"  wenzelm@13515  159  shows "b \ \f\\V"  wenzelm@13515  160 proof -  ballarin@29234  161  interpret continuous V norm f by fact  wenzelm@13547  162  have "lub (B V f) (\f\\V)"  wenzelm@23378  163  using continuous V norm f by (rule fn_norm_works)  wenzelm@13515  164  from this and b show ?thesis ..  wenzelm@13515  165 qed  wenzelm@13515  166 ballarin@27611  167 lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:  ballarin@27611  168  assumes "continuous V norm f"  wenzelm@13515  169  assumes b: "\b. b \ B V f \ b \ y"  wenzelm@13515  170  shows "\f\\V \ y"  wenzelm@13515  171 proof -  ballarin@29234  172  interpret continuous V norm f by fact  wenzelm@13547  173  have "lub (B V f) (\f\\V)"  wenzelm@23378  174  using continuous V norm f by (rule fn_norm_works)  wenzelm@13515  175  from this and b show ?thesis ..  wenzelm@9035  176 qed  wenzelm@7535  177 wenzelm@11472  178 text {* The norm of a continuous function is always @{text "\ 0"}. *}  wenzelm@7917  179 ballarin@27611  180 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:  ballarin@27611  181  assumes "continuous V norm f"  wenzelm@13515  182  shows "0 \ \f\\V"  wenzelm@9035  183 proof -  ballarin@29234  184  interpret continuous V norm f by fact  wenzelm@10687  185  txt {* The function norm is defined as the supremum of @{text B}.  wenzelm@13515  186  So it is @{text "\ 0"} if all elements in @{text B} are @{text "\  wenzelm@13515  187  0"}, provided the supremum exists and @{text B} is not empty. *}  wenzelm@13547  188  have "lub (B V f) (\f\\V)"  wenzelm@23378  189  using continuous V norm f by (rule fn_norm_works)  wenzelm@13515  190  moreover have "0 \ B V f" ..  wenzelm@13515  191  ultimately show ?thesis ..  wenzelm@9035  192 qed  wenzelm@10687  193 wenzelm@10687  194 text {*  wenzelm@10687  195  \medskip The fundamental property of function norms is:  wenzelm@10687  196  \begin{center}  wenzelm@11472  197  @{text "\f x\ \ \f\ \ \x\"}  wenzelm@10687  198  \end{center}  wenzelm@9035  199 *}  wenzelm@7917  200 ballarin@27611  201 lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:  ballarin@27611  202  assumes "continuous V norm f" "linearform V f"  wenzelm@13515  203  assumes x: "x \ V"  wenzelm@13515  204  shows "\f x\ \ \f\\V * \x\"  ballarin@27611  205 proof -  ballarin@29234  206  interpret continuous V norm f by fact  wenzelm@29291  207  interpret linearform V f by fact  wenzelm@27612  208  show ?thesis  wenzelm@27612  209  proof cases  ballarin@27611  210  assume "x = 0"  ballarin@27611  211  then have "\f x\ = \f 0\" by simp  ballarin@27611  212  also have "f 0 = 0" by rule unfold_locales  ballarin@27611  213  also have "\\\ = 0" by simp  ballarin@27611  214  also have a: "0 \ \f\\V"  ballarin@27611  215  using continuous V norm f by (rule fn_norm_ge_zero)  ballarin@27611  216  from x have "0 \ norm x" ..  ballarin@27611  217  with a have "0 \ \f\\V * \x\" by (simp add: zero_le_mult_iff)  ballarin@27611  218  finally show "\f x\ \ \f\\V * \x\" .  ballarin@27611  219  next  ballarin@27611  220  assume "x \ 0"  ballarin@27611  221  with x have neq: "\x\ \ 0" by simp  ballarin@27611  222  then have "\f x\ = (\f x\ * inverse \x\) * \x\" by simp  ballarin@27611  223  also have "\ \ \f\\V * \x\"  ballarin@27611  224  proof (rule mult_right_mono)  ballarin@27611  225  from x show "0 \ \x\" ..  ballarin@27611  226  from x and neq have "\f x\ * inverse \x\ \ B V f"  huffman@36778  227  by (auto simp add: B_def divide_inverse)  ballarin@27611  228  with continuous V norm f show "\f x\ * inverse \x\ \ \f\\V"  wenzelm@32960  229  by (rule fn_norm_ub)  ballarin@27611  230  qed  ballarin@27611  231  finally show ?thesis .  wenzelm@9035  232  qed  wenzelm@9035  233 qed  wenzelm@7535  234 wenzelm@10687  235 text {*  wenzelm@10687  236  \medskip The function norm is the least positive real number for  wenzelm@10687  237  which the following inequation holds:  wenzelm@10687  238  \begin{center}  wenzelm@13515  239  @{text "\f x\ \ c \ \x\"}  wenzelm@10687  240  \end{center}  wenzelm@9035  241 *}  wenzelm@7917  242 ballarin@27611  243 lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:  ballarin@27611  244  assumes "continuous V norm f"  wenzelm@13515  245  assumes ineq: "\x \ V. \f x\ \ c * \x\" and ge: "0 \ c"  wenzelm@13515  246  shows "\f\\V \ c"  ballarin@27611  247 proof -  ballarin@29234  248  interpret continuous V norm f by fact  wenzelm@27612  249  show ?thesis  wenzelm@27612  250  proof (rule fn_norm_leastB [folded B_def fn_norm_def])  ballarin@27611  251  fix b assume b: "b \ B V f"  ballarin@27611  252  show "b \ c"  ballarin@27611  253  proof cases  ballarin@27611  254  assume "b = 0"  ballarin@27611  255  with ge show ?thesis by simp  ballarin@27611  256  next  ballarin@27611  257  assume "b \ 0"  ballarin@27611  258  with b obtain x where b_rep: "b = \f x\ * inverse \x\"  wenzelm@13515  259  and x_neq: "x \ 0" and x: "x \ V"  huffman@36778  260  by (auto simp add: B_def divide_inverse)  ballarin@27611  261  note b_rep  ballarin@27611  262  also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\"  ballarin@27611  263  proof (rule mult_right_mono)  wenzelm@32960  264  have "0 < \x\" using x x_neq ..  wenzelm@32960  265  then show "0 \ inverse \x\" by simp  wenzelm@32960  266  from ineq and x show "\f x\ \ c * \x\" ..  ballarin@27611  267  qed  ballarin@27611  268  also have "\ = c"  ballarin@27611  269  proof -  wenzelm@32960  270  from x_neq and x have "\x\ \ 0" by simp  wenzelm@32960  271  then show ?thesis by simp  ballarin@27611  272  qed  ballarin@27611  273  finally show ?thesis .  wenzelm@13515  274  qed  ballarin@27611  275  qed (insert continuous V norm f, simp_all add: continuous_def)  ballarin@27611  276 qed  wenzelm@7535  277 wenzelm@10687  278 end