src/HOL/Hahn_Banach/Function_Norm.thy
author wenzelm
Sun Mar 11 13:39:16 2012 +0100 (2012-03-11)
changeset 46867 0883804b67bb
parent 44887 7ca82df6e951
child 50918 3b6417e9f73e
permissions -rw-r--r--
modernized locale expression, with some fluctuation of arguments;
wenzelm@31795
     1
(*  Title:      HOL/Hahn_Banach/Function_Norm.thy
wenzelm@7566
     2
    Author:     Gertrud Bauer, TU Munich
wenzelm@7566
     3
*)
wenzelm@7535
     4
wenzelm@9035
     5
header {* The norm of a function *}
wenzelm@7808
     6
wenzelm@31795
     7
theory Function_Norm
wenzelm@31795
     8
imports Normed_Space Function_Order
wenzelm@27612
     9
begin
wenzelm@7535
    10
wenzelm@9035
    11
subsection {* Continuous linear forms*}
wenzelm@7917
    12
wenzelm@10687
    13
text {*
wenzelm@11472
    14
  A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
wenzelm@13515
    15
  is \emph{continuous}, iff it is bounded, i.e.
wenzelm@10687
    16
  \begin{center}
wenzelm@11472
    17
  @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
wenzelm@10687
    18
  \end{center}
wenzelm@10687
    19
  In our application no other functions than linear forms are
wenzelm@10687
    20
  considered, so we can define continuous linear forms as bounded
wenzelm@10687
    21
  linear forms:
wenzelm@9035
    22
*}
wenzelm@7535
    23
wenzelm@46867
    24
locale continuous = linearform +
wenzelm@46867
    25
  fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
wenzelm@13515
    26
  assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
wenzelm@7535
    27
ballarin@14254
    28
declare continuous.intro [intro?] continuous_axioms.intro [intro?]
ballarin@14254
    29
wenzelm@10687
    30
lemma continuousI [intro]:
ballarin@27611
    31
  fixes norm :: "_ \<Rightarrow> real"  ("\<parallel>_\<parallel>")
ballarin@27611
    32
  assumes "linearform V f"
wenzelm@13515
    33
  assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
wenzelm@46867
    34
  shows "continuous V f norm"
wenzelm@13515
    35
proof
wenzelm@23378
    36
  show "linearform V f" by fact
wenzelm@13515
    37
  from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
wenzelm@46867
    38
  then show "continuous_axioms V f norm" ..
wenzelm@13515
    39
qed
wenzelm@7535
    40
wenzelm@11472
    41
wenzelm@13515
    42
subsection {* The norm of a linear form *}
wenzelm@7917
    43
wenzelm@10687
    44
text {*
wenzelm@10687
    45
  The least real number @{text c} for which holds
wenzelm@10687
    46
  \begin{center}
wenzelm@11472
    47
  @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
wenzelm@10687
    48
  \end{center}
wenzelm@10687
    49
  is called the \emph{norm} of @{text f}.
wenzelm@7917
    50
wenzelm@11472
    51
  For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
wenzelm@10687
    52
  defined as
wenzelm@10687
    53
  \begin{center}
wenzelm@11472
    54
  @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
wenzelm@10687
    55
  \end{center}
wenzelm@7917
    56
wenzelm@10687
    57
  For the case @{text "V = {0}"} the supremum would be taken from an
wenzelm@11472
    58
  empty set. Since @{text \<real>} is unbounded, there would be no supremum.
wenzelm@10687
    59
  To avoid this situation it must be guaranteed that there is an
wenzelm@11472
    60
  element in this set. This element must be @{text "{} \<ge> 0"} so that
wenzelm@13547
    61
  @{text fn_norm} has the norm properties. Furthermore it does not
wenzelm@13547
    62
  have to change the norm in all other cases, so it must be @{text 0},
wenzelm@13547
    63
  as all other elements are @{text "{} \<ge> 0"}.
wenzelm@7917
    64
wenzelm@13515
    65
  Thus we define the set @{text B} where the supremum is taken from as
wenzelm@13515
    66
  follows:
wenzelm@10687
    67
  \begin{center}
wenzelm@11472
    68
  @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
wenzelm@10687
    69
  \end{center}
wenzelm@10687
    70
wenzelm@13547
    71
  @{text fn_norm} is equal to the supremum of @{text B}, if the
wenzelm@13515
    72
  supremum exists (otherwise it is undefined).
wenzelm@9035
    73
*}
wenzelm@7917
    74
wenzelm@46867
    75
locale fn_norm =
wenzelm@46867
    76
  fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
wenzelm@13547
    77
  fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
wenzelm@13547
    78
  fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
wenzelm@13515
    79
  defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
wenzelm@7535
    80
ballarin@27611
    81
locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm
ballarin@27611
    82
wenzelm@13547
    83
lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
wenzelm@13547
    84
  by (simp add: B_def)
wenzelm@7917
    85
wenzelm@10687
    86
text {*
wenzelm@10687
    87
  The following lemma states that every continuous linear form on a
wenzelm@11472
    88
  normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
wenzelm@10687
    89
*}
wenzelm@10687
    90
ballarin@27611
    91
lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
wenzelm@46867
    92
  assumes "continuous V f norm"
wenzelm@13515
    93
  shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
wenzelm@13515
    94
proof -
wenzelm@46867
    95
  interpret continuous V f norm by fact
wenzelm@10687
    96
  txt {* The existence of the supremum is shown using the
wenzelm@13515
    97
    completeness of the reals. Completeness means, that every
wenzelm@13515
    98
    non-empty bounded set of reals has a supremum. *}
wenzelm@13515
    99
  have "\<exists>a. lub (B V f) a"
wenzelm@13515
   100
  proof (rule real_complete)
wenzelm@10687
   101
    txt {* First we have to show that @{text B} is non-empty: *}
wenzelm@13515
   102
    have "0 \<in> B V f" ..
wenzelm@27612
   103
    then show "\<exists>x. x \<in> B V f" ..
wenzelm@7535
   104
wenzelm@10687
   105
    txt {* Then we have to show that @{text B} is bounded: *}
wenzelm@13515
   106
    show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
wenzelm@13515
   107
    proof -
wenzelm@10687
   108
      txt {* We know that @{text f} is bounded by some value @{text c}. *}
wenzelm@13515
   109
      from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
wenzelm@7535
   110
wenzelm@13515
   111
      txt {* To prove the thesis, we have to show that there is some
wenzelm@13515
   112
        @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
wenzelm@13515
   113
        B"}. Due to the definition of @{text B} there are two cases. *}
wenzelm@7917
   114
wenzelm@13515
   115
      def b \<equiv> "max c 0"
wenzelm@13515
   116
      have "\<forall>y \<in> B V f. y \<le> b"
wenzelm@13515
   117
      proof
wenzelm@13515
   118
        fix y assume y: "y \<in> B V f"
wenzelm@13515
   119
        show "y \<le> b"
wenzelm@13515
   120
        proof cases
wenzelm@13515
   121
          assume "y = 0"
wenzelm@27612
   122
          then show ?thesis unfolding b_def by arith
wenzelm@13515
   123
        next
wenzelm@13515
   124
          txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
wenzelm@13515
   125
            @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
wenzelm@13515
   126
          assume "y \<noteq> 0"
wenzelm@13515
   127
          with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
wenzelm@13515
   128
              and x: "x \<in> V" and neq: "x \<noteq> 0"
huffman@36778
   129
            by (auto simp add: B_def divide_inverse)
wenzelm@13515
   130
          from x neq have gt: "0 < \<parallel>x\<parallel>" ..
wenzelm@7917
   131
wenzelm@13515
   132
          txt {* The thesis follows by a short calculation using the
wenzelm@13515
   133
            fact that @{text f} is bounded. *}
wenzelm@13515
   134
wenzelm@13515
   135
          note y_rep
wenzelm@13515
   136
          also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
paulson@14334
   137
          proof (rule mult_right_mono)
wenzelm@23378
   138
            from c x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
paulson@14334
   139
            from gt have "0 < inverse \<parallel>x\<parallel>" 
paulson@14334
   140
              by (rule positive_imp_inverse_positive)
wenzelm@27612
   141
            then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
wenzelm@13515
   142
          qed
wenzelm@13515
   143
          also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
huffman@36778
   144
            by (rule Groups.mult_assoc)
wenzelm@13515
   145
          also
wenzelm@13515
   146
          from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
wenzelm@27612
   147
          then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 
wenzelm@44887
   148
          also have "c * 1 \<le> b" by (simp add: b_def)
wenzelm@13515
   149
          finally show "y \<le> b" .
wenzelm@9035
   150
        qed
wenzelm@13515
   151
      qed
wenzelm@27612
   152
      then show ?thesis ..
wenzelm@9035
   153
    qed
wenzelm@9035
   154
  qed
wenzelm@27612
   155
  then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
wenzelm@13515
   156
qed
wenzelm@13515
   157
ballarin@27611
   158
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
wenzelm@46867
   159
  assumes "continuous V f norm"
wenzelm@13515
   160
  assumes b: "b \<in> B V f"
wenzelm@13515
   161
  shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
wenzelm@13515
   162
proof -
wenzelm@46867
   163
  interpret continuous V f norm by fact
wenzelm@13547
   164
  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
wenzelm@46867
   165
    using `continuous V f norm` by (rule fn_norm_works)
wenzelm@13515
   166
  from this and b show ?thesis ..
wenzelm@13515
   167
qed
wenzelm@13515
   168
ballarin@27611
   169
lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
wenzelm@46867
   170
  assumes "continuous V f norm"
wenzelm@13515
   171
  assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
wenzelm@13515
   172
  shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
wenzelm@13515
   173
proof -
wenzelm@46867
   174
  interpret continuous V f norm by fact
wenzelm@13547
   175
  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
wenzelm@46867
   176
    using `continuous V f norm` by (rule fn_norm_works)
wenzelm@13515
   177
  from this and b show ?thesis ..
wenzelm@9035
   178
qed
wenzelm@7535
   179
wenzelm@11472
   180
text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
wenzelm@7917
   181
ballarin@27611
   182
lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
wenzelm@46867
   183
  assumes "continuous V f norm"
wenzelm@13515
   184
  shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
wenzelm@9035
   185
proof -
wenzelm@46867
   186
  interpret continuous V f norm by fact
wenzelm@10687
   187
  txt {* The function norm is defined as the supremum of @{text B}.
wenzelm@13515
   188
    So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
wenzelm@13515
   189
    0"}, provided the supremum exists and @{text B} is not empty. *}
wenzelm@13547
   190
  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
wenzelm@46867
   191
    using `continuous V f norm` by (rule fn_norm_works)
wenzelm@13515
   192
  moreover have "0 \<in> B V f" ..
wenzelm@13515
   193
  ultimately show ?thesis ..
wenzelm@9035
   194
qed
wenzelm@10687
   195
wenzelm@10687
   196
text {*
wenzelm@10687
   197
  \medskip The fundamental property of function norms is:
wenzelm@10687
   198
  \begin{center}
wenzelm@11472
   199
  @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
wenzelm@10687
   200
  \end{center}
wenzelm@9035
   201
*}
wenzelm@7917
   202
ballarin@27611
   203
lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
wenzelm@46867
   204
  assumes "continuous V f norm" "linearform V f"
wenzelm@13515
   205
  assumes x: "x \<in> V"
wenzelm@13515
   206
  shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
ballarin@27611
   207
proof -
wenzelm@46867
   208
  interpret continuous V f norm by fact
wenzelm@29291
   209
  interpret linearform V f by fact
wenzelm@27612
   210
  show ?thesis
wenzelm@27612
   211
  proof cases
ballarin@27611
   212
    assume "x = 0"
ballarin@27611
   213
    then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
ballarin@27611
   214
    also have "f 0 = 0" by rule unfold_locales
ballarin@27611
   215
    also have "\<bar>\<dots>\<bar> = 0" by simp
ballarin@27611
   216
    also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
wenzelm@46867
   217
      using `continuous V f norm` by (rule fn_norm_ge_zero)
ballarin@27611
   218
    from x have "0 \<le> norm x" ..
ballarin@27611
   219
    with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
ballarin@27611
   220
    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
ballarin@27611
   221
  next
ballarin@27611
   222
    assume "x \<noteq> 0"
ballarin@27611
   223
    with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
ballarin@27611
   224
    then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
ballarin@27611
   225
    also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
ballarin@27611
   226
    proof (rule mult_right_mono)
ballarin@27611
   227
      from x show "0 \<le> \<parallel>x\<parallel>" ..
ballarin@27611
   228
      from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
huffman@36778
   229
        by (auto simp add: B_def divide_inverse)
wenzelm@46867
   230
      with `continuous V f norm` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
wenzelm@32960
   231
        by (rule fn_norm_ub)
ballarin@27611
   232
    qed
ballarin@27611
   233
    finally show ?thesis .
wenzelm@9035
   234
  qed
wenzelm@9035
   235
qed
wenzelm@7535
   236
wenzelm@10687
   237
text {*
wenzelm@10687
   238
  \medskip The function norm is the least positive real number for
wenzelm@10687
   239
  which the following inequation holds:
wenzelm@10687
   240
  \begin{center}
wenzelm@13515
   241
    @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
wenzelm@10687
   242
  \end{center}
wenzelm@9035
   243
*}
wenzelm@7917
   244
ballarin@27611
   245
lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
wenzelm@46867
   246
  assumes "continuous V f norm"
wenzelm@13515
   247
  assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
wenzelm@13515
   248
  shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
ballarin@27611
   249
proof -
wenzelm@46867
   250
  interpret continuous V f norm by fact
wenzelm@27612
   251
  show ?thesis
wenzelm@27612
   252
  proof (rule fn_norm_leastB [folded B_def fn_norm_def])
ballarin@27611
   253
    fix b assume b: "b \<in> B V f"
ballarin@27611
   254
    show "b \<le> c"
ballarin@27611
   255
    proof cases
ballarin@27611
   256
      assume "b = 0"
ballarin@27611
   257
      with ge show ?thesis by simp
ballarin@27611
   258
    next
ballarin@27611
   259
      assume "b \<noteq> 0"
ballarin@27611
   260
      with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
wenzelm@13515
   261
        and x_neq: "x \<noteq> 0" and x: "x \<in> V"
huffman@36778
   262
        by (auto simp add: B_def divide_inverse)
ballarin@27611
   263
      note b_rep
ballarin@27611
   264
      also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
ballarin@27611
   265
      proof (rule mult_right_mono)
wenzelm@32960
   266
        have "0 < \<parallel>x\<parallel>" using x x_neq ..
wenzelm@32960
   267
        then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
wenzelm@32960
   268
        from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
ballarin@27611
   269
      qed
ballarin@27611
   270
      also have "\<dots> = c"
ballarin@27611
   271
      proof -
wenzelm@32960
   272
        from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
wenzelm@32960
   273
        then show ?thesis by simp
ballarin@27611
   274
      qed
ballarin@27611
   275
      finally show ?thesis .
wenzelm@13515
   276
    qed
wenzelm@46867
   277
  qed (insert `continuous V f norm`, simp_all add: continuous_def)
ballarin@27611
   278
qed
wenzelm@7535
   279
wenzelm@10687
   280
end