1 section \<open>The Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close> |
|
2 |
|
3 text\<open>By L C Paulson (2015)\<close> |
|
4 |
|
5 theory Weierstrass_Theorems |
|
6 imports Uniform_Limit Path_Connected |
|
7 begin |
|
8 |
|
9 subsection \<open>Bernstein polynomials\<close> |
|
10 |
|
11 definition Bernstein :: "[nat,nat,real] \<Rightarrow> real" where |
|
12 "Bernstein n k x \<equiv> of_nat (n choose k) * x ^ k * (1 - x) ^ (n - k)" |
|
13 |
|
14 lemma Bernstein_nonneg: "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> Bernstein n k x" |
|
15 by (simp add: Bernstein_def) |
|
16 |
|
17 lemma Bernstein_pos: "\<lbrakk>0 < x; x < 1; k \<le> n\<rbrakk> \<Longrightarrow> 0 < Bernstein n k x" |
|
18 by (simp add: Bernstein_def) |
|
19 |
|
20 lemma sum_Bernstein [simp]: "(\<Sum> k = 0..n. Bernstein n k x) = 1" |
|
21 using binomial_ring [of x "1-x" n] |
|
22 by (simp add: Bernstein_def) |
|
23 |
|
24 lemma binomial_deriv1: |
|
25 "(\<Sum>k=0..n. (of_nat k * of_nat (n choose k)) * a^(k-1) * b^(n-k)) = real_of_nat n * (a+b) ^ (n-1)" |
|
26 apply (rule DERIV_unique [where f = "\<lambda>a. (a+b)^n" and x=a]) |
|
27 apply (subst binomial_ring) |
|
28 apply (rule derivative_eq_intros setsum.cong | simp)+ |
|
29 done |
|
30 |
|
31 lemma binomial_deriv2: |
|
32 "(\<Sum>k=0..n. (of_nat k * of_nat (k-1) * of_nat (n choose k)) * a^(k-2) * b^(n-k)) = |
|
33 of_nat n * of_nat (n-1) * (a+b::real) ^ (n-2)" |
|
34 apply (rule DERIV_unique [where f = "\<lambda>a. of_nat n * (a+b::real) ^ (n-1)" and x=a]) |
|
35 apply (subst binomial_deriv1 [symmetric]) |
|
36 apply (rule derivative_eq_intros setsum.cong | simp add: Num.numeral_2_eq_2)+ |
|
37 done |
|
38 |
|
39 lemma sum_k_Bernstein [simp]: "(\<Sum>k = 0..n. real k * Bernstein n k x) = of_nat n * x" |
|
40 apply (subst binomial_deriv1 [of n x "1-x", simplified, symmetric]) |
|
41 apply (simp add: setsum_left_distrib) |
|
42 apply (auto simp: Bernstein_def algebra_simps realpow_num_eq_if intro!: setsum.cong) |
|
43 done |
|
44 |
|
45 lemma sum_kk_Bernstein [simp]: "(\<Sum> k = 0..n. real k * (real k - 1) * Bernstein n k x) = real n * (real n - 1) * x\<^sup>2" |
|
46 proof - |
|
47 have "(\<Sum> k = 0..n. real k * (real k - 1) * Bernstein n k x) = real_of_nat n * real_of_nat (n - Suc 0) * x\<^sup>2" |
|
48 apply (subst binomial_deriv2 [of n x "1-x", simplified, symmetric]) |
|
49 apply (simp add: setsum_left_distrib) |
|
50 apply (rule setsum.cong [OF refl]) |
|
51 apply (simp add: Bernstein_def power2_eq_square algebra_simps) |
|
52 apply (rename_tac k) |
|
53 apply (subgoal_tac "k = 0 \<or> k = 1 \<or> (\<exists>k'. k = Suc (Suc k'))") |
|
54 apply (force simp add: field_simps of_nat_Suc power2_eq_square) |
|
55 by presburger |
|
56 also have "... = n * (n - 1) * x\<^sup>2" |
|
57 by auto |
|
58 finally show ?thesis |
|
59 by auto |
|
60 qed |
|
61 |
|
62 subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close> |
|
63 |
|
64 lemma Bernstein_Weierstrass: |
|
65 fixes f :: "real \<Rightarrow> real" |
|
66 assumes contf: "continuous_on {0..1} f" and e: "0 < e" |
|
67 shows "\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> {0..1} |
|
68 \<longrightarrow> \<bar>f x - (\<Sum>k = 0..n. f(k/n) * Bernstein n k x)\<bar> < e" |
|
69 proof - |
|
70 have "bounded (f ` {0..1})" |
|
71 using compact_continuous_image compact_imp_bounded contf by blast |
|
72 then obtain M where M: "\<And>x. 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<bar>f x\<bar> \<le> M" |
|
73 by (force simp add: bounded_iff) |
|
74 then have Mge0: "0 \<le> M" by force |
|
75 have ucontf: "uniformly_continuous_on {0..1} f" |
|
76 using compact_uniformly_continuous contf by blast |
|
77 then obtain d where d: "d>0" "\<And>x x'. \<lbrakk> x \<in> {0..1}; x' \<in> {0..1}; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> \<bar>f x' - f x\<bar> < e/2" |
|
78 apply (rule uniformly_continuous_onE [where e = "e/2"]) |
|
79 using e by (auto simp: dist_norm) |
|
80 { fix n::nat and x::real |
|
81 assume n: "Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>) \<le> n" and x: "0 \<le> x" "x \<le> 1" |
|
82 have "0 < n" using n by simp |
|
83 have ed0: "- (e * d\<^sup>2) < 0" |
|
84 using e \<open>0<d\<close> by simp |
|
85 also have "... \<le> M * 4" |
|
86 using \<open>0\<le>M\<close> by simp |
|
87 finally have [simp]: "real_of_int (nat \<lceil>4 * M / (e * d\<^sup>2)\<rceil>) = real_of_int \<lceil>4 * M / (e * d\<^sup>2)\<rceil>" |
|
88 using \<open>0\<le>M\<close> e \<open>0<d\<close> |
|
89 by (simp add: of_nat_Suc field_simps) |
|
90 have "4*M/(e*d\<^sup>2) + 1 \<le> real (Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>))" |
|
91 by (simp add: of_nat_Suc real_nat_ceiling_ge) |
|
92 also have "... \<le> real n" |
|
93 using n by (simp add: of_nat_Suc field_simps) |
|
94 finally have nbig: "4*M/(e*d\<^sup>2) + 1 \<le> real n" . |
|
95 have sum_bern: "(\<Sum>k = 0..n. (x - k/n)\<^sup>2 * Bernstein n k x) = x * (1 - x) / n" |
|
96 proof - |
|
97 have *: "\<And>a b x::real. (a - b)\<^sup>2 * x = a * (a - 1) * x + (1 - 2 * b) * a * x + b * b * x" |
|
98 by (simp add: algebra_simps power2_eq_square) |
|
99 have "(\<Sum> k = 0..n. (k - n * x)\<^sup>2 * Bernstein n k x) = n * x * (1 - x)" |
|
100 apply (simp add: * setsum.distrib) |
|
101 apply (simp add: setsum_right_distrib [symmetric] mult.assoc) |
|
102 apply (simp add: algebra_simps power2_eq_square) |
|
103 done |
|
104 then have "(\<Sum> k = 0..n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n" |
|
105 by (simp add: power2_eq_square) |
|
106 then show ?thesis |
|
107 using n by (simp add: setsum_divide_distrib divide_simps mult.commute power2_commute) |
|
108 qed |
|
109 { fix k |
|
110 assume k: "k \<le> n" |
|
111 then have kn: "0 \<le> k / n" "k / n \<le> 1" |
|
112 by (auto simp: divide_simps) |
|
113 consider (lessd) "\<bar>x - k / n\<bar> < d" | (ged) "d \<le> \<bar>x - k / n\<bar>" |
|
114 by linarith |
|
115 then have "\<bar>(f x - f (k/n))\<bar> \<le> e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2" |
|
116 proof cases |
|
117 case lessd |
|
118 then have "\<bar>(f x - f (k/n))\<bar> < e/2" |
|
119 using d x kn by (simp add: abs_minus_commute) |
|
120 also have "... \<le> (e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2)" |
|
121 using Mge0 d by simp |
|
122 finally show ?thesis by simp |
|
123 next |
|
124 case ged |
|
125 then have dle: "d\<^sup>2 \<le> (x - k/n)\<^sup>2" |
|
126 by (metis d(1) less_eq_real_def power2_abs power_mono) |
|
127 have "\<bar>(f x - f (k/n))\<bar> \<le> \<bar>f x\<bar> + \<bar>f (k/n)\<bar>" |
|
128 by (rule abs_triangle_ineq4) |
|
129 also have "... \<le> M+M" |
|
130 by (meson M add_mono_thms_linordered_semiring(1) kn x) |
|
131 also have "... \<le> 2 * M * ((x - k/n)\<^sup>2 / d\<^sup>2)" |
|
132 apply simp |
|
133 apply (rule Rings.ordered_semiring_class.mult_left_mono [of 1 "((x - k/n)\<^sup>2 / d\<^sup>2)", simplified]) |
|
134 using dle \<open>d>0\<close> \<open>M\<ge>0\<close> by auto |
|
135 also have "... \<le> e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2" |
|
136 using e by simp |
|
137 finally show ?thesis . |
|
138 qed |
|
139 } note * = this |
|
140 have "\<bar>f x - (\<Sum> k = 0..n. f(k / n) * Bernstein n k x)\<bar> \<le> \<bar>\<Sum> k = 0..n. (f x - f(k / n)) * Bernstein n k x\<bar>" |
|
141 by (simp add: setsum_subtractf setsum_right_distrib [symmetric] algebra_simps) |
|
142 also have "... \<le> (\<Sum> k = 0..n. (e/2 + (2 * M / d\<^sup>2) * (x - k / n)\<^sup>2) * Bernstein n k x)" |
|
143 apply (rule order_trans [OF setsum_abs setsum_mono]) |
|
144 using * |
|
145 apply (simp add: abs_mult Bernstein_nonneg x mult_right_mono) |
|
146 done |
|
147 also have "... \<le> e/2 + (2 * M) / (d\<^sup>2 * n)" |
|
148 apply (simp only: setsum.distrib Rings.semiring_class.distrib_right setsum_right_distrib [symmetric] mult.assoc sum_bern) |
|
149 using \<open>d>0\<close> x |
|
150 apply (simp add: divide_simps Mge0 mult_le_one mult_left_le) |
|
151 done |
|
152 also have "... < e" |
|
153 apply (simp add: field_simps) |
|
154 using \<open>d>0\<close> nbig e \<open>n>0\<close> |
|
155 apply (simp add: divide_simps algebra_simps) |
|
156 using ed0 by linarith |
|
157 finally have "\<bar>f x - (\<Sum>k = 0..n. f (real k / real n) * Bernstein n k x)\<bar> < e" . |
|
158 } |
|
159 then show ?thesis |
|
160 by auto |
|
161 qed |
|
162 |
|
163 |
|
164 subsection \<open>General Stone-Weierstrass theorem\<close> |
|
165 |
|
166 text\<open>Source: |
|
167 Bruno Brosowski and Frank Deutsch. |
|
168 An Elementary Proof of the Stone-Weierstrass Theorem. |
|
169 Proceedings of the American Mathematical Society |
|
170 Volume 81, Number 1, January 1981. |
|
171 DOI: 10.2307/2043993 http://www.jstor.org/stable/2043993\<close> |
|
172 |
|
173 locale function_ring_on = |
|
174 fixes R :: "('a::t2_space \<Rightarrow> real) set" and s :: "'a set" |
|
175 assumes compact: "compact s" |
|
176 assumes continuous: "f \<in> R \<Longrightarrow> continuous_on s f" |
|
177 assumes add: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x + g x) \<in> R" |
|
178 assumes mult: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x * g x) \<in> R" |
|
179 assumes const: "(\<lambda>_. c) \<in> R" |
|
180 assumes separable: "x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x \<noteq> y \<Longrightarrow> \<exists>f\<in>R. f x \<noteq> f y" |
|
181 |
|
182 begin |
|
183 lemma minus: "f \<in> R \<Longrightarrow> (\<lambda>x. - f x) \<in> R" |
|
184 by (frule mult [OF const [of "-1"]]) simp |
|
185 |
|
186 lemma diff: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x - g x) \<in> R" |
|
187 unfolding diff_conv_add_uminus by (metis add minus) |
|
188 |
|
189 lemma power: "f \<in> R \<Longrightarrow> (\<lambda>x. f x ^ n) \<in> R" |
|
190 by (induct n) (auto simp: const mult) |
|
191 |
|
192 lemma setsum: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>i \<in> I. f i x) \<in> R" |
|
193 by (induct I rule: finite_induct; simp add: const add) |
|
194 |
|
195 lemma setprod: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Prod>i \<in> I. f i x) \<in> R" |
|
196 by (induct I rule: finite_induct; simp add: const mult) |
|
197 |
|
198 definition normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real" |
|
199 where "normf f \<equiv> SUP x:s. \<bar>f x\<bar>" |
|
200 |
|
201 lemma normf_upper: "\<lbrakk>continuous_on s f; x \<in> s\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f" |
|
202 apply (simp add: normf_def) |
|
203 apply (rule cSUP_upper, assumption) |
|
204 by (simp add: bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs) |
|
205 |
|
206 lemma normf_least: "s \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> s \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M" |
|
207 by (simp add: normf_def cSUP_least) |
|
208 |
|
209 end |
|
210 |
|
211 lemma (in function_ring_on) one: |
|
212 assumes U: "open U" and t0: "t0 \<in> s" "t0 \<in> U" and t1: "t1 \<in> s-U" |
|
213 shows "\<exists>V. open V \<and> t0 \<in> V \<and> s \<inter> V \<subseteq> U \<and> |
|
214 (\<forall>e>0. \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>t \<in> s \<inter> V. f t < e) \<and> (\<forall>t \<in> s - U. f t > 1 - e))" |
|
215 proof - |
|
216 have "\<exists>pt \<in> R. pt t0 = 0 \<and> pt t > 0 \<and> pt ` s \<subseteq> {0..1}" if t: "t \<in> s - U" for t |
|
217 proof - |
|
218 have "t \<noteq> t0" using t t0 by auto |
|
219 then obtain g where g: "g \<in> R" "g t \<noteq> g t0" |
|
220 using separable t0 by (metis Diff_subset subset_eq t) |
|
221 define h where [abs_def]: "h x = g x - g t0" for x |
|
222 have "h \<in> R" |
|
223 unfolding h_def by (fast intro: g const diff) |
|
224 then have hsq: "(\<lambda>w. (h w)\<^sup>2) \<in> R" |
|
225 by (simp add: power2_eq_square mult) |
|
226 have "h t \<noteq> h t0" |
|
227 by (simp add: h_def g) |
|
228 then have "h t \<noteq> 0" |
|
229 by (simp add: h_def) |
|
230 then have ht2: "0 < (h t)^2" |
|
231 by simp |
|
232 also have "... \<le> normf (\<lambda>w. (h w)\<^sup>2)" |
|
233 using t normf_upper [where x=t] continuous [OF hsq] by force |
|
234 finally have nfp: "0 < normf (\<lambda>w. (h w)\<^sup>2)" . |
|
235 define p where [abs_def]: "p x = (1 / normf (\<lambda>w. (h w)\<^sup>2)) * (h x)^2" for x |
|
236 have "p \<in> R" |
|
237 unfolding p_def by (fast intro: hsq const mult) |
|
238 moreover have "p t0 = 0" |
|
239 by (simp add: p_def h_def) |
|
240 moreover have "p t > 0" |
|
241 using nfp ht2 by (simp add: p_def) |
|
242 moreover have "\<And>x. x \<in> s \<Longrightarrow> p x \<in> {0..1}" |
|
243 using nfp normf_upper [OF continuous [OF hsq] ] by (auto simp: p_def) |
|
244 ultimately show "\<exists>pt \<in> R. pt t0 = 0 \<and> pt t > 0 \<and> pt ` s \<subseteq> {0..1}" |
|
245 by auto |
|
246 qed |
|
247 then obtain pf where pf: "\<And>t. t \<in> s-U \<Longrightarrow> pf t \<in> R \<and> pf t t0 = 0 \<and> pf t t > 0" |
|
248 and pf01: "\<And>t. t \<in> s-U \<Longrightarrow> pf t ` s \<subseteq> {0..1}" |
|
249 by metis |
|
250 have com_sU: "compact (s-U)" |
|
251 using compact closed_Int_compact U by (simp add: Diff_eq compact_Int_closed open_closed) |
|
252 have "\<And>t. t \<in> s-U \<Longrightarrow> \<exists>A. open A \<and> A \<inter> s = {x\<in>s. 0 < pf t x}" |
|
253 apply (rule open_Collect_positive) |
|
254 by (metis pf continuous) |
|
255 then obtain Uf where Uf: "\<And>t. t \<in> s-U \<Longrightarrow> open (Uf t) \<and> (Uf t) \<inter> s = {x\<in>s. 0 < pf t x}" |
|
256 by metis |
|
257 then have open_Uf: "\<And>t. t \<in> s-U \<Longrightarrow> open (Uf t)" |
|
258 by blast |
|
259 have tUft: "\<And>t. t \<in> s-U \<Longrightarrow> t \<in> Uf t" |
|
260 using pf Uf by blast |
|
261 then have *: "s-U \<subseteq> (\<Union>x \<in> s-U. Uf x)" |
|
262 by blast |
|
263 obtain subU where subU: "subU \<subseteq> s - U" "finite subU" "s - U \<subseteq> (\<Union>x \<in> subU. Uf x)" |
|
264 by (blast intro: that open_Uf compactE_image [OF com_sU _ *]) |
|
265 then have [simp]: "subU \<noteq> {}" |
|
266 using t1 by auto |
|
267 then have cardp: "card subU > 0" using subU |
|
268 by (simp add: card_gt_0_iff) |
|
269 define p where [abs_def]: "p x = (1 / card subU) * (\<Sum>t \<in> subU. pf t x)" for x |
|
270 have pR: "p \<in> R" |
|
271 unfolding p_def using subU pf by (fast intro: pf const mult setsum) |
|
272 have pt0 [simp]: "p t0 = 0" |
|
273 using subU pf by (auto simp: p_def intro: setsum.neutral) |
|
274 have pt_pos: "p t > 0" if t: "t \<in> s-U" for t |
|
275 proof - |
|
276 obtain i where i: "i \<in> subU" "t \<in> Uf i" using subU t by blast |
|
277 show ?thesis |
|
278 using subU i t |
|
279 apply (clarsimp simp: p_def divide_simps) |
|
280 apply (rule setsum_pos2 [OF \<open>finite subU\<close>]) |
|
281 using Uf t pf01 apply auto |
|
282 apply (force elim!: subsetCE) |
|
283 done |
|
284 qed |
|
285 have p01: "p x \<in> {0..1}" if t: "x \<in> s" for x |
|
286 proof - |
|
287 have "0 \<le> p x" |
|
288 using subU cardp t |
|
289 apply (simp add: p_def divide_simps setsum_nonneg) |
|
290 apply (rule setsum_nonneg) |
|
291 using pf01 by force |
|
292 moreover have "p x \<le> 1" |
|
293 using subU cardp t |
|
294 apply (simp add: p_def divide_simps setsum_nonneg) |
|
295 apply (rule setsum_bounded_above [where 'a=real and K=1, simplified]) |
|
296 using pf01 by force |
|
297 ultimately show ?thesis |
|
298 by auto |
|
299 qed |
|
300 have "compact (p ` (s-U))" |
|
301 by (meson Diff_subset com_sU compact_continuous_image continuous continuous_on_subset pR) |
|
302 then have "open (- (p ` (s-U)))" |
|
303 by (simp add: compact_imp_closed open_Compl) |
|
304 moreover have "0 \<in> - (p ` (s-U))" |
|
305 by (metis (no_types) ComplI image_iff not_less_iff_gr_or_eq pt_pos) |
|
306 ultimately obtain delta0 where delta0: "delta0 > 0" "ball 0 delta0 \<subseteq> - (p ` (s-U))" |
|
307 by (auto simp: elim!: openE) |
|
308 then have pt_delta: "\<And>x. x \<in> s-U \<Longrightarrow> p x \<ge> delta0" |
|
309 by (force simp: ball_def dist_norm dest: p01) |
|
310 define \<delta> where "\<delta> = delta0/2" |
|
311 have "delta0 \<le> 1" using delta0 p01 [of t1] t1 |
|
312 by (force simp: ball_def dist_norm dest: p01) |
|
313 with delta0 have \<delta>01: "0 < \<delta>" "\<delta> < 1" |
|
314 by (auto simp: \<delta>_def) |
|
315 have pt_\<delta>: "\<And>x. x \<in> s-U \<Longrightarrow> p x \<ge> \<delta>" |
|
316 using pt_delta delta0 by (force simp: \<delta>_def) |
|
317 have "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. p x < \<delta>/2}" |
|
318 by (rule open_Collect_less_Int [OF continuous [OF pR] continuous_on_const]) |
|
319 then obtain V where V: "open V" "V \<inter> s = {x\<in>s. p x < \<delta>/2}" |
|
320 by blast |
|
321 define k where "k = nat\<lfloor>1/\<delta>\<rfloor> + 1" |
|
322 have "k>0" by (simp add: k_def) |
|
323 have "k-1 \<le> 1/\<delta>" |
|
324 using \<delta>01 by (simp add: k_def) |
|
325 with \<delta>01 have "k \<le> (1+\<delta>)/\<delta>" |
|
326 by (auto simp: algebra_simps add_divide_distrib) |
|
327 also have "... < 2/\<delta>" |
|
328 using \<delta>01 by (auto simp: divide_simps) |
|
329 finally have k2\<delta>: "k < 2/\<delta>" . |
|
330 have "1/\<delta> < k" |
|
331 using \<delta>01 unfolding k_def by linarith |
|
332 with \<delta>01 k2\<delta> have k\<delta>: "1 < k*\<delta>" "k*\<delta> < 2" |
|
333 by (auto simp: divide_simps) |
|
334 define q where [abs_def]: "q n t = (1 - p t ^ n) ^ (k^n)" for n t |
|
335 have qR: "q n \<in> R" for n |
|
336 by (simp add: q_def const diff power pR) |
|
337 have q01: "\<And>n t. t \<in> s \<Longrightarrow> q n t \<in> {0..1}" |
|
338 using p01 by (simp add: q_def power_le_one algebra_simps) |
|
339 have qt0 [simp]: "\<And>n. n>0 \<Longrightarrow> q n t0 = 1" |
|
340 using t0 pf by (simp add: q_def power_0_left) |
|
341 { fix t and n::nat |
|
342 assume t: "t \<in> s \<inter> V" |
|
343 with \<open>k>0\<close> V have "k * p t < k * \<delta> / 2" |
|
344 by force |
|
345 then have "1 - (k * \<delta> / 2)^n \<le> 1 - (k * p t)^n" |
|
346 using \<open>k>0\<close> p01 t by (simp add: power_mono) |
|
347 also have "... \<le> q n t" |
|
348 using Bernoulli_inequality [of "- ((p t)^n)" "k^n"] |
|
349 apply (simp add: q_def) |
|
350 by (metis IntE atLeastAtMost_iff p01 power_le_one power_mult_distrib t) |
|
351 finally have "1 - (k * \<delta> / 2) ^ n \<le> q n t" . |
|
352 } note limitV = this |
|
353 { fix t and n::nat |
|
354 assume t: "t \<in> s - U" |
|
355 with \<open>k>0\<close> U have "k * \<delta> \<le> k * p t" |
|
356 by (simp add: pt_\<delta>) |
|
357 with k\<delta> have kpt: "1 < k * p t" |
|
358 by (blast intro: less_le_trans) |
|
359 have ptn_pos: "0 < p t ^ n" |
|
360 using pt_pos [OF t] by simp |
|
361 have ptn_le: "p t ^ n \<le> 1" |
|
362 by (meson DiffE atLeastAtMost_iff p01 power_le_one t) |
|
363 have "q n t = (1/(k^n * (p t)^n)) * (1 - p t ^ n) ^ (k^n) * k^n * (p t)^n" |
|
364 using pt_pos [OF t] \<open>k>0\<close> by (simp add: q_def) |
|
365 also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + k^n * (p t)^n)" |
|
366 using pt_pos [OF t] \<open>k>0\<close> |
|
367 apply simp |
|
368 apply (simp only: times_divide_eq_right [symmetric]) |
|
369 apply (rule mult_left_mono [of "1::real", simplified]) |
|
370 apply (simp_all add: power_mult_distrib) |
|
371 apply (rule zero_le_power) |
|
372 using ptn_le by linarith |
|
373 also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + (p t)^n) ^ (k^n)" |
|
374 apply (rule mult_left_mono [OF Bernoulli_inequality [of "p t ^ n" "k^n"]]) |
|
375 using \<open>k>0\<close> ptn_pos ptn_le |
|
376 apply (auto simp: power_mult_distrib) |
|
377 done |
|
378 also have "... = (1/(k * (p t))^n) * (1 - p t ^ (2*n)) ^ (k^n)" |
|
379 using pt_pos [OF t] \<open>k>0\<close> |
|
380 by (simp add: algebra_simps power_mult power2_eq_square power_mult_distrib [symmetric]) |
|
381 also have "... \<le> (1/(k * (p t))^n) * 1" |
|
382 apply (rule mult_left_mono [OF power_le_one]) |
|
383 using pt_pos \<open>k>0\<close> p01 power_le_one t apply auto |
|
384 done |
|
385 also have "... \<le> (1 / (k*\<delta>))^n" |
|
386 using \<open>k>0\<close> \<delta>01 power_mono pt_\<delta> t |
|
387 by (fastforce simp: field_simps) |
|
388 finally have "q n t \<le> (1 / (real k * \<delta>)) ^ n " . |
|
389 } note limitNonU = this |
|
390 define NN |
|
391 where "NN e = 1 + nat \<lceil>max (ln e / ln (real k * \<delta> / 2)) (- ln e / ln (real k * \<delta>))\<rceil>" for e |
|
392 have NN: "of_nat (NN e) > ln e / ln (real k * \<delta> / 2)" "of_nat (NN e) > - ln e / ln (real k * \<delta>)" |
|
393 if "0<e" for e |
|
394 unfolding NN_def by linarith+ |
|
395 have NN1: "\<And>e. e>0 \<Longrightarrow> (k * \<delta> / 2)^NN e < e" |
|
396 apply (subst Transcendental.ln_less_cancel_iff [symmetric]) |
|
397 prefer 3 apply (subst ln_realpow) |
|
398 using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta> |
|
399 apply (force simp add: field_simps)+ |
|
400 done |
|
401 have NN0: "\<And>e. e>0 \<Longrightarrow> (1/(k*\<delta>))^NN e < e" |
|
402 apply (subst Transcendental.ln_less_cancel_iff [symmetric]) |
|
403 prefer 3 apply (subst ln_realpow) |
|
404 using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta> |
|
405 apply (force simp add: field_simps ln_div)+ |
|
406 done |
|
407 { fix t and e::real |
|
408 assume "e>0" |
|
409 have "t \<in> s \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> s - U \<Longrightarrow> q (NN e) t < e" |
|
410 proof - |
|
411 assume t: "t \<in> s \<inter> V" |
|
412 show "1 - q (NN e) t < e" |
|
413 by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF \<open>e>0\<close>]]) |
|
414 next |
|
415 assume t: "t \<in> s - U" |
|
416 show "q (NN e) t < e" |
|
417 using limitNonU [OF t] less_le_trans [OF NN0 [OF \<open>e>0\<close>]] not_le by blast |
|
418 qed |
|
419 } then have "\<And>e. e > 0 \<Longrightarrow> \<exists>f\<in>R. f ` s \<subseteq> {0..1} \<and> (\<forall>t \<in> s \<inter> V. f t < e) \<and> (\<forall>t \<in> s - U. 1 - e < f t)" |
|
420 using q01 |
|
421 by (rule_tac x="\<lambda>x. 1 - q (NN e) x" in bexI) (auto simp: algebra_simps intro: diff const qR) |
|
422 moreover have t0V: "t0 \<in> V" "s \<inter> V \<subseteq> U" |
|
423 using pt_\<delta> t0 U V \<delta>01 by fastforce+ |
|
424 ultimately show ?thesis using V t0V |
|
425 by blast |
|
426 qed |
|
427 |
|
428 text\<open>Non-trivial case, with @{term A} and @{term B} both non-empty\<close> |
|
429 lemma (in function_ring_on) two_special: |
|
430 assumes A: "closed A" "A \<subseteq> s" "a \<in> A" |
|
431 and B: "closed B" "B \<subseteq> s" "b \<in> B" |
|
432 and disj: "A \<inter> B = {}" |
|
433 and e: "0 < e" "e < 1" |
|
434 shows "\<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> A. f x < e) \<and> (\<forall>x \<in> B. f x > 1 - e)" |
|
435 proof - |
|
436 { fix w |
|
437 assume "w \<in> A" |
|
438 then have "open ( - B)" "b \<in> s" "w \<notin> B" "w \<in> s" |
|
439 using assms by auto |
|
440 then have "\<exists>V. open V \<and> w \<in> V \<and> s \<inter> V \<subseteq> -B \<and> |
|
441 (\<forall>e>0. \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> s \<inter> V. f x < e) \<and> (\<forall>x \<in> s \<inter> B. f x > 1 - e))" |
|
442 using one [of "-B" w b] assms \<open>w \<in> A\<close> by simp |
|
443 } |
|
444 then obtain Vf where Vf: |
|
445 "\<And>w. w \<in> A \<Longrightarrow> open (Vf w) \<and> w \<in> Vf w \<and> s \<inter> Vf w \<subseteq> -B \<and> |
|
446 (\<forall>e>0. \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> s \<inter> Vf w. f x < e) \<and> (\<forall>x \<in> s \<inter> B. f x > 1 - e))" |
|
447 by metis |
|
448 then have open_Vf: "\<And>w. w \<in> A \<Longrightarrow> open (Vf w)" |
|
449 by blast |
|
450 have tVft: "\<And>w. w \<in> A \<Longrightarrow> w \<in> Vf w" |
|
451 using Vf by blast |
|
452 then have setsum_max_0: "A \<subseteq> (\<Union>x \<in> A. Vf x)" |
|
453 by blast |
|
454 have com_A: "compact A" using A |
|
455 by (metis compact compact_Int_closed inf.absorb_iff2) |
|
456 obtain subA where subA: "subA \<subseteq> A" "finite subA" "A \<subseteq> (\<Union>x \<in> subA. Vf x)" |
|
457 by (blast intro: that open_Vf compactE_image [OF com_A _ setsum_max_0]) |
|
458 then have [simp]: "subA \<noteq> {}" |
|
459 using \<open>a \<in> A\<close> by auto |
|
460 then have cardp: "card subA > 0" using subA |
|
461 by (simp add: card_gt_0_iff) |
|
462 have "\<And>w. w \<in> A \<Longrightarrow> \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> s \<inter> Vf w. f x < e / card subA) \<and> (\<forall>x \<in> s \<inter> B. f x > 1 - e / card subA)" |
|
463 using Vf e cardp by simp |
|
464 then obtain ff where ff: |
|
465 "\<And>w. w \<in> A \<Longrightarrow> ff w \<in> R \<and> ff w ` s \<subseteq> {0..1} \<and> |
|
466 (\<forall>x \<in> s \<inter> Vf w. ff w x < e / card subA) \<and> (\<forall>x \<in> s \<inter> B. ff w x > 1 - e / card subA)" |
|
467 by metis |
|
468 define pff where [abs_def]: "pff x = (\<Prod>w \<in> subA. ff w x)" for x |
|
469 have pffR: "pff \<in> R" |
|
470 unfolding pff_def using subA ff by (auto simp: intro: setprod) |
|
471 moreover |
|
472 have pff01: "pff x \<in> {0..1}" if t: "x \<in> s" for x |
|
473 proof - |
|
474 have "0 \<le> pff x" |
|
475 using subA cardp t |
|
476 apply (simp add: pff_def divide_simps setsum_nonneg) |
|
477 apply (rule Groups_Big.linordered_semidom_class.setprod_nonneg) |
|
478 using ff by fastforce |
|
479 moreover have "pff x \<le> 1" |
|
480 using subA cardp t |
|
481 apply (simp add: pff_def divide_simps setsum_nonneg) |
|
482 apply (rule setprod_mono [where g = "\<lambda>x. 1", simplified]) |
|
483 using ff by fastforce |
|
484 ultimately show ?thesis |
|
485 by auto |
|
486 qed |
|
487 moreover |
|
488 { fix v x |
|
489 assume v: "v \<in> subA" and x: "x \<in> Vf v" "x \<in> s" |
|
490 from subA v have "pff x = ff v x * (\<Prod>w \<in> subA - {v}. ff w x)" |
|
491 unfolding pff_def by (metis setprod.remove) |
|
492 also have "... \<le> ff v x * 1" |
|
493 apply (rule Rings.ordered_semiring_class.mult_left_mono) |
|
494 apply (rule setprod_mono [where g = "\<lambda>x. 1", simplified]) |
|
495 using ff [THEN conjunct2, THEN conjunct1] v subA x |
|
496 apply auto |
|
497 apply (meson atLeastAtMost_iff contra_subsetD imageI) |
|
498 apply (meson atLeastAtMost_iff contra_subsetD image_eqI) |
|
499 using atLeastAtMost_iff by blast |
|
500 also have "... < e / card subA" |
|
501 using ff [THEN conjunct2, THEN conjunct2, THEN conjunct1] v subA x |
|
502 by auto |
|
503 also have "... \<le> e" |
|
504 using cardp e by (simp add: divide_simps) |
|
505 finally have "pff x < e" . |
|
506 } |
|
507 then have "\<And>x. x \<in> A \<Longrightarrow> pff x < e" |
|
508 using A Vf subA by (metis UN_E contra_subsetD) |
|
509 moreover |
|
510 { fix x |
|
511 assume x: "x \<in> B" |
|
512 then have "x \<in> s" |
|
513 using B by auto |
|
514 have "1 - e \<le> (1 - e / card subA) ^ card subA" |
|
515 using Bernoulli_inequality [of "-e / card subA" "card subA"] e cardp |
|
516 by (auto simp: field_simps) |
|
517 also have "... = (\<Prod>w \<in> subA. 1 - e / card subA)" |
|
518 by (simp add: setprod_constant subA(2)) |
|
519 also have "... < pff x" |
|
520 apply (simp add: pff_def) |
|
521 apply (rule setprod_mono_strict [where f = "\<lambda>x. 1 - e / card subA", simplified]) |
|
522 apply (simp_all add: subA(2)) |
|
523 apply (intro ballI conjI) |
|
524 using e apply (force simp: divide_simps) |
|
525 using ff [THEN conjunct2, THEN conjunct2, THEN conjunct2] subA B x |
|
526 apply blast |
|
527 done |
|
528 finally have "1 - e < pff x" . |
|
529 } |
|
530 ultimately |
|
531 show ?thesis by blast |
|
532 qed |
|
533 |
|
534 lemma (in function_ring_on) two: |
|
535 assumes A: "closed A" "A \<subseteq> s" |
|
536 and B: "closed B" "B \<subseteq> s" |
|
537 and disj: "A \<inter> B = {}" |
|
538 and e: "0 < e" "e < 1" |
|
539 shows "\<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> A. f x < e) \<and> (\<forall>x \<in> B. f x > 1 - e)" |
|
540 proof (cases "A \<noteq> {} \<and> B \<noteq> {}") |
|
541 case True then show ?thesis |
|
542 apply (simp add: ex_in_conv [symmetric]) |
|
543 using assms |
|
544 apply safe |
|
545 apply (force simp add: intro!: two_special) |
|
546 done |
|
547 next |
|
548 case False with e show ?thesis |
|
549 apply simp |
|
550 apply (erule disjE) |
|
551 apply (rule_tac [2] x="\<lambda>x. 0" in bexI) |
|
552 apply (rule_tac x="\<lambda>x. 1" in bexI) |
|
553 apply (auto simp: const) |
|
554 done |
|
555 qed |
|
556 |
|
557 text\<open>The special case where @{term f} is non-negative and @{term"e<1/3"}\<close> |
|
558 lemma (in function_ring_on) Stone_Weierstrass_special: |
|
559 assumes f: "continuous_on s f" and fpos: "\<And>x. x \<in> s \<Longrightarrow> f x \<ge> 0" |
|
560 and e: "0 < e" "e < 1/3" |
|
561 shows "\<exists>g \<in> R. \<forall>x\<in>s. \<bar>f x - g x\<bar> < 2*e" |
|
562 proof - |
|
563 define n where "n = 1 + nat \<lceil>normf f / e\<rceil>" |
|
564 define A where "A j = {x \<in> s. f x \<le> (j - 1/3)*e}" for j :: nat |
|
565 define B where "B j = {x \<in> s. f x \<ge> (j + 1/3)*e}" for j :: nat |
|
566 have ngt: "(n-1) * e \<ge> normf f" "n\<ge>1" |
|
567 using e |
|
568 apply (simp_all add: n_def field_simps of_nat_Suc) |
|
569 by (metis real_nat_ceiling_ge mult.commute not_less pos_less_divide_eq) |
|
570 then have ge_fx: "(n-1) * e \<ge> f x" if "x \<in> s" for x |
|
571 using f normf_upper that by fastforce |
|
572 { fix j |
|
573 have A: "closed (A j)" "A j \<subseteq> s" |
|
574 apply (simp_all add: A_def Collect_restrict) |
|
575 apply (rule continuous_on_closed_Collect_le [OF f continuous_on_const]) |
|
576 apply (simp add: compact compact_imp_closed) |
|
577 done |
|
578 have B: "closed (B j)" "B j \<subseteq> s" |
|
579 apply (simp_all add: B_def Collect_restrict) |
|
580 apply (rule continuous_on_closed_Collect_le [OF continuous_on_const f]) |
|
581 apply (simp add: compact compact_imp_closed) |
|
582 done |
|
583 have disj: "(A j) \<inter> (B j) = {}" |
|
584 using e by (auto simp: A_def B_def field_simps) |
|
585 have "\<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> A j. f x < e/n) \<and> (\<forall>x \<in> B j. f x > 1 - e/n)" |
|
586 apply (rule two) |
|
587 using e A B disj ngt |
|
588 apply simp_all |
|
589 done |
|
590 } |
|
591 then obtain xf where xfR: "\<And>j. xf j \<in> R" and xf01: "\<And>j. xf j ` s \<subseteq> {0..1}" |
|
592 and xfA: "\<And>x j. x \<in> A j \<Longrightarrow> xf j x < e/n" |
|
593 and xfB: "\<And>x j. x \<in> B j \<Longrightarrow> xf j x > 1 - e/n" |
|
594 by metis |
|
595 define g where [abs_def]: "g x = e * (\<Sum>i\<le>n. xf i x)" for x |
|
596 have gR: "g \<in> R" |
|
597 unfolding g_def by (fast intro: mult const setsum xfR) |
|
598 have gge0: "\<And>x. x \<in> s \<Longrightarrow> g x \<ge> 0" |
|
599 using e xf01 by (simp add: g_def zero_le_mult_iff image_subset_iff setsum_nonneg) |
|
600 have A0: "A 0 = {}" |
|
601 using fpos e by (fastforce simp: A_def) |
|
602 have An: "A n = s" |
|
603 using e ngt f normf_upper by (fastforce simp: A_def field_simps of_nat_diff) |
|
604 have Asub: "A j \<subseteq> A i" if "i\<ge>j" for i j |
|
605 using e that apply (clarsimp simp: A_def) |
|
606 apply (erule order_trans, simp) |
|
607 done |
|
608 { fix t |
|
609 assume t: "t \<in> s" |
|
610 define j where "j = (LEAST j. t \<in> A j)" |
|
611 have jn: "j \<le> n" |
|
612 using t An by (simp add: Least_le j_def) |
|
613 have Aj: "t \<in> A j" |
|
614 using t An by (fastforce simp add: j_def intro: LeastI) |
|
615 then have Ai: "t \<in> A i" if "i\<ge>j" for i |
|
616 using Asub [OF that] by blast |
|
617 then have fj1: "f t \<le> (j - 1/3)*e" |
|
618 by (simp add: A_def) |
|
619 then have Anj: "t \<notin> A i" if "i<j" for i |
|
620 using Aj \<open>i<j\<close> |
|
621 apply (simp add: j_def) |
|
622 using not_less_Least by blast |
|
623 have j1: "1 \<le> j" |
|
624 using A0 Aj j_def not_less_eq_eq by (fastforce simp add: j_def) |
|
625 then have Anj: "t \<notin> A (j-1)" |
|
626 using Least_le by (fastforce simp add: j_def) |
|
627 then have fj2: "(j - 4/3)*e < f t" |
|
628 using j1 t by (simp add: A_def of_nat_diff) |
|
629 have ***: "xf i t \<le> e/n" if "i\<ge>j" for i |
|
630 using xfA [OF Ai] that by (simp add: less_eq_real_def) |
|
631 { fix i |
|
632 assume "i+2 \<le> j" |
|
633 then obtain d where "i+2+d = j" |
|
634 using le_Suc_ex that by blast |
|
635 then have "t \<in> B i" |
|
636 using Anj e ge_fx [OF t] \<open>1 \<le> n\<close> fpos [OF t] t |
|
637 apply (simp add: A_def B_def) |
|
638 apply (clarsimp simp add: field_simps of_nat_diff not_le of_nat_Suc) |
|
639 apply (rule order_trans [of _ "e * 2 + (e * (real d * 3) + e * (real i * 3))"]) |
|
640 apply auto |
|
641 done |
|
642 then have "xf i t > 1 - e/n" |
|
643 by (rule xfB) |
|
644 } note **** = this |
|
645 have xf_le1: "\<And>i. xf i t \<le> 1" |
|
646 using xf01 t by force |
|
647 have "g t = e * (\<Sum>i<j. xf i t) + e * (\<Sum>i=j..n. xf i t)" |
|
648 using j1 jn e |
|
649 apply (simp add: g_def distrib_left [symmetric]) |
|
650 apply (subst setsum.union_disjoint [symmetric]) |
|
651 apply (auto simp: ivl_disj_un) |
|
652 done |
|
653 also have "... \<le> e*j + e * ((Suc n - j)*e/n)" |
|
654 apply (rule add_mono) |
|
655 apply (simp_all only: mult_le_cancel_left_pos e) |
|
656 apply (rule setsum_bounded_above [OF xf_le1, where A = "lessThan j", simplified]) |
|
657 using setsum_bounded_above [of "{j..n}" "\<lambda>i. xf i t", OF ***] |
|
658 apply simp |
|
659 done |
|
660 also have "... \<le> j*e + e*(n - j + 1)*e/n " |
|
661 using \<open>1 \<le> n\<close> e by (simp add: field_simps del: of_nat_Suc) |
|
662 also have "... \<le> j*e + e*e" |
|
663 using \<open>1 \<le> n\<close> e j1 by (simp add: field_simps del: of_nat_Suc) |
|
664 also have "... < (j + 1/3)*e" |
|
665 using e by (auto simp: field_simps) |
|
666 finally have gj1: "g t < (j + 1 / 3) * e" . |
|
667 have gj2: "(j - 4/3)*e < g t" |
|
668 proof (cases "2 \<le> j") |
|
669 case False |
|
670 then have "j=1" using j1 by simp |
|
671 with t gge0 e show ?thesis by force |
|
672 next |
|
673 case True |
|
674 then have "(j - 4/3)*e < (j-1)*e - e^2" |
|
675 using e by (auto simp: of_nat_diff algebra_simps power2_eq_square) |
|
676 also have "... < (j-1)*e - ((j - 1)/n) * e^2" |
|
677 using e True jn by (simp add: power2_eq_square field_simps) |
|
678 also have "... = e * (j-1) * (1 - e/n)" |
|
679 by (simp add: power2_eq_square field_simps) |
|
680 also have "... \<le> e * (\<Sum>i\<le>j-2. xf i t)" |
|
681 using e |
|
682 apply simp |
|
683 apply (rule order_trans [OF _ setsum_bounded_below [OF less_imp_le [OF ****]]]) |
|
684 using True |
|
685 apply (simp_all add: of_nat_Suc of_nat_diff) |
|
686 done |
|
687 also have "... \<le> g t" |
|
688 using jn e |
|
689 using e xf01 t |
|
690 apply (simp add: g_def zero_le_mult_iff image_subset_iff setsum_nonneg) |
|
691 apply (rule Groups_Big.setsum_mono2, auto) |
|
692 done |
|
693 finally show ?thesis . |
|
694 qed |
|
695 have "\<bar>f t - g t\<bar> < 2 * e" |
|
696 using fj1 fj2 gj1 gj2 by (simp add: abs_less_iff field_simps) |
|
697 } |
|
698 then show ?thesis |
|
699 by (rule_tac x=g in bexI) (auto intro: gR) |
|
700 qed |
|
701 |
|
702 text\<open>The ``unpretentious'' formulation\<close> |
|
703 lemma (in function_ring_on) Stone_Weierstrass_basic: |
|
704 assumes f: "continuous_on s f" and e: "e > 0" |
|
705 shows "\<exists>g \<in> R. \<forall>x\<in>s. \<bar>f x - g x\<bar> < e" |
|
706 proof - |
|
707 have "\<exists>g \<in> R. \<forall>x\<in>s. \<bar>(f x + normf f) - g x\<bar> < 2 * min (e/2) (1/4)" |
|
708 apply (rule Stone_Weierstrass_special) |
|
709 apply (rule Limits.continuous_on_add [OF f Topological_Spaces.continuous_on_const]) |
|
710 using normf_upper [OF f] apply force |
|
711 apply (simp add: e, linarith) |
|
712 done |
|
713 then obtain g where "g \<in> R" "\<forall>x\<in>s. \<bar>g x - (f x + normf f)\<bar> < e" |
|
714 by force |
|
715 then show ?thesis |
|
716 apply (rule_tac x="\<lambda>x. g x - normf f" in bexI) |
|
717 apply (auto simp: algebra_simps intro: diff const) |
|
718 done |
|
719 qed |
|
720 |
|
721 |
|
722 theorem (in function_ring_on) Stone_Weierstrass: |
|
723 assumes f: "continuous_on s f" |
|
724 shows "\<exists>F\<in>UNIV \<rightarrow> R. LIM n sequentially. F n :> uniformly_on s f" |
|
725 proof - |
|
726 { fix e::real |
|
727 assume e: "0 < e" |
|
728 then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e" |
|
729 by (auto simp: real_arch_inverse [of e]) |
|
730 { fix n :: nat and x :: 'a and g :: "'a \<Rightarrow> real" |
|
731 assume n: "N \<le> n" "\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + real n)" |
|
732 assume x: "x \<in> s" |
|
733 have "\<not> real (Suc n) < inverse e" |
|
734 using \<open>N \<le> n\<close> N using less_imp_inverse_less by force |
|
735 then have "1 / (1 + real n) \<le> e" |
|
736 using e by (simp add: field_simps of_nat_Suc) |
|
737 then have "\<bar>f x - g x\<bar> < e" |
|
738 using n(2) x by auto |
|
739 } note * = this |
|
740 have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<bar>f x - (SOME g. g \<in> R \<and> (\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + real n))) x\<bar> < e" |
|
741 apply (rule eventually_sequentiallyI [of N]) |
|
742 apply (auto intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]] *) |
|
743 done |
|
744 } then |
|
745 show ?thesis |
|
746 apply (rule_tac x="\<lambda>n::nat. SOME g. g \<in> R \<and> (\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + n))" in bexI) |
|
747 prefer 2 apply (force intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]]) |
|
748 unfolding uniform_limit_iff |
|
749 apply (auto simp: dist_norm abs_minus_commute) |
|
750 done |
|
751 qed |
|
752 |
|
753 text\<open>A HOL Light formulation\<close> |
|
754 corollary Stone_Weierstrass_HOL: |
|
755 fixes R :: "('a::t2_space \<Rightarrow> real) set" and s :: "'a set" |
|
756 assumes "compact s" "\<And>c. P(\<lambda>x. c::real)" |
|
757 "\<And>f. P f \<Longrightarrow> continuous_on s f" |
|
758 "\<And>f g. P(f) \<and> P(g) \<Longrightarrow> P(\<lambda>x. f x + g x)" "\<And>f g. P(f) \<and> P(g) \<Longrightarrow> P(\<lambda>x. f x * g x)" |
|
759 "\<And>x y. x \<in> s \<and> y \<in> s \<and> ~(x = y) \<Longrightarrow> \<exists>f. P(f) \<and> ~(f x = f y)" |
|
760 "continuous_on s f" |
|
761 "0 < e" |
|
762 shows "\<exists>g. P(g) \<and> (\<forall>x \<in> s. \<bar>f x - g x\<bar> < e)" |
|
763 proof - |
|
764 interpret PR: function_ring_on "Collect P" |
|
765 apply unfold_locales |
|
766 using assms |
|
767 by auto |
|
768 show ?thesis |
|
769 using PR.Stone_Weierstrass_basic [OF \<open>continuous_on s f\<close> \<open>0 < e\<close>] |
|
770 by blast |
|
771 qed |
|
772 |
|
773 |
|
774 subsection \<open>Polynomial functions\<close> |
|
775 |
|
776 inductive real_polynomial_function :: "('a::real_normed_vector \<Rightarrow> real) \<Rightarrow> bool" where |
|
777 linear: "bounded_linear f \<Longrightarrow> real_polynomial_function f" |
|
778 | const: "real_polynomial_function (\<lambda>x. c)" |
|
779 | add: "\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x + g x)" |
|
780 | mult: "\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x * g x)" |
|
781 |
|
782 declare real_polynomial_function.intros [intro] |
|
783 |
|
784 definition polynomial_function :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> bool" |
|
785 where |
|
786 "polynomial_function p \<equiv> (\<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f o p))" |
|
787 |
|
788 lemma real_polynomial_function_eq: "real_polynomial_function p = polynomial_function p" |
|
789 unfolding polynomial_function_def |
|
790 proof |
|
791 assume "real_polynomial_function p" |
|
792 then show " \<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f \<circ> p)" |
|
793 proof (induction p rule: real_polynomial_function.induct) |
|
794 case (linear h) then show ?case |
|
795 by (auto simp: bounded_linear_compose real_polynomial_function.linear) |
|
796 next |
|
797 case (const h) then show ?case |
|
798 by (simp add: real_polynomial_function.const) |
|
799 next |
|
800 case (add h) then show ?case |
|
801 by (force simp add: bounded_linear_def linear_add real_polynomial_function.add) |
|
802 next |
|
803 case (mult h) then show ?case |
|
804 by (force simp add: real_bounded_linear const real_polynomial_function.mult) |
|
805 qed |
|
806 next |
|
807 assume [rule_format, OF bounded_linear_ident]: "\<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f \<circ> p)" |
|
808 then show "real_polynomial_function p" |
|
809 by (simp add: o_def) |
|
810 qed |
|
811 |
|
812 lemma polynomial_function_const [iff]: "polynomial_function (\<lambda>x. c)" |
|
813 by (simp add: polynomial_function_def o_def const) |
|
814 |
|
815 lemma polynomial_function_bounded_linear: |
|
816 "bounded_linear f \<Longrightarrow> polynomial_function f" |
|
817 by (simp add: polynomial_function_def o_def bounded_linear_compose real_polynomial_function.linear) |
|
818 |
|
819 lemma polynomial_function_id [iff]: "polynomial_function(\<lambda>x. x)" |
|
820 by (simp add: polynomial_function_bounded_linear) |
|
821 |
|
822 lemma polynomial_function_add [intro]: |
|
823 "\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x + g x)" |
|
824 by (auto simp: polynomial_function_def bounded_linear_def linear_add real_polynomial_function.add o_def) |
|
825 |
|
826 lemma polynomial_function_mult [intro]: |
|
827 assumes f: "polynomial_function f" and g: "polynomial_function g" |
|
828 shows "polynomial_function (\<lambda>x. f x *\<^sub>R g x)" |
|
829 using g |
|
830 apply (auto simp: polynomial_function_def bounded_linear_def Real_Vector_Spaces.linear.scaleR const real_polynomial_function.mult o_def) |
|
831 apply (rule mult) |
|
832 using f |
|
833 apply (auto simp: real_polynomial_function_eq) |
|
834 done |
|
835 |
|
836 lemma polynomial_function_cmul [intro]: |
|
837 assumes f: "polynomial_function f" |
|
838 shows "polynomial_function (\<lambda>x. c *\<^sub>R f x)" |
|
839 by (rule polynomial_function_mult [OF polynomial_function_const f]) |
|
840 |
|
841 lemma polynomial_function_minus [intro]: |
|
842 assumes f: "polynomial_function f" |
|
843 shows "polynomial_function (\<lambda>x. - f x)" |
|
844 using polynomial_function_cmul [OF f, of "-1"] by simp |
|
845 |
|
846 lemma polynomial_function_diff [intro]: |
|
847 "\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x - g x)" |
|
848 unfolding add_uminus_conv_diff [symmetric] |
|
849 by (metis polynomial_function_add polynomial_function_minus) |
|
850 |
|
851 lemma polynomial_function_setsum [intro]: |
|
852 "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> polynomial_function (\<lambda>x. f x i)\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. setsum (f x) I)" |
|
853 by (induct I rule: finite_induct) auto |
|
854 |
|
855 lemma real_polynomial_function_minus [intro]: |
|
856 "real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. - f x)" |
|
857 using polynomial_function_minus [of f] |
|
858 by (simp add: real_polynomial_function_eq) |
|
859 |
|
860 lemma real_polynomial_function_diff [intro]: |
|
861 "\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x - g x)" |
|
862 using polynomial_function_diff [of f] |
|
863 by (simp add: real_polynomial_function_eq) |
|
864 |
|
865 lemma real_polynomial_function_setsum [intro]: |
|
866 "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> real_polynomial_function (\<lambda>x. f x i)\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. setsum (f x) I)" |
|
867 using polynomial_function_setsum [of I f] |
|
868 by (simp add: real_polynomial_function_eq) |
|
869 |
|
870 lemma real_polynomial_function_power [intro]: |
|
871 "real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. f x ^ n)" |
|
872 by (induct n) (simp_all add: const mult) |
|
873 |
|
874 lemma real_polynomial_function_compose [intro]: |
|
875 assumes f: "polynomial_function f" and g: "real_polynomial_function g" |
|
876 shows "real_polynomial_function (g o f)" |
|
877 using g |
|
878 apply (induction g rule: real_polynomial_function.induct) |
|
879 using f |
|
880 apply (simp_all add: polynomial_function_def o_def const add mult) |
|
881 done |
|
882 |
|
883 lemma polynomial_function_compose [intro]: |
|
884 assumes f: "polynomial_function f" and g: "polynomial_function g" |
|
885 shows "polynomial_function (g o f)" |
|
886 using g real_polynomial_function_compose [OF f] |
|
887 by (auto simp: polynomial_function_def o_def) |
|
888 |
|
889 lemma setsum_max_0: |
|
890 fixes x::real (*in fact "'a::comm_ring_1"*) |
|
891 shows "(\<Sum>i = 0..max m n. x^i * (if i \<le> m then a i else 0)) = (\<Sum>i = 0..m. x^i * a i)" |
|
892 proof - |
|
893 have "(\<Sum>i = 0..max m n. x^i * (if i \<le> m then a i else 0)) = (\<Sum>i = 0..max m n. (if i \<le> m then x^i * a i else 0))" |
|
894 by (auto simp: algebra_simps intro: setsum.cong) |
|
895 also have "... = (\<Sum>i = 0..m. (if i \<le> m then x^i * a i else 0))" |
|
896 by (rule setsum.mono_neutral_right) auto |
|
897 also have "... = (\<Sum>i = 0..m. x^i * a i)" |
|
898 by (auto simp: algebra_simps intro: setsum.cong) |
|
899 finally show ?thesis . |
|
900 qed |
|
901 |
|
902 lemma real_polynomial_function_imp_setsum: |
|
903 assumes "real_polynomial_function f" |
|
904 shows "\<exists>a n::nat. f = (\<lambda>x. \<Sum>i=0..n. a i * x ^ i)" |
|
905 using assms |
|
906 proof (induct f) |
|
907 case (linear f) |
|
908 then show ?case |
|
909 apply (clarsimp simp add: real_bounded_linear) |
|
910 apply (rule_tac x="\<lambda>i. if i=0 then 0 else c" in exI) |
|
911 apply (rule_tac x=1 in exI) |
|
912 apply (simp add: mult_ac) |
|
913 done |
|
914 next |
|
915 case (const c) |
|
916 show ?case |
|
917 apply (rule_tac x="\<lambda>i. c" in exI) |
|
918 apply (rule_tac x=0 in exI) |
|
919 apply (auto simp: mult_ac of_nat_Suc) |
|
920 done |
|
921 case (add f1 f2) |
|
922 then obtain a1 n1 a2 n2 where |
|
923 "f1 = (\<lambda>x. \<Sum>i = 0..n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. a2 i * x ^ i)" |
|
924 by auto |
|
925 then show ?case |
|
926 apply (rule_tac x="\<lambda>i. (if i \<le> n1 then a1 i else 0) + (if i \<le> n2 then a2 i else 0)" in exI) |
|
927 apply (rule_tac x="max n1 n2" in exI) |
|
928 using setsum_max_0 [where m=n1 and n=n2] setsum_max_0 [where m=n2 and n=n1] |
|
929 apply (simp add: setsum.distrib algebra_simps max.commute) |
|
930 done |
|
931 case (mult f1 f2) |
|
932 then obtain a1 n1 a2 n2 where |
|
933 "f1 = (\<lambda>x. \<Sum>i = 0..n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. a2 i * x ^ i)" |
|
934 by auto |
|
935 then obtain b1 b2 where |
|
936 "f1 = (\<lambda>x. \<Sum>i = 0..n1. b1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. b2 i * x ^ i)" |
|
937 "b1 = (\<lambda>i. if i\<le>n1 then a1 i else 0)" "b2 = (\<lambda>i. if i\<le>n2 then a2 i else 0)" |
|
938 by auto |
|
939 then show ?case |
|
940 apply (rule_tac x="\<lambda>i. \<Sum>k\<le>i. b1 k * b2 (i - k)" in exI) |
|
941 apply (rule_tac x="n1+n2" in exI) |
|
942 using polynomial_product [of n1 b1 n2 b2] |
|
943 apply (simp add: Set_Interval.atLeast0AtMost) |
|
944 done |
|
945 qed |
|
946 |
|
947 lemma real_polynomial_function_iff_setsum: |
|
948 "real_polynomial_function f \<longleftrightarrow> (\<exists>a n::nat. f = (\<lambda>x. \<Sum>i=0..n. a i * x ^ i))" |
|
949 apply (rule iffI) |
|
950 apply (erule real_polynomial_function_imp_setsum) |
|
951 apply (auto simp: linear mult const real_polynomial_function_power real_polynomial_function_setsum) |
|
952 done |
|
953 |
|
954 lemma polynomial_function_iff_Basis_inner: |
|
955 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" |
|
956 shows "polynomial_function f \<longleftrightarrow> (\<forall>b\<in>Basis. real_polynomial_function (\<lambda>x. inner (f x) b))" |
|
957 (is "?lhs = ?rhs") |
|
958 unfolding polynomial_function_def |
|
959 proof (intro iffI allI impI) |
|
960 assume "\<forall>h. bounded_linear h \<longrightarrow> real_polynomial_function (h \<circ> f)" |
|
961 then show ?rhs |
|
962 by (force simp add: bounded_linear_inner_left o_def) |
|
963 next |
|
964 fix h :: "'b \<Rightarrow> real" |
|
965 assume rp: "\<forall>b\<in>Basis. real_polynomial_function (\<lambda>x. f x \<bullet> b)" and h: "bounded_linear h" |
|
966 have "real_polynomial_function (h \<circ> (\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b))" |
|
967 apply (rule real_polynomial_function_compose [OF _ linear [OF h]]) |
|
968 using rp |
|
969 apply (auto simp: real_polynomial_function_eq polynomial_function_mult) |
|
970 done |
|
971 then show "real_polynomial_function (h \<circ> f)" |
|
972 by (simp add: euclidean_representation_setsum_fun) |
|
973 qed |
|
974 |
|
975 subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close> |
|
976 |
|
977 text\<open>First, we need to show that they are continous, differentiable and separable.\<close> |
|
978 |
|
979 lemma continuous_real_polymonial_function: |
|
980 assumes "real_polynomial_function f" |
|
981 shows "continuous (at x) f" |
|
982 using assms |
|
983 by (induct f) (auto simp: linear_continuous_at) |
|
984 |
|
985 lemma continuous_polymonial_function: |
|
986 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" |
|
987 assumes "polynomial_function f" |
|
988 shows "continuous (at x) f" |
|
989 apply (rule euclidean_isCont) |
|
990 using assms apply (simp add: polynomial_function_iff_Basis_inner) |
|
991 apply (force dest: continuous_real_polymonial_function intro: isCont_scaleR) |
|
992 done |
|
993 |
|
994 lemma continuous_on_polymonial_function: |
|
995 fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" |
|
996 assumes "polynomial_function f" |
|
997 shows "continuous_on s f" |
|
998 using continuous_polymonial_function [OF assms] continuous_at_imp_continuous_on |
|
999 by blast |
|
1000 |
|
1001 lemma has_real_derivative_polynomial_function: |
|
1002 assumes "real_polynomial_function p" |
|
1003 shows "\<exists>p'. real_polynomial_function p' \<and> |
|
1004 (\<forall>x. (p has_real_derivative (p' x)) (at x))" |
|
1005 using assms |
|
1006 proof (induct p) |
|
1007 case (linear p) |
|
1008 then show ?case |
|
1009 by (force simp: real_bounded_linear const intro!: derivative_eq_intros) |
|
1010 next |
|
1011 case (const c) |
|
1012 show ?case |
|
1013 by (rule_tac x="\<lambda>x. 0" in exI) auto |
|
1014 case (add f1 f2) |
|
1015 then obtain p1 p2 where |
|
1016 "real_polynomial_function p1" "\<And>x. (f1 has_real_derivative p1 x) (at x)" |
|
1017 "real_polynomial_function p2" "\<And>x. (f2 has_real_derivative p2 x) (at x)" |
|
1018 by auto |
|
1019 then show ?case |
|
1020 apply (rule_tac x="\<lambda>x. p1 x + p2 x" in exI) |
|
1021 apply (auto intro!: derivative_eq_intros) |
|
1022 done |
|
1023 case (mult f1 f2) |
|
1024 then obtain p1 p2 where |
|
1025 "real_polynomial_function p1" "\<And>x. (f1 has_real_derivative p1 x) (at x)" |
|
1026 "real_polynomial_function p2" "\<And>x. (f2 has_real_derivative p2 x) (at x)" |
|
1027 by auto |
|
1028 then show ?case |
|
1029 using mult |
|
1030 apply (rule_tac x="\<lambda>x. f1 x * p2 x + f2 x * p1 x" in exI) |
|
1031 apply (auto intro!: derivative_eq_intros) |
|
1032 done |
|
1033 qed |
|
1034 |
|
1035 lemma has_vector_derivative_polynomial_function: |
|
1036 fixes p :: "real \<Rightarrow> 'a::euclidean_space" |
|
1037 assumes "polynomial_function p" |
|
1038 shows "\<exists>p'. polynomial_function p' \<and> |
|
1039 (\<forall>x. (p has_vector_derivative (p' x)) (at x))" |
|
1040 proof - |
|
1041 { fix b :: 'a |
|
1042 assume "b \<in> Basis" |
|
1043 then |
|
1044 obtain p' where p': "real_polynomial_function p'" and pd: "\<And>x. ((\<lambda>x. p x \<bullet> b) has_real_derivative p' x) (at x)" |
|
1045 using assms [unfolded polynomial_function_iff_Basis_inner, rule_format] \<open>b \<in> Basis\<close> |
|
1046 has_real_derivative_polynomial_function |
|
1047 by blast |
|
1048 have "\<exists>q. polynomial_function q \<and> (\<forall>x. ((\<lambda>u. (p u \<bullet> b) *\<^sub>R b) has_vector_derivative q x) (at x))" |
|
1049 apply (rule_tac x="\<lambda>x. p' x *\<^sub>R b" in exI) |
|
1050 using \<open>b \<in> Basis\<close> p' |
|
1051 apply (simp add: polynomial_function_iff_Basis_inner inner_Basis) |
|
1052 apply (auto intro: derivative_eq_intros pd) |
|
1053 done |
|
1054 } |
|
1055 then obtain qf where qf: |
|
1056 "\<And>b. b \<in> Basis \<Longrightarrow> polynomial_function (qf b)" |
|
1057 "\<And>b x. b \<in> Basis \<Longrightarrow> ((\<lambda>u. (p u \<bullet> b) *\<^sub>R b) has_vector_derivative qf b x) (at x)" |
|
1058 by metis |
|
1059 show ?thesis |
|
1060 apply (subst euclidean_representation_setsum_fun [of p, symmetric]) |
|
1061 apply (rule_tac x="\<lambda>x. \<Sum>b\<in>Basis. qf b x" in exI) |
|
1062 apply (auto intro: has_vector_derivative_setsum qf) |
|
1063 done |
|
1064 qed |
|
1065 |
|
1066 lemma real_polynomial_function_separable: |
|
1067 fixes x :: "'a::euclidean_space" |
|
1068 assumes "x \<noteq> y" shows "\<exists>f. real_polynomial_function f \<and> f x \<noteq> f y" |
|
1069 proof - |
|
1070 have "real_polynomial_function (\<lambda>u. \<Sum>b\<in>Basis. (inner (x-u) b)^2)" |
|
1071 apply (rule real_polynomial_function_setsum) |
|
1072 apply (auto simp: algebra_simps real_polynomial_function_power real_polynomial_function_diff |
|
1073 const linear bounded_linear_inner_left) |
|
1074 done |
|
1075 then show ?thesis |
|
1076 apply (intro exI conjI, assumption) |
|
1077 using assms |
|
1078 apply (force simp add: euclidean_eq_iff [of x y] setsum_nonneg_eq_0_iff algebra_simps) |
|
1079 done |
|
1080 qed |
|
1081 |
|
1082 lemma Stone_Weierstrass_real_polynomial_function: |
|
1083 fixes f :: "'a::euclidean_space \<Rightarrow> real" |
|
1084 assumes "compact s" "continuous_on s f" "0 < e" |
|
1085 shows "\<exists>g. real_polynomial_function g \<and> (\<forall>x \<in> s. \<bar>f x - g x\<bar> < e)" |
|
1086 proof - |
|
1087 interpret PR: function_ring_on "Collect real_polynomial_function" |
|
1088 apply unfold_locales |
|
1089 using assms continuous_on_polymonial_function real_polynomial_function_eq |
|
1090 apply (auto intro: real_polynomial_function_separable) |
|
1091 done |
|
1092 show ?thesis |
|
1093 using PR.Stone_Weierstrass_basic [OF \<open>continuous_on s f\<close> \<open>0 < e\<close>] |
|
1094 by blast |
|
1095 qed |
|
1096 |
|
1097 lemma Stone_Weierstrass_polynomial_function: |
|
1098 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
1099 assumes s: "compact s" |
|
1100 and f: "continuous_on s f" |
|
1101 and e: "0 < e" |
|
1102 shows "\<exists>g. polynomial_function g \<and> (\<forall>x \<in> s. norm(f x - g x) < e)" |
|
1103 proof - |
|
1104 { fix b :: 'b |
|
1105 assume "b \<in> Basis" |
|
1106 have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> s. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))" |
|
1107 apply (rule exE [OF Stone_Weierstrass_real_polynomial_function [OF s _, of "\<lambda>x. f x \<bullet> b" "e / card Basis"]]) |
|
1108 using e f |
|
1109 apply (auto simp: Euclidean_Space.DIM_positive intro: continuous_intros) |
|
1110 done |
|
1111 } |
|
1112 then obtain pf where pf: |
|
1113 "\<And>b. b \<in> Basis \<Longrightarrow> real_polynomial_function (pf b) \<and> (\<forall>x \<in> s. \<bar>f x \<bullet> b - pf b x\<bar> < e / DIM('b))" |
|
1114 apply (rule bchoice [rule_format, THEN exE]) |
|
1115 apply assumption |
|
1116 apply (force simp add: intro: that) |
|
1117 done |
|
1118 have "polynomial_function (\<lambda>x. \<Sum>b\<in>Basis. pf b x *\<^sub>R b)" |
|
1119 using pf |
|
1120 by (simp add: polynomial_function_setsum polynomial_function_mult real_polynomial_function_eq) |
|
1121 moreover |
|
1122 { fix x |
|
1123 assume "x \<in> s" |
|
1124 have "norm (\<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b - pf b x *\<^sub>R b) \<le> (\<Sum>b\<in>Basis. norm ((f x \<bullet> b) *\<^sub>R b - pf b x *\<^sub>R b))" |
|
1125 by (rule norm_setsum) |
|
1126 also have "... < of_nat DIM('b) * (e / DIM('b))" |
|
1127 apply (rule setsum_bounded_above_strict) |
|
1128 apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf \<open>x \<in> s\<close>) |
|
1129 apply (rule DIM_positive) |
|
1130 done |
|
1131 also have "... = e" |
|
1132 using DIM_positive by (simp add: field_simps) |
|
1133 finally have "norm (\<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b - pf b x *\<^sub>R b) < e" . |
|
1134 } |
|
1135 ultimately |
|
1136 show ?thesis |
|
1137 apply (subst euclidean_representation_setsum_fun [of f, symmetric]) |
|
1138 apply (rule_tac x="\<lambda>x. \<Sum>b\<in>Basis. pf b x *\<^sub>R b" in exI) |
|
1139 apply (auto simp: setsum_subtractf [symmetric]) |
|
1140 done |
|
1141 qed |
|
1142 |
|
1143 |
|
1144 subsection\<open>Polynomial functions as paths\<close> |
|
1145 |
|
1146 text\<open>One application is to pick a smooth approximation to a path, |
|
1147 or just pick a smooth path anyway in an open connected set\<close> |
|
1148 |
|
1149 lemma path_polynomial_function: |
|
1150 fixes g :: "real \<Rightarrow> 'b::euclidean_space" |
|
1151 shows "polynomial_function g \<Longrightarrow> path g" |
|
1152 by (simp add: path_def continuous_on_polymonial_function) |
|
1153 |
|
1154 lemma path_approx_polynomial_function: |
|
1155 fixes g :: "real \<Rightarrow> 'b::euclidean_space" |
|
1156 assumes "path g" "0 < e" |
|
1157 shows "\<exists>p. polynomial_function p \<and> |
|
1158 pathstart p = pathstart g \<and> |
|
1159 pathfinish p = pathfinish g \<and> |
|
1160 (\<forall>t \<in> {0..1}. norm(p t - g t) < e)" |
|
1161 proof - |
|
1162 obtain q where poq: "polynomial_function q" and noq: "\<And>x. x \<in> {0..1} \<Longrightarrow> norm (g x - q x) < e/4" |
|
1163 using Stone_Weierstrass_polynomial_function [of "{0..1}" g "e/4"] assms |
|
1164 by (auto simp: path_def) |
|
1165 have pf: "polynomial_function (\<lambda>t. q t + (g 0 - q 0) + t *\<^sub>R (g 1 - q 1 - (g 0 - q 0)))" |
|
1166 by (force simp add: poq) |
|
1167 have *: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (((q t - g t) + (g 0 - q 0)) + (t *\<^sub>R (g 1 - q 1) + t *\<^sub>R (q 0 - g 0))) < (e/4 + e/4) + (e/4+e/4)" |
|
1168 apply (intro Real_Vector_Spaces.norm_add_less) |
|
1169 using noq |
|
1170 apply (auto simp: norm_minus_commute intro: le_less_trans [OF mult_left_le_one_le noq] simp del: less_divide_eq_numeral1) |
|
1171 done |
|
1172 show ?thesis |
|
1173 apply (intro exI conjI) |
|
1174 apply (rule pf) |
|
1175 using * |
|
1176 apply (auto simp add: pathstart_def pathfinish_def algebra_simps) |
|
1177 done |
|
1178 qed |
|
1179 |
|
1180 lemma connected_open_polynomial_connected: |
|
1181 fixes s :: "'a::euclidean_space set" |
|
1182 assumes s: "open s" "connected s" |
|
1183 and "x \<in> s" "y \<in> s" |
|
1184 shows "\<exists>g. polynomial_function g \<and> path_image g \<subseteq> s \<and> |
|
1185 pathstart g = x \<and> pathfinish g = y" |
|
1186 proof - |
|
1187 have "path_connected s" using assms |
|
1188 by (simp add: connected_open_path_connected) |
|
1189 with \<open>x \<in> s\<close> \<open>y \<in> s\<close> obtain p where p: "path p" "path_image p \<subseteq> s" "pathstart p = x" "pathfinish p = y" |
|
1190 by (force simp: path_connected_def) |
|
1191 have "\<exists>e. 0 < e \<and> (\<forall>x \<in> path_image p. ball x e \<subseteq> s)" |
|
1192 proof (cases "s = UNIV") |
|
1193 case True then show ?thesis |
|
1194 by (simp add: gt_ex) |
|
1195 next |
|
1196 case False |
|
1197 then have "- s \<noteq> {}" by blast |
|
1198 then show ?thesis |
|
1199 apply (rule_tac x="setdist (path_image p) (-s)" in exI) |
|
1200 using s p |
|
1201 apply (simp add: setdist_gt_0_compact_closed compact_path_image open_closed) |
|
1202 using setdist_le_dist [of _ "path_image p" _ "-s"] |
|
1203 by fastforce |
|
1204 qed |
|
1205 then obtain e where "0 < e"and eb: "\<And>x. x \<in> path_image p \<Longrightarrow> ball x e \<subseteq> s" |
|
1206 by auto |
|
1207 show ?thesis |
|
1208 using path_approx_polynomial_function [OF \<open>path p\<close> \<open>0 < e\<close>] |
|
1209 apply clarify |
|
1210 apply (intro exI conjI, assumption) |
|
1211 using p |
|
1212 apply (fastforce simp add: dist_norm path_image_def norm_minus_commute intro: eb [THEN subsetD])+ |
|
1213 done |
|
1214 qed |
|
1215 |
|
1216 hide_fact linear add mult const |
|
1217 |
|
1218 end |
|