18 $\Union c = \idt{graph}\ap H\ap h$. |
16 $\Union c = \idt{graph}\ap H\ap h$. |
19 We will show some properties about the limit function $h$, |
17 We will show some properties about the limit function $h$, |
20 i.e.\ the supremum of the chain $c$. |
18 i.e.\ the supremum of the chain $c$. |
21 *} |
19 *} |
22 |
20 |
23 |
|
24 text{* Let $c$ be a chain of norm-preserving extensions of the |
21 text{* Let $c$ be a chain of norm-preserving extensions of the |
25 function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$. |
22 function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$. |
26 Every element in $H$ is member of |
23 Every element in $H$ is member of |
27 one of the elements of the chain. *} |
24 one of the elements of the chain. *} |
28 |
25 |
29 lemma some_H'h't: |
26 lemma some_H'h't: |
30 "[| M = norm_pres_extensions E p F f; c \<in> chain M; |
27 "[| M = norm_pres_extensions E p F f; c \<in> chain M; |
31 graph H h = Union c; x \\<in> H |] |
28 graph H h = \<Union> c; x \<in> H |] |
32 ==> \\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h' |
29 ==> \<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h' |
33 & is_linearform H' h' & is_subspace H' E |
30 \<and> is_linearform H' h' \<and> is_subspace H' E |
34 & is_subspace F H' & graph F f \\<subseteq> graph H' h' |
31 \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' |
35 & (\\<forall>x \\<in> H'. h' x \\<le> p x)" |
32 \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
36 proof - |
33 proof - |
37 assume m: "M = norm_pres_extensions E p F f" and "c \<in> chain M" |
34 assume m: "M = norm_pres_extensions E p F f" and "c \<in> chain M" |
38 and u: "graph H h = Union c" "x \\<in> H" |
35 and u: "graph H h = \<Union> c" "x \<in> H" |
39 |
36 |
40 have h: "(x, h x) \<in> graph H h" .. |
37 have h: "(x, h x) \<in> graph H h" .. |
41 with u have "(x, h x) \<in> Union c" by simp |
38 with u have "(x, h x) \<in> \<Union> c" by simp |
42 hence ex1: "\<exists> g \\<in> c. (x, h x) \<in> g" |
39 hence ex1: "\<exists>g \<in> c. (x, h x) \<in> g" |
43 by (simp only: Union_iff) |
40 by (simp only: Union_iff) |
44 thus ?thesis |
41 thus ?thesis |
45 proof (elim bexE) |
42 proof (elim bexE) |
46 fix g assume g: "g \\<in> c" "(x, h x) \\<in> g" |
43 fix g assume g: "g \<in> c" "(x, h x) \<in> g" |
47 have "c \\<subseteq> M" by (rule chainD2) |
44 have "c \<subseteq> M" by (rule chainD2) |
48 hence "g \\<in> M" .. |
45 hence "g \<in> M" .. |
49 hence "g \<in> norm_pres_extensions E p F f" by (simp only: m) |
46 hence "g \<in> norm_pres_extensions E p F f" by (simp only: m) |
50 hence "\<exists> H' h'. graph H' h' = g |
47 hence "\<exists>H' h'. graph H' h' = g |
51 & is_linearform H' h' |
48 \<and> is_linearform H' h' |
52 & is_subspace H' E |
49 \<and> is_subspace H' E |
53 & is_subspace F H' |
50 \<and> is_subspace F H' |
54 & graph F f \\<subseteq> graph H' h' |
51 \<and> graph F f \<subseteq> graph H' h' |
55 & (\<forall>x \\<in> H'. h' x \\<le> p x)" |
52 \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
56 by (rule norm_pres_extension_D) |
53 by (rule norm_pres_extension_D) |
57 thus ?thesis |
54 thus ?thesis |
58 proof (elim exE conjE) |
55 proof (elim exE conjE) |
59 fix H' h' |
56 fix H' h' |
60 assume "graph H' h' = g" "is_linearform H' h'" |
57 assume "graph H' h' = g" "is_linearform H' h'" |
61 "is_subspace H' E" "is_subspace F H'" |
58 "is_subspace H' E" "is_subspace F H'" |
62 "graph F f \\<subseteq> graph H' h'" "\<forall>x \\<in> H'. h' x \\<le> p x" |
59 "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" |
63 show ?thesis |
60 show ?thesis |
64 proof (intro exI conjI) |
61 proof (intro exI conjI) |
65 show "graph H' h' \<in> c" by (simp!) |
62 show "graph H' h' \<in> c" by (simp!) |
66 show "(x, h x) \<in> graph H' h'" by (simp!) |
63 show "(x, h x) \<in> graph H' h'" by (simp!) |
67 qed |
64 qed |
76 the domain $H'$ of some function $h'$, such that $h$ extends $h'$. |
73 the domain $H'$ of some function $h'$, such that $h$ extends $h'$. |
77 *} |
74 *} |
78 |
75 |
79 lemma some_H'h': |
76 lemma some_H'h': |
80 "[| M = norm_pres_extensions E p F f; c \<in> chain M; |
77 "[| M = norm_pres_extensions E p F f; c \<in> chain M; |
81 graph H h = Union c; x \\<in> H |] |
78 graph H h = \<Union> c; x \<in> H |] |
82 ==> \<exists> H' h'. x \\<in> H' & graph H' h' \\<subseteq> graph H h |
79 ==> \<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h |
83 & is_linearform H' h' & is_subspace H' E & is_subspace F H' |
80 \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H' |
84 & graph F f \\<subseteq> graph H' h' & (\<forall>x \\<in> H'. h' x \\<le> p x)" |
81 \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
85 proof - |
82 proof - |
86 assume "M = norm_pres_extensions E p F f" and cM: "c \<in> chain M" |
83 assume "M = norm_pres_extensions E p F f" and cM: "c \<in> chain M" |
87 and u: "graph H h = Union c" "x \\<in> H" |
84 and u: "graph H h = \<Union> c" "x \<in> H" |
88 |
85 |
89 have "\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h' |
86 have "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h' |
90 & is_linearform H' h' & is_subspace H' E |
87 \<and> is_linearform H' h' \<and> is_subspace H' E |
91 & is_subspace F H' & graph F f \\<subseteq> graph H' h' |
88 \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' |
92 & (\<forall> x \\<in> H'. h' x \\<le> p x)" |
89 \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
93 by (rule some_H'h't) |
90 by (rule some_H'h't) |
94 thus ?thesis |
91 thus ?thesis |
95 proof (elim exE conjE) |
92 proof (elim exE conjE) |
96 fix H' h' assume "(x, h x) \<in> graph H' h'" "graph H' h' \<in> c" |
93 fix H' h' assume "(x, h x) \<in> graph H' h'" "graph H' h' \<in> c" |
97 "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" |
94 "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" |
98 "graph F f \\<subseteq> graph H' h'" "\<forall> x\<in>H'. h' x \\<le> p x" |
95 "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" |
99 show ?thesis |
96 show ?thesis |
100 proof (intro exI conjI) |
97 proof (intro exI conjI) |
101 show "x\<in>H'" by (rule graphD1) |
98 show "x \<in> H'" by (rule graphD1) |
102 from cM u show "graph H' h' \\<subseteq> graph H h" |
99 from cM u show "graph H' h' \<subseteq> graph H h" |
103 by (simp! only: chain_ball_Union_upper) |
100 by (simp! only: chain_ball_Union_upper) |
104 qed |
101 qed |
105 qed |
102 qed |
106 qed |
103 qed |
107 |
104 |
109 text{* \medskip Any two elements $x$ and $y$ in the domain $H$ of the |
106 text{* \medskip Any two elements $x$ and $y$ in the domain $H$ of the |
110 supremum function $h$ are both in the domain $H'$ of some function |
107 supremum function $h$ are both in the domain $H'$ of some function |
111 $h'$, such that $h$ extends $h'$. *} |
108 $h'$, such that $h$ extends $h'$. *} |
112 |
109 |
113 lemma some_H'h'2: |
110 lemma some_H'h'2: |
114 "[| M = norm_pres_extensions E p F f; c\<in> chain M; |
111 "[| M = norm_pres_extensions E p F f; c \<in> chain M; |
115 graph H h = Union c; x\<in>H; y\<in>H |] |
112 graph H h = \<Union> c; x \<in> H; y \<in> H |] |
116 ==> \<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h |
113 ==> \<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h |
117 & is_linearform H' h' & is_subspace H' E & is_subspace F H' |
114 \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H' |
118 & graph F f \\<subseteq> graph H' h' & (\<forall> x\<in>H'. h' x \\<le> p x)" |
115 \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
119 proof - |
116 proof - |
120 assume "M = norm_pres_extensions E p F f" "c\<in> chain M" |
117 assume "M = norm_pres_extensions E p F f" "c \<in> chain M" |
121 "graph H h = Union c" "x\<in>H" "y\<in>H" |
118 "graph H h = \<Union> c" "x \<in> H" "y \<in> H" |
122 |
119 |
123 txt {* $x$ is in the domain $H'$ of some function $h'$, |
120 txt {* $x$ is in the domain $H'$ of some function $h'$, |
124 such that $h$ extends $h'$. *} |
121 such that $h$ extends $h'$. *} |
125 |
122 |
126 have e1: "\<exists> H' h'. graph H' h' \<in> c & (x, h x) \<in> graph H' h' |
123 have e1: "\<exists>H' h'. graph H' h' \<in> c \<and> (x, h x) \<in> graph H' h' |
127 & is_linearform H' h' & is_subspace H' E |
124 \<and> is_linearform H' h' \<and> is_subspace H' E |
128 & is_subspace F H' & graph F f \\<subseteq> graph H' h' |
125 \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' |
129 & (\<forall> x\<in>H'. h' x \\<le> p x)" |
126 \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
130 by (rule some_H'h't) |
127 by (rule some_H'h't) |
131 |
128 |
132 txt {* $y$ is in the domain $H''$ of some function $h''$, |
129 txt {* $y$ is in the domain $H''$ of some function $h''$, |
133 such that $h$ extends $h''$. *} |
130 such that $h$ extends $h''$. *} |
134 |
131 |
135 have e2: "\<exists> H'' h''. graph H'' h'' \<in> c & (y, h y) \<in> graph H'' h'' |
132 have e2: "\<exists>H'' h''. graph H'' h'' \<in> c \<and> (y, h y) \<in> graph H'' h'' |
136 & is_linearform H'' h'' & is_subspace H'' E |
133 \<and> is_linearform H'' h'' \<and> is_subspace H'' E |
137 & is_subspace F H'' & graph F f \\<subseteq> graph H'' h'' |
134 \<and> is_subspace F H'' \<and> graph F f \<subseteq> graph H'' h'' |
138 & (\<forall> x\<in>H''. h'' x \\<le> p x)" |
135 \<and> (\<forall>x \<in> H''. h'' x \<le> p x)" |
139 by (rule some_H'h't) |
136 by (rule some_H'h't) |
140 |
137 |
141 from e1 e2 show ?thesis |
138 from e1 e2 show ?thesis |
142 proof (elim exE conjE) |
139 proof (elim exE conjE) |
143 fix H' h' assume "(y, h y)\<in> graph H' h'" "graph H' h' \<in> c" |
140 fix H' h' assume "(y, h y) \<in> graph H' h'" "graph H' h' \<in> c" |
144 "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" |
141 "is_linearform H' h'" "is_subspace H' E" "is_subspace F H'" |
145 "graph F f \\<subseteq> graph H' h'" "\<forall> x\<in>H'. h' x \\<le> p x" |
142 "graph F f \<subseteq> graph H' h'" "\<forall>x \<in> H'. h' x \<le> p x" |
146 |
143 |
147 fix H'' h'' assume "(x, h x)\<in> graph H'' h''" "graph H'' h'' \<in> c" |
144 fix H'' h'' assume "(x, h x) \<in> graph H'' h''" "graph H'' h'' \<in> c" |
148 "is_linearform H'' h''" "is_subspace H'' E" "is_subspace F H''" |
145 "is_linearform H'' h''" "is_subspace H'' E" "is_subspace F H''" |
149 "graph F f \\<subseteq> graph H'' h''" "\<forall> x\<in>H''. h'' x \\<le> p x" |
146 "graph F f \<subseteq> graph H'' h''" "\<forall>x \<in> H''. h'' x \<le> p x" |
150 |
147 |
151 txt {* Since both $h'$ and $h''$ are elements of the chain, |
148 txt {* Since both $h'$ and $h''$ are elements of the chain, |
152 $h''$ is an extension of $h'$ or vice versa. Thus both |
149 $h''$ is an extension of $h'$ or vice versa. Thus both |
153 $x$ and $y$ are contained in the greater one. \label{cases1}*} |
150 $x$ and $y$ are contained in the greater one. \label{cases1}*} |
154 |
151 |
155 have "graph H'' h'' \\<subseteq> graph H' h' | graph H' h' \\<subseteq> graph H'' h''" |
152 have "graph H'' h'' \<subseteq> graph H' h' | graph H' h' \<subseteq> graph H'' h''" |
156 (is "?case1 | ?case2") |
153 (is "?case1 | ?case2") |
157 by (rule chainD) |
154 by (rule chainD) |
158 thus ?thesis |
155 thus ?thesis |
159 proof |
156 proof |
160 assume ?case1 |
157 assume ?case1 |
161 show ?thesis |
158 show ?thesis |
162 proof (intro exI conjI) |
159 proof (intro exI conjI) |
163 have "(x, h x) \<in> graph H'' h''" . |
160 have "(x, h x) \<in> graph H'' h''" . |
164 also have "... \\<subseteq> graph H' h'" . |
161 also have "... \<subseteq> graph H' h'" . |
165 finally have xh\<in> "(x, h x)\<in> graph H' h'" . |
162 finally have xh:"(x, h x) \<in> graph H' h'" . |
166 thus x: "x\<in>H'" .. |
163 thus x: "x \<in> H'" .. |
167 show y: "y\<in>H'" .. |
164 show y: "y \<in> H'" .. |
168 show "graph H' h' \\<subseteq> graph H h" |
165 show "graph H' h' \<subseteq> graph H h" |
169 by (simp! only: chain_ball_Union_upper) |
166 by (simp! only: chain_ball_Union_upper) |
170 qed |
167 qed |
171 next |
168 next |
172 assume ?case2 |
169 assume ?case2 |
173 show ?thesis |
170 show ?thesis |
174 proof (intro exI conjI) |
171 proof (intro exI conjI) |
175 show x: "x\<in>H''" .. |
172 show x: "x \<in> H''" .. |
176 have "(y, h y) \<in> graph H' h'" by (simp!) |
173 have "(y, h y) \<in> graph H' h'" by (simp!) |
177 also have "... \\<subseteq> graph H'' h''" . |
174 also have "... \<subseteq> graph H'' h''" . |
178 finally have yh: "(y, h y)\<in> graph H'' h''" . |
175 finally have yh: "(y, h y) \<in> graph H'' h''" . |
179 thus y: "y\<in>H''" .. |
176 thus y: "y \<in> H''" .. |
180 show "graph H'' h'' \\<subseteq> graph H h" |
177 show "graph H'' h'' \<subseteq> graph H h" |
181 by (simp! only: chain_ball_Union_upper) |
178 by (simp! only: chain_ball_Union_upper) |
182 qed |
179 qed |
183 qed |
180 qed |
184 qed |
181 qed |
185 qed |
182 qed |
186 |
183 |
187 |
184 |
188 |
185 |
189 text{* \medskip The relation induced by the graph of the supremum |
186 text{* \medskip The relation induced by the graph of the supremum |
190 of a chain $c$ is definite, i.~e.~it is the graph of a function. *} |
187 of a chain $c$ is definite, i.~e.~t is the graph of a function. *} |
191 |
188 |
192 lemma sup_definite: |
189 lemma sup_definite: |
193 "[| M == norm_pres_extensions E p F f; c \<in> chain M; |
190 "[| M == norm_pres_extensions E p F f; c \<in> chain M; |
194 (x, y) \<in> Union c; (x, z) \<in> Union c |] ==> z = y" |
191 (x, y) \<in> \<Union> c; (x, z) \<in> \<Union> c |] ==> z = y" |
195 proof - |
192 proof - |
196 assume "c\<in>chain M" "M == norm_pres_extensions E p F f" |
193 assume "c \<in> chain M" "M == norm_pres_extensions E p F f" |
197 "(x, y) \<in> Union c" "(x, z) \<in> Union c" |
194 "(x, y) \<in> \<Union> c" "(x, z) \<in> \<Union> c" |
198 thus ?thesis |
195 thus ?thesis |
199 proof (elim UnionE chainE2) |
196 proof (elim UnionE chainE2) |
200 |
197 |
201 txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$ |
198 txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$ |
202 they are members of some graphs $G_1$ and $G_2$, resp., such that |
199 they are members of some graphs $G_1$ and $G_2$, resp., such that |
203 both $G_1$ and $G_2$ are members of $c$.*} |
200 both $G_1$ and $G_2$ are members of $c$.*} |
204 |
201 |
205 fix G1 G2 assume |
202 fix G1 G2 assume |
206 "(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \\<subseteq> M" |
203 "(x, y) \<in> G1" "G1 \<in> c" "(x, z) \<in> G2" "G2 \<in> c" "c \<subseteq> M" |
207 |
204 |
208 have "G1 \<in> M" .. |
205 have "G1 \<in> M" .. |
209 hence e1: "\<exists> H1 h1. graph H1 h1 = G1" |
206 hence e1: "\<exists> H1 h1. graph H1 h1 = G1" |
210 by (force! dest: norm_pres_extension_D) |
207 by (force! dest: norm_pres_extension_D) |
211 have "G2 \<in> M" .. |
208 have "G2 \<in> M" .. |
245 preserving extensions. Furthermore, $h$ is an extension of $h'$ so |
242 preserving extensions. Furthermore, $h$ is an extension of $h'$ so |
246 the function values of $x$ are identical for $h'$ and $h$. Finally, the |
243 the function values of $x$ are identical for $h'$ and $h$. Finally, the |
247 function $h'$ is linear by construction of $M$. *} |
244 function $h'$ is linear by construction of $M$. *} |
248 |
245 |
249 lemma sup_lf: |
246 lemma sup_lf: |
250 "[| M = norm_pres_extensions E p F f; c\<in> chain M; |
247 "[| M = norm_pres_extensions E p F f; c \<in> chain M; |
251 graph H h = Union c |] ==> is_linearform H h" |
248 graph H h = \<Union> c |] ==> is_linearform H h" |
252 proof - |
249 proof - |
253 assume "M = norm_pres_extensions E p F f" "c\<in> chain M" |
250 assume "M = norm_pres_extensions E p F f" "c \<in> chain M" |
254 "graph H h = Union c" |
251 "graph H h = \<Union> c" |
255 |
252 |
256 show "is_linearform H h" |
253 show "is_linearform H h" |
257 proof |
254 proof |
258 fix x y assume "x \<in> H" "y \<in> H" |
255 fix x y assume "x \<in> H" "y \<in> H" |
259 have "\<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h |
256 have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h |
260 & is_linearform H' h' & is_subspace H' E |
257 \<and> is_linearform H' h' \<and> is_subspace H' E |
261 & is_subspace F H' & graph F f \\<subseteq> graph H' h' |
258 \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' |
262 & (\<forall> x\<in>H'. h' x \\<le> p x)" |
259 \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
263 by (rule some_H'h'2) |
260 by (rule some_H'h'2) |
264 |
261 |
265 txt {* We have to show that $h$ is additive. *} |
262 txt {* We have to show that $h$ is additive. *} |
266 |
263 |
267 thus "h (x + y) = h x + h y" |
264 thus "h (x + y) = h x + h y" |
268 proof (elim exE conjE) |
265 proof (elim exE conjE) |
269 fix H' h' assume "x\<in>H'" "y\<in>H'" |
266 fix H' h' assume "x \<in> H'" "y \<in> H'" |
270 and b: "graph H' h' \\<subseteq> graph H h" |
267 and b: "graph H' h' \<subseteq> graph H h" |
271 and "is_linearform H' h'" "is_subspace H' E" |
268 and "is_linearform H' h'" "is_subspace H' E" |
272 have "h' (x + y) = h' x + h' y" |
269 have "h' (x + y) = h' x + h' y" |
273 by (rule linearform_add) |
270 by (rule linearform_add) |
274 also have "h' x = h x" .. |
271 also have "h' x = h x" .. |
275 also have "h' y = h y" .. |
272 also have "h' y = h y" .. |
277 with b have "h' (x + y) = h (x + y)" .. |
274 with b have "h' (x + y) = h (x + y)" .. |
278 finally show ?thesis . |
275 finally show ?thesis . |
279 qed |
276 qed |
280 next |
277 next |
281 fix a x assume "x \<in> H" |
278 fix a x assume "x \<in> H" |
282 have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h |
279 have "\<exists> H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h |
283 & is_linearform H' h' & is_subspace H' E |
280 \<and> is_linearform H' h' \<and> is_subspace H' E |
284 & is_subspace F H' & graph F f \\<subseteq> graph H' h' |
281 \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' |
285 & (\<forall> x\<in>H'. h' x \\<le> p x)" |
282 \<and> (\<forall> x \<in> H'. h' x \<le> p x)" |
286 by (rule some_H'h') |
283 by (rule some_H'h') |
287 |
284 |
288 txt{* We have to show that $h$ is multiplicative. *} |
285 txt{* We have to show that $h$ is multiplicative. *} |
289 |
286 |
290 thus "h (a \<prod> x) = a * h x" |
287 thus "h (a \<cdot> x) = a * h x" |
291 proof (elim exE conjE) |
288 proof (elim exE conjE) |
292 fix H' h' assume "x\<in>H'" |
289 fix H' h' assume "x \<in> H'" |
293 and b: "graph H' h' \\<subseteq> graph H h" |
290 and b: "graph H' h' \<subseteq> graph H h" |
294 and "is_linearform H' h'" "is_subspace H' E" |
291 and "is_linearform H' h'" "is_subspace H' E" |
295 have "h' (a \<prod> x) = a * h' x" |
292 have "h' (a \<cdot> x) = a * h' x" |
296 by (rule linearform_mult) |
293 by (rule linearform_mult) |
297 also have "h' x = h x" .. |
294 also have "h' x = h x" .. |
298 also have "a \<prod> x \<in> H'" .. |
295 also have "a \<cdot> x \<in> H'" .. |
299 with b have "h' (a \<prod> x) = h (a \<prod> x)" .. |
296 with b have "h' (a \<cdot> x) = h (a \<cdot> x)" .. |
300 finally show ?thesis . |
297 finally show ?thesis . |
301 qed |
298 qed |
302 qed |
299 qed |
303 qed |
300 qed |
304 |
301 |
307 since every element of the chain is an extension |
304 since every element of the chain is an extension |
308 of $f$ and the supremum is an extension |
305 of $f$ and the supremum is an extension |
309 for every element of the chain.*} |
306 for every element of the chain.*} |
310 |
307 |
311 lemma sup_ext: |
308 lemma sup_ext: |
312 "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c; |
309 "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f; |
313 graph H h = Union c |] ==> graph F f \\<subseteq> graph H h" |
310 c \<in> chain M; \<exists>x. x \<in> c |] ==> graph F f \<subseteq> graph H h" |
314 proof - |
311 proof - |
315 assume "M = norm_pres_extensions E p F f" "c\<in> chain M" |
312 assume "M = norm_pres_extensions E p F f" "c \<in> chain M" |
316 "graph H h = Union c" |
313 "graph H h = \<Union> c" |
317 assume "\<exists> x. x\<in>c" |
314 assume "\<exists>x. x \<in> c" |
318 thus ?thesis |
315 thus ?thesis |
319 proof |
316 proof |
320 fix x assume "x\<in>c" |
317 fix x assume "x \<in> c" |
321 have "c \\<subseteq> M" by (rule chainD2) |
318 have "c \<subseteq> M" by (rule chainD2) |
322 hence "x\<in>M" .. |
319 hence "x \<in> M" .. |
323 hence "x \<in> norm_pres_extensions E p F f" by (simp!) |
320 hence "x \<in> norm_pres_extensions E p F f" by (simp!) |
324 |
321 |
325 hence "\<exists> G g. graph G g = x |
322 hence "\<exists>G g. graph G g = x |
326 & is_linearform G g |
323 \<and> is_linearform G g |
327 & is_subspace G E |
324 \<and> is_subspace G E |
328 & is_subspace F G |
325 \<and> is_subspace F G |
329 & graph F f \\<subseteq> graph G g |
326 \<and> graph F f \<subseteq> graph G g |
330 & (\<forall> x\<in>G. g x \\<le> p x)" |
327 \<and> (\<forall>x \<in> G. g x \<le> p x)" |
331 by (simp! add: norm_pres_extension_D) |
328 by (simp! add: norm_pres_extension_D) |
332 |
329 |
333 thus ?thesis |
330 thus ?thesis |
334 proof (elim exE conjE) |
331 proof (elim exE conjE) |
335 fix G g assume "graph F f \\<subseteq> graph G g" |
332 fix G g assume "graph F f \<subseteq> graph G g" |
336 also assume "graph G g = x" |
333 also assume "graph G g = x" |
337 also have "... \<in> c" . |
334 also have "... \<in> c" . |
338 hence "x \\<subseteq> Union c" by fast |
335 hence "x \<subseteq> \<Union> c" by fast |
339 also have [RS sym]: "graph H h = Union c" . |
336 also have [RS sym]: "graph H h = \<Union> c" . |
340 finally show ?thesis . |
337 finally show ?thesis . |
341 qed |
338 qed |
342 qed |
339 qed |
343 qed |
340 qed |
344 |
341 |
346 since $F$ is a subset of $H$. The existence of the $\zero$ element in |
343 since $F$ is a subset of $H$. The existence of the $\zero$ element in |
347 $F$ and the closure properties follow from the fact that $F$ is a |
344 $F$ and the closure properties follow from the fact that $F$ is a |
348 vector space. *} |
345 vector space. *} |
349 |
346 |
350 lemma sup_supF: |
347 lemma sup_supF: |
351 "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c; |
348 "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f; |
352 graph H h = Union c; is_subspace F E; is_vectorspace E |] |
349 c \<in> chain M; \<exists>x. x \<in> c; is_subspace F E; is_vectorspace E |] |
353 ==> is_subspace F H" |
350 ==> is_subspace F H" |
354 proof - |
351 proof - |
355 assume "M = norm_pres_extensions E p F f" "c\<in> chain M" "\<exists> x. x\<in>c" |
352 assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c" |
356 "graph H h = Union c" "is_subspace F E" "is_vectorspace E" |
353 "graph H h = \<Union> c" "is_subspace F E" "is_vectorspace E" |
357 |
354 |
358 show ?thesis |
355 show ?thesis |
359 proof |
356 proof |
360 show "\<zero> \<in> F" .. |
357 show "0 \<in> F" .. |
361 show "F \\<subseteq> H" |
358 show "F \<subseteq> H" |
362 proof (rule graph_extD2) |
359 proof (rule graph_extD2) |
363 show "graph F f \\<subseteq> graph H h" |
360 show "graph F f \<subseteq> graph H h" |
364 by (rule sup_ext) |
361 by (rule sup_ext) |
365 qed |
362 qed |
366 show "\<forall> x\<in>F. \<forall> y\<in>F. x + y \<in> F" |
363 show "\<forall>x \<in> F. \<forall>y \<in> F. x + y \<in> F" |
367 proof (intro ballI) |
364 proof (intro ballI) |
368 fix x y assume "x\<in>F" "y\<in>F" |
365 fix x y assume "x \<in> F" "y \<in> F" |
369 show "x + y \<in> F" by (simp!) |
366 show "x + y \<in> F" by (simp!) |
370 qed |
367 qed |
371 show "\<forall> x\<in>F. \<forall> a. a \<prod> x \<in> F" |
368 show "\<forall>x \<in> F. \<forall>a. a \<cdot> x \<in> F" |
372 proof (intro ballI allI) |
369 proof (intro ballI allI) |
373 fix x a assume "x\<in>F" |
370 fix x a assume "x\<in>F" |
374 show "a \<prod> x \<in> F" by (simp!) |
371 show "a \<cdot> x \<in> F" by (simp!) |
375 qed |
372 qed |
376 qed |
373 qed |
377 qed |
374 qed |
378 |
375 |
379 text{* \medskip The domain $H$ of the limit function is a subspace |
376 text{* \medskip The domain $H$ of the limit function is a subspace |
380 of $E$. *} |
377 of $E$. *} |
381 |
378 |
382 lemma sup_subE: |
379 lemma sup_subE: |
383 "[| M = norm_pres_extensions E p F f; c\<in> chain M; \<exists> x. x\<in>c; |
380 "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f; |
384 graph H h = Union c; is_subspace F E; is_vectorspace E |] |
381 c \<in> chain M; \<exists>x. x \<in> c; is_subspace F E; is_vectorspace E |] |
385 ==> is_subspace H E" |
382 ==> is_subspace H E" |
386 proof - |
383 proof - |
387 assume "M = norm_pres_extensions E p F f" "c\<in> chain M" "\<exists> x. x\<in>c" |
384 assume "M = norm_pres_extensions E p F f" "c \<in> chain M" "\<exists>x. x \<in> c" |
388 "graph H h = Union c" "is_subspace F E" "is_vectorspace E" |
385 "graph H h = \<Union> c" "is_subspace F E" "is_vectorspace E" |
389 show ?thesis |
386 show ?thesis |
390 proof |
387 proof |
391 |
388 |
392 txt {* The $\zero$ element is in $H$, as $F$ is a subset |
389 txt {* The $\zero$ element is in $H$, as $F$ is a subset |
393 of $H$: *} |
390 of $H$: *} |
394 |
391 |
395 have "\<zero> \<in> F" .. |
392 have "0 \<in> F" .. |
396 also have "is_subspace F H" by (rule sup_supF) |
393 also have "is_subspace F H" by (rule sup_supF) |
397 hence "F \\<subseteq> H" .. |
394 hence "F \<subseteq> H" .. |
398 finally show "\<zero> \<in> H" . |
395 finally show "0 \<in> H" . |
399 |
396 |
400 txt{* $H$ is a subset of $E$: *} |
397 txt{* $H$ is a subset of $E$: *} |
401 |
398 |
402 show "H \\<subseteq> E" |
399 show "H \<subseteq> E" |
403 proof |
400 proof |
404 fix x assume "x\<in>H" |
401 fix x assume "x \<in> H" |
405 have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h |
402 have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h |
406 & is_linearform H' h' & is_subspace H' E |
403 \<and> is_linearform H' h' \<and> is_subspace H' E |
407 & is_subspace F H' & graph F f \\<subseteq> graph H' h' |
404 \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' |
408 & (\<forall> x\<in>H'. h' x \\<le> p x)" |
405 \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
409 by (rule some_H'h') |
406 by (rule some_H'h') |
410 thus "x\<in>E" |
407 thus "x \<in> E" |
411 proof (elim exE conjE) |
408 proof (elim exE conjE) |
412 fix H' h' assume "x\<in>H'" "is_subspace H' E" |
409 fix H' h' assume "x \<in> H'" "is_subspace H' E" |
413 have "H' \\<subseteq> E" .. |
410 have "H' \<subseteq> E" .. |
414 thus "x\<in>E" .. |
411 thus "x \<in> E" .. |
415 qed |
412 qed |
416 qed |
413 qed |
417 |
414 |
418 txt{* $H$ is closed under addition: *} |
415 txt{* $H$ is closed under addition: *} |
419 |
416 |
420 show "\<forall> x\<in>H. \<forall> y\<in>H. x + y \<in> H" |
417 show "\<forall>x \<in> H. \<forall>y \<in> H. x + y \<in> H" |
421 proof (intro ballI) |
418 proof (intro ballI) |
422 fix x y assume "x\<in>H" "y\<in>H" |
419 fix x y assume "x \<in> H" "y \<in> H" |
423 have "\<exists> H' h'. x\<in>H' & y\<in>H' & graph H' h' \\<subseteq> graph H h |
420 have "\<exists>H' h'. x \<in> H' \<and> y \<in> H' \<and> graph H' h' \<subseteq> graph H h |
424 & is_linearform H' h' & is_subspace H' E |
421 \<and> is_linearform H' h' \<and> is_subspace H' E |
425 & is_subspace F H' & graph F f \\<subseteq> graph H' h' |
422 \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' |
426 & (\<forall> x\<in>H'. h' x \\<le> p x)" |
423 \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
427 by (rule some_H'h'2) |
424 by (rule some_H'h'2) |
428 thus "x + y \<in> H" |
425 thus "x + y \<in> H" |
429 proof (elim exE conjE) |
426 proof (elim exE conjE) |
430 fix H' h' |
427 fix H' h' |
431 assume "x\<in>H'" "y\<in>H'" "is_subspace H' E" |
428 assume "x \<in> H'" "y \<in> H'" "is_subspace H' E" |
432 "graph H' h' \\<subseteq> graph H h" |
429 "graph H' h' \<subseteq> graph H h" |
433 have "x + y \<in> H'" .. |
430 have "x + y \<in> H'" .. |
434 also have "H' \\<subseteq> H" .. |
431 also have "H' \<subseteq> H" .. |
435 finally show ?thesis . |
432 finally show ?thesis . |
436 qed |
433 qed |
437 qed |
434 qed |
438 |
435 |
439 txt{* $H$ is closed under scalar multiplication: *} |
436 txt{* $H$ is closed under scalar multiplication: *} |
440 |
437 |
441 show "\<forall> x\<in>H. \<forall> a. a \<prod> x \<in> H" |
438 show "\<forall>x \<in> H. \<forall>a. a \<cdot> x \<in> H" |
442 proof (intro ballI allI) |
439 proof (intro ballI allI) |
443 fix x a assume "x\<in>H" |
440 fix x a assume "x \<in> H" |
444 have "\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h |
441 have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h |
445 & is_linearform H' h' & is_subspace H' E |
442 \<and> is_linearform H' h' \<and> is_subspace H' E |
446 & is_subspace F H' & graph F f \\<subseteq> graph H' h' |
443 \<and> is_subspace F H' \<and> graph F f \<subseteq> graph H' h' |
447 & (\<forall> x\<in>H'. h' x \\<le> p x)" |
444 \<and> (\<forall>x \<in> H'. h' x \<le> p x)" |
448 by (rule some_H'h') |
445 by (rule some_H'h') |
449 thus "a \<prod> x \<in> H" |
446 thus "a \<cdot> x \<in> H" |
450 proof (elim exE conjE) |
447 proof (elim exE conjE) |
451 fix H' h' |
448 fix H' h' |
452 assume "x\<in>H'" "is_subspace H' E" "graph H' h' \\<subseteq> graph H h" |
449 assume "x \<in> H'" "is_subspace H' E" "graph H' h' \<subseteq> graph H h" |
453 have "a \<prod> x \<in> H'" .. |
450 have "a \<cdot> x \<in> H'" .. |
454 also have "H' \\<subseteq> H" .. |
451 also have "H' \<subseteq> H" .. |
455 finally show ?thesis . |
452 finally show ?thesis . |
456 qed |
453 qed |
457 qed |
454 qed |
458 qed |
455 qed |
459 qed |
456 qed |
461 text {* \medskip The limit function is bounded by |
458 text {* \medskip The limit function is bounded by |
462 the norm $p$ as well, since all elements in the chain are |
459 the norm $p$ as well, since all elements in the chain are |
463 bounded by $p$. |
460 bounded by $p$. |
464 *} |
461 *} |
465 |
462 |
466 lemma sup_norm_pres\<in> |
463 lemma sup_norm_pres: |
467 "[| M = norm_pres_extensions E p F f; c\<in> chain M; |
464 "[| graph H h = \<Union> c; M = norm_pres_extensions E p F f; c \<in> chain M |] |
468 graph H h = Union c |] ==> \<forall> x\<in>H. h x \\<le> p x" |
465 ==> \<forall> x \<in> H. h x \<le> p x" |
469 proof |
466 proof |
470 assume "M = norm_pres_extensions E p F f" "c\<in> chain M" |
467 assume "M = norm_pres_extensions E p F f" "c \<in> chain M" |
471 "graph H h = Union c" |
468 "graph H h = \<Union> c" |
472 fix x assume "x\<in>H" |
469 fix x assume "x \<in> H" |
473 have "\\<exists> H' h'. x\<in>H' & graph H' h' \\<subseteq> graph H h |
470 have "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h |
474 & is_linearform H' h' & is_subspace H' E & is_subspace F H' |
471 \<and> is_linearform H' h' \<and> is_subspace H' E \<and> is_subspace F H' |
475 & graph F f \\<subseteq> graph H' h' & (\<forall> x\<in>H'. h' x \\<le> p x)" |
472 \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall> x \<in> H'. h' x \<le> p x)" |
476 by (rule some_H'h') |
473 by (rule some_H'h') |
477 thus "h x \\<le> p x" |
474 thus "h x \<le> p x" |
478 proof (elim exE conjE) |
475 proof (elim exE conjE) |
479 fix H' h' |
476 fix H' h' |
480 assume "x\<in> H'" "graph H' h' \\<subseteq> graph H h" |
477 assume "x \<in> H'" "graph H' h' \<subseteq> graph H h" |
481 and a: "\<forall> x\<in> H'. h' x \\<le> p x" |
478 and a: "\<forall>x \<in> H'. h' x \<le> p x" |
482 have [RS sym]: "h' x = h x" .. |
479 have [RS sym]: "h' x = h x" .. |
483 also from a have "h' x \\<le> p x " .. |
480 also from a have "h' x \<le> p x " .. |
484 finally show ?thesis . |
481 finally show ?thesis . |
485 qed |
482 qed |
486 qed |
483 qed |
487 |
484 |
488 |
485 |
497 *} |
494 *} |
498 |
495 |
499 lemma abs_ineq_iff: |
496 lemma abs_ineq_iff: |
500 "[| is_subspace H E; is_vectorspace E; is_seminorm E p; |
497 "[| is_subspace H E; is_vectorspace E; is_seminorm E p; |
501 is_linearform H h |] |
498 is_linearform H h |] |
502 ==> (\<forall> x\<in>H. abs (h x) \\<le> p x) = (\<forall> x\<in>H. h x \\<le> p x)" |
499 ==> (\<forall>x \<in> H. |h x| \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" |
503 (concl is "?L = ?R") |
500 (concl is "?L = ?R") |
504 proof - |
501 proof - |
505 assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p" |
502 assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p" |
506 "is_linearform H h" |
503 "is_linearform H h" |
507 have h: "is_vectorspace H" .. |
504 have h: "is_vectorspace H" .. |
508 show ?thesis |
505 show ?thesis |
509 proof |
506 proof |
510 assume l: ?L |
507 assume l: ?L |
511 show ?R |
508 show ?R |
512 proof |
509 proof |
513 fix x assume x: "x\<in>H" |
510 fix x assume x: "x \<in> H" |
514 have "h x \\<le> abs (h x)" by (rule abs_ge_self) |
511 have "h x \<le> |h x|" by (rule abs_ge_self) |
515 also from l have "... \\<le> p x" .. |
512 also from l have "... \<le> p x" .. |
516 finally show "h x \\<le> p x" . |
513 finally show "h x \<le> p x" . |
517 qed |
514 qed |
518 next |
515 next |
519 assume r: ?R |
516 assume r: ?R |
520 show ?L |
517 show ?L |
521 proof |
518 proof |
522 fix x assume "x\<in>H" |
519 fix x assume "x \<in> H" |
523 show "!! a b \<in>: real. [| - a \\<le> b; b \\<le> a |] ==> abs b \\<le> a" |
520 show "!! a b :: real. [| - a \<le> b; b \<le> a |] ==> |b| \<le> a" |
524 by arith |
521 by arith |
525 show "- p x \\<le> h x" |
522 show "- p x \<le> h x" |
526 proof (rule real_minus_le) |
523 proof (rule real_minus_le) |
527 from h have "- h x = h (- x)" |
524 from h have "- h x = h (- x)" |
528 by (rule linearform_neg [RS sym]) |
525 by (rule linearform_neg [RS sym]) |
529 also from r have "... \\<le> p (- x)" by (simp!) |
526 also from r have "... \<le> p (- x)" by (simp!) |
530 also have "... = p x" |
527 also have "... = p x" |
531 by (rule seminorm_minus [OF _ subspace_subsetD]) |
528 by (rule seminorm_minus [OF _ subspace_subsetD]) |
532 finally show "- h x \\<le> p x" . |
529 finally show "- h x \<le> p x" . |
533 qed |
530 qed |
534 from r show "h x \\<le> p x" .. |
531 from r show "h x \<le> p x" .. |
535 qed |
532 qed |
536 qed |
533 qed |
537 qed |
534 qed |
538 |
535 |
539 |
536 |