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