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';
tuned comments;
     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