author  wenzelm 
Mon, 25 Apr 2016 16:09:26 +0200  
changeset 63040  eb4ddd18d635 
parent 61879  e4f9d8f094fe 
permissions  rwrr 
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

1 
(* Title: HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy 
7917  2 
Author: Gertrud Bauer, TU Munich 
3 
*) 

4 

58889  5 
section \<open>Extending nonmaximal functions\<close> 
7917  6 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

7 
theory Hahn_Banach_Ext_Lemmas 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

8 
imports Function_Norm 
27612  9 
begin 
7917  10 

58744  11 
text \<open> 
61879  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>. 

7917  19 

61540  20 
Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>. 
7917  21 

61486  22 
\<^medskip> 
61540  23 
This lemma will be used to show the existence of a linear extension of \<open>f\<close> 
24 
(see page \pageref{exxiuse}). It is a consequence of the completeness of 

25 
\<open>\<real>\<close>. To show 

10687  26 
\begin{center} 
27 
\begin{tabular}{l} 

61539  28 
\<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close> 
10687  29 
\end{tabular} 
30 
\end{center} 

61540  31 
\<^noindent> it suffices to show that 
10687  32 
\begin{center} 
33 
\begin{tabular}{l} 

61539  34 
\<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close> 
10687  35 
\end{tabular} 
36 
\end{center} 

58744  37 
\<close> 
7917  38 

10687  39 
lemma ex_xi: 
27611  40 
assumes "vectorspace F" 
13515  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" 

10007  43 
proof  
29234  44 
interpret vectorspace F by fact 
58744  45 
txt \<open>From the completeness of the reals follows: 
61539  46 
The set \<open>S = {a u. u \<in> F}\<close> has a supremum, if it is 
58744  47 
nonempty and has an upper bound.\<close> 
7917  48 

13515  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:) 

10007  60 
qed 
13515  61 
then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" .. 
10007  62 
qed 
13515  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) 

60458  68 
} 
69 
moreover { 

13515  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:) 

10007  77 
qed 
60458  78 
} 
79 
ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast 

10007  80 
qed 
7917  81 

58744  82 
text \<open> 
61486  83 
\<^medskip> 
61879  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>. 

58744  86 
\<close> 
7917  87 

10687  88 
lemma h'_lf: 
63040  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" 

13515  92 
and HE: "H \<unlhd> E" 
27611  93 
assumes "linearform H h" 
13515  94 
assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" 
27611  95 
assumes E: "vectorspace E" 
13515  96 
shows "linearform H' h'" 
27611  97 
proof  
29234  98 
interpret linearform H h by fact 
99 
interpret vectorspace E by fact 

27612  100 
show ?thesis 
101 
proof 

58744  102 
note E = \<open>vectorspace E\<close> 
27611  103 
have H': "vectorspace H'" 
104 
proof (unfold H'_def) 

58744  105 
from \<open>x0 \<in> E\<close> 
27611  106 
have "lin x0 \<unlhd> E" .. 
47445
69e96e5500df
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
krauss
parents:
44190
diff
changeset

107 
with HE show "vectorspace (H + lin x0)" using E .. 
27611  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  

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

113 
from H' x1 x2 have "x1 + x2 \<in> H'" 
27611  114 
by (rule vectorspace.add_closed) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

115 
with x1 x2 obtain y y1 y2 a a1 a2 where 
27611  116 
x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H" 
13515  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" 

27612  119 
unfolding H'_def sum_def lin_def by blast 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

120 

69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

121 
have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0 
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58889
diff
changeset

122 
proof (rule decomp_H') text_raw \<open>\label{decompHuse}\<close> 
27611  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" . 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

131 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

132 

69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

133 
from h'_def x1x2 E HE y x0 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

134 
have "h' (x1 + x2) = h y + a * xi" 
27611  135 
by (rule h'_definite) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

136 
also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi" 
27611  137 
by (simp only: ya) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

138 
also from y1 y2 have "h (y1 + y2) = h y1 + h y2" 
27611  139 
by simp 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

140 
also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47445
diff
changeset

141 
by (simp add: distrib_right) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

142 
also from h'_def x1_rep E HE y1 x0 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

143 
have "h y1 + a1 * xi = h' x1" 
27611  144 
by (rule h'_definite [symmetric]) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

145 
also from h'_def x2_rep E HE y2 x0 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

146 
have "h y2 + a2 * xi = h' x2" 
27611  147 
by (rule h'_definite [symmetric]) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

148 
finally show ?thesis . 
10007  149 
qed 
27611  150 
next 
151 
fix x1 c assume x1: "x1 \<in> H'" 

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

153 
proof  

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

154 
from H' x1 have ax1: "c \<cdot> x1 \<in> H'" 
27611  155 
by (rule vectorspace.mult_closed) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

156 
with x1 obtain y a y1 a1 where 
27612  157 
cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H" 
13515  158 
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" 
27612  159 
unfolding H'_def sum_def lin_def by blast 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

160 

69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

161 
have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using E HE _ y x0 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

162 
proof (rule decomp_H') 
27611  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" . 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

171 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

172 

69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

173 
from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi" 
27611  174 
by (rule h'_definite) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

175 
also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi" 
27611  176 
by (simp only: ya) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

177 
also from y1 have "h (c \<cdot> y1) = c * h y1" 
27611  178 
by simp 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

179 
also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)" 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47445
diff
changeset

180 
by (simp only: distrib_left) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

181 
also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" 
27611  182 
by (rule h'_definite [symmetric]) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

183 
finally show ?thesis . 
10007  184 
qed 
27611  185 
} 
186 
qed 

10007  187 
qed 
7917  188 

61486  189 
text \<open> 
190 
\<^medskip> 

61540  191 
The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>. 
192 
\<close> 

7917  193 

9374  194 
lemma h'_norm_pres: 
63040  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" 

13515  198 
and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" 
27611  199 
assumes E: "vectorspace E" and HE: "subspace H E" 
200 
and "seminorm E p" and "linearform H h" 

13515  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" 

27611  204 
proof  
29234  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 

27612  209 
show ?thesis 
210 
proof 

27611  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" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

215 
and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0)  h ya" by auto 
27611  216 
from x' obtain y a where 
27612  217 
x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

218 
unfolding H'_def sum_def lin_def by blast 
27611  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" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

223 
by (rule h'_definite) 
27611  224 
also have "\<dots> \<le> p (y + a \<cdot> x0)" 
225 
proof (rule linorder_cases) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

226 
assume z: "a = 0" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

227 
then have "h y + a * xi = h y" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

228 
also from a y have "\<dots> \<le> p y" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

229 
also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

230 
finally show ?thesis . 
27611  231 
next 
61539  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> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

234 
assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

235 
from a1 ay 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

236 
have " p (inverse a \<cdot> y + x0)  h (inverse a \<cdot> y) \<le> xi" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

237 
with lz have "a * xi \<le> 
13515  238 
a * ( p (inverse a \<cdot> y + x0)  h (inverse a \<cdot> y))" 
27611  239 
by (simp add: mult_left_mono_neg order_less_imp_le) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

240 

69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

241 
also have "\<dots> = 
13515  242 
 a * (p (inverse a \<cdot> y + x0))  a * (h (inverse a \<cdot> y))" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

243 
by (simp add: right_diff_distrib) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

244 
also from lz x0 y' have " a * (p (inverse a \<cdot> y + x0)) = 
13515  245 
p (a \<cdot> (inverse a \<cdot> y + x0))" 
27611  246 
by (simp add: abs_homogenous) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

247 
also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" 
27611  248 
by (simp add: add_mult_distrib1 mult_assoc [symmetric]) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

249 
also from nz y have "a * (h (inverse a \<cdot> y)) = h y" 
27611  250 
by simp 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

251 
finally have "a * xi \<le> p (y + a \<cdot> x0)  h y" . 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

252 
then show ?thesis by simp 
27611  253 
next 
61539  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> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

256 
assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

257 
from a2 ay 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

258 
have "xi \<le> p (inverse a \<cdot> y + x0)  h (inverse a \<cdot> y)" .. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

259 
with gz have "a * xi \<le> 
13515  260 
a * (p (inverse a \<cdot> y + x0)  h (inverse a \<cdot> y))" 
27611  261 
by simp 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

262 
also have "\<dots> = a * p (inverse a \<cdot> y + x0)  a * h (inverse a \<cdot> y)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

263 
by (simp add: right_diff_distrib) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

264 
also from gz x0 y' 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

265 
have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))" 
27611  266 
by (simp add: abs_homogenous) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

267 
also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" 
27611  268 
by (simp add: add_mult_distrib1 mult_assoc [symmetric]) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

269 
also from nz y have "a * h (inverse a \<cdot> y) = h y" 
27611  270 
by simp 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

271 
finally have "a * xi \<le> p (y + a \<cdot> x0)  h y" . 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

272 
then show ?thesis by simp 
27611  273 
qed 
274 
also from x_rep have "\<dots> = p x" by (simp only:) 

275 
finally show ?thesis . 

10007  276 
qed 
277 
qed 

13515  278 
qed 
7917  279 

10007  280 
end 