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