Theory HOL-Analysis.Weierstrass_Theorems

section ‹Bernstein-Weierstrass and Stone-Weierstrass›

text‹By L C Paulson (2015)›

theory Weierstrass_Theorems
imports Uniform_Limit Path_Connected Derivative
begin

subsection ‹Bernstein polynomials›

definitiontag important› Bernstein :: "[nat,nat,real]  real" where
  "Bernstein n k x  of_nat (n choose k) * x^k * (1 - x)^(n - k)"

lemma Bernstein_nonneg: "0  x; x  1  0  Bernstein n k x"
  by (simp add: Bernstein_def)

lemma Bernstein_pos: "0 < x; x < 1; k  n  0 < Bernstein n k x"
  by (simp add: Bernstein_def)

lemma sum_Bernstein [simp]: "(kn. Bernstein n k x) = 1"
  using binomial_ring [of x "1-x" n]
  by (simp add: Bernstein_def)

lemma binomial_deriv1:
    "(kn. (of_nat k * of_nat (n choose k)) * a^(k-1) * b^(n-k)) = real_of_nat n * (a+b)^(n-1)"
  apply (rule DERIV_unique [where f = "λa. (a+b)^n" and x=a])
  apply (subst binomial_ring)
  apply (rule derivative_eq_intros sum.cong | simp add: atMost_atLeast0)+
  done

lemma binomial_deriv2:
    "(kn. (of_nat k * of_nat (k-1) * of_nat (n choose k)) * a^(k-2) * b^(n-k)) =
     of_nat n * of_nat (n-1) * (a+b::real)^(n-2)"
  apply (rule DERIV_unique [where f = "λa. of_nat n * (a+b::real)^(n-1)" and x=a])
  apply (subst binomial_deriv1 [symmetric])
  apply (rule derivative_eq_intros sum.cong | simp add: Num.numeral_2_eq_2)+
  done

lemma sum_k_Bernstein [simp]: "(kn. real k * Bernstein n k x) = of_nat n * x"
  apply (subst binomial_deriv1 [of n x "1-x", simplified, symmetric])
  apply (simp add: sum_distrib_right)
  apply (auto simp: Bernstein_def algebra_simps power_eq_if intro!: sum.cong)
  done

lemma sum_kk_Bernstein [simp]: "(kn. real k * (real k - 1) * Bernstein n k x) = real n * (real n - 1) * x2"
proof -
  have "(kn. real k * (real k - 1) * Bernstein n k x) =
        (kn. real k * real (k - Suc 0) * real (n choose k) * x^(k - 2) * (1 - x)^(n - k) * x2)"
  proof (rule sum.cong [OF refl], simp)
    fix k
    assume "k  n"
    then consider "k = 0" | "k = 1" | k' where "k = Suc (Suc k')"
      by (metis One_nat_def not0_implies_Suc)
    then show "k = 0 
          (real k - 1) * Bernstein n k x =
          real (k - Suc 0) *
          (real (n choose k) * (x^(k - 2) * ((1 - x)^(n - k) * x2)))"
      by cases (auto simp add: Bernstein_def power2_eq_square algebra_simps)
  qed
  also have "... = real_of_nat n * real_of_nat (n - Suc 0) * x2"
    by (subst binomial_deriv2 [of n x "1-x", simplified, symmetric]) (simp add: sum_distrib_right)
  also have "... = n * (n - 1) * x2"
    by auto
  finally show ?thesis
    by auto
qed

subsection ‹Explicit Bernstein version of the 1D Weierstrass approximation theorem›

theorem Bernstein_Weierstrass:
  fixes f :: "real  real"
  assumes contf: "continuous_on {0..1} f" and e: "0 < e"
    shows "N. n x. N  n  x  {0..1}
                     ¦f x - (kn. f(k/n) * Bernstein n k x)¦ < e"
proof -
  have "bounded (f ` {0..1})"
    using compact_continuous_image compact_imp_bounded contf by blast
  then obtain M where M: "x. 0  x  x  1  ¦f x¦  M"
    by (force simp add: bounded_iff)
  then have "0  M" by force
  have ucontf: "uniformly_continuous_on {0..1} f"
    using compact_uniformly_continuous contf by blast
  then obtain d where d: "d>0" "x x'.  x  {0..1}; x'  {0..1}; ¦x' - x¦ < d  ¦f x' - f x¦ < e/2"
     apply (rule uniformly_continuous_onE [where e = "e/2"])
     using e by (auto simp: dist_norm)
  { fix n::nat and x::real
    assume n: "Suc (nat4*M/(e*d2))  n" and x: "0  x" "x  1"
    have "0 < n" using n by simp
    have ed0: "- (e * d2) < 0"
      using e 0<d by simp
    also have "...  M * 4"
      using 0M by simp
    finally have [simp]: "real_of_int (nat 4 * M / (e * d2)) = real_of_int 4 * M / (e * d2)"
      using 0M e 0<d
      by (simp add: field_simps)
    have "4*M/(e*d2) + 1  real (Suc (nat4*M/(e*d2)))"
      by (simp add: real_nat_ceiling_ge)
    also have "...  real n"
      using n by (simp add: field_simps)
    finally have nbig: "4*M/(e*d2) + 1  real n" .
    have sum_bern: "(kn. (x - k/n)2 * Bernstein n k x) = x * (1 - x) / n"
    proof -
      have *: "a b x::real. (a - b)2 * x = a * (a - 1) * x + (1 - 2 * b) * a * x + b * b * x"
        by (simp add: algebra_simps power2_eq_square)
      have "(kn. (k - n * x)2 * Bernstein n k x) = n * x * (1 - x)"
        apply (simp add: * sum.distrib)
        apply (simp flip: sum_distrib_left add: mult.assoc)
        apply (simp add: algebra_simps power2_eq_square)
        done
      then have "(kn. (k - n * x)2 * Bernstein n k x)/n^2 = x * (1 - x) / n"
        by (simp add: power2_eq_square)
      then show ?thesis
        using n by (simp add: sum_divide_distrib field_split_simps power2_commute)
    qed
    { fix k
      assume k: "k  n"
      then have kn: "0  k / n" "k / n  1"
        by (auto simp: field_split_simps)
      consider (lessd) "¦x - k / n¦ < d" | (ged) "d  ¦x - k / n¦"
        by linarith
      then have "¦(f x - f (k/n))¦  e/2 + 2 * M / d2 * (x - k/n)2"
      proof cases
        case lessd
        then have "¦(f x - f (k/n))¦ < e/2"
          using d x kn by (simp add: abs_minus_commute)
        also have "...  (e/2 + 2 * M / d2 * (x - k/n)2)"
          using M0 d by simp
        finally show ?thesis by simp
      next
        case ged
        then have dle: "d2  (x - k/n)2"
          by (metis d(1) less_eq_real_def power2_abs power_mono)
        have §: "1  (x - real k / real n)2 / d2"
          using dle d>0 by auto
        have "¦(f x - f (k/n))¦  ¦f x¦ + ¦f (k/n)¦"
          by (rule abs_triangle_ineq4)
        also have "...  M+M"
          by (meson M add_mono_thms_linordered_semiring(1) kn x)
        also have "...  2 * M * ((x - k/n)2 / d2)"
          using § M0 mult_left_mono by fastforce
        also have "...  e/2 + 2 * M / d2 * (x - k/n)2"
          using e  by simp
        finally show ?thesis .
        qed
    } note * = this
    have "¦f x - (kn. f(k / n) * Bernstein n k x)¦  ¦kn. (f x - f(k / n)) * Bernstein n k x¦"
      by (simp add: sum_subtractf sum_distrib_left [symmetric] algebra_simps)
    also have "...  (kn. ¦(f x - f(k / n)) * Bernstein n k x¦)"
      by (rule sum_abs)
    also have "...  (kn. (e/2 + (2 * M / d2) * (x - k / n)2) * Bernstein n k x)"
      using *
      by (force simp add: abs_mult Bernstein_nonneg x mult_right_mono intro: sum_mono)
    also have "...  e/2 + (2 * M) / (d2 * n)"
      unfolding sum.distrib Rings.semiring_class.distrib_right sum_distrib_left [symmetric] mult.assoc sum_bern
      using d>0 x by (simp add: divide_simps M0 mult_le_one mult_left_le)
    also have "... < e"
      using d>0 nbig e n>0 
      apply (simp add: field_split_simps)
      using ed0 by linarith
    finally have "¦f x - (kn. f (real k / real n) * Bernstein n k x)¦ < e" .
  }
  then show ?thesis
    by auto
qed


subsection ‹General Stone-Weierstrass theorem›

text‹Source:
Bruno Brosowski and Frank Deutsch.
An Elementary Proof of the Stone-Weierstrass Theorem.
Proceedings of the American Mathematical Society
Volume 81, Number 1, January 1981.
DOI: 10.2307/2043993  🌐‹https://www.jstor.org/stable/2043993›

locale function_ring_on =
  fixes R :: "('a::t2_space  real) set" and S :: "'a set"
  assumes compact: "compact S"
  assumes continuous: "f  R  continuous_on S f"
  assumes add: "f  R  g  R  (λx. f x + g x)  R"
  assumes mult: "f  R  g  R  (λx. f x * g x)  R"
  assumes const: "(λ_. c)  R"
  assumes separable: "x  S  y  S  x  y  fR. f x  f y"

begin
  lemma minus: "f  R  (λx. - f x)  R"
    by (frule mult [OF const [of "-1"]]) simp

  lemma diff: "f  R  g  R  (λx. f x - g x)  R"
    unfolding diff_conv_add_uminus by (metis add minus)

  lemma power: "f  R  (λx. f x^n)  R"
    by (induct n) (auto simp: const mult)

  lemma sum: "finite I; i. i  I  f i  R  (λx. i  I. f i x)  R"
    by (induct I rule: finite_induct; simp add: const add)

  lemma prod: "finite I; i. i  I  f i  R  (λx. i  I. f i x)  R"
    by (induct I rule: finite_induct; simp add: const mult)

  definitiontag important› normf :: "('a::t2_space  real)  real"
    where "normf f  SUP xS. ¦f x¦"

  lemma normf_upper: 
    assumes "continuous_on S f" "x  S" shows "¦f x¦  normf f"
  proof -
    have "bdd_above ((λx. ¦f x¦) ` S)"
      by (simp add: assms(1) bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs)
    then show ?thesis
      using assms cSUP_upper normf_def by fastforce
  qed

  lemma normf_least: "S  {}  (x. x  S  ¦f x¦  M)  normf f  M"
    by (simp add: normf_def cSUP_least)

end

lemma (in function_ring_on) one:
  assumes U: "open U" and t0: "t0  S" "t0  U" and t1: "t1  S-U"
    shows "V. open V  t0  V  S  V  U 
               (e>0. f  R. f ` S  {0..1}  (t  S  V. f t < e)  (t  S - U. f t > 1 - e))"
proof -
  have "pt  R. pt t0 = 0  pt t > 0  pt ` S  {0..1}" if t: "t  S - U" for t
  proof -
    have "t  t0" using t t0 by auto
    then obtain g where g: "g  R" "g t  g t0"
      using separable t0  by (metis Diff_subset subset_eq t)
    define h where [abs_def]: "h x = g x - g t0" for x
    have "h  R"
      unfolding h_def by (fast intro: g const diff)
    then have hsq: "(λw. (h w)2)  R"
      by (simp add: power2_eq_square mult)
    have "h t  h t0"
      by (simp add: h_def g)
    then have "h t  0"
      by (simp add: h_def)
    then have ht2: "0 < (h t)^2"
      by simp
    also have "...  normf (λw. (h w)2)"
      using t normf_upper [where x=t] continuous [OF hsq] by force
    finally have nfp: "0 < normf (λw. (h w)2)" .
    define p where [abs_def]: "p x = (1 / normf (λw. (h w)2)) * (h x)^2" for x
    have "p  R"
      unfolding p_def by (fast intro: hsq const mult)
    moreover have "p t0 = 0"
      by (simp add: p_def h_def)
    moreover have "p t > 0"
      using nfp ht2 by (simp add: p_def)
    moreover have "x. x  S  p x  {0..1}"
      using nfp normf_upper [OF continuous [OF hsq] ] by (auto simp: p_def)
    ultimately show "pt  R. pt t0 = 0  pt t > 0  pt ` S  {0..1}"
      by auto
  qed
  then obtain pf where pf: "t. t  S-U  pf t  R  pf t t0 = 0  pf t t > 0"
                   and pf01: "t. t  S-U  pf t ` S  {0..1}"
    by metis
  have com_sU: "compact (S-U)"
    using compact closed_Int_compact U by (simp add: Diff_eq compact_Int_closed open_closed)
  have "t. t  S-U  A. open A  A  S = {xS. 0 < pf t x}"
    apply (rule open_Collect_positive)
    by (metis pf continuous)
  then obtain Uf where Uf: "t. t  S-U  open (Uf t)  (Uf t)  S = {xS. 0 < pf t x}"
    by metis
  then have open_Uf: "t. t  S-U  open (Uf t)"
    by blast
  have tUft: "t. t  S-U  t  Uf t"
    using pf Uf by blast
  then have *: "S-U  (x  S-U. Uf x)"
    by blast
  obtain subU where subU: "subU  S - U" "finite subU" "S - U  (x  subU. Uf x)"
    by (blast intro: that compactE_image [OF com_sU open_Uf *])
  then have [simp]: "subU  {}"
    using t1 by auto
  then have cardp: "card subU > 0" using subU
    by (simp add: card_gt_0_iff)
  define p where [abs_def]: "p x = (1 / card subU) * (t  subU. pf t x)" for x
  have pR: "p  R"
    unfolding p_def using subU pf by (fast intro: pf const mult sum)
  have pt0 [simp]: "p t0 = 0"
    using subU pf by (auto simp: p_def intro: sum.neutral)
  have pt_pos: "p t > 0" if t: "t  S-U" for t
  proof -
    obtain i where i: "i  subU" "t  Uf i" using subU t by blast
    show ?thesis
      using subU i t
      apply (clarsimp simp: p_def field_split_simps)
      apply (rule sum_pos2 [OF finite subU])
      using Uf t pf01 apply auto
      apply (force elim!: subsetCE)
      done
  qed
  have p01: "p x  {0..1}" if t: "x  S" for x
  proof -
    have "0  p x"
      using subU cardp t pf01
      by (fastforce simp add: p_def field_split_simps intro: sum_nonneg)
    moreover have "p x  1"
      using subU cardp t 
      apply (simp add: p_def field_split_simps)
      apply (rule sum_bounded_above [where 'a=real and K=1, simplified])
      using pf01 by force
    ultimately show ?thesis
      by auto
  qed
  have "compact (p ` (S-U))"
    by (meson Diff_subset com_sU compact_continuous_image continuous continuous_on_subset pR)
  then have "open (- (p ` (S-U)))"
    by (simp add: compact_imp_closed open_Compl)
  moreover have "0  - (p ` (S-U))"
    by (metis (no_types) ComplI image_iff not_less_iff_gr_or_eq pt_pos)
  ultimately obtain delta0 where delta0: "delta0 > 0" "ball 0 delta0  - (p ` (S-U))"
    by (auto simp: elim!: openE)
  then have pt_delta: "x. x  S-U  p x  delta0"
    by (force simp: ball_def dist_norm dest: p01)
  define δ where "δ = delta0/2"
  have "delta0  1" using delta0 p01 [of t1] t1
      by (force simp: ball_def dist_norm dest: p01)
  with delta0 have δ01: "0 < δ" "δ < 1"
    by (auto simp: δ_def)
  have pt_δ: "x. x  S-U  p x  δ"
    using pt_delta delta0 by (force simp: δ_def)
  have "A. open A  A  S = {xS. p x < δ/2}"
    by (rule open_Collect_less_Int [OF continuous [OF pR] continuous_on_const])
  then obtain V where V: "open V" "V  S = {xS. p x < δ/2}"
    by blast
  define k where "k = nat1/δ + 1"
  have "k>0"  by (simp add: k_def)
  have "k-1  1/δ"
    using δ01 by (simp add: k_def)
  with δ01 have "k  (1+δ)/δ"
    by (auto simp: algebra_simps add_divide_distrib)
  also have "... < 2/δ"
    using δ01 by (auto simp: field_split_simps)
  finally have k2δ: "k < 2/δ" .
  have "1/δ < k"
    using δ01 unfolding k_def by linarith
  with δ01 k2δ have : "1 < k*δ" "k*δ < 2"
    by (auto simp: field_split_simps)
  define q where [abs_def]: "q n t = (1 - p t^n)^(k^n)" for n t
  have qR: "q n  R" for n
    by (simp add: q_def const diff power pR)
  have q01: "n t. t  S  q n t  {0..1}"
    using p01 by (simp add: q_def power_le_one algebra_simps)
  have qt0 [simp]: "n. n>0  q n t0 = 1"
    using t0 pf by (simp add: q_def power_0_left)
  { fix t and n::nat
    assume t: "t  S  V"
    with k>0 V have "k * p t < k * δ / 2"
       by force
    then have "1 - (k * δ / 2)^n  1 - (k * p t)^n"
      using  k>0 p01 t by (simp add: power_mono)
    also have "...  q n t"
      using Bernoulli_inequality [of "- ((p t)^n)" "k^n"] 
      apply (simp add: q_def)
      by (metis IntE atLeastAtMost_iff p01 power_le_one power_mult_distrib t)
    finally have "1 - (k * δ / 2)^n  q n t" .
  } note limitV = this
  { fix t and n::nat
    assume t: "t  S - U"
    with k>0 U have "k * δ  k * p t"
      by (simp add: pt_δ)
    with  have kpt: "1 < k * p t"
      by (blast intro: less_le_trans)
    have ptn_pos: "0 < p t^n"
      using pt_pos [OF t] by simp
    have ptn_le: "p t^n  1"
      by (meson DiffE atLeastAtMost_iff p01 power_le_one t)
    have "q n t = (1/(k^n * (p t)^n)) * (1 - p t^n)^(k^n) * k^n * (p t)^n"
      using pt_pos [OF t] k>0 by (simp add: q_def)
    also have "...  (1/(k * (p t))^n) * (1 - p t^n)^(k^n) * (1 + k^n * (p t)^n)"
      using pt_pos [OF t] k>0
      by (simp add: divide_simps mult_left_mono ptn_le)
    also have "...  (1/(k * (p t))^n) * (1 - p t^n)^(k^n) * (1 + (p t)^n)^(k^n)"
    proof (rule mult_left_mono [OF Bernoulli_inequality])
      show "0  1 / (real k * p t)^n * (1 - p t^n)^k^n"
        using ptn_pos ptn_le by (auto simp: power_mult_distrib)
    qed (use ptn_pos in auto)
    also have "... = (1/(k * (p t))^n) * (1 - p t^(2*n))^(k^n)"
      using pt_pos [OF t] k>0
      by (simp add: algebra_simps power_mult power2_eq_square flip: power_mult_distrib)
    also have "...  (1/(k * (p t))^n) * 1"
      using pt_pos k>0 p01 power_le_one t
      by (intro mult_left_mono [OF power_le_one]) auto
    also have "...  (1 / (k*δ))^n"
      using k>0 δ01  power_mono pt_δ t
      by (fastforce simp: field_simps)
    finally have "q n t  (1 / (real k * δ))^n " .
  } note limitNonU = this
  define NN
    where "NN e = 1 + nat max (ln e / ln (real k * δ / 2)) (- ln e / ln (real k * δ))" for e
  have NN: "of_nat (NN e) > ln e / ln (real k * δ / 2)"  "of_nat (NN e) > - ln e / ln (real k * δ)"
              if "0<e" for e
      unfolding NN_def  by linarith+
    have NN1: "(k * δ / 2)^NN e < e" if "e>0" for e
    proof -
      have "ln ((real k * δ / 2)^NN e) = real (NN e) * ln (real k * δ / 2)"
        by (simp add: δ>0 0 < k ln_realpow)
      also have "... < ln e"
        using NN  that by (force simp add: field_simps)
      finally show ?thesis
        by (simp add: δ>0 0 < k that)
    qed
  have NN0: "(1/(k*δ))^(NN e) < e" if "e>0" for e
  proof -
    have "0 < ln (real k) + ln δ"
      using δ01(1) 0 < k (1) ln_gt_zero ln_mult by fastforce 
    then have "real (NN e) * ln (1 / (real k * δ)) < ln e"
      using (1) NN(2) [of e] that by (simp add: ln_div divide_simps)
    then have "exp (real (NN e) * ln (1 / (real k * δ))) < e"
      by (metis exp_less_mono exp_ln that)
    then show ?thesis
      by (simp add: δ01(1) 0 < k exp_of_nat_mult)
  qed
  { fix t and e::real
    assume "e>0"
    have "t  S  V  1 - q (NN e) t < e" "t  S - U  q (NN e) t < e"
    proof -
      assume t: "t  S  V"
      show "1 - q (NN e) t < e"
        by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF e>0]])
    next
      assume t: "t  S - U"
      show "q (NN e) t < e"
      using  limitNonU [OF t] less_le_trans [OF NN0 [OF e>0]] not_le by blast
    qed
  } then have "e. e > 0  fR. f ` S  {0..1}  (t  S  V. f t < e)  (t  S - U. 1 - e < f t)"
    using q01
    by (rule_tac x="λx. 1 - q (NN e) x" in bexI) (auto simp: algebra_simps intro: diff const qR)
  moreover have t0V: "t0  V"  "S  V  U"
    using pt_δ t0 U V δ01  by fastforce+
  ultimately show ?thesis using V t0V
    by blast
qed

text‹Non-trivial case, with termA and termB both non-empty›
lemma (in function_ring_on) two_special:
  assumes A: "closed A" "A  S" "a  A"
      and B: "closed B" "B  S" "b  B"
      and disj: "A  B = {}"
      and e: "0 < e" "e < 1"
    shows "f  R. f ` S  {0..1}  (x  A. f x < e)  (x  B. f x > 1 - e)"
proof -
  { fix w
    assume "w  A"
    then have "open ( - B)" "b  S" "w  B" "w  S"
      using assms by auto
    then have "V. open V  w  V  S  V  -B 
               (e>0. f  R. f ` S  {0..1}  (x  S  V. f x < e)  (x  S  B. f x > 1 - e))"
      using one [of "-B" w b] assms w  A by simp
  }
  then obtain Vf where Vf:
         "w. w  A  open (Vf w)  w  Vf w  S  Vf w  -B 
                         (e>0. f  R. f ` S  {0..1}  (x  S  Vf w. f x < e)  (x  S  B. f x > 1 - e))"
    by metis
  then have open_Vf: "w. w  A  open (Vf w)"
    by blast
  have tVft: "w. w  A  w  Vf w"
    using Vf by blast
  then have sum_max_0: "A  (x  A. Vf x)"
    by blast
  have com_A: "compact A" using A
    by (metis compact compact_Int_closed inf.absorb_iff2)
  obtain subA where subA: "subA  A" "finite subA" "A  (x  subA. Vf x)"
    by (blast intro: that compactE_image [OF com_A open_Vf sum_max_0])
  then have [simp]: "subA  {}"
    using a  A by auto
  then have cardp: "card subA > 0" using subA
    by (simp add: card_gt_0_iff)
  have "w. w  A  f  R. f ` S  {0..1}  (x  S  Vf w. f x < e / card subA)  (x  S  B. f x > 1 - e / card subA)"
    using Vf e cardp by simp
  then obtain ff where ff:
         "w. w  A  ff w  R  ff w ` S  {0..1} 
                         (x  S  Vf w. ff w x < e / card subA)  (x  S  B. ff w x > 1 - e / card subA)"
    by metis
  define pff where [abs_def]: "pff x = (w  subA. ff w x)" for x
  have pffR: "pff  R"
    unfolding pff_def using subA ff by (auto simp: intro: prod)
  moreover
  have pff01: "pff x  {0..1}" if t: "x  S" for x
  proof -
    have "0  pff x"
      using subA cardp t ff
      by (fastforce simp: pff_def field_split_simps sum_nonneg intro: prod_nonneg)
    moreover have "pff x  1"
      using subA cardp t ff 
      by (fastforce simp add: pff_def field_split_simps sum_nonneg intro: prod_mono [where g = "λx. 1", simplified])
    ultimately show ?thesis
      by auto
  qed
  moreover
  { fix v x
    assume v: "v  subA" and x: "x  Vf v" "x  S"
    from subA v have "pff x = ff v x * (w  subA - {v}. ff w x)"
      unfolding pff_def  by (metis prod.remove)
    also have "...  ff v x * 1"
    proof -
      have "i. i  subA - {v}  0  ff i x  ff i x  1"
        by (metis Diff_subset atLeastAtMost_iff ff image_subset_iff subA(1) subsetD x(2))
      moreover have "0  ff v x"
        using ff subA(1) v x(2) by fastforce
      ultimately show ?thesis
        by (metis mult_left_mono prod_mono [where g = "λx. 1", simplified])
    qed
    also have "... < e / card subA"
      using ff subA(1) v x by auto
    also have "...  e"
      using cardp e by (simp add: field_split_simps)
    finally have "pff x < e" .
  }
  then have "x. x  A  pff x < e"
    using A Vf subA by (metis UN_E contra_subsetD)
  moreover
  { fix x
    assume x: "x  B"
    then have "x  S"
      using B by auto
    have "1 - e  (1 - e / card subA)^card subA"
      using Bernoulli_inequality [of "-e / card subA" "card subA"] e cardp
      by (auto simp: field_simps)
    also have "... = (w  subA. 1 - e / card subA)"
      by (simp add: subA(2))
    also have "... < pff x"
    proof -
      have "i. i  subA  e / real (card subA)  1  1 - e / real (card subA) < ff i x"
        using e B  S ff subA(1) x by (force simp: field_split_simps)
      then show ?thesis
        using prod_mono_strict[of _ subA "λx. 1 - e / card subA" ] subA
        unfolding pff_def by (smt (verit, best) UN_E assms(3) subsetD)
    qed
    finally have "1 - e < pff x" .
  }
  ultimately show ?thesis by blast
qed

lemma (in function_ring_on) two:
  assumes A: "closed A" "A  S"
      and B: "closed B" "B  S"
      and disj: "A  B = {}"
      and e: "0 < e" "e < 1"
    shows "f  R. f ` S  {0..1}  (x  A. f x < e)  (x  B. f x > 1 - e)"
proof (cases "A  {}  B  {}")
  case True then show ?thesis
    using assms
    by (force simp flip: ex_in_conv intro!: two_special)
next
  case False 
  then consider "A={}" | "B={}" by force
  then show ?thesis
  proof cases
    case 1
    with e show ?thesis
      by (rule_tac x="λx. 1" in bexI) (auto simp: const)
  next
    case 2
    with e show ?thesis
      by (rule_tac x="λx. 0" in bexI) (auto simp: const)
  qed
qed

text‹The special case where termf is non-negative and terme<1/3
lemma (in function_ring_on) Stone_Weierstrass_special:
  assumes f: "continuous_on S f" and fpos: "x. x  S  f x  0"
      and e: "0 < e" "e < 1/3"
  shows "g  R. xS. ¦f x - g x¦ < 2*e"
proof -
  define n where "n = 1 + nat normf f / e"
  define A where "A j = {x  S. f x  (j - 1/3)*e}" for j :: nat
  define B where "B j = {x  S. f x  (j + 1/3)*e}" for j :: nat
  have ngt: "(n-1) * e  normf f"
    using e pos_divide_le_eq real_nat_ceiling_ge[of "normf f / e"]
    by (fastforce simp add: divide_simps n_def)
  moreover have "n1"
    by (simp_all add: n_def)
  ultimately have ge_fx: "(n-1) * e  f x" if "x  S" for x
    using f normf_upper that by fastforce
  have "closed S"
    by (simp add: compact compact_imp_closed)
  { fix j
    have "closed (A j)" "A j  S"
      using closed S continuous_on_closed_Collect_le [OF f continuous_on_const]
      by (simp_all add: A_def Collect_restrict)
    moreover have "closed (B j)" "B j  S"
      using closed S continuous_on_closed_Collect_le [OF continuous_on_const f]
      by (simp_all add: B_def Collect_restrict)
    moreover have "(A j)  (B j) = {}"
      using e by (auto simp: A_def B_def field_simps)
    ultimately have "f  R. f ` S  {0..1}  (x  A j. f x < e/n)  (x  B j. f x > 1 - e/n)"
      using e 1  n by (auto intro: two)
  }
  then obtain xf where xfR: "j. xf j  R" and xf01: "j. xf j ` S  {0..1}"
                   and xfA: "x j. x  A j  xf j x < e/n"
                   and xfB: "x j. x  B j  xf j x > 1 - e/n"
    by metis
  define g where [abs_def]: "g x = e * (in. xf i x)" for x
  have gR: "g  R"
    unfolding g_def by (fast intro: mult const sum xfR)
  have gge0: "x. x  S  g x  0"
    using e xf01 by (simp add: g_def zero_le_mult_iff image_subset_iff sum_nonneg)
  have A0: "A 0 = {}"
    using fpos e by (fastforce simp: A_def)
  have An: "A n = S"
    using e ngt n1 f normf_upper by (fastforce simp: A_def field_simps of_nat_diff)
  have Asub: "A j  A i" if "ij" for i j
    using e that by (force simp: A_def intro: order_trans)
  { fix t
    assume t: "t  S"
    define j where "j = (LEAST j. t  A j)"
    have jn: "j  n"
      using t An by (simp add: Least_le j_def)
    have Aj: "t  A j"
      using t An by (fastforce simp add: j_def intro: LeastI)
    then have Ai: "t  A i" if "ij" for i
      using Asub [OF that] by blast
    then have fj1: "f t  (j - 1/3)*e"
      by (simp add: A_def)
    then have Anj: "t  A i" if "i<j" for i
      using  Aj i<j not_less_Least by (fastforce simp add: j_def)
    have j1: "1  j"
      using A0 Aj j_def not_less_eq_eq by (fastforce simp add: j_def)
    then have Anj: "t  A (j-1)"
      using Least_le by (fastforce simp add: j_def)
    then have fj2: "(j - 4/3)*e < f t"
      using j1 t  by (simp add: A_def of_nat_diff)
    have xf_le1: "i. xf i t  1"
      using xf01 t by force
    have "g t = e * (in. xf i t)"
      by (simp add: g_def flip: distrib_left)
    also have "... = e * (i  {..<j}  {j..n}. xf i t)"
      by (simp add: ivl_disj_un_one(4) jn)
    also have "... = e * (i<j. xf i t) + e * (i=j..n. xf i t)"
      by (simp add: distrib_left ivl_disj_int sum.union_disjoint)
    also have "...  e*j + e * ((Suc n - j)*e/n)"
    proof (intro add_mono mult_left_mono)
      show "(i<j. xf i t)  j"
        by (rule sum_bounded_above [OF xf_le1, where A = "lessThan j", simplified])
      have "xf i t  e/n" if "ij" for i
        using xfA [OF Ai] that by (simp add: less_eq_real_def)
      then show "(i = j..n. xf i t)  real (Suc n - j) * e / real n"
        using sum_bounded_above [of "{j..n}" "λi. xf i t"]
        by fastforce 
    qed (use e in auto)
    also have "...  j*e + e*(n - j + 1)*e/n "
      using 1  n e  by (simp add: field_simps del: of_nat_Suc)
    also have "...  j*e + e*e"
      using 1  n e j1 by (simp add: field_simps del: of_nat_Suc)
    also have "... < (j + 1/3)*e"
      using e by (auto simp: field_simps)
    finally have gj1: "g t < (j + 1 / 3) * e" .
    have gj2: "(j - 4/3)*e < g t"
    proof (cases "2  j")
      case False
      then have "j=1" using j1 by simp
      with t gge0 e show ?thesis by force
    next
      case True
      then have "(j - 4/3)*e < (j-1)*e - e^2"
        using e by (auto simp: of_nat_diff algebra_simps power2_eq_square)
      also have "... < (j-1)*e - ((j - 1)/n) * e^2"
        using e True jn by (simp add: power2_eq_square field_simps)
      also have "... = e * (j-1) * (1 - e/n)"
        by (simp add: power2_eq_square field_simps)
      also have "...  e * (ij-2. xf i t)"
      proof -
        { fix i
          assume "i+2  j"
          then obtain d where "i+2+d = j"
            using le_Suc_ex that by blast
          then have "t  B i"
            using Anj e ge_fx [OF t] 1  n fpos [OF t] t
            unfolding A_def B_def
            by (auto simp add: field_simps of_nat_diff not_le intro: order_trans [of _ "e * 2 + e * d * 3 + e * i * 3"])
          then have "xf i t > 1 - e/n"
            by (rule xfB)
        } 
        moreover have "real (j - Suc 0) * (1 - e / real n)  real (card {..j - 2}) * (1 - e / real n)"
          using Suc_diff_le True by fastforce
        ultimately show ?thesis
          using e True by (auto intro: order_trans [OF _ sum_bounded_below [OF less_imp_le]])
      qed
      also have "...  g t"
        using jn e xf01 t
        by (auto intro!: Groups_Big.sum_mono2 simp add: g_def zero_le_mult_iff image_subset_iff sum_nonneg)
      finally show ?thesis .
    qed
    have "¦f t - g t¦ < 2 * e"
      using fj1 fj2 gj1 gj2 by (simp add: abs_less_iff field_simps)
  }
  then show ?thesis
    by (rule_tac x=g in bexI) (auto intro: gR)
qed

text‹The ``unpretentious'' formulation›
proposition (in function_ring_on) Stone_Weierstrass_basic:
  assumes f: "continuous_on S f" and e: "e > 0"
  shows "g  R. xS. ¦f x - g x¦ < e"
proof -
  have "g  R. xS. ¦(f x + normf f) - g x¦ < 2 * min (e/2) (1/4)"
  proof (rule Stone_Weierstrass_special)
    show "continuous_on S (λx. f x + normf f)"
      by (force intro: Limits.continuous_on_add [OF f Topological_Spaces.continuous_on_const])
    show "x. x  S  0  f x + normf f"
      using normf_upper [OF f] by force 
  qed (use e in auto)
  then obtain g where "g  R" "xS. ¦g x - (f x + normf f)¦ < e"
    by force
  then show ?thesis
    by (rule_tac x="λx. g x - normf f" in bexI) (auto simp: algebra_simps intro: diff const)
qed


theorem (in function_ring_on) Stone_Weierstrass:
  assumes f: "continuous_on S f"
  shows "FUNIV  R. LIM n sequentially. F n :> uniformly_on S f"
proof -
  define h where "h  λn::nat. SOME g. g  R  (xS. ¦f x - g x¦ < 1 / (1 + n))"
  show ?thesis
  proof
    { fix e::real
      assume e: "0 < e"
      then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e"
        by (auto simp: real_arch_inverse [of e])
      { fix n :: nat and x :: 'a and g :: "'a  real"
        assume n: "N  n"  "xS. ¦f x - g x¦ < 1 / (1 + real n)"
        assume x: "x  S"
        have "¬ real (Suc n) < inverse e"
          using N  n N using less_imp_inverse_less by force
        then have "1 / (1 + real n)  e"
          using e by (simp add: field_simps)
        then have "¦f x - g x¦ < e"
          using n(2) x by auto
      } 
      then have "F n in sequentially. xS. ¦f x - h n x¦ < e"
        unfolding h_def
        by (force intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]] eventually_sequentiallyI [of N])
    } 
    then show "uniform_limit S h f sequentially"
      unfolding uniform_limit_iff by (auto simp: dist_norm abs_minus_commute)
    show "h  UNIV  R"
      unfolding h_def by (force intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]])
  qed
qed

text‹A HOL Light formulation›
corollary Stone_Weierstrass_HOL:
  fixes R :: "('a::t2_space  real) set" and S :: "'a set"
  assumes "compact S"  "c. P(λx. c::real)"
          "f. P f  continuous_on S f"
          "f g. P(f)  P(g)  P(λx. f x + g x)"  "f g. P(f)  P(g)  P(λx. f x * g x)"
          "x y. x  S  y  S  x  y  f. P(f)  f x  f y"
          "continuous_on S f"
       "0 < e"
    shows "g. P(g)  (x  S. ¦f x - g x¦ < e)"
proof -
  interpret PR: function_ring_on "Collect P"
    by unfold_locales (use assms in auto)
  show ?thesis
    using PR.Stone_Weierstrass_basic [OF continuous_on S f 0 < e]
    by blast
qed


subsection ‹Polynomial functions›

inductive real_polynomial_function :: "('a::real_normed_vector  real)  bool" where
    linear: "bounded_linear f  real_polynomial_function f"
  | const: "real_polynomial_function (λx. c)"
  | add:   "real_polynomial_function f; real_polynomial_function g  real_polynomial_function (λx. f x + g x)"
  | mult:  "real_polynomial_function f; real_polynomial_function g  real_polynomial_function (λx. f x * g x)"

declare real_polynomial_function.intros [intro]

definitiontag important› polynomial_function :: "('a::real_normed_vector  'b::real_normed_vector)  bool"
  where
   "polynomial_function p  (f. bounded_linear f  real_polynomial_function (f o p))"

lemma real_polynomial_function_eq: "real_polynomial_function p = polynomial_function p"
unfolding polynomial_function_def
proof
  assume "real_polynomial_function p"
  then show " f. bounded_linear f  real_polynomial_function (f  p)"
  proof (induction p rule: real_polynomial_function.induct)
    case (linear h) then show ?case
      by (auto simp: bounded_linear_compose real_polynomial_function.linear)
  next
    case (const h) then show ?case
      by (simp add: real_polynomial_function.const)
  next
    case (add h) then show ?case
      by (force simp add: bounded_linear_def linear_add real_polynomial_function.add)
  next
    case (mult h) then show ?case
      by (force simp add: real_bounded_linear const real_polynomial_function.mult)
  qed
next
  assume [rule_format, OF bounded_linear_ident]: "f. bounded_linear f  real_polynomial_function (f  p)"
  then show "real_polynomial_function p"
    by (simp add: o_def)
qed

lemma polynomial_function_const [iff]: "polynomial_function (λx. c)"
  by (simp add: polynomial_function_def o_def const)

lemma polynomial_function_bounded_linear:
  "bounded_linear f  polynomial_function f"
  by (simp add: polynomial_function_def o_def bounded_linear_compose real_polynomial_function.linear)

lemma polynomial_function_id [iff]: "polynomial_function(λx. x)"
  by (simp add: polynomial_function_bounded_linear)

lemma polynomial_function_add [intro]:
    "polynomial_function f; polynomial_function g  polynomial_function (λx. f x + g x)"
  by (auto simp: polynomial_function_def bounded_linear_def linear_add real_polynomial_function.add o_def)

lemma polynomial_function_mult [intro]:
  assumes f: "polynomial_function f" and g: "polynomial_function g"
  shows "polynomial_function (λx. f x *R g x)"
proof -
  have "real_polynomial_function (λx. h (g x))" if "bounded_linear h" for h
    using g that unfolding polynomial_function_def o_def bounded_linear_def
    by (auto simp: real_polynomial_function_eq)
  moreover have "real_polynomial_function f"
    by (simp add: f real_polynomial_function_eq)
  ultimately show ?thesis
    unfolding polynomial_function_def bounded_linear_def o_def
    by (auto simp: linear.scaleR)
qed

lemma polynomial_function_cmul [intro]:
  assumes f: "polynomial_function f"
    shows "polynomial_function (λx. c *R f x)"
  by (rule polynomial_function_mult [OF polynomial_function_const f])

lemma polynomial_function_minus [intro]:
  assumes f: "polynomial_function f"
    shows "polynomial_function (λx. - f x)"
  using polynomial_function_cmul [OF f, of "-1"] by simp

lemma polynomial_function_diff [intro]:
    "polynomial_function f; polynomial_function g  polynomial_function (λx. f x - g x)"
  unfolding add_uminus_conv_diff [symmetric]
  by (metis polynomial_function_add polynomial_function_minus)

lemma polynomial_function_sum [intro]:
    "finite I; i. i  I  polynomial_function (λx. f x i)  polynomial_function (λx. sum (f x) I)"
by (induct I rule: finite_induct) auto

lemma real_polynomial_function_minus [intro]:
    "real_polynomial_function f  real_polynomial_function (λx. - f x)"
  using polynomial_function_minus [of f]
  by (simp add: real_polynomial_function_eq)

lemma real_polynomial_function_diff [intro]:
    "real_polynomial_function f; real_polynomial_function g  real_polynomial_function (λx. f x - g x)"
  using polynomial_function_diff [of f]
  by (simp add: real_polynomial_function_eq)

lemma real_polynomial_function_divide [intro]:
  assumes "real_polynomial_function p" shows "real_polynomial_function (λx. p x / c)"
proof -
  have "real_polynomial_function (λx. p x * Fields.inverse c)"
    using assms by auto
  then show ?thesis
    by (simp add: divide_inverse)
qed

lemma real_polynomial_function_sum [intro]:
    "finite I; i. i  I  real_polynomial_function (λx. f x i)  real_polynomial_function (λx. sum (f x) I)"
  using polynomial_function_sum [of I f]
  by (simp add: real_polynomial_function_eq)

lemma real_polynomial_function_prod [intro]:
  "finite I; i. i  I  real_polynomial_function (λx. f x i)  real_polynomial_function (λx. prod (f x) I)"
  by (induct I rule: finite_induct) auto

lemma real_polynomial_function_gchoose:
  obtains p where "real_polynomial_function p" "x. x gchoose r = p x"
proof
  show "real_polynomial_function (λx. (i = 0..<r. x - real i) / fact r)"
    by force
qed (simp add: gbinomial_prod_rev)

lemma real_polynomial_function_power [intro]:
    "real_polynomial_function f  real_polynomial_function (λx. f x^n)"
  by (induct n) (simp_all add: const mult)

lemma real_polynomial_function_compose [intro]:
  assumes f: "polynomial_function f" and g: "real_polynomial_function g"
    shows "real_polynomial_function (g o f)"
  using g
proof (induction g rule: real_polynomial_function.induct)
  case (linear f)
  then show ?case
    using f polynomial_function_def by blast
next
  case (add f g)
  then show ?case
    using f add by (auto simp: polynomial_function_def)
next
  case (mult f g)
  then show ?case
  using f mult by (auto simp: polynomial_function_def)
qed auto

lemma polynomial_function_compose [intro]:
  assumes f: "polynomial_function f" and g: "polynomial_function g"
    shows "polynomial_function (g o f)"
  using g real_polynomial_function_compose [OF f]
  by (auto simp: polynomial_function_def o_def)

lemma sum_max_0:
  fixes x::real (*in fact "'a::comm_ring_1"*)
  shows "(imax m n. x^i * (if i  m then a i else 0)) = (im. x^i * a i)"
proof -
  have "(imax m n. x^i * (if i  m then a i else 0)) = (imax m n. (if i  m then x^i * a i else 0))"
    by (auto simp: algebra_simps intro: sum.cong)
  also have "... = (im. (if i  m then x^i * a i else 0))"
    by (rule sum.mono_neutral_right) auto
  also have "... = (im. x^i * a i)"
    by (auto simp: algebra_simps intro: sum.cong)
  finally show ?thesis .
qed

lemma real_polynomial_function_imp_sum:
  assumes "real_polynomial_function f"
    shows "a n::nat. f = (λx. in. a i * x^i)"
using assms
proof (induct f)
  case (linear f)
  then obtain c where f: "f = (λx. x * c)"
    by (auto simp add: real_bounded_linear)
  have "x * c = (i1. (if i = 0 then 0 else c) * x^i)" for x
    by (simp add: mult_ac)
  with f show ?case
    by fastforce
next
  case (const c)
  have "c = (i0. c * x^i)" for x
    by auto
  then show ?case
    by fastforce
  case (add f1 f2)
  then obtain a1 n1 a2 n2 where
    "f1 = (λx. in1. a1 i * x^i)" "f2 = (λx. in2. a2 i * x^i)"
    by auto
  then have "f1 x + f2 x = (imax n1 n2. ((if i  n1 then a1 i else 0) + (if i  n2 then a2 i else 0)) * x^i)" 
      for x
    using sum_max_0 [where m=n1 and n=n2] sum_max_0 [where m=n2 and n=n1]
    by (simp add: sum.distrib algebra_simps max.commute)
  then show ?case
    by force
  case (mult f1 f2)
  then obtain a1 n1 a2 n2 where
    "f1 = (λx. in1. a1 i * x^i)" "f2 = (λx. in2. a2 i * x^i)"
    by auto
  then obtain b1 b2 where
    "f1 = (λx. in1. b1 i * x^i)" "f2 = (λx. in2. b2 i * x^i)"
    "b1 = (λi. if in1 then a1 i else 0)" "b2 = (λi. if in2 then a2 i else 0)"
    by auto
  then have "f1 x * f2 x = (in1 + n2. (ki. b1 k * b2 (i - k)) * x ^ i)" for x
    using polynomial_product [of n1 b1 n2 b2] by (simp add: Set_Interval.atLeast0AtMost)
  then show ?case
    by force
qed

lemma real_polynomial_function_iff_sum:
     "real_polynomial_function f  (a n. f = (λx. in. a i * x^i))"  (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    by (metis real_polynomial_function_imp_sum)
next
  assume ?rhs then show ?lhs
    by (auto simp: linear mult const real_polynomial_function_power real_polynomial_function_sum)
qed

lemma polynomial_function_iff_Basis_inner:
  fixes f :: "'a::real_normed_vector  'b::euclidean_space"
  shows "polynomial_function f  (bBasis. real_polynomial_function (λx. inner (f x) b))"
        (is "?lhs = ?rhs")
unfolding polynomial_function_def
proof (intro iffI allI impI)
  assume "h. bounded_linear h  real_polynomial_function (h  f)"
  then show ?rhs
    by (force simp add: bounded_linear_inner_left o_def)
next
  fix h :: "'b  real"
  assume rp: "bBasis. real_polynomial_function (λx. f x  b)" and h: "bounded_linear h"
  have "real_polynomial_function (h  (λx. bBasis. (f x  b) *R b))"
    using rp
    by (force simp: real_polynomial_function_eq polynomial_function_mult 
              intro!: real_polynomial_function_compose [OF _  linear [OF h]])
  then show "real_polynomial_function (h  f)"
    by (simp add: euclidean_representation_sum_fun)
qed

subsection ‹Stone-Weierstrass theorem for polynomial functions›

text‹First, we need to show that they are continuous, differentiable and separable.›

lemma continuous_real_polymonial_function:
  assumes "real_polynomial_function f"
    shows "continuous (at x) f"
using assms
by (induct f) (auto simp: linear_continuous_at)

lemma continuous_polymonial_function:
  fixes f :: "'a::real_normed_vector  'b::euclidean_space"
  assumes "polynomial_function f"
    shows "continuous (at x) f"
proof (rule euclidean_isCont)
  show "b. b  Basis  isCont (λx. (f x  b) *R b) x"
  using assms continuous_real_polymonial_function
  by (force simp: polynomial_function_iff_Basis_inner intro: isCont_scaleR)
qed

lemma continuous_on_polymonial_function:
  fixes f :: "'a::real_normed_vector  'b::euclidean_space"
  assumes "polynomial_function f"
    shows "continuous_on S f"
  using continuous_polymonial_function [OF assms] continuous_at_imp_continuous_on
  by blast

lemma has_real_derivative_polynomial_function:
  assumes "real_polynomial_function p"
    shows "p'. real_polynomial_function p' 
                 (x. (p has_real_derivative (p' x)) (at x))"
using assms
proof (induct p)
  case (linear p)
  then show ?case
    by (force simp: real_bounded_linear const intro!: derivative_eq_intros)
next
  case (const c)
  show ?case
    by (rule_tac x="λx. 0" in exI) auto
  case (add f1 f2)
  then obtain p1 p2 where
    "real_polynomial_function p1" "x. (f1 has_real_derivative p1 x) (at x)"
    "real_polynomial_function p2" "x. (f2 has_real_derivative p2 x) (at x)"
    by auto
  then show ?case
    by (rule_tac x="λx. p1 x + p2 x" in exI) (auto intro!: derivative_eq_intros)
  case (mult f1 f2)
  then obtain p1 p2 where
    "real_polynomial_function p1" "x. (f1 has_real_derivative p1 x) (at x)"
    "real_polynomial_function p2" "x. (f2 has_real_derivative p2 x) (at x)"
    by auto
  then show ?case
    using mult
    by (rule_tac x="λx. f1 x * p2 x + f2 x * p1 x" in exI) (auto intro!: derivative_eq_intros)
qed

lemma has_vector_derivative_polynomial_function:
  fixes p :: "real  'a::euclidean_space"
  assumes "polynomial_function p"
  obtains p' where "polynomial_function p'" "x. (p has_vector_derivative (p' x)) (at x)"
proof -
  { fix b :: 'a
    assume "b  Basis"
    then
    obtain p' where p': "real_polynomial_function p'" and pd: "x. ((λx. p x  b) has_real_derivative p' x) (at x)"
      using assms [unfolded polynomial_function_iff_Basis_inner] has_real_derivative_polynomial_function
      by blast
    have "polynomial_function (λx. p' x *R b)"
      using b  Basis p' const [where 'a=real and c=0]
      by (simp add: polynomial_function_iff_Basis_inner inner_Basis)
    then have "q. polynomial_function q  (x. ((λu. (p u  b) *R b) has_vector_derivative q x) (at x))"
      by (fastforce intro: derivative_eq_intros pd)
  }
  then obtain qf where qf:
      "b. b  Basis  polynomial_function (qf b)"
      "b x. b  Basis  ((λu. (p u  b) *R b) has_vector_derivative qf b x) (at x)"
    by metis
  show ?thesis
  proof
    show "x. (p has_vector_derivative (bBasis. qf b x)) (at x)"
      apply (subst euclidean_representation_sum_fun [of p, symmetric])
      by (auto intro: has_vector_derivative_sum qf)
  qed (force intro: qf)
qed

lemma real_polynomial_function_separable:
  fixes x :: "'a::euclidean_space"
  assumes "x  y" shows "f. real_polynomial_function f  f x  f y"
proof -
  have "real_polynomial_function (λu. bBasis. (inner (x-u) b)^2)"
  proof (rule real_polynomial_function_sum)
    show "i. i  Basis  real_polynomial_function (λu. ((x - u)  i)2)"
      by (auto simp: algebra_simps real_polynomial_function_diff const linear bounded_linear_inner_left)
  qed auto
  moreover have "(bBasis. ((x - y)  b)2)  0"
    using assms by (force simp add: euclidean_eq_iff [of x y] sum_nonneg_eq_0_iff algebra_simps)
  ultimately show ?thesis
    by auto
qed

lemma Stone_Weierstrass_real_polynomial_function:
  fixes f :: "'a::euclidean_space  real"
  assumes "compact S" "continuous_on S f" "0 < e"
  obtains g where "real_polynomial_function g" "x. x  S  ¦f x - g x¦ < e"
proof -
  interpret PR: function_ring_on "Collect real_polynomial_function"
  proof unfold_locales
  qed (use assms continuous_on_polymonial_function real_polynomial_function_eq 
       in auto intro: real_polynomial_function_separable)
  show ?thesis
    using PR.Stone_Weierstrass_basic [OF continuous_on S f 0 < e] that by blast
qed

theorem Stone_Weierstrass_polynomial_function:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes S: "compact S"
      and f: "continuous_on S f"
      and e: "0 < e"
    shows "g. polynomial_function g  (x  S. norm(f x - g x) < e)"
proof -
  { fix b :: 'b
    assume "b  Basis"
    have "p. real_polynomial_function p  (x  S. ¦f x  b - p x¦ < e / DIM('b))"
    proof (rule Stone_Weierstrass_real_polynomial_function [OF S _, of "λx. f x  b" "e / card Basis"])
      show "continuous_on S (λx. f x  b)"
        using f by (auto intro: continuous_intros)
    qed (use e in auto)
  }
  then obtain pf where pf:
      "b. b  Basis  real_polynomial_function (pf b)  (x  S. ¦f x  b - pf b x¦ < e / DIM('b))"
    by metis
  let ?g = "λx. bBasis. pf b x *R b"
  { fix x
    assume "x  S"
    have "norm (bBasis. (f x  b) *R b - pf b x *R b)  (bBasis. norm ((f x  b) *R b - pf b x *R b))"
      by (rule norm_sum)
    also have "... < of_nat DIM('b) * (e / DIM('b))"
    proof (rule sum_bounded_above_strict)
      show "i. i  Basis  norm ((f x  i) *R i - pf i x *R i) < e / real DIM('b)"
        by (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf x  S)
    qed (rule DIM_positive)
    also have "... = e"
      by (simp add: field_simps)
    finally have "norm (bBasis. (f x  b) *R b - pf b x *R b) < e" .
  }
  then have "xS. norm ((bBasis. (f x  b) *R b) - ?g x) < e"
    by (auto simp flip: sum_subtractf)
  moreover
  have "polynomial_function ?g"
    using pf by (simp add: polynomial_function_sum polynomial_function_mult real_polynomial_function_eq)
  ultimately show ?thesis
    using euclidean_representation_sum_fun [of f] by (metis (no_types, lifting))
qed

proposition Stone_Weierstrass_uniform_limit:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes S: "compact S"
    and f: "continuous_on S f"
  obtains g where "uniform_limit S g f sequentially" "n. polynomial_function (g n)"
proof -
  have pos: "inverse (Suc n) > 0" for n by auto
  obtain g where g: "n. polynomial_function (g n)" "x n. x  S  norm(f x - g n x) < inverse (Suc n)"
    using Stone_Weierstrass_polynomial_function[OF S f pos]
    by metis
  have "uniform_limit S g f sequentially"
  proof (rule uniform_limitI)
    fix e::real assume "0 < e"
    with LIMSEQ_inverse_real_of_nat have "F n in sequentially. inverse (Suc n) < e"
      by (rule order_tendstoD)
    moreover have "F n in sequentially. xS. dist (g n x) (f x) < inverse (Suc n)"
      using g by (simp add: dist_norm norm_minus_commute)
    ultimately show "F n in sequentially. xS. dist (g n x) (f x) < e"
      by (eventually_elim) auto
  qed
  then show ?thesis using g(1) ..
qed


subsection‹Polynomial functions as paths›

text‹One application is to pick a smooth approximation to a path,
or just pick a smooth path anyway in an open connected set›

lemma path_polynomial_function:
    fixes g  :: "real  'b::euclidean_space"
    shows "polynomial_function g  path g"
  by (simp add: path_def continuous_on_polymonial_function)

lemma path_approx_polynomial_function:
    fixes g :: "real  'b::euclidean_space"
    assumes "path g" "0 < e"
    obtains p where "polynomial_function p" "pathstart p = pathstart g" "pathfinish p = pathfinish g"
                    "t. t  {0..1}  norm(p t - g t) < e"
proof -
  obtain q where poq: "polynomial_function q" and noq: "x. x  {0..1}  norm (g x - q x) < e/4"
    using Stone_Weierstrass_polynomial_function [of "{0..1}" g "e/4"] assms
    by (auto simp: path_def)
  define pf where "pf  λt. q t + (g 0 - q 0) + t *R (g 1 - q 1 - (g 0 - q 0))"
  show thesis
  proof 
    show "polynomial_function pf"
      by (force simp add: poq pf_def)
    show "norm (pf t - g t) < e"
      if "t  {0..1}" for t
    proof -
      have *: "norm (((q t - g t) + (g 0 - q 0)) + (t *R (g 1 - q 1) + t *R (q 0 - g 0))) < (e/4 + e/4) + (e/4+e/4)"
      proof (intro Real_Vector_Spaces.norm_add_less)
        show "norm (q t - g t) < e / 4"
          by (metis noq norm_minus_commute that)
        show "norm (t *R (g 1 - q 1)) < e / 4"
          using noq that le_less_trans [OF mult_left_le_one_le noq]
          by auto
        show "norm (t *R (q 0 - g 0)) < e / 4"
          using noq that le_less_trans [OF mult_left_le_one_le noq]
          by simp (metis norm_minus_commute order_refl zero_le_one)
      qed (use noq norm_minus_commute that in auto)
      then show ?thesis
        by (auto simp add: algebra_simps pf_def)
    qed
  qed (auto simp add: path_defs pf_def)
qed

proposition connected_open_polynomial_connected:
  fixes S :: "'a::euclidean_space set"
  assumes S: "open S" "connected S"
      and "x  S" "y  S"
    shows "g. polynomial_function g  path_image g  S  pathstart g = x  pathfinish g = y"
proof -
  have "path_connected S" using assms
    by (simp add: connected_open_path_connected)
  with x  S y  S obtain p where p: "path p" "path_image p  S" "pathstart p = x" "pathfinish p = y"
    by (force simp: path_connected_def)
  have "e. 0 < e  (x  path_image p. ball x e  S)"
  proof (cases "S = UNIV")
    case True then show ?thesis
      by (simp add: gt_ex)
  next
    case False
    show ?thesis
    proof (intro exI conjI ballI)
      show "x. x  path_image p  ball x (setdist (path_image p) (-S))  S"
        using setdist_le_dist [of _ "path_image p" _ "-S"] by fastforce
      show "0 < setdist (path_image p) (- S)"
        using S p False
        by (fastforce simp add: setdist_gt_0_compact_closed compact_path_image open_closed)
    qed
  qed
  then obtain e where "0 < e"and eb: "x. x  path_image p  ball x e  S"
    by auto
  obtain pf where "polynomial_function pf" and pf: "pathstart pf = pathstart p" "pathfinish pf = pathfinish p"
                   and pf_e: "t. t  {0..1}  norm(pf t - p t) < e"
    using path_approx_polynomial_function [OF path p 0 < e] by blast
  show ?thesis 
  proof (intro exI conjI)
    show "polynomial_function pf"
      by fact
    show "pathstart pf = x" "pathfinish pf = y"
      by (simp_all add: p pf)
    show "path_image pf  S"
      unfolding path_image_def
    proof clarsimp
      fix x'::real
      assume "0  x'" "x'  1"
      then have "dist (p x') (pf x') < e"
        by (metis atLeastAtMost_iff dist_commute dist_norm pf_e)
      then show "pf x'  S"
        by (metis 0  x' x'  1 atLeastAtMost_iff eb imageI mem_ball path_image_def subset_iff)
    qed
  qed
qed

lemma differentiable_componentwise_within:
   "f differentiable (at a within S) 
    (i  Basis. (λx. f x  i) differentiable at a within S)"
proof -
  { assume "iBasis. D. ((λx. f x  i) has_derivative D) (at a within S)"
    then obtain f' where f':
           "i. i  Basis  ((λx. f x  i) has_derivative f' i) (at a within S)"
      by metis
    have eq: "(λx. (jBasis. f' j x *R j)  i) = f' i" if "i  Basis" for i
      using that by (simp add: inner_add_left inner_add_right)
    have "D. iBasis. ((λx. f x  i) has_derivative (λx. D x  i)) (at a within S)"
      apply (rule_tac x="λx::'a. (jBasis. f' j x *R j) :: 'b" in exI)
      apply (simp add: eq f')
      done
  }
  then show ?thesis
    apply (simp add: differentiable_def)
    using has_derivative_componentwise_within
    by blast
qed

lemma polynomial_function_inner [intro]:
  fixes i :: "'a::euclidean_space"
  shows "polynomial_function g  polynomial_function (λx. g x  i)"
  apply (subst euclidean_representation [where x=i, symmetric])
  apply (force simp: inner_sum_right polynomial_function_iff_Basis_inner polynomial_function_sum)
  done

text‹ Differentiability of real and vector polynomial functions.›

lemma differentiable_at_real_polynomial_function:
   "real_polynomial_function f  f differentiable (at a within S)"
  by (induction f rule: real_polynomial_function.induct)
     (simp_all add: bounded_linear_imp_differentiable)

lemma differentiable_on_real_polynomial_function:
   "real_polynomial_function p  p differentiable_on S"
by (simp add: differentiable_at_imp_differentiable_on differentiable_at_real_polynomial_function)

lemma differentiable_at_polynomial_function:
  fixes f :: "_  'a::euclidean_space"
  shows "polynomial_function f  f differentiable (at a within S)"
  by (metis differentiable_at_real_polynomial_function polynomial_function_iff_Basis_inner differentiable_componentwise_within)

lemma differentiable_on_polynomial_function:
  fixes f :: "_  'a::euclidean_space"
  shows "polynomial_function f  f differentiable_on S"
by (simp add: differentiable_at_polynomial_function differentiable_on_def)

lemma vector_eq_dot_span:
  assumes "x  span B" "y  span B" and i: "i. i  B  i  x = i  y"
  shows "x = y"
proof -
  have "i. i  B  orthogonal (x - y) i"
    by (simp add: i inner_commute inner_diff_right orthogonal_def)
  moreover have "x - y  span B"
    by (simp add: assms span_diff)
  ultimately have "x - y = 0"
    using orthogonal_to_span orthogonal_self by blast
    then show ?thesis by simp
qed

lemma orthonormal_basis_expand:
  assumes B: "pairwise orthogonal B"
      and 1: "i. i  B  norm i = 1"
      and "x  span B"
      and "finite B"
    shows "(iB. (x  i) *R i) = x"
proof (rule vector_eq_dot_span [OF _ x  span B])
  show "(iB. (x  i) *R i)  span B"
    by (simp add: span_clauses span_sum)
  show "i  (iB. (x  i) *R i) = i  x" if "i  B" for i
  proof -
    have [simp]: "i  j = (if j = i then 1 else 0)" if "j  B" for j
      using B 1 that i  B
      by (force simp: norm_eq_1 orthogonal_def pairwise_def)
    have "i  (iB. (x  i) *R i) = (jB. x  j * (i  j))"
      by (simp add: inner_sum_right)
    also have "... = (jB. if j = i then x  i else 0)"
      by (rule sum.cong; simp)
    also have "... = i  x"
      by (simp add: finite B that inner_commute)
    finally show ?thesis .
  qed
qed


theorem Stone_Weierstrass_polynomial_function_subspace:
  fixes f :: "'a::euclidean_space  'b::euclidean_space"
  assumes "compact S"
      and contf: "continuous_on S f"
      and "0 < e"
      and "subspace T" "f ` S  T"
    obtains g where "polynomial_function g" "g ` S  T"
                    "x. x  S  norm(f x - g x) < e"
proof -
  obtain B where "B  T" and orthB: "pairwise orthogonal B"
             and B1: "x. x  B  norm x = 1"
             and "independent B" and cardB: "card B = dim T"
             and spanB: "span B = T"
    using orthonormal_basis_subspace subspace T by metis
  then have "finite B"
    by (simp add: independent_imp_finite)
  then obtain n::nat and b where "B = b ` {i. i < n}" "inj_on b {i. i < n}"
    using finite_imp_nat_seg_image_inj_on by metis
  with cardB have "n = card B" "dim T = n"
    by (auto simp: card_image)
  have fx: "(iB. (f x  i) *R i) = f x" if "x  S" for x
    by (metis (no_types, lifting) B1 finite B assms(5) image_subset_iff orthB orthonormal_basis_expand spanB sum.cong that)
  have cont: "continuous_on S (λx. iB. (f x  i) *R i)"
    by (intro continuous_intros contf)
  obtain g where "polynomial_function g"
             and g: "x. x  S  norm ((iB. (f x  i) *R i) - g x) < e / (n+2)"
    using Stone_Weierstrass_polynomial_function [OF compact S cont, of "e / real (n + 2)"] 0 < e
    by auto
  with fx have g: "x. x  S  norm (f x - g x) < e / (n+2)"
    by auto
  show ?thesis
  proof
    show "polynomial_function (λx. iB. (g x  i) *R i)"
      using polynomial_function g by (force intro: finite B)
    show "(λx. iB. (g x  i) *R i) ` S  T"
      using B  T
      by (blast intro: subspace_sum subspace_mul subspace T)
    show "norm (f x - (iB. (g x  i) *R i)) < e" if "x  S" for x
    proof -
      have orth': "pairwise (λi j. orthogonal ((f x  i) *R i - (g x  i) *R i)
                                              ((f x  j) *R j - (g x  j) *R j)) B"
        by (auto simp: orthogonal_def inner_diff_right inner_diff_left intro: pairwise_mono [OF orthB])
      then have "(norm (iB. (f x  i) *R i - (g x  i) *R i))2 =
                 (iB. (norm ((f x  i) *R i - (g x  i) *R i))2)"
        by (simp add:  norm_sum_Pythagorean [OF finite B orth'])
      also have "... = (iB. (norm (((f x - g x)  i) *R i))2)"
        by (simp add: algebra_simps)
      also have "...  (iB. (norm (f x - g x))2)"
      proof -
        have "i. i  B  ((f x - g x)  i)2  (norm (f x - g x))2"
          by (metis B1 Cauchy_Schwarz_ineq inner_commute mult.left_neutral norm_eq_1 power2_norm_eq_inner)
        then show ?thesis
          by (intro sum_mono) (simp add: sum_mono B1)
      qed
      also have "... = n * norm (f x - g x)^2"
        by (simp add: n = card B)
      also have "...  n * (e / (n+2))^2"
      proof (rule mult_left_mono)
        show "(norm (f x - g x))2  (e / real (n + 2))2"
          by (meson dual_order.order_iff_strict g norm_ge_zero power_mono that)
      qed auto
      also have "...  e^2 / (n+2)"
        using 0 < e by (simp add: divide_simps power2_eq_square)
      also have "... < e^2"
        using 0 < e by (simp add: divide_simps)
      finally have "(norm (iB. (f x  i) *R i - (g x  i) *R i))2 < e^2" .
      then have "(norm (iB. (f x  i) *R i - (g x  i) *R i)) < e"
        by (simp add: 0 < e norm_lt_square power2_norm_eq_inner)
      then show ?thesis
        using fx that by (simp add: sum_subtractf)
    qed
  qed
qed


hide_fact linear add mult const

end