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