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