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