1 (* Title: HOL/Multivariate_Analysis/Extension.thy |
|
2 Authors: LC Paulson, based on material from HOL Light |
|
3 *) |
|
4 |
|
5 section \<open>Continuous extensions of functions: Urysohn's lemma, Dugundji extension theorem, Tietze\<close> |
|
6 |
|
7 theory Extension |
|
8 imports Convex_Euclidean_Space |
|
9 begin |
|
10 |
|
11 subsection\<open>Partitions of unity subordinate to locally finite open coverings\<close> |
|
12 |
|
13 text\<open>A difference from HOL Light: all summations over infinite sets equal zero, |
|
14 so the "support" must be made explicit in the summation below!\<close> |
|
15 |
|
16 proposition subordinate_partition_of_unity: |
|
17 fixes S :: "'a :: euclidean_space set" |
|
18 assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T" |
|
19 and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}" |
|
20 obtains F :: "['a set, 'a] \<Rightarrow> real" |
|
21 where "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x \<in> S. 0 \<le> F U x)" |
|
22 and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0" |
|
23 and "\<And>x. x \<in> S \<Longrightarrow> supp_setsum (\<lambda>W. F W x) \<C> = 1" |
|
24 and "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}" |
|
25 proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W") |
|
26 case True |
|
27 then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis |
|
28 then show ?thesis |
|
29 apply (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that) |
|
30 apply (auto simp: continuous_on_const supp_setsum_def support_on_def) |
|
31 done |
|
32 next |
|
33 case False |
|
34 have nonneg: "0 \<le> supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>" for x |
|
35 by (simp add: supp_setsum_def setsum_nonneg) |
|
36 have sd_pos: "0 < setdist {x} (S - V)" if "V \<in> \<C>" "x \<in> S" "x \<in> V" for V x |
|
37 proof - |
|
38 have "closedin (subtopology euclidean S) (S - V)" |
|
39 by (simp add: Diff_Diff_Int Diff_subset closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>) |
|
40 with that False setdist_eq_0_closedin [of S "S-V" x] setdist_pos_le [of "{x}" "S - V"] |
|
41 show ?thesis |
|
42 by (simp add: order_class.order.order_iff_strict) |
|
43 qed |
|
44 have ss_pos: "0 < supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>" if "x \<in> S" for x |
|
45 proof - |
|
46 obtain U where "U \<in> \<C>" "x \<in> U" using \<open>x \<in> S\<close> \<open>S \<subseteq> \<Union>\<C>\<close> |
|
47 by blast |
|
48 obtain V where "open V" "x \<in> V" "finite {U \<in> \<C>. U \<inter> V \<noteq> {}}" |
|
49 using \<open>x \<in> S\<close> fin by blast |
|
50 then have *: "finite {A \<in> \<C>. \<not> S \<subseteq> A \<and> x \<notin> closure (S - A)}" |
|
51 using closure_def that by (blast intro: rev_finite_subset) |
|
52 have "x \<notin> closure (S - U)" |
|
53 by (metis \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> less_irrefl sd_pos setdist_eq_0_sing_1 that) |
|
54 then show ?thesis |
|
55 apply (simp add: setdist_eq_0_sing_1 supp_setsum_def support_on_def) |
|
56 apply (rule ordered_comm_monoid_add_class.setsum_pos2 [OF *, of U]) |
|
57 using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> False |
|
58 apply (auto simp: setdist_pos_le sd_pos that) |
|
59 done |
|
60 qed |
|
61 define F where |
|
62 "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C> |
|
63 else 0" |
|
64 show ?thesis |
|
65 proof (rule_tac F = F in that) |
|
66 have "continuous_on S (F U)" if "U \<in> \<C>" for U |
|
67 proof - |
|
68 have *: "continuous_on S (\<lambda>x. supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>)" |
|
69 proof (clarsimp simp add: continuous_on_eq_continuous_within) |
|
70 fix x assume "x \<in> S" |
|
71 then obtain X where "open X" and x: "x \<in> S \<inter> X" and finX: "finite {U \<in> \<C>. U \<inter> X \<noteq> {}}" |
|
72 using assms by blast |
|
73 then have OSX: "openin (subtopology euclidean S) (S \<inter> X)" by blast |
|
74 have sumeq: "\<And>x. x \<in> S \<inter> X \<Longrightarrow> |
|
75 (\<Sum>V | V \<in> \<C> \<and> V \<inter> X \<noteq> {}. setdist {x} (S - V)) |
|
76 = supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>" |
|
77 apply (simp add: supp_setsum_def) |
|
78 apply (rule setsum.mono_neutral_right [OF finX]) |
|
79 apply (auto simp: setdist_eq_0_sing_1 support_on_def subset_iff) |
|
80 apply (meson DiffI closure_subset disjoint_iff_not_equal subsetCE) |
|
81 done |
|
82 show "continuous (at x within S) (\<lambda>x. supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>)" |
|
83 apply (rule continuous_transform_within_openin |
|
84 [where f = "\<lambda>x. (setsum (\<lambda>V. setdist {x} (S - V)) {V \<in> \<C>. V \<inter> X \<noteq> {}})" |
|
85 and S ="S \<inter> X"]) |
|
86 apply (rule continuous_intros continuous_at_setdist continuous_at_imp_continuous_at_within OSX x)+ |
|
87 apply (simp add: sumeq) |
|
88 done |
|
89 qed |
|
90 show ?thesis |
|
91 apply (simp add: F_def) |
|
92 apply (rule continuous_intros *)+ |
|
93 using ss_pos apply force |
|
94 done |
|
95 qed |
|
96 moreover have "\<lbrakk>U \<in> \<C>; x \<in> S\<rbrakk> \<Longrightarrow> 0 \<le> F U x" for U x |
|
97 using nonneg [of x] by (simp add: F_def divide_simps setdist_pos_le) |
|
98 ultimately show "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x\<in>S. 0 \<le> F U x)" |
|
99 by metis |
|
100 next |
|
101 show "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0" |
|
102 by (simp add: setdist_eq_0_sing_1 closure_def F_def) |
|
103 next |
|
104 show "supp_setsum (\<lambda>W. F W x) \<C> = 1" if "x \<in> S" for x |
|
105 using that ss_pos [OF that] |
|
106 by (simp add: F_def divide_simps supp_setsum_divide_distrib [symmetric]) |
|
107 next |
|
108 show "\<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}" if "x \<in> S" for x |
|
109 using fin [OF that] that |
|
110 by (fastforce simp: setdist_eq_0_sing_1 closure_def F_def elim!: rev_finite_subset) |
|
111 qed |
|
112 qed |
|
113 |
|
114 |
|
115 subsection\<open>Urysohn's lemma (for Euclidean spaces, where the proof is easy using distances)\<close> |
|
116 |
|
117 lemma Urysohn_both_ne: |
|
118 assumes US: "closedin (subtopology euclidean U) S" |
|
119 and UT: "closedin (subtopology euclidean U) T" |
|
120 and "S \<inter> T = {}" "S \<noteq> {}" "T \<noteq> {}" "a \<noteq> b" |
|
121 obtains f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
|
122 where "continuous_on U f" |
|
123 "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b" |
|
124 "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)" |
|
125 "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)" |
|
126 proof - |
|
127 have S0: "\<And>x. x \<in> U \<Longrightarrow> setdist {x} S = 0 \<longleftrightarrow> x \<in> S" |
|
128 using \<open>S \<noteq> {}\<close> US setdist_eq_0_closedin by auto |
|
129 have T0: "\<And>x. x \<in> U \<Longrightarrow> setdist {x} T = 0 \<longleftrightarrow> x \<in> T" |
|
130 using \<open>T \<noteq> {}\<close> UT setdist_eq_0_closedin by auto |
|
131 have sdpos: "0 < setdist {x} S + setdist {x} T" if "x \<in> U" for x |
|
132 proof - |
|
133 have "~ (setdist {x} S = 0 \<and> setdist {x} T = 0)" |
|
134 using assms by (metis IntI empty_iff setdist_eq_0_closedin that) |
|
135 then show ?thesis |
|
136 by (metis add.left_neutral add.right_neutral add_pos_pos linorder_neqE_linordered_idom not_le setdist_pos_le) |
|
137 qed |
|
138 define f where "f \<equiv> \<lambda>x. a + (setdist {x} S / (setdist {x} S + setdist {x} T)) *\<^sub>R (b - a)" |
|
139 show ?thesis |
|
140 proof (rule_tac f = f in that) |
|
141 show "continuous_on U f" |
|
142 using sdpos unfolding f_def |
|
143 by (intro continuous_intros | force)+ |
|
144 show "f x \<in> closed_segment a b" if "x \<in> U" for x |
|
145 unfolding f_def |
|
146 apply (simp add: closed_segment_def) |
|
147 apply (rule_tac x="(setdist {x} S / (setdist {x} S + setdist {x} T))" in exI) |
|
148 using sdpos that apply (simp add: algebra_simps) |
|
149 done |
|
150 show "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)" |
|
151 using S0 \<open>a \<noteq> b\<close> f_def sdpos by force |
|
152 show "(f x = b \<longleftrightarrow> x \<in> T)" if "x \<in> U" for x |
|
153 proof - |
|
154 have "f x = b \<longleftrightarrow> (setdist {x} S / (setdist {x} S + setdist {x} T)) = 1" |
|
155 unfolding f_def |
|
156 apply (rule iffI) |
|
157 apply (metis \<open>a \<noteq> b\<close> add_diff_cancel_left' eq_iff_diff_eq_0 pth_1 real_vector.scale_right_imp_eq, force) |
|
158 done |
|
159 also have "... \<longleftrightarrow> setdist {x} T = 0 \<and> setdist {x} S \<noteq> 0" |
|
160 using sdpos that |
|
161 by (simp add: divide_simps) linarith |
|
162 also have "... \<longleftrightarrow> x \<in> T" |
|
163 using \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>S \<inter> T = {}\<close> that |
|
164 by (force simp: S0 T0) |
|
165 finally show ?thesis . |
|
166 qed |
|
167 qed |
|
168 qed |
|
169 |
|
170 proposition Urysohn_local_strong: |
|
171 assumes US: "closedin (subtopology euclidean U) S" |
|
172 and UT: "closedin (subtopology euclidean U) T" |
|
173 and "S \<inter> T = {}" "a \<noteq> b" |
|
174 obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
175 where "continuous_on U f" |
|
176 "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b" |
|
177 "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)" |
|
178 "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)" |
|
179 proof (cases "S = {}") |
|
180 case True show ?thesis |
|
181 proof (cases "T = {}") |
|
182 case True show ?thesis |
|
183 proof (rule_tac f = "\<lambda>x. midpoint a b" in that) |
|
184 show "continuous_on U (\<lambda>x. midpoint a b)" |
|
185 by (intro continuous_intros) |
|
186 show "midpoint a b \<in> closed_segment a b" |
|
187 using csegment_midpoint_subset by blast |
|
188 show "(midpoint a b = a) = (x \<in> S)" for x |
|
189 using \<open>S = {}\<close> \<open>a \<noteq> b\<close> by simp |
|
190 show "(midpoint a b = b) = (x \<in> T)" for x |
|
191 using \<open>T = {}\<close> \<open>a \<noteq> b\<close> by simp |
|
192 qed |
|
193 next |
|
194 case False |
|
195 show ?thesis |
|
196 proof (cases "T = U") |
|
197 case True with \<open>S = {}\<close> \<open>a \<noteq> b\<close> show ?thesis |
|
198 by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const) |
|
199 next |
|
200 case False |
|
201 with UT closedin_subset obtain c where c: "c \<in> U" "c \<notin> T" |
|
202 by fastforce |
|
203 obtain f where f: "continuous_on U f" |
|
204 "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment (midpoint a b) b" |
|
205 "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)" |
|
206 "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)" |
|
207 apply (rule Urysohn_both_ne [of U "{c}" T "midpoint a b" "b"]) |
|
208 using c \<open>T \<noteq> {}\<close> assms apply simp_all |
|
209 done |
|
210 show ?thesis |
|
211 apply (rule_tac f=f in that) |
|
212 using \<open>S = {}\<close> \<open>T \<noteq> {}\<close> f csegment_midpoint_subset notin_segment_midpoint [OF \<open>a \<noteq> b\<close>] |
|
213 apply force+ |
|
214 done |
|
215 qed |
|
216 qed |
|
217 next |
|
218 case False |
|
219 show ?thesis |
|
220 proof (cases "T = {}") |
|
221 case True show ?thesis |
|
222 proof (cases "S = U") |
|
223 case True with \<open>T = {}\<close> \<open>a \<noteq> b\<close> show ?thesis |
|
224 by (rule_tac f = "\<lambda>x. a" in that) (auto simp: continuous_on_const) |
|
225 next |
|
226 case False |
|
227 with US closedin_subset obtain c where c: "c \<in> U" "c \<notin> S" |
|
228 by fastforce |
|
229 obtain f where f: "continuous_on U f" |
|
230 "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a (midpoint a b)" |
|
231 "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)" |
|
232 "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)" |
|
233 apply (rule Urysohn_both_ne [of U S "{c}" a "midpoint a b"]) |
|
234 using c \<open>S \<noteq> {}\<close> assms apply simp_all |
|
235 apply (metis midpoint_eq_endpoint) |
|
236 done |
|
237 show ?thesis |
|
238 apply (rule_tac f=f in that) |
|
239 using \<open>S \<noteq> {}\<close> \<open>T = {}\<close> f \<open>a \<noteq> b\<close> |
|
240 apply simp_all |
|
241 apply (metis (no_types) closed_segment_commute csegment_midpoint_subset midpoint_sym subset_iff) |
|
242 apply (metis closed_segment_commute midpoint_sym notin_segment_midpoint) |
|
243 done |
|
244 qed |
|
245 next |
|
246 case False |
|
247 show ?thesis |
|
248 using Urysohn_both_ne [OF US UT \<open>S \<inter> T = {}\<close> \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>a \<noteq> b\<close>] that |
|
249 by blast |
|
250 qed |
|
251 qed |
|
252 |
|
253 lemma Urysohn_local: |
|
254 assumes US: "closedin (subtopology euclidean U) S" |
|
255 and UT: "closedin (subtopology euclidean U) T" |
|
256 and "S \<inter> T = {}" |
|
257 obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
258 where "continuous_on U f" |
|
259 "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b" |
|
260 "\<And>x. x \<in> S \<Longrightarrow> f x = a" |
|
261 "\<And>x. x \<in> T \<Longrightarrow> f x = b" |
|
262 proof (cases "a = b") |
|
263 case True then show ?thesis |
|
264 by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const) |
|
265 next |
|
266 case False |
|
267 then show ?thesis |
|
268 apply (rule Urysohn_local_strong [OF assms]) |
|
269 apply (erule that, assumption) |
|
270 apply (meson US closedin_singleton closedin_trans) |
|
271 apply (meson UT closedin_singleton closedin_trans) |
|
272 done |
|
273 qed |
|
274 |
|
275 lemma Urysohn_strong: |
|
276 assumes US: "closed S" |
|
277 and UT: "closed T" |
|
278 and "S \<inter> T = {}" "a \<noteq> b" |
|
279 obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
280 where "continuous_on UNIV f" |
|
281 "\<And>x. f x \<in> closed_segment a b" |
|
282 "\<And>x. f x = a \<longleftrightarrow> x \<in> S" |
|
283 "\<And>x. f x = b \<longleftrightarrow> x \<in> T" |
|
284 apply (rule Urysohn_local_strong [of UNIV S T]) |
|
285 using assms |
|
286 apply (auto simp: closed_closedin) |
|
287 done |
|
288 |
|
289 proposition Urysohn: |
|
290 assumes US: "closed S" |
|
291 and UT: "closed T" |
|
292 and "S \<inter> T = {}" |
|
293 obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
294 where "continuous_on UNIV f" |
|
295 "\<And>x. f x \<in> closed_segment a b" |
|
296 "\<And>x. x \<in> S \<Longrightarrow> f x = a" |
|
297 "\<And>x. x \<in> T \<Longrightarrow> f x = b" |
|
298 apply (rule Urysohn_local [of UNIV S T a b]) |
|
299 using assms |
|
300 apply (auto simp: closed_closedin) |
|
301 done |
|
302 |
|
303 |
|
304 subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close> |
|
305 |
|
306 text\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367. |
|
307 http://projecteuclid.org/euclid.pjm/1103052106\<close> |
|
308 |
|
309 theorem Dugundji: |
|
310 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner" |
|
311 assumes "convex C" "C \<noteq> {}" |
|
312 and cloin: "closedin (subtopology euclidean U) S" |
|
313 and contf: "continuous_on S f" and "f ` S \<subseteq> C" |
|
314 obtains g where "continuous_on U g" "g ` U \<subseteq> C" |
|
315 "\<And>x. x \<in> S \<Longrightarrow> g x = f x" |
|
316 proof (cases "S = {}") |
|
317 case True then show thesis |
|
318 apply (rule_tac g="\<lambda>x. @y. y \<in> C" in that) |
|
319 apply (rule continuous_intros) |
|
320 apply (meson all_not_in_conv \<open>C \<noteq> {}\<close> image_subsetI someI_ex, simp) |
|
321 done |
|
322 next |
|
323 case False |
|
324 then have sd_pos: "\<And>x. \<lbrakk>x \<in> U; x \<notin> S\<rbrakk> \<Longrightarrow> 0 < setdist {x} S" |
|
325 using setdist_eq_0_closedin [OF cloin] le_less setdist_pos_le by fastforce |
|
326 define \<B> where "\<B> = {ball x (setdist {x} S / 2) |x. x \<in> U - S}" |
|
327 have [simp]: "\<And>T. T \<in> \<B> \<Longrightarrow> open T" |
|
328 by (auto simp: \<B>_def) |
|
329 have USS: "U - S \<subseteq> \<Union>\<B>" |
|
330 by (auto simp: sd_pos \<B>_def) |
|
331 obtain \<C> where USsub: "U - S \<subseteq> \<Union>\<C>" |
|
332 and nbrhd: "\<And>U. U \<in> \<C> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<B> \<and> U \<subseteq> T)" |
|
333 and fin: "\<And>x. x \<in> U - S |
|
334 \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}" |
|
335 using paracompact [OF USS] by auto |
|
336 have "\<exists>v a. v \<in> U \<and> v \<notin> S \<and> a \<in> S \<and> |
|
337 T \<subseteq> ball v (setdist {v} S / 2) \<and> |
|
338 dist v a \<le> 2 * setdist {v} S" if "T \<in> \<C>" for T |
|
339 proof - |
|
340 obtain v where v: "T \<subseteq> ball v (setdist {v} S / 2)" "v \<in> U" "v \<notin> S" |
|
341 using \<open>T \<in> \<C>\<close> nbrhd by (force simp: \<B>_def) |
|
342 then obtain a where "a \<in> S" "dist v a < 2 * setdist {v} S" |
|
343 using setdist_ltE [of "{v}" S "2 * setdist {v} S"] |
|
344 using False sd_pos by force |
|
345 with v show ?thesis |
|
346 apply (rule_tac x=v in exI) |
|
347 apply (rule_tac x=a in exI, auto) |
|
348 done |
|
349 qed |
|
350 then obtain \<V> \<A> where |
|
351 VA: "\<And>T. T \<in> \<C> \<Longrightarrow> \<V> T \<in> U \<and> \<V> T \<notin> S \<and> \<A> T \<in> S \<and> |
|
352 T \<subseteq> ball (\<V> T) (setdist {\<V> T} S / 2) \<and> |
|
353 dist (\<V> T) (\<A> T) \<le> 2 * setdist {\<V> T} S" |
|
354 by metis |
|
355 have sdle: "setdist {\<V> T} S \<le> 2 * setdist {v} S" if "T \<in> \<C>" "v \<in> T" for T v |
|
356 using setdist_Lipschitz [of "\<V> T" S v] VA [OF \<open>T \<in> \<C>\<close>] \<open>v \<in> T\<close> by auto |
|
357 have d6: "dist a (\<A> T) \<le> 6 * dist a v" if "T \<in> \<C>" "v \<in> T" "a \<in> S" for T v a |
|
358 proof - |
|
359 have "dist (\<V> T) v < setdist {\<V> T} S / 2" |
|
360 using that VA mem_ball by blast |
|
361 also have "... \<le> setdist {v} S" |
|
362 using sdle [OF \<open>T \<in> \<C>\<close> \<open>v \<in> T\<close>] by simp |
|
363 also have vS: "setdist {v} S \<le> dist a v" |
|
364 by (simp add: setdist_le_dist setdist_sym \<open>a \<in> S\<close>) |
|
365 finally have VTV: "dist (\<V> T) v < dist a v" . |
|
366 have VTS: "setdist {\<V> T} S \<le> 2 * dist a v" |
|
367 using sdle that vS by force |
|
368 have "dist a (\<A> T) \<le> dist a v + dist v (\<V> T) + dist (\<V> T) (\<A> T)" |
|
369 by (metis add.commute add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le) |
|
370 also have "... \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)" |
|
371 using VTV by (simp add: dist_commute) |
|
372 also have "... \<le> 2 * dist a v + 2 * setdist {\<V> T} S" |
|
373 using VA [OF \<open>T \<in> \<C>\<close>] by auto |
|
374 finally show ?thesis |
|
375 using VTS by linarith |
|
376 qed |
|
377 obtain H :: "['a set, 'a] \<Rightarrow> real" |
|
378 where Hcont: "\<And>Z. Z \<in> \<C> \<Longrightarrow> continuous_on (U-S) (H Z)" |
|
379 and Hge0: "\<And>Z x. \<lbrakk>Z \<in> \<C>; x \<in> U-S\<rbrakk> \<Longrightarrow> 0 \<le> H Z x" |
|
380 and Heq0: "\<And>x Z. \<lbrakk>Z \<in> \<C>; x \<in> U-S; x \<notin> Z\<rbrakk> \<Longrightarrow> H Z x = 0" |
|
381 and H1: "\<And>x. x \<in> U-S \<Longrightarrow> supp_setsum (\<lambda>W. H W x) \<C> = 1" |
|
382 and Hfin: "\<And>x. x \<in> U-S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. H U x \<noteq> 0}" |
|
383 apply (rule subordinate_partition_of_unity [OF USsub _ fin]) |
|
384 using nbrhd by auto |
|
385 define g where "g \<equiv> \<lambda>x. if x \<in> S then f x else supp_setsum (\<lambda>T. H T x *\<^sub>R f(\<A> T)) \<C>" |
|
386 show ?thesis |
|
387 proof (rule that) |
|
388 show "continuous_on U g" |
|
389 proof (clarsimp simp: continuous_on_eq_continuous_within) |
|
390 fix a assume "a \<in> U" |
|
391 show "continuous (at a within U) g" |
|
392 proof (cases "a \<in> S") |
|
393 case True show ?thesis |
|
394 proof (clarsimp simp add: continuous_within_topological) |
|
395 fix W |
|
396 assume "open W" "g a \<in> W" |
|
397 then obtain e where "0 < e" and e: "ball (f a) e \<subseteq> W" |
|
398 using openE True g_def by auto |
|
399 have "continuous (at a within S) f" |
|
400 using True contf continuous_on_eq_continuous_within by blast |
|
401 then obtain d where "0 < d" |
|
402 and d: "\<And>x. \<lbrakk>x \<in> S; dist x a < d\<rbrakk> \<Longrightarrow> dist (f x) (f a) < e" |
|
403 using continuous_within_eps_delta \<open>0 < e\<close> by force |
|
404 have "g y \<in> ball (f a) e" if "y \<in> U" and y: "y \<in> ball a (d / 6)" for y |
|
405 proof (cases "y \<in> S") |
|
406 case True |
|
407 then have "dist (f a) (f y) < e" |
|
408 by (metis ball_divide_subset_numeral dist_commute in_mono mem_ball y d) |
|
409 then show ?thesis |
|
410 by (simp add: True g_def) |
|
411 next |
|
412 case False |
|
413 have *: "dist (f (\<A> T)) (f a) < e" if "T \<in> \<C>" "H T y \<noteq> 0" for T |
|
414 proof - |
|
415 have "y \<in> T" |
|
416 using Heq0 that False \<open>y \<in> U\<close> by blast |
|
417 have "dist (\<A> T) a < d" |
|
418 using d6 [OF \<open>T \<in> \<C>\<close> \<open>y \<in> T\<close> \<open>a \<in> S\<close>] y |
|
419 by (simp add: dist_commute mult.commute) |
|
420 then show ?thesis |
|
421 using VA [OF \<open>T \<in> \<C>\<close>] by (auto simp: d) |
|
422 qed |
|
423 have "supp_setsum (\<lambda>T. H T y *\<^sub>R f (\<A> T)) \<C> \<in> ball (f a) e" |
|
424 apply (rule convex_supp_setsum [OF convex_ball]) |
|
425 apply (simp_all add: False H1 Hge0 \<open>y \<in> U\<close>) |
|
426 by (metis dist_commute *) |
|
427 then show ?thesis |
|
428 by (simp add: False g_def) |
|
429 qed |
|
430 then show "\<exists>A. open A \<and> a \<in> A \<and> (\<forall>y\<in>U. y \<in> A \<longrightarrow> g y \<in> W)" |
|
431 apply (rule_tac x = "ball a (d / 6)" in exI) |
|
432 using e \<open>0 < d\<close> by fastforce |
|
433 qed |
|
434 next |
|
435 case False |
|
436 obtain N where N: "open N" "a \<in> N" |
|
437 and finN: "finite {U \<in> \<C>. \<exists>a\<in>N. H U a \<noteq> 0}" |
|
438 using Hfin False \<open>a \<in> U\<close> by auto |
|
439 have oUS: "openin (subtopology euclidean U) (U - S)" |
|
440 using cloin by (simp add: openin_diff) |
|
441 have HcontU: "continuous (at a within U) (H T)" if "T \<in> \<C>" for T |
|
442 using Hcont [OF \<open>T \<in> \<C>\<close>] False \<open>a \<in> U\<close> \<open>T \<in> \<C>\<close> |
|
443 apply (simp add: continuous_on_eq_continuous_within continuous_within) |
|
444 apply (rule Lim_transform_within_set) |
|
445 using oUS |
|
446 apply (force simp: eventually_at openin_contains_ball dist_commute dest!: bspec)+ |
|
447 done |
|
448 show ?thesis |
|
449 proof (rule continuous_transform_within_openin [OF _ oUS]) |
|
450 show "continuous (at a within U) (\<lambda>x. supp_setsum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>)" |
|
451 proof (rule continuous_transform_within_openin) |
|
452 show "continuous (at a within U) |
|
453 (\<lambda>x. \<Sum>T\<in>{U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))" |
|
454 by (force intro: continuous_intros HcontU)+ |
|
455 next |
|
456 show "openin (subtopology euclidean U) ((U - S) \<inter> N)" |
|
457 using N oUS openin_trans by blast |
|
458 next |
|
459 show "a \<in> (U - S) \<inter> N" using False \<open>a \<in> U\<close> N by blast |
|
460 next |
|
461 show "\<And>x. x \<in> (U - S) \<inter> N \<Longrightarrow> |
|
462 (\<Sum>T \<in> {U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T)) |
|
463 = supp_setsum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>" |
|
464 by (auto simp: supp_setsum_def support_on_def |
|
465 intro: setsum.mono_neutral_right [OF finN]) |
|
466 qed |
|
467 next |
|
468 show "a \<in> U - S" using False \<open>a \<in> U\<close> by blast |
|
469 next |
|
470 show "\<And>x. x \<in> U - S \<Longrightarrow> supp_setsum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C> = g x" |
|
471 by (simp add: g_def) |
|
472 qed |
|
473 qed |
|
474 qed |
|
475 show "g ` U \<subseteq> C" |
|
476 using \<open>f ` S \<subseteq> C\<close> VA |
|
477 by (fastforce simp: g_def Hge0 intro!: convex_supp_setsum [OF \<open>convex C\<close>] H1) |
|
478 show "\<And>x. x \<in> S \<Longrightarrow> g x = f x" |
|
479 by (simp add: g_def) |
|
480 qed |
|
481 qed |
|
482 |
|
483 |
|
484 corollary Tietze: |
|
485 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner" |
|
486 assumes "continuous_on S f" |
|
487 and "closedin (subtopology euclidean U) S" |
|
488 and "0 \<le> B" |
|
489 and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B" |
|
490 obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x" |
|
491 "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B" |
|
492 using assms |
|
493 by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f]) |
|
494 |
|
495 corollary Tietze_closed_interval: |
|
496 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
497 assumes "continuous_on S f" |
|
498 and "closedin (subtopology euclidean U) S" |
|
499 and "cbox a b \<noteq> {}" |
|
500 and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b" |
|
501 obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x" |
|
502 "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b" |
|
503 apply (rule Dugundji [of "cbox a b" U S f]) |
|
504 using assms by auto |
|
505 |
|
506 corollary Tietze_closed_interval_1: |
|
507 fixes f :: "'a::euclidean_space \<Rightarrow> real" |
|
508 assumes "continuous_on S f" |
|
509 and "closedin (subtopology euclidean U) S" |
|
510 and "a \<le> b" |
|
511 and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b" |
|
512 obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x" |
|
513 "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b" |
|
514 apply (rule Dugundji [of "cbox a b" U S f]) |
|
515 using assms by (auto simp: image_subset_iff) |
|
516 |
|
517 corollary Tietze_open_interval: |
|
518 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
519 assumes "continuous_on S f" |
|
520 and "closedin (subtopology euclidean U) S" |
|
521 and "box a b \<noteq> {}" |
|
522 and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b" |
|
523 obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x" |
|
524 "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b" |
|
525 apply (rule Dugundji [of "box a b" U S f]) |
|
526 using assms by auto |
|
527 |
|
528 corollary Tietze_open_interval_1: |
|
529 fixes f :: "'a::euclidean_space \<Rightarrow> real" |
|
530 assumes "continuous_on S f" |
|
531 and "closedin (subtopology euclidean U) S" |
|
532 and "a < b" |
|
533 and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b" |
|
534 obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x" |
|
535 "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b" |
|
536 apply (rule Dugundji [of "box a b" U S f]) |
|
537 using assms by (auto simp: image_subset_iff) |
|
538 |
|
539 corollary Tietze_unbounded: |
|
540 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner" |
|
541 assumes "continuous_on S f" |
|
542 and "closedin (subtopology euclidean U) S" |
|
543 obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x" |
|
544 apply (rule Dugundji [of UNIV U S f]) |
|
545 using assms by auto |
|
546 |
|
547 end |
|