src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
author wenzelm
Mon Nov 02 11:10:28 2015 +0100 (2015-11-02)
changeset 61539 a29295dac1ca
parent 61486 3590367b0ce9
child 61540 f92bf6674699
permissions -rw-r--r--
isabelle update_cartouches -t;
wenzelm@31795
     1
(*  Title:      HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
wenzelm@7917
     2
    Author:     Gertrud Bauer, TU Munich
wenzelm@7917
     3
*)
wenzelm@7917
     4
wenzelm@58889
     5
section \<open>Extending non-maximal functions\<close>
wenzelm@7917
     6
wenzelm@31795
     7
theory Hahn_Banach_Ext_Lemmas
wenzelm@31795
     8
imports Function_Norm
wenzelm@27612
     9
begin
wenzelm@7917
    10
wenzelm@58744
    11
text \<open>
wenzelm@61539
    12
  In this section the following context is presumed.  Let \<open>E\<close> be
wenzelm@61539
    13
  a real vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> a linear function on
wenzelm@61539
    14
  \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a
wenzelm@61539
    15
  superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> and \<open>x\<^sub>0\<close> is
wenzelm@61539
    16
  an element in \<open>E - H\<close>.  \<open>H\<close> is extended to the direct
wenzelm@61539
    17
  sum \<open>H' = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close>
wenzelm@61539
    18
  the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is
wenzelm@61539
    19
  unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y +
wenzelm@61539
    20
  a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>.
wenzelm@7917
    21
wenzelm@61539
    22
  Subsequently we show some properties of this extension \<open>h'\<close> of
wenzelm@61539
    23
  \<open>h\<close>.
wenzelm@7917
    24
wenzelm@61486
    25
  \<^medskip>
wenzelm@61486
    26
  This lemma will be used to show the existence of a linear
wenzelm@61539
    27
  extension of \<open>f\<close> (see page \pageref{ex-xi-use}). It is a
wenzelm@61539
    28
  consequence of the completeness of \<open>\<real>\<close>. To show
wenzelm@10687
    29
  \begin{center}
wenzelm@10687
    30
  \begin{tabular}{l}
wenzelm@61539
    31
  \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close>
wenzelm@10687
    32
  \end{tabular}
wenzelm@10687
    33
  \end{center}
wenzelm@10687
    34
  \noindent it suffices to show that
wenzelm@10687
    35
  \begin{center}
wenzelm@10687
    36
  \begin{tabular}{l}
wenzelm@61539
    37
  \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close>
wenzelm@10687
    38
  \end{tabular}
wenzelm@10687
    39
  \end{center}
wenzelm@58744
    40
\<close>
wenzelm@7917
    41
wenzelm@10687
    42
lemma ex_xi:
ballarin@27611
    43
  assumes "vectorspace F"
wenzelm@13515
    44
  assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
wenzelm@13515
    45
  shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
wenzelm@10007
    46
proof -
ballarin@29234
    47
  interpret vectorspace F by fact
wenzelm@58744
    48
  txt \<open>From the completeness of the reals follows:
wenzelm@61539
    49
    The set \<open>S = {a u. u \<in> F}\<close> has a supremum, if it is
wenzelm@58744
    50
    non-empty and has an upper bound.\<close>
wenzelm@7917
    51
wenzelm@13515
    52
  let ?S = "{a u | u. u \<in> F}"
wenzelm@13515
    53
  have "\<exists>xi. lub ?S xi"
wenzelm@13515
    54
  proof (rule real_complete)
wenzelm@13515
    55
    have "a 0 \<in> ?S" by blast
wenzelm@13515
    56
    then show "\<exists>X. X \<in> ?S" ..
wenzelm@13515
    57
    have "\<forall>y \<in> ?S. y \<le> b 0"
wenzelm@13515
    58
    proof
wenzelm@13515
    59
      fix y assume y: "y \<in> ?S"
wenzelm@13515
    60
      then obtain u where u: "u \<in> F" and y: "y = a u" by blast
wenzelm@13515
    61
      from u and zero have "a u \<le> b 0" by (rule r)
wenzelm@13515
    62
      with y show "y \<le> b 0" by (simp only:)
wenzelm@10007
    63
    qed
wenzelm@13515
    64
    then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..
wenzelm@10007
    65
  qed
wenzelm@13515
    66
  then obtain xi where xi: "lub ?S xi" ..
wenzelm@13515
    67
  {
wenzelm@13515
    68
    fix y assume "y \<in> F"
wenzelm@13515
    69
    then have "a y \<in> ?S" by blast
wenzelm@13515
    70
    with xi have "a y \<le> xi" by (rule lub.upper)
wenzelm@60458
    71
  }
wenzelm@60458
    72
  moreover {
wenzelm@13515
    73
    fix y assume y: "y \<in> F"
wenzelm@13515
    74
    from xi have "xi \<le> b y"
wenzelm@13515
    75
    proof (rule lub.least)
wenzelm@13515
    76
      fix au assume "au \<in> ?S"
wenzelm@13515
    77
      then obtain u where u: "u \<in> F" and au: "au = a u" by blast
wenzelm@13515
    78
      from u y have "a u \<le> b y" by (rule r)
wenzelm@13515
    79
      with au show "au \<le> b y" by (simp only:)
wenzelm@10007
    80
    qed
wenzelm@60458
    81
  }
wenzelm@60458
    82
  ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
wenzelm@10007
    83
qed
wenzelm@7917
    84
wenzelm@58744
    85
text \<open>
wenzelm@61486
    86
  \<^medskip>
wenzelm@61539
    87
  The function \<open>h'\<close> is defined as a \<open>h' x = h y
wenzelm@61539
    88
  + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of
wenzelm@61539
    89
  \<open>h\<close> to \<open>H'\<close>.
wenzelm@58744
    90
\<close>
wenzelm@7917
    91
wenzelm@10687
    92
lemma h'_lf:
wenzelm@13515
    93
  assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
wenzelm@13515
    94
      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
krauss@47445
    95
    and H'_def: "H' \<equiv> H + lin x0"
wenzelm@13515
    96
    and HE: "H \<unlhd> E"
ballarin@27611
    97
  assumes "linearform H h"
wenzelm@13515
    98
  assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
ballarin@27611
    99
  assumes E: "vectorspace E"
wenzelm@13515
   100
  shows "linearform H' h'"
ballarin@27611
   101
proof -
ballarin@29234
   102
  interpret linearform H h by fact
ballarin@29234
   103
  interpret vectorspace E by fact
wenzelm@27612
   104
  show ?thesis
wenzelm@27612
   105
  proof
wenzelm@58744
   106
    note E = \<open>vectorspace E\<close>
ballarin@27611
   107
    have H': "vectorspace H'"
ballarin@27611
   108
    proof (unfold H'_def)
wenzelm@58744
   109
      from \<open>x0 \<in> E\<close>
ballarin@27611
   110
      have "lin x0 \<unlhd> E" ..
krauss@47445
   111
      with HE show "vectorspace (H + lin x0)" using E ..
ballarin@27611
   112
    qed
ballarin@27611
   113
    {
ballarin@27611
   114
      fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
ballarin@27611
   115
      show "h' (x1 + x2) = h' x1 + h' x2"
ballarin@27611
   116
      proof -
wenzelm@32960
   117
        from H' x1 x2 have "x1 + x2 \<in> H'"
ballarin@27611
   118
          by (rule vectorspace.add_closed)
wenzelm@32960
   119
        with x1 x2 obtain y y1 y2 a a1 a2 where
ballarin@27611
   120
          x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
wenzelm@13515
   121
          and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
wenzelm@13515
   122
          and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
wenzelm@27612
   123
          unfolding H'_def sum_def lin_def by blast
wenzelm@32960
   124
        
wenzelm@32960
   125
        have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
wenzelm@58999
   126
        proof (rule decomp_H') text_raw \<open>\label{decomp-H-use}\<close>
ballarin@27611
   127
          from HE y1 y2 show "y1 + y2 \<in> H"
ballarin@27611
   128
            by (rule subspace.add_closed)
ballarin@27611
   129
          from x0 and HE y y1 y2
ballarin@27611
   130
          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
ballarin@27611
   131
          with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
ballarin@27611
   132
            by (simp add: add_ac add_mult_distrib2)
ballarin@27611
   133
          also note x1x2
ballarin@27611
   134
          finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
wenzelm@32960
   135
        qed
wenzelm@32960
   136
        
wenzelm@32960
   137
        from h'_def x1x2 E HE y x0
wenzelm@32960
   138
        have "h' (x1 + x2) = h y + a * xi"
ballarin@27611
   139
          by (rule h'_definite)
wenzelm@32960
   140
        also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
ballarin@27611
   141
          by (simp only: ya)
wenzelm@32960
   142
        also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
ballarin@27611
   143
          by simp
wenzelm@32960
   144
        also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
webertj@49962
   145
          by (simp add: distrib_right)
wenzelm@32960
   146
        also from h'_def x1_rep E HE y1 x0
wenzelm@32960
   147
        have "h y1 + a1 * xi = h' x1"
ballarin@27611
   148
          by (rule h'_definite [symmetric])
wenzelm@32960
   149
        also from h'_def x2_rep E HE y2 x0
wenzelm@32960
   150
        have "h y2 + a2 * xi = h' x2"
ballarin@27611
   151
          by (rule h'_definite [symmetric])
wenzelm@32960
   152
        finally show ?thesis .
wenzelm@10007
   153
      qed
ballarin@27611
   154
    next
ballarin@27611
   155
      fix x1 c assume x1: "x1 \<in> H'"
ballarin@27611
   156
      show "h' (c \<cdot> x1) = c * (h' x1)"
ballarin@27611
   157
      proof -
wenzelm@32960
   158
        from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
ballarin@27611
   159
          by (rule vectorspace.mult_closed)
wenzelm@32960
   160
        with x1 obtain y a y1 a1 where
wenzelm@27612
   161
            cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
wenzelm@13515
   162
          and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
wenzelm@27612
   163
          unfolding H'_def sum_def lin_def by blast
wenzelm@32960
   164
        
wenzelm@32960
   165
        have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
wenzelm@32960
   166
        proof (rule decomp_H')
ballarin@27611
   167
          from HE y1 show "c \<cdot> y1 \<in> H"
ballarin@27611
   168
            by (rule subspace.mult_closed)
ballarin@27611
   169
          from x0 and HE y y1
ballarin@27611
   170
          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
ballarin@27611
   171
          with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
ballarin@27611
   172
            by (simp add: mult_assoc add_mult_distrib1)
ballarin@27611
   173
          also note cx1_rep
ballarin@27611
   174
          finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
wenzelm@32960
   175
        qed
wenzelm@32960
   176
        
wenzelm@32960
   177
        from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
ballarin@27611
   178
          by (rule h'_definite)
wenzelm@32960
   179
        also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
ballarin@27611
   180
          by (simp only: ya)
wenzelm@32960
   181
        also from y1 have "h (c \<cdot> y1) = c * h y1"
ballarin@27611
   182
          by simp
wenzelm@32960
   183
        also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
webertj@49962
   184
          by (simp only: distrib_left)
wenzelm@32960
   185
        also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
ballarin@27611
   186
          by (rule h'_definite [symmetric])
wenzelm@32960
   187
        finally show ?thesis .
wenzelm@10007
   188
      qed
ballarin@27611
   189
    }
ballarin@27611
   190
  qed
wenzelm@10007
   191
qed
wenzelm@7917
   192
wenzelm@61486
   193
text \<open>
wenzelm@61486
   194
  \<^medskip>
wenzelm@61539
   195
  The linear extension \<open>h'\<close> of \<open>h\<close>
wenzelm@61539
   196
  is bounded by the seminorm \<open>p\<close>.\<close>
wenzelm@7917
   197
bauerg@9374
   198
lemma h'_norm_pres:
wenzelm@13515
   199
  assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
wenzelm@13515
   200
      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
krauss@47445
   201
    and H'_def: "H' \<equiv> H + lin x0"
wenzelm@13515
   202
    and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
ballarin@27611
   203
  assumes E: "vectorspace E" and HE: "subspace H E"
ballarin@27611
   204
    and "seminorm E p" and "linearform H h"
wenzelm@13515
   205
  assumes a: "\<forall>y \<in> H. h y \<le> p y"
wenzelm@13515
   206
    and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
wenzelm@13515
   207
  shows "\<forall>x \<in> H'. h' x \<le> p x"
ballarin@27611
   208
proof -
ballarin@29234
   209
  interpret vectorspace E by fact
ballarin@29234
   210
  interpret subspace H E by fact
ballarin@29234
   211
  interpret seminorm E p by fact
ballarin@29234
   212
  interpret linearform H h by fact
wenzelm@27612
   213
  show ?thesis
wenzelm@27612
   214
  proof
ballarin@27611
   215
    fix x assume x': "x \<in> H'"
ballarin@27611
   216
    show "h' x \<le> p x"
ballarin@27611
   217
    proof -
ballarin@27611
   218
      from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
wenzelm@32960
   219
        and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
ballarin@27611
   220
      from x' obtain y a where
wenzelm@27612
   221
          x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
wenzelm@32960
   222
        unfolding H'_def sum_def lin_def by blast
ballarin@27611
   223
      from y have y': "y \<in> E" ..
ballarin@27611
   224
      from y have ay: "inverse a \<cdot> y \<in> H" by simp
ballarin@27611
   225
      
ballarin@27611
   226
      from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
wenzelm@32960
   227
        by (rule h'_definite)
ballarin@27611
   228
      also have "\<dots> \<le> p (y + a \<cdot> x0)"
ballarin@27611
   229
      proof (rule linorder_cases)
wenzelm@32960
   230
        assume z: "a = 0"
wenzelm@32960
   231
        then have "h y + a * xi = h y" by simp
wenzelm@32960
   232
        also from a y have "\<dots> \<le> p y" ..
wenzelm@32960
   233
        also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
wenzelm@32960
   234
        finally show ?thesis .
ballarin@27611
   235
      next
wenzelm@61539
   236
        txt \<open>In the case \<open>a < 0\<close>, we use \<open>a\<^sub>1\<close>
wenzelm@61539
   237
          with \<open>ya\<close> taken as \<open>y / a\<close>:\<close>
wenzelm@32960
   238
        assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp
wenzelm@32960
   239
        from a1 ay
wenzelm@32960
   240
        have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
wenzelm@32960
   241
        with lz have "a * xi \<le>
wenzelm@13515
   242
          a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
ballarin@27611
   243
          by (simp add: mult_left_mono_neg order_less_imp_le)
wenzelm@32960
   244
        
wenzelm@32960
   245
        also have "\<dots> =
wenzelm@13515
   246
          - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
wenzelm@32960
   247
          by (simp add: right_diff_distrib)
wenzelm@32960
   248
        also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
wenzelm@13515
   249
          p (a \<cdot> (inverse a \<cdot> y + x0))"
ballarin@27611
   250
          by (simp add: abs_homogenous)
wenzelm@32960
   251
        also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
ballarin@27611
   252
          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
wenzelm@32960
   253
        also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
ballarin@27611
   254
          by simp
wenzelm@32960
   255
        finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
wenzelm@32960
   256
        then show ?thesis by simp
ballarin@27611
   257
      next
wenzelm@61539
   258
        txt \<open>In the case \<open>a > 0\<close>, we use \<open>a\<^sub>2\<close>
wenzelm@61539
   259
          with \<open>ya\<close> taken as \<open>y / a\<close>:\<close>
wenzelm@32960
   260
        assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
wenzelm@32960
   261
        from a2 ay
wenzelm@32960
   262
        have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
wenzelm@32960
   263
        with gz have "a * xi \<le>
wenzelm@13515
   264
          a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
ballarin@27611
   265
          by simp
wenzelm@32960
   266
        also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
wenzelm@32960
   267
          by (simp add: right_diff_distrib)
wenzelm@32960
   268
        also from gz x0 y'
wenzelm@32960
   269
        have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
ballarin@27611
   270
          by (simp add: abs_homogenous)
wenzelm@32960
   271
        also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
ballarin@27611
   272
          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
wenzelm@32960
   273
        also from nz y have "a * h (inverse a \<cdot> y) = h y"
ballarin@27611
   274
          by simp
wenzelm@32960
   275
        finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
wenzelm@32960
   276
        then show ?thesis by simp
ballarin@27611
   277
      qed
ballarin@27611
   278
      also from x_rep have "\<dots> = p x" by (simp only:)
ballarin@27611
   279
      finally show ?thesis .
wenzelm@10007
   280
    qed
wenzelm@10007
   281
  qed
wenzelm@13515
   282
qed
wenzelm@7917
   283
wenzelm@10007
   284
end