section \<open>Bernstein-Weierstrass and Stone-Weierstrass\<close>
text\<open>By L C Paulson (2015)\<close>
theory Weierstrass_Theorems
imports Uniform_Limit Path_Connected Derivative
begin
subsection \<open>Bernstein polynomials\<close>
definition\<^marker>\<open>tag important\<close> Bernstein :: "[nat,nat,real] \<Rightarrow> 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]: "(\k\n. Bernstein n k x) = 1"
using binomial_ring [of x "1-x" n]
by (simp add: Bernstein_def)
lemma binomial_deriv1:
"(\k\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 add: atMost_atLeast0)+
done
lemma binomial_deriv2:
"(\k\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\n. 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]: "(\k\n. real k * (real k - 1) * Bernstein n k x) = real n * (real n - 1) * x\<^sup>2"
proof -
have "(\k\n. real k * (real k - 1) * Bernstein n k x) =
(\<Sum>k\<le>n. real k * real (k - Suc 0) * real (n choose k) * x^(k - 2) * (1 - x)^(n - k) * x\<^sup>2)"
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) * x\<^sup>2)))"
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) * x\<^sup>2"
by (subst binomial_deriv2 [of n x "1-x", simplified, symmetric]) (simp add: sum_distrib_right)
also have "... = n * (n - 1) * x\<^sup>2"
by auto
finally show ?thesis
by auto
qed
subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
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}
\<longrightarrow> \<bar>f x - (\<Sum>k\<le>n. f(k/n) * Bernstein n k x)\<bar> < 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 (nat\4*M/(e*d\<^sup>2)\) \ n" and x: "0 \ x" "x \ 1"
have "0 < n" using n by simp
have ed0: "- (e * d\<^sup>2) < 0"
using e \<open>0<d\<close> by simp
also have "... \ M * 4"
using \<open>0\<le>M\<close> by simp
finally have [simp]: "real_of_int (nat \4 * M / (e * d\<^sup>2)\) = real_of_int \4 * M / (e * d\<^sup>2)\"
using \<open>0\<le>M\<close> e \<open>0<d\<close>
by (simp add: field_simps)
have "4*M/(e*d\<^sup>2) + 1 \ real (Suc (nat\4*M/(e*d\<^sup>2)\))"
by (simp add: real_nat_ceiling_ge)
also have "... \ real n"
using n by (simp add: field_simps)
finally have nbig: "4*M/(e*d\<^sup>2) + 1 \ real n" .
have sum_bern: "(\k\n. (x - k/n)\<^sup>2 * Bernstein n k x) = x * (1 - x) / n"
proof -
have *: "\a b x::real. (a - b)\<^sup>2 * x = a * (a - 1) * x + (1 - 2 * b) * a * x + b * b * x"
by (simp add: algebra_simps power2_eq_square)
have "(\k\n. (k - n * x)\<^sup>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 "(\k\n. (k - n * x)\<^sup>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 / d\<^sup>2 * (x - k/n)\<^sup>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\<^sup>2 * (x - k/n)\<^sup>2)"
using \<open>M\<ge>0\<close> d by simp
finally show ?thesis by simp
next
case ged
then have dle: "d\<^sup>2 \ (x - k/n)\<^sup>2"
by (metis d(1) less_eq_real_def power2_abs power_mono)
have \<section>: "1 \<le> (x - real k / real n)\<^sup>2 / d\<^sup>2"
using dle \<open>d>0\<close> 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)\<^sup>2 / d\<^sup>2)"
using \<section> \<open>M\<ge>0\<close> mult_left_mono by fastforce
also have "... \ e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2"
using e by simp
finally show ?thesis .
qed
} note * = this
have "\f x - (\k\n. f(k / n) * Bernstein n k x)\ \ \\k\n. (f x - f(k / n)) * Bernstein n k x\"
by (simp add: sum_subtractf sum_distrib_left [symmetric] algebra_simps)
also have "... \ (\k\n. \(f x - f(k / n)) * Bernstein n k x\)"
by (rule sum_abs)
also have "... \ (\k\n. (e/2 + (2 * M / d\<^sup>2) * (x - k / n)\<^sup>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) / (d\<^sup>2 * n)"
unfolding sum.distrib Rings.semiring_class.distrib_right sum_distrib_left [symmetric] mult.assoc sum_bern
using \<open>d>0\<close> x by (simp add: divide_simps \<open>M\<ge>0\<close> mult_le_one mult_left_le)
also have "... < e"
using \<open>d>0\<close> nbig e \<open>n>0\<close>
apply (simp add: field_split_simps)
using ed0 by linarith
finally have "\f x - (\k\n. f (real k / real n) * Bernstein n k x)\ < e" .
}
then show ?thesis
by auto
qed
subsection \<open>General Stone-Weierstrass theorem\<close>
text\<open>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 \<^url>\<open>https://www.jstor.org/stable/2043993\<close>\<close>
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"
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)
definition\<^marker>\<open>tag important\<close> normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
where "normf f \ SUP x\S. \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 \
(\<forall>e>0. \<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>t \<in> S \<inter> V. f t < e) \<and> (\<forall>t \<in> S - U. f t > 1 - e))"
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)\<^sup>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)\<^sup>2)"
using t normf_upper [where x=t] continuous [OF hsq] by force
finally have nfp: "0 < normf (\w. (h w)\<^sup>2)" .
define p where [abs_def]: "p x = (1 / normf (\w. (h w)\<^sup>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 = {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
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 \<open>finite subU\<close>])
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 \<delta> where "\<delta> = delta0/2"
have "delta0 \ 1" using delta0 p01 [of t1] t1
by (force simp: ball_def dist_norm dest: p01)
with delta0 have \<delta>01: "0 < \<delta>" "\<delta> < 1"
by (auto simp: \<delta>_def)
have pt_\<delta>: "\<And>x. x \<in> S-U \<Longrightarrow> p x \<ge> \<delta>"
using pt_delta delta0 by (force simp: \<delta>_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 \<delta>01 by (simp add: k_def)
with \<delta>01 have "k \<le> (1+\<delta>)/\<delta>"
by (auto simp: algebra_simps add_divide_distrib)
also have "... < 2/\"
using \<delta>01 by (auto simp: field_split_simps)
finally have k2\<delta>: "k < 2/\<delta>" .
have "1/\ < k"
using \<delta>01 unfolding k_def by linarith
with \<delta>01 k2\<delta> have k\<delta>: "1 < k*\<delta>" "k*\<delta> < 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 \<open>k>0\<close> V have "k * p t < k * \<delta> / 2"
by force
then have "1 - (k * \ / 2)^n \ 1 - (k * p t)^n"
using \<open>k>0\<close> 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 \<open>k>0\<close> U have "k * \<delta> \<le> k * p t"
by (simp add: pt_\<delta>)
with k\<delta> 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] \<open>k>0\<close> 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] \<open>k>0\<close>
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] \<open>k>0\<close>
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 \<open>k>0\<close> p01 power_le_one t
by (intro mult_left_mono [OF power_le_one]) auto
also have "... \ (1 / (k*\))^n"
using \<open>k>0\<close> \<delta>01 power_mono pt_\<delta> 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 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: \<open>\<delta>>0\<close> \<open>0 < k\<close> ln_realpow)
also have "... < ln e"
using NN k\<delta> that by (force simp add: field_simps)
finally show ?thesis
by (simp add: \<open>\<delta>>0\<close> \<open>0 < k\<close> that)
qed
have NN0: "(1/(k*\))^(NN e) < e" if "e>0" for e
proof -
have "0 < ln (real k) + ln \"
using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero ln_mult by fastforce
then have "real (NN e) * ln (1 / (real k * \)) < ln e"
using k\<delta>(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: \<delta>01(1) \<open>0 < k\<close> 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 \<open>e>0\<close>]])
next
assume t: "t \ S - U"
show "q (NN e) t < e"
using limitNonU [OF t] less_le_trans [OF NN0 [OF \<open>e>0\<close>]] 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_\<delta> t0 U V \<delta>01 by fastforce+
ultimately show ?thesis using V t0V
by blast
qed
text\<open>Non-trivial case, with \<^term>\<open>A\<close> and \<^term>\<open>B\<close> both non-empty\<close>
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 \
(\<forall>e>0. \<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>x \<in> S \<inter> V. f x < e) \<and> (\<forall>x \<in> S \<inter> B. f x > 1 - e))"
using one [of "-B" w b] assms \<open>w \<in> A\<close> by simp
}
then obtain Vf where Vf:
"\w. w \ A \ open (Vf w) \ w \ Vf w \ S \ Vf w \ -B \
(\<forall>e>0. \<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>x \<in> S \<inter> Vf w. f x < e) \<and> (\<forall>x \<in> S \<inter> B. f x > 1 - e))"
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 \<open>a \<in> A\<close> 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} \
(\<forall>x \<in> S \<inter> Vf w. ff w x < e / card subA) \<and> (\<forall>x \<in> S \<inter> B. ff w x > 1 - e / card subA)"
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 \<open>B \<subseteq> S\<close> ff subA(1) x by (force simp: field_split_simps)
then show ?thesis
using prod_mono_strict [where f = "\x. 1 - e / card subA"] subA(2) by (force simp add: pff_def)
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\<open>The special case where \<^term>\<open>f\<close> is non-negative and \<^term>\<open>e<1/3\<close>\<close>
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"
using e pos_divide_le_eq real_nat_ceiling_ge[of "normf f / e"]
by (fastforce simp add: divide_simps n_def)
moreover have "n\1"
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 \<open>closed S\<close> 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 \<open>closed S\<close> 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 \<open>1 \<le> n\<close> 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 * (\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 \<open>n\<ge>1\<close> 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 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 "i\j" 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
using Aj \<open>i<j\<close> 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 * (\i\n. xf i t)"
by (simp add: g_def flip: distrib_left)
also have "... = e * (\i \ {.. {j..n}. xf i t)"
by (simp add: ivl_disj_un_one(4) jn)
also have "... = e * (\ii=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"
by (rule sum_bounded_above [OF xf_le1, where A = "lessThan j", simplified])
have "xf i t \ e/n" if "i\j" 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 \<open>1 \<le> n\<close> e by (simp add: field_simps del: of_nat_Suc)
also have "... \ j*e + e*e"
using \<open>1 \<le> n\<close> 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 * (\i\j-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] \<open>1 \<le> n\<close> 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\<open>The ``unpretentious'' formulation\<close>
proposition (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)"
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" "\x\S. \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 "\F\UNIV \ R. LIM n sequentially. F n :> uniformly_on S f"
proof -
define h where "h \ \n::nat. SOME g. g \ R \ (\x\S. \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 \<Rightarrow> 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 \<open>N \<le> n\<close> 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 "\\<^sub>F n in sequentially. \x\S. \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\<open>A HOL Light formulation\<close>
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 \<open>continuous_on S f\<close> \<open>0 < e\<close>]
by blast
qed
subsection \<open>Polynomial functions\<close>
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\<^marker>\<open>tag important\<close> polynomial_function :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 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 *\<^sub>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 *\<^sub>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_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_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 "(\i\max m n. x^i * (if i \ m then a i else 0)) = (\i\m. x^i * a i)"
proof -
have "(\i\max m n. x^i * (if i \ m then a i else 0)) = (\i\max m n. (if i \ m then x^i * a i else 0))"
by (auto simp: algebra_simps intro: sum.cong)
also have "... = (\i\m. (if i \ m then x^i * a i else 0))"
by (rule sum.mono_neutral_right) auto
also have "... = (\i\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\n. 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 = (\i\1. (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 = (\i\0. 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. \i\n1. a1 i * x^i)" "f2 = (\x. \i\n2. a2 i * x^i)"
by auto
then have "f1 x + f2 x = (\i\max 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. \i\n1. a1 i * x^i)" "f2 = (\x. \i\n2. a2 i * x^i)"
by auto
then obtain b1 b2 where
"f1 = (\x. \i\n1. b1 i * x^i)" "f2 = (\x. \i\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 have "f1 x * f2 x = (\i\n1 + n2. (\k\i. 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. \i\n. 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 \ (\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) *\<^sub>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 \<open>Stone-Weierstrass theorem for polynomial functions\<close>
text\<open>First, we need to show that they are continuous, differentiable and separable.\<close>
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) *\<^sub>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' \
(\<forall>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'" "\<And>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 *\<^sub>R b)"
using \<open>b \<in> Basis\<close> 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) *\<^sub>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) *\<^sub>R b) has_vector_derivative qf b x) (at x)"
by metis
show ?thesis
proof
show "\x. (p has_vector_derivative (\b\Basis. 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. \b\Basis. (inner (x-u) b)^2)"
proof (rule real_polynomial_function_sum)
show "\i. i \ Basis \ real_polynomial_function (\u. ((x - u) \ i)\<^sup>2)"
by (auto simp: algebra_simps real_polynomial_function_diff const linear bounded_linear_inner_left)
qed auto
moreover have "(\b\Basis. ((x - y) \ b)\<^sup>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 \<open>auto intro: real_polynomial_function_separable\<close>)
show ?thesis
using PR.Stone_Weierstrass_basic [OF \<open>continuous_on S f\<close> \<open>0 < e\<close>] 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. \b\Basis. pf b x *\<^sub>R b"
{ fix x
assume "x \ S"
have "norm (\b\Basis. (f x \ b) *\<^sub>R b - pf b x *\<^sub>R b) \ (\b\Basis. norm ((f x \ b) *\<^sub>R b - pf b x *\<^sub>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) *\<^sub>R i - pf i x *\<^sub>R i) < e / real DIM('b)"
by (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf \<open>x \<in> S\<close>)
qed (rule DIM_positive)
also have "... = e"
by (simp add: field_simps)
finally have "norm (\b\Basis. (f x \ b) *\<^sub>R b - pf b x *\<^sub>R b) < e" .
}
then have "\x\S. norm ((\b\Basis. (f x \ b) *\<^sub>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 "\\<^sub>F n in sequentially. inverse (Suc n) < e"
by (rule order_tendstoD)
moreover have "\\<^sub>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 "\\<^sub>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\<open>Polynomial functions as paths\<close>
text\<open>One application is to pick a smooth approximation to a path,
or just pick a smooth path anyway in an open connected set\<close>
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 *\<^sub>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 *\<^sub>R (g 1 - q 1) + t *\<^sub>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 *\<^sub>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 *\<^sub>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 \<open>x \<in> S\<close> \<open>y \<in> S\<close> obtain p where p: "path p" "path_image p \<subseteq> S" "pathstart p = x" "pathfinish p = y"
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 \<open>path p\<close> \<open>0 < e\<close>] 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 \<open>0 \<le> x'\<close> \<open>x' \<le> 1\<close> atLeastAtMost_iff eb imageI mem_ball path_image_def subset_iff)
qed
qed
qed
lemma differentiable_componentwise_within:
"f differentiable (at a within S) \
(\<forall>i \<in> Basis. (\<lambda>x. f x \<bullet> 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 *\<^sub>R j) \ i) = f' i" if "i \ Basis" for i
using that by (simp add: inner_add_left inner_add_right)
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 *\<^sub>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\<open> Differentiability of real and vector polynomial functions.\<close>
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 "(\i\B. (x \ i) *\<^sub>R i) = x"
proof (rule vector_eq_dot_span [OF _ \<open>x \<in> span B\<close>])
show "(\i\B. (x \ i) *\<^sub>R i) \ span B"
by (simp add: span_clauses span_sum)
show "i \ (\i\B. (x \ i) *\<^sub>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 \<open>i \<in> B\<close>
by (force simp: norm_eq_1 orthogonal_def pairwise_def)
have "i \ (\i\B. (x \ i) *\<^sub>R i) = (\j\B. x \ j * (i \ j))"
by (simp add: inner_sum_right)
also have "... = (\j\B. if j = i then x \ i else 0)"
by (rule sum.cong; simp)
also have "... = i \ x"
by (simp add: \<open>finite B\<close> 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 \<open>subspace T\<close> 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: "(\i\B. (f x \ i) *\<^sub>R i) = f x" if "x \ S" for x
by (metis (no_types, lifting) B1 \<open>finite B\<close> assms(5) image_subset_iff orthB orthonormal_basis_expand spanB sum.cong that)
have cont: "continuous_on S (\x. \i\B. (f x \ i) *\<^sub>R i)"
by (intro continuous_intros contf)
obtain g where "polynomial_function g"
and g: "\x. x \ S \ norm ((\i\B. (f x \ i) *\<^sub>R i) - g x) < e / (n+2)"
using Stone_Weierstrass_polynomial_function [OF \<open>compact S\<close> cont, of "e / real (n + 2)"] \<open>0 < e\<close>
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) *\<^sub>R i)"
using \<open>polynomial_function g\<close> by (force intro: \<open>finite B\<close>)
show "(\x. \i\B. (g x \ i) *\<^sub>R i) ` S \ T"
using \<open>B \<subseteq> T\<close>
by (blast intro: subspace_sum subspace_mul \<open>subspace T\<close>)
show "norm (f x - (\i\B. (g x \ i) *\<^sub>R i)) < e" if "x \ S" for x
proof -
have orth': "pairwise (\i j. orthogonal ((f x \ i) *\<^sub>R i - (g x \ i) *\<^sub>R i)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.50 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
