author | wenzelm |
Tue, 21 Sep 1999 17:31:20 +0200 | |
changeset 7566 | c5a3f980a7af |
parent 7535 | 599d3414b51d |
child 7567 | 62384a807775 |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/FunctionNorm.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
5 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
6 |
theory FunctionNorm = NormedSpace + FunctionOrder:; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
7 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
8 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
9 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
10 |
is_continous :: "['a set, 'a => real, 'a => real] => bool" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
11 |
"is_continous V norm f == (is_linearform V f |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
12 |
& (EX c. ALL x:V. rabs (f x) <= c * norm x))"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
13 |
|
7566 | 14 |
lemma lipschitz_continousI [intro]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
15 |
"[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
16 |
==> is_continous V norm f"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
17 |
proof (unfold is_continous_def, intro exI conjI ballI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
18 |
assume r: "!! x. x:V ==> rabs (f x) <= c * norm x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
19 |
fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
20 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
21 |
|
7566 | 22 |
lemma continous_linearform [intro!!]: "is_continous V norm f ==> is_linearform V f"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
23 |
by (unfold is_continous_def) force; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
24 |
|
7566 | 25 |
lemma continous_bounded [intro!!]: |
26 |
"is_continous V norm f ==> EX c. ALL x:V. rabs (f x) <= c * norm x"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
27 |
by (unfold is_continous_def) force; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
28 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
29 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
30 |
B:: "[ 'a set, 'a => real, 'a => real ] => real set" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
31 |
"B V norm f == {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm (x)))}"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
32 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
33 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
34 |
function_norm :: " ['a set, 'a => real, 'a => real] => real" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
35 |
"function_norm V norm f == |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
36 |
Sup UNIV (B V norm f)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
37 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
38 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
39 |
is_function_norm :: " ['a set, 'a => real, 'a => real] => real => bool" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
40 |
"is_function_norm V norm f fn == |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
41 |
is_Sup UNIV (B V norm f) fn"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
42 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
43 |
lemma B_not_empty: "0r : B V norm f"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
44 |
by (unfold B_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
45 |
|
7566 | 46 |
lemma ex_fnorm [intro!!]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
47 |
"[| is_normed_vectorspace V norm; is_continous V norm f|] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
48 |
==> is_function_norm V norm f (function_norm V norm f)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
49 |
proof (unfold function_norm_def is_function_norm_def is_continous_def Sup_def, elim conjE, |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
50 |
rule selectI2EX); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
51 |
assume "is_normed_vectorspace V norm"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
52 |
assume "is_linearform V f" and e: "EX c. ALL x:V. rabs (f x) <= c * norm x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
53 |
show "EX a. is_Sup UNIV (B V norm f) a"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
54 |
proof (unfold is_Sup_def, rule reals_complete); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
55 |
show "EX X. X : B V norm f"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
56 |
proof (intro exI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
57 |
show "0r : (B V norm f)"; by (unfold B_def, force); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
58 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
59 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
60 |
from e; show "EX Y. isUb UNIV (B V norm f) Y"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
61 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
62 |
fix c; assume a: "ALL x:V. rabs (f x) <= c * norm x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
63 |
def b == "max c 0r"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
64 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
65 |
show "EX Y. isUb UNIV (B V norm f) Y"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
66 |
proof (intro exI isUbI setleI ballI, unfold B_def, |
7566 | 67 |
elim CollectE disjE bexE conjE); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
68 |
fix x y; assume "x:V" "x ~= <0>" "y = rabs (f x) * rinv (norm x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
69 |
from a; have le: "rabs (f x) <= c * norm x"; ..; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
70 |
have "y = rabs (f x) * rinv (norm x)";.; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
71 |
also; from _ le; have "... <= c * norm x * rinv (norm x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
72 |
proof (rule real_mult_le_le_mono2); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
73 |
show "0r <= rinv (norm x)"; |
7566 | 74 |
proof (rule less_imp_le); |
75 |
show "0r < rinv (norm x)"; |
|
76 |
proof (rule real_rinv_gt_zero); |
|
77 |
show "0r < norm x"; ..; |
|
78 |
qed; |
|
79 |
qed; |
|
80 |
(*** or: by (rule less_imp_le, rule real_rinv_gt_zero, rule normed_vs_norm_gt_zero); ***) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
81 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
82 |
also; have "... = c * (norm x * rinv (norm x))"; by (rule real_mult_assoc); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
83 |
also; have "(norm x * rinv (norm x)) = 1r"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
84 |
proof (rule real_mult_inv_right); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
85 |
show "norm x ~= 0r"; |
7566 | 86 |
proof (rule not_sym); |
87 |
show "0r ~= norm x"; |
|
88 |
proof (rule lt_imp_not_eq); |
|
89 |
show "0r < norm x"; ..; |
|
90 |
qed; |
|
91 |
qed; |
|
92 |
(*** or: by (rule not_sym, rule lt_imp_not_eq, rule normed_vs_norm_gt_zero); ***) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
93 |
qed; |
7566 | 94 |
also; have "c * ... = c"; by (simp!); |
95 |
also; have "... <= b"; by (simp! add: le_max1); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
96 |
finally; show "y <= b"; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
97 |
next; |
7566 | 98 |
fix y; assume "y = 0r"; show "y <= b"; by (simp! add: le_max2); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
99 |
qed simp; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
100 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
101 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
102 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
103 |
|
7566 | 104 |
lemma fnorm_ge_zero [intro!!]: "[| is_continous V norm f; is_normed_vectorspace V norm|] |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
105 |
==> 0r <= function_norm V norm f"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
106 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
107 |
assume c: "is_continous V norm f" and n: "is_normed_vectorspace V norm"; |
7566 | 108 |
have "is_function_norm V norm f (function_norm V norm f)"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
109 |
hence s: "is_Sup UNIV (B V norm f) (function_norm V norm f)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
110 |
by (simp add: is_function_norm_def); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
111 |
show ?thesis; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
112 |
proof (unfold function_norm_def, rule sup_ub1); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
113 |
show "ALL x:(B V norm f). 0r <= x"; |
7566 | 114 |
proof (intro ballI, unfold B_def, elim CollectE bexE conjE disjE); |
115 |
fix x r; assume "x : V" "x ~= <0>" |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
116 |
"r = rabs (f x) * rinv (norm x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
117 |
show "0r <= r"; |
7566 | 118 |
proof (simp!, rule real_le_mult_order); |
119 |
show "0r <= rabs (f x)"; by (simp! only: rabs_ge_zero); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
120 |
show "0r <= rinv (norm x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
121 |
proof (rule less_imp_le); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
122 |
show "0r < rinv (norm x)"; |
7566 | 123 |
proof (rule real_rinv_gt_zero); |
124 |
show "0r < norm x"; ..; |
|
125 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
126 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
127 |
qed; |
7566 | 128 |
qed (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
129 |
from ex_fnorm [OF n c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; |
7566 | 130 |
by (simp! add: is_function_norm_def function_norm_def); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
131 |
show "0r : B V norm f"; by (rule B_not_empty); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
132 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
133 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
134 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
135 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
136 |
lemma norm_fx_le_norm_f_norm_x: |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
137 |
"[| is_normed_vectorspace V norm; x:V; is_continous V norm f |] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
138 |
==> rabs (f x) <= (function_norm V norm f) * norm x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
139 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
140 |
assume "is_normed_vectorspace V norm" "x:V" and c: "is_continous V norm f"; |
7566 | 141 |
have v: "is_vectorspace V"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
142 |
assume "x:V"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
143 |
show "?thesis"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
144 |
proof (rule case [of "x = <0>"]); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
145 |
assume "x ~= <0>"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
146 |
show "?thesis"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
147 |
proof -; |
7566 | 148 |
have n: "0r <= norm x"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
149 |
have le: "rabs (f x) * rinv (norm x) <= function_norm V norm f"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
150 |
proof (unfold function_norm_def, rule sup_ub); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
151 |
from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; |
7566 | 152 |
by (simp! add: is_function_norm_def function_norm_def); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
153 |
show "rabs (f x) * rinv (norm x) : B V norm f"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
154 |
by (unfold B_def, intro CollectI disjI2 bexI [of _ x] conjI, simp); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
155 |
qed; |
7566 | 156 |
have "rabs (f x) = rabs (f x) * 1r"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
157 |
also; have "1r = rinv (norm x) * norm x"; |
7566 | 158 |
proof (rule real_mult_inv_left [RS sym]); |
159 |
show "norm x ~= 0r"; |
|
160 |
proof (rule lt_imp_not_eq[RS not_sym]); |
|
161 |
show "0r < norm x"; ..; |
|
162 |
qed; |
|
163 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
164 |
also; have "rabs (f x) * ... = rabs (f x) * rinv (norm x) * norm x"; |
7566 | 165 |
by (simp! add: real_mult_assoc [of "rabs (f x)"]); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
166 |
also; have "rabs (f x) * rinv (norm x) * norm x <= function_norm V norm f * norm x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
167 |
by (rule real_mult_le_le_mono2 [OF n le]); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
168 |
finally; show "rabs (f x) <= function_norm V norm f * norm x"; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
169 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
170 |
next; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
171 |
assume "x = <0>"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
172 |
then; show "?thesis"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
173 |
proof -; |
7566 | 174 |
have "rabs (f x) = rabs (f <0>)"; by (simp!); |
175 |
also; from v continous_linearform; have "f <0> = 0r"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
176 |
also; note rabs_zero; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
177 |
also; have" 0r <= function_norm V norm f * norm x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
178 |
proof (rule real_le_mult_order); |
7566 | 179 |
show "0r <= function_norm V norm f"; ..; |
180 |
show "0r <= norm x"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
181 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
182 |
finally; show "rabs (f x) <= function_norm V norm f * norm x"; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
183 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
184 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
185 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
186 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
187 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
188 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
189 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
190 |
lemma fnorm_le_ub: |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
191 |
"[| is_normed_vectorspace V norm; is_continous V norm f; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
192 |
ALL x:V. rabs (f x) <= c * norm x; 0r <= c |] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
193 |
==> function_norm V norm f <= c"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
194 |
proof (unfold function_norm_def); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
195 |
assume "is_normed_vectorspace V norm"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
196 |
assume c: "is_continous V norm f"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
197 |
assume fb: "ALL x:V. rabs (f x) <= c * norm x" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
198 |
and "0r <= c"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
199 |
show "Sup UNIV (B V norm f) <= c"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
200 |
proof (rule ub_ge_sup); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
201 |
from ex_fnorm [OF _ c]; show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; |
7566 | 202 |
by (simp! add: is_function_norm_def function_norm_def); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
203 |
show "isUb UNIV (B V norm f) c"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
204 |
proof (intro isUbI setleI ballI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
205 |
fix y; assume "y: B V norm f"; |
7566 | 206 |
thus le: "y <= c"; |
207 |
proof (-, unfold B_def, elim CollectE disjE bexE); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
208 |
fix x; assume Px: "x ~= <0> & y = rabs (f x) * rinv (norm x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
209 |
assume x: "x : V"; |
7566 | 210 |
have lt: "0r < norm x"; by (simp! add: normed_vs_norm_gt_zero); |
211 |
||
212 |
have neq: "norm x ~= 0r"; |
|
213 |
proof (rule not_sym); |
|
214 |
from lt; show "0r ~= norm x"; |
|
215 |
by (simp! add: order_less_imp_not_eq); |
|
216 |
qed; |
|
217 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
218 |
from lt; have "0r < rinv (norm x)"; |
7566 | 219 |
by (simp! add: real_rinv_gt_zero); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
220 |
then; have inv_leq: "0r <= rinv (norm x)"; by (rule less_imp_le); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
221 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
222 |
from Px; have "y = rabs (f x) * rinv (norm x)"; ..; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
223 |
also; from inv_leq; have "... <= c * norm x * rinv (norm x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
224 |
proof (rule real_mult_le_le_mono2); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
225 |
from fb x; show "rabs (f x) <= c * norm x"; ..; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
226 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
227 |
also; have "... <= c"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
228 |
by (simp add: neq real_mult_assoc); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
229 |
finally; show ?thesis; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
230 |
next; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
231 |
assume "y = 0r"; |
7566 | 232 |
show "y <= c"; by (force!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
233 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
234 |
qed force; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
235 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
236 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
237 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
238 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
239 |
end; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
240 |