7917

1 
(* Title: HOL/Real/HahnBanach/HahnBanachExtLemmas.thy


2 
ID: $Id$


3 
Author: Gertrud Bauer, TU Munich


4 
*)


5 

10007

6 
header {* Extending nonmaximal functions *}

7917

7 

27612

8 
theory HahnBanachExtLemmas


9 
imports FunctionNorm


10 
begin

7917

11 

10687

12 
text {*


13 
In this section the following context is presumed. Let @{text E} be


14 
a real vector space with a seminorm @{text q} on @{text E}. @{text


15 
F} is a subspace of @{text E} and @{text f} a linear function on


16 
@{text F}. We consider a subspace @{text H} of @{text E} that is a


17 
superspace of @{text F} and a linear form @{text h} on @{text


18 
H}. @{text H} is a not equal to @{text E} and @{text "x\<^sub>0"} is


19 
an element in @{text "E  H"}. @{text H} is extended to the direct


20 
sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"}


21 
the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is

13515

22 
unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +


23 
a \<cdot> \<xi>"} for a certain @{text \<xi>}.

7917

24 

10687

25 
Subsequently we show some properties of this extension @{text h'} of


26 
@{text h}.

7917

27 

13515

28 
\medskip This lemma will be used to show the existence of a linear


29 
extension of @{text f} (see page \pageref{exxiuse}). It is a


30 
consequence of the completeness of @{text \<real>}. To show

10687

31 
\begin{center}


32 
\begin{tabular}{l}


33 
@{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"}


34 
\end{tabular}


35 
\end{center}


36 
\noindent it suffices to show that


37 
\begin{center}


38 
\begin{tabular}{l}


39 
@{text "\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v"}


40 
\end{tabular}


41 
\end{center}


42 
*}

7917

43 

10687

44 
lemma ex_xi:

27611

45 
assumes "vectorspace F"

13515

46 
assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"


47 
shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"

10007

48 
proof 

27611

49 
interpret vectorspace [F] by fact

7917

50 
txt {* From the completeness of the reals follows:

13515

51 
The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is


52 
nonempty and has an upper bound. *}

7917

53 

13515

54 
let ?S = "{a u  u. u \<in> F}"


55 
have "\<exists>xi. lub ?S xi"


56 
proof (rule real_complete)


57 
have "a 0 \<in> ?S" by blast


58 
then show "\<exists>X. X \<in> ?S" ..


59 
have "\<forall>y \<in> ?S. y \<le> b 0"


60 
proof


61 
fix y assume y: "y \<in> ?S"


62 
then obtain u where u: "u \<in> F" and y: "y = a u" by blast


63 
from u and zero have "a u \<le> b 0" by (rule r)


64 
with y show "y \<le> b 0" by (simp only:)

10007

65 
qed

13515

66 
then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..

10007

67 
qed

13515

68 
then obtain xi where xi: "lub ?S xi" ..


69 
{


70 
fix y assume "y \<in> F"


71 
then have "a y \<in> ?S" by blast


72 
with xi have "a y \<le> xi" by (rule lub.upper)


73 
} moreover {


74 
fix y assume y: "y \<in> F"


75 
from xi have "xi \<le> b y"


76 
proof (rule lub.least)


77 
fix au assume "au \<in> ?S"


78 
then obtain u where u: "u \<in> F" and au: "au = a u" by blast


79 
from u y have "a u \<le> b y" by (rule r)


80 
with au show "au \<le> b y" by (simp only:)

10007

81 
qed

13515

82 
} ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast

10007

83 
qed

7917

84 

10687

85 
text {*

13515

86 
\medskip The function @{text h'} is defined as a @{text "h' x = h y


87 
+ a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of


88 
@{text h} to @{text H'}.


89 
*}

7917

90 

10687

91 
lemma h'_lf:

13515

92 
assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =


93 
SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"

10687

94 
and H'_def: "H' \<equiv> H + lin x0"

13515

95 
and HE: "H \<unlhd> E"

27611

96 
assumes "linearform H h"

13515

97 
assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"

27611

98 
assumes E: "vectorspace E"

13515

99 
shows "linearform H' h'"

27611

100 
proof 


101 
interpret linearform [H h] by fact


102 
interpret vectorspace [E] by fact

27612

103 
show ?thesis


104 
proof

27611

105 
note E = `vectorspace E`


106 
have H': "vectorspace H'"


107 
proof (unfold H'_def)


108 
from `x0 \<in> E`


109 
have "lin x0 \<unlhd> E" ..


110 
with HE show "vectorspace (H + lin x0)" using E ..


111 
qed


112 
{


113 
fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"


114 
show "h' (x1 + x2) = h' x1 + h' x2"


115 
proof 


116 
from H' x1 x2 have "x1 + x2 \<in> H'"


117 
by (rule vectorspace.add_closed)


118 
with x1 x2 obtain y y1 y2 a a1 a2 where


119 
x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"

13515

120 
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"


121 
and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"

27612

122 
unfolding H'_def sum_def lin_def by blast

27611

123 


124 
have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0


125 
proof (rule decomp_H') txt_raw {* \label{decompHuse} *}


126 
from HE y1 y2 show "y1 + y2 \<in> H"


127 
by (rule subspace.add_closed)


128 
from x0 and HE y y1 y2


129 
have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto


130 
with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"


131 
by (simp add: add_ac add_mult_distrib2)


132 
also note x1x2


133 
finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .


134 
qed


135 


136 
from h'_def x1x2 E HE y x0


137 
have "h' (x1 + x2) = h y + a * xi"


138 
by (rule h'_definite)


139 
also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi"


140 
by (simp only: ya)


141 
also from y1 y2 have "h (y1 + y2) = h y1 + h y2"


142 
by simp


143 
also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"


144 
by (simp add: left_distrib)


145 
also from h'_def x1_rep E HE y1 x0


146 
have "h y1 + a1 * xi = h' x1"


147 
by (rule h'_definite [symmetric])


148 
also from h'_def x2_rep E HE y2 x0


149 
have "h y2 + a2 * xi = h' x2"


150 
by (rule h'_definite [symmetric])


151 
finally show ?thesis .

10007

152 
qed

27611

153 
next


154 
fix x1 c assume x1: "x1 \<in> H'"


155 
show "h' (c \<cdot> x1) = c * (h' x1)"


156 
proof 


157 
from H' x1 have ax1: "c \<cdot> x1 \<in> H'"


158 
by (rule vectorspace.mult_closed)


159 
with x1 obtain y a y1 a1 where

27612

160 
cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"

13515

161 
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"

27612

162 
unfolding H'_def sum_def lin_def by blast

27611

163 


164 
have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0


165 
proof (rule decomp_H')


166 
from HE y1 show "c \<cdot> y1 \<in> H"


167 
by (rule subspace.mult_closed)


168 
from x0 and HE y y1


169 
have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto


170 
with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"


171 
by (simp add: mult_assoc add_mult_distrib1)


172 
also note cx1_rep


173 
finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .


174 
qed


175 


176 
from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"


177 
by (rule h'_definite)


178 
also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"


179 
by (simp only: ya)


180 
also from y1 have "h (c \<cdot> y1) = c * h y1"


181 
by simp


182 
also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"


183 
by (simp only: right_distrib)


184 
also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"


185 
by (rule h'_definite [symmetric])


186 
finally show ?thesis .

10007

187 
qed

27611

188 
}


189 
qed

10007

190 
qed

7917

191 

10687

192 
text {* \medskip The linear extension @{text h'} of @{text h}

13515

193 
is bounded by the seminorm @{text p}. *}

7917

194 

9374

195 
lemma h'_norm_pres:

13515

196 
assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =


197 
SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"

10687

198 
and H'_def: "H' \<equiv> H + lin x0"

13515

199 
and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"

27611

200 
assumes E: "vectorspace E" and HE: "subspace H E"


201 
and "seminorm E p" and "linearform H h"

13515

202 
assumes a: "\<forall>y \<in> H. h y \<le> p y"


203 
and a': "\<forall>y \<in> H.  p (y + x0)  h y \<le> xi \<and> xi \<le> p (y + x0)  h y"


204 
shows "\<forall>x \<in> H'. h' x \<le> p x"

27611

205 
proof 


206 
interpret vectorspace [E] by fact


207 
interpret subspace [H E] by fact


208 
interpret seminorm [E p] by fact


209 
interpret linearform [H h] by fact

27612

210 
show ?thesis


211 
proof

27611

212 
fix x assume x': "x \<in> H'"


213 
show "h' x \<le> p x"


214 
proof 


215 
from a' have a1: "\<forall>ya \<in> H.  p (ya + x0)  h ya \<le> xi"


216 
and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0)  h ya" by auto


217 
from x' obtain y a where

27612

218 
x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"


219 
unfolding H'_def sum_def lin_def by blast

27611

220 
from y have y': "y \<in> E" ..


221 
from y have ay: "inverse a \<cdot> y \<in> H" by simp


222 


223 
from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"


224 
by (rule h'_definite)


225 
also have "\<dots> \<le> p (y + a \<cdot> x0)"


226 
proof (rule linorder_cases)


227 
assume z: "a = 0"


228 
then have "h y + a * xi = h y" by simp


229 
also from a y have "\<dots> \<le> p y" ..


230 
also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp


231 
finally show ?thesis .


232 
next


233 
txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}


234 
with @{text ya} taken as @{text "y / a"}: *}

27612

235 
assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp

27611

236 
from a1 ay


237 
have " p (inverse a \<cdot> y + x0)  h (inverse a \<cdot> y) \<le> xi" ..


238 
with lz have "a * xi \<le>

13515

239 
a * ( p (inverse a \<cdot> y + x0)  h (inverse a \<cdot> y))"

27611

240 
by (simp add: mult_left_mono_neg order_less_imp_le)


241 


242 
also have "\<dots> =

13515

243 
 a * (p (inverse a \<cdot> y + x0))  a * (h (inverse a \<cdot> y))"

27611

244 
by (simp add: right_diff_distrib)


245 
also from lz x0 y' have " a * (p (inverse a \<cdot> y + x0)) =

13515

246 
p (a \<cdot> (inverse a \<cdot> y + x0))"

27611

247 
by (simp add: abs_homogenous)


248 
also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"


249 
by (simp add: add_mult_distrib1 mult_assoc [symmetric])


250 
also from nz y have "a * (h (inverse a \<cdot> y)) = h y"


251 
by simp


252 
finally have "a * xi \<le> p (y + a \<cdot> x0)  h y" .


253 
then show ?thesis by simp


254 
next


255 
txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}


256 
with @{text ya} taken as @{text "y / a"}: *}

27612

257 
assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp

27611

258 
from a2 ay


259 
have "xi \<le> p (inverse a \<cdot> y + x0)  h (inverse a \<cdot> y)" ..


260 
with gz have "a * xi \<le>

13515

261 
a * (p (inverse a \<cdot> y + x0)  h (inverse a \<cdot> y))"

27611

262 
by simp

27612

263 
also have "\<dots> = a * p (inverse a \<cdot> y + x0)  a * h (inverse a \<cdot> y)"

27611

264 
by (simp add: right_diff_distrib)


265 
also from gz x0 y'


266 
have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"


267 
by (simp add: abs_homogenous)


268 
also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"


269 
by (simp add: add_mult_distrib1 mult_assoc [symmetric])


270 
also from nz y have "a * h (inverse a \<cdot> y) = h y"


271 
by simp


272 
finally have "a * xi \<le> p (y + a \<cdot> x0)  h y" .


273 
then show ?thesis by simp


274 
qed


275 
also from x_rep have "\<dots> = p x" by (simp only:)


276 
finally show ?thesis .

10007

277 
qed


278 
qed

13515

279 
qed

7917

280 

10007

281 
end
