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