src/HOL/Real/HahnBanach/FunctionNorm.thy
author wenzelm
Fri Oct 22 20:14:31 1999 +0200 (1999-10-22)
changeset 7917 5e5b9813cce7
parent 7808 fd019ac3485f
child 7927 b50446a33c16
permissions -rw-r--r--
HahnBanach update by Gertrud Bauer;
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@7808
     6
header {* The norm of a function *};
wenzelm@7808
     7
wenzelm@7535
     8
theory FunctionNorm = NormedSpace + FunctionOrder:;
wenzelm@7535
     9
wenzelm@7917
    10
subsection {* Continous linearforms*};
wenzelm@7917
    11
wenzelm@7917
    12
text{* A linearform $f$ on a normed vector space $(V, \norm{\cdot})$
wenzelm@7917
    13
is \emph{continous}, iff it is bounded, i.~e.
wenzelm@7917
    14
\[\exists\ap c\in R.\ap \forall\ap x\in V.\ap 
wenzelm@7917
    15
|f\ap x| \leq c \cdot \norm x.\]
wenzelm@7917
    16
In our application no other functions than linearforms are considered,
wenzelm@7917
    17
so we can define continous linearforms as follows:
wenzelm@7917
    18
*};
wenzelm@7535
    19
wenzelm@7535
    20
constdefs
wenzelm@7917
    21
  is_continous ::
wenzelm@7917
    22
  "['a::{minus, plus} set, 'a => real, 'a => real] => bool" 
wenzelm@7808
    23
  "is_continous V norm f == 
wenzelm@7917
    24
    is_linearform V f & (EX c. ALL x:V. rabs (f x) <= c * norm x)";
wenzelm@7535
    25
wenzelm@7917
    26
lemma continousI [intro]: 
wenzelm@7535
    27
  "[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |] 
wenzelm@7535
    28
  ==> is_continous V norm f";
wenzelm@7535
    29
proof (unfold is_continous_def, intro exI conjI ballI);
wenzelm@7535
    30
  assume r: "!! x. x:V ==> rabs (f x) <= c * norm x"; 
wenzelm@7535
    31
  fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
wenzelm@7535
    32
qed;
wenzelm@7535
    33
  
wenzelm@7808
    34
lemma continous_linearform [intro!!]: 
wenzelm@7808
    35
  "is_continous V norm f ==> is_linearform V f";
wenzelm@7535
    36
  by (unfold is_continous_def) force;
wenzelm@7535
    37
wenzelm@7566
    38
lemma continous_bounded [intro!!]:
wenzelm@7917
    39
  "is_continous V norm f 
wenzelm@7917
    40
  ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
wenzelm@7535
    41
  by (unfold is_continous_def) force;
wenzelm@7535
    42
wenzelm@7917
    43
subsection{* The norm of a linearform *};
wenzelm@7917
    44
wenzelm@7917
    45
wenzelm@7917
    46
text{* The least real number $c$ for which holds
wenzelm@7917
    47
\[\forall\ap x\in V.\ap |f\ap x| \leq c \cdot \norm x\]
wenzelm@7917
    48
is called the \emph{norm} of $f$.
wenzelm@7917
    49
wenzelm@7917
    50
For the non-trivial vector space $V$ the norm can be defined as 
wenzelm@7917
    51
\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}. \] 
wenzelm@7917
    52
wenzelm@7917
    53
For the case that the vector space $V$ contains only the zero vector 
wenzelm@7917
    54
set, the set $B$ this supremum is taken from would be empty, and any 
wenzelm@7917
    55
real number is a supremum of $B$. So it must be guarateed that there 
wenzelm@7917
    56
is an element in $B$. This element must be greater or equal $0$ so 
wenzelm@7917
    57
that $\idt{function{\dsh}norm}$ has the norm properties. Furthermore 
wenzelm@7917
    58
it does not have to change the norm in all other cases, so it must be
wenzelm@7917
    59
$0$, as all other elements of $B$ are greater or equal $0$.
wenzelm@7917
    60
wenzelm@7917
    61
Thus $B$ is defined as follows.
wenzelm@7917
    62
*};
wenzelm@7917
    63
wenzelm@7535
    64
constdefs
wenzelm@7917
    65
  B :: "[ 'a set, 'a => real, 'a => real ] => real set"
wenzelm@7808
    66
  "B V norm f == 
wenzelm@7917
    67
  {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm x))}";
wenzelm@7917
    68
wenzelm@7917
    69
text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
wenzelm@7917
    70
if there exists a supremum. *};
wenzelm@7535
    71
wenzelm@7535
    72
constdefs 
wenzelm@7535
    73
  function_norm :: " ['a set, 'a => real, 'a => real] => real"
wenzelm@7917
    74
  "function_norm V norm f == Sup UNIV (B V norm f)";
wenzelm@7917
    75
wenzelm@7917
    76
text{* $\idt{is{\dsh}function{\dsh}norm}$ also guarantees that there 
wenzelm@7917
    77
is a funciton norm .*};
wenzelm@7535
    78
wenzelm@7535
    79
constdefs 
wenzelm@7917
    80
  is_function_norm :: 
wenzelm@7917
    81
  " ['a set, 'a => real, 'a => real] => real => bool"
wenzelm@7917
    82
  "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn";
wenzelm@7535
    83
wenzelm@7535
    84
lemma B_not_empty: "0r : B V norm f";
wenzelm@7535
    85
  by (unfold B_def, force);
wenzelm@7535
    86
wenzelm@7917
    87
text {* The following lemma states every continous linearform on a 
wenzelm@7917
    88
normed space $(V, \norm{\cdot})$ has a function norm. *};
wenzelm@7917
    89
wenzelm@7566
    90
lemma ex_fnorm [intro!!]: 
wenzelm@7535
    91
  "[| is_normed_vectorspace V norm; is_continous V norm f|]
wenzelm@7535
    92
     ==> is_function_norm V norm f (function_norm V norm f)"; 
wenzelm@7917
    93
proof (unfold function_norm_def is_function_norm_def 
wenzelm@7917
    94
  is_continous_def Sup_def, elim conjE, rule selectI2EX);
wenzelm@7535
    95
  assume "is_normed_vectorspace V norm";
wenzelm@7808
    96
  assume "is_linearform V f" 
wenzelm@7808
    97
  and e: "EX c. ALL x:V. rabs (f x) <= c * norm x";
wenzelm@7917
    98
wenzelm@7917
    99
  txt {* The existence of the supremum is shown using the 
wenzelm@7917
   100
  completeness of the reals. Completeness means, that
wenzelm@7917
   101
  for every non-empty and bounded set of reals there exists a 
wenzelm@7917
   102
  supremum. *};
wenzelm@7535
   103
  show  "EX a. is_Sup UNIV (B V norm f) a"; 
wenzelm@7535
   104
  proof (unfold is_Sup_def, rule reals_complete);
wenzelm@7917
   105
wenzelm@7917
   106
    txt {* First we have to show that $B$ is non-empty. *}; 
wenzelm@7917
   107
wenzelm@7535
   108
    show "EX X. X : B V norm f"; 
wenzelm@7535
   109
    proof (intro exI);
wenzelm@7535
   110
      show "0r : (B V norm f)"; by (unfold B_def, force);
wenzelm@7535
   111
    qed;
wenzelm@7535
   112
wenzelm@7917
   113
    txt {* Then we have to show that $B$ is bounded. *};
wenzelm@7917
   114
wenzelm@7535
   115
    from e; show "EX Y. isUb UNIV (B V norm f) Y";
wenzelm@7535
   116
    proof;
wenzelm@7917
   117
wenzelm@7917
   118
      txt {* We know that $f$ is bounded by some value $c$. *};  
wenzelm@7917
   119
  
wenzelm@7535
   120
      fix c; assume a: "ALL x:V. rabs (f x) <= c * norm x";
wenzelm@7535
   121
      def b == "max c 0r";
wenzelm@7535
   122
wenzelm@7917
   123
      show "?thesis";
wenzelm@7535
   124
      proof (intro exI isUbI setleI ballI, unfold B_def, 
wenzelm@7566
   125
	elim CollectE disjE bexE conjE);
wenzelm@7917
   126
wenzelm@7917
   127
        txt{* To proof the thesis, we have to show that there is 
wenzelm@7917
   128
        some constant b, which is greater than every $y$ in $B$. 
wenzelm@7917
   129
        Due to the definition of $B$ there are two cases for
wenzelm@7917
   130
        $y\in B$. If $y = 0$ then $y$ is less than 
wenzelm@7917
   131
        $\idt{max}\ap c\ap 0$: *};
wenzelm@7917
   132
wenzelm@7917
   133
	fix y; assume "y = 0r";
wenzelm@7917
   134
        show "y <= b"; by (simp! add: le_max2);
wenzelm@7917
   135
wenzelm@7917
   136
        txt{* The second case is 
wenzelm@7917
   137
        $y = \frac{|f\ap x|}{\norm x}$ for some 
wenzelm@7917
   138
        $x\in V$ with $x \neq \zero$. *};
wenzelm@7917
   139
wenzelm@7917
   140
      next;
wenzelm@7917
   141
	fix x y;
wenzelm@7917
   142
        assume "x:V" "x ~= <0>"; (***
wenzelm@7917
   143
wenzelm@7917
   144
         have ge: "0r <= rinv (norm x)";
wenzelm@7917
   145
          by (rule real_less_imp_le, rule real_rinv_gt_zero, 
wenzelm@7917
   146
                rule normed_vs_norm_gt_zero); (***
wenzelm@7656
   147
          proof (rule real_less_imp_le);
wenzelm@7566
   148
            show "0r < rinv (norm x)";
wenzelm@7566
   149
            proof (rule real_rinv_gt_zero);
wenzelm@7566
   150
              show "0r < norm x"; ..;
wenzelm@7566
   151
            qed;
wenzelm@7917
   152
          qed; ***)
wenzelm@7917
   153
        have nz: "norm x ~= 0r"; 
wenzelm@7917
   154
          by (rule not_sym, rule lt_imp_not_eq, 
wenzelm@7917
   155
              rule normed_vs_norm_gt_zero); (***
wenzelm@7917
   156
          proof (rule not_sym);
wenzelm@7917
   157
            show "0r ~= norm x"; 
wenzelm@7917
   158
            proof (rule lt_imp_not_eq);
wenzelm@7917
   159
              show "0r < norm x"; ..;
wenzelm@7917
   160
            qed;
wenzelm@7917
   161
          qed; ***)***)
wenzelm@7917
   162
wenzelm@7917
   163
        txt {* The thesis follows by a short calculation using the 
wenzelm@7917
   164
        fact that $f$ is bounded. *};
wenzelm@7917
   165
    
wenzelm@7917
   166
        assume "y = rabs (f x) * rinv (norm x)";
wenzelm@7917
   167
        also; have "... <= c * norm x * rinv (norm x)";
wenzelm@7917
   168
        proof (rule real_mult_le_le_mono2);
wenzelm@7917
   169
          show "0r <= rinv (norm x)";
wenzelm@7917
   170
            by (rule real_less_imp_le, rule real_rinv_gt_zero, 
wenzelm@7917
   171
                rule normed_vs_norm_gt_zero);
wenzelm@7917
   172
          from a; show "rabs (f x) <= c * norm x"; ..;
wenzelm@7535
   173
        qed;
wenzelm@7808
   174
        also; have "... = c * (norm x * rinv (norm x))"; 
wenzelm@7808
   175
          by (rule real_mult_assoc);
wenzelm@7535
   176
        also; have "(norm x * rinv (norm x)) = 1r"; 
wenzelm@7535
   177
        proof (rule real_mult_inv_right);
wenzelm@7917
   178
          show nz: "norm x ~= 0r"; 
wenzelm@7917
   179
            by (rule not_sym, rule lt_imp_not_eq, 
wenzelm@7917
   180
              rule normed_vs_norm_gt_zero);
wenzelm@7535
   181
        qed;
wenzelm@7917
   182
        also; have "c * ... <= b "; by (simp! add: le_max1);
wenzelm@7535
   183
	finally; show "y <= b"; .;
wenzelm@7535
   184
      qed simp;
wenzelm@7535
   185
    qed;
wenzelm@7535
   186
  qed;
wenzelm@7535
   187
qed;
wenzelm@7535
   188
wenzelm@7917
   189
text {* The norm of a continous function is always $\geq 0$. *};
wenzelm@7917
   190
wenzelm@7808
   191
lemma fnorm_ge_zero [intro!!]: 
wenzelm@7808
   192
  "[| is_continous V norm f; is_normed_vectorspace V norm|]
wenzelm@7535
   193
   ==> 0r <= function_norm V norm f";
wenzelm@7535
   194
proof -;
wenzelm@7917
   195
  assume c: "is_continous V norm f" 
wenzelm@7917
   196
     and n: "is_normed_vectorspace V norm";
wenzelm@7917
   197
wenzelm@7917
   198
  txt {* The function norm is defined as the supremum of $B$. 
wenzelm@7917
   199
  So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided
wenzelm@7917
   200
  the supremum exists and $B$ is not empty. *};
wenzelm@7917
   201
wenzelm@7535
   202
  show ?thesis; 
wenzelm@7535
   203
  proof (unfold function_norm_def, rule sup_ub1);
wenzelm@7535
   204
    show "ALL x:(B V norm f). 0r <= x"; 
wenzelm@7917
   205
    proof (intro ballI, unfold B_def, 
wenzelm@7917
   206
           elim CollectE bexE conjE disjE);
wenzelm@7917
   207
      fix x r; 
wenzelm@7917
   208
      assume "x : V" "x ~= <0>" 
wenzelm@7917
   209
        and r: "r = rabs (f x) * rinv (norm x)";
wenzelm@7917
   210
wenzelm@7917
   211
      have ge: "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero);
wenzelm@7917
   212
      have "0r <= rinv (norm x)"; 
wenzelm@7917
   213
        by (rule real_less_imp_le, rule real_rinv_gt_zero, rule);(***
wenzelm@7656
   214
        proof (rule real_less_imp_le);
wenzelm@7535
   215
          show "0r < rinv (norm x)"; 
wenzelm@7566
   216
          proof (rule real_rinv_gt_zero);
wenzelm@7566
   217
            show "0r < norm x"; ..;
wenzelm@7566
   218
          qed;
wenzelm@7917
   219
        qed; ***)
wenzelm@7917
   220
      with ge; show "0r <= r";
wenzelm@7917
   221
       by (simp only: r,rule real_le_mult_order);
wenzelm@7566
   222
    qed (simp!);
wenzelm@7917
   223
wenzelm@7917
   224
    txt {* Since $f$ is continous the function norm exists. *};
wenzelm@7917
   225
wenzelm@7917
   226
    have "is_function_norm V norm f (function_norm V norm f)"; ..;
wenzelm@7917
   227
    thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
wenzelm@7917
   228
      by (unfold is_function_norm_def, unfold function_norm_def);
wenzelm@7917
   229
wenzelm@7917
   230
    txt {* $B$ is non-empty by construction. *};
wenzelm@7917
   231
wenzelm@7535
   232
    show "0r : B V norm f"; by (rule B_not_empty);
wenzelm@7535
   233
  qed;
wenzelm@7535
   234
qed;
wenzelm@7535
   235
  
wenzelm@7917
   236
text{* The basic property of function norms is: 
wenzelm@7917
   237
\begin{matharray}{l}
wenzelm@7917
   238
| f\ap x | \leq {\fnorm {f}} \cdot {\norm x}  
wenzelm@7917
   239
\end{matharray}
wenzelm@7917
   240
*};
wenzelm@7917
   241
wenzelm@7535
   242
lemma norm_fx_le_norm_f_norm_x: 
wenzelm@7535
   243
  "[| is_normed_vectorspace V norm; x:V; is_continous V norm f |] 
wenzelm@7535
   244
    ==> rabs (f x) <= (function_norm V norm f) * norm x"; 
wenzelm@7535
   245
proof -; 
wenzelm@7917
   246
  assume "is_normed_vectorspace V norm" "x:V" 
wenzelm@7917
   247
  and c: "is_continous V norm f";
wenzelm@7566
   248
  have v: "is_vectorspace V"; ..;
wenzelm@7535
   249
  assume "x:V";
wenzelm@7917
   250
wenzelm@7917
   251
 txt{* The proof is by case analysis on $x$. *};
wenzelm@7917
   252
 
wenzelm@7535
   253
  show "?thesis";
wenzelm@7917
   254
  proof (rule case_split);
wenzelm@7917
   255
wenzelm@7917
   256
    txt {* For the case $x = \zero$ the thesis follows
wenzelm@7917
   257
    from the linearity of $f$: for every linear function
wenzelm@7917
   258
    holds $f\ap \zero = 0$. *};
wenzelm@7917
   259
wenzelm@7917
   260
    assume "x = <0>";
wenzelm@7917
   261
    have "rabs (f x) = rabs (f <0>)"; by (simp!);
wenzelm@7917
   262
    also; from v continous_linearform; have "f <0> = 0r"; ..;
wenzelm@7917
   263
    also; note rabs_zero;
wenzelm@7917
   264
    also; have "0r <= function_norm V norm f * norm x";
wenzelm@7917
   265
    proof (rule real_le_mult_order);
wenzelm@7917
   266
      show "0r <= function_norm V norm f"; ..;
wenzelm@7917
   267
      show "0r <= norm x"; ..;
wenzelm@7917
   268
    qed;
wenzelm@7917
   269
    finally; 
wenzelm@7917
   270
    show "rabs (f x) <= function_norm V norm f * norm x"; .;
wenzelm@7917
   271
wenzelm@7917
   272
  next;
wenzelm@7535
   273
    assume "x ~= <0>";
wenzelm@7917
   274
    have n: "0r <= norm x"; ..;
wenzelm@7917
   275
    have nz: "norm x ~= 0r";
wenzelm@7917
   276
    proof (rule lt_imp_not_eq [RS not_sym]);
wenzelm@7917
   277
      show "0r < norm x"; ..;
wenzelm@7535
   278
    qed;
wenzelm@7917
   279
wenzelm@7917
   280
    txt {* For the case $x\neq \zero$ we derive the following
wenzelm@7917
   281
    fact from the definition of the function norm:*};
wenzelm@7917
   282
wenzelm@7917
   283
    have l: "rabs (f x) * rinv (norm x) <= function_norm V norm f";
wenzelm@7917
   284
    proof (unfold function_norm_def, rule sup_ub);
wenzelm@7917
   285
      from ex_fnorm [OF _ c];
wenzelm@7917
   286
      show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
wenzelm@7917
   287
         by (simp! add: is_function_norm_def function_norm_def);
wenzelm@7917
   288
      show "rabs (f x) * rinv (norm x) : B V norm f"; 
wenzelm@7917
   289
        by (unfold B_def, intro CollectI disjI2 bexI [of _ x]
wenzelm@7917
   290
            conjI, simp);
wenzelm@7535
   291
    qed;
wenzelm@7917
   292
wenzelm@7917
   293
    txt {* The thesis follows by a short calculation: *};
wenzelm@7917
   294
wenzelm@7917
   295
    have "rabs (f x) = rabs (f x) * 1r"; by (simp!);
wenzelm@7917
   296
    also; from nz; have "1r = rinv (norm x) * norm x"; 
wenzelm@7917
   297
      by (rule real_mult_inv_left [RS sym]);
wenzelm@7917
   298
    also; 
wenzelm@7917
   299
    have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x";
wenzelm@7917
   300
      by (simp! add: real_mult_assoc [of "rabs (f x)"]);
wenzelm@7917
   301
    also; have "... <= function_norm V norm f * norm x"; 
wenzelm@7917
   302
      by (rule real_mult_le_le_mono2 [OF n l]);
wenzelm@7917
   303
    finally; 
wenzelm@7917
   304
    show "rabs (f x) <= function_norm V norm f * norm x"; .;
wenzelm@7535
   305
  qed;
wenzelm@7535
   306
qed;
wenzelm@7535
   307
wenzelm@7917
   308
text{* The function norm is the least positive real number for 
wenzelm@7917
   309
which the inequation
wenzelm@7917
   310
\begin{matharray}{l}
wenzelm@7917
   311
| f\ap x | \leq c \cdot {\norm x}  
wenzelm@7917
   312
\end{matharray} 
wenzelm@7917
   313
holds.
wenzelm@7917
   314
*};
wenzelm@7917
   315
wenzelm@7535
   316
lemma fnorm_le_ub: 
wenzelm@7535
   317
  "[| is_normed_vectorspace V norm; is_continous V norm f;
wenzelm@7535
   318
     ALL x:V. rabs (f x) <= c * norm x; 0r <= c |]
wenzelm@7535
   319
  ==> function_norm V norm f <= c";
wenzelm@7535
   320
proof (unfold function_norm_def);
wenzelm@7535
   321
  assume "is_normed_vectorspace V norm"; 
wenzelm@7535
   322
  assume c: "is_continous V norm f";
wenzelm@7535
   323
  assume fb: "ALL x:V. rabs (f x) <= c * norm x"
wenzelm@7535
   324
         and "0r <= c";
wenzelm@7917
   325
wenzelm@7917
   326
  txt {* Suppose the inequation holds for some $c\geq 0$.
wenzelm@7917
   327
  If $c$ is an upper bound of $B$, then $c$ is greater 
wenzelm@7917
   328
  than the function norm since the function norm is the
wenzelm@7917
   329
  least upper bound.
wenzelm@7917
   330
  *};
wenzelm@7917
   331
wenzelm@7535
   332
  show "Sup UNIV (B V norm f) <= c"; 
wenzelm@7656
   333
  proof (rule sup_le_ub);
wenzelm@7808
   334
    from ex_fnorm [OF _ c]; 
wenzelm@7808
   335
    show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
wenzelm@7566
   336
      by (simp! add: is_function_norm_def function_norm_def); 
wenzelm@7917
   337
  
wenzelm@7917
   338
    txt {* $c$ is an upper bound of $B$, i.~e.~every
wenzelm@7917
   339
    $y\in B$ is less than $c$. *};
wenzelm@7917
   340
wenzelm@7535
   341
    show "isUb UNIV (B V norm f) c";  
wenzelm@7535
   342
    proof (intro isUbI setleI ballI);
wenzelm@7535
   343
      fix y; assume "y: B V norm f";
wenzelm@7566
   344
      thus le: "y <= c";
wenzelm@7917
   345
      proof (unfold B_def, elim CollectE disjE bexE conjE);
wenzelm@7917
   346
wenzelm@7917
   347
       txt {* The first case for $y\in B$ is $y=0$. *};
wenzelm@7917
   348
wenzelm@7917
   349
        assume "y = 0r";
wenzelm@7917
   350
        show "y <= c"; by (force!);
wenzelm@7917
   351
wenzelm@7917
   352
        txt{* The second case is 
wenzelm@7917
   353
        $y = \frac{|f\ap x|}{\norm x}$ for some 
wenzelm@7917
   354
        $x\in V$ with $x \neq \zero$. *};  
wenzelm@7917
   355
wenzelm@7917
   356
      next;
wenzelm@7917
   357
	fix x; 
wenzelm@7917
   358
        assume "x : V" "x ~= <0>"; 
wenzelm@7917
   359
wenzelm@7917
   360
        have lz: "0r < norm x"; 
wenzelm@7917
   361
          by (simp! add: normed_vs_norm_gt_zero);
wenzelm@7566
   362
          
wenzelm@7917
   363
        have nz: "norm x ~= 0r"; 
wenzelm@7566
   364
        proof (rule not_sym);
wenzelm@7917
   365
          from lz; show "0r ~= norm x";
wenzelm@7917
   366
            by (simp! add: order_less_imp_not_eq);
wenzelm@7566
   367
        qed;
wenzelm@7566
   368
            
wenzelm@7917
   369
	from lz; have "0r < rinv (norm x)";
wenzelm@7566
   370
	  by (simp! add: real_rinv_gt_zero);
wenzelm@7917
   371
	hence rinv_gez: "0r <= rinv (norm x)";
wenzelm@7808
   372
          by (rule real_less_imp_le);
wenzelm@7535
   373
wenzelm@7917
   374
	assume "y = rabs (f x) * rinv (norm x)"; 
wenzelm@7917
   375
	also; from rinv_gez; have "... <= c * norm x * rinv (norm x)";
wenzelm@7535
   376
	  proof (rule real_mult_le_le_mono2);
wenzelm@7917
   377
	    show "rabs (f x) <= c * norm x"; by (rule bspec);
wenzelm@7535
   378
	  qed;
wenzelm@7917
   379
	also; have "... <= c"; by (simp add: nz real_mult_assoc);
wenzelm@7535
   380
	finally; show ?thesis; .;
wenzelm@7535
   381
      qed;
wenzelm@7535
   382
    qed force;
wenzelm@7535
   383
  qed;
wenzelm@7535
   384
qed;
wenzelm@7535
   385
wenzelm@7808
   386
end;