(* Title: HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Author: Gertrud Bauer, TU Munich *) section ‹Extending non-maximal functions› theory Hahn_Banach_Ext_Lemmas imports Function_Norm begin text ‹ In this section the following context is presumed. Let ‹E› be a real vector space with a seminorm ‹q› on ‹E›. ‹F› is a subspace of ‹E› and ‹f› a linear function on ‹F›. We consider a subspace ‹H› of ‹E› that is a superspace of ‹F› and a linear form ‹h› on ‹H›. ‹H› is a not equal to ‹E› and ‹x⇩_{0}› is an element in ‹E - H›. ‹H› is extended to the direct sum ‹H' = H + lin x⇩_{0}›, so for any ‹x ∈ H'› the decomposition of ‹x = y + a ⋅ x› with ‹y ∈ H› is unique. ‹h'› is defined on ‹H'› by ‹h' x = h y + a ⋅ ξ› for a certain ‹ξ›. Subsequently we show some properties of this extension ‹h'› of ‹h›. ┉ This lemma will be used to show the existence of a linear extension of ‹f› (see page \pageref{ex-xi-use}). It is a consequence of the completeness of ‹ℝ›. To show \begin{center} \begin{tabular}{l} ‹∃ξ. ∀y ∈ F. a y ≤ ξ ∧ ξ ≤ b y› \end{tabular} \end{center} ⇤ it suffices to show that \begin{center} \begin{tabular}{l} ‹∀u ∈ F. ∀v ∈ F. a u ≤ b v› \end{tabular} \end{center} › lemma ex_xi: assumes "vectorspace F" assumes r: "⋀u v. u ∈ F ⟹ v ∈ F ⟹ a u ≤ b v" shows "∃xi::real. ∀y ∈ F. a y ≤ xi ∧ xi ≤ b y" proof - interpret vectorspace F by fact txt ‹From the completeness of the reals follows: The set ‹S = {a u. u ∈ F}› has a supremum, if it is non-empty and has an upper bound.› let ?S = "{a u | u. u ∈ F}" have "∃xi. lub ?S xi" proof (rule real_complete) have "a 0 ∈ ?S" by blast then show "∃X. X ∈ ?S" .. have "∀y ∈ ?S. y ≤ b 0" proof fix y assume y: "y ∈ ?S" then obtain u where u: "u ∈ F" and y: "y = a u" by blast from u and zero have "a u ≤ b 0" by (rule r) with y show "y ≤ b 0" by (simp only:) qed then show "∃u. ∀y ∈ ?S. y ≤ u" .. qed then obtain xi where xi: "lub ?S xi" .. { fix y assume "y ∈ F" then have "a y ∈ ?S" by blast with xi have "a y ≤ xi" by (rule lub.upper) } moreover { fix y assume y: "y ∈ F" from xi have "xi ≤ b y" proof (rule lub.least) fix au assume "au ∈ ?S" then obtain u where u: "u ∈ F" and au: "au = a u" by blast from u y have "a u ≤ b y" by (rule r) with au show "au ≤ b y" by (simp only:) qed } ultimately show "∃xi. ∀y ∈ F. a y ≤ xi ∧ xi ≤ b y" by blast qed text ‹ ┉ The function ‹h'› is defined as a ‹h' x = h y + a ⋅ ξ› where ‹x = y + a ⋅ ξ› is a linear extension of ‹h› to ‹H'›. › lemma h'_lf: assumes h'_def: "⋀x. h' x = (let (y, a) = SOME (y, a). x = y + a ⋅ x0 ∧ y ∈ H in h y + a * xi)" and H'_def: "H' = H + lin x0" and HE: "H ⊴ E" assumes "linearform H h" assumes x0: "x0 ∉ H" "x0 ∈ E" "x0 ≠ 0" assumes E: "vectorspace E" shows "linearform H' h'" proof - interpret linearform H h by fact interpret vectorspace E by fact show ?thesis proof note E = ‹vectorspace E› have H': "vectorspace H'" proof (unfold H'_def) from ‹x0 ∈ E› have "lin x0 ⊴ E" .. with HE show "vectorspace (H + lin x0)" using E .. qed { fix x1 x2 assume x1: "x1 ∈ H'" and x2: "x2 ∈ H'" show "h' (x1 + x2) = h' x1 + h' x2" proof - from H' x1 x2 have "x1 + x2 ∈ H'" by (rule vectorspace.add_closed) with x1 x2 obtain y y1 y2 a a1 a2 where x1x2: "x1 + x2 = y + a ⋅ x0" and y: "y ∈ H" and x1_rep: "x1 = y1 + a1 ⋅ x0" and y1: "y1 ∈ H" and x2_rep: "x2 = y2 + a2 ⋅ x0" and y2: "y2 ∈ H" unfolding H'_def sum_def lin_def by blast have ya: "y1 + y2 = y ∧ a1 + a2 = a" using E HE _ y x0 proof (rule decomp_H') text_raw ‹\label{decomp-H-use}› from HE y1 y2 show "y1 + y2 ∈ H" by (rule subspace.add_closed) from x0 and HE y y1 y2 have "x0 ∈ E" "y ∈ E" "y1 ∈ E" "y2 ∈ E" by auto with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) ⋅ x0 = x1 + x2" by (simp add: add_ac add_mult_distrib2) also note x1x2 finally show "(y1 + y2) + (a1 + a2) ⋅ x0 = y + a ⋅ x0" . qed from h'_def x1x2 E HE y x0 have "h' (x1 + x2) = h y + a * xi" by (rule h'_definite) also have "… = h (y1 + y2) + (a1 + a2) * xi" by (simp only: ya) also from y1 y2 have "h (y1 + y2) = h y1 + h y2" by simp also have "… + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" by (simp add: distrib_right) also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" by (rule h'_definite [symmetric]) also from h'_def x2_rep E HE y2 x0 have "h y2 + a2 * xi = h' x2" by (rule h'_definite [symmetric]) finally show ?thesis . qed next fix x1 c assume x1: "x1 ∈ H'" show "h' (c ⋅ x1) = c * (h' x1)" proof - from H' x1 have ax1: "c ⋅ x1 ∈ H'" by (rule vectorspace.mult_closed) with x1 obtain y a y1 a1 where cx1_rep: "c ⋅ x1 = y + a ⋅ x0" and y: "y ∈ H" and x1_rep: "x1 = y1 + a1 ⋅ x0" and y1: "y1 ∈ H" unfolding H'_def sum_def lin_def by blast have ya: "c ⋅ y1 = y ∧ c * a1 = a" using E HE _ y x0 proof (rule decomp_H') from HE y1 show "c ⋅ y1 ∈ H" by (rule subspace.mult_closed) from x0 and HE y y1 have "x0 ∈ E" "y ∈ E" "y1 ∈ E" by auto with x1_rep have "c ⋅ y1 + (c * a1) ⋅ x0 = c ⋅ x1" by (simp add: mult_assoc add_mult_distrib1) also note cx1_rep finally show "c ⋅ y1 + (c * a1) ⋅ x0 = y + a ⋅ x0" . qed from h'_def cx1_rep E HE y x0 have "h' (c ⋅ x1) = h y + a * xi" by (rule h'_definite) also have "… = h (c ⋅ y1) + (c * a1) * xi" by (simp only: ya) also from y1 have "h (c ⋅ y1) = c * h y1" by simp also have "… + (c * a1) * xi = c * (h y1 + a1 * xi)" by (simp only: distrib_left) also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" by (rule h'_definite [symmetric]) finally show ?thesis . qed } qed qed text ‹ ┉ The linear extension ‹h'› of ‹h› is bounded by the seminorm ‹p›. › lemma h'_norm_pres: assumes h'_def: "⋀x. h' x = (let (y, a) = SOME (y, a). x = y + a ⋅ x0 ∧ y ∈ H in h y + a * xi)" and H'_def: "H' = H + lin x0" and x0: "x0 ∉ H" "x0 ∈ E" "x0 ≠ 0" assumes E: "vectorspace E" and HE: "subspace H E" and "seminorm E p" and "linearform H h" assumes a: "∀y ∈ H. h y ≤ p y" and a': "∀y ∈ H. - p (y + x0) - h y ≤ xi ∧ xi ≤ p (y + x0) - h y" shows "∀x ∈ H'. h' x ≤ p x" proof - interpret vectorspace E by fact interpret subspace H E by fact interpret seminorm E p by fact interpret linearform H h by fact show ?thesis proof fix x assume x': "x ∈ H'" show "h' x ≤ p x" proof - from a' have a1: "∀ya ∈ H. - p (ya + x0) - h ya ≤ xi" and a2: "∀ya ∈ H. xi ≤ p (ya + x0) - h ya" by auto from x' obtain y a where x_rep: "x = y + a ⋅ x0" and y: "y ∈ H" unfolding H'_def sum_def lin_def by blast from y have y': "y ∈ E" .. from y have ay: "inverse a ⋅ y ∈ H" by simp from h'_def x_rep E HE y x0 have "h' x = h y + a * xi" by (rule h'_definite) also have "… ≤ p (y + a ⋅ x0)" proof (rule linorder_cases) assume z: "a = 0" then have "h y + a * xi = h y" by simp also from a y have "… ≤ p y" .. also from x0 y' z have "p y = p (y + a ⋅ x0)" by simp finally show ?thesis . next txt ‹In the case ‹a < 0›, we use ‹a⇩_{1}› with ‹ya› taken as ‹y / a›:› assume lz: "a < 0" then have nz: "a ≠ 0" by simp from a1 ay have "- p (inverse a ⋅ y + x0) - h (inverse a ⋅ y) ≤ xi" .. with lz have "a * xi ≤ a * (- p (inverse a ⋅ y + x0) - h (inverse a ⋅ y))" by (simp add: mult_left_mono_neg order_less_imp_le) also have "… = - a * (p (inverse a ⋅ y + x0)) - a * (h (inverse a ⋅ y))" by (simp add: right_diff_distrib) also from lz x0 y' have "- a * (p (inverse a ⋅ y + x0)) = p (a ⋅ (inverse a ⋅ y + x0))" by (simp add: abs_homogenous) also from nz x0 y' have "… = p (y + a ⋅ x0)" by (simp add: add_mult_distrib1 mult_assoc [symmetric]) also from nz y have "a * (h (inverse a ⋅ y)) = h y" by simp finally have "a * xi ≤ p (y + a ⋅ x0) - h y" . then show ?thesis by simp next txt ‹In the case ‹a > 0›, we use ‹a⇩_{2}› with ‹ya› taken as ‹y / a›:› assume gz: "0 < a" then have nz: "a ≠ 0" by simp from a2 ay have "xi ≤ p (inverse a ⋅ y + x0) - h (inverse a ⋅ y)" .. with gz have "a * xi ≤ a * (p (inverse a ⋅ y + x0) - h (inverse a ⋅ y))" by simp also have "… = a * p (inverse a ⋅ y + x0) - a * h (inverse a ⋅ y)" by (simp add: right_diff_distrib) also from gz x0 y' have "a * p (inverse a ⋅ y + x0) = p (a ⋅ (inverse a ⋅ y + x0))" by (simp add: abs_homogenous) also from nz x0 y' have "… = p (y + a ⋅ x0)" by (simp add: add_mult_distrib1 mult_assoc [symmetric]) also from nz y have "a * h (inverse a ⋅ y) = h y" by simp finally have "a * xi ≤ p (y + a ⋅ x0) - h y" . then show ?thesis by simp qed also from x_rep have "… = p x" by (simp only:) finally show ?thesis . qed qed qed end