1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/HahnBanach/HahnBanachSupLemmas.thy Tue Dec 30 11:10:01 2008 +0100
1.3 @@ -0,0 +1,446 @@
1.4 +(* Title: HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
1.5 + ID: $Id$
1.6 + Author: Gertrud Bauer, TU Munich
1.7 +*)
1.8 +
1.9 +header {* The supremum w.r.t.~the function order *}
1.10 +
1.11 +theory HahnBanachSupLemmas
1.12 +imports FunctionNorm ZornLemma
1.13 +begin
1.14 +
1.15 +text {*
1.16 + This section contains some lemmas that will be used in the proof of
1.17 + the Hahn-Banach Theorem. In this section the following context is
1.18 + presumed. Let @{text E} be a real vector space with a seminorm
1.19 + @{text p} on @{text E}. @{text F} is a subspace of @{text E} and
1.20 + @{text f} a linear form on @{text F}. We consider a chain @{text c}
1.21 + of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =
1.22 + graph H h"}. We will show some properties about the limit function
1.23 + @{text h}, i.e.\ the supremum of the chain @{text c}.
1.24 +
1.25 + \medskip Let @{text c} be a chain of norm-preserving extensions of
1.26 + the function @{text f} and let @{text "graph H h"} be the supremum
1.27 + of @{text c}. Every element in @{text H} is member of one of the
1.28 + elements of the chain.
1.29 +*}
1.30 +lemmas [dest?] = chainD
1.31 +lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
1.32 +
1.33 +lemma some_H'h't:
1.34 + assumes M: "M = norm_pres_extensions E p F f"
1.35 + and cM: "c \<in> chain M"
1.36 + and u: "graph H h = \<Union>c"
1.37 + and x: "x \<in> H"
1.38 + shows "\<exists>H' h'. graph H' h' \<in> c
1.39 + \<and> (x, h x) \<in> graph H' h'
1.40 + \<and> linearform H' h' \<and> H' \<unlhd> E
1.41 + \<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h'
1.42 + \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
1.43 +proof -
1.44 + from x have "(x, h x) \<in> graph H h" ..
1.45 + also from u have "\<dots> = \<Union>c" .
1.46 + finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast
1.47 +
1.48 + from cM have "c \<subseteq> M" ..
1.49 + with gc have "g \<in> M" ..
1.50 + also from M have "\<dots> = norm_pres_extensions E p F f" .
1.51 + finally obtain H' and h' where g: "g = graph H' h'"
1.52 + and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'"
1.53 + "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" ..
1.54 +
1.55 + from gc and g have "graph H' h' \<in> c" by (simp only:)
1.56 + moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:)
1.57 + ultimately show ?thesis using * by blast
1.58 +qed
1.59 +
1.60 +text {*
1.61 + \medskip Let @{text c} be a chain of norm-preserving extensions of
1.62 + the function @{text f} and let @{text "graph H h"} be the supremum
1.63 + of @{text c}. Every element in the domain @{text H} of the supremum
1.64 + function is member of the domain @{text H'} of some function @{text
1.65 + h'}, such that @{text h} extends @{text h'}.
1.66 +*}
1.67 +
1.68 +lemma some_H'h':
1.69 + assumes M: "M = norm_pres_extensions E p F f"
1.70 + and cM: "c \<in> chain M"
1.71 + and u: "graph H h = \<Union>c"
1.72 + and x: "x \<in> H"
1.73 + shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
1.74 + \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
1.75 + \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
1.76 +proof -
1.77 + from M cM u x obtain H' h' where
1.78 + x_hx: "(x, h x) \<in> graph H' h'"
1.79 + and c: "graph H' h' \<in> c"
1.80 + and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'"
1.81 + "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
1.82 + by (rule some_H'h't [elim_format]) blast
1.83 + from x_hx have "x \<in> H'" ..
1.84 + moreover from cM u c have "graph H' h' \<subseteq> graph H h"
1.85 + by (simp only: chain_ball_Union_upper)
1.86 + ultimately show ?thesis using * by blast
1.87 +qed
1.88 +
1.89 +text {*
1.90 + \medskip Any two elements @{text x} and @{text y} in the domain
1.91 + @{text H} of the supremum function @{text h} are both in the domain
1.92 + @{text H'} of some function @{text h'}, such that @{text h} extends
1.93 + @{text h'}.
1.94 +*}
1.95 +
1.96 +lemma some_H'h'2:
1.97 + assumes M: "M = norm_pres_extensions E p F f"
1.98 + and cM: "c \<in> chain M"
1.99 + and u: "graph H h = \<Union>c"
1.100 + and x: "x \<in> H"
1.101 + and y: "y \<in> H"
1.102 + shows "\<exists>H' h'. x \<in> H' \<and> y \<in> H'
1.103 + \<and> graph H' h' \<subseteq> graph H h
1.104 + \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
1.105 + \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
1.106 +proof -
1.107 + txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
1.108 + such that @{text h} extends @{text h''}. *}
1.109 +
1.110 + from M cM u and y obtain H' h' where
1.111 + y_hy: "(y, h y) \<in> graph H' h'"
1.112 + and c': "graph H' h' \<in> c"
1.113 + and * :
1.114 + "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'"
1.115 + "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x"
1.116 + by (rule some_H'h't [elim_format]) blast
1.117 +
1.118 + txt {* @{text x} is in the domain @{text H'} of some function @{text h'},
1.119 + such that @{text h} extends @{text h'}. *}
1.120 +
1.121 + from M cM u and x obtain H'' h'' where
1.122 + x_hx: "(x, h x) \<in> graph H'' h''"
1.123 + and c'': "graph H'' h'' \<in> c"
1.124 + and ** :
1.125 + "linearform H'' h''" "H'' \<unlhd> E" "F \<unlhd> H''"
1.126 + "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x"
1.127 + by (rule some_H'h't [elim_format]) blast
1.128 +
1.129 + txt {* Since both @{text h'} and @{text h''} are elements of the chain,
1.130 + @{text h''} is an extension of @{text h'} or vice versa. Thus both
1.131 + @{text x} and @{text y} are contained in the greater
1.132 + one. \label{cases1}*}
1.133 +
1.134 + from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
1.135 + (is "?case1 \<or> ?case2") ..
1.136 + then show ?thesis
1.137 + proof
1.138 + assume ?case1
1.139 + have "(x, h x) \<in> graph H'' h''" by fact
1.140 + also have "\<dots> \<subseteq> graph H' h'" by fact
1.141 + finally have xh:"(x, h x) \<in> graph H' h'" .
1.142 + then have "x \<in> H'" ..
1.143 + moreover from y_hy have "y \<in> H'" ..
1.144 + moreover from cM u and c' have "graph H' h' \<subseteq> graph H h"
1.145 + by (simp only: chain_ball_Union_upper)
1.146 + ultimately show ?thesis using * by blast
1.147 + next
1.148 + assume ?case2
1.149 + from x_hx have "x \<in> H''" ..
1.150 + moreover {
1.151 + have "(y, h y) \<in> graph H' h'" by (rule y_hy)
1.152 + also have "\<dots> \<subseteq> graph H'' h''" by fact
1.153 + finally have "(y, h y) \<in> graph H'' h''" .
1.154 + } then have "y \<in> H''" ..
1.155 + moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h"
1.156 + by (simp only: chain_ball_Union_upper)
1.157 + ultimately show ?thesis using ** by blast
1.158 + qed
1.159 +qed
1.160 +
1.161 +text {*
1.162 + \medskip The relation induced by the graph of the supremum of a
1.163 + chain @{text c} is definite, i.~e.~t is the graph of a function.
1.164 +*}
1.165 +
1.166 +lemma sup_definite:
1.167 + assumes M_def: "M \<equiv> norm_pres_extensions E p F f"
1.168 + and cM: "c \<in> chain M"
1.169 + and xy: "(x, y) \<in> \<Union>c"
1.170 + and xz: "(x, z) \<in> \<Union>c"
1.171 + shows "z = y"
1.172 +proof -
1.173 + from cM have c: "c \<subseteq> M" ..
1.174 + from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" ..
1.175 + from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" ..
1.176 +
1.177 + from G1 c have "G1 \<in> M" ..
1.178 + then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
1.179 + unfolding M_def by blast
1.180 +
1.181 + from G2 c have "G2 \<in> M" ..
1.182 + then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
1.183 + unfolding M_def by blast
1.184 +
1.185 + txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
1.186 + or vice versa, since both @{text "G\<^sub>1"} and @{text
1.187 + "G\<^sub>2"} are members of @{text c}. \label{cases2}*}
1.188 +
1.189 + from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
1.190 + then show ?thesis
1.191 + proof
1.192 + assume ?case1
1.193 + with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
1.194 + then have "y = h2 x" ..
1.195 + also
1.196 + from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)
1.197 + then have "z = h2 x" ..
1.198 + finally show ?thesis .
1.199 + next
1.200 + assume ?case2
1.201 + with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
1.202 + then have "z = h1 x" ..
1.203 + also
1.204 + from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)
1.205 + then have "y = h1 x" ..
1.206 + finally show ?thesis ..
1.207 + qed
1.208 +qed
1.209 +
1.210 +text {*
1.211 + \medskip The limit function @{text h} is linear. Every element
1.212 + @{text x} in the domain of @{text h} is in the domain of a function
1.213 + @{text h'} in the chain of norm preserving extensions. Furthermore,
1.214 + @{text h} is an extension of @{text h'} so the function values of
1.215 + @{text x} are identical for @{text h'} and @{text h}. Finally, the
1.216 + function @{text h'} is linear by construction of @{text M}.
1.217 +*}
1.218 +
1.219 +lemma sup_lf:
1.220 + assumes M: "M = norm_pres_extensions E p F f"
1.221 + and cM: "c \<in> chain M"
1.222 + and u: "graph H h = \<Union>c"
1.223 + shows "linearform H h"
1.224 +proof
1.225 + fix x y assume x: "x \<in> H" and y: "y \<in> H"
1.226 + with M cM u obtain H' h' where
1.227 + x': "x \<in> H'" and y': "y \<in> H'"
1.228 + and b: "graph H' h' \<subseteq> graph H h"
1.229 + and linearform: "linearform H' h'"
1.230 + and subspace: "H' \<unlhd> E"
1.231 + by (rule some_H'h'2 [elim_format]) blast
1.232 +
1.233 + show "h (x + y) = h x + h y"
1.234 + proof -
1.235 + from linearform x' y' have "h' (x + y) = h' x + h' y"
1.236 + by (rule linearform.add)
1.237 + also from b x' have "h' x = h x" ..
1.238 + also from b y' have "h' y = h y" ..
1.239 + also from subspace x' y' have "x + y \<in> H'"
1.240 + by (rule subspace.add_closed)
1.241 + with b have "h' (x + y) = h (x + y)" ..
1.242 + finally show ?thesis .
1.243 + qed
1.244 +next
1.245 + fix x a assume x: "x \<in> H"
1.246 + with M cM u obtain H' h' where
1.247 + x': "x \<in> H'"
1.248 + and b: "graph H' h' \<subseteq> graph H h"
1.249 + and linearform: "linearform H' h'"
1.250 + and subspace: "H' \<unlhd> E"
1.251 + by (rule some_H'h' [elim_format]) blast
1.252 +
1.253 + show "h (a \<cdot> x) = a * h x"
1.254 + proof -
1.255 + from linearform x' have "h' (a \<cdot> x) = a * h' x"
1.256 + by (rule linearform.mult)
1.257 + also from b x' have "h' x = h x" ..
1.258 + also from subspace x' have "a \<cdot> x \<in> H'"
1.259 + by (rule subspace.mult_closed)
1.260 + with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
1.261 + finally show ?thesis .
1.262 + qed
1.263 +qed
1.264 +
1.265 +text {*
1.266 + \medskip The limit of a non-empty chain of norm preserving
1.267 + extensions of @{text f} is an extension of @{text f}, since every
1.268 + element of the chain is an extension of @{text f} and the supremum
1.269 + is an extension for every element of the chain.
1.270 +*}
1.271 +
1.272 +lemma sup_ext:
1.273 + assumes graph: "graph H h = \<Union>c"
1.274 + and M: "M = norm_pres_extensions E p F f"
1.275 + and cM: "c \<in> chain M"
1.276 + and ex: "\<exists>x. x \<in> c"
1.277 + shows "graph F f \<subseteq> graph H h"
1.278 +proof -
1.279 + from ex obtain x where xc: "x \<in> c" ..
1.280 + from cM have "c \<subseteq> M" ..
1.281 + with xc have "x \<in> M" ..
1.282 + with M have "x \<in> norm_pres_extensions E p F f"
1.283 + by (simp only:)
1.284 + then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" ..
1.285 + then have "graph F f \<subseteq> x" by (simp only:)
1.286 + also from xc have "\<dots> \<subseteq> \<Union>c" by blast
1.287 + also from graph have "\<dots> = graph H h" ..
1.288 + finally show ?thesis .
1.289 +qed
1.290 +
1.291 +text {*
1.292 + \medskip The domain @{text H} of the limit function is a superspace
1.293 + of @{text F}, since @{text F} is a subset of @{text H}. The
1.294 + existence of the @{text 0} element in @{text F} and the closure
1.295 + properties follow from the fact that @{text F} is a vector space.
1.296 +*}
1.297 +
1.298 +lemma sup_supF:
1.299 + assumes graph: "graph H h = \<Union>c"
1.300 + and M: "M = norm_pres_extensions E p F f"
1.301 + and cM: "c \<in> chain M"
1.302 + and ex: "\<exists>x. x \<in> c"
1.303 + and FE: "F \<unlhd> E"
1.304 + shows "F \<unlhd> H"
1.305 +proof
1.306 + from FE show "F \<noteq> {}" by (rule subspace.non_empty)
1.307 + from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext)
1.308 + then show "F \<subseteq> H" ..
1.309 + fix x y assume "x \<in> F" and "y \<in> F"
1.310 + with FE show "x + y \<in> F" by (rule subspace.add_closed)
1.311 +next
1.312 + fix x a assume "x \<in> F"
1.313 + with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)
1.314 +qed
1.315 +
1.316 +text {*
1.317 + \medskip The domain @{text H} of the limit function is a subspace of
1.318 + @{text E}.
1.319 +*}
1.320 +
1.321 +lemma sup_subE:
1.322 + assumes graph: "graph H h = \<Union>c"
1.323 + and M: "M = norm_pres_extensions E p F f"
1.324 + and cM: "c \<in> chain M"
1.325 + and ex: "\<exists>x. x \<in> c"
1.326 + and FE: "F \<unlhd> E"
1.327 + and E: "vectorspace E"
1.328 + shows "H \<unlhd> E"
1.329 +proof
1.330 + show "H \<noteq> {}"
1.331 + proof -
1.332 + from FE E have "0 \<in> F" by (rule subspace.zero)
1.333 + also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF)
1.334 + then have "F \<subseteq> H" ..
1.335 + finally show ?thesis by blast
1.336 + qed
1.337 + show "H \<subseteq> E"
1.338 + proof
1.339 + fix x assume "x \<in> H"
1.340 + with M cM graph
1.341 + obtain H' h' where x: "x \<in> H'" and H'E: "H' \<unlhd> E"
1.342 + by (rule some_H'h' [elim_format]) blast
1.343 + from H'E have "H' \<subseteq> E" ..
1.344 + with x show "x \<in> E" ..
1.345 + qed
1.346 + fix x y assume x: "x \<in> H" and y: "y \<in> H"
1.347 + show "x + y \<in> H"
1.348 + proof -
1.349 + from M cM graph x y obtain H' h' where
1.350 + x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E"
1.351 + and graphs: "graph H' h' \<subseteq> graph H h"
1.352 + by (rule some_H'h'2 [elim_format]) blast
1.353 + from H'E x' y' have "x + y \<in> H'"
1.354 + by (rule subspace.add_closed)
1.355 + also from graphs have "H' \<subseteq> H" ..
1.356 + finally show ?thesis .
1.357 + qed
1.358 +next
1.359 + fix x a assume x: "x \<in> H"
1.360 + show "a \<cdot> x \<in> H"
1.361 + proof -
1.362 + from M cM graph x
1.363 + obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E"
1.364 + and graphs: "graph H' h' \<subseteq> graph H h"
1.365 + by (rule some_H'h' [elim_format]) blast
1.366 + from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed)
1.367 + also from graphs have "H' \<subseteq> H" ..
1.368 + finally show ?thesis .
1.369 + qed
1.370 +qed
1.371 +
1.372 +text {*
1.373 + \medskip The limit function is bounded by the norm @{text p} as
1.374 + well, since all elements in the chain are bounded by @{text p}.
1.375 +*}
1.376 +
1.377 +lemma sup_norm_pres:
1.378 + assumes graph: "graph H h = \<Union>c"
1.379 + and M: "M = norm_pres_extensions E p F f"
1.380 + and cM: "c \<in> chain M"
1.381 + shows "\<forall>x \<in> H. h x \<le> p x"
1.382 +proof
1.383 + fix x assume "x \<in> H"
1.384 + with M cM graph obtain H' h' where x': "x \<in> H'"
1.385 + and graphs: "graph H' h' \<subseteq> graph H h"
1.386 + and a: "\<forall>x \<in> H'. h' x \<le> p x"
1.387 + by (rule some_H'h' [elim_format]) blast
1.388 + from graphs x' have [symmetric]: "h' x = h x" ..
1.389 + also from a x' have "h' x \<le> p x " ..
1.390 + finally show "h x \<le> p x" .
1.391 +qed
1.392 +
1.393 +text {*
1.394 + \medskip The following lemma is a property of linear forms on real
1.395 + vector spaces. It will be used for the lemma @{text abs_HahnBanach}
1.396 + (see page \pageref{abs-HahnBanach}). \label{abs-ineq-iff} For real
1.397 + vector spaces the following inequations are equivalent:
1.398 + \begin{center}
1.399 + \begin{tabular}{lll}
1.400 + @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
1.401 + @{text "\<forall>x \<in> H. h x \<le> p x"} \\
1.402 + \end{tabular}
1.403 + \end{center}
1.404 +*}
1.405 +
1.406 +lemma abs_ineq_iff:
1.407 + assumes "subspace H E" and "vectorspace E" and "seminorm E p"
1.408 + and "linearform H h"
1.409 + shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
1.410 +proof
1.411 + interpret subspace H E by fact
1.412 + interpret vectorspace E by fact
1.413 + interpret seminorm E p by fact
1.414 + interpret linearform H h by fact
1.415 + have H: "vectorspace H" using `vectorspace E` ..
1.416 + {
1.417 + assume l: ?L
1.418 + show ?R
1.419 + proof
1.420 + fix x assume x: "x \<in> H"
1.421 + have "h x \<le> \<bar>h x\<bar>" by arith
1.422 + also from l x have "\<dots> \<le> p x" ..
1.423 + finally show "h x \<le> p x" .
1.424 + qed
1.425 + next
1.426 + assume r: ?R
1.427 + show ?L
1.428 + proof
1.429 + fix x assume x: "x \<in> H"
1.430 + show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
1.431 + by arith
1.432 + from `linearform H h` and H x
1.433 + have "- h x = h (- x)" by (rule linearform.neg [symmetric])
1.434 + also
1.435 + from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
1.436 + with r have "h (- x) \<le> p (- x)" ..
1.437 + also have "\<dots> = p x"
1.438 + using `seminorm E p` `vectorspace E`
1.439 + proof (rule seminorm.minus)
1.440 + from x show "x \<in> E" ..
1.441 + qed
1.442 + finally have "- h x \<le> p x" .
1.443 + then show "- p x \<le> h x" by simp
1.444 + from r x show "h x \<le> p x" ..
1.445 + qed
1.446 + }
1.447 +qed
1.448 +
1.449 +end