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