src/HOL/Real/HahnBanach/FunctionNorm.thy
 author wenzelm Tue Sep 21 17:31:20 1999 +0200 (1999-09-21) changeset 7566 c5a3f980a7af parent 7535 599d3414b51d child 7567 62384a807775 permissions -rw-r--r--
accomodate refined facts handling;
```     1 (*  Title:      HOL/Real/HahnBanach/FunctionNorm.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Gertrud Bauer, TU Munich
```
```     4 *)
```
```     5
```
```     6 theory FunctionNorm = NormedSpace + FunctionOrder:;
```
```     7
```
```     8
```
```     9 constdefs
```
```    10   is_continous :: "['a set, 'a => real, 'a => real] => bool"
```
```    11   "is_continous V norm f == (is_linearform V f
```
```    12                            & (EX c. ALL x:V. rabs (f x) <= c * norm x))";
```
```    13
```
```    14 lemma lipschitz_continousI [intro]:
```
```    15   "[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |]
```
```    16   ==> is_continous V norm f";
```
```    17 proof (unfold is_continous_def, intro exI conjI ballI);
```
```    18   assume r: "!! x. x:V ==> rabs (f x) <= c * norm x";
```
```    19   fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
```
```    20 qed;
```
```    21
```
```    22 lemma continous_linearform [intro!!]: "is_continous V norm f ==> is_linearform V f";
```
```    23   by (unfold is_continous_def) force;
```
```    24
```
```    25 lemma continous_bounded [intro!!]:
```
```    26   "is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
```
```    27   by (unfold is_continous_def) force;
```
```    28
```
```    29 constdefs
```
```    30   B:: "[ 'a set, 'a => real, 'a => real ] => real set"
```
```    31   "B V norm f == {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm (x)))}";
```
```    32
```
```    33 constdefs
```
```    34   function_norm :: " ['a set, 'a => real, 'a => real] => real"
```
```    35   "function_norm V norm f ==
```
```    36      Sup UNIV (B V norm f)";
```
```    37
```
```    38 constdefs
```
```    39   is_function_norm :: " ['a set, 'a => real, 'a => real] => real => bool"
```
```    40   "is_function_norm V norm f fn ==
```
```    41      is_Sup UNIV (B V norm f) fn";
```
```    42
```
```    43 lemma B_not_empty: "0r : B V norm f";
```
```    44   by (unfold B_def, force);
```
```    45
```
```    46 lemma ex_fnorm [intro!!]:
```
```    47   "[| is_normed_vectorspace V norm; is_continous V norm f|]
```
```    48      ==> is_function_norm V norm f (function_norm V norm f)";
```
```    49 proof (unfold function_norm_def is_function_norm_def is_continous_def Sup_def, elim conjE,
```
```    50     rule selectI2EX);
```
```    51   assume "is_normed_vectorspace V norm";
```
```    52   assume "is_linearform V f" and e: "EX c. ALL x:V. rabs (f x) <= c * norm x";
```
```    53   show  "EX a. is_Sup UNIV (B V norm f) a";
```
```    54   proof (unfold is_Sup_def, rule reals_complete);
```
```    55     show "EX X. X : B V norm f";
```
```    56     proof (intro exI);
```
```    57       show "0r : (B V norm f)"; by (unfold B_def, force);
```
```    58     qed;
```
```    59
```
```    60     from e; show "EX Y. isUb UNIV (B V norm f) Y";
```
```    61     proof;
```
```    62       fix c; assume a: "ALL x:V. rabs (f x) <= c * norm x";
```
```    63       def b == "max c 0r";
```
```    64
```
```    65       show "EX Y. isUb UNIV (B V norm f) Y";
```
```    66       proof (intro exI isUbI setleI ballI, unfold B_def,
```
```    67 	elim CollectE disjE bexE conjE);
```
```    68 	fix x y; assume "x:V" "x ~= <0>" "y = rabs (f x) * rinv (norm x)";
```
```    69         from a; have le: "rabs (f x) <= c * norm x"; ..;
```
```    70         have "y = rabs (f x) * rinv (norm x)";.;
```
```    71         also; from _  le; have "... <= c * norm x * rinv (norm x)";
```
```    72         proof (rule real_mult_le_le_mono2);
```
```    73           show "0r <= rinv (norm x)";
```
```    74           proof (rule less_imp_le);
```
```    75             show "0r < rinv (norm x)";
```
```    76             proof (rule real_rinv_gt_zero);
```
```    77               show "0r < norm x"; ..;
```
```    78             qed;
```
```    79           qed;
```
```    80      (*** or:  by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero); ***)
```
```    81         qed;
```
```    82         also; have "... = c * (norm x * rinv (norm x))"; by (rule real_mult_assoc);
```
```    83         also; have "(norm x * rinv (norm x)) = 1r";
```
```    84         proof (rule real_mult_inv_right);
```
```    85           show "norm x ~= 0r";
```
```    86           proof (rule not_sym);
```
```    87             show "0r ~= norm x";
```
```    88             proof (rule lt_imp_not_eq);
```
```    89               show "0r < norm x"; ..;
```
```    90             qed;
```
```    91           qed;
```
```    92      (*** or:  by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero); ***)
```
```    93         qed;
```
```    94         also; have "c * ... = c"; by (simp!);
```
```    95         also; have "... <= b"; by (simp! add: le_max1);
```
```    96 	finally; show "y <= b"; .;
```
```    97       next;
```
```    98 	fix y; assume "y = 0r"; show "y <= b"; by (simp! add: le_max2);
```
```    99       qed simp;
```
```   100     qed;
```
```   101   qed;
```
```   102 qed;
```
```   103
```
```   104 lemma fnorm_ge_zero [intro!!]: "[| is_continous V norm f; is_normed_vectorspace V norm|]
```
```   105    ==> 0r <= function_norm V norm f";
```
```   106 proof -;
```
```   107   assume c: "is_continous V norm f" and n: "is_normed_vectorspace V norm";
```
```   108   have "is_function_norm V norm f (function_norm V norm f)"; ..;
```
```   109   hence s: "is_Sup UNIV (B V norm f) (function_norm V norm f)";
```
```   110     by (simp add: is_function_norm_def);
```
```   111   show ?thesis;
```
```   112   proof (unfold function_norm_def, rule sup_ub1);
```
```   113     show "ALL x:(B V norm f). 0r <= x";
```
```   114     proof (intro ballI, unfold B_def, elim CollectE bexE conjE disjE);
```
```   115       fix x r; assume "x : V" "x ~= <0>"
```
```   116         "r = rabs (f x) * rinv (norm x)";
```
```   117       show  "0r <= r";
```
```   118       proof (simp!, rule real_le_mult_order);
```
```   119         show "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
```
```   120         show "0r <= rinv (norm x)";
```
```   121         proof (rule less_imp_le);
```
```   122           show "0r < rinv (norm x)";
```
```   123           proof (rule real_rinv_gt_zero);
```
```   124             show "0r < norm x"; ..;
```
```   125           qed;
```
```   126         qed;
```
```   127       qed;
```
```   128     qed (simp!);
```
```   129     from ex_fnorm [OF n c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
```
```   130       by (simp! add: is_function_norm_def function_norm_def);
```
```   131     show "0r : B V norm f"; by (rule B_not_empty);
```
```   132   qed;
```
```   133 qed;
```
```   134
```
```   135
```
```   136 lemma norm_fx_le_norm_f_norm_x:
```
```   137   "[| is_normed_vectorspace V norm; x:V; is_continous V norm f |]
```
```   138     ==> rabs (f x) <= (function_norm V norm f) * norm x";
```
```   139 proof -;
```
```   140   assume "is_normed_vectorspace V norm" "x:V" and c: "is_continous V norm f";
```
```   141   have v: "is_vectorspace V"; ..;
```
```   142   assume "x:V";
```
```   143   show "?thesis";
```
```   144   proof (rule case [of "x = <0>"]);
```
```   145     assume "x ~= <0>";
```
```   146     show "?thesis";
```
```   147     proof -;
```
```   148       have n: "0r <= norm x"; ..;
```
```   149       have le: "rabs (f x) * rinv (norm x) <= function_norm V norm f";
```
```   150         proof (unfold function_norm_def, rule sup_ub);
```
```   151           from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
```
```   152              by (simp! add: is_function_norm_def function_norm_def);
```
```   153           show "rabs (f x) * rinv (norm x) : B V norm f";
```
```   154             by (unfold B_def, intro CollectI disjI2 bexI [of _ x] conjI, simp);
```
```   155         qed;
```
```   156       have "rabs (f x) = rabs (f x) * 1r"; by (simp!);
```
```   157       also; have "1r = rinv (norm x) * norm x";
```
```   158       proof (rule real_mult_inv_left [RS sym]);
```
```   159         show "norm x ~= 0r";
```
```   160         proof (rule lt_imp_not_eq[RS not_sym]);
```
```   161           show "0r < norm x"; ..;
```
```   162         qed;
```
```   163       qed;
```
```   164       also; have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x";
```
```   165         by (simp! add: real_mult_assoc [of "rabs (f x)"]);
```
```   166       also; have "rabs (f x) * rinv (norm x) * norm x <= function_norm V norm f * norm x";
```
```   167         by (rule real_mult_le_le_mono2 [OF n le]);
```
```   168       finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
```
```   169     qed;
```
```   170   next;
```
```   171     assume "x = <0>";
```
```   172     then; show "?thesis";
```
```   173     proof -;
```
```   174       have "rabs (f x) = rabs (f <0>)"; by (simp!);
```
```   175       also; from v continous_linearform; have "f <0> = 0r"; ..;
```
```   176       also; note rabs_zero;
```
```   177       also; have" 0r <= function_norm V norm f * norm x";
```
```   178       proof (rule real_le_mult_order);
```
```   179         show "0r <= function_norm V norm f"; ..;
```
```   180         show "0r <= norm x"; ..;
```
```   181       qed;
```
```   182       finally; show "rabs (f x) <= function_norm V norm f * norm x"; .;
```
```   183     qed;
```
```   184   qed;
```
```   185 qed;
```
```   186
```
```   187
```
```   188
```
```   189
```
```   190 lemma fnorm_le_ub:
```
```   191   "[| is_normed_vectorspace V norm; is_continous V norm f;
```
```   192      ALL x:V. rabs (f x) <= c * norm x; 0r <= c |]
```
```   193   ==> function_norm V norm f <= c";
```
```   194 proof (unfold function_norm_def);
```
```   195   assume "is_normed_vectorspace V norm";
```
```   196   assume c: "is_continous V norm f";
```
```   197   assume fb: "ALL x:V. rabs (f x) <= c * norm x"
```
```   198          and "0r <= c";
```
```   199   show "Sup UNIV (B V norm f) <= c";
```
```   200   proof (rule ub_ge_sup);
```
```   201     from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
```
```   202       by (simp! add: is_function_norm_def function_norm_def);
```
```   203     show "isUb UNIV (B V norm f) c";
```
```   204     proof (intro isUbI setleI ballI);
```
```   205       fix y; assume "y: B V norm f";
```
```   206       thus le: "y <= c";
```
```   207       proof (-, unfold B_def, elim CollectE disjE bexE);
```
```   208 	fix x; assume Px: "x ~= <0> & y = rabs (f x) * rinv (norm x)";
```
```   209 	assume x: "x : V";
```
```   210         have lt: "0r < norm x";  by (simp! add: normed_vs_norm_gt_zero);
```
```   211
```
```   212         have neq: "norm x ~= 0r";
```
```   213         proof (rule not_sym);
```
```   214           from lt; show "0r ~= norm x";
```
```   215           by (simp! add: order_less_imp_not_eq);
```
```   216         qed;
```
```   217
```
```   218 	from lt; have "0r < rinv (norm x)";
```
```   219 	  by (simp! add: real_rinv_gt_zero);
```
```   220 	then; have inv_leq: "0r <= rinv (norm x)"; by (rule less_imp_le);
```
```   221
```
```   222 	from Px; have "y = rabs (f x) * rinv (norm x)"; ..;
```
```   223 	also; from inv_leq; have "... <= c * norm x * rinv (norm x)";
```
```   224 	  proof (rule real_mult_le_le_mono2);
```
```   225 	    from fb x; show "rabs (f x) <= c * norm x"; ..;
```
```   226 	  qed;
```
```   227 	also; have "... <= c";
```
```   228 	  by (simp add: neq real_mult_assoc);
```
```   229 	finally; show ?thesis; .;
```
```   230       next;
```
```   231         assume "y = 0r";
```
```   232         show "y <= c"; by (force!);
```
```   233       qed;
```
```   234     qed force;
```
```   235   qed;
```
```   236 qed;
```
```   237
```
```   238
```
```   239 end;
```
```   240
```