src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
 author wenzelm Mon Apr 25 16:09:26 2016 +0200 (2016-04-25) changeset 63040 eb4ddd18d635 parent 61879 e4f9d8f094fe permissions -rw-r--r--
eliminated old 'def';
     1 (*  Title:      HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy

     2     Author:     Gertrud Bauer, TU Munich

     3 *)

     4

     5 section \<open>The supremum wrt.\ the function order\<close>

     6

     7 theory Hahn_Banach_Sup_Lemmas

     8 imports Function_Norm Zorn_Lemma

     9 begin

    10

    11 text \<open>

    12   This section contains some lemmas that will be used in the proof of the

    13   Hahn-Banach Theorem. In this section the following context is presumed. Let

    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

    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

    16   extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will show some properties

    17   about the limit function \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>.

    18

    19   \<^medskip>

    20   Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let

    21   \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of one of

    22   the elements of the chain.

    23 \<close>

    24

    25 lemmas [dest?] = chainsD

    26 lemmas chainsE2 [elim?] = chainsD2 [elim_format]

    27

    28 lemma some_H'h't:

    29   assumes M: "M = norm_pres_extensions E p F f"

    30     and cM: "c \<in> chains M"

    31     and u: "graph H h = \<Union>c"

    32     and x: "x \<in> H"

    33   shows "\<exists>H' h'. graph H' h' \<in> c

    34     \<and> (x, h x) \<in> graph H' h'

    35     \<and> linearform H' h' \<and> H' \<unlhd> E

    36     \<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h'

    37     \<and> (\<forall>x \<in> H'. h' x \<le> p x)"

    38 proof -

    39   from x have "(x, h x) \<in> graph H h" ..

    40   also from u have "\<dots> = \<Union>c" .

    41   finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast

    42

    43   from cM have "c \<subseteq> M" ..

    44   with gc have "g \<in> M" ..

    45   also from M have "\<dots> = norm_pres_extensions E p F f" .

    46   finally obtain H' and h' where g: "g = graph H' h'"

    47     and * : "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"

    48       "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x" ..

    49

    50   from gc and g have "graph H' h' \<in> c" by (simp only:)

    51   moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:)

    52   ultimately show ?thesis using * by blast

    53 qed

    54

    55 text \<open>

    56   \<^medskip>

    57   Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let

    58   \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of the

    59   supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such

    60   that \<open>h\<close> extends \<open>h'\<close>.

    61 \<close>

    62

    63 lemma some_H'h':

    64   assumes M: "M = norm_pres_extensions E p F f"

    65     and cM: "c \<in> chains M"

    66     and u: "graph H h = \<Union>c"

    67     and x: "x \<in> H"

    68   shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h

    69     \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'

    70     \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"

    71 proof -

    72   from M cM u x obtain H' h' where

    73       x_hx: "(x, h x) \<in> graph H' h'"

    74     and c: "graph H' h' \<in> c"

    75     and * : "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"

    76       "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"

    77     by (rule some_H'h't [elim_format]) blast

    78   from x_hx have "x \<in> H'" ..

    79   moreover from cM u c have "graph H' h' \<subseteq> graph H h" by blast

    80   ultimately show ?thesis using * by blast

    81 qed

    82

    83 text \<open>

    84   \<^medskip>

    85   Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function \<open>h\<close>

    86   are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends

    87   \<open>h'\<close>.

    88 \<close>

    89

    90 lemma some_H'h'2:

    91   assumes M: "M = norm_pres_extensions E p F f"

    92     and cM: "c \<in> chains M"

    93     and u: "graph H h = \<Union>c"

    94     and x: "x \<in> H"

    95     and y: "y \<in> H"

    96   shows "\<exists>H' h'. x \<in> H' \<and> y \<in> H'

    97     \<and> graph H' h' \<subseteq> graph H h

    98     \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'

    99     \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"

   100 proof -

   101   txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, such that \<open>h\<close>

   102     extends \<open>h''\<close>.\<close>

   103

   104   from M cM u and y obtain H' h' where

   105       y_hy: "(y, h y) \<in> graph H' h'"

   106     and c': "graph H' h' \<in> c"

   107     and * :

   108       "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"

   109       "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"

   110     by (rule some_H'h't [elim_format]) blast

   111

   112   txt \<open>\<open>x\<close> is in the domain \<open>H'\<close> of some function \<open>h'\<close>,

   113     such that \<open>h\<close> extends \<open>h'\<close>.\<close>

   114

   115   from M cM u and x obtain H'' h'' where

   116       x_hx: "(x, h x) \<in> graph H'' h''"

   117     and c'': "graph H'' h'' \<in> c"

   118     and ** :

   119       "linearform H'' h''"  "H'' \<unlhd> E"  "F \<unlhd> H''"

   120       "graph F f \<subseteq> graph H'' h''"  "\<forall>x \<in> H''. h'' x \<le> p x"

   121     by (rule some_H'h't [elim_format]) blast

   122

   123   txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, \<open>h''\<close> is an

   124     extension of \<open>h'\<close> or vice versa. Thus both \<open>x\<close> and \<open>y\<close> are contained in

   125     the greater one. \label{cases1}\<close>

   126

   127   from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"

   128     by (blast dest: chainsD)

   129   then show ?thesis

   130   proof cases

   131     case 1

   132     have "(x, h x) \<in> graph H'' h''" by fact

   133     also have "\<dots> \<subseteq> graph H' h'" by fact

   134     finally have xh:"(x, h x) \<in> graph H' h'" .

   135     then have "x \<in> H'" ..

   136     moreover from y_hy have "y \<in> H'" ..

   137     moreover from cM u and c' have "graph H' h' \<subseteq> graph H h" by blast

   138     ultimately show ?thesis using * by blast

   139   next

   140     case 2

   141     from x_hx have "x \<in> H''" ..

   142     moreover have "y \<in> H''"

   143     proof -

   144       have "(y, h y) \<in> graph H' h'" by (rule y_hy)

   145       also have "\<dots> \<subseteq> graph H'' h''" by fact

   146       finally have "(y, h y) \<in> graph H'' h''" .

   147       then show ?thesis ..

   148     qed

   149     moreover from u 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 \<open>

   155   \<^medskip>

   156   The relation induced by the graph of the supremum of a chain \<open>c\<close> is

   157   definite, i.e.\ it is the graph of a function.

   158 \<close>

   159

   160 lemma sup_definite:

   161   assumes M_def: "M = norm_pres_extensions E p F f"

   162     and cM: "c \<in> chains M"

   163     and xy: "(x, y) \<in> \<Union>c"

   164     and xz: "(x, z) \<in> \<Union>c"

   165   shows "z = y"

   166 proof -

   167   from cM have c: "c \<subseteq> M" ..

   168   from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" ..

   169   from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" ..

   170

   171   from G1 c have "G1 \<in> M" ..

   172   then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"

   173     unfolding M_def by blast

   174

   175   from G2 c have "G2 \<in> M" ..

   176   then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"

   177     unfolding M_def by blast

   178

   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>

   180     are members of \<open>c\<close>. \label{cases2}\<close>

   181

   182   from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"

   183     by (blast dest: chainsD)

   184   then show ?thesis

   185   proof cases

   186     case 1

   187     with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast

   188     then have "y = h2 x" ..

   189     also

   190     from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)

   191     then have "z = h2 x" ..

   192     finally show ?thesis .

   193   next

   194     case 2

   195     with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast

   196     then have "z = h1 x" ..

   197     also

   198     from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)

   199     then have "y = h1 x" ..

   200     finally show ?thesis ..

   201   qed

   202 qed

   203

   204 text \<open>

   205   \<^medskip>

   206   The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> is

   207   in the domain of a function \<open>h'\<close> in the chain of norm preserving extensions.

   208   Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function values of \<open>x\<close> are

   209   identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> is linear by

   210   construction of \<open>M\<close>.

   211 \<close>

   212

   213 lemma sup_lf:

   214   assumes M: "M = norm_pres_extensions E p F f"

   215     and cM: "c \<in> chains M"

   216     and u: "graph H h = \<Union>c"

   217   shows "linearform H h"

   218 proof

   219   fix x y assume x: "x \<in> H" and y: "y \<in> H"

   220   with M cM u obtain H' h' where

   221         x': "x \<in> H'" and y': "y \<in> H'"

   222       and b: "graph H' h' \<subseteq> graph H h"

   223       and linearform: "linearform H' h'"

   224       and subspace: "H' \<unlhd> E"

   225     by (rule some_H'h'2 [elim_format]) blast

   226

   227   show "h (x + y) = h x + h y"

   228   proof -

   229     from linearform x' y' have "h' (x + y) = h' x + h' y"

   230       by (rule linearform.add)

   231     also from b x' have "h' x = h x" ..

   232     also from b y' have "h' y = h y" ..

   233     also from subspace x' y' have "x + y \<in> H'"

   234       by (rule subspace.add_closed)

   235     with b have "h' (x + y) = h (x + y)" ..

   236     finally show ?thesis .

   237   qed

   238 next

   239   fix x a assume x: "x \<in> H"

   240   with M cM u obtain H' h' where

   241         x': "x \<in> H'"

   242       and b: "graph H' h' \<subseteq> graph H h"

   243       and linearform: "linearform H' h'"

   244       and subspace: "H' \<unlhd> E"

   245     by (rule some_H'h' [elim_format]) blast

   246

   247   show "h (a \<cdot> x) = a * h x"

   248   proof -

   249     from linearform x' have "h' (a \<cdot> x) = a * h' x"

   250       by (rule linearform.mult)

   251     also from b x' have "h' x = h x" ..

   252     also from subspace x' have "a \<cdot> x \<in> H'"

   253       by (rule subspace.mult_closed)

   254     with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..

   255     finally show ?thesis .

   256   qed

   257 qed

   258

   259 text \<open>

   260   \<^medskip>

   261   The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an

   262   extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close>

   263   and the supremum is an extension for every element of the chain.

   264 \<close>

   265

   266 lemma sup_ext:

   267   assumes graph: "graph H h = \<Union>c"

   268     and M: "M = norm_pres_extensions E p F f"

   269     and cM: "c \<in> chains M"

   270     and ex: "\<exists>x. x \<in> c"

   271   shows "graph F f \<subseteq> graph H h"

   272 proof -

   273   from ex obtain x where xc: "x \<in> c" ..

   274   from cM have "c \<subseteq> M" ..

   275   with xc have "x \<in> M" ..

   276   with M have "x \<in> norm_pres_extensions E p F f"

   277     by (simp only:)

   278   then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" ..

   279   then have "graph F f \<subseteq> x" by (simp only:)

   280   also from xc have "\<dots> \<subseteq> \<Union>c" by blast

   281   also from graph have "\<dots> = graph H h" ..

   282   finally show ?thesis .

   283 qed

   284

   285 text \<open>

   286   \<^medskip>

   287   The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is a

   288   subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure

   289   properties follow from the fact that \<open>F\<close> is a vector space.

   290 \<close>

   291

   292 lemma sup_supF:

   293   assumes graph: "graph H h = \<Union>c"

   294     and M: "M = norm_pres_extensions E p F f"

   295     and cM: "c \<in> chains M"

   296     and ex: "\<exists>x. x \<in> c"

   297     and FE: "F \<unlhd> E"

   298   shows "F \<unlhd> H"

   299 proof

   300   from FE show "F \<noteq> {}" by (rule subspace.non_empty)

   301   from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext)

   302   then show "F \<subseteq> H" ..

   303   fix x y assume "x \<in> F" and "y \<in> F"

   304   with FE show "x + y \<in> F" by (rule subspace.add_closed)

   305 next

   306   fix x a assume "x \<in> F"

   307   with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)

   308 qed

   309

   310 text \<open>

   311   \<^medskip>

   312   The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>.

   313 \<close>

   314

   315 lemma sup_subE:

   316   assumes graph: "graph H h = \<Union>c"

   317     and M: "M = norm_pres_extensions E p F f"

   318     and cM: "c \<in> chains M"

   319     and ex: "\<exists>x. x \<in> c"

   320     and FE: "F \<unlhd> E"

   321     and E: "vectorspace E"

   322   shows "H \<unlhd> E"

   323 proof

   324   show "H \<noteq> {}"

   325   proof -

   326     from FE E have "0 \<in> F" by (rule subspace.zero)

   327     also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF)

   328     then have "F \<subseteq> H" ..

   329     finally show ?thesis by blast

   330   qed

   331   show "H \<subseteq> E"

   332   proof

   333     fix x assume "x \<in> H"

   334     with M cM graph

   335     obtain H' where x: "x \<in> H'" and H'E: "H' \<unlhd> E"

   336       by (rule some_H'h' [elim_format]) blast

   337     from H'E have "H' \<subseteq> E" ..

   338     with x show "x \<in> E" ..

   339   qed

   340   fix x y assume x: "x \<in> H" and y: "y \<in> H"

   341   show "x + y \<in> H"

   342   proof -

   343     from M cM graph x y obtain H' h' where

   344           x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E"

   345         and graphs: "graph H' h' \<subseteq> graph H h"

   346       by (rule some_H'h'2 [elim_format]) blast

   347     from H'E x' y' have "x + y \<in> H'"

   348       by (rule subspace.add_closed)

   349     also from graphs have "H' \<subseteq> H" ..

   350     finally show ?thesis .

   351   qed

   352 next

   353   fix x a assume x: "x \<in> H"

   354   show "a \<cdot> x \<in> H"

   355   proof -

   356     from M cM graph x

   357     obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E"

   358         and graphs: "graph H' h' \<subseteq> graph H h"

   359       by (rule some_H'h' [elim_format]) blast

   360     from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed)

   361     also from graphs have "H' \<subseteq> H" ..

   362     finally show ?thesis .

   363   qed

   364 qed

   365

   366 text \<open>

   367   \<^medskip>

   368   The limit function is bounded by the norm \<open>p\<close> as well, since all elements in

   369   the chain are bounded by \<open>p\<close>.

   370 \<close>

   371

   372 lemma sup_norm_pres:

   373   assumes graph: "graph H h = \<Union>c"

   374     and M: "M = norm_pres_extensions E p F f"

   375     and cM: "c \<in> chains M"

   376   shows "\<forall>x \<in> H. h x \<le> p x"

   377 proof

   378   fix x assume "x \<in> H"

   379   with M cM graph obtain H' h' where x': "x \<in> H'"

   380       and graphs: "graph H' h' \<subseteq> graph H h"

   381       and a: "\<forall>x \<in> H'. h' x \<le> p x"

   382     by (rule some_H'h' [elim_format]) blast

   383   from graphs x' have [symmetric]: "h' x = h x" ..

   384   also from a x' have "h' x \<le> p x " ..

   385   finally show "h x \<le> p x" .

   386 qed

   387

   388 text \<open>

   389   \<^medskip>

   390   The following lemma is a property of linear forms on real vector spaces. It

   391   will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page

   392   \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces the

   393   following inequality are equivalent:

   394   \begin{center}

   395   \begin{tabular}{lll}

   396   \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &

   397   \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\

   398   \end{tabular}

   399   \end{center}

   400 \<close>

   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 \<open>vectorspace E\<close> ..

   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 "\<bar>b\<bar> \<le> a" when "- a \<le> b" "b \<le> a" for a b :: real

   427         using that by arith

   428       from \<open>linearform H h\<close> 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 \<open>seminorm E p\<close> \<open>vectorspace E\<close>

   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