section ‹Bernstein-Weierstrass and Stone-Weierstrass› text‹By L C Paulson (2015)› theory Weierstrass_Theorems imports Uniform_Limit Path_Connected Derivative begin subsection ‹Bernstein polynomials› definition✐‹tag important› Bernstein :: "[nat,nat,real] ⇒ real" where "Bernstein n k x ≡ of_nat (n choose k) * x^k * (1 - x)^(n - k)" lemma Bernstein_nonneg: "⟦0 ≤ x; x ≤ 1⟧ ⟹ 0 ≤ Bernstein n k x" by (simp add: Bernstein_def) lemma Bernstein_pos: "⟦0 < x; x < 1; k ≤ n⟧ ⟹ 0 < Bernstein n k x" by (simp add: Bernstein_def) lemma sum_Bernstein [simp]: "(∑k≤n. Bernstein n k x) = 1" using binomial_ring [of x "1-x" n] by (simp add: Bernstein_def) lemma binomial_deriv1: "(∑k≤n. (of_nat k * of_nat (n choose k)) * a^(k-1) * b^(n-k)) = real_of_nat n * (a+b)^(n-1)" apply (rule DERIV_unique [where f = "λa. (a+b)^n" and x=a]) apply (subst binomial_ring) apply (rule derivative_eq_intros sum.cong | simp add: atMost_atLeast0)+ done lemma binomial_deriv2: "(∑k≤n. (of_nat k * of_nat (k-1) * of_nat (n choose k)) * a^(k-2) * b^(n-k)) = of_nat n * of_nat (n-1) * (a+b::real)^(n-2)" apply (rule DERIV_unique [where f = "λa. of_nat n * (a+b::real)^(n-1)" and x=a]) apply (subst binomial_deriv1 [symmetric]) apply (rule derivative_eq_intros sum.cong | simp add: Num.numeral_2_eq_2)+ done lemma sum_k_Bernstein [simp]: "(∑k≤n. real k * Bernstein n k x) = of_nat n * x" apply (subst binomial_deriv1 [of n x "1-x", simplified, symmetric]) apply (simp add: sum_distrib_right) apply (auto simp: Bernstein_def algebra_simps power_eq_if intro!: sum.cong) done lemma sum_kk_Bernstein [simp]: "(∑k≤n. real k * (real k - 1) * Bernstein n k x) = real n * (real n - 1) * x⇧^{2}" proof - have "(∑k≤n. real k * (real k - 1) * Bernstein n k x) = (∑k≤n. real k * real (k - Suc 0) * real (n choose k) * x^(k - 2) * (1 - x)^(n - k) * x⇧^{2})" proof (rule sum.cong [OF refl], simp) fix k assume "k ≤ n" then consider "k = 0" | "k = 1" | k' where "k = Suc (Suc k')" by (metis One_nat_def not0_implies_Suc) then show "k = 0 ∨ (real k - 1) * Bernstein n k x = real (k - Suc 0) * (real (n choose k) * (x^(k - 2) * ((1 - x)^(n - k) * x⇧^{2})))" by cases (auto simp add: Bernstein_def power2_eq_square algebra_simps) qed also have "... = real_of_nat n * real_of_nat (n - Suc 0) * x⇧^{2}" by (subst binomial_deriv2 [of n x "1-x", simplified, symmetric]) (simp add: sum_distrib_right) also have "... = n * (n - 1) * x⇧^{2}" by auto finally show ?thesis by auto qed subsection ‹Explicit Bernstein version of the 1D Weierstrass approximation theorem› theorem Bernstein_Weierstrass: fixes f :: "real ⇒ real" assumes contf: "continuous_on {0..1} f" and e: "0 < e" shows "∃N. ∀n x. N ≤ n ∧ x ∈ {0..1} ⟶ ¦f x - (∑k≤n. f(k/n) * Bernstein n k x)¦ < e" proof - have "bounded (f ` {0..1})" using compact_continuous_image compact_imp_bounded contf by blast then obtain M where M: "⋀x. 0 ≤ x ⟹ x ≤ 1 ⟹ ¦f x¦ ≤ M" by (force simp add: bounded_iff) then have "0 ≤ M" by force have ucontf: "uniformly_continuous_on {0..1} f" using compact_uniformly_continuous contf by blast then obtain d where d: "d>0" "⋀x x'. ⟦ x ∈ {0..1}; x' ∈ {0..1}; ¦x' - x¦ < d⟧ ⟹ ¦f x' - f x¦ < e/2" apply (rule uniformly_continuous_onE [where e = "e/2"]) using e by (auto simp: dist_norm) { fix n::nat and x::real assume n: "Suc (nat⌈4*M/(e*d⇧^{2})⌉) ≤ n" and x: "0 ≤ x" "x ≤ 1" have "0 < n" using n by simp have ed0: "- (e * d⇧^{2}) < 0" using e ‹0<d› by simp also have "... ≤ M * 4" using ‹0≤M› by simp finally have [simp]: "real_of_int (nat ⌈4 * M / (e * d⇧^{2})⌉) = real_of_int ⌈4 * M / (e * d⇧^{2})⌉" using ‹0≤M› e ‹0<d› by (simp add: field_simps) have "4*M/(e*d⇧^{2}) + 1 ≤ real (Suc (nat⌈4*M/(e*d⇧^{2})⌉))" by (simp add: real_nat_ceiling_ge) also have "... ≤ real n" using n by (simp add: field_simps) finally have nbig: "4*M/(e*d⇧^{2}) + 1 ≤ real n" . have sum_bern: "(∑k≤n. (x - k/n)⇧^{2}* Bernstein n k x) = x * (1 - x) / n" proof - have *: "⋀a b x::real. (a - b)⇧^{2}* x = a * (a - 1) * x + (1 - 2 * b) * a * x + b * b * x" by (simp add: algebra_simps power2_eq_square) have "(∑k≤n. (k - n * x)⇧^{2}* Bernstein n k x) = n * x * (1 - x)" apply (simp add: * sum.distrib) apply (simp flip: sum_distrib_left add: mult.assoc) apply (simp add: algebra_simps power2_eq_square) done then have "(∑k≤n. (k - n * x)⇧^{2}* Bernstein n k x)/n^2 = x * (1 - x) / n" by (simp add: power2_eq_square) then show ?thesis using n by (simp add: sum_divide_distrib field_split_simps power2_commute) qed { fix k assume k: "k ≤ n" then have kn: "0 ≤ k / n" "k / n ≤ 1" by (auto simp: field_split_simps) consider (lessd) "¦x - k / n¦ < d" | (ged) "d ≤ ¦x - k / n¦" by linarith then have "¦(f x - f (k/n))¦ ≤ e/2 + 2 * M / d⇧^{2}* (x - k/n)⇧^{2}" proof cases case lessd then have "¦(f x - f (k/n))¦ < e/2" using d x kn by (simp add: abs_minus_commute) also have "... ≤ (e/2 + 2 * M / d⇧^{2}* (x - k/n)⇧^{2})" using ‹M≥0› d by simp finally show ?thesis by simp next case ged then have dle: "d⇧^{2}≤ (x - k/n)⇧^{2}" by (metis d(1) less_eq_real_def power2_abs power_mono) have §: "1 ≤ (x - real k / real n)⇧^{2}/ d⇧^{2}" using dle ‹d>0› by auto have "¦(f x - f (k/n))¦ ≤ ¦f x¦ + ¦f (k/n)¦" by (rule abs_triangle_ineq4) also have "... ≤ M+M" by (meson M add_mono_thms_linordered_semiring(1) kn x) also have "... ≤ 2 * M * ((x - k/n)⇧^{2}/ d⇧^{2})" using § ‹M≥0› mult_left_mono by fastforce also have "... ≤ e/2 + 2 * M / d⇧^{2}* (x - k/n)⇧^{2}" using e by simp finally show ?thesis . qed } note * = this have "¦f x - (∑k≤n. f(k / n) * Bernstein n k x)¦ ≤ ¦∑k≤n. (f x - f(k / n)) * Bernstein n k x¦" by (simp add: sum_subtractf sum_distrib_left [symmetric] algebra_simps) also have "... ≤ (∑k≤n. ¦(f x - f(k / n)) * Bernstein n k x¦)" by (rule sum_abs) also have "... ≤ (∑k≤n. (e/2 + (2 * M / d⇧^{2}) * (x - k / n)⇧^{2}) * Bernstein n k x)" using * by (force simp add: abs_mult Bernstein_nonneg x mult_right_mono intro: sum_mono) also have "... ≤ e/2 + (2 * M) / (d⇧^{2}* n)" unfolding sum.distrib Rings.semiring_class.distrib_right sum_distrib_left [symmetric] mult.assoc sum_bern using ‹d>0› x by (simp add: divide_simps ‹M≥0› mult_le_one mult_left_le) also have "... < e" using ‹d>0› nbig e ‹n>0› apply (simp add: field_split_simps) using ed0 by linarith finally have "¦f x - (∑k≤n. f (real k / real n) * Bernstein n k x)¦ < e" . } then show ?thesis by auto qed subsection ‹General Stone-Weierstrass theorem› text‹Source: Bruno Brosowski and Frank Deutsch. An Elementary Proof of the Stone-Weierstrass Theorem. Proceedings of the American Mathematical Society Volume 81, Number 1, January 1981. DOI: 10.2307/2043993 🌐‹https://www.jstor.org/stable/2043993›› locale function_ring_on = fixes R :: "('a::t2_space ⇒ real) set" and S :: "'a set" assumes compact: "compact S" assumes continuous: "f ∈ R ⟹ continuous_on S f" assumes add: "f ∈ R ⟹ g ∈ R ⟹ (λx. f x + g x) ∈ R" assumes mult: "f ∈ R ⟹ g ∈ R ⟹ (λx. f x * g x) ∈ R" assumes const: "(λ_. c) ∈ R" assumes separable: "x ∈ S ⟹ y ∈ S ⟹ x ≠ y ⟹ ∃f∈R. f x ≠ f y" begin lemma minus: "f ∈ R ⟹ (λx. - f x) ∈ R" by (frule mult [OF const [of "-1"]]) simp lemma diff: "f ∈ R ⟹ g ∈ R ⟹ (λx. f x - g x) ∈ R" unfolding diff_conv_add_uminus by (metis add minus) lemma power: "f ∈ R ⟹ (λx. f x^n) ∈ R" by (induct n) (auto simp: const mult) lemma sum: "⟦finite I; ⋀i. i ∈ I ⟹ f i ∈ R⟧ ⟹ (λx. ∑i ∈ I. f i x) ∈ R" by (induct I rule: finite_induct; simp add: const add) lemma prod: "⟦finite I; ⋀i. i ∈ I ⟹ f i ∈ R⟧ ⟹ (λx. ∏i ∈ I. f i x) ∈ R" by (induct I rule: finite_induct; simp add: const mult) definition✐‹tag important› normf :: "('a::t2_space ⇒ real) ⇒ real" where "normf f ≡ SUP x∈S. ¦f x¦" lemma normf_upper: assumes "continuous_on S f" "x ∈ S" shows "¦f x¦ ≤ normf f" proof - have "bdd_above ((λx. ¦f x¦) ` S)" by (simp add: assms(1) bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs) then show ?thesis using assms cSUP_upper normf_def by fastforce qed lemma normf_least: "S ≠ {} ⟹ (⋀x. x ∈ S ⟹ ¦f x¦ ≤ M) ⟹ normf f ≤ M" by (simp add: normf_def cSUP_least) end lemma (in function_ring_on) one: assumes U: "open U" and t0: "t0 ∈ S" "t0 ∈ U" and t1: "t1 ∈ S-U" shows "∃V. open V ∧ t0 ∈ V ∧ S ∩ V ⊆ U ∧ (∀e>0. ∃f ∈ R. f ` S ⊆ {0..1} ∧ (∀t ∈ S ∩ V. f t < e) ∧ (∀t ∈ S - U. f t > 1 - e))" proof - have "∃pt ∈ R. pt t0 = 0 ∧ pt t > 0 ∧ pt ` S ⊆ {0..1}" if t: "t ∈ S - U" for t proof - have "t ≠ t0" using t t0 by auto then obtain g where g: "g ∈ R" "g t ≠ g t0" using separable t0 by (metis Diff_subset subset_eq t) define h where [abs_def]: "h x = g x - g t0" for x have "h ∈ R" unfolding h_def by (fast intro: g const diff) then have hsq: "(λw. (h w)⇧^{2}) ∈ R" by (simp add: power2_eq_square mult) have "h t ≠ h t0" by (simp add: h_def g) then have "h t ≠ 0" by (simp add: h_def) then have ht2: "0 < (h t)^2" by simp also have "... ≤ normf (λw. (h w)⇧^{2})" using t normf_upper [where x=t] continuous [OF hsq] by force finally have nfp: "0 < normf (λw. (h w)⇧^{2})" . define p where [abs_def]: "p x = (1 / normf (λw. (h w)⇧^{2})) * (h x)^2" for x have "p ∈ R" unfolding p_def by (fast intro: hsq const mult) moreover have "p t0 = 0" by (simp add: p_def h_def) moreover have "p t > 0" using nfp ht2 by (simp add: p_def) moreover have "⋀x. x ∈ S ⟹ p x ∈ {0..1}" using nfp normf_upper [OF continuous [OF hsq] ] by (auto simp: p_def) ultimately show "∃pt ∈ R. pt t0 = 0 ∧ pt t > 0 ∧ pt ` S ⊆ {0..1}" by auto qed then obtain pf where pf: "⋀t. t ∈ S-U ⟹ pf t ∈ R ∧ pf t t0 = 0 ∧ pf t t > 0" and pf01: "⋀t. t ∈ S-U ⟹ pf t ` S ⊆ {0..1}" by metis have com_sU: "compact (S-U)" using compact closed_Int_compact U by (simp add: Diff_eq compact_Int_closed open_closed) have "⋀t. t ∈ S-U ⟹ ∃A. open A ∧ A ∩ S = {x∈S. 0 < pf t x}" apply (rule open_Collect_positive) by (metis pf continuous) then obtain Uf where Uf: "⋀t. t ∈ S-U ⟹ open (Uf t) ∧ (Uf t) ∩ S = {x∈S. 0 < pf t x}" by metis then have open_Uf: "⋀t. t ∈ S-U ⟹ open (Uf t)" by blast have tUft: "⋀t. t ∈ S-U ⟹ t ∈ Uf t" using pf Uf by blast then have *: "S-U ⊆ (⋃x ∈ S-U. Uf x)" by blast obtain subU where subU: "subU ⊆ S - U" "finite subU" "S - U ⊆ (⋃x ∈ subU. Uf x)" by (blast intro: that compactE_image [OF com_sU open_Uf *]) then have [simp]: "subU ≠ {}" using t1 by auto then have cardp: "card subU > 0" using subU by (simp add: card_gt_0_iff) define p where [abs_def]: "p x = (1 / card subU) * (∑t ∈ subU. pf t x)" for x have pR: "p ∈ R" unfolding p_def using subU pf by (fast intro: pf const mult sum) have pt0 [simp]: "p t0 = 0" using subU pf by (auto simp: p_def intro: sum.neutral) have pt_pos: "p t > 0" if t: "t ∈ S-U" for t proof - obtain i where i: "i ∈ subU" "t ∈ Uf i" using subU t by blast show ?thesis using subU i t apply (clarsimp simp: p_def field_split_simps) apply (rule sum_pos2 [OF ‹finite subU›]) using Uf t pf01 apply auto apply (force elim!: subsetCE) done qed have p01: "p x ∈ {0..1}" if t: "x ∈ S" for x proof - have "0 ≤ p x" using subU cardp t pf01 by (fastforce simp add: p_def field_split_simps intro: sum_nonneg) moreover have "p x ≤ 1" using subU cardp t apply (simp add: p_def field_split_simps) apply (rule sum_bounded_above [where 'a=real and K=1, simplified]) using pf01 by force ultimately show ?thesis by auto qed have "compact (p ` (S-U))" by (meson Diff_subset com_sU compact_continuous_image continuous continuous_on_subset pR) then have "open (- (p ` (S-U)))" by (simp add: compact_imp_closed open_Compl) moreover have "0 ∈ - (p ` (S-U))" by (metis (no_types) ComplI image_iff not_less_iff_gr_or_eq pt_pos) ultimately obtain delta0 where delta0: "delta0 > 0" "ball 0 delta0 ⊆ - (p ` (S-U))" by (auto simp: elim!: openE) then have pt_delta: "⋀x. x ∈ S-U ⟹ p x ≥ delta0" by (force simp: ball_def dist_norm dest: p01) define δ where "δ = delta0/2" have "delta0 ≤ 1" using delta0 p01 [of t1] t1 by (force simp: ball_def dist_norm dest: p01) with delta0 have δ01: "0 < δ" "δ < 1" by (auto simp: δ_def) have pt_δ: "⋀x. x ∈ S-U ⟹ p x ≥ δ" using pt_delta delta0 by (force simp: δ_def) have "∃A. open A ∧ A ∩ S = {x∈S. p x < δ/2}" by (rule open_Collect_less_Int [OF continuous [OF pR] continuous_on_const]) then obtain V where V: "open V" "V ∩ S = {x∈S. p x < δ/2}" by blast define k where "k = nat⌊1/δ⌋ + 1" have "k>0" by (simp add: k_def) have "k-1 ≤ 1/δ" using δ01 by (simp add: k_def) with δ01 have "k ≤ (1+δ)/δ" by (auto simp: algebra_simps add_divide_distrib) also have "... < 2/δ" using δ01 by (auto simp: field_split_simps) finally have k2δ: "k < 2/δ" . have "1/δ < k" using δ01 unfolding k_def by linarith with δ01 k2δ have kδ: "1 < k*δ" "k*δ < 2" by (auto simp: field_split_simps) define q where [abs_def]: "q n t = (1 - p t^n)^(k^n)" for n t have qR: "q n ∈ R" for n by (simp add: q_def const diff power pR) have q01: "⋀n t. t ∈ S ⟹ q n t ∈ {0..1}" using p01 by (simp add: q_def power_le_one algebra_simps) have qt0 [simp]: "⋀n. n>0 ⟹ q n t0 = 1" using t0 pf by (simp add: q_def power_0_left) { fix t and n::nat assume t: "t ∈ S ∩ V" with ‹k>0› V have "k * p t < k * δ / 2" by force then have "1 - (k * δ / 2)^n ≤ 1 - (k * p t)^n" using ‹k>0› p01 t by (simp add: power_mono) also have "... ≤ q n t" using Bernoulli_inequality [of "- ((p t)^n)" "k^n"] apply (simp add: q_def) by (metis IntE atLeastAtMost_iff p01 power_le_one power_mult_distrib t) finally have "1 - (k * δ / 2)^n ≤ q n t" . } note limitV = this { fix t and n::nat assume t: "t ∈ S - U" with ‹k>0› U have "k * δ ≤ k * p t" by (simp add: pt_δ) with kδ have kpt: "1 < k * p t" by (blast intro: less_le_trans) have ptn_pos: "0 < p t^n" using pt_pos [OF t] by simp have ptn_le: "p t^n ≤ 1" by (meson DiffE atLeastAtMost_iff p01 power_le_one t) have "q n t = (1/(k^n * (p t)^n)) * (1 - p t^n)^(k^n) * k^n * (p t)^n" using pt_pos [OF t] ‹k>0› by (simp add: q_def) also have "... ≤ (1/(k * (p t))^n) * (1 - p t^n)^(k^n) * (1 + k^n * (p t)^n)" using pt_pos [OF t] ‹k>0› by (simp add: divide_simps mult_left_mono ptn_le) also have "... ≤ (1/(k * (p t))^n) * (1 - p t^n)^(k^n) * (1 + (p t)^n)^(k^n)" proof (rule mult_left_mono [OF Bernoulli_inequality]) show "0 ≤ 1 / (real k * p t)^n * (1 - p t^n)^k^n" using ptn_pos ptn_le by (auto simp: power_mult_distrib) qed (use ptn_pos in auto) also have "... = (1/(k * (p t))^n) * (1 - p t^(2*n))^(k^n)" using pt_pos [OF t] ‹k>0› by (simp add: algebra_simps power_mult power2_eq_square flip: power_mult_distrib) also have "... ≤ (1/(k * (p t))^n) * 1" using pt_pos ‹k>0› p01 power_le_one t by (intro mult_left_mono [OF power_le_one]) auto also have "... ≤ (1 / (k*δ))^n" using ‹k>0› δ01 power_mono pt_δ t by (fastforce simp: field_simps) finally have "q n t ≤ (1 / (real k * δ))^n " . } note limitNonU = this define NN where "NN e = 1 + nat ⌈max (ln e / ln (real k * δ / 2)) (- ln e / ln (real k * δ))⌉" for e have NN: "of_nat (NN e) > ln e / ln (real k * δ / 2)" "of_nat (NN e) > - ln e / ln (real k * δ)" if "0<e" for e unfolding NN_def by linarith+ have NN1: "(k * δ / 2)^NN e < e" if "e>0" for e proof - have "ln ((real k * δ / 2)^NN e) = real (NN e) * ln (real k * δ / 2)" by (simp add: ‹δ>0› ‹0 < k› ln_realpow) also have "... < ln e" using NN kδ that by (force simp add: field_simps) finally show ?thesis by (simp add: ‹δ>0› ‹0 < k› that) qed have NN0: "(1/(k*δ))^(NN e) < e" if "e>0" for e proof - have "0 < ln (real k) + ln δ" using δ01(1) ‹0 < k› kδ(1) ln_gt_zero ln_mult by fastforce then have "real (NN e) * ln (1 / (real k * δ)) < ln e" using kδ(1) NN(2) [of e] ‹0 < δ› ‹0 < k› that by (simp add: ln_div divide_simps) then have "exp (real (NN e) * ln (1 / (real k * δ))) < e" by (metis exp_less_mono exp_ln that) then show ?thesis by (simp add: δ01(1) ‹0 < k› exp_of_nat_mult) qed { fix t and e::real assume "e>0" have "t ∈ S ∩ V ⟹ 1 - q (NN e) t < e" "t ∈ S - U ⟹ q (NN e) t < e" proof - assume t: "t ∈ S ∩ V" show "1 - q (NN e) t < e" by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF ‹e>0›]]) next assume t: "t ∈ S - U" show "q (NN e) t < e" using limitNonU [OF t] less_le_trans [OF NN0 [OF ‹e>0›]] not_le by blast qed } then have "⋀e. e > 0 ⟹ ∃f∈R. f ` S ⊆ {0..1} ∧ (∀t ∈ S ∩ V. f t < e) ∧ (∀t ∈ S - U. 1 - e < f t)" using q01 by (rule_tac x="λx. 1 - q (NN e) x" in bexI) (auto simp: algebra_simps intro: diff const qR) moreover have t0V: "t0 ∈ V" "S ∩ V ⊆ U" using pt_δ t0 U V δ01 by fastforce+ ultimately show ?thesis using V t0V by blast qed text‹Non-trivial case, with \<^term>‹A› and \<^term>‹B› both non-empty› lemma (in function_ring_on) two_special: assumes A: "closed A" "A ⊆ S" "a ∈ A" and B: "closed B" "B ⊆ S" "b ∈ B" and disj: "A ∩ B = {}" and e: "0 < e" "e < 1" shows "∃f ∈ R. f ` S ⊆ {0..1} ∧ (∀x ∈ A. f x < e) ∧ (∀x ∈ B. f x > 1 - e)" proof - { fix w assume "w ∈ A" then have "open ( - B)" "b ∈ S" "w ∉ B" "w ∈ S" using assms by auto then have "∃V. open V ∧ w ∈ V ∧ S ∩ V ⊆ -B ∧ (∀e>0. ∃f ∈ R. f ` S ⊆ {0..1} ∧ (∀x ∈ S ∩ V. f x < e) ∧ (∀x ∈ S ∩ B. f x > 1 - e))" using one [of "-B" w b] assms ‹w ∈ A› by simp } then obtain Vf where Vf: "⋀w. w ∈ A ⟹ open (Vf w) ∧ w ∈ Vf w ∧ S ∩ Vf w ⊆ -B ∧ (∀e>0. ∃f ∈ R. f ` S ⊆ {0..1} ∧ (∀x ∈ S ∩ Vf w. f x < e) ∧ (∀x ∈ S ∩ B. f x > 1 - e))" by metis then have open_Vf: "⋀w. w ∈ A ⟹ open (Vf w)" by blast have tVft: "⋀w. w ∈ A ⟹ w ∈ Vf w" using Vf by blast then have sum_max_0: "A ⊆ (⋃x ∈ A. Vf x)" by blast have com_A: "compact A" using A by (metis compact compact_Int_closed inf.absorb_iff2) obtain subA where subA: "subA ⊆ A" "finite subA" "A ⊆ (⋃x ∈ subA. Vf x)" by (blast intro: that compactE_image [OF com_A open_Vf sum_max_0]) then have [simp]: "subA ≠ {}" using ‹a ∈ A› by auto then have cardp: "card subA > 0" using subA by (simp add: card_gt_0_iff) 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)" using Vf e cardp by simp then obtain ff where ff: "⋀w. w ∈ A ⟹ ff w ∈ R ∧ ff w ` S ⊆ {0..1} ∧ (∀x ∈ S ∩ Vf w. ff w x < e / card subA) ∧ (∀x ∈ S ∩ B. ff w x > 1 - e / card subA)" by metis define pff where [abs_def]: "pff x = (∏w ∈ subA. ff w x)" for x have pffR: "pff ∈ R" unfolding pff_def using subA ff by (auto simp: intro: prod) moreover have pff01: "pff x ∈ {0..1}" if t: "x ∈ S" for x proof - have "0 ≤ pff x" using subA cardp t ff by (fastforce simp: pff_def field_split_simps sum_nonneg intro: prod_nonneg) moreover have "pff x ≤ 1" using subA cardp t ff by (fastforce simp add: pff_def field_split_simps sum_nonneg intro: prod_mono [where g = "λx. 1", simplified]) ultimately show ?thesis by auto qed moreover { fix v x assume v: "v ∈ subA" and x: "x ∈ Vf v" "x ∈ S" from subA v have "pff x = ff v x * (∏w ∈ subA - {v}. ff w x)" unfolding pff_def by (metis prod.remove) also have "... ≤ ff v x * 1" proof - have "⋀i. i ∈ subA - {v} ⟹ 0 ≤ ff i x ∧ ff i x ≤ 1" by (metis Diff_subset atLeastAtMost_iff ff image_subset_iff subA(1) subsetD x(2)) moreover have "0 ≤ ff v x" using ff subA(1) v x(2) by fastforce ultimately show ?thesis by (metis mult_left_mono prod_mono [where g = "λx. 1", simplified]) qed also have "... < e / card subA" using ff subA(1) v x by auto also have "... ≤ e" using cardp e by (simp add: field_split_simps) finally have "pff x < e" . } then have "⋀x. x ∈ A ⟹ pff x < e" using A Vf subA by (metis UN_E contra_subsetD) moreover { fix x assume x: "x ∈ B" then have "x ∈ S" using B by auto have "1 - e ≤ (1 - e / card subA)^card subA" using Bernoulli_inequality [of "-e / card subA" "card subA"] e cardp by (auto simp: field_simps) also have "... = (∏w ∈ subA. 1 - e / card subA)" by (simp add: subA(2)) also have "... < pff x" proof - have "⋀i. i ∈ subA ⟹ e / real (card subA) ≤ 1 ∧ 1 - e / real (card subA) < ff i x" using e ‹B ⊆ S› ff subA(1) x by (force simp: field_split_simps) then show ?thesis using prod_mono_strict[of _ subA "λx. 1 - e / card subA" ] subA unfolding pff_def by (smt (verit, best) UN_E assms(3) subsetD) qed finally have "1 - e < pff x" . } ultimately show ?thesis by blast qed lemma (in function_ring_on) two: assumes A: "closed A" "A ⊆ S" and B: "closed B" "B ⊆ S" and disj: "A ∩ B = {}" and e: "0 < e" "e < 1" shows "∃f ∈ R. f ` S ⊆ {0..1} ∧ (∀x ∈ A. f x < e) ∧ (∀x ∈ B. f x > 1 - e)" proof (cases "A ≠ {} ∧ B ≠ {}") case True then show ?thesis using assms by (force simp flip: ex_in_conv intro!: two_special) next case False then consider "A={}" | "B={}" by force then show ?thesis proof cases case 1 with e show ?thesis by (rule_tac x="λx. 1" in bexI) (auto simp: const) next case 2 with e show ?thesis by (rule_tac x="λx. 0" in bexI) (auto simp: const) qed qed text‹The special case where \<^term>‹f› is non-negative and \<^term>‹e<1/3›› lemma (in function_ring_on) Stone_Weierstrass_special: assumes f: "continuous_on S f" and fpos: "⋀x. x ∈ S ⟹ f x ≥ 0" and e: "0 < e" "e < 1/3" shows "∃g ∈ R. ∀x∈S. ¦f x - g x¦ < 2*e" proof - define n where "n = 1 + nat ⌈normf f / e⌉" define A where "A j = {x ∈ S. f x ≤ (j - 1/3)*e}" for j :: nat define B where "B j = {x ∈ S. f x ≥ (j + 1/3)*e}" for j :: nat have ngt: "(n-1) * e ≥ normf f" using e pos_divide_le_eq real_nat_ceiling_ge[of "normf f / e"] by (fastforce simp add: divide_simps n_def) moreover have "n≥1" by (simp_all add: n_def) ultimately have ge_fx: "(n-1) * e ≥ f x" if "x ∈ S" for x using f normf_upper that by fastforce have "closed S" by (simp add: compact compact_imp_closed) { fix j have "closed (A j)" "A j ⊆ S" using ‹closed S› continuous_on_closed_Collect_le [OF f continuous_on_const] by (simp_all add: A_def Collect_restrict) moreover have "closed (B j)" "B j ⊆ S" using ‹closed S› continuous_on_closed_Collect_le [OF continuous_on_const f] by (simp_all add: B_def Collect_restrict) moreover have "(A j) ∩ (B j) = {}" using e by (auto simp: A_def B_def field_simps) ultimately have "∃f ∈ R. f ` S ⊆ {0..1} ∧ (∀x ∈ A j. f x < e/n) ∧ (∀x ∈ B j. f x > 1 - e/n)" using e ‹1 ≤ n› by (auto intro: two) } then obtain xf where xfR: "⋀j. xf j ∈ R" and xf01: "⋀j. xf j ` S ⊆ {0..1}" and xfA: "⋀x j. x ∈ A j ⟹ xf j x < e/n" and xfB: "⋀x j. x ∈ B j ⟹ xf j x > 1 - e/n" by metis define g where [abs_def]: "g x = e * (∑i≤n. xf i x)" for x have gR: "g ∈ R" unfolding g_def by (fast intro: mult const sum xfR) have gge0: "⋀x. x ∈ S ⟹ g x ≥ 0" using e xf01 by (simp add: g_def zero_le_mult_iff image_subset_iff sum_nonneg) have A0: "A 0 = {}" using fpos e by (fastforce simp: A_def) have An: "A n = S" using e ngt ‹n≥1› f normf_upper by (fastforce simp: A_def field_simps of_nat_diff) have Asub: "A j ⊆ A i" if "i≥j" for i j using e that by (force simp: A_def intro: order_trans) { fix t assume t: "t ∈ S" define j where "j = (LEAST j. t ∈ A j)" have jn: "j ≤ n" using t An by (simp add: Least_le j_def) have Aj: "t ∈ A j" using t An by (fastforce simp add: j_def intro: LeastI) then have Ai: "t ∈ A i" if "i≥j" for i using Asub [OF that] by blast then have fj1: "f t ≤ (j - 1/3)*e" by (simp add: A_def) then have Anj: "t ∉ A i" if "i<j" for i using Aj ‹i<j› not_less_Least by (fastforce simp add: j_def) have j1: "1 ≤ j" using A0 Aj j_def not_less_eq_eq by (fastforce simp add: j_def) then have Anj: "t ∉ A (j-1)" using Least_le by (fastforce simp add: j_def) then have fj2: "(j - 4/3)*e < f t" using j1 t by (simp add: A_def of_nat_diff) have xf_le1: "⋀i. xf i t ≤ 1" using xf01 t by force have "g t = e * (∑i≤n. xf i t)" by (simp add: g_def flip: distrib_left) also have "... = e * (∑i ∈ {..<j} ∪ {j..n}. xf i t)" by (simp add: ivl_disj_un_one(4) jn) also have "... = e * (∑i<j. xf i t) + e * (∑i=j..n. xf i t)" by (simp add: distrib_left ivl_disj_int sum.union_disjoint) also have "... ≤ e*j + e * ((Suc n - j)*e/n)" proof (intro add_mono mult_left_mono) show "(∑i<j. xf i t) ≤ j" by (rule sum_bounded_above [OF xf_le1, where A = "lessThan j", simplified]) have "xf i t ≤ e/n" if "i≥j" for i using xfA [OF Ai] that by (simp add: less_eq_real_def) then show "(∑i = j..n. xf i t) ≤ real (Suc n - j) * e / real n" using sum_bounded_above [of "{j..n}" "λi. xf i t"] by fastforce qed (use e in auto) also have "... ≤ j*e + e*(n - j + 1)*e/n " using ‹1 ≤ n› e by (simp add: field_simps del: of_nat_Suc) also have "... ≤ j*e + e*e" using ‹1 ≤ n› e j1 by (simp add: field_simps del: of_nat_Suc) also have "... < (j + 1/3)*e" using e by (auto simp: field_simps) finally have gj1: "g t < (j + 1 / 3) * e" . have gj2: "(j - 4/3)*e < g t" proof (cases "2 ≤ j") case False then have "j=1" using j1 by simp with t gge0 e show ?thesis by force next case True then have "(j - 4/3)*e < (j-1)*e - e^2" using e by (auto simp: of_nat_diff algebra_simps power2_eq_square) also have "... < (j-1)*e - ((j - 1)/n) * e^2" proof - have "(j - 1) / n < 1" using j1 jn by fastforce with ‹e>0› show ?thesis by (smt (verit, best) mult_less_cancel_right2 zero_less_power) qed also have "... = e * (j-1) * (1 - e/n)" by (simp add: power2_eq_square field_simps) also have "... ≤ e * (∑i≤j-2. xf i t)" proof - { fix i assume "i+2 ≤ j" then obtain d where "i+2+d = j" using le_Suc_ex that by blast then have "t ∈ B i" using Anj e ge_fx [OF t] ‹1 ≤ n› fpos [OF t] t unfolding A_def B_def by (auto simp add: field_simps of_nat_diff not_le intro: order_trans [of _ "e * 2 + e * d * 3 + e * i * 3"]) then have "xf i t > 1 - e/n" by (rule xfB) } moreover have "real (j - Suc 0) * (1 - e / real n) ≤ real (card {..j - 2}) * (1 - e / real n)" using Suc_diff_le True by fastforce ultimately show ?thesis using e True by (auto intro: order_trans [OF _ sum_bounded_below [OF less_imp_le]]) qed also have "... ≤ g t" using jn e xf01 t by (auto intro!: Groups_Big.sum_mono2 simp add: g_def zero_le_mult_iff image_subset_iff sum_nonneg) finally show ?thesis . qed have "¦f t - g t¦ < 2 * e" using fj1 fj2 gj1 gj2 by (simp add: abs_less_iff field_simps) } then show ?thesis by (rule_tac x=g in bexI) (auto intro: gR) qed text‹The ``unpretentious'' formulation› proposition (in function_ring_on) Stone_Weierstrass_basic: assumes f: "continuous_on S f" and e: "e > 0" shows "∃g ∈ R. ∀x∈S. ¦f x - g x¦ < e" proof - have "∃g ∈ R. ∀x∈S. ¦(f x + normf f) - g x¦ < 2 * min (e/2) (1/4)" proof (rule Stone_Weierstrass_special) show "continuous_on S (λx. f x + normf f)" by (force intro: Limits.continuous_on_add [OF f Topological_Spaces.continuous_on_const]) show "⋀x. x ∈ S ⟹ 0 ≤ f x + normf f" using normf_upper [OF f] by force qed (use e in auto) then obtain g where "g ∈ R" "∀x∈S. ¦g x - (f x + normf f)¦ < e" by force then show ?thesis by (rule_tac x="λx. g x - normf f" in bexI) (auto simp: algebra_simps intro: diff const) qed theorem (in function_ring_on) Stone_Weierstrass: assumes f: "continuous_on S f" shows "∃F∈UNIV → R. LIM n sequentially. F n :> uniformly_on S f" proof - define h where "h ≡ λn::nat. SOME g. g ∈ R ∧ (∀x∈S. ¦f x - g x¦ < 1 / (1 + n))" show ?thesis proof { fix e::real assume e: "0 < e" then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e" by (auto simp: real_arch_inverse [of e]) { fix n :: nat and x :: 'a and g :: "'a ⇒ real" assume n: "N ≤ n" "∀x∈S. ¦f x - g x¦ < 1 / (1 + real n)" assume x: "x ∈ S" have "¬ real (Suc n) < inverse e" using ‹N ≤ n› N using less_imp_inverse_less by force then have "1 / (1 + real n) ≤ e" using e by (simp add: field_simps) then have "¦f x - g x¦ < e" using n(2) x by auto } then have "∀⇩_{F}n in sequentially. ∀x∈S. ¦f x - h n x¦ < e" unfolding h_def by (force intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]] eventually_sequentiallyI [of N]) } then show "uniform_limit S h f sequentially" unfolding uniform_limit_iff by (auto simp: dist_norm abs_minus_commute) show "h ∈ UNIV → R" unfolding h_def by (force intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]]) qed qed text‹A HOL Light formulation› corollary Stone_Weierstrass_HOL: fixes R :: "('a::t2_space ⇒ real) set" and S :: "'a set" assumes "compact S" "⋀c. P(λx. c::real)" "⋀f. P f ⟹ continuous_on S f" "⋀f g. P(f) ∧ P(g) ⟹ P(λx. f x + g x)" "⋀f g. P(f) ∧ P(g) ⟹ P(λx. f x * g x)" "⋀x y. x ∈ S ∧ y ∈ S ∧ x ≠ y ⟹ ∃f. P(f) ∧ f x ≠ f y" "continuous_on S f" "0 < e" shows "∃g. P(g) ∧ (∀x ∈ S. ¦f x - g x¦ < e)" proof - interpret PR: function_ring_on "Collect P" by unfold_locales (use assms in auto) show ?thesis using PR.Stone_Weierstrass_basic [OF ‹continuous_on S f› ‹0 < e›] by blast qed subsection ‹Polynomial functions› inductive real_polynomial_function :: "('a::real_normed_vector ⇒ real) ⇒ bool" where linear: "bounded_linear f ⟹ real_polynomial_function f" | const: "real_polynomial_function (λx. c)" | add: "⟦real_polynomial_function f; real_polynomial_function g⟧ ⟹ real_polynomial_function (λx. f x + g x)" | mult: "⟦real_polynomial_function f; real_polynomial_function g⟧ ⟹ real_polynomial_function (λx. f x * g x)" declare real_polynomial_function.intros [intro] definition✐‹tag important› polynomial_function :: "('a::real_normed_vector ⇒ 'b::real_normed_vector) ⇒ bool" where "polynomial_function p ≡ (∀f. bounded_linear f ⟶ real_polynomial_function (f o p))" lemma real_polynomial_function_eq: "real_polynomial_function p = polynomial_function p" unfolding polynomial_function_def proof assume "real_polynomial_function p" then show " ∀f. bounded_linear f ⟶ real_polynomial_function (f ∘ p)" proof (induction p rule: real_polynomial_function.induct) case (linear h) then show ?case by (auto simp: bounded_linear_compose real_polynomial_function.linear) next case (const h) then show ?case by (simp add: real_polynomial_function.const) next case (add h) then show ?case by (force simp add: bounded_linear_def linear_add real_polynomial_function.add) next case (mult h) then show ?case by (force simp add: real_bounded_linear const real_polynomial_function.mult) qed next assume [rule_format, OF bounded_linear_ident]: "∀f. bounded_linear f ⟶ real_polynomial_function (f ∘ p)" then show "real_polynomial_function p" by (simp add: o_def) qed lemma polynomial_function_const [iff]: "polynomial_function (λx. c)" by (simp add: polynomial_function_def o_def const) lemma polynomial_function_bounded_linear: "bounded_linear f ⟹ polynomial_function f" by (simp add: polynomial_function_def o_def bounded_linear_compose real_polynomial_function.linear) lemma polynomial_function_id [iff]: "polynomial_function(λx. x)" by (simp add: polynomial_function_bounded_linear) lemma polynomial_function_add [intro]: "⟦polynomial_function f; polynomial_function g⟧ ⟹ polynomial_function (λx. f x + g x)" by (auto simp: polynomial_function_def bounded_linear_def linear_add real_polynomial_function.add o_def) lemma polynomial_function_mult [intro]: assumes f: "polynomial_function f" and g: "polynomial_function g" shows "polynomial_function (λx. f x *⇩_{R}g x)" proof - have "real_polynomial_function (λx. h (g x))" if "bounded_linear h" for h using g that unfolding polynomial_function_def o_def bounded_linear_def by (auto simp: real_polynomial_function_eq) moreover have "real_polynomial_function f" by (simp add: f real_polynomial_function_eq) ultimately show ?thesis unfolding polynomial_function_def bounded_linear_def o_def by (auto simp: linear.scaleR) qed lemma polynomial_function_cmul [intro]: assumes f: "polynomial_function f" shows "polynomial_function (λx. c *⇩_{R}f x)" by (rule polynomial_function_mult [OF polynomial_function_const f]) lemma polynomial_function_minus [intro]: assumes f: "polynomial_function f" shows "polynomial_function (λx. - f x)" using polynomial_function_cmul [OF f, of "-1"] by simp lemma polynomial_function_diff [intro]: "⟦polynomial_function f; polynomial_function g⟧ ⟹ polynomial_function (λx. f x - g x)" unfolding add_uminus_conv_diff [symmetric] by (metis polynomial_function_add polynomial_function_minus) lemma polynomial_function_sum [intro]: "⟦finite I; ⋀i. i ∈ I ⟹ polynomial_function (λx. f x i)⟧ ⟹ polynomial_function (λx. sum (f x) I)" by (induct I rule: finite_induct) auto lemma real_polynomial_function_minus [intro]: "real_polynomial_function f ⟹ real_polynomial_function (λx. - f x)" using polynomial_function_minus [of f] by (simp add: real_polynomial_function_eq) lemma real_polynomial_function_diff [intro]: "⟦real_polynomial_function f; real_polynomial_function g⟧ ⟹ real_polynomial_function (λx. f x - g x)" using polynomial_function_diff [of f] by (simp add: real_polynomial_function_eq) lemma real_polynomial_function_divide [intro]: assumes "real_polynomial_function p" shows "real_polynomial_function (λx. p x / c)" proof - have "real_polynomial_function (λx. p x * Fields.inverse c)" using assms by auto then show ?thesis by (simp add: divide_inverse) qed lemma real_polynomial_function_sum [intro]: "⟦finite I; ⋀i. i ∈ I ⟹ real_polynomial_function (λx. f x i)⟧ ⟹ real_polynomial_function (λx. sum (f x) I)" using polynomial_function_sum [of I f] by (simp add: real_polynomial_function_eq) lemma real_polynomial_function_prod [intro]: "⟦finite I; ⋀i. i ∈ I ⟹ real_polynomial_function (λx. f x i)⟧ ⟹ real_polynomial_function (λx. prod (f x) I)" by (induct I rule: finite_induct) auto lemma real_polynomial_function_gchoose: obtains p where "real_polynomial_function p" "⋀x. x gchoose r = p x" proof show "real_polynomial_function (λx. (∏i = 0..<r. x - real i) / fact r)" by force qed (simp add: gbinomial_prod_rev) lemma real_polynomial_function_power [intro]: "real_polynomial_function f ⟹ real_polynomial_function (λx. f x^n)" by (induct n) (simp_all add: const mult) lemma real_polynomial_function_compose [intro]: assumes f: "polynomial_function f" and g: "real_polynomial_function g" shows "real_polynomial_function (g o f)" using g proof (induction g rule: real_polynomial_function.induct) case (linear f) then show ?case using f polynomial_function_def by blast next case (add f g) then show ?case using f add by (auto simp: polynomial_function_def) next case (mult f g) then show ?case using f mult by (auto simp: polynomial_function_def) qed auto lemma polynomial_function_compose [intro]: assumes f: "polynomial_function f" and g: "polynomial_function g" shows "polynomial_function (g o f)" using g real_polynomial_function_compose [OF f] by (auto simp: polynomial_function_def o_def) lemma sum_max_0: fixes x::real (*in fact "'a::comm_ring_1"*) shows "(∑i≤max m n. x^i * (if i ≤ m then a i else 0)) = (∑i≤m. x^i * a i)" proof - 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))" by (auto simp: algebra_simps intro: sum.cong) also have "... = (∑i≤m. (if i ≤ m then x^i * a i else 0))" by (rule sum.mono_neutral_right) auto also have "... = (∑i≤m. x^i * a i)" by (auto simp: algebra_simps intro: sum.cong) finally show ?thesis . qed lemma real_polynomial_function_imp_sum: assumes "real_polynomial_function f" shows "∃a n::nat. f = (λx. ∑i≤n. a i * x^i)" using assms proof (induct f) case (linear f) then obtain c where f: "f = (λx. x * c)" by (auto simp add: real_bounded_linear) have "x * c = (∑i≤1. (if i = 0 then 0 else c) * x^i)" for x by (simp add: mult_ac) with f show ?case by fastforce next case (const c) have "c = (∑i≤0. c * x^i)" for x by auto then show ?case by fastforce case (add f1 f2) then obtain a1 n1 a2 n2 where "f1 = (λx. ∑i≤n1. a1 i * x^i)" "f2 = (λx. ∑i≤n2. a2 i * x^i)" by auto then have "f1 x + f2 x = (∑i≤max n1 n2. ((if i ≤ n1 then a1 i else 0) + (if i ≤ n2 then a2 i else 0)) * x^i)" for x using sum_max_0 [where m=n1 and n=n2] sum_max_0 [where m=n2 and n=n1] by (simp add: sum.distrib algebra_simps max.commute) then show ?case by force case (mult f1 f2) then obtain a1 n1 a2 n2 where "f1 = (λx. ∑i≤n1. a1 i * x^i)" "f2 = (λx. ∑i≤n2. a2 i * x^i)" by auto then obtain b1 b2 where "f1 = (λx. ∑i≤n1. b1 i * x^i)" "f2 = (λx. ∑i≤n2. b2 i * x^i)" "b1 = (λi. if i≤n1 then a1 i else 0)" "b2 = (λi. if i≤n2 then a2 i else 0)" by auto then have "f1 x * f2 x = (∑i≤n1 + n2. (∑k≤i. b1 k * b2 (i - k)) * x ^ i)" for x using polynomial_product [of n1 b1 n2 b2] by (simp add: Set_Interval.atLeast0AtMost) then show ?case by force qed lemma real_polynomial_function_iff_sum: "real_polynomial_function f ⟷ (∃a n. f = (λx. ∑i≤n. a i * x^i))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (metis real_polynomial_function_imp_sum) next assume ?rhs then show ?lhs by (auto simp: linear mult const real_polynomial_function_power real_polynomial_function_sum) qed lemma polynomial_function_iff_Basis_inner: fixes f :: "'a::real_normed_vector ⇒ 'b::euclidean_space" shows "polynomial_function f ⟷ (∀b∈Basis. real_polynomial_function (λx. inner (f x) b))" (is "?lhs = ?rhs") unfolding polynomial_function_def proof (intro iffI allI impI) assume "∀h. bounded_linear h ⟶ real_polynomial_function (h ∘ f)" then show ?rhs by (force simp add: bounded_linear_inner_left o_def) next fix h :: "'b ⇒ real" assume rp: "∀b∈Basis. real_polynomial_function (λx. f x ∙ b)" and h: "bounded_linear h" have "real_polynomial_function (h ∘ (λx. ∑b∈Basis. (f x ∙ b) *⇩_{R}b))" using rp by (force simp: real_polynomial_function_eq polynomial_function_mult intro!: real_polynomial_function_compose [OF _ linear [OF h]]) then show "real_polynomial_function (h ∘ f)" by (simp add: euclidean_representation_sum_fun) qed subsection ‹Stone-Weierstrass theorem for polynomial functions› text‹First, we need to show that they are continuous, differentiable and separable.› lemma continuous_real_polymonial_function: assumes "real_polynomial_function f" shows "continuous (at x) f" using assms by (induct f) (auto simp: linear_continuous_at) lemma continuous_polymonial_function: fixes f :: "'a::real_normed_vector ⇒ 'b::euclidean_space" assumes "polynomial_function f" shows "continuous (at x) f" proof (rule euclidean_isCont) show "⋀b. b ∈ Basis ⟹ isCont (λx. (f x ∙ b) *⇩_{R}b) x" using assms continuous_real_polymonial_function by (force simp: polynomial_function_iff_Basis_inner intro: isCont_scaleR) qed lemma continuous_on_polymonial_function: fixes f :: "'a::real_normed_vector ⇒ 'b::euclidean_space" assumes "polynomial_function f" shows "continuous_on S f" using continuous_polymonial_function [OF assms] continuous_at_imp_continuous_on by blast lemma has_real_derivative_polynomial_function: assumes "real_polynomial_function p" shows "∃p'. real_polynomial_function p' ∧ (∀x. (p has_real_derivative (p' x)) (at x))" using assms proof (induct p) case (linear p) then show ?case by (force simp: real_bounded_linear const intro!: derivative_eq_intros) next case (const c) show ?case by (rule_tac x="λx. 0" in exI) auto case (add f1 f2) then obtain p1 p2 where "real_polynomial_function p1" "⋀x. (f1 has_real_derivative p1 x) (at x)" "real_polynomial_function p2" "⋀x. (f2 has_real_derivative p2 x) (at x)" by auto then show ?case by (rule_tac x="λx. p1 x + p2 x" in exI) (auto intro!: derivative_eq_intros) case (mult f1 f2) then obtain p1 p2 where "real_polynomial_function p1" "⋀x. (f1 has_real_derivative p1 x) (at x)" "real_polynomial_function p2" "⋀x. (f2 has_real_derivative p2 x) (at x)" by auto then show ?case using mult by (rule_tac x="λx. f1 x * p2 x + f2 x * p1 x" in exI) (auto intro!: derivative_eq_intros) qed lemma has_vector_derivative_polynomial_function: fixes p :: "real ⇒ 'a::euclidean_space" assumes "polynomial_function p" obtains p' where "polynomial_function p'" "⋀x. (p has_vector_derivative (p' x)) (at x)" proof - { fix b :: 'a assume "b ∈ Basis" then obtain p' where p': "real_polynomial_function p'" and pd: "⋀x. ((λx. p x ∙ b) has_real_derivative p' x) (at x)" using assms [unfolded polynomial_function_iff_Basis_inner] has_real_derivative_polynomial_function by blast have "polynomial_function (λx. p' x *⇩_{R}b)" using ‹b ∈ Basis› p' const [where 'a=real and c=0] by (simp add: polynomial_function_iff_Basis_inner inner_Basis) then have "∃q. polynomial_function q ∧ (∀x. ((λu. (p u ∙ b) *⇩_{R}b) has_vector_derivative q x) (at x))" by (fastforce intro: derivative_eq_intros pd) } then obtain qf where qf: "⋀b. b ∈ Basis ⟹ polynomial_function (qf b)" "⋀b x. b ∈ Basis ⟹ ((λu. (p u ∙ b) *⇩_{R}b) has_vector_derivative qf b x) (at x)" by metis show ?thesis proof show "⋀x. (p has_vector_derivative (∑b∈Basis. qf b x)) (at x)" apply (subst euclidean_representation_sum_fun [of p, symmetric]) by (auto intro: has_vector_derivative_sum qf) qed (force intro: qf) qed lemma real_polynomial_function_separable: fixes x :: "'a::euclidean_space" assumes "x ≠ y" shows "∃f. real_polynomial_function f ∧ f x ≠ f y" proof - have "real_polynomial_function (λu. ∑b∈Basis. (inner (x-u) b)^2)" proof (rule real_polynomial_function_sum) show "⋀i. i ∈ Basis ⟹ real_polynomial_function (λu. ((x - u) ∙ i)⇧^{2})" by (auto simp: algebra_simps real_polynomial_function_diff const linear bounded_linear_inner_left) qed auto moreover have "(∑b∈Basis. ((x - y) ∙ b)⇧^{2}) ≠ 0" using assms by (force simp add: euclidean_eq_iff [of x y] sum_nonneg_eq_0_iff algebra_simps) ultimately show ?thesis by auto qed lemma Stone_Weierstrass_real_polynomial_function: fixes f :: "'a::euclidean_space ⇒ real" assumes "compact S" "continuous_on S f" "0 < e" obtains g where "real_polynomial_function g" "⋀x. x ∈ S ⟹ ¦f x - g x¦ < e" proof - interpret PR: function_ring_on "Collect real_polynomial_function" proof unfold_locales qed (use assms continuous_on_polymonial_function real_polynomial_function_eq in ‹auto intro: real_polynomial_function_separable›) show ?thesis using PR.Stone_Weierstrass_basic [OF ‹continuous_on S f› ‹0 < e›] that by blast qed theorem Stone_Weierstrass_polynomial_function: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes S: "compact S" and f: "continuous_on S f" and e: "0 < e" shows "∃g. polynomial_function g ∧ (∀x ∈ S. norm(f x - g x) < e)" proof - { fix b :: 'b assume "b ∈ Basis" have "∃p. real_polynomial_function p ∧ (∀x ∈ S. ¦f x ∙ b - p x¦ < e / DIM('b))" proof (rule Stone_Weierstrass_real_polynomial_function [OF S _, of "λx. f x ∙ b" "e / card Basis"]) show "continuous_on S (λx. f x ∙ b)" using f by (auto intro: continuous_intros) qed (use e in auto) } then obtain pf where pf: "⋀b. b ∈ Basis ⟹ real_polynomial_function (pf b) ∧ (∀x ∈ S. ¦f x ∙ b - pf b x¦ < e / DIM('b))" by metis let ?g = "λx. ∑b∈Basis. pf b x *⇩_{R}b" { fix x assume "x ∈ S" have "norm (∑b∈Basis. (f x ∙ b) *⇩_{R}b - pf b x *⇩_{R}b) ≤ (∑b∈Basis. norm ((f x ∙ b) *⇩_{R}b - pf b x *⇩_{R}b))" by (rule norm_sum) also have "... < of_nat DIM('b) * (e / DIM('b))" proof (rule sum_bounded_above_strict) show "⋀i. i ∈ Basis ⟹ norm ((f x ∙ i) *⇩_{R}i - pf i x *⇩_{R}i) < e / real DIM('b)" by (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf ‹x ∈ S›) qed (rule DIM_positive) also have "... = e" by (simp add: field_simps) finally have "norm (∑b∈Basis. (f x ∙ b) *⇩_{R}b - pf b x *⇩_{R}b) < e" . } then have "