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