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