--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Fri Oct 08 16:40:27 1999 +0200
@@ -3,28 +3,29 @@
Author: Gertrud Bauer, TU Munich
*)
-(* The proof of two different versions of the Hahn-Banach theorem,
- following H. Heuser, Funktionalanalysis, p. 228 - 232.
-*)
+header {* The Hahn-Banach theorem *};
theory HahnBanach = HahnBanach_lemmas + HahnBanach_h0_lemmas:;
+text {*
+ The proof of two different versions of the Hahn-Banach theorem,
+ following \cite{Heuser}.
+*};
-section {* The Hahn-Banach theorem for general linear spaces,
- H. Heuser, Funktionalanalysis, p.231 *};
+subsection {* The Hahn-Banach theorem for general linear spaces *};
-text {* Every linear function f on a subspace of E, which is bounded by a quasinorm on E,
- can be extended norm preserving to a function on E *};
+text {* Every linear function f on a subspace of E, which is bounded by a
+ quasinorm on E, can be extended norm preserving to a function on E *};
theorem hahnbanach:
- "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
- ALL x:F. f x <= p x |]
+ "[| is_vectorspace E; is_subspace F E; is_quasinorm E p;
+ is_linearform F f; ALL x:F. f x <= p x |]
==> EX h. is_linearform E h
& (ALL x:F. h x = f x)
& (ALL x:E. h x <= p x)";
proof -;
- assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" "is_linearform F f"
- "ALL x:F. f x <= p x";
+ assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p"
+ "is_linearform F f" "ALL x:F. f x <= p x";
def M == "norm_pres_extensions E p F f";
@@ -36,13 +37,10 @@
qed;
qed (blast!)+;
+ subsubsect {* Existence of a supremum of the norm preserving functions *};
- sect {* Part I b of the proof of the Hahn-Banach Theorem,
- H. Heuser, Funktionalanalysis, p.231 *};
-
- txt {* Every chain of norm presenting functions has a supremum in M *};
-
- have "!! (c:: 'a graph set). c : chain M ==> EX x. x:c ==> (Union c) : M";
+ have "!! (c:: 'a graph set). c : chain M ==> EX x. x:c
+ ==> (Union c) : M";
proof -;
fix c; assume "c:chain M"; assume "EX x. x:c";
show "(Union c) : M";
@@ -53,7 +51,8 @@
& is_subspace H E
& is_subspace F H
& (graph F f <= graph H h)
- & (ALL x::'a:H. h x <= p x)" (is "EX (H::'a set) h::'a => real. ?Q H h");
+ & (ALL x::'a:H. h x <= p x)"
+ (is "EX (H::'a set) h::'a => real. ?Q H h");
proof (intro exI conjI);
let ?H = "domain (Union c)";
let ?h = "funct (Union c)";
@@ -101,7 +100,8 @@
thus ?thesis;
proof (elim exE conjE);
fix H h;
- assume "graph H h = g" "is_linearform (H::'a set) h" "is_subspace H E" "is_subspace F H"
+ assume "graph H h = g" "is_linearform (H::'a set) h"
+ "is_subspace H E" "is_subspace F H"
and h_ext: "(graph F f <= graph H h)"
and h_bound: "ALL x:H. h x <= p x";
@@ -110,203 +110,218 @@
have h: "is_vectorspace H"; ..;
have f: "is_vectorspace F"; ..;
- sect {* Part I a of the proof of the Hahn-Banach Theorem,
- H. Heuser, Funktionalanalysis, p.230 *};
-
- txt {* the maximal norm-preserving function is defined on whole E *};
+subsubsect {* The supremal norm-preserving function is defined on the
+ whole vectorspace *};
- have eq: "H = E";
- proof (rule classical);
-
- txt {* assume h is not defined on whole E *};
-
- assume "H ~= E";
- show ?thesis;
- proof -;
+have eq: "H = E";
+proof (rule classical);
- have "EX x:M. g <= x & g ~= x";
- proof -;
-
- txt {* h can be extended norm-preserving to H0 *};
+txt {* assume h is not defined on whole E *};
- have "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M";
- proof-;
- have "H <= E"; ..;
- hence "H < E"; ..;
- hence "EX x0:E. x0~:H"; by (rule set_less_imp_diff_not_empty);
- thus ?thesis;
- proof;
- fix x0; assume "x0:E" "x0~:H";
+ assume "H ~= E";
+ show ?thesis;
+ proof -;
- have x0: "x0 ~= <0>";
- proof (rule classical);
- presume "x0 = <0>";
- with h; have "x0:H"; by simp;
- thus ?thesis; by contradiction;
- qed force;
+ have "EX x:M. g <= x & g ~= x";
+ proof -;
- def H0 == "vectorspace_sum H (lin x0)";
- have "EX h0. g <= graph H0 h0 & g ~= graph H0 h0 & graph H0 h0 : M";
- proof -;
- from h; have xi: "EX xi. (ALL y:H. - p (y [+] x0) - h y <= xi)
- & (ALL y:H. xi <= p (y [+] x0) - h y)";
- proof (rule ex_xi);
- fix u v; assume "u:H" "v:H";
- show "- p (u [+] x0) - h u <= p (v [+] x0) - h v";
- proof (rule real_diff_ineq_swap);
+ txt {* h can be extended norm-preserving to H0 *};
- show "h v - h u <= p (v [+] x0) + p (u [+] x0)";
- proof -;
- from h; have "h v - h u = h (v [-] u)";
- by (simp! add: linearform_diff_linear);
- also; from h_bound; have "... <= p (v [-] u)"; by (simp!);
- also; have "v [-] u = x0 [+] [-] x0 [+] v [+] [-] u";
- by (simp! add: vs_add_minus_eq_diff);
- also; have "... = v [+] x0 [+] [-] (u [+] x0)"; by (simp!);
- also; have "... = (v [+] x0) [-] (u [+] x0)";
- by (simp! only: vs_add_minus_eq_diff);
- also; have "p ... <= p (v [+] x0) + p (u [+] x0)";
- by (rule quasinorm_diff_triangle_ineq) (simp!)+;
- finally; show ?thesis; .;
- qed;
- qed;
- qed;
-
- thus ?thesis;
- proof (elim exE, intro exI conjI);
- fix xi; assume a: "(ALL y:H. - p (y [+] x0) - h y <= xi) &
- (ALL y:H. xi <= p (y [+] x0) - h y)";
- def h0 == "%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H )
- in (h y) + a * xi";
+ have "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0
+ & graph H0 h0 : M";
+ proof-;
+ have "H <= E"; ..;
+ hence "H < E"; ..;
+ hence "EX x0:E. x0~:H";
+ by (rule set_less_imp_diff_not_empty);
+ thus ?thesis;
+ proof;
+ fix x0; assume "x0:E" "x0~:H";
- have "graph H h <= graph H0 h0";
- proof (rule graph_extI);
- fix t; assume "t:H";
- show "h t = h0 t";
- proof -;
- have "(@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
- by (rule decomp1, rule x0);
- thus ?thesis; by (simp! add: Let_def);
- qed;
- next;
- show "H <= H0";
- proof (rule subspace_subset);
- show "is_subspace H H0";
- proof (unfold H0_def, rule subspace_vs_sum1);
- show "is_vectorspace H"; ..;
- show "is_vectorspace (lin x0)"; ..;
- qed;
- qed;
- qed;
- thus "g <= graph H0 h0"; by (simp!);
-
- have "graph H h ~= graph H0 h0";
- proof;
- assume e: "graph H h = graph H0 h0";
- have "x0:H0";
- proof (unfold H0_def, rule vs_sumI);
- show "x0 = <0> [+] x0"; by (simp!);
- show "x0 :lin x0"; by (rule x_lin_x);
- from h; show "<0> : H"; ..;
- qed;
- hence "(x0, h0 x0) : graph H0 h0"; by (rule graphI);
- with e; have "(x0, h0 x0) : graph H h"; by simp;
- hence "x0 : H"; ..;
- thus "False"; by contradiction;
- qed;
- thus "g ~= graph H0 h0"; by (simp!);
-
- have "graph H0 h0 : norm_pres_extensions E p F f";
- proof (rule norm_pres_extensionI2);
+ have x0: "x0 ~= <0>";
+ proof (rule classical);
+ presume "x0 = <0>";
+ with h; have "x0:H"; by simp;
+ thus ?thesis; by contradiction;
+ qed force;
- show "is_linearform H0 h0";
- by (rule h0_lf, rule x0) (simp!)+;
-
- show "is_subspace H0 E";
- by (unfold H0_def, rule vs_sum_subspace, rule lin_subspace);
-
- show f_h0: "is_subspace F H0";
- proof (rule subspace_trans [of F H H0]);
- from h lin_vs; have "is_subspace H (vectorspace_sum H (lin x0))"; ..;
- thus "is_subspace H H0"; by (unfold H0_def);
- qed;
-
- show "graph F f <= graph H0 h0";
- proof (rule graph_extI);
- fix x; assume "x:F";
- show "f x = h0 x";
- proof -;
- have eq: "(@ (y, a). x = y [+] a [*] x0 & y : H) = (x, 0r)";
- by (rule decomp1, rule x0) (simp!)+;
+ def H0 == "vectorspace_sum H (lin x0)";
+ have "EX h0. g <= graph H0 h0 & g ~= graph H0 h0
+ & graph H0 h0 : M";
+ proof -;
+ from h;
+ have xi: "EX xi. (ALL y:H. - p (y [+] x0) - h y <= xi)
+ & (ALL y:H. xi <= p (y [+] x0) - h y)";
+ proof (rule ex_xi);
+ fix u v; assume "u:H" "v:H";
+ show "- p (u [+] x0) - h u <= p (v [+] x0) - h v";
+ proof (rule real_diff_ineq_swap);
- have "f x = h x"; ..;
- also; have " ... = h x + 0r * xi"; by simp;
- also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
- by (simp add: Let_def);
- also; from eq;
- have "... = (let (y,a) = @ (y,a). x = y [+] a [*] x0 & y : H
- in h y + a * xi)"; by simp;
- also; have "... = h0 x"; by (simp!);
- finally; show ?thesis; .;
- qed;
- next;
- from f_h0; show "F <= H0"; ..;
- qed;
-
- show "ALL x:H0. h0 x <= p x";
- by (rule h0_norm_pres, rule x0) (assumption | (simp!))+;
- qed;
- thus "graph H0 h0 : M"; by (simp!);
- qed;
- qed;
- thus ?thesis; ..;
+ show "h v - h u <= p (v [+] x0) + p (u [+] x0)";
+ proof -;
+ from h; have "h v - h u = h (v [-] u)";
+ by (simp! add: linearform_diff_linear);
+ also; from h_bound; have "... <= p (v [-] u)";
+ by (simp!);
+ also;
+ have "v [-] u = x0 [+] [-] x0 [+] v [+] [-] u";
+ by (unfold diff_def) (simp!);
+ also; have "... = v [+] x0 [+] [-] (u [+] x0)";
+ by (simp!);
+ also; have "... = (v [+] x0) [-] (u [+] x0)";
+ by (unfold diff_def) (simp!);
+ also; have "p ... <= p (v [+] x0) + p (u [+] x0)";
+ by (rule quasinorm_diff_triangle_ineq)
+ (simp!)+;
+ finally; show ?thesis; .;
qed;
qed;
+ qed;
+
+ thus ?thesis;
+ proof (elim exE, intro exI conjI);
+ fix xi;
+ assume a: "(ALL y:H. - p (y [+] x0) - h y <= xi)
+ & (ALL y:H. xi <= p (y [+] x0) - h y)";
+ def h0 ==
+ "%x. let (y,a) = @(y,a). (x = y [+] a [*] x0 & y:H )
+ in (h y) + a * xi";
- thus ?thesis;
- by (elim exE conjE, intro bexI conjI);
- qed;
- hence "~ (ALL x:M. g <= x --> g = x)"; by force;
- thus ?thesis; by contradiction;
- qed;
- qed;
+ have "graph H h <= graph H0 h0";
+ proof (rule graph_extI);
+ fix t; assume "t:H";
+ show "h t = h0 t";
+ proof -;
+ have "(@ (y, a). t = y [+] a [*] x0 & y : H)
+ = (t,0r)";
+ by (rule decomp1, rule x0);
+ thus ?thesis; by (simp! add: Let_def);
+ qed;
+ next;
+ show "H <= H0";
+ proof (rule subspace_subset);
+ show "is_subspace H H0";
+ proof (unfold H0_def, rule subspace_vs_sum1);
+ show "is_vectorspace H"; ..;
+ show "is_vectorspace (lin x0)"; ..;
+ qed;
+ qed;
+ qed;
+ thus "g <= graph H0 h0"; by (simp!);
+
+ have "graph H h ~= graph H0 h0";
+ proof;
+ assume e: "graph H h = graph H0 h0";
+ have "x0:H0";
+ proof (unfold H0_def, rule vs_sumI);
+ show "x0 = <0> [+] x0"; by (simp!);
+ show "x0 :lin x0"; by (rule x_lin_x);
+ from h; show "<0> : H"; ..;
+ qed;
+ hence "(x0, h0 x0) : graph H0 h0"; by (rule graphI);
+ with e; have "(x0, h0 x0) : graph H h"; by simp;
+ hence "x0 : H"; ..;
+ thus "False"; by contradiction;
+ qed;
+ thus "g ~= graph H0 h0"; by (simp!);
+
+ have "graph H0 h0 : norm_pres_extensions E p F f";
+ proof (rule norm_pres_extensionI2);
+
+ show "is_linearform H0 h0";
+ by (rule h0_lf, rule x0) (simp!)+;
+
+ show "is_subspace H0 E";
+ by (unfold H0_def, rule vs_sum_subspace,
+ rule lin_subspace);
- show "is_linearform E h & (ALL x:F. h x = f x) & (ALL x:E. h x <= p x)";
- proof (intro conjI);
- from eq; show "is_linearform E h"; by (simp!);
- show "ALL x:F. h x = f x";
- proof (intro ballI, rule sym);
- fix x; assume "x:F"; show "f x = h x "; ..;
+ show f_h0: "is_subspace F H0";
+ proof (rule subspace_trans [of F H H0]);
+ from h lin_vs;
+ have "is_subspace H (vectorspace_sum H (lin x0))";
+ ..;
+ thus "is_subspace H H0"; by (unfold H0_def);
+ qed;
+
+ show "graph F f <= graph H0 h0";
+ proof (rule graph_extI);
+ fix x; assume "x:F";
+ show "f x = h0 x";
+ proof -;
+ have eq:
+ "(@(y, a). x = y [+] a [*] x0 & y : H)
+ = (x, 0r)";
+ by (rule decomp1, rule x0) (simp!)+;
+
+ have "f x = h x"; ..;
+ also; have " ... = h x + 0r * xi"; by simp;
+ also; have
+ "... = (let (y,a) = (x, 0r) in h y + a * xi)";
+ by (simp add: Let_def);
+ also; from eq; have
+ "... = (let (y,a) = @ (y,a).
+ x = y [+] a [*] x0 & y : H
+ in h y + a * xi)"; by simp;
+ also; have "... = h0 x"; by (simp!);
+ finally; show ?thesis; .;
+ qed;
+ next;
+ from f_h0; show "F <= H0"; ..;
+ qed;
+
+ show "ALL x:H0. h0 x <= p x";
+ by (rule h0_norm_pres, rule x0)
+ (assumption | (simp!))+;
+ qed;
+ thus "graph H0 h0 : M"; by (simp!);
+ qed;
qed;
- from eq; show "ALL x:E. h x <= p x"; by (force!);
+ thus ?thesis; ..;
qed;
- qed;
- qed;
+ qed;
+
+ thus ?thesis;
+ by (elim exE conjE, intro bexI conjI);
+ qed;
+ hence "~ (ALL x:M. g <= x --> g = x)"; by force;
+ thus ?thesis; by contradiction;
qed;
+qed;
+
+show "is_linearform E h & (ALL x:F. h x = f x)
+ & (ALL x:E. h x <= p x)";
+proof (intro conjI);
+ from eq; show "is_linearform E h"; by (simp!);
+ show "ALL x:F. h x = f x";
+ proof (intro ballI, rule sym);
+ fix x; assume "x:F"; show "f x = h x "; ..;
+ qed;
+ from eq; show "ALL x:E. h x <= p x"; by (force!);
+qed;
+qed;
+qed;
+qed;
qed;
-
-section {* Part I (for real linear spaces) of the proof of the Hahn-banach Theorem,
- H. Heuser, Funktionalanalysis, p.229 *};
-
-text {* Alternative Formulation of the theorem *};
+subsection {* Alternative formulation of the theorem *};
theorem rabs_hahnbanach:
- "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; is_linearform F f;
- ALL x:F. rabs (f x) <= p x |]
- ==> EX g. is_linearform E g
- & (ALL x:F. g x = f x)
- & (ALL x:E. rabs (g x) <= p x)";
+ "[| is_vectorspace E; is_subspace F E; is_quasinorm E p;
+ is_linearform F f; ALL x:F. rabs (f x) <= p x |]
+ ==> EX g. is_linearform E g
+ & (ALL x:F. g x = f x)
+ & (ALL x:E. rabs (g x) <= p x)";
proof -;
-
- assume e: "is_vectorspace E" and "is_subspace F E" "is_quasinorm E p" "is_linearform F f"
- "ALL x:F. rabs (f x) <= p x";
+ assume e: "is_vectorspace E" "is_subspace F E" "is_quasinorm E p"
+ "is_linearform F f" "ALL x:F. rabs (f x) <= p x";
have "ALL x:F. f x <= p x"; by (rule rabs_ineq [RS iffD1]);
- hence "EX g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. g x <= p x)";
+ hence "EX g. is_linearform E g & (ALL x:F. g x = f x)
+ & (ALL x:E. g x <= p x)";
by (simp! only: hahnbanach);
thus ?thesis;
proof (elim exE conjE);
- fix g; assume "is_linearform E g" "ALL x:F. g x = f x" "ALL x:E. g x <= p x";
+ fix g; assume "is_linearform E g" "ALL x:F. g x = f x"
+ "ALL x:E. g x <= p x";
show ?thesis;
proof (intro exI conjI)+;
from e; show "ALL x:E. rabs (g x) <= p x";
@@ -316,8 +331,7 @@
qed;
-section {* The Hahn-Banach theorem for normd spaces,
- H. Heuser, Funktionalanalysis, p.232 *};
+subsection {* The Hahn-Banach theorem for normed spaces *};
text {* Every continous linear function f on a subspace of E,
can be extended to a continous function on E with the same norm *};
@@ -330,9 +344,7 @@
& (ALL x:F. g x = f x)
& function_norm E norm g = function_norm F norm f"
(concl is "EX g::'a=>real. ?P g");
-
proof -;
-
assume a: "is_normed_vectorspace E norm";
assume b: "is_subspace F E" "is_linearform F f";
assume c: "is_continous F norm f";
@@ -341,7 +353,8 @@
def p == "%x::'a. (function_norm F norm f) * norm x";
- let ?P' = "%g. is_linearform E g & (ALL x:F. g x = f x) & (ALL x:E. rabs (g x) <= p x)";
+ let ?P' = "%g. is_linearform E g & (ALL x:F. g x = f x)
+ & (ALL x:E. rabs (g x) <= p x)";
have q: "is_quasinorm E p";
proof;
@@ -355,9 +368,12 @@
show "p (a [*] x) = (rabs a) * (p x)";
proof -;
- have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)"; by (simp!);
- also; have "norm (a [*] x) = rabs a * norm x"; by (rule normed_vs_norm_mult_distrib);
- also; have "(function_norm F norm f) * ... = rabs a * ((function_norm F norm f) * norm x)";
+ have "p (a [*] x) = (function_norm F norm f) * norm (a [*] x)";
+ by (simp!);
+ also; have "norm (a [*] x) = rabs a * norm x";
+ by (rule normed_vs_norm_mult_distrib);
+ also; have "(function_norm F norm f) * ...
+ = rabs a * ((function_norm F norm f) * norm x)";
by (simp! only: real_mult_left_commute);
also; have "... = (rabs a) * (p x)"; by (simp!);
finally; show ?thesis; .;
@@ -365,13 +381,15 @@
show "p (x [+] y) <= p x + p y";
proof -;
- have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)"; by (simp!);
- also; have "... <= (function_norm F norm f) * (norm x + norm y)";
+ have "p (x [+] y) = (function_norm F norm f) * norm (x [+] y)";
+ by (simp!);
+ also; have "... <= (function_norm F norm f) * (norm x + norm y)";
proof (rule real_mult_le_le_mono1);
from _ f; show "0r <= function_norm F norm f"; ..;
show "norm (x [+] y) <= norm x + norm y"; ..;
qed;
- also; have "... = (function_norm F norm f) * (norm x) + (function_norm F norm f) * (norm y)";
+ also; have "... = (function_norm F norm f) * (norm x)
+ + (function_norm F norm f) * (norm y)";
by (simp! only: real_add_mult_distrib2);
finally; show ?thesis; by (simp!);
qed;
@@ -380,7 +398,8 @@
have "ALL x:F. rabs (f x) <= p x";
proof;
fix x; assume "x:F";
- from f; show "rabs (f x) <= p x"; by (simp! add: norm_fx_le_norm_f_norm_x);
+ from f; show "rabs (f x) <= p x";
+ by (simp! add: norm_fx_le_norm_f_norm_x);
qed;
with e b q; have "EX g. ?P' g";
@@ -389,7 +408,8 @@
thus "?thesis";
proof (elim exE conjE, intro exI conjI);
fix g;
- assume "is_linearform E g" and a: "ALL x:F. g x = f x" and "ALL x:E. rabs (g x) <= p x";
+ assume "is_linearform E g" and a: "ALL x:F. g x = f x"
+ and "ALL x:E. rabs (g x) <= p x";
show ce: "is_continous E norm g";
proof (rule lipschitz_continousI);
fix x; assume "x:E";
@@ -398,7 +418,8 @@
qed;
show "function_norm E norm g = function_norm F norm f";
proof (rule order_antisym);
- from _ ce; show "function_norm E norm g <= function_norm F norm f";
+ from _ ce;
+ show "function_norm E norm g <= function_norm F norm f";
proof (rule fnorm_le_ub);
show "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";
proof;
@@ -415,14 +436,16 @@
fix x; assume "x : F";
from a; have "g x = f x"; ..;
hence "rabs (f x) = rabs (g x)"; by simp;
- also; from _ _ ce; have "... <= function_norm E norm g * norm x";
+ also; from _ _ ce;
+ have "... <= function_norm E norm g * norm x";
proof (rule norm_fx_le_norm_f_norm_x);
show "x : E";
proof (rule subsetD);
show "F <= E"; ..;
qed;
qed;
- finally; show "rabs (f x) <= function_norm E norm g * norm x"; .;
+ finally;
+ show "rabs (f x) <= function_norm E norm g * norm x"; .;
qed;
from _ e; show "is_normed_vectorspace F norm"; ..;
from ce; show "0r <= function_norm E norm g"; ..;
@@ -431,6 +454,4 @@
qed;
qed;
-
-end;
-
+end;
\ No newline at end of file