src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
 author wenzelm Wed Jun 24 21:46:54 2009 +0200 (2009-06-24) changeset 31795 be3e1cc5005c parent 29252 src/HOL/HahnBanach/HahnBanachSupLemmas.thy@ea97aa6aeba2 child 32960 69916a850301 permissions -rw-r--r--
standard naming conventions for session and theories;
     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