(* Title: HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Author: Gertrud Bauer, TU Munich *) section ‹The supremum wrt.\ the function order› theory Hahn_Banach_Sup_Lemmas imports Function_Norm Zorn_Lemma 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 ‹E› be a real vector space with a seminorm ‹p› on ‹E›. ‹F› is a subspace of ‹E› and ‹f› a linear form on ‹F›. We consider a chain ‹c› of norm-preserving extensions of ‹f›, such that ‹⋃c = graph H h›. We will show some properties about the limit function ‹h›, i.e.\ the supremum of the chain ‹c›. ┉ Let ‹c› be a chain of norm-preserving extensions of the function ‹f› and let ‹graph H h› be the supremum of ‹c›. Every element in ‹H› is member of one of the elements of the chain. › lemmas [dest?] = chainsD lemmas chainsE2 [elim?] = chainsD2 [elim_format] lemma some_H'h't: assumes M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chains M" and u: "graph H h = ⋃c" and x: "x ∈ H" shows "∃H' h'. graph H' h' ∈ c ∧ (x, h x) ∈ graph H' h' ∧ linearform H' h' ∧ H' ⊴ E ∧ F ⊴ 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 "… = ⋃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' ⊴ E" "F ⊴ 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 ‹ ┉ Let ‹c› be a chain of norm-preserving extensions of the function ‹f› and let ‹graph H h› be the supremum of ‹c›. Every element in the domain ‹H› of the supremum function is member of the domain ‹H'› of some function ‹h'›, such that ‹h› extends ‹h'›. › lemma some_H'h': assumes M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chains M" and u: "graph H h = ⋃c" and x: "x ∈ H" shows "∃H' h'. x ∈ H' ∧ graph H' h' ⊆ graph H h ∧ linearform H' h' ∧ H' ⊴ E ∧ F ⊴ 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' ⊴ E" "F ⊴ 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 blast ultimately show ?thesis using * by blast qed text ‹ ┉ Any two elements ‹x› and ‹y› in the domain ‹H› of the supremum function ‹h› are both in the domain ‹H'› of some function ‹h'›, such that ‹h› extends ‹h'›. › lemma some_H'h'2: assumes M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chains M" and u: "graph H h = ⋃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' ⊴ E ∧ F ⊴ H' ∧ graph F f ⊆ graph H' h' ∧ (∀x ∈ H'. h' x ≤ p x)" proof - txt ‹‹y› is in the domain ‹H''› of some function ‹h''›, such that ‹h› extends ‹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' ⊴ E" "F ⊴ H'" "graph F f ⊆ graph H' h'" "∀x ∈ H'. h' x ≤ p x" by (rule some_H'h't [elim_format]) blast txt ‹‹x› is in the domain ‹H'› of some function ‹h'›, such that ‹h› extends ‹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'' ⊴ E" "F ⊴ 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 ‹h'› and ‹h''› are elements of the chain, ‹h''› is an extension of ‹h'› or vice versa. Thus both ‹x› and ‹y› are contained in the greater one. \label{cases1}› from cM c'' c' consider "graph H'' h'' ⊆ graph H' h'" | "graph H' h' ⊆ graph H'' h''" by (blast dest: chainsD) then show ?thesis proof cases case 1 have "(x, h x) ∈ graph H'' h''" by fact also have "… ⊆ graph H' h'" by fact 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 blast ultimately show ?thesis using * by blast next case 2 from x_hx have "x ∈ H''" .. moreover have "y ∈ H''" proof - have "(y, h y) ∈ graph H' h'" by (rule y_hy) also have "… ⊆ graph H'' h''" by fact finally have "(y, h y) ∈ graph H'' h''" . then show ?thesis .. qed moreover from u c'' have "graph H'' h'' ⊆ graph H h" by blast ultimately show ?thesis using ** by blast qed qed text ‹ ┉ The relation induced by the graph of the supremum of a chain ‹c› is definite, i.e.\ it is the graph of a function. › lemma sup_definite: assumes M_def: "M = norm_pres_extensions E p F f" and cM: "c ∈ chains M" and xy: "(x, y) ∈ ⋃c" and xz: "(x, z) ∈ ⋃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" unfolding M_def by blast from G2 c have "G2 ∈ M" .. then obtain H2 h2 where G2_rep: "G2 = graph H2 h2" unfolding M_def by blast txt ‹‹G⇩_{1}› is contained in ‹G⇩_{2}› or vice versa, since both ‹G⇩_{1}› and ‹G⇩_{2}› are members of ‹c›. \label{cases2}› from cM G1 G2 consider "G1 ⊆ G2" | "G2 ⊆ G1" by (blast dest: chainsD) then show ?thesis proof cases case 1 with xy' G2_rep have "(x, y) ∈ graph H2 h2" by blast then have "y = h2 x" .. also from xz' G2_rep have "(x, z) ∈ graph H2 h2" by (simp only:) then have "z = h2 x" .. finally show ?thesis . next case 2 with xz' G1_rep have "(x, z) ∈ graph H1 h1" by blast then have "z = h1 x" .. also from xy' G1_rep have "(x, y) ∈ graph H1 h1" by (simp only:) then have "y = h1 x" .. finally show ?thesis .. qed qed text ‹ ┉ The limit function ‹h› is linear. Every element ‹x› in the domain of ‹h› is in the domain of a function ‹h'› in the chain of norm preserving extensions. Furthermore, ‹h› is an extension of ‹h'› so the function values of ‹x› are identical for ‹h'› and ‹h›. Finally, the function ‹h'› is linear by construction of ‹M›. › lemma sup_lf: assumes M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chains M" and u: "graph H h = ⋃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' ⊴ 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' ⊴ 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 ‹ ┉ The limit of a non-empty chain of norm preserving extensions of ‹f› is an extension of ‹f›, since every element of the chain is an extension of ‹f› and the supremum is an extension for every element of the chain. › lemma sup_ext: assumes graph: "graph H h = ⋃c" and M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chains 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 "… ⊆ ⋃c" by blast also from graph have "… = graph H h" .. finally show ?thesis . qed text ‹ ┉ The domain ‹H› of the limit function is a superspace of ‹F›, since ‹F› is a subset of ‹H›. The existence of the ‹0› element in ‹F› and the closure properties follow from the fact that ‹F› is a vector space. › lemma sup_supF: assumes graph: "graph H h = ⋃c" and M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chains M" and ex: "∃x. x ∈ c" and FE: "F ⊴ E" shows "F ⊴ 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 ‹ ┉ The domain ‹H› of the limit function is a subspace of ‹E›. › lemma sup_subE: assumes graph: "graph H h = ⋃c" and M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chains M" and ex: "∃x. x ∈ c" and FE: "F ⊴ E" and E: "vectorspace E" shows "H ⊴ E" proof show "H ≠ {}" proof - from FE E have "0 ∈ F" by (rule subspace.zero) also from graph M cM ex FE have "F ⊴ 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' where x: "x ∈ H'" and H'E: "H' ⊴ 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' ⊴ 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' ⊴ 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 ‹ ┉ The limit function is bounded by the norm ‹p› as well, since all elements in the chain are bounded by ‹p›. › lemma sup_norm_pres: assumes graph: "graph H h = ⋃c" and M: "M = norm_pres_extensions E p F f" and cM: "c ∈ chains 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 ‹ ┉ The following lemma is a property of linear forms on real vector spaces. It will be used for the lemma ‹abs_Hahn_Banach› (see page \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces the following inequality are equivalent: \begin{center} \begin{tabular}{lll} ‹∀x ∈ H. ¦h x¦ ≤ p x› & and & ‹∀x ∈ H. h x ≤ p x› \\ \end{tabular} \end{center} › lemma abs_ineq_iff: assumes "subspace H E" and "vectorspace E" and "seminorm E p" and "linearform H h" shows "(∀x ∈ H. ¦h x¦ ≤ p x) = (∀x ∈ H. h x ≤ p x)" (is "?L = ?R") proof interpret subspace H E by fact interpret vectorspace E by fact interpret seminorm E p by fact interpret linearform H h by fact have H: "vectorspace H" using ‹vectorspace E› .. { 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 "¦b¦ ≤ a" when "- a ≤ b" "b ≤ a" for a b :: real using that by arith from ‹linearform H h› and 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" using ‹seminorm E p› ‹vectorspace E› 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