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