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