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