author | wenzelm |
Mon, 02 Nov 2015 11:43:02 +0100 | |
changeset 61540 | f92bf6674699 |
parent 61539 | a29295dac1ca |
child 61879 | e4f9d8f094fe |
permissions | -rw-r--r-- |
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 non-maximal 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> |
61540 | 12 |
In this section the following context is presumed. Let \<open>E\<close> be a real |
13 |
vector 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> |
|
14 |
a linear function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a |
|
15 |
superspace of \<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> |
|
16 |
and \<open>x\<^sub>0\<close> is an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' |
|
17 |
= H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> |
|
18 |
with \<open>y \<in> H\<close> is unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> |
|
19 |
for a certain \<open>\<xi>\<close>. |
|
7917 | 20 |
|
61540 | 21 |
Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>. |
7917 | 22 |
|
61486 | 23 |
\<^medskip> |
61540 | 24 |
This lemma will be used to show the existence of a linear extension of \<open>f\<close> |
25 |
(see page \pageref{ex-xi-use}). It is a consequence of the completeness of |
|
26 |
\<open>\<real>\<close>. To show |
|
10687 | 27 |
\begin{center} |
28 |
\begin{tabular}{l} |
|
61539 | 29 |
\<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close> |
10687 | 30 |
\end{tabular} |
31 |
\end{center} |
|
61540 | 32 |
\<^noindent> it suffices to show that |
10687 | 33 |
\begin{center} |
34 |
\begin{tabular}{l} |
|
61539 | 35 |
\<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close> |
10687 | 36 |
\end{tabular} |
37 |
\end{center} |
|
58744 | 38 |
\<close> |
7917 | 39 |
|
10687 | 40 |
lemma ex_xi: |
27611 | 41 |
assumes "vectorspace F" |
13515 | 42 |
assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v" |
43 |
shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" |
|
10007 | 44 |
proof - |
29234 | 45 |
interpret vectorspace F by fact |
58744 | 46 |
txt \<open>From the completeness of the reals follows: |
61539 | 47 |
The set \<open>S = {a u. u \<in> F}\<close> has a supremum, if it is |
58744 | 48 |
non-empty and has an upper bound.\<close> |
7917 | 49 |
|
13515 | 50 |
let ?S = "{a u | u. u \<in> F}" |
51 |
have "\<exists>xi. lub ?S xi" |
|
52 |
proof (rule real_complete) |
|
53 |
have "a 0 \<in> ?S" by blast |
|
54 |
then show "\<exists>X. X \<in> ?S" .. |
|
55 |
have "\<forall>y \<in> ?S. y \<le> b 0" |
|
56 |
proof |
|
57 |
fix y assume y: "y \<in> ?S" |
|
58 |
then obtain u where u: "u \<in> F" and y: "y = a u" by blast |
|
59 |
from u and zero have "a u \<le> b 0" by (rule r) |
|
60 |
with y show "y \<le> b 0" by (simp only:) |
|
10007 | 61 |
qed |
13515 | 62 |
then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" .. |
10007 | 63 |
qed |
13515 | 64 |
then obtain xi where xi: "lub ?S xi" .. |
65 |
{ |
|
66 |
fix y assume "y \<in> F" |
|
67 |
then have "a y \<in> ?S" by blast |
|
68 |
with xi have "a y \<le> xi" by (rule lub.upper) |
|
60458 | 69 |
} |
70 |
moreover { |
|
13515 | 71 |
fix y assume y: "y \<in> F" |
72 |
from xi have "xi \<le> b y" |
|
73 |
proof (rule lub.least) |
|
74 |
fix au assume "au \<in> ?S" |
|
75 |
then obtain u where u: "u \<in> F" and au: "au = a u" by blast |
|
76 |
from u y have "a u \<le> b y" by (rule r) |
|
77 |
with au show "au \<le> b y" by (simp only:) |
|
10007 | 78 |
qed |
60458 | 79 |
} |
80 |
ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast |
|
10007 | 81 |
qed |
7917 | 82 |
|
58744 | 83 |
text \<open> |
61486 | 84 |
\<^medskip> |
61540 | 85 |
The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where |
86 |
\<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>. |
|
58744 | 87 |
\<close> |
7917 | 88 |
|
10687 | 89 |
lemma h'_lf: |
13515 | 90 |
assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) = |
91 |
SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi" |
|
47445
69e96e5500df
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
krauss
parents:
44190
diff
changeset
|
92 |
and H'_def: "H' \<equiv> H + lin x0" |
13515 | 93 |
and HE: "H \<unlhd> E" |
27611 | 94 |
assumes "linearform H h" |
13515 | 95 |
assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" |
27611 | 96 |
assumes E: "vectorspace E" |
13515 | 97 |
shows "linearform H' h'" |
27611 | 98 |
proof - |
29234 | 99 |
interpret linearform H h by fact |
100 |
interpret vectorspace E by fact |
|
27612 | 101 |
show ?thesis |
102 |
proof |
|
58744 | 103 |
note E = \<open>vectorspace E\<close> |
27611 | 104 |
have H': "vectorspace H'" |
105 |
proof (unfold H'_def) |
|
58744 | 106 |
from \<open>x0 \<in> E\<close> |
27611 | 107 |
have "lin x0 \<unlhd> E" .. |
47445
69e96e5500df
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
krauss
parents:
44190
diff
changeset
|
108 |
with HE show "vectorspace (H + lin x0)" using E .. |
27611 | 109 |
qed |
110 |
{ |
|
111 |
fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'" |
|
112 |
show "h' (x1 + x2) = h' x1 + h' x2" |
|
113 |
proof - |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
114 |
from H' x1 x2 have "x1 + x2 \<in> H'" |
27611 | 115 |
by (rule vectorspace.add_closed) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
116 |
with x1 x2 obtain y y1 y2 a a1 a2 where |
27611 | 117 |
x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H" |
13515 | 118 |
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" |
119 |
and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H" |
|
27612 | 120 |
unfolding H'_def sum_def lin_def by blast |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
121 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
122 |
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
|
123 |
proof (rule decomp_H') text_raw \<open>\label{decomp-H-use}\<close> |
27611 | 124 |
from HE y1 y2 show "y1 + y2 \<in> H" |
125 |
by (rule subspace.add_closed) |
|
126 |
from x0 and HE y y1 y2 |
|
127 |
have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto |
|
128 |
with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2" |
|
129 |
by (simp add: add_ac add_mult_distrib2) |
|
130 |
also note x1x2 |
|
131 |
finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" . |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
132 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
133 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
134 |
from h'_def x1x2 E HE y x0 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
135 |
have "h' (x1 + x2) = h y + a * xi" |
27611 | 136 |
by (rule h'_definite) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
137 |
also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi" |
27611 | 138 |
by (simp only: ya) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
139 |
also from y1 y2 have "h (y1 + y2) = h y1 + h y2" |
27611 | 140 |
by simp |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
141 |
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
|
142 |
by (simp add: distrib_right) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
143 |
also from h'_def x1_rep E HE y1 x0 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
144 |
have "h y1 + a1 * xi = h' x1" |
27611 | 145 |
by (rule h'_definite [symmetric]) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
146 |
also from h'_def x2_rep E HE y2 x0 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
147 |
have "h y2 + a2 * xi = h' x2" |
27611 | 148 |
by (rule h'_definite [symmetric]) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
149 |
finally show ?thesis . |
10007 | 150 |
qed |
27611 | 151 |
next |
152 |
fix x1 c assume x1: "x1 \<in> H'" |
|
153 |
show "h' (c \<cdot> x1) = c * (h' x1)" |
|
154 |
proof - |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
155 |
from H' x1 have ax1: "c \<cdot> x1 \<in> H'" |
27611 | 156 |
by (rule vectorspace.mult_closed) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
157 |
with x1 obtain y a y1 a1 where |
27612 | 158 |
cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H" |
13515 | 159 |
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" |
27612 | 160 |
unfolding H'_def sum_def lin_def by blast |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
161 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
162 |
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 tab-width;
wenzelm
parents:
31795
diff
changeset
|
163 |
proof (rule decomp_H') |
27611 | 164 |
from HE y1 show "c \<cdot> y1 \<in> H" |
165 |
by (rule subspace.mult_closed) |
|
166 |
from x0 and HE y y1 |
|
167 |
have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto |
|
168 |
with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1" |
|
169 |
by (simp add: mult_assoc add_mult_distrib1) |
|
170 |
also note cx1_rep |
|
171 |
finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" . |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
172 |
qed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
173 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
174 |
from h'_def cx1_rep E HE y x0 have "h' (c \<cdot> x1) = h y + a * xi" |
27611 | 175 |
by (rule h'_definite) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
176 |
also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi" |
27611 | 177 |
by (simp only: ya) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
178 |
also from y1 have "h (c \<cdot> y1) = c * h y1" |
27611 | 179 |
by simp |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
180 |
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
|
181 |
by (simp only: distrib_left) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
182 |
also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1" |
27611 | 183 |
by (rule h'_definite [symmetric]) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
184 |
finally show ?thesis . |
10007 | 185 |
qed |
27611 | 186 |
} |
187 |
qed |
|
10007 | 188 |
qed |
7917 | 189 |
|
61486 | 190 |
text \<open> |
191 |
\<^medskip> |
|
61540 | 192 |
The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>. |
193 |
\<close> |
|
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" |
|
47445
69e96e5500df
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
krauss
parents:
44190
diff
changeset
|
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 - |
29234 | 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" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
216 |
and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto |
27611 | 217 |
from x' obtain y a where |
27612 | 218 |
x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
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" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
224 |
by (rule h'_definite) |
27611 | 225 |
also have "\<dots> \<le> p (y + a \<cdot> x0)" |
226 |
proof (rule linorder_cases) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
227 |
assume z: "a = 0" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
228 |
then have "h y + a * xi = h y" by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
229 |
also from a y have "\<dots> \<le> p y" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
230 |
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 tab-width;
wenzelm
parents:
31795
diff
changeset
|
231 |
finally show ?thesis . |
27611 | 232 |
next |
61539 | 233 |
txt \<open>In the case \<open>a < 0\<close>, we use \<open>a\<^sub>1\<close> |
234 |
with \<open>ya\<close> taken as \<open>y / a\<close>:\<close> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
235 |
assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
236 |
from a1 ay |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
237 |
have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
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) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
241 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
242 |
also have "\<dots> = |
13515 | 243 |
- a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
244 |
by (simp add: right_diff_distrib) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
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) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
248 |
also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" |
27611 | 249 |
by (simp add: add_mult_distrib1 mult_assoc [symmetric]) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
250 |
also from nz y have "a * (h (inverse a \<cdot> y)) = h y" |
27611 | 251 |
by simp |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
252 |
finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
253 |
then show ?thesis by simp |
27611 | 254 |
next |
61539 | 255 |
txt \<open>In the case \<open>a > 0\<close>, we use \<open>a\<^sub>2\<close> |
256 |
with \<open>ya\<close> taken as \<open>y / a\<close>:\<close> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
257 |
assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
258 |
from a2 ay |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
259 |
have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" .. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
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 |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
263 |
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 tab-width;
wenzelm
parents:
31795
diff
changeset
|
264 |
by (simp add: right_diff_distrib) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
265 |
also from gz x0 y' |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
266 |
have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))" |
27611 | 267 |
by (simp add: abs_homogenous) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
268 |
also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" |
27611 | 269 |
by (simp add: add_mult_distrib1 mult_assoc [symmetric]) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
270 |
also from nz y have "a * h (inverse a \<cdot> y) = h y" |
27611 | 271 |
by simp |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
272 |
finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
31795
diff
changeset
|
273 |
then show ?thesis by simp |
27611 | 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 |