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