--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Sun Jun 04 00:09:04 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Sun Jun 04 19:39:29 2000 +0200
@@ -3,9 +3,9 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Extending non-maximal functions *};
+header {* Extending non-maximal functions *}
-theory HahnBanachExtLemmas = FunctionNorm:;
+theory HahnBanachExtLemmas = FunctionNorm:
text{* In this section the following context is presumed.
Let $E$ be a real vector space with a
@@ -19,7 +19,7 @@
$h_0\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$.
Subsequently we show some properties of this extension $h_0$ of $h$.
-*};
+*}
text {* This lemma will be used to show the existence of a linear
@@ -32,212 +32,212 @@
it suffices to show that
\begin{matharray}{l} \All
{u\in F}{\All {v\in F}{a\ap u \leq b \ap v}}
-\end{matharray} *};
+\end{matharray} *}
lemma ex_xi:
"[| is_vectorspace F; !! u v. [| u:F; v:F |] ==> a u <= b v |]
- ==> EX (xi::real). ALL y:F. a y <= xi & xi <= b y";
-proof -;
- assume vs: "is_vectorspace F";
- assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
+ ==> EX (xi::real). ALL y:F. a y <= xi & xi <= b y"
+proof -
+ assume vs: "is_vectorspace F"
+ assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))"
txt {* From the completeness of the reals follows:
The set $S = \{a\: u\dt\: u\in F\}$ has a supremum, if
- it is non-empty and has an upper bound. *};
+ it is non-empty and has an upper bound. *}
- let ?S = "{a u :: real | u. u:F}";
+ let ?S = "{a u :: real | u. u:F}"
- have "EX xi. isLub UNIV ?S xi";
- proof (rule reals_complete);
+ have "EX xi. isLub UNIV ?S xi"
+ proof (rule reals_complete)
- txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
+ txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *}
- from vs; have "a 00 : ?S"; by force;
- thus "EX X. X : ?S"; ..;
+ from vs have "a 00 : ?S" by force
+ thus "EX X. X : ?S" ..
- txt {* $b\ap \zero$ is an upper bound of $S$: *};
+ txt {* $b\ap \zero$ is an upper bound of $S$: *}
- show "EX Y. isUb UNIV ?S Y";
- proof;
- show "isUb UNIV ?S (b 00)";
- proof (intro isUbI setleI ballI);
- show "b 00 : UNIV"; ..;
- next;
+ show "EX Y. isUb UNIV ?S Y"
+ proof
+ show "isUb UNIV ?S (b 00)"
+ proof (intro isUbI setleI ballI)
+ show "b 00 : UNIV" ..
+ next
- txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
+ txt {* Every element $y\in S$ is less than $b\ap \zero$: *}
- fix y; assume y: "y : ?S";
- from y; have "EX u:F. y = a u"; by fast;
- thus "y <= b 00";
- proof;
- fix u; assume "u:F";
- assume "y = a u";
- also; have "a u <= b 00"; by (rule r) (simp!)+;
- finally; show ?thesis; .;
- qed;
- qed;
- qed;
- qed;
+ fix y assume y: "y : ?S"
+ from y have "EX u:F. y = a u" by fast
+ thus "y <= b 00"
+ proof
+ fix u assume "u:F"
+ assume "y = a u"
+ also have "a u <= b 00" by (rule r) (simp!)+
+ finally show ?thesis .
+ qed
+ qed
+ qed
+ qed
- thus "EX xi. ALL y:F. a y <= xi & xi <= b y";
- proof (elim exE);
- fix xi; assume "isLub UNIV ?S xi";
- show ?thesis;
- proof (intro exI conjI ballI);
+ thus "EX xi. ALL y:F. a y <= xi & xi <= b y"
+ proof (elim exE)
+ fix xi assume "isLub UNIV ?S xi"
+ show ?thesis
+ proof (intro exI conjI ballI)
- txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *};
+ txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *}
- fix y; assume y: "y:F";
- show "a y <= xi";
- proof (rule isUbD);
- show "isUb UNIV ?S xi"; ..;
- qed (force!);
- next;
+ fix y assume y: "y:F"
+ show "a y <= xi"
+ proof (rule isUbD)
+ show "isUb UNIV ?S xi" ..
+ qed (force!)
+ next
- txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *};
+ txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *}
- fix y; assume "y:F";
- show "xi <= b y";
- proof (intro isLub_le_isUb isUbI setleI);
- show "b y : UNIV"; ..;
- show "ALL ya : ?S. ya <= b y";
- proof;
- fix au; assume au: "au : ?S ";
- hence "EX u:F. au = a u"; by fast;
- thus "au <= b y";
- proof;
- fix u; assume "u:F"; assume "au = a u";
- also; have "... <= b y"; by (rule r);
- finally; show ?thesis; .;
- qed;
- qed;
- qed;
- qed;
- qed;
-qed;
+ fix y assume "y:F"
+ show "xi <= b y"
+ proof (intro isLub_le_isUb isUbI setleI)
+ show "b y : UNIV" ..
+ show "ALL ya : ?S. ya <= b y"
+ proof
+ fix au assume au: "au : ?S "
+ hence "EX u:F. au = a u" by fast
+ thus "au <= b y"
+ proof
+ fix u assume "u:F" assume "au = a u"
+ also have "... <= b y" by (rule r)
+ finally show ?thesis .
+ qed
+ qed
+ qed
+ qed
+ qed
+qed
text{* \medskip The function $h_0$ is defined as a
$h_0\ap x = h\ap y + a\cdot \xi$ where $x = y + a\mult \xi$
-is a linear extension of $h$ to $H_0$. *};
+is a linear extension of $h$ to $H_0$. *}
lemma h0_lf:
"[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in h y + a * xi);
H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H;
x0 : E; x0 ~= 00; is_vectorspace E |]
- ==> is_linearform H0 h0";
-proof -;
+ ==> is_linearform H0 h0"
+proof -
assume h0_def:
"h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in h y + a * xi)"
and H0_def: "H0 == H + lin x0"
and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
- "x0 ~= 00" "x0 : E" "is_vectorspace E";
+ "x0 ~= 00" "x0 : E" "is_vectorspace E"
- have h0: "is_vectorspace H0";
- proof (unfold H0_def, rule vs_sum_vs);
- show "is_subspace (lin x0) E"; ..;
- qed;
+ have h0: "is_vectorspace H0"
+ proof (unfold H0_def, rule vs_sum_vs)
+ show "is_subspace (lin x0) E" ..
+ qed
- show ?thesis;
- proof;
- fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0";
+ show ?thesis
+ proof
+ fix x1 x2 assume x1: "x1 : H0" and x2: "x2 : H0"
txt{* We now have to show that $h_0$ is additive, i.~e.\
$h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
- for $x_1, x_2\in H$. *};
+ for $x_1, x_2\in H$. *}
- have x1x2: "x1 + x2 : H0";
- by (rule vs_add_closed, rule h0);
- from x1;
- have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
- from x2;
- have ex_x2: "EX y2 a2. x2 = y2 + a2 (*) x0 & y2 : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
- from x1x2;
- have ex_x1x2: "EX y a. x1 + x2 = y + a (*) x0 & y : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
+ have x1x2: "x1 + x2 : H0"
+ by (rule vs_add_closed, rule h0)
+ from x1
+ have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H"
+ by (unfold H0_def vs_sum_def lin_def) fast
+ from x2
+ have ex_x2: "EX y2 a2. x2 = y2 + a2 (*) x0 & y2 : H"
+ by (unfold H0_def vs_sum_def lin_def) fast
+ from x1x2
+ have ex_x1x2: "EX y a. x1 + x2 = y + a (*) x0 & y : H"
+ by (unfold H0_def vs_sum_def lin_def) fast
- from ex_x1 ex_x2 ex_x1x2;
- show "h0 (x1 + x2) = h0 x1 + h0 x2";
- proof (elim exE conjE);
- fix y1 y2 y a1 a2 a;
+ from ex_x1 ex_x2 ex_x1x2
+ show "h0 (x1 + x2) = h0 x1 + h0 x2"
+ proof (elim exE conjE)
+ fix y1 y2 y a1 a2 a
assume y1: "x1 = y1 + a1 (*) x0" and y1': "y1 : H"
and y2: "x2 = y2 + a2 (*) x0" and y2': "y2 : H"
- and y: "x1 + x2 = y + a (*) x0" and y': "y : H";
+ and y: "x1 + x2 = y + a (*) x0" and y': "y : H"
- have ya: "y1 + y2 = y & a1 + a2 = a";
- proof (rule decomp_H0);;
- txt_raw {* \label{decomp-H0-use} *};;
- show "y1 + y2 + (a1 + a2) (*) x0 = y + a (*) x0";
- by (simp! add: vs_add_mult_distrib2 [of E]);
- show "y1 + y2 : H"; ..;
- qed;
+ have ya: "y1 + y2 = y & a1 + a2 = a"
+ proof (rule decomp_H0)
+ txt_raw {* \label{decomp-H0-use} *}
+ show "y1 + y2 + (a1 + a2) (*) x0 = y + a (*) x0"
+ by (simp! add: vs_add_mult_distrib2 [of E])
+ show "y1 + y2 : H" ..
+ qed
- have "h0 (x1 + x2) = h y + a * xi";
- by (rule h0_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";
+ have "h0 (x1 + x2) = h y + a * xi"
+ by (rule h0_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)";
- by simp;
- also; have "h y1 + a1 * xi = h0 x1";
- by (rule h0_definite [RS sym]);
- also; have "h y2 + a2 * xi = h0 x2";
- by (rule h0_definite [RS sym]);
- finally; show ?thesis; .;
- qed;
+ real_add_mult_distrib)
+ also have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"
+ by simp
+ also have "h y1 + a1 * xi = h0 x1"
+ by (rule h0_definite [RS sym])
+ also have "h y2 + a2 * xi = h0 x2"
+ by (rule h0_definite [RS sym])
+ finally show ?thesis .
+ qed
txt{* We further have to show that $h_0$ is multiplicative,
i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
for $x\in H$ and $c\in \bbbR$.
- *};
+ *}
- next;
- fix c x1; assume x1: "x1 : H0";
- have ax1: "c (*) x1 : H0";
- by (rule vs_mult_closed, rule h0);
- from x1; have ex_x: "!! x. x: H0
- ==> EX y a. x = y + a (*) x0 & y : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
+ next
+ fix c x1 assume x1: "x1 : H0"
+ have ax1: "c (*) x1 : H0"
+ by (rule vs_mult_closed, rule h0)
+ from x1 have ex_x: "!! x. x: H0
+ ==> EX y a. x = y + a (*) x0 & y : H"
+ by (unfold H0_def vs_sum_def lin_def) fast
- from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
- with ex_x [of "c (*) x1", OF ax1];
- show "h0 (c (*) x1) = c * (h0 x1)";
- proof (elim exE conjE);
- fix y1 y a1 a;
+ from x1 have ex_x1: "EX y1 a1. x1 = y1 + a1 (*) x0 & y1 : H"
+ by (unfold H0_def vs_sum_def lin_def) fast
+ with ex_x [of "c (*) x1", OF ax1]
+ show "h0 (c (*) x1) = c * (h0 x1)"
+ proof (elim exE conjE)
+ fix y1 y a1 a
assume y1: "x1 = y1 + a1 (*) x0" and y1': "y1 : H"
- and y: "c (*) x1 = y + a (*) x0" and y': "y : H";
+ and y: "c (*) x1 = y + a (*) x0" and y': "y : H"
- have ya: "c (*) y1 = y & c * a1 = a";
- proof (rule decomp_H0);
- show "c (*) y1 + (c * a1) (*) x0 = y + a (*) x0";
- by (simp! add: add: vs_add_mult_distrib1);
- show "c (*) y1 : H"; ..;
- qed;
+ have ya: "c (*) y1 = y & c * a1 = a"
+ proof (rule decomp_H0)
+ show "c (*) y1 + (c * a1) (*) x0 = y + a (*) x0"
+ by (simp! add: add: vs_add_mult_distrib1)
+ show "c (*) y1 : H" ..
+ qed
- have "h0 (c (*) x1) = h y + a * xi";
- by (rule h0_definite);
- also; have "... = h (c (*) 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 = h0 x1";
- by (rule h0_definite [RS sym]);
- finally; show ?thesis; .;
- qed;
- qed;
-qed;
+ have "h0 (c (*) x1) = h y + a * xi"
+ by (rule h0_definite)
+ also have "... = h (c (*) 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 = h0 x1"
+ by (rule h0_definite [RS sym])
+ finally show ?thesis .
+ qed
+ qed
+qed
text{* \medskip The linear extension $h_0$ of $h$
-is bounded by the seminorm $p$. *};
+is bounded by the seminorm $p$. *}
lemma h0_norm_pres:
"[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
@@ -245,105 +245,105 @@
H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= 00; is_vectorspace E;
is_subspace H E; is_seminorm E p; is_linearform H h; ALL y:H. h y <= p y;
ALL y:H. - p (y + x0) - h y <= xi & xi <= p (y + x0) - h y |]
- ==> ALL x:H0. h0 x <= p x";
-proof;
+ ==> ALL x:H0. h0 x <= p x"
+proof
assume h0_def:
"h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a (*) x0 & y:H
in (h y) + a * xi)"
and H0_def: "H0 == H + lin x0"
and vs: "x0 ~: H" "x0 : E" "x0 ~= 00" "is_vectorspace E"
"is_subspace H E" "is_seminorm E p" "is_linearform H h"
- and a: "ALL y:H. h y <= p y";
- presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
- presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
- fix x; assume "x : H0";
+ and a: "ALL y:H. h y <= p y"
+ presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi"
+ presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya"
+ fix x assume "x : H0"
have ex_x:
- "!! x. x : H0 ==> EX y a. x = y + a (*) x0 & y : H";
- by (unfold H0_def vs_sum_def lin_def) fast;
- have "EX y a. x = y + a (*) x0 & y : H";
- by (rule ex_x);
- thus "h0 x <= p x";
- proof (elim exE conjE);
- fix y a; assume x: "x = y + a (*) x0" and y: "y : H";
- have "h0 x = h y + a * xi";
- by (rule h0_definite);
+ "!! x. x : H0 ==> EX y a. x = y + a (*) x0 & y : H"
+ by (unfold H0_def vs_sum_def lin_def) fast
+ have "EX y a. x = y + a (*) x0 & y : H"
+ by (rule ex_x)
+ thus "h0 x <= p x"
+ proof (elim exE conjE)
+ fix y a assume x: "x = y + a (*) x0" and y: "y : H"
+ have "h0 x = h y + a * xi"
+ by (rule h0_definite)
txt{* Now we show
$h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$
- by case analysis on $a$. \label{linorder_linear_split}*};
+ by case analysis on $a$. \label{linorder_linear_split}*}
- also; have "... <= p (y + a (*) x0)";
- proof (rule linorder_linear_split);
+ also have "... <= p (y + a (*) x0)"
+ proof (rule linorder_linear_split)
- assume z: "a = (#0::real)";
- with vs y a; show ?thesis; by simp;
+ assume z: "a = #0"
+ with vs y a show ?thesis by simp
txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$
- taken as $y/a$: *};
+ taken as $y/a$: *}
- next;
- assume lz: "a < #0"; hence nz: "a ~= #0"; by simp;
- from a1;
- have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi";
- by (rule bspec) (simp!);
+ next
+ assume lz: "a < #0" hence nz: "a ~= #0" by simp
+ from a1
+ have "- p (rinv a (*) y + x0) - h (rinv a (*) y) <= xi"
+ by (rule bspec) (simp!)
txt {* The thesis for this case now follows by a short
- calculation. *};
+ calculation. *}
hence "a * xi
- <= a * (- p (rinv a (*) y + x0) - h (rinv a (*) y))";
- by (rule real_mult_less_le_anti [OF lz]);
- also; have "... = - a * (p (rinv a (*) y + x0))
- - a * (h (rinv a (*) y))";
- by (rule real_mult_diff_distrib);
- also; from lz vs y; have "- a * (p (rinv a (*) y + x0))
- = p (a (*) (rinv a (*) y + x0))";
- by (simp add: seminorm_abs_homogenous abs_minus_eqI2);
- also; from nz vs y; have "... = p (y + a (*) x0)";
- by (simp add: vs_add_mult_distrib1);
- also; from nz vs y; have "a * (h (rinv a (*) y)) = h y";
- by (simp add: linearform_mult [RS sym]);
- finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
+ <= a * (- p (rinv a (*) y + x0) - h (rinv a (*) y))"
+ by (rule real_mult_less_le_anti [OF lz])
+ also have "... = - a * (p (rinv a (*) y + x0))
+ - a * (h (rinv a (*) y))"
+ by (rule real_mult_diff_distrib)
+ also from lz vs y have "- a * (p (rinv a (*) y + x0))
+ = p (a (*) (rinv a (*) y + x0))"
+ by (simp add: seminorm_abs_homogenous abs_minus_eqI2)
+ also from nz vs y have "... = p (y + a (*) x0)"
+ by (simp add: vs_add_mult_distrib1)
+ also from nz vs y have "a * (h (rinv a (*) y)) = h y"
+ by (simp add: linearform_mult [RS sym])
+ finally have "a * xi <= p (y + a (*) x0) - h y" .
- hence "h y + a * xi <= h y + p (y + a (*) x0) - h y";
- by (simp add: real_add_left_cancel_le);
- thus ?thesis; by simp;
+ hence "h y + a * xi <= h y + p (y + a (*) x0) - h y"
+ by (simp add: real_add_left_cancel_le)
+ thus ?thesis by simp
txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$
- taken as $y/a$: *};
+ taken as $y/a$: *}
- next;
- assume gz: "#0 < a"; hence nz: "a ~= #0"; by simp;
- from a2;
- have "xi <= p (rinv a (*) y + x0) - h (rinv a (*) y)";
- by (rule bspec) (simp!);
+ next
+ assume gz: "#0 < a" hence nz: "a ~= #0" by simp
+ from a2
+ have "xi <= p (rinv a (*) y + x0) - h (rinv a (*) y)"
+ by (rule bspec) (simp!)
txt {* The thesis for this case follows by a short
- calculation: *};
+ calculation: *}
- with gz; have "a * xi
- <= a * (p (rinv a (*) y + x0) - h (rinv a (*) y))";
- by (rule real_mult_less_le_mono);
- also; have "... = a * p (rinv a (*) y + x0)
- - a * h (rinv a (*) y)";
- by (rule real_mult_diff_distrib2);
- also; from gz vs y;
+ with gz have "a * xi
+ <= a * (p (rinv a (*) y + x0) - h (rinv a (*) y))"
+ by (rule real_mult_less_le_mono)
+ also have "... = a * p (rinv a (*) y + x0)
+ - a * h (rinv a (*) y)"
+ by (rule real_mult_diff_distrib2)
+ also from gz vs y
have "a * p (rinv a (*) y + x0)
- = p (a (*) (rinv a (*) y + x0))";
- by (simp add: seminorm_abs_homogenous abs_eqI2);
- also; from nz vs y;
- have "... = p (y + a (*) x0)";
- by (simp add: vs_add_mult_distrib1);
- also; from nz vs y; have "a * h (rinv a (*) y) = h y";
- by (simp add: linearform_mult [RS sym]);
- finally; have "a * xi <= p (y + a (*) x0) - h y"; .;
+ = p (a (*) (rinv a (*) y + x0))"
+ by (simp add: seminorm_abs_homogenous abs_eqI2)
+ also from nz vs y
+ have "... = p (y + a (*) x0)"
+ by (simp add: vs_add_mult_distrib1)
+ also from nz vs y have "a * h (rinv a (*) y) = h y"
+ by (simp add: linearform_mult [RS sym])
+ finally have "a * xi <= p (y + a (*) x0) - h y" .
- hence "h y + a * xi <= h y + (p (y + a (*) x0) - h y)";
- by (simp add: real_add_left_cancel_le);
- thus ?thesis; by simp;
- qed;
- also; from x; have "... = p x"; by simp;
- finally; show ?thesis; .;
- qed;
-qed blast+;
+ hence "h y + a * xi <= h y + (p (y + a (*) x0) - h y)"
+ by (simp add: real_add_left_cancel_le)
+ thus ?thesis by simp
+ qed
+ also from x have "... = p x" by simp
+ finally show ?thesis .
+ qed
+qed blast+
-end;
\ No newline at end of file
+end
\ No newline at end of file