author | paulson <lp15@cam.ac.uk> |
Wed, 26 Apr 2017 16:58:31 +0100 | |
changeset 65585 | a043de9ad41e |
parent 65583 | 8d53b3bebab4 |
child 67986 | b65c4a6a015e |
permissions | -rw-r--r-- |
61711
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset
|
1 |
section \<open>The Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close> |
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset
|
2 |
|
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset
|
3 |
text\<open>By L C Paulson (2015)\<close> |
60987 | 4 |
|
63594
bd218a9320b5
HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63040
diff
changeset
|
5 |
theory Weierstrass_Theorems |
63938 | 6 |
imports Uniform_Limit Path_Connected Derivative |
60987 | 7 |
begin |
8 |
||
61222 | 9 |
subsection \<open>Bernstein polynomials\<close> |
60987 | 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: |
|
61711
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset
|
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)" |
60987 | 26 |
apply (rule DERIV_unique [where f = "\<lambda>a. (a+b)^n" and x=a]) |
27 |
apply (subst binomial_ring) |
|
64267 | 28 |
apply (rule derivative_eq_intros sum.cong | simp)+ |
60987 | 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]) |
|
64267 | 36 |
apply (rule derivative_eq_intros sum.cong | simp add: Num.numeral_2_eq_2)+ |
60987 | 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]) |
|
64267 | 41 |
apply (simp add: sum_distrib_right) |
42 |
apply (auto simp: Bernstein_def algebra_simps realpow_num_eq_if intro!: sum.cong) |
|
60987 | 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]) |
|
64267 | 49 |
apply (simp add: sum_distrib_right) |
50 |
apply (rule sum.cong [OF refl]) |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
51 |
apply (simp add: Bernstein_def power2_eq_square algebra_simps) |
60987 | 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 |
||
61222 | 62 |
subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close> |
60987 | 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} |
|
61945 | 68 |
\<longrightarrow> \<bar>f x - (\<Sum>k = 0..n. f(k/n) * Bernstein n k x)\<bar> < e" |
60987 | 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" |
|
61222 | 84 |
using e \<open>0<d\<close> by simp |
60987 | 85 |
also have "... \<le> M * 4" |
61222 | 86 |
using \<open>0\<le>M\<close> by simp |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
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>" |
61222 | 88 |
using \<open>0\<le>M\<close> e \<open>0<d\<close> |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
89 |
by (simp add: of_nat_Suc field_simps) |
60987 | 90 |
have "4*M/(e*d\<^sup>2) + 1 \<le> real (Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>))" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
91 |
by (simp add: of_nat_Suc real_nat_ceiling_ge) |
60987 | 92 |
also have "... \<le> real n" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
93 |
using n by (simp add: of_nat_Suc field_simps) |
60987 | 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)" |
|
64267 | 100 |
apply (simp add: * sum.distrib) |
101 |
apply (simp add: sum_distrib_left [symmetric] mult.assoc) |
|
60987 | 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 |
|
64267 | 107 |
using n by (simp add: sum_divide_distrib divide_simps mult.commute power2_commute) |
60987 | 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) |
|
61945 | 113 |
consider (lessd) "\<bar>x - k / n\<bar> < d" | (ged) "d \<le> \<bar>x - k / n\<bar>" |
60987 | 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]) |
|
61222 | 134 |
using dle \<open>d>0\<close> \<open>M\<ge>0\<close> by auto |
60987 | 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>" |
|
64267 | 141 |
by (simp add: sum_subtractf sum_distrib_left [symmetric] algebra_simps) |
60987 | 142 |
also have "... \<le> (\<Sum> k = 0..n. (e/2 + (2 * M / d\<^sup>2) * (x - k / n)\<^sup>2) * Bernstein n k x)" |
64267 | 143 |
apply (rule order_trans [OF sum_abs sum_mono]) |
60987 | 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)" |
|
64267 | 148 |
apply (simp only: sum.distrib Rings.semiring_class.distrib_right sum_distrib_left [symmetric] mult.assoc sum_bern) |
61222 | 149 |
using \<open>d>0\<close> x |
60987 | 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) |
|
61222 | 154 |
using \<open>d>0\<close> nbig e \<open>n>0\<close> |
60987 | 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 |
||
61222 | 164 |
subsection \<open>General Stone-Weierstrass theorem\<close> |
60987 | 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 |
|
61711
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset
|
170 |
Volume 81, Number 1, January 1981. |
21d7910d6816
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
paulson <lp15@cam.ac.uk>
parents:
61610
diff
changeset
|
171 |
DOI: 10.2307/2043993 http://www.jstor.org/stable/2043993\<close> |
60987 | 172 |
|
173 |
locale function_ring_on = |
|
63938 | 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" |
|
60987 | 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" |
|
63938 | 180 |
assumes separable: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> \<exists>f\<in>R. f x \<noteq> f y" |
60987 | 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 |
||
64267 | 192 |
lemma sum: "\<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" |
60987 | 193 |
by (induct I rule: finite_induct; simp add: const add) |
194 |
||
64272 | 195 |
lemma prod: "\<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" |
60987 | 196 |
by (induct I rule: finite_induct; simp add: const mult) |
197 |
||
198 |
definition normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real" |
|
63938 | 199 |
where "normf f \<equiv> SUP x:S. \<bar>f x\<bar>" |
60987 | 200 |
|
63938 | 201 |
lemma normf_upper: "\<lbrakk>continuous_on S f; x \<in> S\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f" |
60987 | 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 |
||
63938 | 206 |
lemma normf_least: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M" |
60987 | 207 |
by (simp add: normf_def cSUP_least) |
208 |
||
209 |
end |
|
210 |
||
211 |
lemma (in function_ring_on) one: |
|
63938 | 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))" |
|
60987 | 215 |
proof - |
63938 | 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 |
60987 | 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) |
|
63040 | 221 |
define h where [abs_def]: "h x = g x - g t0" for x |
60987 | 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)" . |
|
63040 | 235 |
define p where [abs_def]: "p x = (1 / normf (\<lambda>w. (h w)\<^sup>2)) * (h x)^2" for x |
60987 | 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) |
|
63938 | 242 |
moreover have "\<And>x. x \<in> S \<Longrightarrow> p x \<in> {0..1}" |
60987 | 243 |
using nfp normf_upper [OF continuous [OF hsq] ] by (auto simp: p_def) |
63938 | 244 |
ultimately show "\<exists>pt \<in> R. pt t0 = 0 \<and> pt t > 0 \<and> pt ` S \<subseteq> {0..1}" |
60987 | 245 |
by auto |
246 |
qed |
|
63938 | 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}" |
|
60987 | 249 |
by metis |
63938 | 250 |
have com_sU: "compact (S-U)" |
62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset
|
251 |
using compact closed_Int_compact U by (simp add: Diff_eq compact_Int_closed open_closed) |
63938 | 252 |
have "\<And>t. t \<in> S-U \<Longrightarrow> \<exists>A. open A \<and> A \<inter> S = {x\<in>S. 0 < pf t x}" |
60987 | 253 |
apply (rule open_Collect_positive) |
254 |
by (metis pf continuous) |
|
63938 | 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}" |
60987 | 256 |
by metis |
63938 | 257 |
then have open_Uf: "\<And>t. t \<in> S-U \<Longrightarrow> open (Uf t)" |
60987 | 258 |
by blast |
63938 | 259 |
have tUft: "\<And>t. t \<in> S-U \<Longrightarrow> t \<in> Uf t" |
60987 | 260 |
using pf Uf by blast |
63938 | 261 |
then have *: "S-U \<subseteq> (\<Union>x \<in> S-U. Uf x)" |
60987 | 262 |
by blast |
63938 | 263 |
obtain subU where subU: "subU \<subseteq> S - U" "finite subU" "S - U \<subseteq> (\<Union>x \<in> subU. Uf x)" |
65585
a043de9ad41e
Some fixes related to compactE_image
paulson <lp15@cam.ac.uk>
parents:
65583
diff
changeset
|
264 |
by (blast intro: that compactE_image [OF com_sU open_Uf *]) |
60987 | 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) |
|
63040 | 269 |
define p where [abs_def]: "p x = (1 / card subU) * (\<Sum>t \<in> subU. pf t x)" for x |
60987 | 270 |
have pR: "p \<in> R" |
64267 | 271 |
unfolding p_def using subU pf by (fast intro: pf const mult sum) |
60987 | 272 |
have pt0 [simp]: "p t0 = 0" |
64267 | 273 |
using subU pf by (auto simp: p_def intro: sum.neutral) |
63938 | 274 |
have pt_pos: "p t > 0" if t: "t \<in> S-U" for t |
60987 | 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) |
|
64267 | 280 |
apply (rule sum_pos2 [OF \<open>finite subU\<close>]) |
60987 | 281 |
using Uf t pf01 apply auto |
282 |
apply (force elim!: subsetCE) |
|
283 |
done |
|
284 |
qed |
|
63938 | 285 |
have p01: "p x \<in> {0..1}" if t: "x \<in> S" for x |
60987 | 286 |
proof - |
287 |
have "0 \<le> p x" |
|
288 |
using subU cardp t |
|
64267 | 289 |
apply (simp add: p_def divide_simps sum_nonneg) |
290 |
apply (rule sum_nonneg) |
|
60987 | 291 |
using pf01 by force |
292 |
moreover have "p x \<le> 1" |
|
293 |
using subU cardp t |
|
64267 | 294 |
apply (simp add: p_def divide_simps sum_nonneg) |
295 |
apply (rule sum_bounded_above [where 'a=real and K=1, simplified]) |
|
60987 | 296 |
using pf01 by force |
297 |
ultimately show ?thesis |
|
298 |
by auto |
|
299 |
qed |
|
63938 | 300 |
have "compact (p ` (S-U))" |
60987 | 301 |
by (meson Diff_subset com_sU compact_continuous_image continuous continuous_on_subset pR) |
63938 | 302 |
then have "open (- (p ` (S-U)))" |
60987 | 303 |
by (simp add: compact_imp_closed open_Compl) |
63938 | 304 |
moreover have "0 \<in> - (p ` (S-U))" |
60987 | 305 |
by (metis (no_types) ComplI image_iff not_less_iff_gr_or_eq pt_pos) |
63938 | 306 |
ultimately obtain delta0 where delta0: "delta0 > 0" "ball 0 delta0 \<subseteq> - (p ` (S-U))" |
60987 | 307 |
by (auto simp: elim!: openE) |
63938 | 308 |
then have pt_delta: "\<And>x. x \<in> S-U \<Longrightarrow> p x \<ge> delta0" |
60987 | 309 |
by (force simp: ball_def dist_norm dest: p01) |
63040 | 310 |
define \<delta> where "\<delta> = delta0/2" |
60987 | 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) |
|
63938 | 315 |
have pt_\<delta>: "\<And>x. x \<in> S-U \<Longrightarrow> p x \<ge> \<delta>" |
60987 | 316 |
using pt_delta delta0 by (force simp: \<delta>_def) |
63938 | 317 |
have "\<exists>A. open A \<and> A \<inter> S = {x\<in>S. p x < \<delta>/2}" |
60987 | 318 |
by (rule open_Collect_less_Int [OF continuous [OF pR] continuous_on_const]) |
63938 | 319 |
then obtain V where V: "open V" "V \<inter> S = {x\<in>S. p x < \<delta>/2}" |
60987 | 320 |
by blast |
63040 | 321 |
define k where "k = nat\<lfloor>1/\<delta>\<rfloor> + 1" |
60987 | 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) |
|
63040 | 334 |
define q where [abs_def]: "q n t = (1 - p t ^ n) ^ (k^n)" for n t |
60987 | 335 |
have qR: "q n \<in> R" for n |
336 |
by (simp add: q_def const diff power pR) |
|
63938 | 337 |
have q01: "\<And>n t. t \<in> S \<Longrightarrow> q n t \<in> {0..1}" |
60987 | 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 |
|
63938 | 342 |
assume t: "t \<in> S \<inter> V" |
61222 | 343 |
with \<open>k>0\<close> V have "k * p t < k * \<delta> / 2" |
60987 | 344 |
by force |
345 |
then have "1 - (k * \<delta> / 2)^n \<le> 1 - (k * p t)^n" |
|
61222 | 346 |
using \<open>k>0\<close> p01 t by (simp add: power_mono) |
60987 | 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 |
|
63938 | 354 |
assume t: "t \<in> S - U" |
61222 | 355 |
with \<open>k>0\<close> U have "k * \<delta> \<le> k * p t" |
60987 | 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" |
|
61222 | 364 |
using pt_pos [OF t] \<open>k>0\<close> by (simp add: q_def) |
60987 | 365 |
also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + k^n * (p t)^n)" |
61222 | 366 |
using pt_pos [OF t] \<open>k>0\<close> |
60987 | 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"]]) |
|
61222 | 375 |
using \<open>k>0\<close> ptn_pos ptn_le |
60987 | 376 |
apply (auto simp: power_mult_distrib) |
377 |
done |
|
378 |
also have "... = (1/(k * (p t))^n) * (1 - p t ^ (2*n)) ^ (k^n)" |
|
61222 | 379 |
using pt_pos [OF t] \<open>k>0\<close> |
60987 | 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]) |
|
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61711
diff
changeset
|
383 |
using pt_pos \<open>k>0\<close> p01 power_le_one t apply auto |
60987 | 384 |
done |
385 |
also have "... \<le> (1 / (k*\<delta>))^n" |
|
61222 | 386 |
using \<open>k>0\<close> \<delta>01 power_mono pt_\<delta> t |
60987 | 387 |
by (fastforce simp: field_simps) |
388 |
finally have "q n t \<le> (1 / (real k * \<delta>)) ^ n " . |
|
389 |
} note limitNonU = this |
|
63040 | 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 |
|
60987 | 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) |
|
61222 | 398 |
using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta> |
60987 | 399 |
apply (force simp add: field_simps)+ |
400 |
done |
|
65578
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
65204
diff
changeset
|
401 |
have NN0: "(1/(k*\<delta>)) ^ (NN e) < e" if "e>0" for e |
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
65204
diff
changeset
|
402 |
proof - |
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
65204
diff
changeset
|
403 |
have "0 < ln (real k) + ln \<delta>" |
65585
a043de9ad41e
Some fixes related to compactE_image
paulson <lp15@cam.ac.uk>
parents:
65583
diff
changeset
|
404 |
using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero ln_mult by fastforce |
65578
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
65204
diff
changeset
|
405 |
then have "real (NN e) * ln (1 / (real k * \<delta>)) < ln e" |
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
65204
diff
changeset
|
406 |
using k\<delta>(1) NN(2) [of e] that by (simp add: ln_div divide_simps) |
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
65204
diff
changeset
|
407 |
then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e" |
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
65204
diff
changeset
|
408 |
by (metis exp_less_mono exp_ln that) |
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
65204
diff
changeset
|
409 |
then show ?thesis |
65583
8d53b3bebab4
Further new material. The simprule status of some exp and ln identities was reverted.
paulson <lp15@cam.ac.uk>
parents:
65578
diff
changeset
|
410 |
by (simp add: \<delta>01(1) \<open>0 < k\<close> exp_of_nat_mult) |
65578
e4997c181cce
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
paulson <lp15@cam.ac.uk>
parents:
65204
diff
changeset
|
411 |
qed |
60987 | 412 |
{ fix t and e::real |
413 |
assume "e>0" |
|
63938 | 414 |
have "t \<in> S \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> S - U \<Longrightarrow> q (NN e) t < e" |
60987 | 415 |
proof - |
63938 | 416 |
assume t: "t \<in> S \<inter> V" |
60987 | 417 |
show "1 - q (NN e) t < e" |
61222 | 418 |
by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF \<open>e>0\<close>]]) |
60987 | 419 |
next |
63938 | 420 |
assume t: "t \<in> S - U" |
60987 | 421 |
show "q (NN e) t < e" |
61222 | 422 |
using limitNonU [OF t] less_le_trans [OF NN0 [OF \<open>e>0\<close>]] not_le by blast |
60987 | 423 |
qed |
63938 | 424 |
} 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)" |
60987 | 425 |
using q01 |
426 |
by (rule_tac x="\<lambda>x. 1 - q (NN e) x" in bexI) (auto simp: algebra_simps intro: diff const qR) |
|
63938 | 427 |
moreover have t0V: "t0 \<in> V" "S \<inter> V \<subseteq> U" |
60987 | 428 |
using pt_\<delta> t0 U V \<delta>01 by fastforce+ |
429 |
ultimately show ?thesis using V t0V |
|
430 |
by blast |
|
431 |
qed |
|
432 |
||
433 |
text\<open>Non-trivial case, with @{term A} and @{term B} both non-empty\<close> |
|
434 |
lemma (in function_ring_on) two_special: |
|
63938 | 435 |
assumes A: "closed A" "A \<subseteq> S" "a \<in> A" |
436 |
and B: "closed B" "B \<subseteq> S" "b \<in> B" |
|
60987 | 437 |
and disj: "A \<inter> B = {}" |
438 |
and e: "0 < e" "e < 1" |
|
63938 | 439 |
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)" |
60987 | 440 |
proof - |
441 |
{ fix w |
|
442 |
assume "w \<in> A" |
|
63938 | 443 |
then have "open ( - B)" "b \<in> S" "w \<notin> B" "w \<in> S" |
60987 | 444 |
using assms by auto |
63938 | 445 |
then have "\<exists>V. open V \<and> w \<in> V \<and> S \<inter> V \<subseteq> -B \<and> |
446 |
(\<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))" |
|
61222 | 447 |
using one [of "-B" w b] assms \<open>w \<in> A\<close> by simp |
60987 | 448 |
} |
449 |
then obtain Vf where Vf: |
|
63938 | 450 |
"\<And>w. w \<in> A \<Longrightarrow> open (Vf w) \<and> w \<in> Vf w \<and> S \<inter> Vf w \<subseteq> -B \<and> |
451 |
(\<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))" |
|
60987 | 452 |
by metis |
453 |
then have open_Vf: "\<And>w. w \<in> A \<Longrightarrow> open (Vf w)" |
|
454 |
by blast |
|
455 |
have tVft: "\<And>w. w \<in> A \<Longrightarrow> w \<in> Vf w" |
|
456 |
using Vf by blast |
|
64267 | 457 |
then have sum_max_0: "A \<subseteq> (\<Union>x \<in> A. Vf x)" |
60987 | 458 |
by blast |
459 |
have com_A: "compact A" using A |
|
62843
313d3b697c9a
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
paulson <lp15@cam.ac.uk>
parents:
62623
diff
changeset
|
460 |
by (metis compact compact_Int_closed inf.absorb_iff2) |
60987 | 461 |
obtain subA where subA: "subA \<subseteq> A" "finite subA" "A \<subseteq> (\<Union>x \<in> subA. Vf x)" |
65585
a043de9ad41e
Some fixes related to compactE_image
paulson <lp15@cam.ac.uk>
parents:
65583
diff
changeset
|
462 |
by (blast intro: that compactE_image [OF com_A open_Vf sum_max_0]) |
60987 | 463 |
then have [simp]: "subA \<noteq> {}" |
61222 | 464 |
using \<open>a \<in> A\<close> by auto |
60987 | 465 |
then have cardp: "card subA > 0" using subA |
466 |
by (simp add: card_gt_0_iff) |
|
63938 | 467 |
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)" |
60987 | 468 |
using Vf e cardp by simp |
469 |
then obtain ff where ff: |
|
63938 | 470 |
"\<And>w. w \<in> A \<Longrightarrow> ff w \<in> R \<and> ff w ` S \<subseteq> {0..1} \<and> |
471 |
(\<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)" |
|
60987 | 472 |
by metis |
63040 | 473 |
define pff where [abs_def]: "pff x = (\<Prod>w \<in> subA. ff w x)" for x |
60987 | 474 |
have pffR: "pff \<in> R" |
64272 | 475 |
unfolding pff_def using subA ff by (auto simp: intro: prod) |
60987 | 476 |
moreover |
63938 | 477 |
have pff01: "pff x \<in> {0..1}" if t: "x \<in> S" for x |
60987 | 478 |
proof - |
479 |
have "0 \<le> pff x" |
|
480 |
using subA cardp t |
|
64267 | 481 |
apply (simp add: pff_def divide_simps sum_nonneg) |
64272 | 482 |
apply (rule Groups_Big.linordered_semidom_class.prod_nonneg) |
60987 | 483 |
using ff by fastforce |
484 |
moreover have "pff x \<le> 1" |
|
485 |
using subA cardp t |
|
64267 | 486 |
apply (simp add: pff_def divide_simps sum_nonneg) |
64272 | 487 |
apply (rule prod_mono [where g = "\<lambda>x. 1", simplified]) |
60987 | 488 |
using ff by fastforce |
489 |
ultimately show ?thesis |
|
490 |
by auto |
|
491 |
qed |
|
492 |
moreover |
|
493 |
{ fix v x |
|
63938 | 494 |
assume v: "v \<in> subA" and x: "x \<in> Vf v" "x \<in> S" |
60987 | 495 |
from subA v have "pff x = ff v x * (\<Prod>w \<in> subA - {v}. ff w x)" |
64272 | 496 |
unfolding pff_def by (metis prod.remove) |
60987 | 497 |
also have "... \<le> ff v x * 1" |
498 |
apply (rule Rings.ordered_semiring_class.mult_left_mono) |
|
64272 | 499 |
apply (rule prod_mono [where g = "\<lambda>x. 1", simplified]) |
60987 | 500 |
using ff [THEN conjunct2, THEN conjunct1] v subA x |
501 |
apply auto |
|
502 |
apply (meson atLeastAtMost_iff contra_subsetD imageI) |
|
503 |
apply (meson atLeastAtMost_iff contra_subsetD image_eqI) |
|
504 |
using atLeastAtMost_iff by blast |
|
505 |
also have "... < e / card subA" |
|
506 |
using ff [THEN conjunct2, THEN conjunct2, THEN conjunct1] v subA x |
|
507 |
by auto |
|
508 |
also have "... \<le> e" |
|
509 |
using cardp e by (simp add: divide_simps) |
|
510 |
finally have "pff x < e" . |
|
511 |
} |
|
512 |
then have "\<And>x. x \<in> A \<Longrightarrow> pff x < e" |
|
513 |
using A Vf subA by (metis UN_E contra_subsetD) |
|
514 |
moreover |
|
515 |
{ fix x |
|
516 |
assume x: "x \<in> B" |
|
63938 | 517 |
then have "x \<in> S" |
60987 | 518 |
using B by auto |
519 |
have "1 - e \<le> (1 - e / card subA) ^ card subA" |
|
520 |
using Bernoulli_inequality [of "-e / card subA" "card subA"] e cardp |
|
521 |
by (auto simp: field_simps) |
|
522 |
also have "... = (\<Prod>w \<in> subA. 1 - e / card subA)" |
|
64272 | 523 |
by (simp add: prod_constant subA(2)) |
60987 | 524 |
also have "... < pff x" |
525 |
apply (simp add: pff_def) |
|
64272 | 526 |
apply (rule prod_mono_strict [where f = "\<lambda>x. 1 - e / card subA", simplified]) |
60987 | 527 |
apply (simp_all add: subA(2)) |
528 |
apply (intro ballI conjI) |
|
529 |
using e apply (force simp: divide_simps) |
|
530 |
using ff [THEN conjunct2, THEN conjunct2, THEN conjunct2] subA B x |
|
531 |
apply blast |
|
532 |
done |
|
533 |
finally have "1 - e < pff x" . |
|
534 |
} |
|
535 |
ultimately |
|
536 |
show ?thesis by blast |
|
537 |
qed |
|
538 |
||
539 |
lemma (in function_ring_on) two: |
|
63938 | 540 |
assumes A: "closed A" "A \<subseteq> S" |
541 |
and B: "closed B" "B \<subseteq> S" |
|
60987 | 542 |
and disj: "A \<inter> B = {}" |
543 |
and e: "0 < e" "e < 1" |
|
63938 | 544 |
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)" |
60987 | 545 |
proof (cases "A \<noteq> {} \<and> B \<noteq> {}") |
546 |
case True then show ?thesis |
|
547 |
apply (simp add: ex_in_conv [symmetric]) |
|
548 |
using assms |
|
549 |
apply safe |
|
550 |
apply (force simp add: intro!: two_special) |
|
551 |
done |
|
552 |
next |
|
553 |
case False with e show ?thesis |
|
554 |
apply simp |
|
555 |
apply (erule disjE) |
|
556 |
apply (rule_tac [2] x="\<lambda>x. 0" in bexI) |
|
557 |
apply (rule_tac x="\<lambda>x. 1" in bexI) |
|
558 |
apply (auto simp: const) |
|
559 |
done |
|
560 |
qed |
|
561 |
||
562 |
text\<open>The special case where @{term f} is non-negative and @{term"e<1/3"}\<close> |
|
563 |
lemma (in function_ring_on) Stone_Weierstrass_special: |
|
63938 | 564 |
assumes f: "continuous_on S f" and fpos: "\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0" |
60987 | 565 |
and e: "0 < e" "e < 1/3" |
63938 | 566 |
shows "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>f x - g x\<bar> < 2*e" |
60987 | 567 |
proof - |
63040 | 568 |
define n where "n = 1 + nat \<lceil>normf f / e\<rceil>" |
63938 | 569 |
define A where "A j = {x \<in> S. f x \<le> (j - 1/3)*e}" for j :: nat |
570 |
define B where "B j = {x \<in> S. f x \<ge> (j + 1/3)*e}" for j :: nat |
|
60987 | 571 |
have ngt: "(n-1) * e \<ge> normf f" "n\<ge>1" |
572 |
using e |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
573 |
apply (simp_all add: n_def field_simps of_nat_Suc) |
60987 | 574 |
by (metis real_nat_ceiling_ge mult.commute not_less pos_less_divide_eq) |
63938 | 575 |
then have ge_fx: "(n-1) * e \<ge> f x" if "x \<in> S" for x |
60987 | 576 |
using f normf_upper that by fastforce |
577 |
{ fix j |
|
63938 | 578 |
have A: "closed (A j)" "A j \<subseteq> S" |
60987 | 579 |
apply (simp_all add: A_def Collect_restrict) |
580 |
apply (rule continuous_on_closed_Collect_le [OF f continuous_on_const]) |
|
581 |
apply (simp add: compact compact_imp_closed) |
|
582 |
done |
|
63938 | 583 |
have B: "closed (B j)" "B j \<subseteq> S" |
60987 | 584 |
apply (simp_all add: B_def Collect_restrict) |
585 |
apply (rule continuous_on_closed_Collect_le [OF continuous_on_const f]) |
|
586 |
apply (simp add: compact compact_imp_closed) |
|
587 |
done |
|
588 |
have disj: "(A j) \<inter> (B j) = {}" |
|
589 |
using e by (auto simp: A_def B_def field_simps) |
|
63938 | 590 |
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)" |
60987 | 591 |
apply (rule two) |
592 |
using e A B disj ngt |
|
593 |
apply simp_all |
|
594 |
done |
|
595 |
} |
|
63938 | 596 |
then obtain xf where xfR: "\<And>j. xf j \<in> R" and xf01: "\<And>j. xf j ` S \<subseteq> {0..1}" |
60987 | 597 |
and xfA: "\<And>x j. x \<in> A j \<Longrightarrow> xf j x < e/n" |
598 |
and xfB: "\<And>x j. x \<in> B j \<Longrightarrow> xf j x > 1 - e/n" |
|
599 |
by metis |
|
63040 | 600 |
define g where [abs_def]: "g x = e * (\<Sum>i\<le>n. xf i x)" for x |
60987 | 601 |
have gR: "g \<in> R" |
64267 | 602 |
unfolding g_def by (fast intro: mult const sum xfR) |
63938 | 603 |
have gge0: "\<And>x. x \<in> S \<Longrightarrow> g x \<ge> 0" |
64267 | 604 |
using e xf01 by (simp add: g_def zero_le_mult_iff image_subset_iff sum_nonneg) |
60987 | 605 |
have A0: "A 0 = {}" |
606 |
using fpos e by (fastforce simp: A_def) |
|
63938 | 607 |
have An: "A n = S" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
608 |
using e ngt f normf_upper by (fastforce simp: A_def field_simps of_nat_diff) |
60987 | 609 |
have Asub: "A j \<subseteq> A i" if "i\<ge>j" for i j |
610 |
using e that apply (clarsimp simp: A_def) |
|
611 |
apply (erule order_trans, simp) |
|
612 |
done |
|
613 |
{ fix t |
|
63938 | 614 |
assume t: "t \<in> S" |
63040 | 615 |
define j where "j = (LEAST j. t \<in> A j)" |
60987 | 616 |
have jn: "j \<le> n" |
617 |
using t An by (simp add: Least_le j_def) |
|
618 |
have Aj: "t \<in> A j" |
|
619 |
using t An by (fastforce simp add: j_def intro: LeastI) |
|
620 |
then have Ai: "t \<in> A i" if "i\<ge>j" for i |
|
621 |
using Asub [OF that] by blast |
|
622 |
then have fj1: "f t \<le> (j - 1/3)*e" |
|
623 |
by (simp add: A_def) |
|
624 |
then have Anj: "t \<notin> A i" if "i<j" for i |
|
61222 | 625 |
using Aj \<open>i<j\<close> |
60987 | 626 |
apply (simp add: j_def) |
627 |
using not_less_Least by blast |
|
628 |
have j1: "1 \<le> j" |
|
629 |
using A0 Aj j_def not_less_eq_eq by (fastforce simp add: j_def) |
|
630 |
then have Anj: "t \<notin> A (j-1)" |
|
631 |
using Least_le by (fastforce simp add: j_def) |
|
632 |
then have fj2: "(j - 4/3)*e < f t" |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
633 |
using j1 t by (simp add: A_def of_nat_diff) |
60987 | 634 |
have ***: "xf i t \<le> e/n" if "i\<ge>j" for i |
635 |
using xfA [OF Ai] that by (simp add: less_eq_real_def) |
|
636 |
{ fix i |
|
637 |
assume "i+2 \<le> j" |
|
638 |
then obtain d where "i+2+d = j" |
|
639 |
using le_Suc_ex that by blast |
|
640 |
then have "t \<in> B i" |
|
61222 | 641 |
using Anj e ge_fx [OF t] \<open>1 \<le> n\<close> fpos [OF t] t |
60987 | 642 |
apply (simp add: A_def B_def) |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
643 |
apply (clarsimp simp add: field_simps of_nat_diff not_le of_nat_Suc) |
60987 | 644 |
apply (rule order_trans [of _ "e * 2 + (e * (real d * 3) + e * (real i * 3))"]) |
645 |
apply auto |
|
646 |
done |
|
647 |
then have "xf i t > 1 - e/n" |
|
648 |
by (rule xfB) |
|
649 |
} note **** = this |
|
650 |
have xf_le1: "\<And>i. xf i t \<le> 1" |
|
651 |
using xf01 t by force |
|
652 |
have "g t = e * (\<Sum>i<j. xf i t) + e * (\<Sum>i=j..n. xf i t)" |
|
653 |
using j1 jn e |
|
654 |
apply (simp add: g_def distrib_left [symmetric]) |
|
64267 | 655 |
apply (subst sum.union_disjoint [symmetric]) |
60987 | 656 |
apply (auto simp: ivl_disj_un) |
657 |
done |
|
658 |
also have "... \<le> e*j + e * ((Suc n - j)*e/n)" |
|
659 |
apply (rule add_mono) |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
660 |
apply (simp_all only: mult_le_cancel_left_pos e) |
64267 | 661 |
apply (rule sum_bounded_above [OF xf_le1, where A = "lessThan j", simplified]) |
662 |
using sum_bounded_above [of "{j..n}" "\<lambda>i. xf i t", OF ***] |
|
60987 | 663 |
apply simp |
664 |
done |
|
665 |
also have "... \<le> j*e + e*(n - j + 1)*e/n " |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
666 |
using \<open>1 \<le> n\<close> e by (simp add: field_simps del: of_nat_Suc) |
60987 | 667 |
also have "... \<le> j*e + e*e" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
668 |
using \<open>1 \<le> n\<close> e j1 by (simp add: field_simps del: of_nat_Suc) |
60987 | 669 |
also have "... < (j + 1/3)*e" |
670 |
using e by (auto simp: field_simps) |
|
671 |
finally have gj1: "g t < (j + 1 / 3) * e" . |
|
672 |
have gj2: "(j - 4/3)*e < g t" |
|
673 |
proof (cases "2 \<le> j") |
|
674 |
case False |
|
675 |
then have "j=1" using j1 by simp |
|
676 |
with t gge0 e show ?thesis by force |
|
677 |
next |
|
678 |
case True |
|
679 |
then have "(j - 4/3)*e < (j-1)*e - e^2" |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
680 |
using e by (auto simp: of_nat_diff algebra_simps power2_eq_square) |
60987 | 681 |
also have "... < (j-1)*e - ((j - 1)/n) * e^2" |
682 |
using e True jn by (simp add: power2_eq_square field_simps) |
|
683 |
also have "... = e * (j-1) * (1 - e/n)" |
|
684 |
by (simp add: power2_eq_square field_simps) |
|
685 |
also have "... \<le> e * (\<Sum>i\<le>j-2. xf i t)" |
|
686 |
using e |
|
687 |
apply simp |
|
64267 | 688 |
apply (rule order_trans [OF _ sum_bounded_below [OF less_imp_le [OF ****]]]) |
60987 | 689 |
using True |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
690 |
apply (simp_all add: of_nat_Suc of_nat_diff) |
60987 | 691 |
done |
692 |
also have "... \<le> g t" |
|
693 |
using jn e |
|
694 |
using e xf01 t |
|
64267 | 695 |
apply (simp add: g_def zero_le_mult_iff image_subset_iff sum_nonneg) |
696 |
apply (rule Groups_Big.sum_mono2, auto) |
|
60987 | 697 |
done |
698 |
finally show ?thesis . |
|
699 |
qed |
|
700 |
have "\<bar>f t - g t\<bar> < 2 * e" |
|
701 |
using fj1 fj2 gj1 gj2 by (simp add: abs_less_iff field_simps) |
|
702 |
} |
|
703 |
then show ?thesis |
|
704 |
by (rule_tac x=g in bexI) (auto intro: gR) |
|
705 |
qed |
|
706 |
||
707 |
text\<open>The ``unpretentious'' formulation\<close> |
|
708 |
lemma (in function_ring_on) Stone_Weierstrass_basic: |
|
63938 | 709 |
assumes f: "continuous_on S f" and e: "e > 0" |
710 |
shows "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>f x - g x\<bar> < e" |
|
60987 | 711 |
proof - |
63938 | 712 |
have "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>(f x + normf f) - g x\<bar> < 2 * min (e/2) (1/4)" |
60987 | 713 |
apply (rule Stone_Weierstrass_special) |
714 |
apply (rule Limits.continuous_on_add [OF f Topological_Spaces.continuous_on_const]) |
|
715 |
using normf_upper [OF f] apply force |
|
716 |
apply (simp add: e, linarith) |
|
717 |
done |
|
63938 | 718 |
then obtain g where "g \<in> R" "\<forall>x\<in>S. \<bar>g x - (f x + normf f)\<bar> < e" |
60987 | 719 |
by force |
720 |
then show ?thesis |
|
721 |
apply (rule_tac x="\<lambda>x. g x - normf f" in bexI) |
|
722 |
apply (auto simp: algebra_simps intro: diff const) |
|
723 |
done |
|
724 |
qed |
|
725 |
||
726 |
||
727 |
theorem (in function_ring_on) Stone_Weierstrass: |
|
63938 | 728 |
assumes f: "continuous_on S f" |
729 |
shows "\<exists>F\<in>UNIV \<rightarrow> R. LIM n sequentially. F n :> uniformly_on S f" |
|
60987 | 730 |
proof - |
731 |
{ fix e::real |
|
732 |
assume e: "0 < e" |
|
733 |
then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e" |
|
62623
dbc62f86a1a9
rationalisation of theorem names esp about "real Archimedian" etc.
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset
|
734 |
by (auto simp: real_arch_inverse [of e]) |
60987 | 735 |
{ fix n :: nat and x :: 'a and g :: "'a \<Rightarrow> real" |
63938 | 736 |
assume n: "N \<le> n" "\<forall>x\<in>S. \<bar>f x - g x\<bar> < 1 / (1 + real n)" |
737 |
assume x: "x \<in> S" |
|
60987 | 738 |
have "\<not> real (Suc n) < inverse e" |
61222 | 739 |
using \<open>N \<le> n\<close> N using less_imp_inverse_less by force |
60987 | 740 |
then have "1 / (1 + real n) \<le> e" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
741 |
using e by (simp add: field_simps of_nat_Suc) |
60987 | 742 |
then have "\<bar>f x - g x\<bar> < e" |
743 |
using n(2) x by auto |
|
744 |
} note * = this |
|
63938 | 745 |
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" |
60987 | 746 |
apply (rule eventually_sequentiallyI [of N]) |
747 |
apply (auto intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]] *) |
|
748 |
done |
|
749 |
} then |
|
750 |
show ?thesis |
|
63938 | 751 |
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) |
60987 | 752 |
prefer 2 apply (force intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]]) |
753 |
unfolding uniform_limit_iff |
|
754 |
apply (auto simp: dist_norm abs_minus_commute) |
|
755 |
done |
|
756 |
qed |
|
757 |
||
61222 | 758 |
text\<open>A HOL Light formulation\<close> |
60987 | 759 |
corollary Stone_Weierstrass_HOL: |
63938 | 760 |
fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set" |
761 |
assumes "compact S" "\<And>c. P(\<lambda>x. c::real)" |
|
762 |
"\<And>f. P f \<Longrightarrow> continuous_on S f" |
|
60987 | 763 |
"\<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)" |
63938 | 764 |
"\<And>x y. x \<in> S \<and> y \<in> S \<and> ~(x = y) \<Longrightarrow> \<exists>f. P(f) \<and> ~(f x = f y)" |
765 |
"continuous_on S f" |
|
60987 | 766 |
"0 < e" |
63938 | 767 |
shows "\<exists>g. P(g) \<and> (\<forall>x \<in> S. \<bar>f x - g x\<bar> < e)" |
60987 | 768 |
proof - |
769 |
interpret PR: function_ring_on "Collect P" |
|
770 |
apply unfold_locales |
|
771 |
using assms |
|
772 |
by auto |
|
773 |
show ?thesis |
|
63938 | 774 |
using PR.Stone_Weierstrass_basic [OF \<open>continuous_on S f\<close> \<open>0 < e\<close>] |
60987 | 775 |
by blast |
776 |
qed |
|
777 |
||
778 |
||
61222 | 779 |
subsection \<open>Polynomial functions\<close> |
60987 | 780 |
|
781 |
inductive real_polynomial_function :: "('a::real_normed_vector \<Rightarrow> real) \<Rightarrow> bool" where |
|
782 |
linear: "bounded_linear f \<Longrightarrow> real_polynomial_function f" |
|
783 |
| const: "real_polynomial_function (\<lambda>x. c)" |
|
784 |
| add: "\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x + g x)" |
|
785 |
| mult: "\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x * g x)" |
|
786 |
||
787 |
declare real_polynomial_function.intros [intro] |
|
788 |
||
789 |
definition polynomial_function :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> bool" |
|
790 |
where |
|
791 |
"polynomial_function p \<equiv> (\<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f o p))" |
|
792 |
||
793 |
lemma real_polynomial_function_eq: "real_polynomial_function p = polynomial_function p" |
|
794 |
unfolding polynomial_function_def |
|
795 |
proof |
|
796 |
assume "real_polynomial_function p" |
|
797 |
then show " \<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f \<circ> p)" |
|
798 |
proof (induction p rule: real_polynomial_function.induct) |
|
799 |
case (linear h) then show ?case |
|
800 |
by (auto simp: bounded_linear_compose real_polynomial_function.linear) |
|
801 |
next |
|
802 |
case (const h) then show ?case |
|
803 |
by (simp add: real_polynomial_function.const) |
|
804 |
next |
|
805 |
case (add h) then show ?case |
|
806 |
by (force simp add: bounded_linear_def linear_add real_polynomial_function.add) |
|
807 |
next |
|
808 |
case (mult h) then show ?case |
|
809 |
by (force simp add: real_bounded_linear const real_polynomial_function.mult) |
|
810 |
qed |
|
811 |
next |
|
812 |
assume [rule_format, OF bounded_linear_ident]: "\<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f \<circ> p)" |
|
813 |
then show "real_polynomial_function p" |
|
814 |
by (simp add: o_def) |
|
815 |
qed |
|
816 |
||
817 |
lemma polynomial_function_const [iff]: "polynomial_function (\<lambda>x. c)" |
|
818 |
by (simp add: polynomial_function_def o_def const) |
|
819 |
||
820 |
lemma polynomial_function_bounded_linear: |
|
821 |
"bounded_linear f \<Longrightarrow> polynomial_function f" |
|
822 |
by (simp add: polynomial_function_def o_def bounded_linear_compose real_polynomial_function.linear) |
|
823 |
||
824 |
lemma polynomial_function_id [iff]: "polynomial_function(\<lambda>x. x)" |
|
825 |
by (simp add: polynomial_function_bounded_linear) |
|
826 |
||
827 |
lemma polynomial_function_add [intro]: |
|
828 |
"\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x + g x)" |
|
829 |
by (auto simp: polynomial_function_def bounded_linear_def linear_add real_polynomial_function.add o_def) |
|
830 |
||
831 |
lemma polynomial_function_mult [intro]: |
|
832 |
assumes f: "polynomial_function f" and g: "polynomial_function g" |
|
833 |
shows "polynomial_function (\<lambda>x. f x *\<^sub>R g x)" |
|
834 |
using g |
|
835 |
apply (auto simp: polynomial_function_def bounded_linear_def Real_Vector_Spaces.linear.scaleR const real_polynomial_function.mult o_def) |
|
836 |
apply (rule mult) |
|
837 |
using f |
|
838 |
apply (auto simp: real_polynomial_function_eq) |
|
839 |
done |
|
840 |
||
841 |
lemma polynomial_function_cmul [intro]: |
|
842 |
assumes f: "polynomial_function f" |
|
843 |
shows "polynomial_function (\<lambda>x. c *\<^sub>R f x)" |
|
844 |
by (rule polynomial_function_mult [OF polynomial_function_const f]) |
|
845 |
||
846 |
lemma polynomial_function_minus [intro]: |
|
847 |
assumes f: "polynomial_function f" |
|
848 |
shows "polynomial_function (\<lambda>x. - f x)" |
|
849 |
using polynomial_function_cmul [OF f, of "-1"] by simp |
|
850 |
||
851 |
lemma polynomial_function_diff [intro]: |
|
852 |
"\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x - g x)" |
|
853 |
unfolding add_uminus_conv_diff [symmetric] |
|
854 |
by (metis polynomial_function_add polynomial_function_minus) |
|
855 |
||
64267 | 856 |
lemma polynomial_function_sum [intro]: |
857 |
"\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> polynomial_function (\<lambda>x. f x i)\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. sum (f x) I)" |
|
60987 | 858 |
by (induct I rule: finite_induct) auto |
859 |
||
860 |
lemma real_polynomial_function_minus [intro]: |
|
861 |
"real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. - f x)" |
|
862 |
using polynomial_function_minus [of f] |
|
863 |
by (simp add: real_polynomial_function_eq) |
|
864 |
||
865 |
lemma real_polynomial_function_diff [intro]: |
|
866 |
"\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x - g x)" |
|
867 |
using polynomial_function_diff [of f] |
|
868 |
by (simp add: real_polynomial_function_eq) |
|
869 |
||
64267 | 870 |
lemma real_polynomial_function_sum [intro]: |
871 |
"\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> real_polynomial_function (\<lambda>x. f x i)\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. sum (f x) I)" |
|
872 |
using polynomial_function_sum [of I f] |
|
60987 | 873 |
by (simp add: real_polynomial_function_eq) |
874 |
||
875 |
lemma real_polynomial_function_power [intro]: |
|
876 |
"real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. f x ^ n)" |
|
877 |
by (induct n) (simp_all add: const mult) |
|
878 |
||
879 |
lemma real_polynomial_function_compose [intro]: |
|
880 |
assumes f: "polynomial_function f" and g: "real_polynomial_function g" |
|
881 |
shows "real_polynomial_function (g o f)" |
|
882 |
using g |
|
883 |
apply (induction g rule: real_polynomial_function.induct) |
|
884 |
using f |
|
885 |
apply (simp_all add: polynomial_function_def o_def const add mult) |
|
886 |
done |
|
887 |
||
888 |
lemma polynomial_function_compose [intro]: |
|
889 |
assumes f: "polynomial_function f" and g: "polynomial_function g" |
|
890 |
shows "polynomial_function (g o f)" |
|
891 |
using g real_polynomial_function_compose [OF f] |
|
892 |
by (auto simp: polynomial_function_def o_def) |
|
893 |
||
64267 | 894 |
lemma sum_max_0: |
60987 | 895 |
fixes x::real (*in fact "'a::comm_ring_1"*) |
896 |
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)" |
|
897 |
proof - |
|
898 |
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))" |
|
64267 | 899 |
by (auto simp: algebra_simps intro: sum.cong) |
60987 | 900 |
also have "... = (\<Sum>i = 0..m. (if i \<le> m then x^i * a i else 0))" |
64267 | 901 |
by (rule sum.mono_neutral_right) auto |
60987 | 902 |
also have "... = (\<Sum>i = 0..m. x^i * a i)" |
64267 | 903 |
by (auto simp: algebra_simps intro: sum.cong) |
60987 | 904 |
finally show ?thesis . |
905 |
qed |
|
906 |
||
64267 | 907 |
lemma real_polynomial_function_imp_sum: |
60987 | 908 |
assumes "real_polynomial_function f" |
909 |
shows "\<exists>a n::nat. f = (\<lambda>x. \<Sum>i=0..n. a i * x ^ i)" |
|
910 |
using assms |
|
911 |
proof (induct f) |
|
912 |
case (linear f) |
|
913 |
then show ?case |
|
914 |
apply (clarsimp simp add: real_bounded_linear) |
|
915 |
apply (rule_tac x="\<lambda>i. if i=0 then 0 else c" in exI) |
|
916 |
apply (rule_tac x=1 in exI) |
|
917 |
apply (simp add: mult_ac) |
|
918 |
done |
|
919 |
next |
|
920 |
case (const c) |
|
921 |
show ?case |
|
922 |
apply (rule_tac x="\<lambda>i. c" in exI) |
|
923 |
apply (rule_tac x=0 in exI) |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset
|
924 |
apply (auto simp: mult_ac of_nat_Suc) |
60987 | 925 |
done |
926 |
case (add f1 f2) |
|
927 |
then obtain a1 n1 a2 n2 where |
|
928 |
"f1 = (\<lambda>x. \<Sum>i = 0..n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. a2 i * x ^ i)" |
|
929 |
by auto |
|
930 |
then show ?case |
|
931 |
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) |
|
932 |
apply (rule_tac x="max n1 n2" in exI) |
|
64267 | 933 |
using sum_max_0 [where m=n1 and n=n2] sum_max_0 [where m=n2 and n=n1] |
934 |
apply (simp add: sum.distrib algebra_simps max.commute) |
|
60987 | 935 |
done |
936 |
case (mult f1 f2) |
|
937 |
then obtain a1 n1 a2 n2 where |
|
938 |
"f1 = (\<lambda>x. \<Sum>i = 0..n1. a1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. a2 i * x ^ i)" |
|
939 |
by auto |
|
940 |
then obtain b1 b2 where |
|
941 |
"f1 = (\<lambda>x. \<Sum>i = 0..n1. b1 i * x ^ i)" "f2 = (\<lambda>x. \<Sum>i = 0..n2. b2 i * x ^ i)" |
|
942 |
"b1 = (\<lambda>i. if i\<le>n1 then a1 i else 0)" "b2 = (\<lambda>i. if i\<le>n2 then a2 i else 0)" |
|
943 |
by auto |
|
944 |
then show ?case |
|
945 |
apply (rule_tac x="\<lambda>i. \<Sum>k\<le>i. b1 k * b2 (i - k)" in exI) |
|
946 |
apply (rule_tac x="n1+n2" in exI) |
|
947 |
using polynomial_product [of n1 b1 n2 b2] |
|
948 |
apply (simp add: Set_Interval.atLeast0AtMost) |
|
949 |
done |
|
950 |
qed |
|
951 |
||
64267 | 952 |
lemma real_polynomial_function_iff_sum: |
60987 | 953 |
"real_polynomial_function f \<longleftrightarrow> (\<exists>a n::nat. f = (\<lambda>x. \<Sum>i=0..n. a i * x ^ i))" |
954 |
apply (rule iffI) |
|
64267 | 955 |
apply (erule real_polynomial_function_imp_sum) |
956 |
apply (auto simp: linear mult const real_polynomial_function_power real_polynomial_function_sum) |
|
60987 | 957 |
done |
958 |
||
959 |
lemma polynomial_function_iff_Basis_inner: |
|
960 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" |
|
961 |
shows "polynomial_function f \<longleftrightarrow> (\<forall>b\<in>Basis. real_polynomial_function (\<lambda>x. inner (f x) b))" |
|
962 |
(is "?lhs = ?rhs") |
|
963 |
unfolding polynomial_function_def |
|
964 |
proof (intro iffI allI impI) |
|
965 |
assume "\<forall>h. bounded_linear h \<longrightarrow> real_polynomial_function (h \<circ> f)" |
|
966 |
then show ?rhs |
|
967 |
by (force simp add: bounded_linear_inner_left o_def) |
|
968 |
next |
|
969 |
fix h :: "'b \<Rightarrow> real" |
|
970 |
assume rp: "\<forall>b\<in>Basis. real_polynomial_function (\<lambda>x. f x \<bullet> b)" and h: "bounded_linear h" |
|
971 |
have "real_polynomial_function (h \<circ> (\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b))" |
|
972 |
apply (rule real_polynomial_function_compose [OF _ linear [OF h]]) |
|
973 |
using rp |
|
974 |
apply (auto simp: real_polynomial_function_eq polynomial_function_mult) |
|
975 |
done |
|
976 |
then show "real_polynomial_function (h \<circ> f)" |
|
64267 | 977 |
by (simp add: euclidean_representation_sum_fun) |
60987 | 978 |
qed |
979 |
||
61222 | 980 |
subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close> |
60987 | 981 |
|
982 |
text\<open>First, we need to show that they are continous, differentiable and separable.\<close> |
|
983 |
||
984 |
lemma continuous_real_polymonial_function: |
|
985 |
assumes "real_polynomial_function f" |
|
986 |
shows "continuous (at x) f" |
|
987 |
using assms |
|
988 |
by (induct f) (auto simp: linear_continuous_at) |
|
989 |
||
990 |
lemma continuous_polymonial_function: |
|
991 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" |
|
992 |
assumes "polynomial_function f" |
|
993 |
shows "continuous (at x) f" |
|
994 |
apply (rule euclidean_isCont) |
|
995 |
using assms apply (simp add: polynomial_function_iff_Basis_inner) |
|
996 |
apply (force dest: continuous_real_polymonial_function intro: isCont_scaleR) |
|
997 |
done |
|
998 |
||
999 |
lemma continuous_on_polymonial_function: |
|
1000 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" |
|
1001 |
assumes "polynomial_function f" |
|
63938 | 1002 |
shows "continuous_on S f" |
60987 | 1003 |
using continuous_polymonial_function [OF assms] continuous_at_imp_continuous_on |
1004 |
by blast |
|
1005 |
||
1006 |
lemma has_real_derivative_polynomial_function: |
|
1007 |
assumes "real_polynomial_function p" |
|
1008 |
shows "\<exists>p'. real_polynomial_function p' \<and> |
|
1009 |
(\<forall>x. (p has_real_derivative (p' x)) (at x))" |
|
1010 |
using assms |
|
1011 |
proof (induct p) |
|
1012 |
case (linear p) |
|
1013 |
then show ?case |
|
1014 |
by (force simp: real_bounded_linear const intro!: derivative_eq_intros) |
|
1015 |
next |
|
1016 |
case (const c) |
|
1017 |
show ?case |
|
1018 |
by (rule_tac x="\<lambda>x. 0" in exI) auto |
|
1019 |
case (add f1 f2) |
|
1020 |
then obtain p1 p2 where |
|
1021 |
"real_polynomial_function p1" "\<And>x. (f1 has_real_derivative p1 x) (at x)" |
|
1022 |
"real_polynomial_function p2" "\<And>x. (f2 has_real_derivative p2 x) (at x)" |
|
1023 |
by auto |
|
1024 |
then show ?case |
|
1025 |
apply (rule_tac x="\<lambda>x. p1 x + p2 x" in exI) |
|
1026 |
apply (auto intro!: derivative_eq_intros) |
|
1027 |
done |
|
1028 |
case (mult f1 f2) |
|
1029 |
then obtain p1 p2 where |
|
1030 |
"real_polynomial_function p1" "\<And>x. (f1 has_real_derivative p1 x) (at x)" |
|
1031 |
"real_polynomial_function p2" "\<And>x. (f2 has_real_derivative p2 x) (at x)" |
|
1032 |
by auto |
|
1033 |
then show ?case |
|
1034 |
using mult |
|
1035 |
apply (rule_tac x="\<lambda>x. f1 x * p2 x + f2 x * p1 x" in exI) |
|
1036 |
apply (auto intro!: derivative_eq_intros) |
|
1037 |
done |
|
1038 |
qed |
|
1039 |
||
1040 |
lemma has_vector_derivative_polynomial_function: |
|
1041 |
fixes p :: "real \<Rightarrow> 'a::euclidean_space" |
|
1042 |
assumes "polynomial_function p" |
|
63938 | 1043 |
obtains p' where "polynomial_function p'" "\<And>x. (p has_vector_derivative (p' x)) (at x)" |
60987 | 1044 |
proof - |
1045 |
{ fix b :: 'a |
|
1046 |
assume "b \<in> Basis" |
|
1047 |
then |
|
1048 |
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)" |
|
61222 | 1049 |
using assms [unfolded polynomial_function_iff_Basis_inner, rule_format] \<open>b \<in> Basis\<close> |
60987 | 1050 |
has_real_derivative_polynomial_function |
1051 |
by blast |
|
1052 |
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))" |
|
1053 |
apply (rule_tac x="\<lambda>x. p' x *\<^sub>R b" in exI) |
|
61222 | 1054 |
using \<open>b \<in> Basis\<close> p' |
60987 | 1055 |
apply (simp add: polynomial_function_iff_Basis_inner inner_Basis) |
1056 |
apply (auto intro: derivative_eq_intros pd) |
|
1057 |
done |
|
1058 |
} |
|
1059 |
then obtain qf where qf: |
|
1060 |
"\<And>b. b \<in> Basis \<Longrightarrow> polynomial_function (qf b)" |
|
1061 |
"\<And>b x. b \<in> Basis \<Longrightarrow> ((\<lambda>u. (p u \<bullet> b) *\<^sub>R b) has_vector_derivative qf b x) (at x)" |
|
1062 |
by metis |
|
1063 |
show ?thesis |
|
63938 | 1064 |
apply (rule_tac p'="\<lambda>x. \<Sum>b\<in>Basis. qf b x" in that) |
1065 |
apply (force intro: qf) |
|
64267 | 1066 |
apply (subst euclidean_representation_sum_fun [of p, symmetric]) |
1067 |
apply (auto intro: has_vector_derivative_sum qf) |
|
60987 | 1068 |
done |
1069 |
qed |
|
1070 |
||
1071 |
lemma real_polynomial_function_separable: |
|
1072 |
fixes x :: "'a::euclidean_space" |
|
1073 |
assumes "x \<noteq> y" shows "\<exists>f. real_polynomial_function f \<and> f x \<noteq> f y" |
|
1074 |
proof - |
|
1075 |
have "real_polynomial_function (\<lambda>u. \<Sum>b\<in>Basis. (inner (x-u) b)^2)" |
|
64267 | 1076 |
apply (rule real_polynomial_function_sum) |
60987 | 1077 |
apply (auto simp: algebra_simps real_polynomial_function_power real_polynomial_function_diff |
1078 |
const linear bounded_linear_inner_left) |
|
1079 |
done |
|
1080 |
then show ?thesis |
|
1081 |
apply (intro exI conjI, assumption) |
|
1082 |
using assms |
|
64267 | 1083 |
apply (force simp add: euclidean_eq_iff [of x y] sum_nonneg_eq_0_iff algebra_simps) |
60987 | 1084 |
done |
1085 |
qed |
|
1086 |
||
1087 |
lemma Stone_Weierstrass_real_polynomial_function: |
|
1088 |
fixes f :: "'a::euclidean_space \<Rightarrow> real" |
|
63938 | 1089 |
assumes "compact S" "continuous_on S f" "0 < e" |
1090 |
obtains g where "real_polynomial_function g" "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x - g x\<bar> < e" |
|
60987 | 1091 |
proof - |
1092 |
interpret PR: function_ring_on "Collect real_polynomial_function" |
|
1093 |
apply unfold_locales |
|
1094 |
using assms continuous_on_polymonial_function real_polynomial_function_eq |
|
1095 |
apply (auto intro: real_polynomial_function_separable) |
|
1096 |
done |
|
1097 |
show ?thesis |
|
63938 | 1098 |
using PR.Stone_Weierstrass_basic [OF \<open>continuous_on S f\<close> \<open>0 < e\<close>] that |
60987 | 1099 |
by blast |
1100 |
qed |
|
1101 |
||
1102 |
lemma Stone_Weierstrass_polynomial_function: |
|
1103 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
63938 | 1104 |
assumes S: "compact S" |
1105 |
and f: "continuous_on S f" |
|
60987 | 1106 |
and e: "0 < e" |
63938 | 1107 |
shows "\<exists>g. polynomial_function g \<and> (\<forall>x \<in> S. norm(f x - g x) < e)" |
60987 | 1108 |
proof - |
1109 |
{ fix b :: 'b |
|
1110 |
assume "b \<in> Basis" |
|
63938 | 1111 |
have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> S. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))" |
1112 |
apply (rule exE [OF Stone_Weierstrass_real_polynomial_function [OF S _, of "\<lambda>x. f x \<bullet> b" "e / card Basis"]]) |
|
60987 | 1113 |
using e f |
1114 |
apply (auto simp: Euclidean_Space.DIM_positive intro: continuous_intros) |
|
1115 |
done |
|
1116 |
} |
|
1117 |
then obtain pf where pf: |
|
63938 | 1118 |
"\<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))" |
60987 | 1119 |
apply (rule bchoice [rule_format, THEN exE]) |
1120 |
apply assumption |
|
1121 |
apply (force simp add: intro: that) |
|
1122 |
done |
|
1123 |
have "polynomial_function (\<lambda>x. \<Sum>b\<in>Basis. pf b x *\<^sub>R b)" |
|
1124 |
using pf |
|
64267 | 1125 |
by (simp add: polynomial_function_sum polynomial_function_mult real_polynomial_function_eq) |
60987 | 1126 |
moreover |
1127 |
{ fix x |
|
63938 | 1128 |
assume "x \<in> S" |
60987 | 1129 |
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))" |
64267 | 1130 |
by (rule norm_sum) |
60987 | 1131 |
also have "... < of_nat DIM('b) * (e / DIM('b))" |
64267 | 1132 |
apply (rule sum_bounded_above_strict) |
63938 | 1133 |
apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf \<open>x \<in> S\<close>) |
60987 | 1134 |
apply (rule DIM_positive) |
1135 |
done |
|
1136 |
also have "... = e" |
|
1137 |
using DIM_positive by (simp add: field_simps) |
|
1138 |
finally have "norm (\<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b - pf b x *\<^sub>R b) < e" . |
|
1139 |
} |
|
1140 |
ultimately |
|
1141 |
show ?thesis |
|
64267 | 1142 |
apply (subst euclidean_representation_sum_fun [of f, symmetric]) |
60987 | 1143 |
apply (rule_tac x="\<lambda>x. \<Sum>b\<in>Basis. pf b x *\<^sub>R b" in exI) |
64267 | 1144 |
apply (auto simp: sum_subtractf [symmetric]) |
60987 | 1145 |
done |
1146 |
qed |
|
1147 |
||
65204
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1148 |
lemma Stone_Weierstrass_uniform_limit: |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1149 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1150 |
assumes S: "compact S" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1151 |
and f: "continuous_on S f" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1152 |
obtains g where "uniform_limit S g f sequentially" "\<And>n. polynomial_function (g n)" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1153 |
proof - |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1154 |
have pos: "inverse (Suc n) > 0" for n by auto |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1155 |
obtain g where g: "\<And>n. polynomial_function (g n)" "\<And>x n. x \<in> S \<Longrightarrow> norm(f x - g n x) < inverse (Suc n)" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1156 |
using Stone_Weierstrass_polynomial_function[OF S f pos] |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1157 |
by metis |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1158 |
have "uniform_limit S g f sequentially" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1159 |
proof (rule uniform_limitI) |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1160 |
fix e::real assume "0 < e" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1161 |
with LIMSEQ_inverse_real_of_nat have "\<forall>\<^sub>F n in sequentially. inverse (Suc n) < e" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1162 |
by (rule order_tendstoD) |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1163 |
moreover have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. dist (g n x) (f x) < inverse (Suc n)" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1164 |
using g by (simp add: dist_norm norm_minus_commute) |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1165 |
ultimately show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. dist (g n x) (f x) < e" |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1166 |
by (eventually_elim) auto |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1167 |
qed |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1168 |
then show ?thesis using g(1) .. |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1169 |
qed |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1170 |
|
60987 | 1171 |
|
1172 |
subsection\<open>Polynomial functions as paths\<close> |
|
1173 |
||
61222 | 1174 |
text\<open>One application is to pick a smooth approximation to a path, |
1175 |
or just pick a smooth path anyway in an open connected set\<close> |
|
60987 | 1176 |
|
1177 |
lemma path_polynomial_function: |
|
1178 |
fixes g :: "real \<Rightarrow> 'b::euclidean_space" |
|
1179 |
shows "polynomial_function g \<Longrightarrow> path g" |
|
1180 |
by (simp add: path_def continuous_on_polymonial_function) |
|
1181 |
||
1182 |
lemma path_approx_polynomial_function: |
|
1183 |
fixes g :: "real \<Rightarrow> 'b::euclidean_space" |
|
1184 |
assumes "path g" "0 < e" |
|
1185 |
shows "\<exists>p. polynomial_function p \<and> |
|
1186 |
pathstart p = pathstart g \<and> |
|
1187 |
pathfinish p = pathfinish g \<and> |
|
1188 |
(\<forall>t \<in> {0..1}. norm(p t - g t) < e)" |
|
1189 |
proof - |
|
1190 |
obtain q where poq: "polynomial_function q" and noq: "\<And>x. x \<in> {0..1} \<Longrightarrow> norm (g x - q x) < e/4" |
|
1191 |
using Stone_Weierstrass_polynomial_function [of "{0..1}" g "e/4"] assms |
|
1192 |
by (auto simp: path_def) |
|
1193 |
have pf: "polynomial_function (\<lambda>t. q t + (g 0 - q 0) + t *\<^sub>R (g 1 - q 1 - (g 0 - q 0)))" |
|
1194 |
by (force simp add: poq) |
|
1195 |
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)" |
|
1196 |
apply (intro Real_Vector_Spaces.norm_add_less) |
|
1197 |
using noq |
|
1198 |
apply (auto simp: norm_minus_commute intro: le_less_trans [OF mult_left_le_one_le noq] simp del: less_divide_eq_numeral1) |
|
1199 |
done |
|
1200 |
show ?thesis |
|
1201 |
apply (intro exI conjI) |
|
1202 |
apply (rule pf) |
|
1203 |
using * |
|
1204 |
apply (auto simp add: pathstart_def pathfinish_def algebra_simps) |
|
1205 |
done |
|
1206 |
qed |
|
1207 |
||
1208 |
lemma connected_open_polynomial_connected: |
|
63938 | 1209 |
fixes S :: "'a::euclidean_space set" |
1210 |
assumes S: "open S" "connected S" |
|
1211 |
and "x \<in> S" "y \<in> S" |
|
1212 |
shows "\<exists>g. polynomial_function g \<and> path_image g \<subseteq> S \<and> |
|
60987 | 1213 |
pathstart g = x \<and> pathfinish g = y" |
1214 |
proof - |
|
63938 | 1215 |
have "path_connected S" using assms |
60987 | 1216 |
by (simp add: connected_open_path_connected) |
63938 | 1217 |
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" |
60987 | 1218 |
by (force simp: path_connected_def) |
63938 | 1219 |
have "\<exists>e. 0 < e \<and> (\<forall>x \<in> path_image p. ball x e \<subseteq> S)" |
1220 |
proof (cases "S = UNIV") |
|
60987 | 1221 |
case True then show ?thesis |
1222 |
by (simp add: gt_ex) |
|
1223 |
next |
|
1224 |
case False |
|
63938 | 1225 |
then have "- S \<noteq> {}" by blast |
60987 | 1226 |
then show ?thesis |
63938 | 1227 |
apply (rule_tac x="setdist (path_image p) (-S)" in exI) |
1228 |
using S p |
|
60987 | 1229 |
apply (simp add: setdist_gt_0_compact_closed compact_path_image open_closed) |
63938 | 1230 |
using setdist_le_dist [of _ "path_image p" _ "-S"] |
60987 | 1231 |
by fastforce |
1232 |
qed |
|
63938 | 1233 |
then obtain e where "0 < e"and eb: "\<And>x. x \<in> path_image p \<Longrightarrow> ball x e \<subseteq> S" |
60987 | 1234 |
by auto |
1235 |
show ?thesis |
|
61222 | 1236 |
using path_approx_polynomial_function [OF \<open>path p\<close> \<open>0 < e\<close>] |
60987 | 1237 |
apply clarify |
1238 |
apply (intro exI conjI, assumption) |
|
1239 |
using p |
|
1240 |
apply (fastforce simp add: dist_norm path_image_def norm_minus_commute intro: eb [THEN subsetD])+ |
|
1241 |
done |
|
1242 |
qed |
|
1243 |
||
63938 | 1244 |
lemma has_derivative_componentwise_within: |
1245 |
"(f has_derivative f') (at a within S) \<longleftrightarrow> |
|
1246 |
(\<forall>i \<in> Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. f' x \<bullet> i)) (at a within S))" |
|
1247 |
apply (simp add: has_derivative_within) |
|
1248 |
apply (subst tendsto_componentwise_iff) |
|
1249 |
apply (simp add: bounded_linear_componentwise_iff [symmetric] ball_conj_distrib) |
|
1250 |
apply (simp add: algebra_simps) |
|
1251 |
done |
|
1252 |
||
1253 |
lemma differentiable_componentwise_within: |
|
1254 |
"f differentiable (at a within S) \<longleftrightarrow> |
|
1255 |
(\<forall>i \<in> Basis. (\<lambda>x. f x \<bullet> i) differentiable at a within S)" |
|
1256 |
proof - |
|
1257 |
{ assume "\<forall>i\<in>Basis. \<exists>D. ((\<lambda>x. f x \<bullet> i) has_derivative D) (at a within S)" |
|
1258 |
then obtain f' where f': |
|
1259 |
"\<And>i. i \<in> Basis \<Longrightarrow> ((\<lambda>x. f x \<bullet> i) has_derivative f' i) (at a within S)" |
|
1260 |
by metis |
|
1261 |
have eq: "(\<lambda>x. (\<Sum>j\<in>Basis. f' j x *\<^sub>R j) \<bullet> i) = f' i" if "i \<in> Basis" for i |
|
1262 |
using that by (simp add: inner_add_left inner_add_right) |
|
1263 |
have "\<exists>D. \<forall>i\<in>Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. D x \<bullet> i)) (at a within S)" |
|
1264 |
apply (rule_tac x="\<lambda>x::'a. (\<Sum>j\<in>Basis. f' j x *\<^sub>R j) :: 'b" in exI) |
|
1265 |
apply (simp add: eq f') |
|
1266 |
done |
|
1267 |
} |
|
1268 |
then show ?thesis |
|
1269 |
apply (simp add: differentiable_def) |
|
1270 |
using has_derivative_componentwise_within |
|
1271 |
by blast |
|
1272 |
qed |
|
1273 |
||
1274 |
lemma polynomial_function_inner [intro]: |
|
1275 |
fixes i :: "'a::euclidean_space" |
|
1276 |
shows "polynomial_function g \<Longrightarrow> polynomial_function (\<lambda>x. g x \<bullet> i)" |
|
1277 |
apply (subst euclidean_representation [where x=i, symmetric]) |
|
64267 | 1278 |
apply (force simp: inner_sum_right polynomial_function_iff_Basis_inner polynomial_function_sum) |
63938 | 1279 |
done |
1280 |
||
1281 |
text\<open> Differentiability of real and vector polynomial functions.\<close> |
|
1282 |
||
1283 |
lemma differentiable_at_real_polynomial_function: |
|
1284 |
"real_polynomial_function f \<Longrightarrow> f differentiable (at a within S)" |
|
1285 |
by (induction f rule: real_polynomial_function.induct) |
|
1286 |
(simp_all add: bounded_linear_imp_differentiable) |
|
1287 |
||
1288 |
lemma differentiable_on_real_polynomial_function: |
|
1289 |
"real_polynomial_function p \<Longrightarrow> p differentiable_on S" |
|
1290 |
by (simp add: differentiable_at_imp_differentiable_on differentiable_at_real_polynomial_function) |
|
1291 |
||
1292 |
lemma differentiable_at_polynomial_function: |
|
1293 |
fixes f :: "_ \<Rightarrow> 'a::euclidean_space" |
|
1294 |
shows "polynomial_function f \<Longrightarrow> f differentiable (at a within S)" |
|
1295 |
by (metis differentiable_at_real_polynomial_function polynomial_function_iff_Basis_inner differentiable_componentwise_within) |
|
1296 |
||
1297 |
lemma differentiable_on_polynomial_function: |
|
1298 |
fixes f :: "_ \<Rightarrow> 'a::euclidean_space" |
|
1299 |
shows "polynomial_function f \<Longrightarrow> f differentiable_on S" |
|
1300 |
by (simp add: differentiable_at_polynomial_function differentiable_on_def) |
|
1301 |
||
1302 |
lemma vector_eq_dot_span: |
|
1303 |
assumes "x \<in> span B" "y \<in> span B" and i: "\<And>i. i \<in> B \<Longrightarrow> i \<bullet> x = i \<bullet> y" |
|
1304 |
shows "x = y" |
|
1305 |
proof - |
|
1306 |
have "\<And>i. i \<in> B \<Longrightarrow> orthogonal (x - y) i" |
|
1307 |
by (simp add: i inner_commute inner_diff_right orthogonal_def) |
|
1308 |
moreover have "x - y \<in> span B" |
|
1309 |
by (simp add: assms span_diff) |
|
1310 |
ultimately have "x - y = 0" |
|
1311 |
using orthogonal_to_span orthogonal_self by blast |
|
1312 |
then show ?thesis by simp |
|
1313 |
qed |
|
1314 |
||
1315 |
lemma orthonormal_basis_expand: |
|
1316 |
assumes B: "pairwise orthogonal B" |
|
1317 |
and 1: "\<And>i. i \<in> B \<Longrightarrow> norm i = 1" |
|
1318 |
and "x \<in> span B" |
|
1319 |
and "finite B" |
|
1320 |
shows "(\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) = x" |
|
1321 |
proof (rule vector_eq_dot_span [OF _ \<open>x \<in> span B\<close>]) |
|
1322 |
show "(\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) \<in> span B" |
|
64267 | 1323 |
by (simp add: span_clauses span_sum) |
63938 | 1324 |
show "i \<bullet> (\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) = i \<bullet> x" if "i \<in> B" for i |
1325 |
proof - |
|
1326 |
have [simp]: "i \<bullet> j = (if j = i then 1 else 0)" if "j \<in> B" for j |
|
1327 |
using B 1 that \<open>i \<in> B\<close> |
|
1328 |
by (force simp: norm_eq_1 orthogonal_def pairwise_def) |
|
1329 |
have "i \<bullet> (\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) = (\<Sum>j\<in>B. x \<bullet> j * (i \<bullet> j))" |
|
64267 | 1330 |
by (simp add: inner_sum_right) |
63938 | 1331 |
also have "... = (\<Sum>j\<in>B. if j = i then x \<bullet> i else 0)" |
64267 | 1332 |
by (rule sum.cong; simp) |
63938 | 1333 |
also have "... = i \<bullet> x" |
64267 | 1334 |
by (simp add: \<open>finite B\<close> that inner_commute sum.delta) |
63938 | 1335 |
finally show ?thesis . |
1336 |
qed |
|
1337 |
qed |
|
1338 |
||
1339 |
||
1340 |
lemma Stone_Weierstrass_polynomial_function_subspace: |
|
1341 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
|
1342 |
assumes "compact S" |
|
1343 |
and contf: "continuous_on S f" |
|
1344 |
and "0 < e" |
|
1345 |
and "subspace T" "f ` S \<subseteq> T" |
|
1346 |
obtains g where "polynomial_function g" "g ` S \<subseteq> T" |
|
1347 |
"\<And>x. x \<in> S \<Longrightarrow> norm(f x - g x) < e" |
|
1348 |
proof - |
|
1349 |
obtain B where "B \<subseteq> T" and orthB: "pairwise orthogonal B" |
|
1350 |
and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1" |
|
1351 |
and "independent B" and cardB: "card B = dim T" |
|
1352 |
and spanB: "span B = T" |
|
1353 |
using orthonormal_basis_subspace \<open>subspace T\<close> by metis |
|
1354 |
then have "finite B" |
|
1355 |
by (simp add: independent_imp_finite) |
|
1356 |
then obtain n::nat and b where "B = b ` {i. i < n}" "inj_on b {i. i < n}" |
|
1357 |
using finite_imp_nat_seg_image_inj_on by metis |
|
1358 |
with cardB have "n = card B" "dim T = n" |
|
1359 |
by (auto simp: card_image) |
|
1360 |
have fx: "(\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i) = f x" if "x \<in> S" for x |
|
1361 |
apply (rule orthonormal_basis_expand [OF orthB B1 _ \<open>finite B\<close>]) |
|
1362 |
using \<open>f ` S \<subseteq> T\<close> spanB that by auto |
|
1363 |
have cont: "continuous_on S (\<lambda>x. \<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i)" |
|
1364 |
by (intro continuous_intros contf) |
|
1365 |
obtain g where "polynomial_function g" |
|
1366 |
and g: "\<And>x. x \<in> S \<Longrightarrow> norm ((\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i) - g x) < e / (n+2)" |
|
1367 |
using Stone_Weierstrass_polynomial_function [OF \<open>compact S\<close> cont, of "e / real (n + 2)"] \<open>0 < e\<close> |
|
1368 |
by auto |
|
1369 |
with fx have g: "\<And>x. x \<in> S \<Longrightarrow> norm (f x - g x) < e / (n+2)" |
|
1370 |
by auto |
|
1371 |
show ?thesis |
|
1372 |
proof |
|
1373 |
show "polynomial_function (\<lambda>x. \<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i)" |
|
64267 | 1374 |
apply (rule polynomial_function_sum) |
63938 | 1375 |
apply (simp add: \<open>finite B\<close>) |
1376 |
using \<open>polynomial_function g\<close> by auto |
|
1377 |
show "(\<lambda>x. \<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i) ` S \<subseteq> T" |
|
64267 | 1378 |
using \<open>B \<subseteq> T\<close> by (blast intro: subspace_sum subspace_mul \<open>subspace T\<close>) |
63938 | 1379 |
show "norm (f x - (\<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i)) < e" if "x \<in> S" for x |
1380 |
proof - |
|
1381 |
have orth': "pairwise (\<lambda>i j. orthogonal ((f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i) |
|
1382 |
((f x \<bullet> j) *\<^sub>R j - (g x \<bullet> j) *\<^sub>R j)) B" |
|
1383 |
apply (rule pairwise_mono [OF orthB]) |
|
1384 |
apply (auto simp: orthogonal_def inner_diff_right inner_diff_left) |
|
1385 |
done |
|
1386 |
then have "(norm (\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i))\<^sup>2 = |
|
1387 |
(\<Sum>i\<in>B. (norm ((f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i))\<^sup>2)" |
|
64267 | 1388 |
by (simp add: norm_sum_Pythagorean [OF \<open>finite B\<close> orth']) |
63938 | 1389 |
also have "... = (\<Sum>i\<in>B. (norm (((f x - g x) \<bullet> i) *\<^sub>R i))\<^sup>2)" |
1390 |
by (simp add: algebra_simps) |
|
1391 |
also have "... \<le> (\<Sum>i\<in>B. (norm (f x - g x))\<^sup>2)" |
|
64267 | 1392 |
apply (rule sum_mono) |
63938 | 1393 |
apply (simp add: B1) |
1394 |
apply (rule order_trans [OF Cauchy_Schwarz_ineq]) |
|
1395 |
by (simp add: B1 dot_square_norm) |
|
1396 |
also have "... = n * norm (f x - g x)^2" |
|
1397 |
by (simp add: \<open>n = card B\<close>) |
|
1398 |
also have "... \<le> n * (e / (n+2))^2" |
|
1399 |
apply (rule mult_left_mono) |
|
1400 |
apply (meson dual_order.order_iff_strict g norm_ge_zero power_mono that, simp) |
|
1401 |
done |
|
1402 |
also have "... \<le> e^2 / (n+2)" |
|
1403 |
using \<open>0 < e\<close> by (simp add: divide_simps power2_eq_square) |
|
1404 |
also have "... < e^2" |
|
1405 |
using \<open>0 < e\<close> by (simp add: divide_simps) |
|
1406 |
finally have "(norm (\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i))\<^sup>2 < e^2" . |
|
1407 |
then have "(norm (\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i)) < e" |
|
1408 |
apply (rule power2_less_imp_less) |
|
1409 |
using \<open>0 < e\<close> by auto |
|
1410 |
then show ?thesis |
|
64267 | 1411 |
using fx that by (simp add: sum_subtractf) |
63938 | 1412 |
qed |
1413 |
qed |
|
1414 |
qed |
|
1415 |
||
1416 |
||
60987 | 1417 |
hide_fact linear add mult const |
1418 |
||
1419 |
end |