src/HOL/Real/HahnBanach/FunctionNorm.thy
author wenzelm
Sun Jul 23 12:01:05 2000 +0200 (2000-07-23)
changeset 9408 d3d56e1d2ec1
parent 9394 1ff8a6234c6a
child 9503 3324cbbecef8
permissions -rw-r--r--
classical atts now intro! / intro / intro?;
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 ::
bauerg@9374
    21
  "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool" 
wenzelm@7978
    22
  "is_continuous V norm f == 
bauerg@9379
    23
    is_linearform V f \\<and> (\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x)"
wenzelm@7535
    24
wenzelm@7978
    25
lemma continuousI [intro]: 
bauerg@9379
    26
  "[| is_linearform V f; !! x. x \\<in> V ==> |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)
bauerg@9379
    29
  assume r: "!! x. x \\<in> V ==> |f x| <= c * norm x" 
bauerg@9379
    30
  fix x assume "x \\<in> V" show "|f x| <= c * norm x" by (rule r)
wenzelm@9035
    31
qed
wenzelm@7535
    32
  
wenzelm@9408
    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@9408
    37
lemma continuous_bounded [intro?]:
wenzelm@7978
    38
  "is_continuous V norm f 
bauerg@9379
    39
  ==> \\<exists>c. \\<forall>x \\<in> V. |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
\[
bauerg@9374
    62
\{ 0 \} \Union \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
bauerg@9374
    67
  B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"
wenzelm@7808
    68
  "B V norm f == 
bauerg@9379
    69
  {#0} \\<union> {|f x| * rinv (norm x) | x. x \\<noteq> 0 \\<and> x \\<in> 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 :: 
bauerg@9374
    77
  " ['a::{minus,plus,zero}  => real, 'a set, 'a => real] => real => bool"
bauerg@9374
    78
  "is_function_norm f V norm 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 
bauerg@9374
    84
  function_norm :: " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real"
bauerg@9374
    85
  "function_norm f V norm == Sup UNIV (B V norm f)"
wenzelm@7978
    86
bauerg@9374
    87
syntax   
bauerg@9379
    88
  function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\\<parallel>_\\<parallel>_,_")
bauerg@9374
    89
bauerg@9379
    90
lemma B_not_empty: "#0 \\<in> B V norm f"
wenzelm@9035
    91
  by (unfold B_def, force)
wenzelm@7535
    92
wenzelm@7978
    93
text {* The following lemma states that every continuous linear form
wenzelm@9035
    94
on a normed space $(V, \norm{\cdot})$ has a function norm. *}
wenzelm@7917
    95
wenzelm@9408
    96
lemma ex_fnorm [intro?]: 
wenzelm@7978
    97
  "[| is_normed_vectorspace V norm; is_continuous V norm f|]
bauerg@9379
    98
     ==> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" 
wenzelm@7917
    99
proof (unfold function_norm_def is_function_norm_def 
wenzelm@9035
   100
  is_continuous_def Sup_def, elim conjE, rule selectI2EX)
wenzelm@9035
   101
  assume "is_normed_vectorspace V norm"
wenzelm@7808
   102
  assume "is_linearform V f" 
bauerg@9379
   103
  and e: "\\<exists>c. \\<forall>x \\<in> V. |f x| <= c * norm x"
wenzelm@7917
   104
wenzelm@7917
   105
  txt {* The existence of the supremum is shown using the 
wenzelm@7917
   106
  completeness of the reals. Completeness means, that
wenzelm@7978
   107
  every non-empty bounded set of reals has a 
wenzelm@9035
   108
  supremum. *}
bauerg@9379
   109
  show  "\\<exists>a. is_Sup UNIV (B V norm f) a" 
wenzelm@9035
   110
  proof (unfold is_Sup_def, rule reals_complete)
wenzelm@7917
   111
wenzelm@9035
   112
    txt {* First we have to show that $B$ is non-empty: *} 
wenzelm@7917
   113
bauerg@9379
   114
    show "\\<exists>X. X \\<in> B V norm f" 
wenzelm@9035
   115
    proof (intro exI)
bauerg@9379
   116
      show "#0 \\<in> (B V norm f)" by (unfold B_def, force)
wenzelm@9035
   117
    qed
wenzelm@7535
   118
wenzelm@9035
   119
    txt {* Then we have to show that $B$ is bounded: *}
wenzelm@7917
   120
bauerg@9379
   121
    from e show "\\<exists>Y. isUb UNIV (B V norm f) Y"
wenzelm@9035
   122
    proof
wenzelm@7917
   123
wenzelm@9035
   124
      txt {* We know that $f$ is bounded by some value $c$. *}  
wenzelm@7917
   125
  
bauerg@9379
   126
      fix c assume a: "\\<forall>x \\<in> V. |f x| <= c * norm x"
wenzelm@9035
   127
      def b == "max c #0"
wenzelm@7535
   128
wenzelm@9035
   129
      show "?thesis"
wenzelm@7535
   130
      proof (intro exI isUbI setleI ballI, unfold B_def, 
wenzelm@9035
   131
	elim UnE CollectE exE conjE singletonE)
wenzelm@7917
   132
wenzelm@7917
   133
        txt{* To proof the thesis, we have to show that there is 
wenzelm@7978
   134
        some constant $b$, such that $y \leq b$ for all $y\in B$. 
wenzelm@7917
   135
        Due to the definition of $B$ there are two cases for
bauerg@9379
   136
        $y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}
wenzelm@7917
   137
wenzelm@9035
   138
	fix y assume "y = (#0::real)"
wenzelm@9394
   139
        show "y <= b" by (simp! add: le_maxI2)
wenzelm@7917
   140
wenzelm@7917
   141
        txt{* The second case is 
wenzelm@7978
   142
        $y = {|f\ap x|}/{\norm x}$ for some 
wenzelm@9035
   143
        $x\in V$ with $x \neq \zero$. *}
wenzelm@7917
   144
wenzelm@9035
   145
      next
wenzelm@9035
   146
	fix x y
bauerg@9379
   147
        assume "x \\<in> V" "x \\<noteq> 0" (***
wenzelm@7917
   148
wenzelm@9035
   149
         have ge: "#0 <= rinv (norm x)";
wenzelm@7917
   150
          by (rule real_less_imp_le, rule real_rinv_gt_zero, 
wenzelm@9035
   151
                rule normed_vs_norm_gt_zero); ( ***
wenzelm@7656
   152
          proof (rule real_less_imp_le);
wenzelm@9035
   153
            show "#0 < rinv (norm x)";
wenzelm@7566
   154
            proof (rule real_rinv_gt_zero);
wenzelm@9035
   155
              show "#0 < norm x"; ..;
wenzelm@7566
   156
            qed;
wenzelm@9035
   157
          qed; *** )
bauerg@9379
   158
        have nz: "norm x \\<noteq> #0" 
wenzelm@7917
   159
          by (rule not_sym, rule lt_imp_not_eq, 
wenzelm@9035
   160
              rule normed_vs_norm_gt_zero) (***
wenzelm@7917
   161
          proof (rule not_sym);
bauerg@9379
   162
            show "#0 \\<noteq> norm x"; 
wenzelm@7917
   163
            proof (rule lt_imp_not_eq);
wenzelm@9035
   164
              show "#0 < norm x"; ..;
wenzelm@7917
   165
            qed;
wenzelm@7917
   166
          qed; ***)***)
wenzelm@7917
   167
wenzelm@7917
   168
        txt {* The thesis follows by a short calculation using the 
wenzelm@9035
   169
        fact that $f$ is bounded. *}
wenzelm@7917
   170
    
bauerg@9374
   171
        assume "y = |f x| * rinv (norm x)"
wenzelm@9035
   172
        also have "... <= c * norm x * rinv (norm x)"
wenzelm@9035
   173
        proof (rule real_mult_le_le_mono2)
wenzelm@9035
   174
          show "#0 <= rinv (norm x)"
fleuriot@9013
   175
            by (rule real_less_imp_le, rule real_rinv_gt_zero1, 
wenzelm@9035
   176
                rule normed_vs_norm_gt_zero)
bauerg@9374
   177
          from a show "|f x| <= c * norm x" ..
wenzelm@9035
   178
        qed
wenzelm@9035
   179
        also have "... = c * (norm x * rinv (norm x))" 
wenzelm@9035
   180
          by (rule real_mult_assoc)
wenzelm@9035
   181
        also have "(norm x * rinv (norm x)) = (#1::real)" 
wenzelm@9035
   182
        proof (rule real_mult_inv_right1)
bauerg@9379
   183
          show nz: "norm x \\<noteq> #0" 
wenzelm@7917
   184
            by (rule not_sym, rule lt_imp_not_eq, 
wenzelm@9035
   185
              rule normed_vs_norm_gt_zero)
wenzelm@9035
   186
        qed
wenzelm@9394
   187
        also have "c * ... <= b " by (simp! add: le_maxI1)
wenzelm@9035
   188
	finally show "y <= b" .
wenzelm@9035
   189
      qed simp
wenzelm@9035
   190
    qed
wenzelm@9035
   191
  qed
wenzelm@9035
   192
qed
wenzelm@7535
   193
wenzelm@9035
   194
text {* The norm of a continuous function is always $\geq 0$. *}
wenzelm@7917
   195
wenzelm@9408
   196
lemma fnorm_ge_zero [intro?]: 
bauerg@9374
   197
  "[| is_continuous V norm f; is_normed_vectorspace V norm |]
bauerg@9379
   198
   ==> #0 <= \\<parallel>f\\<parallel>V,norm"
wenzelm@9035
   199
proof -
wenzelm@7978
   200
  assume c: "is_continuous V norm f" 
wenzelm@9035
   201
     and n: "is_normed_vectorspace V norm"
wenzelm@7917
   202
wenzelm@7917
   203
  txt {* The function norm is defined as the supremum of $B$. 
wenzelm@7917
   204
  So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided
wenzelm@9035
   205
  the supremum exists and $B$ is not empty. *}
wenzelm@7917
   206
wenzelm@9035
   207
  show ?thesis 
wenzelm@9035
   208
  proof (unfold function_norm_def, rule sup_ub1)
bauerg@9379
   209
    show "\\<forall>x \\<in> (B V norm f). #0 <= x" 
wenzelm@7978
   210
    proof (intro ballI, unfold B_def,
wenzelm@9035
   211
           elim UnE singletonE CollectE exE conjE) 
wenzelm@9035
   212
      fix x r
bauerg@9379
   213
      assume "x \\<in> V" "x \\<noteq> 0" 
bauerg@9374
   214
        and r: "r = |f x| * rinv (norm x)"
wenzelm@7917
   215
bauerg@9374
   216
      have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)
wenzelm@9035
   217
      have "#0 <= rinv (norm x)" 
wenzelm@9035
   218
        by (rule real_less_imp_le, rule real_rinv_gt_zero1, rule)(***
wenzelm@7656
   219
        proof (rule real_less_imp_le);
wenzelm@9035
   220
          show "#0 < rinv (norm x)"; 
wenzelm@7566
   221
          proof (rule real_rinv_gt_zero);
wenzelm@9035
   222
            show "#0 < norm x"; ..;
wenzelm@7566
   223
          qed;
wenzelm@7917
   224
        qed; ***)
wenzelm@9035
   225
      with ge show "#0 <= r"
wenzelm@9035
   226
       by (simp only: r, rule real_le_mult_order1a)
wenzelm@9035
   227
    qed (simp!)
wenzelm@7917
   228
wenzelm@9035
   229
    txt {* Since $f$ is continuous the function norm exists: *}
wenzelm@7917
   230
bauerg@9379
   231
    have "is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" ..
wenzelm@9035
   232
    thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" 
wenzelm@9035
   233
      by (unfold is_function_norm_def function_norm_def)
wenzelm@7917
   234
wenzelm@9035
   235
    txt {* $B$ is non-empty by construction: *}
wenzelm@7917
   236
bauerg@9379
   237
    show "#0 \\<in> B V norm f" by (rule B_not_empty)
wenzelm@9035
   238
  qed
wenzelm@9035
   239
qed
wenzelm@7535
   240
  
wenzelm@7978
   241
text{* \medskip The fundamental property of function norms is: 
wenzelm@7917
   242
\begin{matharray}{l}
wenzelm@7917
   243
| f\ap x | \leq {\fnorm {f}} \cdot {\norm x}  
wenzelm@7917
   244
\end{matharray}
wenzelm@9035
   245
*}
wenzelm@7917
   246
wenzelm@7535
   247
lemma norm_fx_le_norm_f_norm_x: 
bauerg@9379
   248
  "[| is_continuous V norm f; is_normed_vectorspace V norm; x \\<in> V |] 
bauerg@9379
   249
    ==> |f x| <= \\<parallel>f\\<parallel>V,norm * norm x"
wenzelm@9035
   250
proof - 
bauerg@9379
   251
  assume "is_normed_vectorspace V norm" "x \\<in> V" 
wenzelm@9035
   252
  and c: "is_continuous V norm f"
wenzelm@9035
   253
  have v: "is_vectorspace V" ..
wenzelm@7917
   254
wenzelm@9035
   255
 txt{* The proof is by case analysis on $x$. *}
wenzelm@7917
   256
 
wenzelm@9035
   257
  show ?thesis
wenzelm@9035
   258
  proof cases
wenzelm@7917
   259
wenzelm@7917
   260
    txt {* For the case $x = \zero$ the thesis follows
wenzelm@7917
   261
    from the linearity of $f$: for every linear function
wenzelm@9035
   262
    holds $f\ap \zero = 0$. *}
wenzelm@7917
   263
bauerg@9374
   264
    assume "x = 0"
bauerg@9374
   265
    have "|f x| = |f 0|" by (simp!)
bauerg@9374
   266
    also from v continuous_linearform have "f 0 = #0" ..
wenzelm@9035
   267
    also note abs_zero
bauerg@9379
   268
    also have "#0 <= \\<parallel>f\\<parallel>V,norm * norm x"
wenzelm@9035
   269
    proof (rule real_le_mult_order1a)
bauerg@9379
   270
      show "#0 <= \\<parallel>f\\<parallel>V,norm" ..
wenzelm@9035
   271
      show "#0 <= norm x" ..
wenzelm@9035
   272
    qed
wenzelm@9035
   273
    finally 
bauerg@9379
   274
    show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .
wenzelm@7917
   275
wenzelm@9035
   276
  next
bauerg@9379
   277
    assume "x \\<noteq> 0"
bauerg@9379
   278
    have n: "#0 < norm x" ..
bauerg@9379
   279
    hence nz: "norm x \\<noteq> #0" 
bauerg@9379
   280
      by (simp only: lt_imp_not_eq)
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
bauerg@9379
   285
    have l: "|f x| * rinv (norm x) <= \\<parallel>f\\<parallel>V,norm"
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)
bauerg@9379
   290
      show "|f x| * rinv (norm x) \\<in> 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
bauerg@9374
   297
    have "|f x| = |f x| * #1" by (simp!)
bauerg@9374
   298
    also from nz have "#1 = rinv (norm x) * norm x" 
bauerg@9379
   299
      by (simp add: real_mult_inv_left1)
bauerg@9379
   300
    also have "|f x| * ... = |f x| * rinv (norm x) * norm x"
bauerg@9374
   301
      by (simp! add: real_mult_assoc)
bauerg@9379
   302
    also from n l have "... <= \\<parallel>f\\<parallel>V,norm * norm x"
bauerg@9379
   303
      by (simp add: real_mult_le_le_mono2)
bauerg@9379
   304
    finally show "|f x| <= \\<parallel>f\\<parallel>V,norm * norm x" .
wenzelm@9035
   305
  qed
wenzelm@9035
   306
qed
wenzelm@7535
   307
wenzelm@7978
   308
text{* \medskip The function norm is the least positive real number for 
wenzelm@7978
   309
which the following inequation holds:
wenzelm@7917
   310
\begin{matharray}{l}
wenzelm@7917
   311
| f\ap x | \leq c \cdot {\norm x}  
wenzelm@7917
   312
\end{matharray} 
wenzelm@9035
   313
*}
wenzelm@7917
   314
wenzelm@7535
   315
lemma fnorm_le_ub: 
bauerg@9374
   316
  "[| is_continuous V norm f; is_normed_vectorspace V norm; 
bauerg@9379
   317
     \\<forall>x \\<in> V. |f x| <= c * norm x; #0 <= c |]
bauerg@9379
   318
  ==> \\<parallel>f\\<parallel>V,norm <= c"
wenzelm@9035
   319
proof (unfold function_norm_def)
wenzelm@9035
   320
  assume "is_normed_vectorspace V norm" 
wenzelm@9035
   321
  assume c: "is_continuous V norm f"
bauerg@9379
   322
  assume fb: "\\<forall>x \\<in> V. |f x| <= c * norm x"
bauerg@9379
   323
    and "#0 <= c"
wenzelm@7917
   324
wenzelm@7917
   325
  txt {* Suppose the inequation holds for some $c\geq 0$.
wenzelm@7917
   326
  If $c$ is an upper bound of $B$, then $c$ is greater 
wenzelm@7917
   327
  than the function norm since the function norm is the
wenzelm@7917
   328
  least upper bound.
wenzelm@9035
   329
  *}
wenzelm@7917
   330
wenzelm@9035
   331
  show "Sup UNIV (B V norm f) <= c" 
wenzelm@9035
   332
  proof (rule sup_le_ub)
wenzelm@9035
   333
    from ex_fnorm [OF _ c] 
wenzelm@9035
   334
    show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))" 
wenzelm@9035
   335
      by (simp! add: is_function_norm_def function_norm_def) 
wenzelm@7917
   336
  
bauerg@9374
   337
    txt {* $c$ is an upper bound of $B$, i.e. every
wenzelm@9035
   338
    $y\in B$ is less than $c$. *}
wenzelm@7917
   339
wenzelm@9035
   340
    show "isUb UNIV (B V norm f) c"  
wenzelm@9035
   341
    proof (intro isUbI setleI ballI)
bauerg@9379
   342
      fix y assume "y \\<in> B V norm f"
wenzelm@9035
   343
      thus le: "y <= c"
wenzelm@9035
   344
      proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
wenzelm@7917
   345
wenzelm@9035
   346
       txt {* The first case for $y\in B$ is $y=0$. *}
wenzelm@7917
   347
wenzelm@9035
   348
        assume "y = #0"
wenzelm@9035
   349
        show "y <= c" by (force!)
wenzelm@7917
   350
wenzelm@7917
   351
        txt{* The second case is 
wenzelm@7978
   352
        $y = {|f\ap x|}/{\norm x}$ for some 
wenzelm@9035
   353
        $x\in V$ with $x \neq \zero$. *}  
wenzelm@7917
   354
wenzelm@9035
   355
      next
wenzelm@9035
   356
	fix x 
bauerg@9379
   357
        assume "x \\<in> V" "x \\<noteq> 0" 
wenzelm@7917
   358
wenzelm@9035
   359
        have lz: "#0 < norm x" 
wenzelm@9035
   360
          by (simp! add: normed_vs_norm_gt_zero)
wenzelm@7566
   361
          
bauerg@9379
   362
        have nz: "norm x \\<noteq> #0" 
wenzelm@9035
   363
        proof (rule not_sym)
bauerg@9379
   364
          from lz show "#0 \\<noteq> norm x"
wenzelm@9035
   365
            by (simp! add: order_less_imp_not_eq)
wenzelm@9035
   366
        qed
wenzelm@7566
   367
            
wenzelm@9035
   368
	from lz have "#0 < rinv (norm x)"
wenzelm@9035
   369
	  by (simp! add: real_rinv_gt_zero1)
wenzelm@9035
   370
	hence rinv_gez: "#0 <= rinv (norm x)"
wenzelm@9035
   371
          by (rule real_less_imp_le)
wenzelm@7535
   372
bauerg@9374
   373
	assume "y = |f x| * rinv (norm x)" 
wenzelm@9035
   374
	also from rinv_gez have "... <= c * norm x * rinv (norm x)"
wenzelm@9035
   375
	  proof (rule real_mult_le_le_mono2)
bauerg@9374
   376
	    show "|f x| <= c * norm x" by (rule bspec)
wenzelm@9035
   377
	  qed
wenzelm@9035
   378
	also have "... <= c" by (simp add: nz real_mult_assoc)
wenzelm@9035
   379
	finally show ?thesis .
wenzelm@9035
   380
      qed
wenzelm@9035
   381
    qed force
wenzelm@9035
   382
  qed
wenzelm@9035
   383
qed
wenzelm@7535
   384
wenzelm@9035
   385
end