src/HOL/Real/HahnBanach/FunctionNorm.thy
author wenzelm
Thu Aug 22 20:49:43 2002 +0200 (2002-08-22)
changeset 13515 a6a7025fd7e8
parent 12018 ec054019c910
child 13524 604d0f3622d6
permissions -rw-r--r--
updated to use locales (still some rough edges);
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@13515
    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@13515
    23
locale continuous = var V + norm_syntax + linearform +
wenzelm@13515
    24
  assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
wenzelm@7535
    25
wenzelm@10687
    26
lemma continuousI [intro]:
wenzelm@13515
    27
  includes norm_syntax + linearform
wenzelm@13515
    28
  assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
wenzelm@13515
    29
  shows "continuous V norm f"
wenzelm@13515
    30
proof
wenzelm@13515
    31
  show "linearform V f" .
wenzelm@13515
    32
  from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
wenzelm@13515
    33
  then show "continuous_axioms V norm f" ..
wenzelm@13515
    34
qed
wenzelm@7535
    35
wenzelm@11472
    36
wenzelm@13515
    37
subsection {* The norm of a linear form *}
wenzelm@7917
    38
wenzelm@10687
    39
text {*
wenzelm@10687
    40
  The least real number @{text c} for which holds
wenzelm@10687
    41
  \begin{center}
wenzelm@11472
    42
  @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
wenzelm@10687
    43
  \end{center}
wenzelm@10687
    44
  is called the \emph{norm} of @{text f}.
wenzelm@7917
    45
wenzelm@11472
    46
  For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
wenzelm@10687
    47
  defined as
wenzelm@10687
    48
  \begin{center}
wenzelm@11472
    49
  @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
wenzelm@10687
    50
  \end{center}
wenzelm@7917
    51
wenzelm@10687
    52
  For the case @{text "V = {0}"} the supremum would be taken from an
wenzelm@11472
    53
  empty set. Since @{text \<real>} is unbounded, there would be no supremum.
wenzelm@10687
    54
  To avoid this situation it must be guaranteed that there is an
wenzelm@11472
    55
  element in this set. This element must be @{text "{} \<ge> 0"} so that
wenzelm@10687
    56
  @{text function_norm} has the norm properties. Furthermore
wenzelm@10687
    57
  it does not have to change the norm in all other cases, so it must
wenzelm@13515
    58
  be @{text 0}, as all other elements are @{text "{} \<ge> 0"}.
wenzelm@7917
    59
wenzelm@13515
    60
  Thus we define the set @{text B} where the supremum is taken from as
wenzelm@13515
    61
  follows:
wenzelm@10687
    62
  \begin{center}
wenzelm@11472
    63
  @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
wenzelm@10687
    64
  \end{center}
wenzelm@10687
    65
wenzelm@13515
    66
  @{text function_norm} is equal to the supremum of @{text B}, if the
wenzelm@13515
    67
  supremum exists (otherwise it is undefined).
wenzelm@9035
    68
*}
wenzelm@7917
    69
wenzelm@13515
    70
locale function_norm = norm_syntax +
wenzelm@13515
    71
  fixes B
wenzelm@13515
    72
  defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
wenzelm@13515
    73
  fixes function_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
wenzelm@13515
    74
  defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
wenzelm@7535
    75
wenzelm@13515
    76
lemma (in function_norm) B_not_empty [intro]: "0 \<in> B V f"
wenzelm@13515
    77
  by (unfold B_def) simp
wenzelm@7535
    78
wenzelm@13515
    79
locale (open) functional_vectorspace =
wenzelm@13515
    80
    normed_vectorspace + function_norm +
wenzelm@13515
    81
  fixes cont
wenzelm@13515
    82
  defines "cont f \<equiv> continuous V norm f"
wenzelm@7917
    83
wenzelm@10687
    84
text {*
wenzelm@10687
    85
  The following lemma states that every continuous linear form on a
wenzelm@11472
    86
  normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
wenzelm@10687
    87
*}
wenzelm@10687
    88
wenzelm@13515
    89
lemma (in functional_vectorspace) function_norm_works:
wenzelm@13515
    90
  includes continuous
wenzelm@13515
    91
  shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
wenzelm@13515
    92
proof -
wenzelm@10687
    93
  txt {* The existence of the supremum is shown using the
wenzelm@13515
    94
    completeness of the reals. Completeness means, that every
wenzelm@13515
    95
    non-empty bounded set of reals has a supremum. *}
wenzelm@13515
    96
  have "\<exists>a. lub (B V f) a"
wenzelm@13515
    97
  proof (rule real_complete)
wenzelm@10687
    98
    txt {* First we have to show that @{text B} is non-empty: *}
wenzelm@13515
    99
    have "0 \<in> B V f" ..
wenzelm@13515
   100
    thus "\<exists>x. x \<in> B V f" ..
wenzelm@7535
   101
wenzelm@10687
   102
    txt {* Then we have to show that @{text B} is bounded: *}
wenzelm@13515
   103
    show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
wenzelm@13515
   104
    proof -
wenzelm@10687
   105
      txt {* We know that @{text f} is bounded by some value @{text c}. *}
wenzelm@13515
   106
      from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
wenzelm@7535
   107
wenzelm@13515
   108
      txt {* To prove the thesis, we have to show that there is some
wenzelm@13515
   109
        @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
wenzelm@13515
   110
        B"}. Due to the definition of @{text B} there are two cases. *}
wenzelm@7917
   111
wenzelm@13515
   112
      def b \<equiv> "max c 0"
wenzelm@13515
   113
      have "\<forall>y \<in> B V f. y \<le> b"
wenzelm@13515
   114
      proof
wenzelm@13515
   115
        fix y assume y: "y \<in> B V f"
wenzelm@13515
   116
        show "y \<le> b"
wenzelm@13515
   117
        proof cases
wenzelm@13515
   118
          assume "y = 0"
wenzelm@13515
   119
          thus ?thesis by (unfold b_def) arith
wenzelm@13515
   120
        next
wenzelm@13515
   121
          txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
wenzelm@13515
   122
            @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
wenzelm@13515
   123
          assume "y \<noteq> 0"
wenzelm@13515
   124
          with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
wenzelm@13515
   125
              and x: "x \<in> V" and neq: "x \<noteq> 0"
wenzelm@13515
   126
            by (auto simp add: B_def real_divide_def)
wenzelm@13515
   127
          from x neq have gt: "0 < \<parallel>x\<parallel>" ..
wenzelm@7917
   128
wenzelm@13515
   129
          txt {* The thesis follows by a short calculation using the
wenzelm@13515
   130
            fact that @{text f} is bounded. *}
wenzelm@13515
   131
wenzelm@13515
   132
          note y_rep
wenzelm@13515
   133
          also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
wenzelm@13515
   134
          proof (rule real_mult_le_le_mono2)
wenzelm@13515
   135
            from c show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
wenzelm@13515
   136
            from gt have "0 < inverse \<parallel>x\<parallel>" by (rule real_inverse_gt_0)
wenzelm@13515
   137
            thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
wenzelm@13515
   138
          qed
wenzelm@13515
   139
          also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
wenzelm@13515
   140
            by (rule real_mult_assoc)
wenzelm@13515
   141
          also
wenzelm@13515
   142
          from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
wenzelm@13515
   143
          hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by (simp add: real_mult_inv_right1)
wenzelm@13515
   144
          also have "c * 1 \<le> b" by (simp add: b_def le_maxI1)
wenzelm@13515
   145
          finally show "y \<le> b" .
wenzelm@9035
   146
        qed
wenzelm@13515
   147
      qed
wenzelm@13515
   148
      thus ?thesis ..
wenzelm@9035
   149
    qed
wenzelm@9035
   150
  qed
wenzelm@13515
   151
  then show ?thesis
wenzelm@13515
   152
    by (unfold function_norm_def) (rule the_lubI_ex)
wenzelm@13515
   153
qed
wenzelm@13515
   154
wenzelm@13515
   155
lemma (in functional_vectorspace) function_norm_ub [intro?]:
wenzelm@13515
   156
  includes continuous
wenzelm@13515
   157
  assumes b: "b \<in> B V f"
wenzelm@13515
   158
  shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
wenzelm@13515
   159
proof -
wenzelm@13515
   160
  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
wenzelm@13515
   161
  from this and b show ?thesis ..
wenzelm@13515
   162
qed
wenzelm@13515
   163
wenzelm@13515
   164
lemma (in functional_vectorspace) function_norm_least [intro?]:
wenzelm@13515
   165
  includes continuous
wenzelm@13515
   166
  assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
wenzelm@13515
   167
  shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
wenzelm@13515
   168
proof -
wenzelm@13515
   169
  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
wenzelm@13515
   170
  from this and b show ?thesis ..
wenzelm@9035
   171
qed
wenzelm@7535
   172
wenzelm@11472
   173
text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
wenzelm@7917
   174
wenzelm@13515
   175
lemma (in functional_vectorspace) function_norm_ge_zero [iff]:
wenzelm@13515
   176
  includes continuous
wenzelm@13515
   177
  shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
wenzelm@9035
   178
proof -
wenzelm@10687
   179
  txt {* The function norm is defined as the supremum of @{text B}.
wenzelm@13515
   180
    So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
wenzelm@13515
   181
    0"}, provided the supremum exists and @{text B} is not empty. *}
wenzelm@13515
   182
  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
wenzelm@13515
   183
  moreover have "0 \<in> B V f" ..
wenzelm@13515
   184
  ultimately show ?thesis ..
wenzelm@9035
   185
qed
wenzelm@10687
   186
wenzelm@10687
   187
text {*
wenzelm@10687
   188
  \medskip The fundamental property of function norms is:
wenzelm@10687
   189
  \begin{center}
wenzelm@11472
   190
  @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
wenzelm@10687
   191
  \end{center}
wenzelm@9035
   192
*}
wenzelm@7917
   193
wenzelm@13515
   194
lemma (in functional_vectorspace) function_norm_le_cong:
wenzelm@13515
   195
  includes continuous + vectorspace_linearform
wenzelm@13515
   196
  assumes x: "x \<in> V"
wenzelm@13515
   197
  shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
wenzelm@13515
   198
proof cases
wenzelm@13515
   199
  assume "x = 0"
wenzelm@13515
   200
  then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
wenzelm@13515
   201
  also have "f 0 = 0" ..
wenzelm@13515
   202
  also have "\<bar>\<dots>\<bar> = 0" by simp
wenzelm@13515
   203
  also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
wenzelm@13515
   204
  proof (rule real_le_mult_order1a)
wenzelm@13515
   205
    show "0 \<le> \<parallel>f\<parallel>\<hyphen>V" ..
wenzelm@13515
   206
    show "0 \<le> norm x" ..
wenzelm@13515
   207
  qed
wenzelm@13515
   208
  finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
wenzelm@13515
   209
next
wenzelm@13515
   210
  assume "x \<noteq> 0"
wenzelm@13515
   211
  with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
wenzelm@13515
   212
  then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
wenzelm@13515
   213
  also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
wenzelm@13515
   214
  proof (rule real_mult_le_le_mono2)
wenzelm@13515
   215
    from x show "0 \<le> \<parallel>x\<parallel>" ..
wenzelm@13515
   216
    show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
wenzelm@13515
   217
    proof
wenzelm@13515
   218
      from x and neq show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
wenzelm@13515
   219
        by (auto simp add: B_def real_divide_def)
wenzelm@9035
   220
    qed
wenzelm@9035
   221
  qed
wenzelm@13515
   222
  finally show ?thesis .
wenzelm@9035
   223
qed
wenzelm@7535
   224
wenzelm@10687
   225
text {*
wenzelm@10687
   226
  \medskip The function norm is the least positive real number for
wenzelm@10687
   227
  which the following inequation holds:
wenzelm@10687
   228
  \begin{center}
wenzelm@13515
   229
    @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
wenzelm@10687
   230
  \end{center}
wenzelm@9035
   231
*}
wenzelm@7917
   232
wenzelm@13515
   233
lemma (in functional_vectorspace) function_norm_least [intro?]:
wenzelm@13515
   234
  includes continuous
wenzelm@13515
   235
  assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
wenzelm@13515
   236
  shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
wenzelm@13515
   237
proof (rule function_norm_least)
wenzelm@13515
   238
  fix b assume b: "b \<in> B V f"
wenzelm@13515
   239
  show "b \<le> c"
wenzelm@13515
   240
  proof cases
wenzelm@13515
   241
    assume "b = 0"
wenzelm@13515
   242
    with ge show ?thesis by simp
wenzelm@13515
   243
  next
wenzelm@13515
   244
    assume "b \<noteq> 0"
wenzelm@13515
   245
    with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
wenzelm@13515
   246
        and x_neq: "x \<noteq> 0" and x: "x \<in> V"
wenzelm@13515
   247
      by (auto simp add: B_def real_divide_def)
wenzelm@13515
   248
    note b_rep
wenzelm@13515
   249
    also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
wenzelm@13515
   250
    proof (rule real_mult_le_le_mono2)
wenzelm@13515
   251
      have "0 < \<parallel>x\<parallel>" ..
wenzelm@13515
   252
      then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
wenzelm@13515
   253
      from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
wenzelm@13515
   254
    qed
wenzelm@13515
   255
    also have "\<dots> = c"
wenzelm@13515
   256
    proof -
wenzelm@13515
   257
      from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
wenzelm@13515
   258
      then show ?thesis by simp
wenzelm@13515
   259
    qed
wenzelm@13515
   260
    finally show ?thesis .
wenzelm@9035
   261
  qed
wenzelm@9035
   262
qed
wenzelm@7535
   263
wenzelm@13515
   264
lemmas [iff?] =
wenzelm@13515
   265
  functional_vectorspace.function_norm_ge_zero
wenzelm@13515
   266
  functional_vectorspace.function_norm_le_cong
wenzelm@13515
   267
  functional_vectorspace.function_norm_least
wenzelm@13515
   268
wenzelm@10687
   269
end