src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 63040 eb4ddd18d635
permissions -rw-r--r--
Lots of new material for multivariate analysis
wenzelm@31795
     1
(*  Title:      HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
wenzelm@7917
     2
    Author:     Gertrud Bauer, TU Munich
wenzelm@7917
     3
*)
wenzelm@7917
     4
wenzelm@61540
     5
section \<open>The supremum wrt.\ the function order\<close>
wenzelm@7917
     6
wenzelm@31795
     7
theory Hahn_Banach_Sup_Lemmas
wenzelm@31795
     8
imports Function_Norm Zorn_Lemma
wenzelm@27612
     9
begin
bauerg@9256
    10
wenzelm@58744
    11
text \<open>
wenzelm@61540
    12
  This section contains some lemmas that will be used in the proof of the
wenzelm@61879
    13
  Hahn-Banach Theorem. In this section the following context is presumed. Let
wenzelm@61879
    14
  \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of
wenzelm@61879
    15
  \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of norm-preserving
wenzelm@61879
    16
  extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will show some properties
wenzelm@61879
    17
  about the limit function \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>.
wenzelm@7917
    18
wenzelm@61486
    19
  \<^medskip>
wenzelm@61879
    20
  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let
wenzelm@61879
    21
  \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of one of
wenzelm@61879
    22
  the elements of the chain.
wenzelm@58744
    23
\<close>
wenzelm@61486
    24
popescua@52183
    25
lemmas [dest?] = chainsD
popescua@52183
    26
lemmas chainsE2 [elim?] = chainsD2 [elim_format]
wenzelm@7917
    27
wenzelm@7917
    28
lemma some_H'h't:
wenzelm@13515
    29
  assumes M: "M = norm_pres_extensions E p F f"
popescua@52183
    30
    and cM: "c \<in> chains M"
wenzelm@13515
    31
    and u: "graph H h = \<Union>c"
wenzelm@13515
    32
    and x: "x \<in> H"
wenzelm@13515
    33
  shows "\<exists>H' h'. graph H' h' \<in> c
wenzelm@13515
    34
    \<and> (x, h x) \<in> graph H' h'
wenzelm@13515
    35
    \<and> linearform H' h' \<and> H' \<unlhd> E
wenzelm@13515
    36
    \<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h'
wenzelm@13515
    37
    \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
bauerg@9261
    38
proof -
wenzelm@13515
    39
  from x have "(x, h x) \<in> graph H h" ..
wenzelm@13515
    40
  also from u have "\<dots> = \<Union>c" .
wenzelm@13515
    41
  finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast
wenzelm@7917
    42
wenzelm@13515
    43
  from cM have "c \<subseteq> M" ..
wenzelm@13515
    44
  with gc have "g \<in> M" ..
wenzelm@13515
    45
  also from M have "\<dots> = norm_pres_extensions E p F f" .
wenzelm@13515
    46
  finally obtain H' and h' where g: "g = graph H' h'"
wenzelm@13515
    47
    and * : "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
wenzelm@13515
    48
      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x" ..
wenzelm@13515
    49
wenzelm@13515
    50
  from gc and g have "graph H' h' \<in> c" by (simp only:)
wenzelm@13515
    51
  moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:)
wenzelm@13515
    52
  ultimately show ?thesis using * by blast
bauerg@9261
    53
qed
wenzelm@7917
    54
wenzelm@58744
    55
text \<open>
wenzelm@61486
    56
  \<^medskip>
wenzelm@61879
    57
  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let
wenzelm@61879
    58
  \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of the
wenzelm@61879
    59
  supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such
wenzelm@61879
    60
  that \<open>h\<close> extends \<open>h'\<close>.
wenzelm@58744
    61
\<close>
wenzelm@7917
    62
wenzelm@10687
    63
lemma some_H'h':
wenzelm@13515
    64
  assumes M: "M = norm_pres_extensions E p F f"
popescua@52183
    65
    and cM: "c \<in> chains M"
wenzelm@13515
    66
    and u: "graph H h = \<Union>c"
wenzelm@13515
    67
    and x: "x \<in> H"
wenzelm@13515
    68
  shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
wenzelm@13515
    69
    \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
wenzelm@13515
    70
    \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
bauerg@9261
    71
proof -
wenzelm@13515
    72
  from M cM u x obtain H' h' where
wenzelm@13515
    73
      x_hx: "(x, h x) \<in> graph H' h'"
wenzelm@13515
    74
    and c: "graph H' h' \<in> c"
wenzelm@13515
    75
    and * : "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
wenzelm@10687
    76
      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
wenzelm@13515
    77
    by (rule some_H'h't [elim_format]) blast
wenzelm@13515
    78
  from x_hx have "x \<in> H'" ..
popescua@52183
    79
  moreover from cM u c have "graph H' h' \<subseteq> graph H h" by blast
wenzelm@13515
    80
  ultimately show ?thesis using * by blast
bauerg@9261
    81
qed
wenzelm@7917
    82
wenzelm@58744
    83
text \<open>
wenzelm@61486
    84
  \<^medskip>
wenzelm@61879
    85
  Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function \<open>h\<close>
wenzelm@61879
    86
  are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends
wenzelm@61879
    87
  \<open>h'\<close>.
wenzelm@58744
    88
\<close>
wenzelm@7917
    89
wenzelm@10687
    90
lemma some_H'h'2:
wenzelm@13515
    91
  assumes M: "M = norm_pres_extensions E p F f"
popescua@52183
    92
    and cM: "c \<in> chains M"
wenzelm@13515
    93
    and u: "graph H h = \<Union>c"
wenzelm@13515
    94
    and x: "x \<in> H"
wenzelm@13515
    95
    and y: "y \<in> H"
wenzelm@13515
    96
  shows "\<exists>H' h'. x \<in> H' \<and> y \<in> H'
wenzelm@13515
    97
    \<and> graph H' h' \<subseteq> graph H h
wenzelm@13515
    98
    \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
wenzelm@13515
    99
    \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
bauerg@9261
   100
proof -
wenzelm@61879
   101
  txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, such that \<open>h\<close>
wenzelm@61879
   102
    extends \<open>h''\<close>.\<close>
wenzelm@7917
   103
wenzelm@13515
   104
  from M cM u and y obtain H' h' where
wenzelm@13515
   105
      y_hy: "(y, h y) \<in> graph H' h'"
wenzelm@13515
   106
    and c': "graph H' h' \<in> c"
wenzelm@13515
   107
    and * :
wenzelm@13515
   108
      "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
wenzelm@13515
   109
      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
wenzelm@13515
   110
    by (rule some_H'h't [elim_format]) blast
wenzelm@13515
   111
wenzelm@61539
   112
  txt \<open>\<open>x\<close> is in the domain \<open>H'\<close> of some function \<open>h'\<close>,
wenzelm@61539
   113
    such that \<open>h\<close> extends \<open>h'\<close>.\<close>
wenzelm@7917
   114
wenzelm@13515
   115
  from M cM u and x obtain H'' h'' where
wenzelm@13515
   116
      x_hx: "(x, h x) \<in> graph H'' h''"
wenzelm@13515
   117
    and c'': "graph H'' h'' \<in> c"
wenzelm@13515
   118
    and ** :
wenzelm@13515
   119
      "linearform H'' h''"  "H'' \<unlhd> E"  "F \<unlhd> H''"
wenzelm@13515
   120
      "graph F f \<subseteq> graph H'' h''"  "\<forall>x \<in> H''. h'' x \<le> p x"
wenzelm@13515
   121
    by (rule some_H'h't [elim_format]) blast
wenzelm@7917
   122
wenzelm@61879
   123
  txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, \<open>h''\<close> is an
wenzelm@61879
   124
    extension of \<open>h'\<close> or vice versa. Thus both \<open>x\<close> and \<open>y\<close> are contained in
wenzelm@61879
   125
    the greater one. \label{cases1}\<close>
wenzelm@7917
   126
wenzelm@60458
   127
  from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"
wenzelm@60458
   128
    by (blast dest: chainsD)
wenzelm@13515
   129
  then show ?thesis
wenzelm@60458
   130
  proof cases
wenzelm@60458
   131
    case 1
wenzelm@23378
   132
    have "(x, h x) \<in> graph H'' h''" by fact
wenzelm@27612
   133
    also have "\<dots> \<subseteq> graph H' h'" by fact
wenzelm@13515
   134
    finally have xh:"(x, h x) \<in> graph H' h'" .
wenzelm@13515
   135
    then have "x \<in> H'" ..
wenzelm@13515
   136
    moreover from y_hy have "y \<in> H'" ..
popescua@52183
   137
    moreover from cM u and c' have "graph H' h' \<subseteq> graph H h" by blast
wenzelm@13515
   138
    ultimately show ?thesis using * by blast
wenzelm@13515
   139
  next
wenzelm@60458
   140
    case 2
wenzelm@13515
   141
    from x_hx have "x \<in> H''" ..
wenzelm@60458
   142
    moreover have "y \<in> H''"
wenzelm@60458
   143
    proof -
wenzelm@23378
   144
      have "(y, h y) \<in> graph H' h'" by (rule y_hy)
wenzelm@23378
   145
      also have "\<dots> \<subseteq> graph H'' h''" by fact
wenzelm@13515
   146
      finally have "(y, h y) \<in> graph H'' h''" .
wenzelm@60458
   147
      then show ?thesis ..
wenzelm@60458
   148
    qed
wenzelm@60458
   149
    moreover from u c'' have "graph H'' h'' \<subseteq> graph H h" by blast
wenzelm@13515
   150
    ultimately show ?thesis using ** by blast
bauerg@9261
   151
  qed
bauerg@9261
   152
qed
wenzelm@7917
   153
wenzelm@58744
   154
text \<open>
wenzelm@61486
   155
  \<^medskip>
wenzelm@61540
   156
  The relation induced by the graph of the supremum of a chain \<open>c\<close> is
wenzelm@61540
   157
  definite, i.e.\ it is the graph of a function.
wenzelm@58744
   158
\<close>
wenzelm@7917
   159
wenzelm@10687
   160
lemma sup_definite:
wenzelm@63040
   161
  assumes M_def: "M = norm_pres_extensions E p F f"
popescua@52183
   162
    and cM: "c \<in> chains M"
wenzelm@13515
   163
    and xy: "(x, y) \<in> \<Union>c"
wenzelm@13515
   164
    and xz: "(x, z) \<in> \<Union>c"
wenzelm@13515
   165
  shows "z = y"
wenzelm@10687
   166
proof -
wenzelm@13515
   167
  from cM have c: "c \<subseteq> M" ..
wenzelm@13515
   168
  from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" ..
wenzelm@13515
   169
  from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" ..
wenzelm@7917
   170
wenzelm@13515
   171
  from G1 c have "G1 \<in> M" ..
wenzelm@13515
   172
  then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
wenzelm@27612
   173
    unfolding M_def by blast
wenzelm@7917
   174
wenzelm@13515
   175
  from G2 c have "G2 \<in> M" ..
wenzelm@13515
   176
  then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
wenzelm@27612
   177
    unfolding M_def by blast
wenzelm@7917
   178
wenzelm@61540
   179
  txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close> or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close>
wenzelm@61540
   180
    are members of \<open>c\<close>. \label{cases2}\<close>
wenzelm@7917
   181
wenzelm@60458
   182
  from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"
wenzelm@60458
   183
    by (blast dest: chainsD)
wenzelm@13515
   184
  then show ?thesis
wenzelm@60458
   185
  proof cases
wenzelm@60458
   186
    case 1
wenzelm@13515
   187
    with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
wenzelm@27612
   188
    then have "y = h2 x" ..
wenzelm@13515
   189
    also
wenzelm@13515
   190
    from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)
wenzelm@27612
   191
    then have "z = h2 x" ..
wenzelm@13515
   192
    finally show ?thesis .
wenzelm@13515
   193
  next
wenzelm@60458
   194
    case 2
wenzelm@13515
   195
    with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
wenzelm@27612
   196
    then have "z = h1 x" ..
wenzelm@13515
   197
    also
wenzelm@13515
   198
    from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)
wenzelm@27612
   199
    then have "y = h1 x" ..
wenzelm@13515
   200
    finally show ?thesis ..
bauerg@9261
   201
  qed
bauerg@9261
   202
qed
wenzelm@7917
   203
wenzelm@58744
   204
text \<open>
wenzelm@61486
   205
  \<^medskip>
wenzelm@61879
   206
  The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> is
wenzelm@61879
   207
  in the domain of a function \<open>h'\<close> in the chain of norm preserving extensions.
wenzelm@61879
   208
  Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function values of \<open>x\<close> are
wenzelm@61879
   209
  identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> is linear by
wenzelm@61879
   210
  construction of \<open>M\<close>.
wenzelm@58744
   211
\<close>
wenzelm@7917
   212
wenzelm@10687
   213
lemma sup_lf:
wenzelm@13515
   214
  assumes M: "M = norm_pres_extensions E p F f"
popescua@52183
   215
    and cM: "c \<in> chains M"
wenzelm@13515
   216
    and u: "graph H h = \<Union>c"
wenzelm@13515
   217
  shows "linearform H h"
wenzelm@13515
   218
proof
wenzelm@13515
   219
  fix x y assume x: "x \<in> H" and y: "y \<in> H"
wenzelm@13515
   220
  with M cM u obtain H' h' where
wenzelm@13515
   221
        x': "x \<in> H'" and y': "y \<in> H'"
wenzelm@13515
   222
      and b: "graph H' h' \<subseteq> graph H h"
wenzelm@13515
   223
      and linearform: "linearform H' h'"
wenzelm@13515
   224
      and subspace: "H' \<unlhd> E"
wenzelm@13515
   225
    by (rule some_H'h'2 [elim_format]) blast
wenzelm@7917
   226
wenzelm@13515
   227
  show "h (x + y) = h x + h y"
wenzelm@13515
   228
  proof -
wenzelm@13515
   229
    from linearform x' y' have "h' (x + y) = h' x + h' y"
wenzelm@13515
   230
      by (rule linearform.add)
wenzelm@13515
   231
    also from b x' have "h' x = h x" ..
wenzelm@13515
   232
    also from b y' have "h' y = h y" ..
wenzelm@13515
   233
    also from subspace x' y' have "x + y \<in> H'"
wenzelm@13515
   234
      by (rule subspace.add_closed)
wenzelm@13515
   235
    with b have "h' (x + y) = h (x + y)" ..
wenzelm@13515
   236
    finally show ?thesis .
wenzelm@13515
   237
  qed
wenzelm@13515
   238
next
wenzelm@13515
   239
  fix x a assume x: "x \<in> H"
wenzelm@13515
   240
  with M cM u obtain H' h' where
wenzelm@13515
   241
        x': "x \<in> H'"
wenzelm@13515
   242
      and b: "graph H' h' \<subseteq> graph H h"
wenzelm@13515
   243
      and linearform: "linearform H' h'"
wenzelm@13515
   244
      and subspace: "H' \<unlhd> E"
wenzelm@13515
   245
    by (rule some_H'h' [elim_format]) blast
wenzelm@7917
   246
wenzelm@13515
   247
  show "h (a \<cdot> x) = a * h x"
wenzelm@13515
   248
  proof -
wenzelm@13515
   249
    from linearform x' have "h' (a \<cdot> x) = a * h' x"
wenzelm@13515
   250
      by (rule linearform.mult)
wenzelm@13515
   251
    also from b x' have "h' x = h x" ..
wenzelm@13515
   252
    also from subspace x' have "a \<cdot> x \<in> H'"
wenzelm@13515
   253
      by (rule subspace.mult_closed)
wenzelm@13515
   254
    with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
wenzelm@13515
   255
    finally show ?thesis .
bauerg@9261
   256
  qed
bauerg@9261
   257
qed
wenzelm@7917
   258
wenzelm@58744
   259
text \<open>
wenzelm@61486
   260
  \<^medskip>
wenzelm@61540
   261
  The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an
wenzelm@61540
   262
  extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close>
wenzelm@61540
   263
  and the supremum is an extension for every element of the chain.
wenzelm@58744
   264
\<close>
wenzelm@7917
   265
wenzelm@7917
   266
lemma sup_ext:
wenzelm@13515
   267
  assumes graph: "graph H h = \<Union>c"
wenzelm@13515
   268
    and M: "M = norm_pres_extensions E p F f"
popescua@52183
   269
    and cM: "c \<in> chains M"
wenzelm@13515
   270
    and ex: "\<exists>x. x \<in> c"
wenzelm@13515
   271
  shows "graph F f \<subseteq> graph H h"
bauerg@9261
   272
proof -
wenzelm@13515
   273
  from ex obtain x where xc: "x \<in> c" ..
wenzelm@13515
   274
  from cM have "c \<subseteq> M" ..
wenzelm@13515
   275
  with xc have "x \<in> M" ..
wenzelm@13515
   276
  with M have "x \<in> norm_pres_extensions E p F f"
wenzelm@13515
   277
    by (simp only:)
wenzelm@13515
   278
  then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" ..
wenzelm@13515
   279
  then have "graph F f \<subseteq> x" by (simp only:)
wenzelm@13515
   280
  also from xc have "\<dots> \<subseteq> \<Union>c" by blast
wenzelm@13515
   281
  also from graph have "\<dots> = graph H h" ..
wenzelm@13515
   282
  finally show ?thesis .
bauerg@9261
   283
qed
wenzelm@7917
   284
wenzelm@58744
   285
text \<open>
wenzelm@61486
   286
  \<^medskip>
wenzelm@61879
   287
  The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is a
wenzelm@61879
   288
  subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure
wenzelm@61539
   289
  properties follow from the fact that \<open>F\<close> is a vector space.
wenzelm@58744
   290
\<close>
wenzelm@7917
   291
wenzelm@10687
   292
lemma sup_supF:
wenzelm@13515
   293
  assumes graph: "graph H h = \<Union>c"
wenzelm@13515
   294
    and M: "M = norm_pres_extensions E p F f"
popescua@52183
   295
    and cM: "c \<in> chains M"
wenzelm@13515
   296
    and ex: "\<exists>x. x \<in> c"
wenzelm@13515
   297
    and FE: "F \<unlhd> E"
wenzelm@13515
   298
  shows "F \<unlhd> H"
wenzelm@13515
   299
proof
wenzelm@13515
   300
  from FE show "F \<noteq> {}" by (rule subspace.non_empty)
wenzelm@13515
   301
  from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext)
wenzelm@13515
   302
  then show "F \<subseteq> H" ..
wenzelm@13515
   303
  fix x y assume "x \<in> F" and "y \<in> F"
wenzelm@13515
   304
  with FE show "x + y \<in> F" by (rule subspace.add_closed)
wenzelm@13515
   305
next
wenzelm@13515
   306
  fix x a assume "x \<in> F"
wenzelm@13515
   307
  with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)
bauerg@9261
   308
qed
wenzelm@7917
   309
wenzelm@58744
   310
text \<open>
wenzelm@61486
   311
  \<^medskip>
wenzelm@61540
   312
  The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>.
wenzelm@58744
   313
\<close>
wenzelm@7917
   314
wenzelm@10687
   315
lemma sup_subE:
wenzelm@13515
   316
  assumes graph: "graph H h = \<Union>c"
wenzelm@13515
   317
    and M: "M = norm_pres_extensions E p F f"
popescua@52183
   318
    and cM: "c \<in> chains M"
wenzelm@13515
   319
    and ex: "\<exists>x. x \<in> c"
wenzelm@13515
   320
    and FE: "F \<unlhd> E"
wenzelm@13515
   321
    and E: "vectorspace E"
wenzelm@13515
   322
  shows "H \<unlhd> E"
wenzelm@13515
   323
proof
wenzelm@13515
   324
  show "H \<noteq> {}"
wenzelm@13515
   325
  proof -
wenzelm@13547
   326
    from FE E have "0 \<in> F" by (rule subspace.zero)
wenzelm@13515
   327
    also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF)
wenzelm@13515
   328
    then have "F \<subseteq> H" ..
wenzelm@13515
   329
    finally show ?thesis by blast
wenzelm@13515
   330
  qed
wenzelm@13515
   331
  show "H \<subseteq> E"
bauerg@9261
   332
  proof
wenzelm@13515
   333
    fix x assume "x \<in> H"
wenzelm@13515
   334
    with M cM graph
wenzelm@44887
   335
    obtain H' where x: "x \<in> H'" and H'E: "H' \<unlhd> E"
wenzelm@13515
   336
      by (rule some_H'h' [elim_format]) blast
wenzelm@13515
   337
    from H'E have "H' \<subseteq> E" ..
wenzelm@13515
   338
    with x show "x \<in> E" ..
wenzelm@13515
   339
  qed
wenzelm@13515
   340
  fix x y assume x: "x \<in> H" and y: "y \<in> H"
wenzelm@13515
   341
  show "x + y \<in> H"
wenzelm@13515
   342
  proof -
wenzelm@13515
   343
    from M cM graph x y obtain H' h' where
wenzelm@13515
   344
          x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E"
wenzelm@13515
   345
        and graphs: "graph H' h' \<subseteq> graph H h"
wenzelm@13515
   346
      by (rule some_H'h'2 [elim_format]) blast
wenzelm@13515
   347
    from H'E x' y' have "x + y \<in> H'"
wenzelm@13515
   348
      by (rule subspace.add_closed)
wenzelm@13515
   349
    also from graphs have "H' \<subseteq> H" ..
wenzelm@13515
   350
    finally show ?thesis .
wenzelm@13515
   351
  qed
wenzelm@13515
   352
next
wenzelm@13515
   353
  fix x a assume x: "x \<in> H"
wenzelm@13515
   354
  show "a \<cdot> x \<in> H"
wenzelm@13515
   355
  proof -
wenzelm@13515
   356
    from M cM graph x
wenzelm@13515
   357
    obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E"
wenzelm@13515
   358
        and graphs: "graph H' h' \<subseteq> graph H h"
wenzelm@13515
   359
      by (rule some_H'h' [elim_format]) blast
wenzelm@13515
   360
    from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed)
wenzelm@13515
   361
    also from graphs have "H' \<subseteq> H" ..
wenzelm@13515
   362
    finally show ?thesis .
bauerg@9261
   363
  qed
bauerg@9261
   364
qed
wenzelm@7917
   365
wenzelm@58744
   366
text \<open>
wenzelm@61486
   367
  \<^medskip>
wenzelm@61879
   368
  The limit function is bounded by the norm \<open>p\<close> as well, since all elements in
wenzelm@61879
   369
  the chain are bounded by \<open>p\<close>.
wenzelm@58744
   370
\<close>
wenzelm@7917
   371
bauerg@9374
   372
lemma sup_norm_pres:
wenzelm@13515
   373
  assumes graph: "graph H h = \<Union>c"
wenzelm@13515
   374
    and M: "M = norm_pres_extensions E p F f"
popescua@52183
   375
    and cM: "c \<in> chains M"
wenzelm@13515
   376
  shows "\<forall>x \<in> H. h x \<le> p x"
bauerg@9261
   377
proof
wenzelm@9503
   378
  fix x assume "x \<in> H"
wenzelm@13515
   379
  with M cM graph obtain H' h' where x': "x \<in> H'"
wenzelm@13515
   380
      and graphs: "graph H' h' \<subseteq> graph H h"
wenzelm@10687
   381
      and a: "\<forall>x \<in> H'. h' x \<le> p x"
wenzelm@13515
   382
    by (rule some_H'h' [elim_format]) blast
wenzelm@13515
   383
  from graphs x' have [symmetric]: "h' x = h x" ..
wenzelm@13515
   384
  also from a x' have "h' x \<le> p x " ..
wenzelm@13515
   385
  finally show "h x \<le> p x" .
bauerg@9261
   386
qed
wenzelm@7917
   387
wenzelm@58744
   388
text \<open>
wenzelm@61486
   389
  \<^medskip>
wenzelm@61879
   390
  The following lemma is a property of linear forms on real vector spaces. It
wenzelm@61879
   391
  will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page
wenzelm@61879
   392
  \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces the
wenzelm@61879
   393
  following inequality are equivalent:
wenzelm@10687
   394
  \begin{center}
wenzelm@10687
   395
  \begin{tabular}{lll}
wenzelm@61539
   396
  \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
wenzelm@61539
   397
  \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
wenzelm@10687
   398
  \end{tabular}
wenzelm@10687
   399
  \end{center}
wenzelm@58744
   400
\<close>
wenzelm@7917
   401
wenzelm@10687
   402
lemma abs_ineq_iff:
ballarin@27611
   403
  assumes "subspace H E" and "vectorspace E" and "seminorm E p"
ballarin@27611
   404
    and "linearform H h"
wenzelm@13515
   405
  shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
wenzelm@13515
   406
proof
ballarin@29234
   407
  interpret subspace H E by fact
ballarin@29234
   408
  interpret vectorspace E by fact
ballarin@29234
   409
  interpret seminorm E p by fact
ballarin@29234
   410
  interpret linearform H h by fact
wenzelm@58744
   411
  have H: "vectorspace H" using \<open>vectorspace E\<close> ..
wenzelm@13515
   412
  {
bauerg@9261
   413
    assume l: ?L
bauerg@9261
   414
    show ?R
bauerg@9261
   415
    proof
wenzelm@9503
   416
      fix x assume x: "x \<in> H"
wenzelm@13515
   417
      have "h x \<le> \<bar>h x\<bar>" by arith
wenzelm@13515
   418
      also from l x have "\<dots> \<le> p x" ..
wenzelm@10687
   419
      finally show "h x \<le> p x" .
bauerg@9261
   420
    qed
bauerg@9261
   421
  next
bauerg@9261
   422
    assume r: ?R
bauerg@9261
   423
    show ?L
wenzelm@10687
   424
    proof
wenzelm@13515
   425
      fix x assume x: "x \<in> H"
wenzelm@60595
   426
      show "\<bar>b\<bar> \<le> a" when "- a \<le> b" "b \<le> a" for a b :: real
wenzelm@60595
   427
        using that by arith
wenzelm@58744
   428
      from \<open>linearform H h\<close> and H x
wenzelm@23378
   429
      have "- h x = h (- x)" by (rule linearform.neg [symmetric])
bauerg@14710
   430
      also
bauerg@14710
   431
      from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
bauerg@14710
   432
      with r have "h (- x) \<le> p (- x)" ..
bauerg@14710
   433
      also have "\<dots> = p x"
wenzelm@58744
   434
        using \<open>seminorm E p\<close> \<open>vectorspace E\<close>
bauerg@14710
   435
      proof (rule seminorm.minus)
bauerg@14710
   436
        from x show "x \<in> E" ..
bauerg@9261
   437
      qed
bauerg@14710
   438
      finally have "- h x \<le> p x" .
bauerg@14710
   439
      then show "- p x \<le> h x" by simp
wenzelm@13515
   440
      from r x show "h x \<le> p x" ..
bauerg@9261
   441
    qed
wenzelm@13515
   442
  }
wenzelm@10687
   443
qed
wenzelm@7917
   444
wenzelm@10687
   445
end