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