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