--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Aug 22 20:49:43 2002 +0200
@@ -17,17 +17,15 @@
an element in @{text "E - H"}. @{text H} is extended to the direct
sum @{text "H' = H + lin x\<^sub>0"}, so for any @{text "x \<in> H'"}
the decomposition of @{text "x = y + a \<cdot> x"} with @{text "y \<in> H"} is
- unique. @{text h'} is defined on @{text H'} by
- @{text "h' x = h y + a \<cdot> \<xi>"} for a certain @{text \<xi>}.
+ unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +
+ a \<cdot> \<xi>"} for a certain @{text \<xi>}.
Subsequently we show some properties of this extension @{text h'} of
@{text h}.
-*}
-text {*
- This lemma will be used to show the existence of a linear extension
- of @{text f} (see page \pageref{ex-xi-use}). It is a consequence of
- the completeness of @{text \<real>}. To show
+ \medskip This lemma will be used to show the existence of a linear
+ extension of @{text f} (see page \pageref{ex-xi-use}). It is a
+ consequence of the completeness of @{text \<real>}. To show
\begin{center}
\begin{tabular}{l}
@{text "\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y"}
@@ -42,307 +40,227 @@
*}
lemma ex_xi:
- "is_vectorspace F \<Longrightarrow> (\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v)
- \<Longrightarrow> \<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
+ includes vectorspace F
+ assumes r: "\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> b v"
+ shows "\<exists>xi::real. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
proof -
- assume vs: "is_vectorspace F"
- assume r: "(\<And>u v. u \<in> F \<Longrightarrow> v \<in> F \<Longrightarrow> a u \<le> (b v::real))"
-
txt {* From the completeness of the reals follows:
- The set @{text "S = {a u. u \<in> F}"} has a supremum, if
- it is non-empty and has an upper bound. *}
-
- let ?S = "{a u :: real | u. u \<in> F}"
-
- have "\<exists>xi. isLub UNIV ?S xi"
- proof (rule reals_complete)
-
- txt {* The set @{text S} is non-empty, since @{text "a 0 \<in> S"}: *}
-
- from vs have "a 0 \<in> ?S" by blast
- thus "\<exists>X. X \<in> ?S" ..
-
- txt {* @{text "b 0"} is an upper bound of @{text S}: *}
-
- show "\<exists>Y. isUb UNIV ?S Y"
- proof
- show "isUb UNIV ?S (b 0)"
- proof (intro isUbI setleI ballI)
- show "b 0 \<in> UNIV" ..
- next
-
- txt {* Every element @{text "y \<in> S"} is less than @{text "b 0"}: *}
+ The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
+ non-empty and has an upper bound. *}
- fix y assume y: "y \<in> ?S"
- from y have "\<exists>u \<in> F. y = a u" by fast
- thus "y \<le> b 0"
- proof
- fix u assume "u \<in> F"
- assume "y = a u"
- also have "a u \<le> b 0" by (rule r) (simp!)+
- finally show ?thesis .
- qed
- qed
+ let ?S = "{a u | u. u \<in> F}"
+ have "\<exists>xi. lub ?S xi"
+ proof (rule real_complete)
+ have "a 0 \<in> ?S" by blast
+ then show "\<exists>X. X \<in> ?S" ..
+ have "\<forall>y \<in> ?S. y \<le> b 0"
+ proof
+ fix y assume y: "y \<in> ?S"
+ then obtain u where u: "u \<in> F" and y: "y = a u" by blast
+ from u and zero have "a u \<le> b 0" by (rule r)
+ with y show "y \<le> b 0" by (simp only:)
qed
+ then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..
qed
-
- thus "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y"
- proof (elim exE)
- fix xi assume "isLub UNIV ?S xi"
- show ?thesis
- proof (intro exI conjI ballI)
-
- txt {* For all @{text "y \<in> F"} holds @{text "a y \<le> \<xi>"}: *}
-
- fix y assume y: "y \<in> F"
- show "a y \<le> xi"
- proof (rule isUbD)
- show "isUb UNIV ?S xi" ..
- qed (blast!)
- next
-
- txt {* For all @{text "y \<in> F"} holds @{text "\<xi> \<le> b y"}: *}
-
- fix y assume "y \<in> F"
- show "xi \<le> b y"
- proof (intro isLub_le_isUb isUbI setleI)
- show "b y \<in> UNIV" ..
- show "\<forall>ya \<in> ?S. ya \<le> b y"
- proof
- fix au assume au: "au \<in> ?S "
- hence "\<exists>u \<in> F. au = a u" by fast
- thus "au \<le> b y"
- proof
- fix u assume "u \<in> F" assume "au = a u"
- also have "... \<le> b y" by (rule r)
- finally show ?thesis .
- qed
- qed
- qed
+ then obtain xi where xi: "lub ?S xi" ..
+ {
+ fix y assume "y \<in> F"
+ then have "a y \<in> ?S" by blast
+ with xi have "a y \<le> xi" by (rule lub.upper)
+ } moreover {
+ fix y assume y: "y \<in> F"
+ from xi have "xi \<le> b y"
+ proof (rule lub.least)
+ fix au assume "au \<in> ?S"
+ then obtain u where u: "u \<in> F" and au: "au = a u" by blast
+ from u y have "a u \<le> b y" by (rule r)
+ with au show "au \<le> b y" by (simp only:)
qed
- qed
+ } ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
qed
text {*
- \medskip The function @{text h'} is defined as a
- @{text "h' x = h y + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a
- linear extension of @{text h} to @{text H'}. *}
+ \medskip The function @{text h'} is defined as a @{text "h' x = h y
+ + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of
+ @{text h} to @{text H'}.
+*}
lemma h'_lf:
- "h' \<equiv> \<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi
- \<Longrightarrow> H' \<equiv> H + lin x0 \<Longrightarrow> is_subspace H E \<Longrightarrow> is_linearform H h \<Longrightarrow> x0 \<notin> H
- \<Longrightarrow> x0 \<in> E \<Longrightarrow> x0 \<noteq> 0 \<Longrightarrow> is_vectorspace E
- \<Longrightarrow> is_linearform H' h'"
-proof -
- assume h'_def:
- "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
- in h y + a * xi)"
+ includes var H + var h + var E
+ assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
+ SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
and H'_def: "H' \<equiv> H + lin x0"
- and vs: "is_subspace H E" "is_linearform H h" "x0 \<notin> H"
- "x0 \<noteq> 0" "x0 \<in> E" "is_vectorspace E"
-
- have h': "is_vectorspace H'"
- proof (unfold H'_def, rule vs_sum_vs)
- show "is_subspace (lin x0) E" ..
+ and HE: "H \<unlhd> E"
+ includes linearform H h
+ assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
+ includes vectorspace E
+ shows "linearform H' h'"
+proof
+ have H': "vectorspace H'"
+ proof (unfold H'_def)
+ have "x0 \<in> E" .
+ then have "lin x0 \<unlhd> E" ..
+ with HE show "vectorspace (H + lin x0)" ..
qed
-
- show ?thesis
- proof
+ {
fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'"
-
- txt {* We now have to show that @{text h'} is additive, i.~e.\
- @{text "h' (x\<^sub>1 + x\<^sub>2) = h' x\<^sub>1 + h' x\<^sub>2"} for
- @{text "x\<^sub>1, x\<^sub>2 \<in> H"}. *}
+ show "h' (x1 + x2) = h' x1 + h' x2"
+ proof -
+ from H' x1 x2 have "x1 + x2 \<in> H'"
+ by (rule vectorspace.add_closed)
+ with x1 x2 obtain y y1 y2 a a1 a2 where
+ x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H"
+ and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
+ and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H"
+ by (unfold H'_def sum_def lin_def) blast
- have x1x2: "x1 + x2 \<in> H'"
- by (rule vs_add_closed, rule h')
- from x1
- have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H"
- by (unfold H'_def vs_sum_def lin_def) fast
- from x2
- have ex_x2: "\<exists>y2 a2. x2 = y2 + a2 \<cdot> x0 \<and> y2 \<in> H"
- by (unfold H'_def vs_sum_def lin_def) fast
- from x1x2
- have ex_x1x2: "\<exists>y a. x1 + x2 = y + a \<cdot> x0 \<and> y \<in> H"
- by (unfold H'_def vs_sum_def lin_def) fast
-
- from ex_x1 ex_x2 ex_x1x2
- show "h' (x1 + x2) = h' x1 + h' x2"
- proof (elim exE conjE)
- fix y1 y2 y a1 a2 a
- assume y1: "x1 = y1 + a1 \<cdot> x0" and y1': "y1 \<in> H"
- and y2: "x2 = y2 + a2 \<cdot> x0" and y2': "y2 \<in> H"
- and y: "x1 + x2 = y + a \<cdot> x0" and y': "y \<in> H"
- txt {* \label{decomp-H-use}*}
- have ya: "y1 + y2 = y \<and> a1 + a2 = a"
- proof (rule decomp_H')
- show "y1 + y2 + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0"
- by (simp! add: vs_add_mult_distrib2 [of E])
- show "y1 + y2 \<in> H" ..
+ have ya: "y1 + y2 = y \<and> a1 + a2 = a" using _ HE _ y x0
+ proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *}
+ from HE y1 y2 show "y1 + y2 \<in> H"
+ by (rule subspace.add_closed)
+ from x0 and HE y y1 y2
+ have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto
+ with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2"
+ by (simp add: add_ac add_mult_distrib2)
+ also note x1x2
+ finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
qed
+ from h'_def x1x2 _ 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 add: ya)
- also from vs y1' y2'
- have "... = h y1 + h y2 + a1 * xi + a2 * xi"
- by (simp add: linearform_add [of H]
- real_add_mult_distrib)
- also have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
+ also have "\<dots> = 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 "h y1 + a1 * xi = h' x1"
+ also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
+ by (simp add: real_add_mult_distrib)
+ also from h'_def x1_rep _ HE y1 x0
+ have "h y1 + a1 * xi = h' x1"
by (rule h'_definite [symmetric])
- also have "h y2 + a2 * xi = h' x2"
+ also from h'_def x2_rep _ HE y2 x0
+ have "h y2 + a2 * xi = h' x2"
by (rule h'_definite [symmetric])
finally show ?thesis .
qed
-
- txt {* We further have to show that @{text h'} is multiplicative,
- i.~e.\ @{text "h' (c \<cdot> x\<^sub>1) = c \<cdot> h' x\<^sub>1"} for @{text "x \<in> H"}
- and @{text "c \<in> \<real>"}. *}
-
next
- fix c x1 assume x1: "x1 \<in> H'"
- have ax1: "c \<cdot> x1 \<in> H'"
- by (rule vs_mult_closed, rule h')
- from x1
- have ex_x: "\<And>x. x\<in> H' \<Longrightarrow> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
- by (unfold H'_def vs_sum_def lin_def) fast
+ fix x1 c assume x1: "x1 \<in> H'"
+ show "h' (c \<cdot> x1) = c * (h' x1)"
+ proof -
+ from H' x1 have ax1: "c \<cdot> x1 \<in> H'"
+ by (rule vectorspace.mult_closed)
+ with x1 obtain y a y1 a1 where
+ cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
+ and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
+ by (unfold H'_def sum_def lin_def) blast
- from x1 have ex_x1: "\<exists>y1 a1. x1 = y1 + a1 \<cdot> x0 \<and> y1 \<in> H"
- by (unfold H'_def vs_sum_def lin_def) fast
- with ex_x [of "c \<cdot> x1", OF ax1]
- show "h' (c \<cdot> x1) = c * (h' x1)"
- proof (elim exE conjE)
- fix y1 y a1 a
- assume y1: "x1 = y1 + a1 \<cdot> x0" and y1': "y1 \<in> H"
- and y: "c \<cdot> x1 = y + a \<cdot> x0" and y': "y \<in> H"
-
- have ya: "c \<cdot> y1 = y \<and> c * a1 = a"
+ have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using _ HE _ y x0
proof (rule decomp_H')
- show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0"
- by (simp! add: vs_add_mult_distrib1)
- show "c \<cdot> y1 \<in> H" ..
+ from HE y1 show "c \<cdot> y1 \<in> H"
+ by (rule subspace.mult_closed)
+ from x0 and HE y y1
+ have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto
+ with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1"
+ by (simp add: mult_assoc add_mult_distrib1)
+ also note cx1_rep
+ finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
qed
- have "h' (c \<cdot> x1) = h y + a * xi"
+ from h'_def cx1_rep _ HE y x0 have "h' (c \<cdot> x1) = h y + a * xi"
by (rule h'_definite)
- also have "... = h (c \<cdot> y1) + (c * a1) * xi"
- by (simp add: ya)
- also from vs y1' have "... = c * h y1 + c * a1 * xi"
- by (simp add: linearform_mult [of H])
- also from vs y1' have "... = c * (h y1 + a1 * xi)"
- by (simp add: real_add_mult_distrib2 real_mult_assoc)
- also have "h y1 + a1 * xi = h' x1"
+ also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi"
+ by (simp only: ya)
+ also from y1 have "h (c \<cdot> y1) = c * h y1"
+ by simp
+ also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)"
+ by (simp only: real_add_mult_distrib2)
+ also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1"
by (rule h'_definite [symmetric])
finally show ?thesis .
qed
- qed
+ }
qed
text {* \medskip The linear extension @{text h'} of @{text h}
-is bounded by the seminorm @{text p}. *}
+ is bounded by the seminorm @{text p}. *}
lemma h'_norm_pres:
- "h' \<equiv> \<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi
- \<Longrightarrow> H' \<equiv> H + lin x0 \<Longrightarrow> x0 \<notin> H \<Longrightarrow> x0 \<in> E \<Longrightarrow> x0 \<noteq> 0 \<Longrightarrow> is_vectorspace E
- \<Longrightarrow> is_subspace H E \<Longrightarrow> is_seminorm E p \<Longrightarrow> is_linearform H h
- \<Longrightarrow> \<forall>y \<in> H. h y \<le> p y
- \<Longrightarrow> \<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y
- \<Longrightarrow> \<forall>x \<in> H'. h' x \<le> p x"
-proof
- assume h'_def:
- "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H
- in (h y) + a * xi)"
+ includes var H + var h + var E
+ assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =
+ SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
and H'_def: "H' \<equiv> H + lin x0"
- and vs: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" "is_vectorspace E"
- "is_subspace H E" "is_seminorm E p" "is_linearform H h"
- and a: "\<forall>y \<in> H. h y \<le> p y"
- presume a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
- presume a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya"
- fix x assume "x \<in> H'"
- have ex_x:
- "\<And>x. x \<in> H' \<Longrightarrow> \<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
- by (unfold H'_def vs_sum_def lin_def) fast
- have "\<exists>y a. x = y + a \<cdot> x0 \<and> y \<in> H"
- by (rule ex_x)
- thus "h' x \<le> p x"
- proof (elim exE conjE)
- fix y a assume x: "x = y + a \<cdot> x0" and y: "y \<in> H"
- have "h' x = h y + a * xi"
+ and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
+ includes vectorspace E + subvectorspace H E +
+ seminorm E p + linearform H h
+ assumes a: "\<forall>y \<in> H. h y \<le> p y"
+ and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
+ shows "\<forall>x \<in> H'. h' x \<le> p x"
+proof
+ fix x assume x': "x \<in> H'"
+ show "h' x \<le> p x"
+ proof -
+ from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi"
+ and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto
+ from x' obtain y a where
+ x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
+ by (unfold H'_def sum_def lin_def) blast
+ from y have y': "y \<in> E" ..
+ from y have ay: "inverse a \<cdot> y \<in> H" by simp
+
+ from h'_def x_rep _ _ y x0 have "h' x = h y + a * xi"
by (rule h'_definite)
-
- txt {* Now we show @{text "h y + a \<cdot> \<xi> \<le> p (y + a \<cdot> x\<^sub>0)"}
- by case analysis on @{text a}. *}
-
- also have "... \<le> p (y + a \<cdot> x0)"
+ also have "\<dots> \<le> p (y + a \<cdot> x0)"
proof (rule linorder_cases)
-
assume z: "a = 0"
- with vs y a show ?thesis by simp
-
- txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
- with @{text ya} taken as @{text "y / a"}: *}
-
+ then have "h y + a * xi = h y" by simp
+ also from a y have "\<dots> \<le> p y" ..
+ also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp
+ finally show ?thesis .
next
+ txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"}
+ with @{text ya} taken as @{text "y / a"}: *}
assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp
- from a1
- have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi"
- by (rule bspec) (simp!)
-
- txt {* The thesis for this case now follows by a short
- calculation. *}
- hence "a * xi \<le> a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
- by (rule real_mult_less_le_anti [OF lz])
- also
- have "... = - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
+ from a1 ay
+ have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" ..
+ with lz have "a * xi \<le>
+ a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
+ by (rule real_mult_less_le_anti)
+ also have "\<dots> =
+ - a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
by (rule real_mult_diff_distrib)
- also from lz vs y
- have "- a * (p (inverse a \<cdot> y + x0)) = p (a \<cdot> (inverse a \<cdot> y + x0))"
- by (simp add: seminorm_abs_homogenous abs_minus_eqI2)
- also from nz vs y have "... = p (y + a \<cdot> x0)"
- by (simp add: vs_add_mult_distrib1)
- also from nz vs y have "a * (h (inverse a \<cdot> y)) = h y"
- by (simp add: linearform_mult [symmetric])
+ also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
+ p (a \<cdot> (inverse a \<cdot> y + x0))"
+ by (simp add: abs_homogenous abs_minus_eqI2)
+ also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
+ by (simp add: add_mult_distrib1 mult_assoc [symmetric])
+ also from nz y have "a * (h (inverse a \<cdot> y)) = h y"
+ by simp
finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
-
- hence "h y + a * xi \<le> h y + p (y + a \<cdot> x0) - h y"
- by (simp add: real_add_left_cancel_le)
- thus ?thesis by simp
-
+ then show ?thesis by simp
+ next
txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"}
with @{text ya} taken as @{text "y / a"}: *}
-
- next
assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp
- from a2 have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)"
- by (rule bspec) (simp!)
-
- txt {* The thesis for this case follows by a short
- calculation: *}
-
- with gz
- have "a * xi \<le> a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
+ from a2 ay
+ have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" ..
+ with gz have "a * xi \<le>
+ a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
by (rule real_mult_less_le_mono)
also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
by (rule real_mult_diff_distrib2)
- also from gz vs y
+ also from gz x0 y'
have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
- by (simp add: seminorm_abs_homogenous abs_eqI2)
- also from nz vs y have "... = p (y + a \<cdot> x0)"
- by (simp add: vs_add_mult_distrib1)
- also from nz vs y have "a * h (inverse a \<cdot> y) = h y"
- by (simp add: linearform_mult [symmetric])
+ by (simp add: abs_homogenous abs_eqI2)
+ also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)"
+ by (simp add: add_mult_distrib1 mult_assoc [symmetric])
+ also from nz y have "a * h (inverse a \<cdot> y) = h y"
+ by simp
finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" .
-
- hence "h y + a * xi \<le> h y + (p (y + a \<cdot> x0) - h y)"
- by (simp add: real_add_left_cancel_le)
- thus ?thesis by simp
+ then show ?thesis by simp
qed
- also from x have "... = p x" by simp
+ also from x_rep have "\<dots> = p x" by (simp only:)
finally show ?thesis .
qed
-qed blast+
+qed
end