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