1(*  Title:      HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
2    Author:     Gertrud Bauer, TU Munich
3*)
4
5section \<open>Extending non-maximal functions\<close>
6
7theory Hahn_Banach_Ext_Lemmas
8imports Function_Norm
9begin
10
11text \<open>
12  In this section the following context is presumed. Let \<open>E\<close> be a real vector
13  space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> a linear
14  function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a superspace of
15  \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> and \<open>x\<^sub>0\<close> is an
16  element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' = H + lin x\<^sub>0\<close>, so
17  for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is
18  unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>.
19
20  Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>.
21
22  \<^medskip>
23  This lemma will be used to show the existence of a linear extension of \<open>f\<close>
24  (see page \pageref{ex-xi-use}). It is a consequence of the completeness of
25  \<open>\<real>\<close>. To show
26  \begin{center}
27  \begin{tabular}{l}
28  \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close>
29  \end{tabular}
30  \end{center}
31  \<^noindent> it suffices to show that
32  \begin{center}
33  \begin{tabular}{l}
34  \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close>
35  \end{tabular}
36  \end{center}
37\<close>
38
39lemma ex_xi:
40  assumes "vectorspace F"
41  assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
42  shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
43proof -
44  interpret vectorspace F by fact
45  txt \<open>From the completeness of the reals follows:
46    The set \<open>S = {a u. u \<in> F}\<close> has a supremum, if it is
47    non-empty and has an upper bound.\<close>
48
49  let ?S = "{a u | u. u \<in> F}"
50  have "\<exists>xi. lub ?S xi"
51  proof (rule real_complete)
52    have "a 0 \<in> ?S" by blast
53    then show "\<exists>X. X \<in> ?S" ..
54    have "\<forall>y \<in> ?S. y \<le> b 0"
55    proof
56      fix y assume y: "y \<in> ?S"
57      then obtain u where u: "u \<in> F" and y: "y = a u" by blast
58      from u and zero have "a u \<le> b 0" by (rule r)
59      with y show "y \<le> b 0" by (simp only:)
60    qed
61    then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..
62  qed
63  then obtain xi where xi: "lub ?S xi" ..
64  {
65    fix y assume "y \<in> F"
66    then have "a y \<in> ?S" by blast
67    with xi have "a y \<le> xi" by (rule lub.upper)
68  }
69  moreover {
70    fix y assume y: "y \<in> F"
71    from xi have "xi \<le> b y"
72    proof (rule lub.least)
73      fix au assume "au \<in> ?S"
74      then obtain u where u: "u \<in> F" and au: "au = a u" by blast
75      from u y have "a u \<le> b y" by (rule r)
76      with au show "au \<le> b y" by (simp only:)
77    qed
78  }
79  ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
80qed
81
82text \<open>
83  \<^medskip>
84  The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close>
85  is a linear extension of \<open>h\<close> to \<open>H'\<close>.
86\<close>
87
88lemma h'_lf:
89  assumes h'_def: "\<And>x. h' x = (let (y, a) =
90      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi)"
91    and H'_def: "H' = H + lin x0"
92    and HE: "H \<unlhd> E"
93  assumes "linearform H h"
94  assumes x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
95  assumes E: "vectorspace E"
96  shows "linearform H' h'"
97proof -
98  interpret linearform H h by fact
99  interpret vectorspace E by fact
100  show ?thesis
101  proof
102    note E = \<open>vectorspace E\<close>
103    have H': "vectorspace H'"
104    proof (unfold H'_def)
105      from \<open>x0 \<in> E\<close>
106      have "lin x0 \<unlhd> E" ..
107      with HE show "vectorspace (H + lin x0)" using E ..
108    qed
109    {
110      fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
111      show "h' (x1 + x2) = h' x1 + h' x2"
112      proof -
113        from H' x1 x2 have "x1 + x2 \<in> H'"
114          by (rule vectorspace.add_closed)
115        with x1 x2 obtain y y1 y2 a a1 a2 where
116          x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
117          and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
118          and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
119          unfolding H'_def sum_def lin_def by blast
120        
121        have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
122        proof (rule decomp_H') text_raw \<open>\label{decomp-H-use}\<close>
123          from HE y1 y2 show "y1 + y2 \<in> H"
124            by (rule subspace.add_closed)
125          from x0 and HE y y1 y2
126          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E"  "y2 \<in> E" by auto
127          with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
128            by (simp add: add_ac add_mult_distrib2)
129          also note x1x2
130          finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
131        qed
132        
133        from h'_def x1x2 E HE y x0
134        have "h' (x1 + x2) = h y + a * xi"
135          by (rule h'_definite)
136        also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"
137          by (simp only: ya)
138        also from y1 y2 have "h (y1 + y2) = h y1 + h y2"
139          by simp
140        also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
141          by (simp add: distrib_right)
142        also from h'_def x1_rep E HE y1 x0
143        have "h y1 + a1 * xi = h' x1"
144          by (rule h'_definite [symmetric])
145        also from h'_def x2_rep E HE y2 x0
146        have "h y2 + a2 * xi = h' x2"
147          by (rule h'_definite [symmetric])
148        finally show ?thesis .
149      qed
150    next
151      fix x1 c assume x1: "x1 \<in> H'"
152      show "h' (c \<cdot> x1) = c * (h' x1)"
153      proof -
154        from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
155          by (rule vectorspace.mult_closed)
156        with x1 obtain y a y1 a1 where
157            cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
158          and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
159          unfolding H'_def sum_def lin_def by blast
160        
161        have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0
162        proof (rule decomp_H')
163          from HE y1 show "c \<cdot> y1 \<in> H"
164            by (rule subspace.mult_closed)
165          from x0 and HE y y1
166          have "x0 \<in> E"  "y \<in> E"  "y1 \<in> E" by auto
167          with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
168            by (simp add: mult_assoc add_mult_distrib1)
169          also note cx1_rep
170          finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
171        qed
172        
173        from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
174          by (rule h'_definite)
175        also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
176          by (simp only: ya)
177        also from y1 have "h (c \<cdot> y1) = c * h y1"
178          by simp
179        also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
180          by (simp only: distrib_left)
181        also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"
182          by (rule h'_definite [symmetric])
183        finally show ?thesis .
184      qed
185    }
186  qed
187qed
188
189text \<open>
190  \<^medskip>
191  The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>.
192\<close>
193
194lemma h'_norm_pres:
195  assumes h'_def: "\<And>x. h' x = (let (y, a) =
196      SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi)"
197    and H'_def: "H' = H + lin x0"
198    and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
199  assumes E: "vectorspace E" and HE: "subspace H E"
200    and "seminorm E p" and "linearform H h"
201  assumes a: "\<forall>y \<in> H. h y \<le> p y"
202    and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
203  shows "\<forall>x \<in> H'. h' x \<le> p x"
204proof -
205  interpret vectorspace E by fact
206  interpret subspace H E by fact
207  interpret seminorm E p by fact
208  interpret linearform H h by fact
209  show ?thesis
210  proof
211    fix x assume x': "x \<in> H'"
212    show "h' x \<le> p x"
213    proof -
214      from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
215        and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
216      from x' obtain y a where
217          x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
218        unfolding H'_def sum_def lin_def by blast
219      from y have y': "y \<in> E" ..
220      from y have ay: "inverse a \<cdot> y \<in> H" by simp
221      
222      from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"
223        by (rule h'_definite)
224      also have "\<dots> \<le> p (y + a \<cdot> x0)"
225      proof (rule linorder_cases)
226        assume z: "a = 0"
227        then have "h y + a * xi = h y" by simp
228        also from a y have "\<dots> \<le> p y" ..
229        also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
230        finally show ?thesis .
231      next
232        txt \<open>In the case \<open>a < 0\<close>, we use \<open>a\<^sub>1\<close>
233          with \<open>ya\<close> taken as \<open>y / a\<close>:\<close>
234        assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp
235        from a1 ay
236        have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
237        with lz have "a * xi \<le>
238          a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
239          by (simp add: mult_left_mono_neg order_less_imp_le)
240        
241        also have "\<dots> =
242          - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
243          by (simp add: right_diff_distrib)
244        also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
245          p (a \<cdot> (inverse a \<cdot> y + x0))"
246          by (simp add: abs_homogenous)
247        also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
248          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
249        also from nz y have "a * (h (inverse a \<cdot> y)) =  h y"
250          by simp
251        finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
252        then show ?thesis by simp
253      next
254        txt \<open>In the case \<open>a > 0\<close>, we use \<open>a\<^sub>2\<close>
255          with \<open>ya\<close> taken as \<open>y / a\<close>:\<close>
256        assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
257        from a2 ay
258        have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
259        with gz have "a * xi \<le>
260          a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
261          by simp
262        also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
263          by (simp add: right_diff_distrib)
264        also from gz x0 y'
265        have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
266          by (simp add: abs_homogenous)
267        also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
268          by (simp add: add_mult_distrib1 mult_assoc [symmetric])
269        also from nz y have "a * h (inverse a \<cdot> y) = h y"
270          by simp
271        finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
272        then show ?thesis by simp
273      qed
274      also from x_rep have "\<dots> = p x" by (simp only:)
275      finally show ?thesis .
276    qed
277  qed
278qed
279
280end
281