--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri Oct 29 20:18:34 1999 +0200
@@ -3,88 +3,89 @@
Author: Gertrud Bauer, TU Munich
*)
-header {* Extending a non-maximal function *};
+header {* Extending non-maximal functions *};
theory HahnBanachExtLemmas = FunctionNorm:;
text{* In this section the following context is presumed.
Let $E$ be a real vector space with a
-quasinorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear
+seminorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear
function on $F$. We consider a subspace $H$ of $E$ that is a
-superspace of $F$ and a linearform $h$ on $H$. $H$ is a not equal
+superspace of $F$ and a linear form $h$ on $H$. $H$ is a not equal
to $E$ and $x_0$ is an element in $E \backslash H$.
$H$ is extended to the direct sum $H_0 = H + \idt{lin}\ap x_0$, so for
any $x\in H_0$ the decomposition of $x = y + a \mult x$
with $y\in H$ is unique. $h_0$ is defined on $H_0$ by
-$h_0 x = h y + a \cdot \xi$ for some $\xi$.
+$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
-extension of $f$. It is a conclusion of the completenesss of the
-reals. To show
+text {* This lemma will be used to show the existence of a linear
+extension of $f$ (see page \pageref{ex-xi-use}).
+It is a consequence
+of the completeness of $\bbbR$. To show
\begin{matharray}{l}
-\exists \xi. \ap (\forall y\in F.\ap a\ap y \leq \xi) \land (\forall y\in F.\ap xi \leq b\ap y)
-\end{matharray}
+\Ex{\xi}{\All {y\in F}{a\ap y \leq \xi \land \xi \leq b\ap y}}
+\end{matharray}
it suffices to show that
-\begin{matharray}{l}
-\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v
-\end{matharray}
-*};
+\begin{matharray}{l} \All
+{u\in F}{\All {v\in F}{a\ap u \leq b \ap v}}
+\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) & (ALL y:F. xi <= b y)";
+ ==> 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\ap u.\ap u\in F\}$ has a supremum, if
- it is non-empty and if it has an upperbound. *};
+ it is non-empty and has an upper bound. *};
- let ?S = "{s::real. EX u:F. s = a u}";
+ let ?S = "{a u :: real | u. u:F}";
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 <0> : ?S"; by force;
thus "EX X. X : ?S"; ..;
- txt {* $b\ap \zero$ is an upperboud 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 <0>)";
proof (intro isUbI setleI ballI);
+ show "b <0> : 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"; ..;
+ from y; have "EX u:F. y = a u"; by fast;
thus "y <= b <0>";
proof;
- fix u; assume "u:F"; assume "y = a u";
+ fix u; assume "u:F";
+ assume "y = a u";
also; have "a u <= b <0>"; by (rule r) (simp!)+;
finally; show ?thesis; .;
qed;
- next;
- show "b <0> : UNIV"; by simp;
qed;
qed;
qed;
- thus "EX xi. (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)";
+ 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";
@@ -93,16 +94,16 @@
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"; by simp;
+ 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"; ..;
+ hence "EX u:F. au = a u"; by fast;
thus "au <= b y";
proof;
fix u; assume "u:F"; assume "au = a u";
@@ -115,25 +116,26 @@
qed;
qed;
-text{* The function $h_0$ is defined as a canonical linear extension
-of $h$ to $H_0$. *};
+text{* The function $h_0$ is defined as a
+$h_0\ap x = h\ap y + a\cdot \xi$ where $x = y + a\prod \xi$
+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
+ "[| 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;
+ H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H;
x0 : E; x0 ~= <0>; is_vectorspace E |]
==> is_linearform H0 h0";
proof -;
assume h0_def:
- "h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
+ "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 ~= <0>" "x0 : E" "is_vectorspace E";
+ and H0_def: "H0 == H + lin x0"
+ and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
+ "x0 ~= <0>" "x0 : E" "is_vectorspace E";
have h0: "is_vectorspace H0";
- proof (simp only: H0_def, rule vs_sum_vs);
+ proof (unfold H0_def, rule vs_sum_vs);
show "is_subspace (lin x0) E"; ..;
qed;
@@ -141,8 +143,7 @@
proof;
fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0";
- txt{* We now have to show that $h_0$ is linear
- w.~r.~t.~addition, i.~e.\
+ 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$. *};
@@ -150,13 +151,13 @@
by (rule vs_add_closed, rule h0);
from x1;
have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
- by (simp add: H0_def vs_sum_def lin_def) blast;
+ 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 (simp add: H0_def vs_sum_def lin_def) blast;
+ 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 (simp add: H0_def vs_sum_def lin_def) force;
+ 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";
@@ -167,7 +168,7 @@
and y: "x1 + x2 = y + a <*> x0" and y': "y : H";
have ya: "y1 + y2 = y & a1 + a2 = a";
- proof (rule decomp_H0);
+ proof (rule decomp_H0); txt{*\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"; ..;
@@ -179,7 +180,7 @@
by (simp add: ya);
also; from vs y1' y2';
have "... = h y1 + h y2 + a1 * xi + a2 * xi";
- by (simp add: linearform_add_linear [of H]
+ by (simp add: linearform_add [of H]
real_add_mult_distrib);
also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)";
by simp;
@@ -190,24 +191,23 @@
finally; show ?thesis; .;
qed;
- txt{* We further have to show that $h_0$ is linear
- w.~r.~t.~scalar multiplication,
+ 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 any real number $c$.
+ 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_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
- by (simp add: H0_def vs_sum_def lin_def) fast;
from x1; have ex_x: "!! x. x: H0
==> EX y a. x = y + a <*> x0 & y : H";
- by (simp add: H0_def vs_sum_def lin_def) fast;
- note ex_ax1 = ex_x [of "c <*> x1", OF ax1];
+ by (unfold H0_def vs_sum_def lin_def) fast;
- with ex_x1; show "h0 (c <*> x1) = c * (h0 x1)";
+ 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"
@@ -225,7 +225,7 @@
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_linear [of H]);
+ 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";
@@ -235,30 +235,31 @@
qed;
qed;
-text{* $h_0$ is bounded by the quasinorm $p$. *};
+text{* The linear extension $h_0$ of $h$
+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
+ "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
in h y + a * xi);
- H0 = H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E;
- is_subspace H E; is_quasinorm E p; is_linearform H h;
+ H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; 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)
& (ALL y:H. xi <= p (y + x0) - h y) |]
==> 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
+ "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 H0_def: "H0 == H + lin x0"
and vs: "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E"
- "is_subspace H E" "is_quasinorm E p" "is_linearform H h"
- and a: " ALL y:H. h y <= p y";
- presume a1: "ALL y:H. - p (y + x0) - h y <= xi";
- presume a2: "ALL y:H. xi <= p (y + x0) - h y";
+ "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";
have ex_x:
"!! x. x : H0 ==> EX y a. x = y + a <*> x0 & y : H";
- by (simp add: H0_def vs_sum_def lin_def) fast;
+ 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";
@@ -268,7 +269,7 @@
by (rule h0_definite);
txt{* Now we show
- $h\ap y + a \cdot xi\leq p\ap (y\plus a \mult x_0)$
+ $h\ap y + a \cdot \xi\leq p\ap (y\plus a \mult x_0)$
by case analysis on $a$. *};
also; have "... <= p (y + a <*> x0)";
@@ -277,17 +278,17 @@
assume z: "a = 0r";
with vs y a; show ?thesis; by simp;
- txt {* In the case $a < 0$ we use $a_1$ with $y$ taken as
- $y/a$. *};
+ txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$
+ taken as $y/a$: *};
next;
assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
from a1;
have "- p (rinv a <*> y + x0) - h (rinv a <*> y) <= xi";
- by (rule bspec)(simp!);
-
- txt {* The thesis now follows by a short calculation. *};
+ by (rule bspec) (simp!);
+ txt {* The thesis for this case now follows by a short
+ calculation. *};
hence "a * xi
<= a * (- p (rinv a <*> y + x0) - h (rinv a <*> y))";
by (rule real_mult_less_le_anti [OF lz]);
@@ -296,25 +297,28 @@
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: quasinorm_mult_distrib rabs_minus_eqI2);
+ by (simp add: seminorm_rabs_homogenous rabs_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_linear [RS sym]);
+ 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;
- txt {* In the case $a > 0$ we use $a_2$ with $y$ taken
- as $y/a$. *};
+ txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$
+ taken as $y/a$: *};
+
next;
assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
+ from a2;
have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
- by (rule bspec [OF a2]) (simp!);
+ by (rule bspec) (simp!);
- txt {* The thesis follows by a short calculation. *};
+ txt {* The thesis for this case follows by a short
+ calculation: *};
with gz; have "a * xi
<= a * (p (rinv a <*> y + x0) - h (rinv a <*> y))";
@@ -325,12 +329,12 @@
also; from gz vs y;
have "a * p (rinv a <*> y + x0)
= p (a <*> (rinv a <*> y + x0))";
- by (simp add: quasinorm_mult_distrib rabs_eqI2);
+ by (simp add: seminorm_rabs_homogenous rabs_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_linear [RS sym]);
+ 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)";
@@ -342,5 +346,4 @@
qed;
qed blast+;
-
end;
\ No newline at end of file