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