# Theory Weierstrass_Theorems

theory Weierstrass_Theorems
imports Derivative
```section ‹The Bernstein-Weierstrass and Stone-Weierstrass Theorems›

text‹By L C Paulson (2015)›

theory Weierstrass_Theorems
imports Uniform_Limit Path_Connected Derivative
begin

subsection ‹Bernstein polynomials›

definition 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"

lemma Bernstein_pos: "⟦0 < x; x < 1; k ≤ n⟧ ⟹ 0 < Bernstein n k x"

lemma sum_Bernstein [simp]: "(∑ k = 0..n. Bernstein n k x) = 1"
using binomial_ring [of x "1-x" n]

lemma binomial_deriv1:
"(∑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)"
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)+
done

lemma binomial_deriv2:
"(∑k=0..n. (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]: "(∑k = 0..n. real k * Bernstein n k x) = of_nat n * x"
apply (subst binomial_deriv1 [of n x "1-x", simplified, symmetric])
apply (auto simp: Bernstein_def algebra_simps realpow_num_eq_if intro!: sum.cong)
done

lemma sum_kk_Bernstein [simp]: "(∑ k = 0..n. real k * (real k - 1) * Bernstein n k x) = real n * (real n - 1) * x⇧2"
proof -
have "(∑ k = 0..n. real k * (real k - 1) * Bernstein n k x) = real_of_nat n * real_of_nat (n - Suc 0) * x⇧2"
apply (subst binomial_deriv2 [of n x "1-x", simplified, symmetric])
apply (rule sum.cong [OF refl])
apply (simp add: Bernstein_def power2_eq_square algebra_simps)
apply (rename_tac k)
apply (subgoal_tac "k = 0 ∨ k = 1 ∨ (∃k'. k = Suc (Suc k'))")
apply (force simp add: field_simps of_nat_Suc power2_eq_square)
by presburger
also have "... = n * (n - 1) * x⇧2"
by auto
finally show ?thesis
by auto
qed

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

lemma 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 - (∑k = 0..n. 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"
then have Mge0: "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 (nat⌈4*M/(e*d⇧2)⌉) ≤ n" and x: "0 ≤ x" "x ≤ 1"
have "0 < n" using n by simp
have ed0: "- (e * d⇧2) < 0"
using e ‹0<d› by simp
also have "... ≤ M * 4"
using ‹0≤M› by simp
finally have [simp]: "real_of_int (nat ⌈4 * M / (e * d⇧2)⌉) = real_of_int ⌈4 * M / (e * d⇧2)⌉"
using ‹0≤M› e ‹0<d›
have "4*M/(e*d⇧2) + 1 ≤ real (Suc (nat⌈4*M/(e*d⇧2)⌉))"
also have "... ≤ real n"
using n by (simp add: of_nat_Suc field_simps)
finally have nbig: "4*M/(e*d⇧2) + 1 ≤ real n" .
have sum_bern: "(∑k = 0..n. (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"
have "(∑ k = 0..n. (k - n * x)⇧2 * Bernstein n k x) = n * x * (1 - x)"
apply (simp add: sum_distrib_left [symmetric] mult.assoc)
done
then have "(∑ k = 0..n. (k - n * x)⇧2 * Bernstein n k x)/n^2 = x * (1 - x) / n"
then show ?thesis
using n by (simp add: sum_divide_distrib divide_simps mult.commute power2_commute)
qed
{ fix k
assume k: "k ≤ n"
then have kn: "0 ≤ k / n" "k / n ≤ 1"
by (auto simp: divide_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 / d⇧2 * (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 / d⇧2 * (x - k/n)⇧2)"
using Mge0 d by simp
finally show ?thesis by simp
next
case ged
then have dle: "d⇧2 ≤ (x - k/n)⇧2"
by (metis d(1) less_eq_real_def power2_abs power_mono)
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 / d⇧2)"
apply simp
apply (rule Rings.ordered_semiring_class.mult_left_mono [of 1 "((x - k/n)⇧2 / d⇧2)", simplified])
using dle ‹d>0› ‹M≥0› by auto
also have "... ≤ e/2 + 2 * M / d⇧2 * (x - k/n)⇧2"
using e  by simp
finally show ?thesis .
qed
} note * = this
have "¦f x - (∑ k = 0..n. f(k / n) * Bernstein n k x)¦ ≤ ¦∑ k = 0..n. (f x - f(k / n)) * Bernstein n k x¦"
by (simp add: sum_subtractf sum_distrib_left [symmetric] algebra_simps)
also have "... ≤ (∑ k = 0..n. (e/2 + (2 * M / d⇧2) * (x - k / n)⇧2) * Bernstein n k x)"
apply (rule order_trans [OF sum_abs sum_mono])
using *
apply (simp add: abs_mult Bernstein_nonneg x mult_right_mono)
done
also have "... ≤ e/2 + (2 * M) / (d⇧2 * n)"
apply (simp only: sum.distrib Rings.semiring_class.distrib_right sum_distrib_left [symmetric] mult.assoc sum_bern)
using ‹d>0› x
apply (simp add: divide_simps Mge0 mult_le_one mult_left_le)
done
also have "... < e"
using ‹d>0› nbig e ‹n>0›
using ed0 by linarith
finally have "¦f x - (∑k = 0..n. 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  http://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 ⟹ ∃f∈R. 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"

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"

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)

definition normf :: "('a::t2_space ⇒ real) ⇒ real"
where "normf f ≡ SUP x:S. ¦f x¦"

lemma normf_upper: "⟦continuous_on S f; x ∈ S⟧ ⟹ ¦f x¦ ≤ normf f"
apply (rule cSUP_upper, assumption)
by (simp add: bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs)

lemma normf_least: "S ≠ {} ⟹ (⋀x. x ∈ S ⟹ ¦f x¦ ≤ M) ⟹ normf f ≤ M"

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"
have "h t ≠ h t0"
then have "h t ≠ 0"
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"
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 = {x∈S. 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 = {x∈S. 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
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 divide_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
apply (simp add: p_def divide_simps sum_nonneg)
apply (rule sum_nonneg)
using pf01 by force
moreover have "p x ≤ 1"
using subU cardp t
apply (simp add: p_def divide_simps sum_nonneg)
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)))"
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 = {x∈S. 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 = {x∈S. p x < δ/2}"
by blast
define k where "k = nat⌊1/δ⌋ + 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+δ)/δ"
also have "... < 2/δ"
using δ01 by (auto simp: divide_simps)
finally have k2δ: "k < 2/δ" .
have "1/δ < k"
using δ01 unfolding k_def by linarith
with δ01 k2δ have kδ: "1 < k*δ" "k*δ < 2"
by (auto simp: divide_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"]
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"
with kδ 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›
apply simp
apply (simp only: times_divide_eq_right [symmetric])
apply (rule mult_left_mono [of "1::real", simplified])
apply (rule zero_le_power)
using ptn_le by linarith
also have "... ≤ (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + (p t)^n) ^ (k^n)"
apply (rule mult_left_mono [OF Bernoulli_inequality [of "p t ^ n" "k^n"]])
using ‹k>0› ptn_pos ptn_le
apply (auto simp: power_mult_distrib)
done
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 power_mult_distrib [symmetric])
also have "... ≤ (1/(k * (p t))^n) * 1"
apply (rule mult_left_mono [OF power_le_one])
using pt_pos ‹k>0› p01 power_le_one t apply auto
done
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: "⋀e. e>0 ⟹ (k * δ / 2)^NN e < e"
apply (subst Transcendental.ln_less_cancel_iff [symmetric])
prefer 3 apply (subst ln_realpow)
using ‹k>0› ‹δ>0› NN  kδ
done
have NN0: "(1/(k*δ)) ^ (NN e) < e" if "e>0" for e
proof -
have "0 < ln (real k) + ln δ"
using δ01(1) ‹0 < k› kδ(1) ln_gt_zero ln_mult by fastforce
then have "real (NN e) * ln (1 / (real k * δ)) < ln e"
using kδ(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 ⟹ ∃f∈R. 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 @{term A} and @{term B} 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
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
apply (simp add: pff_def divide_simps sum_nonneg)
apply (rule Groups_Big.linordered_semidom_class.prod_nonneg)
using ff by fastforce
moreover have "pff x ≤ 1"
using subA cardp t
apply (simp add: pff_def divide_simps sum_nonneg)
apply (rule prod_mono [where g = "λx. 1", simplified])
using ff by fastforce
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"
apply (rule Rings.ordered_semiring_class.mult_left_mono)
apply (rule prod_mono [where g = "λx. 1", simplified])
using ff [THEN conjunct2, THEN conjunct1] v subA x
apply auto
apply (meson atLeastAtMost_iff contra_subsetD imageI)
apply (meson atLeastAtMost_iff contra_subsetD image_eqI)
using atLeastAtMost_iff by blast
also have "... < e / card subA"
using ff [THEN conjunct2, THEN conjunct2, THEN conjunct1] v subA x
by auto
also have "... ≤ e"
using cardp e by (simp add: divide_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)"
also have "... < pff x"
apply (rule prod_mono_strict [where f = "λx. 1 - e / card subA", simplified])
apply (intro ballI conjI)
using e apply (force simp: divide_simps)
using ff [THEN conjunct2, THEN conjunct2, THEN conjunct2] subA B x
apply blast
done
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
apply safe
apply (force simp add: intro!: two_special)
done
next
case False with e show ?thesis
apply simp
apply (erule disjE)
apply (rule_tac [2] x="λx. 0" in bexI)
apply (rule_tac x="λx. 1" in bexI)
apply (auto simp: const)
done
qed

text‹The special case where @{term f} is non-negative and @{term"e<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. ∀x∈S. ¦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" "n≥1"
using e
apply (simp_all add: n_def field_simps of_nat_Suc)
by (metis real_nat_ceiling_ge mult.commute not_less pos_less_divide_eq)
then have ge_fx: "(n-1) * e ≥ f x" if "x ∈ S" for x
using f normf_upper that by fastforce
{ fix j
have A: "closed (A j)" "A j ⊆ S"
apply (rule continuous_on_closed_Collect_le [OF f continuous_on_const])
done
have B: "closed (B j)" "B j ⊆ S"
apply (rule continuous_on_closed_Collect_le [OF continuous_on_const f])
done
have disj: "(A j) ∩ (B j) = {}"
using e by (auto simp: A_def B_def field_simps)
have "∃f ∈ R. f ` S ⊆ {0..1} ∧ (∀x ∈ A j. f x < e/n) ∧ (∀x ∈ B j. f x > 1 - e/n)"
apply (rule two)
using e A B disj ngt
apply simp_all
done
}
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 * (∑i≤n. 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 f normf_upper by (fastforce simp: A_def field_simps of_nat_diff)
have Asub: "A j ⊆ A i" if "i≥j" for i j
using e that apply (clarsimp simp: A_def)
apply (erule order_trans, simp)
done
{ 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 "i≥j" for i
using Asub [OF that] by blast
then have fj1: "f t ≤ (j - 1/3)*e"
then have Anj: "t ∉ A i" if "i<j" for i
using  Aj  ‹i<j›
using not_less_Least by blast
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 i t ≤ e/n" if "i≥j" for i
using xfA [OF Ai] that by (simp add: less_eq_real_def)
{ 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
apply (clarsimp simp add: field_simps of_nat_diff not_le of_nat_Suc)
apply (rule order_trans [of _ "e * 2 + (e * (real d * 3) + e * (real i * 3))"])
apply auto
done
then have "xf i t > 1 - e/n"
by (rule xfB)
} note **** = this
have xf_le1: "⋀i. xf i t ≤ 1"
using xf01 t by force
have "g t = e * (∑i<j. xf i t) + e * (∑i=j..n. xf i t)"
using j1 jn e
apply (simp add: g_def distrib_left [symmetric])
apply (subst sum.union_disjoint [symmetric])
apply (auto simp: ivl_disj_un)
done
also have "... ≤ e*j + e * ((Suc n - j)*e/n)"
apply (simp_all only: mult_le_cancel_left_pos e)
apply (rule sum_bounded_above [OF xf_le1, where A = "lessThan j", simplified])
using sum_bounded_above [of "{j..n}" "λi. xf i t", OF ***]
apply simp
done
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)"
also have "... ≤ e * (∑i≤j-2. xf i t)"
using e
apply simp
apply (rule order_trans [OF _ sum_bounded_below [OF less_imp_le [OF ****]]])
using True
done
also have "... ≤ g t"
using jn e
using e xf01 t
apply (simp add: g_def zero_le_mult_iff image_subset_iff sum_nonneg)
apply (rule Groups_Big.sum_mono2, auto)
done
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›
lemma (in function_ring_on) Stone_Weierstrass_basic:
assumes f: "continuous_on S f" and e: "e > 0"
shows "∃g ∈ R. ∀x∈S. ¦f x - g x¦ < e"
proof -
have "∃g ∈ R. ∀x∈S. ¦(f x + normf f) - g x¦ < 2 * min (e/2) (1/4)"
apply (rule Stone_Weierstrass_special)
apply (rule Limits.continuous_on_add [OF f Topological_Spaces.continuous_on_const])
using normf_upper [OF f] apply force
done
then obtain g where "g ∈ R" "∀x∈S. ¦g x - (f x + normf f)¦ < e"
by force
then show ?thesis
apply (rule_tac x="λx. g x - normf f" in bexI)
apply (auto simp: algebra_simps intro: diff const)
done
qed

theorem (in function_ring_on) Stone_Weierstrass:
assumes f: "continuous_on S f"
shows "∃F∈UNIV → R. LIM n sequentially. F n :> uniformly_on S f"
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"  "∀x∈S. ¦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 of_nat_Suc)
then have "¦f x - g x¦ < e"
using n(2) x by auto
} note * = this
have "∀⇩F n in sequentially. ∀x∈S. ¦f x - (SOME g. g ∈ R ∧ (∀x∈S. ¦f x - g x¦ < 1 / (1 + real n))) x¦ < e"
apply (rule eventually_sequentiallyI [of N])
apply (auto intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]] *)
done
} then
show ?thesis
apply (rule_tac x="λn::nat. SOME g. g ∈ R ∧ (∀x∈S. ¦f x - g x¦ < 1 / (1 + n))" in bexI)
prefer 2  apply (force intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]])
unfolding uniform_limit_iff
apply (auto simp: dist_norm abs_minus_commute)
done
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"
apply unfold_locales
using assms
by 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]

definition 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
next
case (add h) then show ?case
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"
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)"

"⟦polynomial_function f; polynomial_function g⟧ ⟹ polynomial_function (λx. f x + g x)"

lemma polynomial_function_mult [intro]:
assumes f: "polynomial_function f" and g: "polynomial_function g"
shows "polynomial_function (λx. f x *⇩R g x)"
using g
apply (auto simp: polynomial_function_def bounded_linear_def Real_Vector_Spaces.linear.scaleR  const real_polynomial_function.mult o_def)
apply (rule mult)
using f
apply (auto simp: real_polynomial_function_eq)
done

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)"

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]

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]

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]

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
apply (induction g rule: real_polynomial_function.induct)
using f
done

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 "(∑i = 0..max m n. x^i * (if i ≤ m then a i else 0)) = (∑i = 0..m. x^i * a i)"
proof -
have "(∑i = 0..max m n. x^i * (if i ≤ m then a i else 0)) = (∑i = 0..max m n. (if i ≤ m then x^i * a i else 0))"
by (auto simp: algebra_simps intro: sum.cong)
also have "... = (∑i = 0..m. (if i ≤ m then x^i * a i else 0))"
by (rule sum.mono_neutral_right) auto
also have "... = (∑i = 0..m. 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. ∑i=0..n. a i * x ^ i)"
using assms
proof (induct f)
case (linear f)
then show ?case
apply (rule_tac x="λi. if i=0 then 0 else c" in exI)
apply (rule_tac x=1 in exI)
done
next
case (const c)
show ?case
apply (rule_tac x="λi. c" in exI)
apply (rule_tac x=0 in exI)
apply (auto simp: mult_ac of_nat_Suc)
done
then obtain a1 n1 a2 n2 where
"f1 = (λx. ∑i = 0..n1. a1 i * x ^ i)" "f2 = (λx. ∑i = 0..n2. a2 i * x ^ i)"
by auto
then show ?case
apply (rule_tac x="λi. (if i ≤ n1 then a1 i else 0) + (if i ≤ n2 then a2 i else 0)" in exI)
apply (rule_tac x="max n1 n2" in exI)
using sum_max_0 [where m=n1 and n=n2] sum_max_0 [where m=n2 and n=n1]
apply (simp add: sum.distrib algebra_simps max.commute)
done
case (mult f1 f2)
then obtain a1 n1 a2 n2 where
"f1 = (λx. ∑i = 0..n1. a1 i * x ^ i)" "f2 = (λx. ∑i = 0..n2. a2 i * x ^ i)"
by auto
then obtain b1 b2 where
"f1 = (λx. ∑i = 0..n1. b1 i * x ^ i)" "f2 = (λx. ∑i = 0..n2. b2 i * x ^ i)"
"b1 = (λi. if i≤n1 then a1 i else 0)" "b2 = (λi. if i≤n2 then a2 i else 0)"
by auto
then show ?case
apply (rule_tac x="λi. ∑k≤i. b1 k * b2 (i - k)" in exI)
apply (rule_tac x="n1+n2" in exI)
using polynomial_product [of n1 b1 n2 b2]
done
qed

lemma real_polynomial_function_iff_sum:
"real_polynomial_function f ⟷ (∃a n::nat. f = (λx. ∑i=0..n. a i * x ^ i))"
apply (rule iffI)
apply (erule real_polynomial_function_imp_sum)
apply (auto simp: linear mult const real_polynomial_function_power real_polynomial_function_sum)
done

lemma polynomial_function_iff_Basis_inner:
fixes f :: "'a::real_normed_vector ⇒ 'b::euclidean_space"
shows "polynomial_function f ⟷ (∀b∈Basis. 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: "∀b∈Basis. real_polynomial_function (λx. f x ∙ b)" and h: "bounded_linear h"
have "real_polynomial_function (h ∘ (λx. ∑b∈Basis. (f x ∙ b) *⇩R b))"
apply (rule real_polynomial_function_compose [OF _  linear [OF h]])
using rp
apply (auto simp: real_polynomial_function_eq polynomial_function_mult)
done
then show "real_polynomial_function (h ∘ f)"
qed

subsection ‹Stone-Weierstrass theorem for polynomial functions›

text‹First, we need to show that they are continous, 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"
apply (rule euclidean_isCont)
using assms apply (simp add: polynomial_function_iff_Basis_inner)
apply (force dest: continuous_real_polymonial_function intro: isCont_scaleR)
done

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
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
apply (rule_tac x="λx. p1 x + p2 x" in exI)
apply (auto intro!: derivative_eq_intros)
done
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
apply (rule_tac x="λx. f1 x * p2 x + f2 x * p1 x" in exI)
apply (auto intro!: derivative_eq_intros)
done
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, rule_format]  ‹b ∈ Basis›
has_real_derivative_polynomial_function
by blast
have "∃q. polynomial_function q ∧ (∀x. ((λu. (p u ∙ b) *⇩R b) has_vector_derivative q x) (at x))"
apply (rule_tac x="λx. p' x *⇩R b" in exI)
using ‹b ∈ Basis› p'
apply (auto intro: derivative_eq_intros pd)
done
}
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
apply (rule_tac p'="λx. ∑b∈Basis. qf b x" in that)
apply (force intro: qf)
apply (subst euclidean_representation_sum_fun [of p, symmetric])
apply (auto intro: has_vector_derivative_sum qf)
done
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. ∑b∈Basis. (inner (x-u) b)^2)"
apply (rule real_polynomial_function_sum)
apply (auto simp: algebra_simps real_polynomial_function_power real_polynomial_function_diff
const linear bounded_linear_inner_left)
done
then show ?thesis
apply (intro exI conjI, assumption)
using assms
apply (force simp add: euclidean_eq_iff [of x y] sum_nonneg_eq_0_iff algebra_simps)
done
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"
apply unfold_locales
using assms continuous_on_polymonial_function real_polynomial_function_eq
apply (auto intro: real_polynomial_function_separable)
done
show ?thesis
using PR.Stone_Weierstrass_basic [OF ‹continuous_on S f› ‹0 < e›] that
by blast
qed

lemma 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))"
apply (rule exE [OF Stone_Weierstrass_real_polynomial_function [OF S _, of "λx. f x ∙ b" "e / card Basis"]])
using e f
apply (auto simp: Euclidean_Space.DIM_positive intro: continuous_intros)
done
}
then obtain pf where pf:
"⋀b. b ∈ Basis ⟹ real_polynomial_function (pf b) ∧ (∀x ∈ S. ¦f x ∙ b - pf b x¦ < e / DIM('b))"
apply (rule bchoice [rule_format, THEN exE])
apply assumption
apply (force simp add: intro: that)
done
have "polynomial_function (λx. ∑b∈Basis. pf b x *⇩R b)"
using pf
by (simp add: polynomial_function_sum polynomial_function_mult real_polynomial_function_eq)
moreover
{ fix x
assume "x ∈ S"
have "norm (∑b∈Basis. (f x ∙ b) *⇩R b - pf b x *⇩R b) ≤ (∑b∈Basis. norm ((f x ∙ b) *⇩R b - pf b x *⇩R b))"
by (rule norm_sum)
also have "... < of_nat DIM('b) * (e / DIM('b))"
apply (rule sum_bounded_above_strict)
apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf ‹x ∈ S›)
apply (rule DIM_positive)
done
also have "... = e"
using DIM_positive by (simp add: field_simps)
finally have "norm (∑b∈Basis. (f x ∙ b) *⇩R b - pf b x *⇩R b) < e" .
}
ultimately
show ?thesis
apply (subst euclidean_representation_sum_fun [of f, symmetric])
apply (rule_tac x="λx. ∑b∈Basis. pf b x *⇩R b" in exI)
apply (auto simp: sum_subtractf [symmetric])
done
qed

lemma 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. ∀x∈S. 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. ∀x∈S. 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"

lemma path_approx_polynomial_function:
fixes g :: "real ⇒ 'b::euclidean_space"
assumes "path g" "0 < e"
shows "∃p. polynomial_function p ∧
pathstart p = pathstart g ∧
pathfinish p = pathfinish g ∧
(∀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)
have pf: "polynomial_function (λt. q t + (g 0 - q 0) + t *⇩R (g 1 - q 1 - (g 0 - q 0)))"
have *: "⋀t. t ∈ {0..1} ⟹ 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)"
using noq
apply (auto simp: norm_minus_commute intro: le_less_trans [OF mult_left_le_one_le noq] simp del: less_divide_eq_numeral1)
done
show ?thesis
apply (intro exI conjI)
apply (rule pf)
using *
apply (auto simp add: pathstart_def pathfinish_def algebra_simps)
done
qed

lemma 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
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
next
case False
then have "- S ≠ {}" by blast
then show ?thesis
apply (rule_tac x="setdist (path_image p) (-S)" in exI)
using S p
apply (simp add: setdist_gt_0_compact_closed compact_path_image open_closed)
using setdist_le_dist [of _ "path_image p" _ "-S"]
by fastforce
qed
then obtain e where "0 < e"and eb: "⋀x. x ∈ path_image p ⟹ ball x e ⊆ S"
by auto
show ?thesis
using path_approx_polynomial_function [OF ‹path p› ‹0 < e›]
apply clarify
apply (intro exI conjI, assumption)
using p
apply (fastforce simp add: dist_norm path_image_def norm_minus_commute intro: eb [THEN subsetD])+
done
qed

lemma has_derivative_componentwise_within:
"(f has_derivative f') (at a within S) ⟷
(∀i ∈ Basis. ((λx. f x ∙ i) has_derivative (λx. f' x ∙ i)) (at a within S))"
apply (subst tendsto_componentwise_iff)
apply (simp add: bounded_linear_componentwise_iff [symmetric] ball_conj_distrib)
done

lemma differentiable_componentwise_within:
"f differentiable (at a within S) ⟷
(∀i ∈ Basis. (λx. f x ∙ i) differentiable at a within S)"
proof -
{ assume "∀i∈Basis. ∃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. (∑j∈Basis. f' j x *⇩R j) ∙ i) = f' i" if "i ∈ Basis" for i
have "∃D. ∀i∈Basis. ((λx. f x ∙ i) has_derivative (λx. D x ∙ i)) (at a within S)"
apply (rule_tac x="λx::'a. (∑j∈Basis. f' j x *⇩R j) :: 'b" in exI)
done
}
then show ?thesis
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)

lemma differentiable_on_real_polynomial_function:
"real_polynomial_function p ⟹ p differentiable_on S"

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"

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"
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 "(∑i∈B. (x ∙ i) *⇩R i) = x"
proof (rule vector_eq_dot_span [OF _ ‹x ∈ span B›])
show "(∑i∈B. (x ∙ i) *⇩R i) ∈ span B"
show "i ∙ (∑i∈B. (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 ∙ (∑i∈B. (x ∙ i) *⇩R i) = (∑j∈B. x ∙ j * (i ∙ j))"
also have "... = (∑j∈B. 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 sum.delta)
finally show ?thesis .
qed
qed

lemma 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"
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: "(∑i∈B. (f x ∙ i) *⇩R i) = f x" if "x ∈ S" for x
apply (rule orthonormal_basis_expand [OF orthB B1 _ ‹finite B›])
using ‹f ` S ⊆ T› spanB that by auto
have cont: "continuous_on S (λx. ∑i∈B. (f x ∙ i) *⇩R i)"
by (intro continuous_intros contf)
obtain g where "polynomial_function g"
and g: "⋀x. x ∈ S ⟹ norm ((∑i∈B. (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. ∑i∈B. (g x ∙ i) *⇩R i)"
apply (rule polynomial_function_sum)
using ‹polynomial_function g›  by auto
show "(λx. ∑i∈B. (g x ∙ i) *⇩R i) ` S ⊆ T"
using ‹B ⊆ T› by (blast intro: subspace_sum subspace_mul ‹subspace T›)
show "norm (f x - (∑i∈B. (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"
apply (rule pairwise_mono [OF orthB])
apply (auto simp: orthogonal_def inner_diff_right inner_diff_left)
done
then have "(norm (∑i∈B. (f x ∙ i) *⇩R i - (g x ∙ i) *⇩R i))⇧2 =
(∑i∈B. (norm ((f x ∙ i) *⇩R i - (g x ∙ i) *⇩R i))⇧2)"
by (simp add:  norm_sum_Pythagorean [OF ‹finite B› orth'])
also have "... = (∑i∈B. (norm (((f x - g x) ∙ i) *⇩R i))⇧2)"
also have "... ≤ (∑i∈B. (norm (f x - g x))⇧2)"
apply (rule sum_mono)
apply (rule order_trans [OF Cauchy_Schwarz_ineq])
also have "... = n * norm (f x - g x)^2"
by (simp add: ‹n = card B›)
also have "... ≤ n * (e / (n+2))^2"
apply (rule mult_left_mono)
apply (meson dual_order.order_iff_strict g norm_ge_zero power_mono that, simp)
done
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 (∑i∈B. (f x ∙ i) *⇩R i - (g x ∙ i) *⇩R i))⇧2 < e^2" .
then have "(norm (∑i∈B. (f x ∙ i) *⇩R i - (g x ∙ i) *⇩R i)) < e"
apply (rule power2_less_imp_less)
using  ‹0 < e› by auto
then show ?thesis
using fx that by (simp add: sum_subtractf)
qed
qed
qed