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