Up to index of Isabelle/HOL/HOL-Complex/HahnBanach
theory HahnBanachSupLemmas(* Title: HOL/Real/HahnBanach/HahnBanachSupLemmas.thy ID: $Id: HahnBanachSupLemmas.thy,v 1.21 2005/06/17 14:13:09 haftmann Exp $ Author: Gertrud Bauer, TU Munich *) header {* The supremum w.r.t.~the function order *} theory HahnBanachSupLemmas imports FunctionNorm ZornLemma begin text {* This section contains some lemmas that will be used in the proof of the Hahn-Banach Theorem. In this section the following context is presumed. Let @{text E} be a real vector space with a seminorm @{text p} on @{text E}. @{text F} is a subspace of @{text E} and @{text f} a linear form on @{text F}. We consider a chain @{text c} of norm-preserving extensions of @{text f}, such that @{text "\<Union>c = graph H h"}. We will show some properties about the limit function @{text h}, i.e.\ the supremum of the chain @{text c}. \medskip Let @{text c} be a chain of norm-preserving extensions of the function @{text f} and let @{text "graph H h"} be the supremum of @{text c}. Every element in @{text H} is member of one of the elements of the chain. *} lemmas [dest?] = chainD lemmas chainE2 [elim?] = chainD2 [elim_format, standard] lemma some_H'h't: assumes M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chain M" and u: "graph H h = \<Union>c" and x: "x ∈ H" shows "∃H' h'. graph H' h' ∈ c ∧ (x, h x) ∈ graph H' h' ∧ linearform H' h' ∧ H' \<unlhd> E ∧ F \<unlhd> H' ∧ graph F f ⊆ graph H' h' ∧ (∀x ∈ H'. h' x ≤ p x)" proof - from x have "(x, h x) ∈ graph H h" .. also from u have "… = \<Union>c" . finally obtain g where gc: "g ∈ c" and gh: "(x, h x) ∈ g" by blast from cM have "c ⊆ M" .. with gc have "g ∈ M" .. also from M have "… = norm_pres_extensions E p F f" . finally obtain H' and h' where g: "g = graph H' h'" and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'" "graph F f ⊆ graph H' h'" "∀x ∈ H'. h' x ≤ p x" .. from gc and g have "graph H' h' ∈ c" by (simp only:) moreover from gh and g have "(x, h x) ∈ graph H' h'" by (simp only:) ultimately show ?thesis using * by blast qed text {* \medskip Let @{text c} be a chain of norm-preserving extensions of the function @{text f} and let @{text "graph H h"} be the supremum of @{text c}. Every element in the domain @{text H} of the supremum function is member of the domain @{text H'} of some function @{text h'}, such that @{text h} extends @{text h'}. *} lemma some_H'h': assumes M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chain M" and u: "graph H h = \<Union>c" and x: "x ∈ H" shows "∃H' h'. x ∈ H' ∧ graph H' h' ⊆ graph H h ∧ linearform H' h' ∧ H' \<unlhd> E ∧ F \<unlhd> H' ∧ graph F f ⊆ graph H' h' ∧ (∀x ∈ H'. h' x ≤ p x)" proof - from M cM u x obtain H' h' where x_hx: "(x, h x) ∈ graph H' h'" and c: "graph H' h' ∈ c" and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'" "graph F f ⊆ graph H' h'" "∀x ∈ H'. h' x ≤ p x" by (rule some_H'h't [elim_format]) blast from x_hx have "x ∈ H'" .. moreover from cM u c have "graph H' h' ⊆ graph H h" by (simp only: chain_ball_Union_upper) ultimately show ?thesis using * by blast qed text {* \medskip Any two elements @{text x} and @{text y} in the domain @{text H} of the supremum function @{text h} are both in the domain @{text H'} of some function @{text h'}, such that @{text h} extends @{text h'}. *} lemma some_H'h'2: assumes M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chain M" and u: "graph H h = \<Union>c" and x: "x ∈ H" and y: "y ∈ H" shows "∃H' h'. x ∈ H' ∧ y ∈ H' ∧ graph H' h' ⊆ graph H h ∧ linearform H' h' ∧ H' \<unlhd> E ∧ F \<unlhd> H' ∧ graph F f ⊆ graph H' h' ∧ (∀x ∈ H'. h' x ≤ p x)" proof - txt {* @{text y} is in the domain @{text H''} of some function @{text h''}, such that @{text h} extends @{text h''}. *} from M cM u and y obtain H' h' where y_hy: "(y, h y) ∈ graph H' h'" and c': "graph H' h' ∈ c" and * : "linearform H' h'" "H' \<unlhd> E" "F \<unlhd> H'" "graph F f ⊆ graph H' h'" "∀x ∈ H'. h' x ≤ p x" by (rule some_H'h't [elim_format]) blast txt {* @{text x} is in the domain @{text H'} of some function @{text h'}, such that @{text h} extends @{text h'}. *} from M cM u and x obtain H'' h'' where x_hx: "(x, h x) ∈ graph H'' h''" and c'': "graph H'' h'' ∈ c" and ** : "linearform H'' h''" "H'' \<unlhd> E" "F \<unlhd> H''" "graph F f ⊆ graph H'' h''" "∀x ∈ H''. h'' x ≤ p x" by (rule some_H'h't [elim_format]) blast txt {* Since both @{text h'} and @{text h''} are elements of the chain, @{text h''} is an extension of @{text h'} or vice versa. Thus both @{text x} and @{text y} are contained in the greater one. \label{cases1}*} from cM have "graph H'' h'' ⊆ graph H' h' ∨ graph H' h' ⊆ graph H'' h''" (is "?case1 ∨ ?case2") .. then show ?thesis proof assume ?case1 have "(x, h x) ∈ graph H'' h''" . also have "... ⊆ graph H' h'" . finally have xh:"(x, h x) ∈ graph H' h'" . then have "x ∈ H'" .. moreover from y_hy have "y ∈ H'" .. moreover from cM u and c' have "graph H' h' ⊆ graph H h" by (simp only: chain_ball_Union_upper) ultimately show ?thesis using * by blast next assume ?case2 from x_hx have "x ∈ H''" .. moreover { from y_hy have "(y, h y) ∈ graph H' h'" . also have "… ⊆ graph H'' h''" . finally have "(y, h y) ∈ graph H'' h''" . } then have "y ∈ H''" .. moreover from cM u and c'' have "graph H'' h'' ⊆ graph H h" by (simp only: chain_ball_Union_upper) ultimately show ?thesis using ** by blast qed qed text {* \medskip The relation induced by the graph of the supremum of a chain @{text c} is definite, i.~e.~t is the graph of a function. *} lemma sup_definite: assumes M_def: "M ≡ norm_pres_extensions E p F f" and cM: "c ∈ chain M" and xy: "(x, y) ∈ \<Union>c" and xz: "(x, z) ∈ \<Union>c" shows "z = y" proof - from cM have c: "c ⊆ M" .. from xy obtain G1 where xy': "(x, y) ∈ G1" and G1: "G1 ∈ c" .. from xz obtain G2 where xz': "(x, z) ∈ G2" and G2: "G2 ∈ c" .. from G1 c have "G1 ∈ M" .. then obtain H1 h1 where G1_rep: "G1 = graph H1 h1" by (unfold M_def) blast from G2 c have "G2 ∈ M" .. then obtain H2 h2 where G2_rep: "G2 = graph H2 h2" by (unfold M_def) blast txt {* @{text "G1"} is contained in @{text "G2"} or vice versa, since both @{text "G1"} and @{text "G2"} are members of @{text c}. \label{cases2}*} from cM G1 G2 have "G1 ⊆ G2 ∨ G2 ⊆ G1" (is "?case1 ∨ ?case2") .. then show ?thesis proof assume ?case1 with xy' G2_rep have "(x, y) ∈ graph H2 h2" by blast hence "y = h2 x" .. also from xz' G2_rep have "(x, z) ∈ graph H2 h2" by (simp only:) hence "z = h2 x" .. finally show ?thesis . next assume ?case2 with xz' G1_rep have "(x, z) ∈ graph H1 h1" by blast hence "z = h1 x" .. also from xy' G1_rep have "(x, y) ∈ graph H1 h1" by (simp only:) hence "y = h1 x" .. finally show ?thesis .. qed qed text {* \medskip The limit function @{text h} is linear. Every element @{text x} in the domain of @{text h} is in the domain of a function @{text h'} in the chain of norm preserving extensions. Furthermore, @{text h} is an extension of @{text h'} so the function values of @{text x} are identical for @{text h'} and @{text h}. Finally, the function @{text h'} is linear by construction of @{text M}. *} lemma sup_lf: assumes M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chain M" and u: "graph H h = \<Union>c" shows "linearform H h" proof fix x y assume x: "x ∈ H" and y: "y ∈ H" with M cM u obtain H' h' where x': "x ∈ H'" and y': "y ∈ H'" and b: "graph H' h' ⊆ graph H h" and linearform: "linearform H' h'" and subspace: "H' \<unlhd> E" by (rule some_H'h'2 [elim_format]) blast show "h (x + y) = h x + h y" proof - from linearform x' y' have "h' (x + y) = h' x + h' y" by (rule linearform.add) also from b x' have "h' x = h x" .. also from b y' have "h' y = h y" .. also from subspace x' y' have "x + y ∈ H'" by (rule subspace.add_closed) with b have "h' (x + y) = h (x + y)" .. finally show ?thesis . qed next fix x a assume x: "x ∈ H" with M cM u obtain H' h' where x': "x ∈ H'" and b: "graph H' h' ⊆ graph H h" and linearform: "linearform H' h'" and subspace: "H' \<unlhd> E" by (rule some_H'h' [elim_format]) blast show "h (a · x) = a * h x" proof - from linearform x' have "h' (a · x) = a * h' x" by (rule linearform.mult) also from b x' have "h' x = h x" .. also from subspace x' have "a · x ∈ H'" by (rule subspace.mult_closed) with b have "h' (a · x) = h (a · x)" .. finally show ?thesis . qed qed text {* \medskip The limit of a non-empty chain of norm preserving extensions of @{text f} is an extension of @{text f}, since every element of the chain is an extension of @{text f} and the supremum is an extension for every element of the chain. *} lemma sup_ext: assumes graph: "graph H h = \<Union>c" and M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chain M" and ex: "∃x. x ∈ c" shows "graph F f ⊆ graph H h" proof - from ex obtain x where xc: "x ∈ c" .. from cM have "c ⊆ M" .. with xc have "x ∈ M" .. with M have "x ∈ norm_pres_extensions E p F f" by (simp only:) then obtain G g where "x = graph G g" and "graph F f ⊆ graph G g" .. then have "graph F f ⊆ x" by (simp only:) also from xc have "… ⊆ \<Union>c" by blast also from graph have "… = graph H h" .. finally show ?thesis . qed text {* \medskip The domain @{text H} of the limit function is a superspace of @{text F}, since @{text F} is a subset of @{text H}. The existence of the @{text 0} element in @{text F} and the closure properties follow from the fact that @{text F} is a vector space. *} lemma sup_supF: assumes graph: "graph H h = \<Union>c" and M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chain M" and ex: "∃x. x ∈ c" and FE: "F \<unlhd> E" shows "F \<unlhd> H" proof from FE show "F ≠ {}" by (rule subspace.non_empty) from graph M cM ex have "graph F f ⊆ graph H h" by (rule sup_ext) then show "F ⊆ H" .. fix x y assume "x ∈ F" and "y ∈ F" with FE show "x + y ∈ F" by (rule subspace.add_closed) next fix x a assume "x ∈ F" with FE show "a · x ∈ F" by (rule subspace.mult_closed) qed text {* \medskip The domain @{text H} of the limit function is a subspace of @{text E}. *} lemma sup_subE: assumes graph: "graph H h = \<Union>c" and M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chain M" and ex: "∃x. x ∈ c" and FE: "F \<unlhd> E" and E: "vectorspace E" shows "H \<unlhd> E" proof show "H ≠ {}" proof - from FE E have "0 ∈ F" by (rule subspace.zero) also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF) then have "F ⊆ H" .. finally show ?thesis by blast qed show "H ⊆ E" proof fix x assume "x ∈ H" with M cM graph obtain H' h' where x: "x ∈ H'" and H'E: "H' \<unlhd> E" by (rule some_H'h' [elim_format]) blast from H'E have "H' ⊆ E" .. with x show "x ∈ E" .. qed fix x y assume x: "x ∈ H" and y: "y ∈ H" show "x + y ∈ H" proof - from M cM graph x y obtain H' h' where x': "x ∈ H'" and y': "y ∈ H'" and H'E: "H' \<unlhd> E" and graphs: "graph H' h' ⊆ graph H h" by (rule some_H'h'2 [elim_format]) blast from H'E x' y' have "x + y ∈ H'" by (rule subspace.add_closed) also from graphs have "H' ⊆ H" .. finally show ?thesis . qed next fix x a assume x: "x ∈ H" show "a · x ∈ H" proof - from M cM graph x obtain H' h' where x': "x ∈ H'" and H'E: "H' \<unlhd> E" and graphs: "graph H' h' ⊆ graph H h" by (rule some_H'h' [elim_format]) blast from H'E x' have "a · x ∈ H'" by (rule subspace.mult_closed) also from graphs have "H' ⊆ H" .. finally show ?thesis . qed qed text {* \medskip The limit function is bounded by the norm @{text p} as well, since all elements in the chain are bounded by @{text p}. *} lemma sup_norm_pres: assumes graph: "graph H h = \<Union>c" and M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chain M" shows "∀x ∈ H. h x ≤ p x" proof fix x assume "x ∈ H" with M cM graph obtain H' h' where x': "x ∈ H'" and graphs: "graph H' h' ⊆ graph H h" and a: "∀x ∈ H'. h' x ≤ p x" by (rule some_H'h' [elim_format]) blast from graphs x' have [symmetric]: "h' x = h x" .. also from a x' have "h' x ≤ p x " .. finally show "h x ≤ p x" . qed text {* \medskip The following lemma is a property of linear forms on real vector spaces. It will be used for the lemma @{text abs_HahnBanach} (see page \pageref{abs-HahnBanach}). \label{abs-ineq-iff} For real vector spaces the following inequations are equivalent: \begin{center} \begin{tabular}{lll} @{text "∀x ∈ H. ¦h x¦ ≤ p x"} & and & @{text "∀x ∈ H. h x ≤ p x"} \\ \end{tabular} \end{center} *} lemma abs_ineq_iff: includes subspace H E + vectorspace E + seminorm E p + linearform H h shows "(∀x ∈ H. ¦h x¦ ≤ p x) = (∀x ∈ H. h x ≤ p x)" (is "?L = ?R") proof have H: "vectorspace H" .. { assume l: ?L show ?R proof fix x assume x: "x ∈ H" have "h x ≤ ¦h x¦" by arith also from l x have "… ≤ p x" .. finally show "h x ≤ p x" . qed next assume r: ?R show ?L proof fix x assume x: "x ∈ H" show "!!a b :: real. - a ≤ b ==> b ≤ a ==> ¦b¦ ≤ a" by arith have "linearform H h" . from this H x have "- h x = h (- x)" by (rule linearform.neg [symmetric]) also from H x have "- x ∈ H" by (rule vectorspace.neg_closed) with r have "h (- x) ≤ p (- x)" .. also have "… = p x" proof (rule seminorm.minus) from x show "x ∈ E" .. qed finally have "- h x ≤ p x" . then show "- p x ≤ h x" by simp from r x show "h x ≤ p x" .. qed } qed end
lemmas
[| c ∈ chain S; x ∈ c; y ∈ c |] ==> x ⊆ y ∨ y ⊆ x
lemmas
[| c ∈ chain S; x ∈ c; y ∈ c |] ==> x ⊆ y ∨ y ⊆ x
lemmas chainE2:
[| c ∈ chain S; c ⊆ S ==> PROP W |] ==> PROP W
lemmas chainE2:
[| c ∈ chain S; c ⊆ S ==> PROP W |] ==> PROP W
lemma some_H'h't:
[| M = norm_pres_extensions E p F f; c ∈ chain M; graph H h = Union c; x ∈ H |] ==> ∃H' h'. graph H' h' ∈ c ∧ (x, h x) ∈ graph H' h' ∧ linearform H' h' ∧ subspace H' E ∧ subspace F H' ∧ graph F f ⊆ graph H' h' ∧ (∀x∈H'. h' x ≤ p x)
lemma some_H'h':
[| M = norm_pres_extensions E p F f; c ∈ chain M; graph H h = Union c; x ∈ H |] ==> ∃H' h'. x ∈ H' ∧ graph H' h' ⊆ graph H h ∧ linearform H' h' ∧ subspace H' E ∧ subspace F H' ∧ graph F f ⊆ graph H' h' ∧ (∀x∈H'. h' x ≤ p x)
lemma some_H'h'2:
[| M = norm_pres_extensions E p F f; c ∈ chain M; graph H h = Union c; x ∈ H; y ∈ H |] ==> ∃H' h'. x ∈ H' ∧ y ∈ H' ∧ graph H' h' ⊆ graph H h ∧ linearform H' h' ∧ subspace H' E ∧ subspace F H' ∧ graph F f ⊆ graph H' h' ∧ (∀x∈H'. h' x ≤ p x)
lemma sup_definite:
[| M == norm_pres_extensions E p F f; c ∈ chain M; (x, y) ∈ Union c; (x, z) ∈ Union c |] ==> z = y
lemma sup_lf:
[| M = norm_pres_extensions E p F f; c ∈ chain M; graph H h = Union c |] ==> linearform H h
lemma sup_ext:
[| graph H h = Union c; M = norm_pres_extensions E p F f; c ∈ chain M; ∃x. x ∈ c |] ==> graph F f ⊆ graph H h
lemma sup_supF:
[| graph H h = Union c; M = norm_pres_extensions E p F f; c ∈ chain M; ∃x. x ∈ c; subspace F E |] ==> subspace F H
lemma sup_subE:
[| graph H h = Union c; M = norm_pres_extensions E p F f; c ∈ chain M; ∃x. x ∈ c; subspace F E; vectorspace E |] ==> subspace H E
lemma sup_norm_pres:
[| graph H h = Union c; M = norm_pres_extensions E p F f; c ∈ chain M |] ==> ∀x∈H. h x ≤ p x
lemma abs_ineq_iff:
[| subspace H E; vectorspace E; seminorm E p; linearform H h |] ==> (∀x∈H. ¦h x¦ ≤ p x) = (∀x∈H. h x ≤ p x)