author | wenzelm |
Fri, 27 Nov 2020 11:41:43 +0100 | |
changeset 72740 | 082200ee003d |
parent 72380 | becf08cb81e1 |
child 76037 | f3f1cf4711d7 |
permissions | -rw-r--r-- |
69517 | 1 |
section \<open>Bernstein-Weierstrass and Stone-Weierstrass\<close> |
61711
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 |
||
69683 | 9 |
subsection \<open>Bernstein polynomials\<close> |
60987 | 10 |
|
70136 | 11 |
definition\<^marker>\<open>tag important\<close> Bernstein :: "[nat,nat,real] \<Rightarrow> real" where |
72379 | 12 |
"Bernstein n k x \<equiv> of_nat (n choose k) * x^k * (1 - x)^(n - k)" |
60987 | 13 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
14 |
lemma Bernstein_nonneg: "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> Bernstein n k x" |
60987 | 15 |
by (simp add: Bernstein_def) |
16 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
17 |
lemma Bernstein_pos: "\<lbrakk>0 < x; x < 1; k \<le> n\<rbrakk> \<Longrightarrow> 0 < Bernstein n k x" |
60987 | 18 |
by (simp add: Bernstein_def) |
19 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
20 |
lemma sum_Bernstein [simp]: "(\<Sum>k\<le>n. Bernstein n k x) = 1" |
60987 | 21 |
using binomial_ring [of x "1-x" n] |
22 |
by (simp add: Bernstein_def) |
|
23 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
24 |
lemma binomial_deriv1: |
72379 | 25 |
"(\<Sum>k\<le>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) |
|
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
28 |
apply (rule derivative_eq_intros sum.cong | simp add: atMost_atLeast0)+ |
60987 | 29 |
done |
30 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
31 |
lemma binomial_deriv2: |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
32 |
"(\<Sum>k\<le>n. (of_nat k * of_nat (k-1) * of_nat (n choose k)) * a^(k-2) * b^(n-k)) = |
72379 | 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]) |
|
60987 | 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 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
39 |
lemma sum_k_Bernstein [simp]: "(\<Sum>k\<le>n. real k * Bernstein n k x) = of_nat n * x" |
60987 | 40 |
apply (subst binomial_deriv1 [of n x "1-x", simplified, symmetric]) |
64267 | 41 |
apply (simp add: sum_distrib_right) |
68601 | 42 |
apply (auto simp: Bernstein_def algebra_simps power_eq_if intro!: sum.cong) |
60987 | 43 |
done |
44 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
45 |
lemma sum_kk_Bernstein [simp]: "(\<Sum>k\<le>n. real k * (real k - 1) * Bernstein n k x) = real n * (real n - 1) * x\<^sup>2" |
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
46 |
proof - |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
47 |
have "(\<Sum>k\<le>n. real k * (real k - 1) * Bernstein n k x) = |
72379 | 48 |
(\<Sum>k\<le>n. real k * real (k - Suc 0) * real (n choose k) * x^(k - 2) * (1 - x)^(n - k) * x\<^sup>2)" |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
49 |
proof (rule sum.cong [OF refl], simp) |
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
50 |
fix k |
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
51 |
assume "k \<le> n" |
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
52 |
then consider "k = 0" | "k = 1" | k' where "k = Suc (Suc k')" |
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
53 |
by (metis One_nat_def not0_implies_Suc) |
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
54 |
then show "k = 0 \<or> |
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
55 |
(real k - 1) * Bernstein n k x = |
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
56 |
real (k - Suc 0) * |
72379 | 57 |
(real (n choose k) * (x^(k - 2) * ((1 - x)^(n - k) * x\<^sup>2)))" |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
58 |
by cases (auto simp add: Bernstein_def power2_eq_square algebra_simps) |
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
59 |
qed |
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
60 |
also have "... = real_of_nat n * real_of_nat (n - Suc 0) * x\<^sup>2" |
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
61 |
by (subst binomial_deriv2 [of n x "1-x", simplified, symmetric]) (simp add: sum_distrib_right) |
60987 | 62 |
also have "... = n * (n - 1) * x\<^sup>2" |
63 |
by auto |
|
64 |
finally show ?thesis |
|
65 |
by auto |
|
66 |
qed |
|
67 |
||
69683 | 68 |
subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close> |
60987 | 69 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
70 |
theorem Bernstein_Weierstrass: |
60987 | 71 |
fixes f :: "real \<Rightarrow> real" |
72 |
assumes contf: "continuous_on {0..1} f" and e: "0 < e" |
|
73 |
shows "\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> {0..1} |
|
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
74 |
\<longrightarrow> \<bar>f x - (\<Sum>k\<le>n. f(k/n) * Bernstein n k x)\<bar> < e" |
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
75 |
proof - |
60987 | 76 |
have "bounded (f ` {0..1})" |
77 |
using compact_continuous_image compact_imp_bounded contf by blast |
|
78 |
then obtain M where M: "\<And>x. 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<bar>f x\<bar> \<le> M" |
|
79 |
by (force simp add: bounded_iff) |
|
72221 | 80 |
then have "0 \<le> M" by force |
60987 | 81 |
have ucontf: "uniformly_continuous_on {0..1} f" |
82 |
using compact_uniformly_continuous contf by blast |
|
83 |
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" |
|
84 |
apply (rule uniformly_continuous_onE [where e = "e/2"]) |
|
85 |
using e by (auto simp: dist_norm) |
|
86 |
{ fix n::nat and x::real |
|
87 |
assume n: "Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>) \<le> n" and x: "0 \<le> x" "x \<le> 1" |
|
88 |
have "0 < n" using n by simp |
|
89 |
have ed0: "- (e * d\<^sup>2) < 0" |
|
61222 | 90 |
using e \<open>0<d\<close> by simp |
60987 | 91 |
also have "... \<le> M * 4" |
61222 | 92 |
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
|
93 |
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 | 94 |
using \<open>0\<le>M\<close> e \<open>0<d\<close> |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
95 |
by (simp add: field_simps) |
60987 | 96 |
have "4*M/(e*d\<^sup>2) + 1 \<le> real (Suc (nat\<lceil>4*M/(e*d\<^sup>2)\<rceil>))" |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
97 |
by (simp add: real_nat_ceiling_ge) |
60987 | 98 |
also have "... \<le> real n" |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
99 |
using n by (simp add: field_simps) |
60987 | 100 |
finally have nbig: "4*M/(e*d\<^sup>2) + 1 \<le> real n" . |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
101 |
have sum_bern: "(\<Sum>k\<le>n. (x - k/n)\<^sup>2 * Bernstein n k x) = x * (1 - x) / n" |
60987 | 102 |
proof - |
103 |
have *: "\<And>a b x::real. (a - b)\<^sup>2 * x = a * (a - 1) * x + (1 - 2 * b) * a * x + b * b * x" |
|
104 |
by (simp add: algebra_simps power2_eq_square) |
|
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
105 |
have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x) = n * x * (1 - x)" |
64267 | 106 |
apply (simp add: * sum.distrib) |
68403 | 107 |
apply (simp flip: sum_distrib_left add: mult.assoc) |
60987 | 108 |
apply (simp add: algebra_simps power2_eq_square) |
109 |
done |
|
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
110 |
then have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n" |
60987 | 111 |
by (simp add: power2_eq_square) |
112 |
then show ?thesis |
|
71633 | 113 |
using n by (simp add: sum_divide_distrib field_split_simps power2_commute) |
60987 | 114 |
qed |
115 |
{ fix k |
|
116 |
assume k: "k \<le> n" |
|
117 |
then have kn: "0 \<le> k / n" "k / n \<le> 1" |
|
70817
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70614
diff
changeset
|
118 |
by (auto simp: field_split_simps) |
61945 | 119 |
consider (lessd) "\<bar>x - k / n\<bar> < d" | (ged) "d \<le> \<bar>x - k / n\<bar>" |
60987 | 120 |
by linarith |
121 |
then have "\<bar>(f x - f (k/n))\<bar> \<le> e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2" |
|
122 |
proof cases |
|
123 |
case lessd |
|
124 |
then have "\<bar>(f x - f (k/n))\<bar> < e/2" |
|
125 |
using d x kn by (simp add: abs_minus_commute) |
|
126 |
also have "... \<le> (e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2)" |
|
72221 | 127 |
using \<open>M\<ge>0\<close> d by simp |
60987 | 128 |
finally show ?thesis by simp |
129 |
next |
|
130 |
case ged |
|
131 |
then have dle: "d\<^sup>2 \<le> (x - k/n)\<^sup>2" |
|
132 |
by (metis d(1) less_eq_real_def power2_abs power_mono) |
|
72221 | 133 |
have \<section>: "1 \<le> (x - real k / real n)\<^sup>2 / d\<^sup>2" |
134 |
using dle \<open>d>0\<close> by auto |
|
60987 | 135 |
have "\<bar>(f x - f (k/n))\<bar> \<le> \<bar>f x\<bar> + \<bar>f (k/n)\<bar>" |
136 |
by (rule abs_triangle_ineq4) |
|
137 |
also have "... \<le> M+M" |
|
138 |
by (meson M add_mono_thms_linordered_semiring(1) kn x) |
|
139 |
also have "... \<le> 2 * M * ((x - k/n)\<^sup>2 / d\<^sup>2)" |
|
72221 | 140 |
using \<section> \<open>M\<ge>0\<close> mult_left_mono by fastforce |
60987 | 141 |
also have "... \<le> e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2" |
142 |
using e by simp |
|
143 |
finally show ?thesis . |
|
144 |
qed |
|
145 |
} note * = this |
|
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
146 |
have "\<bar>f x - (\<Sum>k\<le>n. f(k / n) * Bernstein n k x)\<bar> \<le> \<bar>\<Sum>k\<le>n. (f x - f(k / n)) * Bernstein n k x\<bar>" |
64267 | 147 |
by (simp add: sum_subtractf sum_distrib_left [symmetric] algebra_simps) |
72221 | 148 |
also have "... \<le> (\<Sum>k\<le>n. \<bar>(f x - f(k / n)) * Bernstein n k x\<bar>)" |
149 |
by (rule sum_abs) |
|
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
150 |
also have "... \<le> (\<Sum>k\<le>n. (e/2 + (2 * M / d\<^sup>2) * (x - k / n)\<^sup>2) * Bernstein n k x)" |
60987 | 151 |
using * |
72221 | 152 |
by (force simp add: abs_mult Bernstein_nonneg x mult_right_mono intro: sum_mono) |
60987 | 153 |
also have "... \<le> e/2 + (2 * M) / (d\<^sup>2 * n)" |
72221 | 154 |
unfolding sum.distrib Rings.semiring_class.distrib_right sum_distrib_left [symmetric] mult.assoc sum_bern |
155 |
using \<open>d>0\<close> x by (simp add: divide_simps \<open>M\<ge>0\<close> mult_le_one mult_left_le) |
|
60987 | 156 |
also have "... < e" |
72221 | 157 |
using \<open>d>0\<close> nbig e \<open>n>0\<close> |
71633 | 158 |
apply (simp add: field_split_simps) |
60987 | 159 |
using ed0 by linarith |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
160 |
finally have "\<bar>f x - (\<Sum>k\<le>n. f (real k / real n) * Bernstein n k x)\<bar> < e" . |
60987 | 161 |
} |
162 |
then show ?thesis |
|
163 |
by auto |
|
164 |
qed |
|
165 |
||
166 |
||
69683 | 167 |
subsection \<open>General Stone-Weierstrass theorem\<close> |
60987 | 168 |
|
169 |
text\<open>Source: |
|
170 |
Bruno Brosowski and Frank Deutsch. |
|
171 |
An Elementary Proof of the Stone-Weierstrass Theorem. |
|
172 |
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
|
173 |
Volume 81, Number 1, January 1981. |
70138 | 174 |
DOI: 10.2307/2043993 \<^url>\<open>https://www.jstor.org/stable/2043993\<close>\<close> |
60987 | 175 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
176 |
locale function_ring_on = |
63938 | 177 |
fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set" |
178 |
assumes compact: "compact S" |
|
179 |
assumes continuous: "f \<in> R \<Longrightarrow> continuous_on S f" |
|
60987 | 180 |
assumes add: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x + g x) \<in> R" |
181 |
assumes mult: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x * g x) \<in> R" |
|
182 |
assumes const: "(\<lambda>_. c) \<in> R" |
|
63938 | 183 |
assumes separable: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> \<exists>f\<in>R. f x \<noteq> f y" |
60987 | 184 |
|
185 |
begin |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
186 |
lemma minus: "f \<in> R \<Longrightarrow> (\<lambda>x. - f x) \<in> R" |
60987 | 187 |
by (frule mult [OF const [of "-1"]]) simp |
188 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
189 |
lemma diff: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x - g x) \<in> R" |
60987 | 190 |
unfolding diff_conv_add_uminus by (metis add minus) |
191 |
||
72379 | 192 |
lemma power: "f \<in> R \<Longrightarrow> (\<lambda>x. f x^n) \<in> R" |
60987 | 193 |
by (induct n) (auto simp: const mult) |
194 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
195 |
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 | 196 |
by (induct I rule: finite_induct; simp add: const add) |
197 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
198 |
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 | 199 |
by (induct I rule: finite_induct; simp add: const mult) |
200 |
||
70136 | 201 |
definition\<^marker>\<open>tag important\<close> normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real" |
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
68833
diff
changeset
|
202 |
where "normf f \<equiv> SUP x\<in>S. \<bar>f x\<bar>" |
60987 | 203 |
|
72221 | 204 |
lemma normf_upper: |
205 |
assumes "continuous_on S f" "x \<in> S" shows "\<bar>f x\<bar> \<le> normf f" |
|
206 |
proof - |
|
207 |
have "bdd_above ((\<lambda>x. \<bar>f x\<bar>) ` S)" |
|
208 |
by (simp add: assms(1) bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs) |
|
209 |
then show ?thesis |
|
210 |
using assms cSUP_upper normf_def by fastforce |
|
211 |
qed |
|
60987 | 212 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
213 |
lemma normf_least: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M" |
60987 | 214 |
by (simp add: normf_def cSUP_least) |
215 |
||
216 |
end |
|
217 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
218 |
lemma (in function_ring_on) one: |
63938 | 219 |
assumes U: "open U" and t0: "t0 \<in> S" "t0 \<in> U" and t1: "t1 \<in> S-U" |
220 |
shows "\<exists>V. open V \<and> t0 \<in> V \<and> S \<inter> V \<subseteq> U \<and> |
|
221 |
(\<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))" |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
222 |
proof - |
63938 | 223 |
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 | 224 |
proof - |
225 |
have "t \<noteq> t0" using t t0 by auto |
|
226 |
then obtain g where g: "g \<in> R" "g t \<noteq> g t0" |
|
227 |
using separable t0 by (metis Diff_subset subset_eq t) |
|
63040 | 228 |
define h where [abs_def]: "h x = g x - g t0" for x |
60987 | 229 |
have "h \<in> R" |
230 |
unfolding h_def by (fast intro: g const diff) |
|
231 |
then have hsq: "(\<lambda>w. (h w)\<^sup>2) \<in> R" |
|
232 |
by (simp add: power2_eq_square mult) |
|
233 |
have "h t \<noteq> h t0" |
|
234 |
by (simp add: h_def g) |
|
235 |
then have "h t \<noteq> 0" |
|
236 |
by (simp add: h_def) |
|
237 |
then have ht2: "0 < (h t)^2" |
|
238 |
by simp |
|
239 |
also have "... \<le> normf (\<lambda>w. (h w)\<^sup>2)" |
|
240 |
using t normf_upper [where x=t] continuous [OF hsq] by force |
|
241 |
finally have nfp: "0 < normf (\<lambda>w. (h w)\<^sup>2)" . |
|
63040 | 242 |
define p where [abs_def]: "p x = (1 / normf (\<lambda>w. (h w)\<^sup>2)) * (h x)^2" for x |
60987 | 243 |
have "p \<in> R" |
244 |
unfolding p_def by (fast intro: hsq const mult) |
|
245 |
moreover have "p t0 = 0" |
|
246 |
by (simp add: p_def h_def) |
|
247 |
moreover have "p t > 0" |
|
248 |
using nfp ht2 by (simp add: p_def) |
|
63938 | 249 |
moreover have "\<And>x. x \<in> S \<Longrightarrow> p x \<in> {0..1}" |
60987 | 250 |
using nfp normf_upper [OF continuous [OF hsq] ] by (auto simp: p_def) |
63938 | 251 |
ultimately show "\<exists>pt \<in> R. pt t0 = 0 \<and> pt t > 0 \<and> pt ` S \<subseteq> {0..1}" |
60987 | 252 |
by auto |
253 |
qed |
|
63938 | 254 |
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" |
255 |
and pf01: "\<And>t. t \<in> S-U \<Longrightarrow> pf t ` S \<subseteq> {0..1}" |
|
60987 | 256 |
by metis |
63938 | 257 |
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
|
258 |
using compact closed_Int_compact U by (simp add: Diff_eq compact_Int_closed open_closed) |
63938 | 259 |
have "\<And>t. t \<in> S-U \<Longrightarrow> \<exists>A. open A \<and> A \<inter> S = {x\<in>S. 0 < pf t x}" |
60987 | 260 |
apply (rule open_Collect_positive) |
261 |
by (metis pf continuous) |
|
63938 | 262 |
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 | 263 |
by metis |
63938 | 264 |
then have open_Uf: "\<And>t. t \<in> S-U \<Longrightarrow> open (Uf t)" |
60987 | 265 |
by blast |
63938 | 266 |
have tUft: "\<And>t. t \<in> S-U \<Longrightarrow> t \<in> Uf t" |
60987 | 267 |
using pf Uf by blast |
63938 | 268 |
then have *: "S-U \<subseteq> (\<Union>x \<in> S-U. Uf x)" |
60987 | 269 |
by blast |
63938 | 270 |
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
|
271 |
by (blast intro: that compactE_image [OF com_sU open_Uf *]) |
60987 | 272 |
then have [simp]: "subU \<noteq> {}" |
273 |
using t1 by auto |
|
274 |
then have cardp: "card subU > 0" using subU |
|
275 |
by (simp add: card_gt_0_iff) |
|
63040 | 276 |
define p where [abs_def]: "p x = (1 / card subU) * (\<Sum>t \<in> subU. pf t x)" for x |
60987 | 277 |
have pR: "p \<in> R" |
64267 | 278 |
unfolding p_def using subU pf by (fast intro: pf const mult sum) |
60987 | 279 |
have pt0 [simp]: "p t0 = 0" |
64267 | 280 |
using subU pf by (auto simp: p_def intro: sum.neutral) |
63938 | 281 |
have pt_pos: "p t > 0" if t: "t \<in> S-U" for t |
60987 | 282 |
proof - |
283 |
obtain i where i: "i \<in> subU" "t \<in> Uf i" using subU t by blast |
|
284 |
show ?thesis |
|
285 |
using subU i t |
|
70817
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70614
diff
changeset
|
286 |
apply (clarsimp simp: p_def field_split_simps) |
64267 | 287 |
apply (rule sum_pos2 [OF \<open>finite subU\<close>]) |
60987 | 288 |
using Uf t pf01 apply auto |
289 |
apply (force elim!: subsetCE) |
|
290 |
done |
|
291 |
qed |
|
63938 | 292 |
have p01: "p x \<in> {0..1}" if t: "x \<in> S" for x |
60987 | 293 |
proof - |
294 |
have "0 \<le> p x" |
|
72379 | 295 |
using subU cardp t pf01 |
296 |
by (fastforce simp add: p_def field_split_simps intro: sum_nonneg) |
|
60987 | 297 |
moreover have "p x \<le> 1" |
72379 | 298 |
using subU cardp t |
299 |
apply (simp add: p_def field_split_simps) |
|
64267 | 300 |
apply (rule sum_bounded_above [where 'a=real and K=1, simplified]) |
60987 | 301 |
using pf01 by force |
302 |
ultimately show ?thesis |
|
303 |
by auto |
|
304 |
qed |
|
63938 | 305 |
have "compact (p ` (S-U))" |
60987 | 306 |
by (meson Diff_subset com_sU compact_continuous_image continuous continuous_on_subset pR) |
63938 | 307 |
then have "open (- (p ` (S-U)))" |
60987 | 308 |
by (simp add: compact_imp_closed open_Compl) |
63938 | 309 |
moreover have "0 \<in> - (p ` (S-U))" |
60987 | 310 |
by (metis (no_types) ComplI image_iff not_less_iff_gr_or_eq pt_pos) |
63938 | 311 |
ultimately obtain delta0 where delta0: "delta0 > 0" "ball 0 delta0 \<subseteq> - (p ` (S-U))" |
60987 | 312 |
by (auto simp: elim!: openE) |
63938 | 313 |
then have pt_delta: "\<And>x. x \<in> S-U \<Longrightarrow> p x \<ge> delta0" |
60987 | 314 |
by (force simp: ball_def dist_norm dest: p01) |
63040 | 315 |
define \<delta> where "\<delta> = delta0/2" |
60987 | 316 |
have "delta0 \<le> 1" using delta0 p01 [of t1] t1 |
317 |
by (force simp: ball_def dist_norm dest: p01) |
|
318 |
with delta0 have \<delta>01: "0 < \<delta>" "\<delta> < 1" |
|
319 |
by (auto simp: \<delta>_def) |
|
63938 | 320 |
have pt_\<delta>: "\<And>x. x \<in> S-U \<Longrightarrow> p x \<ge> \<delta>" |
60987 | 321 |
using pt_delta delta0 by (force simp: \<delta>_def) |
63938 | 322 |
have "\<exists>A. open A \<and> A \<inter> S = {x\<in>S. p x < \<delta>/2}" |
60987 | 323 |
by (rule open_Collect_less_Int [OF continuous [OF pR] continuous_on_const]) |
63938 | 324 |
then obtain V where V: "open V" "V \<inter> S = {x\<in>S. p x < \<delta>/2}" |
60987 | 325 |
by blast |
63040 | 326 |
define k where "k = nat\<lfloor>1/\<delta>\<rfloor> + 1" |
60987 | 327 |
have "k>0" by (simp add: k_def) |
328 |
have "k-1 \<le> 1/\<delta>" |
|
329 |
using \<delta>01 by (simp add: k_def) |
|
330 |
with \<delta>01 have "k \<le> (1+\<delta>)/\<delta>" |
|
331 |
by (auto simp: algebra_simps add_divide_distrib) |
|
332 |
also have "... < 2/\<delta>" |
|
70817
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70614
diff
changeset
|
333 |
using \<delta>01 by (auto simp: field_split_simps) |
60987 | 334 |
finally have k2\<delta>: "k < 2/\<delta>" . |
335 |
have "1/\<delta> < k" |
|
336 |
using \<delta>01 unfolding k_def by linarith |
|
337 |
with \<delta>01 k2\<delta> have k\<delta>: "1 < k*\<delta>" "k*\<delta> < 2" |
|
70817
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70614
diff
changeset
|
338 |
by (auto simp: field_split_simps) |
72379 | 339 |
define q where [abs_def]: "q n t = (1 - p t^n)^(k^n)" for n t |
60987 | 340 |
have qR: "q n \<in> R" for n |
341 |
by (simp add: q_def const diff power pR) |
|
63938 | 342 |
have q01: "\<And>n t. t \<in> S \<Longrightarrow> q n t \<in> {0..1}" |
60987 | 343 |
using p01 by (simp add: q_def power_le_one algebra_simps) |
344 |
have qt0 [simp]: "\<And>n. n>0 \<Longrightarrow> q n t0 = 1" |
|
345 |
using t0 pf by (simp add: q_def power_0_left) |
|
346 |
{ fix t and n::nat |
|
63938 | 347 |
assume t: "t \<in> S \<inter> V" |
61222 | 348 |
with \<open>k>0\<close> V have "k * p t < k * \<delta> / 2" |
60987 | 349 |
by force |
350 |
then have "1 - (k * \<delta> / 2)^n \<le> 1 - (k * p t)^n" |
|
61222 | 351 |
using \<open>k>0\<close> p01 t by (simp add: power_mono) |
60987 | 352 |
also have "... \<le> q n t" |
72379 | 353 |
using Bernoulli_inequality [of "- ((p t)^n)" "k^n"] |
60987 | 354 |
apply (simp add: q_def) |
355 |
by (metis IntE atLeastAtMost_iff p01 power_le_one power_mult_distrib t) |
|
72379 | 356 |
finally have "1 - (k * \<delta> / 2)^n \<le> q n t" . |
60987 | 357 |
} note limitV = this |
358 |
{ fix t and n::nat |
|
63938 | 359 |
assume t: "t \<in> S - U" |
61222 | 360 |
with \<open>k>0\<close> U have "k * \<delta> \<le> k * p t" |
60987 | 361 |
by (simp add: pt_\<delta>) |
362 |
with k\<delta> have kpt: "1 < k * p t" |
|
363 |
by (blast intro: less_le_trans) |
|
72379 | 364 |
have ptn_pos: "0 < p t^n" |
60987 | 365 |
using pt_pos [OF t] by simp |
72379 | 366 |
have ptn_le: "p t^n \<le> 1" |
60987 | 367 |
by (meson DiffE atLeastAtMost_iff p01 power_le_one t) |
72379 | 368 |
have "q n t = (1/(k^n * (p t)^n)) * (1 - p t^n)^(k^n) * k^n * (p t)^n" |
61222 | 369 |
using pt_pos [OF t] \<open>k>0\<close> by (simp add: q_def) |
72379 | 370 |
also have "... \<le> (1/(k * (p t))^n) * (1 - p t^n)^(k^n) * (1 + k^n * (p t)^n)" |
61222 | 371 |
using pt_pos [OF t] \<open>k>0\<close> |
72379 | 372 |
by (simp add: divide_simps mult_left_mono ptn_le) |
373 |
also have "... \<le> (1/(k * (p t))^n) * (1 - p t^n)^(k^n) * (1 + (p t)^n)^(k^n)" |
|
374 |
proof (rule mult_left_mono [OF Bernoulli_inequality]) |
|
375 |
show "0 \<le> 1 / (real k * p t)^n * (1 - p t^n)^k^n" |
|
376 |
using ptn_pos ptn_le by (auto simp: power_mult_distrib) |
|
377 |
qed (use ptn_pos in auto) |
|
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> |
68403 | 380 |
by (simp add: algebra_simps power_mult power2_eq_square flip: power_mult_distrib) |
60987 | 381 |
also have "... \<le> (1/(k * (p t))^n) * 1" |
72379 | 382 |
using pt_pos \<open>k>0\<close> p01 power_le_one t |
383 |
by (intro mult_left_mono [OF power_le_one]) auto |
|
60987 | 384 |
also have "... \<le> (1 / (k*\<delta>))^n" |
61222 | 385 |
using \<open>k>0\<close> \<delta>01 power_mono pt_\<delta> t |
60987 | 386 |
by (fastforce simp: field_simps) |
72379 | 387 |
finally have "q n t \<le> (1 / (real k * \<delta>))^n " . |
60987 | 388 |
} note limitNonU = this |
63040 | 389 |
define NN |
390 |
where "NN e = 1 + nat \<lceil>max (ln e / ln (real k * \<delta> / 2)) (- ln e / ln (real k * \<delta>))\<rceil>" for e |
|
60987 | 391 |
have NN: "of_nat (NN e) > ln e / ln (real k * \<delta> / 2)" "of_nat (NN e) > - ln e / ln (real k * \<delta>)" |
392 |
if "0<e" for e |
|
393 |
unfolding NN_def by linarith+ |
|
72221 | 394 |
have NN1: "(k * \<delta> / 2)^NN e < e" if "e>0" for e |
395 |
proof - |
|
72379 | 396 |
have "ln ((real k * \<delta> / 2)^NN e) = real (NN e) * ln (real k * \<delta> / 2)" |
397 |
by (simp add: \<open>\<delta>>0\<close> \<open>0 < k\<close> ln_realpow) |
|
398 |
also have "... < ln e" |
|
399 |
using NN k\<delta> that by (force simp add: field_simps) |
|
400 |
finally show ?thesis |
|
72221 | 401 |
by (simp add: \<open>\<delta>>0\<close> \<open>0 < k\<close> that) |
402 |
qed |
|
72379 | 403 |
have NN0: "(1/(k*\<delta>))^(NN e) < e" if "e>0" for e |
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
|
404 |
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
|
405 |
have "0 < ln (real k) + ln \<delta>" |
65585
a043de9ad41e
Some fixes related to compactE_image
paulson <lp15@cam.ac.uk>
parents:
65583
diff
changeset
|
406 |
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
|
407 |
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
|
408 |
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
|
409 |
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
|
410 |
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
|
411 |
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
|
412 |
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
|
413 |
qed |
60987 | 414 |
{ fix t and e::real |
415 |
assume "e>0" |
|
63938 | 416 |
have "t \<in> S \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> S - U \<Longrightarrow> q (NN e) t < e" |
60987 | 417 |
proof - |
63938 | 418 |
assume t: "t \<in> S \<inter> V" |
60987 | 419 |
show "1 - q (NN e) t < e" |
61222 | 420 |
by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF \<open>e>0\<close>]]) |
60987 | 421 |
next |
63938 | 422 |
assume t: "t \<in> S - U" |
60987 | 423 |
show "q (NN e) t < e" |
61222 | 424 |
using limitNonU [OF t] less_le_trans [OF NN0 [OF \<open>e>0\<close>]] not_le by blast |
60987 | 425 |
qed |
63938 | 426 |
} 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 | 427 |
using q01 |
428 |
by (rule_tac x="\<lambda>x. 1 - q (NN e) x" in bexI) (auto simp: algebra_simps intro: diff const qR) |
|
63938 | 429 |
moreover have t0V: "t0 \<in> V" "S \<inter> V \<subseteq> U" |
60987 | 430 |
using pt_\<delta> t0 U V \<delta>01 by fastforce+ |
431 |
ultimately show ?thesis using V t0V |
|
432 |
by blast |
|
433 |
qed |
|
434 |
||
69597 | 435 |
text\<open>Non-trivial case, with \<^term>\<open>A\<close> and \<^term>\<open>B\<close> both non-empty\<close> |
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
436 |
lemma (in function_ring_on) two_special: |
63938 | 437 |
assumes A: "closed A" "A \<subseteq> S" "a \<in> A" |
438 |
and B: "closed B" "B \<subseteq> S" "b \<in> B" |
|
60987 | 439 |
and disj: "A \<inter> B = {}" |
440 |
and e: "0 < e" "e < 1" |
|
63938 | 441 |
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 | 442 |
proof - |
443 |
{ fix w |
|
444 |
assume "w \<in> A" |
|
63938 | 445 |
then have "open ( - B)" "b \<in> S" "w \<notin> B" "w \<in> S" |
60987 | 446 |
using assms by auto |
63938 | 447 |
then have "\<exists>V. open V \<and> w \<in> V \<and> S \<inter> V \<subseteq> -B \<and> |
448 |
(\<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 | 449 |
using one [of "-B" w b] assms \<open>w \<in> A\<close> by simp |
60987 | 450 |
} |
451 |
then obtain Vf where Vf: |
|
63938 | 452 |
"\<And>w. w \<in> A \<Longrightarrow> open (Vf w) \<and> w \<in> Vf w \<and> S \<inter> Vf w \<subseteq> -B \<and> |
453 |
(\<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 | 454 |
by metis |
455 |
then have open_Vf: "\<And>w. w \<in> A \<Longrightarrow> open (Vf w)" |
|
456 |
by blast |
|
457 |
have tVft: "\<And>w. w \<in> A \<Longrightarrow> w \<in> Vf w" |
|
458 |
using Vf by blast |
|
64267 | 459 |
then have sum_max_0: "A \<subseteq> (\<Union>x \<in> A. Vf x)" |
60987 | 460 |
by blast |
461 |
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
|
462 |
by (metis compact compact_Int_closed inf.absorb_iff2) |
60987 | 463 |
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
|
464 |
by (blast intro: that compactE_image [OF com_A open_Vf sum_max_0]) |
60987 | 465 |
then have [simp]: "subA \<noteq> {}" |
61222 | 466 |
using \<open>a \<in> A\<close> by auto |
60987 | 467 |
then have cardp: "card subA > 0" using subA |
468 |
by (simp add: card_gt_0_iff) |
|
63938 | 469 |
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 | 470 |
using Vf e cardp by simp |
471 |
then obtain ff where ff: |
|
63938 | 472 |
"\<And>w. w \<in> A \<Longrightarrow> ff w \<in> R \<and> ff w ` S \<subseteq> {0..1} \<and> |
473 |
(\<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 | 474 |
by metis |
63040 | 475 |
define pff where [abs_def]: "pff x = (\<Prod>w \<in> subA. ff w x)" for x |
60987 | 476 |
have pffR: "pff \<in> R" |
64272 | 477 |
unfolding pff_def using subA ff by (auto simp: intro: prod) |
60987 | 478 |
moreover |
63938 | 479 |
have pff01: "pff x \<in> {0..1}" if t: "x \<in> S" for x |
60987 | 480 |
proof - |
481 |
have "0 \<le> pff x" |
|
72221 | 482 |
using subA cardp t ff |
483 |
by (fastforce simp: pff_def field_split_simps sum_nonneg intro: prod_nonneg) |
|
60987 | 484 |
moreover have "pff x \<le> 1" |
72221 | 485 |
using subA cardp t ff |
486 |
by (fastforce simp add: pff_def field_split_simps sum_nonneg intro: prod_mono [where g = "\<lambda>x. 1", simplified]) |
|
60987 | 487 |
ultimately show ?thesis |
488 |
by auto |
|
489 |
qed |
|
490 |
moreover |
|
491 |
{ fix v x |
|
63938 | 492 |
assume v: "v \<in> subA" and x: "x \<in> Vf v" "x \<in> S" |
60987 | 493 |
from subA v have "pff x = ff v x * (\<Prod>w \<in> subA - {v}. ff w x)" |
64272 | 494 |
unfolding pff_def by (metis prod.remove) |
60987 | 495 |
also have "... \<le> ff v x * 1" |
72221 | 496 |
proof - |
497 |
have "\<And>i. i \<in> subA - {v} \<Longrightarrow> 0 \<le> ff i x \<and> ff i x \<le> 1" |
|
498 |
by (metis Diff_subset atLeastAtMost_iff ff image_subset_iff subA(1) subsetD x(2)) |
|
499 |
moreover have "0 \<le> ff v x" |
|
500 |
using ff subA(1) v x(2) by fastforce |
|
501 |
ultimately show ?thesis |
|
502 |
by (metis mult_left_mono prod_mono [where g = "\<lambda>x. 1", simplified]) |
|
503 |
qed |
|
60987 | 504 |
also have "... < e / card subA" |
72221 | 505 |
using ff subA(1) v x by auto |
60987 | 506 |
also have "... \<le> e" |
70817
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70614
diff
changeset
|
507 |
using cardp e by (simp add: field_split_simps) |
60987 | 508 |
finally have "pff x < e" . |
509 |
} |
|
510 |
then have "\<And>x. x \<in> A \<Longrightarrow> pff x < e" |
|
511 |
using A Vf subA by (metis UN_E contra_subsetD) |
|
512 |
moreover |
|
513 |
{ fix x |
|
514 |
assume x: "x \<in> B" |
|
63938 | 515 |
then have "x \<in> S" |
60987 | 516 |
using B by auto |
72379 | 517 |
have "1 - e \<le> (1 - e / card subA)^card subA" |
60987 | 518 |
using Bernoulli_inequality [of "-e / card subA" "card subA"] e cardp |
519 |
by (auto simp: field_simps) |
|
520 |
also have "... = (\<Prod>w \<in> subA. 1 - e / card subA)" |
|
71172 | 521 |
by (simp add: subA(2)) |
60987 | 522 |
also have "... < pff x" |
72221 | 523 |
proof - |
524 |
have "\<And>i. i \<in> subA \<Longrightarrow> e / real (card subA) \<le> 1 \<and> 1 - e / real (card subA) < ff i x" |
|
525 |
using e \<open>B \<subseteq> S\<close> ff subA(1) x by (force simp: field_split_simps) |
|
526 |
then show ?thesis |
|
72379 | 527 |
using prod_mono_strict [where f = "\<lambda>x. 1 - e / card subA"] subA(2) by (force simp add: pff_def) |
72221 | 528 |
qed |
60987 | 529 |
finally have "1 - e < pff x" . |
530 |
} |
|
72221 | 531 |
ultimately show ?thesis by blast |
60987 | 532 |
qed |
533 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
534 |
lemma (in function_ring_on) two: |
63938 | 535 |
assumes A: "closed A" "A \<subseteq> S" |
536 |
and B: "closed B" "B \<subseteq> S" |
|
60987 | 537 |
and disj: "A \<inter> B = {}" |
538 |
and e: "0 < e" "e < 1" |
|
63938 | 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)" |
60987 | 540 |
proof (cases "A \<noteq> {} \<and> B \<noteq> {}") |
541 |
case True then show ?thesis |
|
542 |
using assms |
|
72221 | 543 |
by (force simp flip: ex_in_conv intro!: two_special) |
60987 | 544 |
next |
72379 | 545 |
case False |
546 |
then consider "A={}" | "B={}" by force |
|
547 |
then show ?thesis |
|
548 |
proof cases |
|
549 |
case 1 |
|
550 |
with e show ?thesis |
|
551 |
by (rule_tac x="\<lambda>x. 1" in bexI) (auto simp: const) |
|
552 |
next |
|
553 |
case 2 |
|
554 |
with e show ?thesis |
|
555 |
by (rule_tac x="\<lambda>x. 0" in bexI) (auto simp: const) |
|
556 |
qed |
|
60987 | 557 |
qed |
558 |
||
69597 | 559 |
text\<open>The special case where \<^term>\<open>f\<close> is non-negative and \<^term>\<open>e<1/3\<close>\<close> |
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
560 |
lemma (in function_ring_on) Stone_Weierstrass_special: |
63938 | 561 |
assumes f: "continuous_on S f" and fpos: "\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0" |
60987 | 562 |
and e: "0 < e" "e < 1/3" |
63938 | 563 |
shows "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>f x - g x\<bar> < 2*e" |
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
564 |
proof - |
63040 | 565 |
define n where "n = 1 + nat \<lceil>normf f / e\<rceil>" |
63938 | 566 |
define A where "A j = {x \<in> S. f x \<le> (j - 1/3)*e}" for j :: nat |
567 |
define B where "B j = {x \<in> S. f x \<ge> (j + 1/3)*e}" for j :: nat |
|
72379 | 568 |
have ngt: "(n-1) * e \<ge> normf f" |
569 |
using e pos_divide_le_eq real_nat_ceiling_ge[of "normf f / e"] |
|
570 |
by (fastforce simp add: divide_simps n_def) |
|
571 |
moreover have "n\<ge>1" |
|
572 |
by (simp_all add: n_def) |
|
573 |
ultimately have ge_fx: "(n-1) * e \<ge> f x" if "x \<in> S" for x |
|
60987 | 574 |
using f normf_upper that by fastforce |
72379 | 575 |
have "closed S" |
576 |
by (simp add: compact compact_imp_closed) |
|
60987 | 577 |
{ fix j |
72379 | 578 |
have "closed (A j)" "A j \<subseteq> S" |
579 |
using \<open>closed S\<close> continuous_on_closed_Collect_le [OF f continuous_on_const] |
|
580 |
by (simp_all add: A_def Collect_restrict) |
|
581 |
moreover have "closed (B j)" "B j \<subseteq> S" |
|
582 |
using \<open>closed S\<close> continuous_on_closed_Collect_le [OF continuous_on_const f] |
|
583 |
by (simp_all add: B_def Collect_restrict) |
|
584 |
moreover have "(A j) \<inter> (B j) = {}" |
|
60987 | 585 |
using e by (auto simp: A_def B_def field_simps) |
72379 | 586 |
ultimately 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)" |
587 |
using e \<open>1 \<le> n\<close> by (auto intro: two) |
|
60987 | 588 |
} |
63938 | 589 |
then obtain xf where xfR: "\<And>j. xf j \<in> R" and xf01: "\<And>j. xf j ` S \<subseteq> {0..1}" |
60987 | 590 |
and xfA: "\<And>x j. x \<in> A j \<Longrightarrow> xf j x < e/n" |
591 |
and xfB: "\<And>x j. x \<in> B j \<Longrightarrow> xf j x > 1 - e/n" |
|
592 |
by metis |
|
63040 | 593 |
define g where [abs_def]: "g x = e * (\<Sum>i\<le>n. xf i x)" for x |
60987 | 594 |
have gR: "g \<in> R" |
64267 | 595 |
unfolding g_def by (fast intro: mult const sum xfR) |
63938 | 596 |
have gge0: "\<And>x. x \<in> S \<Longrightarrow> g x \<ge> 0" |
64267 | 597 |
using e xf01 by (simp add: g_def zero_le_mult_iff image_subset_iff sum_nonneg) |
60987 | 598 |
have A0: "A 0 = {}" |
599 |
using fpos e by (fastforce simp: A_def) |
|
63938 | 600 |
have An: "A n = S" |
72379 | 601 |
using e ngt \<open>n\<ge>1\<close> f normf_upper by (fastforce simp: A_def field_simps of_nat_diff) |
60987 | 602 |
have Asub: "A j \<subseteq> A i" if "i\<ge>j" for i j |
72379 | 603 |
using e that by (force simp: A_def intro: order_trans) |
60987 | 604 |
{ fix t |
63938 | 605 |
assume t: "t \<in> S" |
63040 | 606 |
define j where "j = (LEAST j. t \<in> A j)" |
60987 | 607 |
have jn: "j \<le> n" |
608 |
using t An by (simp add: Least_le j_def) |
|
609 |
have Aj: "t \<in> A j" |
|
610 |
using t An by (fastforce simp add: j_def intro: LeastI) |
|
611 |
then have Ai: "t \<in> A i" if "i\<ge>j" for i |
|
612 |
using Asub [OF that] by blast |
|
613 |
then have fj1: "f t \<le> (j - 1/3)*e" |
|
614 |
by (simp add: A_def) |
|
615 |
then have Anj: "t \<notin> A i" if "i<j" for i |
|
72379 | 616 |
using Aj \<open>i<j\<close> not_less_Least by (fastforce simp add: j_def) |
60987 | 617 |
have j1: "1 \<le> j" |
618 |
using A0 Aj j_def not_less_eq_eq by (fastforce simp add: j_def) |
|
619 |
then have Anj: "t \<notin> A (j-1)" |
|
620 |
using Least_le by (fastforce simp add: j_def) |
|
621 |
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
|
622 |
using j1 t by (simp add: A_def of_nat_diff) |
60987 | 623 |
have xf_le1: "\<And>i. xf i t \<le> 1" |
624 |
using xf01 t by force |
|
72379 | 625 |
have "g t = e * (\<Sum>i\<le>n. xf i t)" |
626 |
by (simp add: g_def flip: distrib_left) |
|
627 |
also have "... = e * (\<Sum>i \<in> {..<j} \<union> {j..n}. xf i t)" |
|
628 |
by (simp add: ivl_disj_un_one(4) jn) |
|
629 |
also have "... = e * (\<Sum>i<j. xf i t) + e * (\<Sum>i=j..n. xf i t)" |
|
630 |
by (simp add: distrib_left ivl_disj_int sum.union_disjoint) |
|
60987 | 631 |
also have "... \<le> e*j + e * ((Suc n - j)*e/n)" |
72379 | 632 |
proof (intro add_mono mult_left_mono) |
633 |
show "(\<Sum>i<j. xf i t) \<le> j" |
|
634 |
by (rule sum_bounded_above [OF xf_le1, where A = "lessThan j", simplified]) |
|
635 |
have "xf i t \<le> e/n" if "i\<ge>j" for i |
|
636 |
using xfA [OF Ai] that by (simp add: less_eq_real_def) |
|
637 |
then show "(\<Sum>i = j..n. xf i t) \<le> real (Suc n - j) * e / real n" |
|
638 |
using sum_bounded_above [of "{j..n}" "\<lambda>i. xf i t"] |
|
639 |
by fastforce |
|
640 |
qed (use e in auto) |
|
60987 | 641 |
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
|
642 |
using \<open>1 \<le> n\<close> e by (simp add: field_simps del: of_nat_Suc) |
60987 | 643 |
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
|
644 |
using \<open>1 \<le> n\<close> e j1 by (simp add: field_simps del: of_nat_Suc) |
60987 | 645 |
also have "... < (j + 1/3)*e" |
646 |
using e by (auto simp: field_simps) |
|
647 |
finally have gj1: "g t < (j + 1 / 3) * e" . |
|
648 |
have gj2: "(j - 4/3)*e < g t" |
|
649 |
proof (cases "2 \<le> j") |
|
650 |
case False |
|
651 |
then have "j=1" using j1 by simp |
|
652 |
with t gge0 e show ?thesis by force |
|
653 |
next |
|
654 |
case True |
|
655 |
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
|
656 |
using e by (auto simp: of_nat_diff algebra_simps power2_eq_square) |
60987 | 657 |
also have "... < (j-1)*e - ((j - 1)/n) * e^2" |
658 |
using e True jn by (simp add: power2_eq_square field_simps) |
|
659 |
also have "... = e * (j-1) * (1 - e/n)" |
|
660 |
by (simp add: power2_eq_square field_simps) |
|
661 |
also have "... \<le> e * (\<Sum>i\<le>j-2. xf i t)" |
|
72379 | 662 |
proof - |
663 |
{ fix i |
|
664 |
assume "i+2 \<le> j" |
|
665 |
then obtain d where "i+2+d = j" |
|
666 |
using le_Suc_ex that by blast |
|
667 |
then have "t \<in> B i" |
|
668 |
using Anj e ge_fx [OF t] \<open>1 \<le> n\<close> fpos [OF t] t |
|
669 |
unfolding A_def B_def |
|
670 |
by (auto simp add: field_simps of_nat_diff not_le intro: order_trans [of _ "e * 2 + e * d * 3 + e * i * 3"]) |
|
671 |
then have "xf i t > 1 - e/n" |
|
672 |
by (rule xfB) |
|
673 |
} |
|
674 |
moreover have "real (j - Suc 0) * (1 - e / real n) \<le> real (card {..j - 2}) * (1 - e / real n)" |
|
675 |
using Suc_diff_le True by fastforce |
|
676 |
ultimately show ?thesis |
|
677 |
using e True by (auto intro: order_trans [OF _ sum_bounded_below [OF less_imp_le]]) |
|
678 |
qed |
|
60987 | 679 |
also have "... \<le> g t" |
72379 | 680 |
using jn e xf01 t |
681 |
by (auto intro!: Groups_Big.sum_mono2 simp add: g_def zero_le_mult_iff image_subset_iff sum_nonneg) |
|
60987 | 682 |
finally show ?thesis . |
683 |
qed |
|
684 |
have "\<bar>f t - g t\<bar> < 2 * e" |
|
685 |
using fj1 fj2 gj1 gj2 by (simp add: abs_less_iff field_simps) |
|
686 |
} |
|
687 |
then show ?thesis |
|
688 |
by (rule_tac x=g in bexI) (auto intro: gR) |
|
689 |
qed |
|
690 |
||
691 |
text\<open>The ``unpretentious'' formulation\<close> |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
692 |
proposition (in function_ring_on) Stone_Weierstrass_basic: |
63938 | 693 |
assumes f: "continuous_on S f" and e: "e > 0" |
694 |
shows "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>f x - g x\<bar> < e" |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
695 |
proof - |
63938 | 696 |
have "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>(f x + normf f) - g x\<bar> < 2 * min (e/2) (1/4)" |
72379 | 697 |
proof (rule Stone_Weierstrass_special) |
698 |
show "continuous_on S (\<lambda>x. f x + normf f)" |
|
699 |
by (force intro: Limits.continuous_on_add [OF f Topological_Spaces.continuous_on_const]) |
|
700 |
show "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x + normf f" |
|
701 |
using normf_upper [OF f] by force |
|
702 |
qed (use e in auto) |
|
63938 | 703 |
then obtain g where "g \<in> R" "\<forall>x\<in>S. \<bar>g x - (f x + normf f)\<bar> < e" |
60987 | 704 |
by force |
705 |
then show ?thesis |
|
72379 | 706 |
by (rule_tac x="\<lambda>x. g x - normf f" in bexI) (auto simp: algebra_simps intro: diff const) |
60987 | 707 |
qed |
708 |
||
709 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
710 |
theorem (in function_ring_on) Stone_Weierstrass: |
63938 | 711 |
assumes f: "continuous_on S f" |
712 |
shows "\<exists>F\<in>UNIV \<rightarrow> R. LIM n sequentially. F n :> uniformly_on S f" |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
713 |
proof - |
72379 | 714 |
define h where "h \<equiv> \<lambda>n::nat. SOME g. g \<in> R \<and> (\<forall>x\<in>S. \<bar>f x - g x\<bar> < 1 / (1 + n))" |
60987 | 715 |
show ?thesis |
72379 | 716 |
proof |
717 |
{ fix e::real |
|
718 |
assume e: "0 < e" |
|
719 |
then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e" |
|
720 |
by (auto simp: real_arch_inverse [of e]) |
|
721 |
{ fix n :: nat and x :: 'a and g :: "'a \<Rightarrow> real" |
|
722 |
assume n: "N \<le> n" "\<forall>x\<in>S. \<bar>f x - g x\<bar> < 1 / (1 + real n)" |
|
723 |
assume x: "x \<in> S" |
|
724 |
have "\<not> real (Suc n) < inverse e" |
|
725 |
using \<open>N \<le> n\<close> N using less_imp_inverse_less by force |
|
726 |
then have "1 / (1 + real n) \<le> e" |
|
727 |
using e by (simp add: field_simps) |
|
728 |
then have "\<bar>f x - g x\<bar> < e" |
|
729 |
using n(2) x by auto |
|
730 |
} |
|
731 |
then have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<bar>f x - h n x\<bar> < e" |
|
732 |
unfolding h_def |
|
733 |
by (force intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]] eventually_sequentiallyI [of N]) |
|
734 |
} |
|
735 |
then show "uniform_limit S h f sequentially" |
|
736 |
unfolding uniform_limit_iff by (auto simp: dist_norm abs_minus_commute) |
|
737 |
show "h \<in> UNIV \<rightarrow> R" |
|
738 |
unfolding h_def by (force intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]]) |
|
739 |
qed |
|
60987 | 740 |
qed |
741 |
||
61222 | 742 |
text\<open>A HOL Light formulation\<close> |
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
743 |
corollary Stone_Weierstrass_HOL: |
63938 | 744 |
fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set" |
745 |
assumes "compact S" "\<And>c. P(\<lambda>x. c::real)" |
|
746 |
"\<And>f. P f \<Longrightarrow> continuous_on S f" |
|
60987 | 747 |
"\<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)" |
69508 | 748 |
"\<And>x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y \<Longrightarrow> \<exists>f. P(f) \<and> f x \<noteq> f y" |
63938 | 749 |
"continuous_on S f" |
60987 | 750 |
"0 < e" |
63938 | 751 |
shows "\<exists>g. P(g) \<and> (\<forall>x \<in> S. \<bar>f x - g x\<bar> < e)" |
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
752 |
proof - |
60987 | 753 |
interpret PR: function_ring_on "Collect P" |
72379 | 754 |
by unfold_locales (use assms in auto) |
60987 | 755 |
show ?thesis |
63938 | 756 |
using PR.Stone_Weierstrass_basic [OF \<open>continuous_on S f\<close> \<open>0 < e\<close>] |
60987 | 757 |
by blast |
758 |
qed |
|
759 |
||
760 |
||
69683 | 761 |
subsection \<open>Polynomial functions\<close> |
60987 | 762 |
|
763 |
inductive real_polynomial_function :: "('a::real_normed_vector \<Rightarrow> real) \<Rightarrow> bool" where |
|
764 |
linear: "bounded_linear f \<Longrightarrow> real_polynomial_function f" |
|
765 |
| const: "real_polynomial_function (\<lambda>x. c)" |
|
766 |
| add: "\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x + g x)" |
|
767 |
| mult: "\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x * g x)" |
|
768 |
||
769 |
declare real_polynomial_function.intros [intro] |
|
770 |
||
70136 | 771 |
definition\<^marker>\<open>tag important\<close> polynomial_function :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> bool" |
60987 | 772 |
where |
773 |
"polynomial_function p \<equiv> (\<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f o p))" |
|
774 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
775 |
lemma real_polynomial_function_eq: "real_polynomial_function p = polynomial_function p" |
60987 | 776 |
unfolding polynomial_function_def |
777 |
proof |
|
778 |
assume "real_polynomial_function p" |
|
779 |
then show " \<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f \<circ> p)" |
|
780 |
proof (induction p rule: real_polynomial_function.induct) |
|
781 |
case (linear h) then show ?case |
|
782 |
by (auto simp: bounded_linear_compose real_polynomial_function.linear) |
|
783 |
next |
|
784 |
case (const h) then show ?case |
|
785 |
by (simp add: real_polynomial_function.const) |
|
786 |
next |
|
787 |
case (add h) then show ?case |
|
788 |
by (force simp add: bounded_linear_def linear_add real_polynomial_function.add) |
|
789 |
next |
|
790 |
case (mult h) then show ?case |
|
791 |
by (force simp add: real_bounded_linear const real_polynomial_function.mult) |
|
792 |
qed |
|
793 |
next |
|
794 |
assume [rule_format, OF bounded_linear_ident]: "\<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f \<circ> p)" |
|
795 |
then show "real_polynomial_function p" |
|
796 |
by (simp add: o_def) |
|
797 |
qed |
|
798 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
799 |
lemma polynomial_function_const [iff]: "polynomial_function (\<lambda>x. c)" |
60987 | 800 |
by (simp add: polynomial_function_def o_def const) |
801 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
802 |
lemma polynomial_function_bounded_linear: |
60987 | 803 |
"bounded_linear f \<Longrightarrow> polynomial_function f" |
804 |
by (simp add: polynomial_function_def o_def bounded_linear_compose real_polynomial_function.linear) |
|
805 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
806 |
lemma polynomial_function_id [iff]: "polynomial_function(\<lambda>x. x)" |
60987 | 807 |
by (simp add: polynomial_function_bounded_linear) |
808 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
809 |
lemma polynomial_function_add [intro]: |
60987 | 810 |
"\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x + g x)" |
811 |
by (auto simp: polynomial_function_def bounded_linear_def linear_add real_polynomial_function.add o_def) |
|
812 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
813 |
lemma polynomial_function_mult [intro]: |
60987 | 814 |
assumes f: "polynomial_function f" and g: "polynomial_function g" |
72379 | 815 |
shows "polynomial_function (\<lambda>x. f x *\<^sub>R g x)" |
816 |
proof - |
|
817 |
have "real_polynomial_function (\<lambda>x. h (g x))" if "bounded_linear h" for h |
|
818 |
using g that unfolding polynomial_function_def o_def bounded_linear_def |
|
819 |
by (auto simp: real_polynomial_function_eq) |
|
820 |
moreover have "real_polynomial_function f" |
|
821 |
by (simp add: f real_polynomial_function_eq) |
|
822 |
ultimately show ?thesis |
|
823 |
unfolding polynomial_function_def bounded_linear_def o_def |
|
824 |
by (auto simp: linear.scaleR) |
|
825 |
qed |
|
60987 | 826 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
827 |
lemma polynomial_function_cmul [intro]: |
60987 | 828 |
assumes f: "polynomial_function f" |
829 |
shows "polynomial_function (\<lambda>x. c *\<^sub>R f x)" |
|
830 |
by (rule polynomial_function_mult [OF polynomial_function_const f]) |
|
831 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
832 |
lemma polynomial_function_minus [intro]: |
60987 | 833 |
assumes f: "polynomial_function f" |
834 |
shows "polynomial_function (\<lambda>x. - f x)" |
|
835 |
using polynomial_function_cmul [OF f, of "-1"] by simp |
|
836 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
837 |
lemma polynomial_function_diff [intro]: |
60987 | 838 |
"\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x - g x)" |
839 |
unfolding add_uminus_conv_diff [symmetric] |
|
840 |
by (metis polynomial_function_add polynomial_function_minus) |
|
841 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
842 |
lemma polynomial_function_sum [intro]: |
64267 | 843 |
"\<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 | 844 |
by (induct I rule: finite_induct) auto |
845 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
846 |
lemma real_polynomial_function_minus [intro]: |
60987 | 847 |
"real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. - f x)" |
848 |
using polynomial_function_minus [of f] |
|
849 |
by (simp add: real_polynomial_function_eq) |
|
850 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
851 |
lemma real_polynomial_function_diff [intro]: |
60987 | 852 |
"\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x - g x)" |
853 |
using polynomial_function_diff [of f] |
|
854 |
by (simp add: real_polynomial_function_eq) |
|
855 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
856 |
lemma real_polynomial_function_sum [intro]: |
64267 | 857 |
"\<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)" |
858 |
using polynomial_function_sum [of I f] |
|
60987 | 859 |
by (simp add: real_polynomial_function_eq) |
860 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
861 |
lemma real_polynomial_function_power [intro]: |
72379 | 862 |
"real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. f x^n)" |
60987 | 863 |
by (induct n) (simp_all add: const mult) |
864 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
865 |
lemma real_polynomial_function_compose [intro]: |
60987 | 866 |
assumes f: "polynomial_function f" and g: "real_polynomial_function g" |
867 |
shows "real_polynomial_function (g o f)" |
|
868 |
using g |
|
72379 | 869 |
proof (induction g rule: real_polynomial_function.induct) |
870 |
case (linear f) |
|
871 |
then show ?case |
|
872 |
using f polynomial_function_def by blast |
|
873 |
next |
|
874 |
case (add f g) |
|
875 |
then show ?case |
|
876 |
using f add by (auto simp: polynomial_function_def) |
|
877 |
next |
|
878 |
case (mult f g) |
|
879 |
then show ?case |
|
880 |
using f mult by (auto simp: polynomial_function_def) |
|
881 |
qed auto |
|
60987 | 882 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
883 |
lemma polynomial_function_compose [intro]: |
60987 | 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 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
889 |
lemma sum_max_0: |
60987 | 890 |
fixes x::real (*in fact "'a::comm_ring_1"*) |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
891 |
shows "(\<Sum>i\<le>max m n. x^i * (if i \<le> m then a i else 0)) = (\<Sum>i\<le>m. x^i * a i)" |
60987 | 892 |
proof - |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
893 |
have "(\<Sum>i\<le>max m n. x^i * (if i \<le> m then a i else 0)) = (\<Sum>i\<le>max m n. (if i \<le> m then x^i * a i else 0))" |
64267 | 894 |
by (auto simp: algebra_simps intro: sum.cong) |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
895 |
also have "... = (\<Sum>i\<le>m. (if i \<le> m then x^i * a i else 0))" |
64267 | 896 |
by (rule sum.mono_neutral_right) auto |
68077
ee8c13ae81e9
Some tidying up (mostly regarding summations from 0)
paulson <lp15@cam.ac.uk>
parents:
68072
diff
changeset
|
897 |
also have "... = (\<Sum>i\<le>m. x^i * a i)" |
64267 | 898 |
by (auto simp: algebra_simps intro: sum.cong) |
60987 | 899 |
finally show ?thesis . |
900 |
qed |
|
901 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
902 |
lemma real_polynomial_function_imp_sum: |
60987 | 903 |
assumes "real_polynomial_function f" |
72379 | 904 |
shows "\<exists>a n::nat. f = (\<lambda>x. \<Sum>i\<le>n. a i * x^i)" |
60987 | 905 |
using assms |
906 |
proof (induct f) |
|
907 |
case (linear f) |
|
72379 | 908 |
then obtain c where f: "f = (\<lambda>x. x * c)" |
909 |
by (auto simp add: real_bounded_linear) |
|
910 |
have "x * c = (\<Sum>i\<le>1. (if i = 0 then 0 else c) * x^i)" for x |
|
911 |
by (simp add: mult_ac) |
|
912 |
with f show ?case |
|
913 |
by fastforce |
|
60987 | 914 |
next |
915 |
case (const c) |
|
72379 | 916 |
have "c = (\<Sum>i\<le>0. c * x^i)" for x |
60987 | 917 |
by auto |
918 |
then show ?case |
|
72379 | 919 |
by fastforce |
920 |
case (add f1 f2) |
|
921 |
then obtain a1 n1 a2 n2 where |
|
922 |
"f1 = (\<lambda>x. \<Sum>i\<le>n1. a1 i * x^i)" "f2 = (\<lambda>x. \<Sum>i\<le>n2. a2 i * x^i)" |
|
923 |
by auto |
|
924 |
then have "f1 x + f2 x = (\<Sum>i\<le>max n1 n2. ((if i \<le> n1 then a1 i else 0) + (if i \<le> n2 then a2 i else 0)) * x^i)" |
|
925 |
for x |
|
64267 | 926 |
using sum_max_0 [where m=n1 and n=n2] sum_max_0 [where m=n2 and n=n1] |
72379 | 927 |
by (simp add: sum.distrib algebra_simps max.commute) |
928 |
then show ?case |
|
929 |
by force |
|
60987 | 930 |
case (mult f1 f2) |
931 |
then obtain a1 n1 a2 n2 where |
|
72379 | 932 |
"f1 = (\<lambda>x. \<Sum>i\<le>n1. a1 i * x^i)" "f2 = (\<lambda>x. \<Sum>i\<le>n2. a2 i * x^i)" |
60987 | 933 |
by auto |
934 |
then obtain b1 b2 where |
|
72379 | 935 |
"f1 = (\<lambda>x. \<Sum>i\<le>n1. b1 i * x^i)" "f2 = (\<lambda>x. \<Sum>i\<le>n2. b2 i * x^i)" |
60987 | 936 |
"b1 = (\<lambda>i. if i\<le>n1 then a1 i else 0)" "b2 = (\<lambda>i. if i\<le>n2 then a2 i else 0)" |
937 |
by auto |
|
72379 | 938 |
then have "f1 x * f2 x = (\<Sum>i\<le>n1 + n2. (\<Sum>k\<le>i. b1 k * b2 (i - k)) * x ^ i)" for x |
939 |
using polynomial_product [of n1 b1 n2 b2] by (simp add: Set_Interval.atLeast0AtMost) |
|
60987 | 940 |
then show ?case |
72379 | 941 |
by force |
60987 | 942 |
qed |
943 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
944 |
lemma real_polynomial_function_iff_sum: |
72379 | 945 |
"real_polynomial_function f \<longleftrightarrow> (\<exists>a n. f = (\<lambda>x. \<Sum>i\<le>n. a i * x^i))" (is "?lhs = ?rhs") |
946 |
proof |
|
947 |
assume ?lhs then show ?rhs |
|
948 |
by (metis real_polynomial_function_imp_sum) |
|
949 |
next |
|
950 |
assume ?rhs then show ?lhs |
|
951 |
by (auto simp: linear mult const real_polynomial_function_power real_polynomial_function_sum) |
|
952 |
qed |
|
60987 | 953 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
954 |
lemma polynomial_function_iff_Basis_inner: |
60987 | 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 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
959 |
proof (intro iffI allI impI) |
60987 | 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 |
using rp |
|
72379 | 968 |
by (force simp: real_polynomial_function_eq polynomial_function_mult |
969 |
intro!: real_polynomial_function_compose [OF _ linear [OF h]]) |
|
60987 | 970 |
then show "real_polynomial_function (h \<circ> f)" |
64267 | 971 |
by (simp add: euclidean_representation_sum_fun) |
60987 | 972 |
qed |
973 |
||
69683 | 974 |
subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close> |
60987 | 975 |
|
70381
b151d1f00204
More results about measure and integration theory
paulson <lp15@cam.ac.uk>
parents:
70138
diff
changeset
|
976 |
text\<open>First, we need to show that they are continuous, differentiable and separable.\<close> |
60987 | 977 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
978 |
lemma continuous_real_polymonial_function: |
60987 | 979 |
assumes "real_polynomial_function f" |
980 |
shows "continuous (at x) f" |
|
981 |
using assms |
|
982 |
by (induct f) (auto simp: linear_continuous_at) |
|
983 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
984 |
lemma continuous_polymonial_function: |
60987 | 985 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" |
986 |
assumes "polynomial_function f" |
|
987 |
shows "continuous (at x) f" |
|
72379 | 988 |
proof (rule euclidean_isCont) |
989 |
show "\<And>b. b \<in> Basis \<Longrightarrow> isCont (\<lambda>x. (f x \<bullet> b) *\<^sub>R b) x" |
|
990 |
using assms continuous_real_polymonial_function |
|
991 |
by (force simp: polynomial_function_iff_Basis_inner intro: isCont_scaleR) |
|
992 |
qed |
|
60987 | 993 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
994 |
lemma continuous_on_polymonial_function: |
60987 | 995 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space" |
996 |
assumes "polynomial_function f" |
|
63938 | 997 |
shows "continuous_on S f" |
60987 | 998 |
using continuous_polymonial_function [OF assms] continuous_at_imp_continuous_on |
999 |
by blast |
|
1000 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1001 |
lemma has_real_derivative_polynomial_function: |
60987 | 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 |
|
72379 | 1020 |
by (rule_tac x="\<lambda>x. p1 x + p2 x" in exI) (auto intro!: derivative_eq_intros) |
60987 | 1021 |
case (mult f1 f2) |
1022 |
then obtain p1 p2 where |
|
1023 |
"real_polynomial_function p1" "\<And>x. (f1 has_real_derivative p1 x) (at x)" |
|
1024 |
"real_polynomial_function p2" "\<And>x. (f2 has_real_derivative p2 x) (at x)" |
|
1025 |
by auto |
|
1026 |
then show ?case |
|
1027 |
using mult |
|
72379 | 1028 |
by (rule_tac x="\<lambda>x. f1 x * p2 x + f2 x * p1 x" in exI) (auto intro!: derivative_eq_intros) |
60987 | 1029 |
qed |
1030 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1031 |
lemma has_vector_derivative_polynomial_function: |
60987 | 1032 |
fixes p :: "real \<Rightarrow> 'a::euclidean_space" |
1033 |
assumes "polynomial_function p" |
|
63938 | 1034 |
obtains p' where "polynomial_function p'" "\<And>x. (p has_vector_derivative (p' x)) (at x)" |
60987 | 1035 |
proof - |
1036 |
{ fix b :: 'a |
|
1037 |
assume "b \<in> Basis" |
|
1038 |
then |
|
1039 |
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)" |
|
72379 | 1040 |
using assms [unfolded polynomial_function_iff_Basis_inner] has_real_derivative_polynomial_function |
60987 | 1041 |
by blast |
72379 | 1042 |
have "polynomial_function (\<lambda>x. p' x *\<^sub>R b)" |
1043 |
using \<open>b \<in> Basis\<close> p' const [where 'a=real and c=0] |
|
1044 |
by (simp add: polynomial_function_iff_Basis_inner inner_Basis) |
|
1045 |
then 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))" |
|
1046 |
by (fastforce intro: derivative_eq_intros pd) |
|
60987 | 1047 |
} |
1048 |
then obtain qf where qf: |
|
1049 |
"\<And>b. b \<in> Basis \<Longrightarrow> polynomial_function (qf b)" |
|
1050 |
"\<And>b x. b \<in> Basis \<Longrightarrow> ((\<lambda>u. (p u \<bullet> b) *\<^sub>R b) has_vector_derivative qf b x) (at x)" |
|
1051 |
by metis |
|
1052 |
show ?thesis |
|
72379 | 1053 |
proof |
1054 |
show "\<And>x. (p has_vector_derivative (\<Sum>b\<in>Basis. qf b x)) (at x)" |
|
1055 |
apply (subst euclidean_representation_sum_fun [of p, symmetric]) |
|
1056 |
by (auto intro: has_vector_derivative_sum qf) |
|
1057 |
qed (force intro: qf) |
|
60987 | 1058 |
qed |
1059 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1060 |
lemma real_polynomial_function_separable: |
60987 | 1061 |
fixes x :: "'a::euclidean_space" |
1062 |
assumes "x \<noteq> y" shows "\<exists>f. real_polynomial_function f \<and> f x \<noteq> f y" |
|
1063 |
proof - |
|
1064 |
have "real_polynomial_function (\<lambda>u. \<Sum>b\<in>Basis. (inner (x-u) b)^2)" |
|
72379 | 1065 |
proof (rule real_polynomial_function_sum) |
1066 |
show "\<And>i. i \<in> Basis \<Longrightarrow> real_polynomial_function (\<lambda>u. ((x - u) \<bullet> i)\<^sup>2)" |
|
1067 |
by (auto simp: algebra_simps real_polynomial_function_diff const linear bounded_linear_inner_left) |
|
1068 |
qed auto |
|
1069 |
moreover have "(\<Sum>b\<in>Basis. ((x - y) \<bullet> b)\<^sup>2) \<noteq> 0" |
|
1070 |
using assms by (force simp add: euclidean_eq_iff [of x y] sum_nonneg_eq_0_iff algebra_simps) |
|
1071 |
ultimately show ?thesis |
|
1072 |
by auto |
|
60987 | 1073 |
qed |
1074 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1075 |
lemma Stone_Weierstrass_real_polynomial_function: |
60987 | 1076 |
fixes f :: "'a::euclidean_space \<Rightarrow> real" |
63938 | 1077 |
assumes "compact S" "continuous_on S f" "0 < e" |
1078 |
obtains g where "real_polynomial_function g" "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x - g x\<bar> < e" |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1079 |
proof - |
60987 | 1080 |
interpret PR: function_ring_on "Collect real_polynomial_function" |
72379 | 1081 |
proof unfold_locales |
1082 |
qed (use assms continuous_on_polymonial_function real_polynomial_function_eq |
|
1083 |
in \<open>auto intro: real_polynomial_function_separable\<close>) |
|
60987 | 1084 |
show ?thesis |
72379 | 1085 |
using PR.Stone_Weierstrass_basic [OF \<open>continuous_on S f\<close> \<open>0 < e\<close>] that by blast |
60987 | 1086 |
qed |
1087 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1088 |
theorem Stone_Weierstrass_polynomial_function: |
60987 | 1089 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
63938 | 1090 |
assumes S: "compact S" |
1091 |
and f: "continuous_on S f" |
|
60987 | 1092 |
and e: "0 < e" |
63938 | 1093 |
shows "\<exists>g. polynomial_function g \<and> (\<forall>x \<in> S. norm(f x - g x) < e)" |
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1094 |
proof - |
60987 | 1095 |
{ fix b :: 'b |
1096 |
assume "b \<in> Basis" |
|
63938 | 1097 |
have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> S. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))" |
72379 | 1098 |
proof (rule Stone_Weierstrass_real_polynomial_function [OF S _, of "\<lambda>x. f x \<bullet> b" "e / card Basis"]) |
1099 |
show "continuous_on S (\<lambda>x. f x \<bullet> b)" |
|
1100 |
using f by (auto intro: continuous_intros) |
|
1101 |
qed (use e in auto) |
|
60987 | 1102 |
} |
1103 |
then obtain pf where pf: |
|
63938 | 1104 |
"\<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))" |
72379 | 1105 |
by metis |
1106 |
let ?g = "\<lambda>x. \<Sum>b\<in>Basis. pf b x *\<^sub>R b" |
|
60987 | 1107 |
{ fix x |
63938 | 1108 |
assume "x \<in> S" |
60987 | 1109 |
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 | 1110 |
by (rule norm_sum) |
60987 | 1111 |
also have "... < of_nat DIM('b) * (e / DIM('b))" |
72379 | 1112 |
proof (rule sum_bounded_above_strict) |
1113 |
show "\<And>i. i \<in> Basis \<Longrightarrow> norm ((f x \<bullet> i) *\<^sub>R i - pf i x *\<^sub>R i) < e / real DIM('b)" |
|
1114 |
by (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf \<open>x \<in> S\<close>) |
|
1115 |
qed (rule DIM_positive) |
|
60987 | 1116 |
also have "... = e" |
71172 | 1117 |
by (simp add: field_simps) |
60987 | 1118 |
finally have "norm (\<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b - pf b x *\<^sub>R b) < e" . |
1119 |
} |
|
72379 | 1120 |
then have "\<forall>x\<in>S. norm ((\<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) - ?g x) < e" |
1121 |
by (auto simp flip: sum_subtractf) |
|
1122 |
moreover |
|
1123 |
have "polynomial_function ?g" |
|
1124 |
using pf by (simp add: polynomial_function_sum polynomial_function_mult real_polynomial_function_eq) |
|
1125 |
ultimately show ?thesis |
|
1126 |
using euclidean_representation_sum_fun [of f] by (metis (no_types, lifting)) |
|
60987 | 1127 |
qed |
1128 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1129 |
proposition Stone_Weierstrass_uniform_limit: |
65204
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1130 |
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
|
1131 |
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
|
1132 |
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
|
1133 |
obtains g where "uniform_limit S g f sequentially" "\<And>n. polynomial_function (g n)" |
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1134 |
proof - |
65204
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1135 |
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
|
1136 |
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
|
1137 |
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
|
1138 |
by metis |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1139 |
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
|
1140 |
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
|
1141 |
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
|
1142 |
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
|
1143 |
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
|
1144 |
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
|
1145 |
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
|
1146 |
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
|
1147 |
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
|
1148 |
qed |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1149 |
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
|
1150 |
qed |
d23eded35a33
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
immler
parents:
64272
diff
changeset
|
1151 |
|
60987 | 1152 |
|
69683 | 1153 |
subsection\<open>Polynomial functions as paths\<close> |
60987 | 1154 |
|
61222 | 1155 |
text\<open>One application is to pick a smooth approximation to a path, |
1156 |
or just pick a smooth path anyway in an open connected set\<close> |
|
60987 | 1157 |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1158 |
lemma path_polynomial_function: |
60987 | 1159 |
fixes g :: "real \<Rightarrow> 'b::euclidean_space" |
1160 |
shows "polynomial_function g \<Longrightarrow> path g" |
|
1161 |
by (simp add: path_def continuous_on_polymonial_function) |
|
1162 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1163 |
lemma path_approx_polynomial_function: |
60987 | 1164 |
fixes g :: "real \<Rightarrow> 'b::euclidean_space" |
1165 |
assumes "path g" "0 < e" |
|
72379 | 1166 |
obtains p where "polynomial_function p" "pathstart p = pathstart g" "pathfinish p = pathfinish g" |
1167 |
"\<And>t. t \<in> {0..1} \<Longrightarrow> norm(p t - g t) < e" |
|
60987 | 1168 |
proof - |
1169 |
obtain q where poq: "polynomial_function q" and noq: "\<And>x. x \<in> {0..1} \<Longrightarrow> norm (g x - q x) < e/4" |
|
1170 |
using Stone_Weierstrass_polynomial_function [of "{0..1}" g "e/4"] assms |
|
1171 |
by (auto simp: path_def) |
|
72379 | 1172 |
define pf where "pf \<equiv> \<lambda>t. q t + (g 0 - q 0) + t *\<^sub>R (g 1 - q 1 - (g 0 - q 0))" |
1173 |
show thesis |
|
1174 |
proof |
|
1175 |
show "polynomial_function pf" |
|
1176 |
by (force simp add: poq pf_def) |
|
1177 |
show "norm (pf t - g t) < e" |
|
1178 |
if "t \<in> {0..1}" for t |
|
1179 |
proof - |
|
1180 |
have *: "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)" |
|
1181 |
proof (intro Real_Vector_Spaces.norm_add_less) |
|
1182 |
show "norm (q t - g t) < e / 4" |
|
1183 |
by (metis noq norm_minus_commute that) |
|
1184 |
show "norm (t *\<^sub>R (g 1 - q 1)) < e / 4" |
|
1185 |
using noq that le_less_trans [OF mult_left_le_one_le noq] |
|
1186 |
by auto |
|
1187 |
show "norm (t *\<^sub>R (q 0 - g 0)) < e / 4" |
|
1188 |
using noq that le_less_trans [OF mult_left_le_one_le noq] |
|
1189 |
by simp (metis norm_minus_commute order_refl zero_le_one) |
|
1190 |
qed (use noq norm_minus_commute that in auto) |
|
1191 |
then show ?thesis |
|
1192 |
by (auto simp add: algebra_simps pf_def) |
|
1193 |
qed |
|
1194 |
qed (auto simp add: path_defs pf_def) |
|
60987 | 1195 |
qed |
1196 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1197 |
proposition connected_open_polynomial_connected: |
63938 | 1198 |
fixes S :: "'a::euclidean_space set" |
1199 |
assumes S: "open S" "connected S" |
|
1200 |
and "x \<in> S" "y \<in> S" |
|
72380
becf08cb81e1
reversion to the explicit existential quantifier
paulson <lp15@cam.ac.uk>
parents:
72379
diff
changeset
|
1201 |
shows "\<exists>g. polynomial_function g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y" |
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1202 |
proof - |
63938 | 1203 |
have "path_connected S" using assms |
60987 | 1204 |
by (simp add: connected_open_path_connected) |
63938 | 1205 |
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 | 1206 |
by (force simp: path_connected_def) |
63938 | 1207 |
have "\<exists>e. 0 < e \<and> (\<forall>x \<in> path_image p. ball x e \<subseteq> S)" |
1208 |
proof (cases "S = UNIV") |
|
60987 | 1209 |
case True then show ?thesis |
1210 |
by (simp add: gt_ex) |
|
1211 |
next |
|
1212 |
case False |
|
72379 | 1213 |
show ?thesis |
1214 |
proof (intro exI conjI ballI) |
|
1215 |
show "\<And>x. x \<in> path_image p \<Longrightarrow> ball x (setdist (path_image p) (-S)) \<subseteq> S" |
|
1216 |
using setdist_le_dist [of _ "path_image p" _ "-S"] by fastforce |
|
1217 |
show "0 < setdist (path_image p) (- S)" |
|
1218 |
using S p False |
|
1219 |
by (fastforce simp add: setdist_gt_0_compact_closed compact_path_image open_closed) |
|
1220 |
qed |
|
60987 | 1221 |
qed |
63938 | 1222 |
then obtain e where "0 < e"and eb: "\<And>x. x \<in> path_image p \<Longrightarrow> ball x e \<subseteq> S" |
60987 | 1223 |
by auto |
72379 | 1224 |
obtain pf where "polynomial_function pf" and pf: "pathstart pf = pathstart p" "pathfinish pf = pathfinish p" |
1225 |
and pf_e: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm(pf t - p t) < e" |
|
1226 |
using path_approx_polynomial_function [OF \<open>path p\<close> \<open>0 < e\<close>] by blast |
|
72380
becf08cb81e1
reversion to the explicit existential quantifier
paulson <lp15@cam.ac.uk>
parents:
72379
diff
changeset
|
1227 |
show ?thesis |
becf08cb81e1
reversion to the explicit existential quantifier
paulson <lp15@cam.ac.uk>
parents:
72379
diff
changeset
|
1228 |
proof (intro exI conjI) |
72379 | 1229 |
show "polynomial_function pf" |
1230 |
by fact |
|
1231 |
show "pathstart pf = x" "pathfinish pf = y" |
|
1232 |
by (simp_all add: p pf) |
|
1233 |
show "path_image pf \<subseteq> S" |
|
1234 |
unfolding path_image_def |
|
1235 |
proof clarsimp |
|
1236 |
fix x'::real |
|
1237 |
assume "0 \<le> x'" "x' \<le> 1" |
|
1238 |
then have "dist (p x') (pf x') < e" |
|
1239 |
by (metis atLeastAtMost_iff dist_commute dist_norm pf_e) |
|
1240 |
then show "pf x' \<in> S" |
|
1241 |
by (metis \<open>0 \<le> x'\<close> \<open>x' \<le> 1\<close> atLeastAtMost_iff eb imageI mem_ball path_image_def subset_iff) |
|
1242 |
qed |
|
1243 |
qed |
|
60987 | 1244 |
qed |
1245 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1246 |
lemma differentiable_componentwise_within: |
63938 | 1247 |
"f differentiable (at a within S) \<longleftrightarrow> |
1248 |
(\<forall>i \<in> Basis. (\<lambda>x. f x \<bullet> i) differentiable at a within S)" |
|
1249 |
proof - |
|
1250 |
{ assume "\<forall>i\<in>Basis. \<exists>D. ((\<lambda>x. f x \<bullet> i) has_derivative D) (at a within S)" |
|
1251 |
then obtain f' where f': |
|
1252 |
"\<And>i. i \<in> Basis \<Longrightarrow> ((\<lambda>x. f x \<bullet> i) has_derivative f' i) (at a within S)" |
|
1253 |
by metis |
|
1254 |
have eq: "(\<lambda>x. (\<Sum>j\<in>Basis. f' j x *\<^sub>R j) \<bullet> i) = f' i" if "i \<in> Basis" for i |
|
1255 |
using that by (simp add: inner_add_left inner_add_right) |
|
1256 |
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)" |
|
1257 |
apply (rule_tac x="\<lambda>x::'a. (\<Sum>j\<in>Basis. f' j x *\<^sub>R j) :: 'b" in exI) |
|
1258 |
apply (simp add: eq f') |
|
1259 |
done |
|
1260 |
} |
|
1261 |
then show ?thesis |
|
1262 |
apply (simp add: differentiable_def) |
|
1263 |
using has_derivative_componentwise_within |
|
1264 |
by blast |
|
1265 |
qed |
|
1266 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1267 |
lemma polynomial_function_inner [intro]: |
63938 | 1268 |
fixes i :: "'a::euclidean_space" |
1269 |
shows "polynomial_function g \<Longrightarrow> polynomial_function (\<lambda>x. g x \<bullet> i)" |
|
1270 |
apply (subst euclidean_representation [where x=i, symmetric]) |
|
64267 | 1271 |
apply (force simp: inner_sum_right polynomial_function_iff_Basis_inner polynomial_function_sum) |
63938 | 1272 |
done |
1273 |
||
1274 |
text\<open> Differentiability of real and vector polynomial functions.\<close> |
|
1275 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1276 |
lemma differentiable_at_real_polynomial_function: |
63938 | 1277 |
"real_polynomial_function f \<Longrightarrow> f differentiable (at a within S)" |
1278 |
by (induction f rule: real_polynomial_function.induct) |
|
1279 |
(simp_all add: bounded_linear_imp_differentiable) |
|
1280 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1281 |
lemma differentiable_on_real_polynomial_function: |
63938 | 1282 |
"real_polynomial_function p \<Longrightarrow> p differentiable_on S" |
1283 |
by (simp add: differentiable_at_imp_differentiable_on differentiable_at_real_polynomial_function) |
|
1284 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1285 |
lemma differentiable_at_polynomial_function: |
63938 | 1286 |
fixes f :: "_ \<Rightarrow> 'a::euclidean_space" |
1287 |
shows "polynomial_function f \<Longrightarrow> f differentiable (at a within S)" |
|
1288 |
by (metis differentiable_at_real_polynomial_function polynomial_function_iff_Basis_inner differentiable_componentwise_within) |
|
1289 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1290 |
lemma differentiable_on_polynomial_function: |
63938 | 1291 |
fixes f :: "_ \<Rightarrow> 'a::euclidean_space" |
1292 |
shows "polynomial_function f \<Longrightarrow> f differentiable_on S" |
|
1293 |
by (simp add: differentiable_at_polynomial_function differentiable_on_def) |
|
1294 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1295 |
lemma vector_eq_dot_span: |
63938 | 1296 |
assumes "x \<in> span B" "y \<in> span B" and i: "\<And>i. i \<in> B \<Longrightarrow> i \<bullet> x = i \<bullet> y" |
1297 |
shows "x = y" |
|
1298 |
proof - |
|
1299 |
have "\<And>i. i \<in> B \<Longrightarrow> orthogonal (x - y) i" |
|
1300 |
by (simp add: i inner_commute inner_diff_right orthogonal_def) |
|
1301 |
moreover have "x - y \<in> span B" |
|
1302 |
by (simp add: assms span_diff) |
|
1303 |
ultimately have "x - y = 0" |
|
1304 |
using orthogonal_to_span orthogonal_self by blast |
|
1305 |
then show ?thesis by simp |
|
1306 |
qed |
|
1307 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1308 |
lemma orthonormal_basis_expand: |
63938 | 1309 |
assumes B: "pairwise orthogonal B" |
1310 |
and 1: "\<And>i. i \<in> B \<Longrightarrow> norm i = 1" |
|
1311 |
and "x \<in> span B" |
|
1312 |
and "finite B" |
|
1313 |
shows "(\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) = x" |
|
1314 |
proof (rule vector_eq_dot_span [OF _ \<open>x \<in> span B\<close>]) |
|
1315 |
show "(\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) \<in> span B" |
|
64267 | 1316 |
by (simp add: span_clauses span_sum) |
63938 | 1317 |
show "i \<bullet> (\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) = i \<bullet> x" if "i \<in> B" for i |
1318 |
proof - |
|
1319 |
have [simp]: "i \<bullet> j = (if j = i then 1 else 0)" if "j \<in> B" for j |
|
1320 |
using B 1 that \<open>i \<in> B\<close> |
|
1321 |
by (force simp: norm_eq_1 orthogonal_def pairwise_def) |
|
1322 |
have "i \<bullet> (\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) = (\<Sum>j\<in>B. x \<bullet> j * (i \<bullet> j))" |
|
64267 | 1323 |
by (simp add: inner_sum_right) |
63938 | 1324 |
also have "... = (\<Sum>j\<in>B. if j = i then x \<bullet> i else 0)" |
64267 | 1325 |
by (rule sum.cong; simp) |
63938 | 1326 |
also have "... = i \<bullet> x" |
71633 | 1327 |
by (simp add: \<open>finite B\<close> that inner_commute) |
63938 | 1328 |
finally show ?thesis . |
1329 |
qed |
|
1330 |
qed |
|
1331 |
||
1332 |
||
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1333 |
theorem Stone_Weierstrass_polynomial_function_subspace: |
63938 | 1334 |
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" |
1335 |
assumes "compact S" |
|
1336 |
and contf: "continuous_on S f" |
|
1337 |
and "0 < e" |
|
1338 |
and "subspace T" "f ` S \<subseteq> T" |
|
1339 |
obtains g where "polynomial_function g" "g ` S \<subseteq> T" |
|
1340 |
"\<And>x. x \<in> S \<Longrightarrow> norm(f x - g x) < e" |
|
69737
ec3cc98c38db
tagged 4 theories
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1341 |
proof - |
63938 | 1342 |
obtain B where "B \<subseteq> T" and orthB: "pairwise orthogonal B" |
1343 |
and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1" |
|
1344 |
and "independent B" and cardB: "card B = dim T" |
|
1345 |
and spanB: "span B = T" |
|
1346 |
using orthonormal_basis_subspace \<open>subspace T\<close> by metis |
|
1347 |
then have "finite B" |
|
1348 |
by (simp add: independent_imp_finite) |
|
1349 |
then obtain n::nat and b where "B = b ` {i. i < n}" "inj_on b {i. i < n}" |
|
1350 |
using finite_imp_nat_seg_image_inj_on by metis |
|
1351 |
with cardB have "n = card B" "dim T = n" |
|
1352 |
by (auto simp: card_image) |
|
1353 |
have fx: "(\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i) = f x" if "x \<in> S" for x |
|
72379 | 1354 |
by (metis (no_types, lifting) B1 \<open>finite B\<close> assms(5) image_subset_iff orthB orthonormal_basis_expand spanB sum.cong that) |
63938 | 1355 |
have cont: "continuous_on S (\<lambda>x. \<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i)" |
1356 |
by (intro continuous_intros contf) |
|
1357 |
obtain g where "polynomial_function g" |
|
1358 |
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)" |
|
1359 |
using Stone_Weierstrass_polynomial_function [OF \<open>compact S\<close> cont, of "e / real (n + 2)"] \<open>0 < e\<close> |
|
1360 |
by auto |
|
1361 |
with fx have g: "\<And>x. x \<in> S \<Longrightarrow> norm (f x - g x) < e / (n+2)" |
|
1362 |
by auto |
|
1363 |
show ?thesis |
|
1364 |
proof |
|
1365 |
show "polynomial_function (\<lambda>x. \<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i)" |
|
72379 | 1366 |
using \<open>polynomial_function g\<close> by (force intro: \<open>finite B\<close>) |
63938 | 1367 |
show "(\<lambda>x. \<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i) ` S \<subseteq> T" |
67986
b65c4a6a015e
quite a few more results about negligibility, etc., and a bit of tidying up
paulson <lp15@cam.ac.uk>
parents:
65585
diff
changeset
|
1368 |
using \<open>B \<subseteq> T\<close> |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67986
diff
changeset
|
1369 |
by (blast intro: subspace_sum subspace_mul \<open>subspace T\<close>) |
63938 | 1370 |
show "norm (f x - (\<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i)) < e" if "x \<in> S" for x |
1371 |
proof - |
|
1372 |
have orth': "pairwise (\<lambda>i j. orthogonal ((f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i) |
|
1373 |
((f x \<bullet> j) *\<^sub>R j - (g x \<bullet> j) *\<^sub>R j)) B" |
|
72379 | 1374 |
by (auto simp: orthogonal_def inner_diff_right inner_diff_left intro: pairwise_mono [OF orthB]) |
63938 | 1375 |
then have "(norm (\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i))\<^sup>2 = |
1376 |
(\<Sum>i\<in>B. (norm ((f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i))\<^sup>2)" |
|
64267 | 1377 |
by (simp add: norm_sum_Pythagorean [OF \<open>finite B\<close> orth']) |
63938 | 1378 |
also have "... = (\<Sum>i\<in>B. (norm (((f x - g x) \<bullet> i) *\<^sub>R i))\<^sup>2)" |
1379 |
by (simp add: algebra_simps) |
|
1380 |
also have "... \<le> (\<Sum>i\<in>B. (norm (f x - g x))\<^sup>2)" |
|
72221 | 1381 |
proof - |
1382 |
have "\<And>i. i \<in> B \<Longrightarrow> ((f x - g x) \<bullet> i)\<^sup>2 \<le> (norm (f x - g x))\<^sup>2" |
|
1383 |
by (metis B1 Cauchy_Schwarz_ineq inner_commute mult.left_neutral norm_eq_1 power2_norm_eq_inner) |
|
1384 |
then show ?thesis |
|
1385 |
by (intro sum_mono) (simp add: sum_mono B1) |
|
1386 |
qed |
|
63938 | 1387 |
also have "... = n * norm (f x - g x)^2" |
1388 |
by (simp add: \<open>n = card B\<close>) |
|
1389 |
also have "... \<le> n * (e / (n+2))^2" |
|
72221 | 1390 |
proof (rule mult_left_mono) |
1391 |
show "(norm (f x - g x))\<^sup>2 \<le> (e / real (n + 2))\<^sup>2" |
|
1392 |
by (meson dual_order.order_iff_strict g norm_ge_zero power_mono that) |
|
1393 |
qed auto |
|
63938 | 1394 |
also have "... \<le> e^2 / (n+2)" |
1395 |
using \<open>0 < e\<close> by (simp add: divide_simps power2_eq_square) |
|
1396 |
also have "... < e^2" |
|
1397 |
using \<open>0 < e\<close> by (simp add: divide_simps) |
|
1398 |
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" . |
|
1399 |
then have "(norm (\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i)) < e" |
|
72221 | 1400 |
by (simp add: \<open>0 < e\<close> norm_lt_square power2_norm_eq_inner) |
63938 | 1401 |
then show ?thesis |
64267 | 1402 |
using fx that by (simp add: sum_subtractf) |
63938 | 1403 |
qed |
1404 |
qed |
|
1405 |
qed |
|
1406 |
||
1407 |
||
60987 | 1408 |
hide_fact linear add mult const |
1409 |
||
1410 |
end |