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