src/HOL/Analysis/Weierstrass_Theorems.thy
 changeset 68833 fde093888c16 parent 68601 7828f3b85156 child 69260 0a9688695a1b
```     1.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Mon Aug 27 22:58:36 2018 +0200
1.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Aug 28 13:28:39 2018 +0100
1.3 @@ -6,29 +6,29 @@
1.4  imports Uniform_Limit Path_Connected Derivative
1.5  begin
1.6
1.7 -subsection \<open>Bernstein polynomials\<close>
1.8 +subsection%important \<open>Bernstein polynomials\<close>
1.9
1.10 -definition Bernstein :: "[nat,nat,real] \<Rightarrow> real" where
1.11 +definition%important Bernstein :: "[nat,nat,real] \<Rightarrow> real" where
1.12    "Bernstein n k x \<equiv> of_nat (n choose k) * x ^ k * (1 - x) ^ (n - k)"
1.13
1.14 -lemma Bernstein_nonneg: "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> Bernstein n k x"
1.15 +lemma%unimportant Bernstein_nonneg: "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> Bernstein n k x"
1.17
1.18 -lemma Bernstein_pos: "\<lbrakk>0 < x; x < 1; k \<le> n\<rbrakk> \<Longrightarrow> 0 < Bernstein n k x"
1.19 +lemma%unimportant Bernstein_pos: "\<lbrakk>0 < x; x < 1; k \<le> n\<rbrakk> \<Longrightarrow> 0 < Bernstein n k x"
1.21
1.22 -lemma sum_Bernstein [simp]: "(\<Sum>k\<le>n. Bernstein n k x) = 1"
1.23 +lemma%unimportant sum_Bernstein [simp]: "(\<Sum>k\<le>n. Bernstein n k x) = 1"
1.24    using binomial_ring [of x "1-x" n]
1.26
1.27 -lemma binomial_deriv1:
1.28 +lemma%unimportant binomial_deriv1:
1.29      "(\<Sum>k\<le>n. (of_nat k * of_nat (n choose k)) * a^(k-1) * b^(n-k)) = real_of_nat n * (a+b) ^ (n-1)"
1.30    apply (rule DERIV_unique [where f = "\<lambda>a. (a+b)^n" and x=a])
1.31    apply (subst binomial_ring)
1.32    apply (rule derivative_eq_intros sum.cong | simp add: atMost_atLeast0)+
1.33    done
1.34
1.35 -lemma binomial_deriv2:
1.36 +lemma%unimportant binomial_deriv2:
1.37      "(\<Sum>k\<le>n. (of_nat k * of_nat (k-1) * of_nat (n choose k)) * a^(k-2) * b^(n-k)) =
1.38       of_nat n * of_nat (n-1) * (a+b::real) ^ (n-2)"
1.39    apply (rule DERIV_unique [where f = "\<lambda>a. of_nat n * (a+b::real) ^ (n-1)" and x=a])
1.40 @@ -36,14 +36,14 @@
1.41    apply (rule derivative_eq_intros sum.cong | simp add: Num.numeral_2_eq_2)+
1.42    done
1.43
1.44 -lemma sum_k_Bernstein [simp]: "(\<Sum>k\<le>n. real k * Bernstein n k x) = of_nat n * x"
1.45 +lemma%important sum_k_Bernstein [simp]: "(\<Sum>k\<le>n. real k * Bernstein n k x) = of_nat n * x"
1.46    apply (subst binomial_deriv1 [of n x "1-x", simplified, symmetric])
1.48    apply (auto simp: Bernstein_def algebra_simps power_eq_if intro!: sum.cong)
1.49    done
1.50
1.51 -lemma sum_kk_Bernstein [simp]: "(\<Sum>k\<le>n. real k * (real k - 1) * Bernstein n k x) = real n * (real n - 1) * x\<^sup>2"
1.52 -proof -
1.53 +lemma%important sum_kk_Bernstein [simp]: "(\<Sum>k\<le>n. real k * (real k - 1) * Bernstein n k x) = real n * (real n - 1) * x\<^sup>2"
1.54 +proof%unimportant -
1.55    have "(\<Sum>k\<le>n. real k * (real k - 1) * Bernstein n k x) =
1.56          (\<Sum>k\<le>n. real k * real (k - Suc 0) * real (n choose k) * x ^ (k - 2) * (1 - x) ^ (n - k) * x\<^sup>2)"
1.57    proof (rule sum.cong [OF refl], simp)
1.58 @@ -65,14 +65,14 @@
1.59      by auto
1.60  qed
1.61
1.62 -subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
1.63 +subsection%important \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
1.64
1.65 -lemma Bernstein_Weierstrass:
1.66 +lemma%important Bernstein_Weierstrass:
1.67    fixes f :: "real \<Rightarrow> real"
1.68    assumes contf: "continuous_on {0..1} f" and e: "0 < e"
1.69      shows "\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> {0..1}
1.70                      \<longrightarrow> \<bar>f x - (\<Sum>k\<le>n. f(k/n) * Bernstein n k x)\<bar> < e"
1.71 -proof -
1.72 +proof%unimportant -
1.73    have "bounded (f ` {0..1})"
1.74      using compact_continuous_image compact_imp_bounded contf by blast
1.75    then obtain M where M: "\<And>x. 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<bar>f x\<bar> \<le> M"
1.76 @@ -167,7 +167,7 @@
1.77  qed
1.78
1.79
1.80 -subsection \<open>General Stone-Weierstrass theorem\<close>
1.81 +subsection%important \<open>General Stone-Weierstrass theorem\<close>
1.82
1.83  text\<open>Source:
1.84  Bruno Brosowski and Frank Deutsch.
1.85 @@ -176,7 +176,7 @@
1.86  Volume 81, Number 1, January 1981.
1.87  DOI: 10.2307/2043993  https://www.jstor.org/stable/2043993\<close>
1.88
1.89 -locale function_ring_on =
1.90 +locale%important function_ring_on =
1.91    fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set"
1.92    assumes compact: "compact S"
1.93    assumes continuous: "f \<in> R \<Longrightarrow> continuous_on S f"
1.94 @@ -186,39 +186,39 @@
1.95    assumes separable: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> \<exists>f\<in>R. f x \<noteq> f y"
1.96
1.97  begin
1.98 -  lemma minus: "f \<in> R \<Longrightarrow> (\<lambda>x. - f x) \<in> R"
1.99 +  lemma%unimportant minus: "f \<in> R \<Longrightarrow> (\<lambda>x. - f x) \<in> R"
1.100      by (frule mult [OF const [of "-1"]]) simp
1.101
1.102 -  lemma diff: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x - g x) \<in> R"
1.103 +  lemma%unimportant diff: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x - g x) \<in> R"
1.105
1.106 -  lemma power: "f \<in> R \<Longrightarrow> (\<lambda>x. f x ^ n) \<in> R"
1.107 +  lemma%unimportant power: "f \<in> R \<Longrightarrow> (\<lambda>x. f x ^ n) \<in> R"
1.108      by (induct n) (auto simp: const mult)
1.109
1.110 -  lemma sum: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>i \<in> I. f i x) \<in> R"
1.111 +  lemma%unimportant sum: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>i \<in> I. f i x) \<in> R"
1.113
1.114 -  lemma prod: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Prod>i \<in> I. f i x) \<in> R"
1.115 +  lemma%unimportant prod: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Prod>i \<in> I. f i x) \<in> R"
1.116      by (induct I rule: finite_induct; simp add: const mult)
1.117
1.118 -  definition normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
1.119 +  definition%important normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
1.120      where "normf f \<equiv> SUP x:S. \<bar>f x\<bar>"
1.121
1.122 -  lemma normf_upper: "\<lbrakk>continuous_on S f; x \<in> S\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f"
1.123 +  lemma%unimportant normf_upper: "\<lbrakk>continuous_on S f; x \<in> S\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f"
1.125      apply (rule cSUP_upper, assumption)
1.126      by (simp add: bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs)
1.127
1.128 -  lemma normf_least: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
1.129 +  lemma%unimportant normf_least: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
1.130      by (simp add: normf_def cSUP_least)
1.131
1.132  end
1.133
1.134 -lemma (in function_ring_on) one:
1.135 +lemma%important (in function_ring_on) one:
1.136    assumes U: "open U" and t0: "t0 \<in> S" "t0 \<in> U" and t1: "t1 \<in> S-U"
1.137      shows "\<exists>V. open V \<and> t0 \<in> V \<and> S \<inter> V \<subseteq> U \<and>
1.138                 (\<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))"
1.139 -proof -
1.140 +proof%unimportant -
1.141    have "\<exists>pt \<in> R. pt t0 = 0 \<and> pt t > 0 \<and> pt ` S \<subseteq> {0..1}" if t: "t \<in> S - U" for t
1.142    proof -
1.143      have "t \<noteq> t0" using t t0 by auto
1.144 @@ -437,7 +437,7 @@
1.145  qed
1.146
1.147  text\<open>Non-trivial case, with @{term A} and @{term B} both non-empty\<close>
1.148 -lemma (in function_ring_on) two_special:
1.149 +lemma%unimportant (in function_ring_on) two_special:
1.150    assumes A: "closed A" "A \<subseteq> S" "a \<in> A"
1.151        and B: "closed B" "B \<subseteq> S" "b \<in> B"
1.152        and disj: "A \<inter> B = {}"
1.153 @@ -542,7 +542,7 @@
1.154    show ?thesis by blast
1.155  qed
1.156
1.157 -lemma (in function_ring_on) two:
1.158 +lemma%unimportant (in function_ring_on) two:
1.159    assumes A: "closed A" "A \<subseteq> S"
1.160        and B: "closed B" "B \<subseteq> S"
1.161        and disj: "A \<inter> B = {}"
1.162 @@ -566,11 +566,11 @@
1.163  qed
1.164
1.165  text\<open>The special case where @{term f} is non-negative and @{term"e<1/3"}\<close>
1.166 -lemma (in function_ring_on) Stone_Weierstrass_special:
1.167 +lemma%important (in function_ring_on) Stone_Weierstrass_special:
1.168    assumes f: "continuous_on S f" and fpos: "\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0"
1.169        and e: "0 < e" "e < 1/3"
1.170    shows "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>f x - g x\<bar> < 2*e"
1.171 -proof -
1.172 +proof%unimportant -
1.173    define n where "n = 1 + nat \<lceil>normf f / e\<rceil>"
1.174    define A where "A j = {x \<in> S. f x \<le> (j - 1/3)*e}" for j :: nat
1.175    define B where "B j = {x \<in> S. f x \<ge> (j + 1/3)*e}" for j :: nat
1.176 @@ -711,10 +711,10 @@
1.177  qed
1.178
1.179  text\<open>The ``unpretentious'' formulation\<close>
1.180 -lemma (in function_ring_on) Stone_Weierstrass_basic:
1.181 +lemma%important (in function_ring_on) Stone_Weierstrass_basic:
1.182    assumes f: "continuous_on S f" and e: "e > 0"
1.183    shows "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>f x - g x\<bar> < e"
1.184 -proof -
1.185 +proof%unimportant -
1.186    have "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>(f x + normf f) - g x\<bar> < 2 * min (e/2) (1/4)"
1.187      apply (rule Stone_Weierstrass_special)
1.188      apply (rule Limits.continuous_on_add [OF f Topological_Spaces.continuous_on_const])
1.189 @@ -730,10 +730,10 @@
1.190  qed
1.191
1.192
1.193 -theorem (in function_ring_on) Stone_Weierstrass:
1.194 +theorem%important (in function_ring_on) Stone_Weierstrass:
1.195    assumes f: "continuous_on S f"
1.196    shows "\<exists>F\<in>UNIV \<rightarrow> R. LIM n sequentially. F n :> uniformly_on S f"
1.197 -proof -
1.198 +proof%unimportant -
1.199    { fix e::real
1.200      assume e: "0 < e"
1.201      then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e"
1.202 @@ -762,7 +762,7 @@
1.203  qed
1.204
1.205  text\<open>A HOL Light formulation\<close>
1.206 -corollary Stone_Weierstrass_HOL:
1.207 +corollary%important Stone_Weierstrass_HOL:
1.208    fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set"
1.209    assumes "compact S"  "\<And>c. P(\<lambda>x. c::real)"
1.210            "\<And>f. P f \<Longrightarrow> continuous_on S f"
1.211 @@ -771,7 +771,7 @@
1.212            "continuous_on S f"
1.213         "0 < e"
1.214      shows "\<exists>g. P(g) \<and> (\<forall>x \<in> S. \<bar>f x - g x\<bar> < e)"
1.215 -proof -
1.216 +proof%unimportant -
1.217    interpret PR: function_ring_on "Collect P"
1.218      apply unfold_locales
1.219      using assms
1.220 @@ -782,7 +782,7 @@
1.221  qed
1.222
1.223
1.224 -subsection \<open>Polynomial functions\<close>
1.225 +subsection%important \<open>Polynomial functions\<close>
1.226
1.227  inductive real_polynomial_function :: "('a::real_normed_vector \<Rightarrow> real) \<Rightarrow> bool" where
1.228      linear: "bounded_linear f \<Longrightarrow> real_polynomial_function f"
1.229 @@ -792,11 +792,11 @@
1.230
1.231  declare real_polynomial_function.intros [intro]
1.232
1.233 -definition polynomial_function :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> bool"
1.234 +definition%important polynomial_function :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> bool"
1.235    where
1.236     "polynomial_function p \<equiv> (\<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f o p))"
1.237
1.238 -lemma real_polynomial_function_eq: "real_polynomial_function p = polynomial_function p"
1.239 +lemma%unimportant real_polynomial_function_eq: "real_polynomial_function p = polynomial_function p"
1.240  unfolding polynomial_function_def
1.241  proof
1.242    assume "real_polynomial_function p"
1.243 @@ -820,21 +820,21 @@
1.245  qed
1.246
1.247 -lemma polynomial_function_const [iff]: "polynomial_function (\<lambda>x. c)"
1.248 +lemma%unimportant polynomial_function_const [iff]: "polynomial_function (\<lambda>x. c)"
1.249    by (simp add: polynomial_function_def o_def const)
1.250
1.251 -lemma polynomial_function_bounded_linear:
1.252 +lemma%unimportant polynomial_function_bounded_linear:
1.253    "bounded_linear f \<Longrightarrow> polynomial_function f"
1.254    by (simp add: polynomial_function_def o_def bounded_linear_compose real_polynomial_function.linear)
1.255
1.256 -lemma polynomial_function_id [iff]: "polynomial_function(\<lambda>x. x)"
1.257 +lemma%unimportant polynomial_function_id [iff]: "polynomial_function(\<lambda>x. x)"
1.259
1.262      "\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x + g x)"
1.264
1.265 -lemma polynomial_function_mult [intro]:
1.266 +lemma%unimportant polynomial_function_mult [intro]:
1.267    assumes f: "polynomial_function f" and g: "polynomial_function g"
1.268      shows "polynomial_function (\<lambda>x. f x *\<^sub>R g x)"
1.269    using g
1.270 @@ -844,45 +844,45 @@
1.271    apply (auto simp: real_polynomial_function_eq)
1.272    done
1.273
1.274 -lemma polynomial_function_cmul [intro]:
1.275 +lemma%unimportant polynomial_function_cmul [intro]:
1.276    assumes f: "polynomial_function f"
1.277      shows "polynomial_function (\<lambda>x. c *\<^sub>R f x)"
1.278    by (rule polynomial_function_mult [OF polynomial_function_const f])
1.279
1.280 -lemma polynomial_function_minus [intro]:
1.281 +lemma%unimportant polynomial_function_minus [intro]:
1.282    assumes f: "polynomial_function f"
1.283      shows "polynomial_function (\<lambda>x. - f x)"
1.284    using polynomial_function_cmul [OF f, of "-1"] by simp
1.285
1.286 -lemma polynomial_function_diff [intro]:
1.287 +lemma%unimportant polynomial_function_diff [intro]:
1.288      "\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x - g x)"
1.291
1.292 -lemma polynomial_function_sum [intro]:
1.293 +lemma%unimportant polynomial_function_sum [intro]:
1.294      "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> polynomial_function (\<lambda>x. f x i)\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. sum (f x) I)"
1.295  by (induct I rule: finite_induct) auto
1.296
1.297 -lemma real_polynomial_function_minus [intro]:
1.298 +lemma%unimportant real_polynomial_function_minus [intro]:
1.299      "real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. - f x)"
1.300    using polynomial_function_minus [of f]
1.302
1.303 -lemma real_polynomial_function_diff [intro]:
1.304 +lemma%unimportant real_polynomial_function_diff [intro]:
1.305      "\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x - g x)"
1.306    using polynomial_function_diff [of f]
1.308
1.309 -lemma real_polynomial_function_sum [intro]:
1.310 +lemma%unimportant real_polynomial_function_sum [intro]:
1.311      "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> real_polynomial_function (\<lambda>x. f x i)\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. sum (f x) I)"
1.312    using polynomial_function_sum [of I f]
1.314
1.315 -lemma real_polynomial_function_power [intro]:
1.316 +lemma%unimportant real_polynomial_function_power [intro]:
1.317      "real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. f x ^ n)"
1.318    by (induct n) (simp_all add: const mult)
1.319
1.320 -lemma real_polynomial_function_compose [intro]:
1.321 +lemma%unimportant real_polynomial_function_compose [intro]:
1.322    assumes f: "polynomial_function f" and g: "real_polynomial_function g"
1.323      shows "real_polynomial_function (g o f)"
1.324    using g
1.325 @@ -891,13 +891,13 @@
1.327    done
1.328
1.329 -lemma polynomial_function_compose [intro]:
1.330 +lemma%unimportant polynomial_function_compose [intro]:
1.331    assumes f: "polynomial_function f" and g: "polynomial_function g"
1.332      shows "polynomial_function (g o f)"
1.333    using g real_polynomial_function_compose [OF f]
1.334    by (auto simp: polynomial_function_def o_def)
1.335
1.336 -lemma sum_max_0:
1.337 +lemma%unimportant sum_max_0:
1.338    fixes x::real (*in fact "'a::comm_ring_1"*)
1.339    shows "(\<Sum>i\<le>max m n. x^i * (if i \<le> m then a i else 0)) = (\<Sum>i\<le>m. x^i * a i)"
1.340  proof -
1.341 @@ -910,7 +910,7 @@
1.342    finally show ?thesis .
1.343  qed
1.344
1.345 -lemma real_polynomial_function_imp_sum:
1.346 +lemma%unimportant real_polynomial_function_imp_sum:
1.347    assumes "real_polynomial_function f"
1.348      shows "\<exists>a n::nat. f = (\<lambda>x. \<Sum>i\<le>n. a i * x ^ i)"
1.349  using assms
1.350 @@ -955,19 +955,19 @@
1.351      done
1.352  qed
1.353
1.354 -lemma real_polynomial_function_iff_sum:
1.355 +lemma%unimportant real_polynomial_function_iff_sum:
1.356       "real_polynomial_function f \<longleftrightarrow> (\<exists>a n::nat. f = (\<lambda>x. \<Sum>i\<le>n. a i * x ^ i))"
1.357    apply (rule iffI)
1.358    apply (erule real_polynomial_function_imp_sum)
1.359    apply (auto simp: linear mult const real_polynomial_function_power real_polynomial_function_sum)
1.360    done
1.361
1.362 -lemma polynomial_function_iff_Basis_inner:
1.363 +lemma%important polynomial_function_iff_Basis_inner:
1.364    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
1.365    shows "polynomial_function f \<longleftrightarrow> (\<forall>b\<in>Basis. real_polynomial_function (\<lambda>x. inner (f x) b))"
1.366          (is "?lhs = ?rhs")
1.367  unfolding polynomial_function_def
1.368 -proof (intro iffI allI impI)
1.369 +proof%unimportant (intro iffI allI impI)
1.370    assume "\<forall>h. bounded_linear h \<longrightarrow> real_polynomial_function (h \<circ> f)"
1.371    then show ?rhs
1.372      by (force simp add: bounded_linear_inner_left o_def)
1.373 @@ -983,17 +983,17 @@
1.375  qed
1.376
1.377 -subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close>
1.378 +subsection%important \<open>Stone-Weierstrass theorem for polynomial functions\<close>
1.379
1.380  text\<open>First, we need to show that they are continous, differentiable and separable.\<close>
1.381
1.382 -lemma continuous_real_polymonial_function:
1.383 +lemma%unimportant continuous_real_polymonial_function:
1.384    assumes "real_polynomial_function f"
1.385      shows "continuous (at x) f"
1.386  using assms
1.387  by (induct f) (auto simp: linear_continuous_at)
1.388
1.389 -lemma continuous_polymonial_function:
1.390 +lemma%unimportant continuous_polymonial_function:
1.391    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
1.392    assumes "polynomial_function f"
1.393      shows "continuous (at x) f"
1.394 @@ -1002,14 +1002,14 @@
1.395    apply (force dest: continuous_real_polymonial_function intro: isCont_scaleR)
1.396    done
1.397
1.398 -lemma continuous_on_polymonial_function:
1.399 +lemma%unimportant continuous_on_polymonial_function:
1.400    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
1.401    assumes "polynomial_function f"
1.402      shows "continuous_on S f"
1.403    using continuous_polymonial_function [OF assms] continuous_at_imp_continuous_on
1.404    by blast
1.405
1.406 -lemma has_real_derivative_polynomial_function:
1.407 +lemma%unimportant has_real_derivative_polynomial_function:
1.408    assumes "real_polynomial_function p"
1.409      shows "\<exists>p'. real_polynomial_function p' \<and>
1.410                   (\<forall>x. (p has_real_derivative (p' x)) (at x))"
1.411 @@ -1043,7 +1043,7 @@
1.412      done
1.413  qed
1.414
1.415 -lemma has_vector_derivative_polynomial_function:
1.416 +lemma%unimportant has_vector_derivative_polynomial_function:
1.417    fixes p :: "real \<Rightarrow> 'a::euclidean_space"
1.418    assumes "polynomial_function p"
1.419    obtains p' where "polynomial_function p'" "\<And>x. (p has_vector_derivative (p' x)) (at x)"
1.420 @@ -1074,7 +1074,7 @@
1.421      done
1.422  qed
1.423
1.424 -lemma real_polynomial_function_separable:
1.425 +lemma%unimportant real_polynomial_function_separable:
1.426    fixes x :: "'a::euclidean_space"
1.427    assumes "x \<noteq> y" shows "\<exists>f. real_polynomial_function f \<and> f x \<noteq> f y"
1.428  proof -
1.429 @@ -1090,11 +1090,11 @@
1.430      done
1.431  qed
1.432
1.433 -lemma Stone_Weierstrass_real_polynomial_function:
1.434 +lemma%important Stone_Weierstrass_real_polynomial_function:
1.435    fixes f :: "'a::euclidean_space \<Rightarrow> real"
1.436    assumes "compact S" "continuous_on S f" "0 < e"
1.437    obtains g where "real_polynomial_function g" "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x - g x\<bar> < e"
1.438 -proof -
1.439 +proof%unimportant -
1.440    interpret PR: function_ring_on "Collect real_polynomial_function"
1.441      apply unfold_locales
1.442      using assms continuous_on_polymonial_function real_polynomial_function_eq
1.443 @@ -1105,13 +1105,13 @@
1.444      by blast
1.445  qed
1.446
1.447 -lemma Stone_Weierstrass_polynomial_function:
1.448 +lemma%important Stone_Weierstrass_polynomial_function:
1.449    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.450    assumes S: "compact S"
1.451        and f: "continuous_on S f"
1.452        and e: "0 < e"
1.453      shows "\<exists>g. polynomial_function g \<and> (\<forall>x \<in> S. norm(f x - g x) < e)"
1.454 -proof -
1.455 +proof%unimportant -
1.456    { fix b :: 'b
1.457      assume "b \<in> Basis"
1.458      have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> S. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))"
1.459 @@ -1151,12 +1151,12 @@
1.460      done
1.461  qed
1.462
1.463 -lemma Stone_Weierstrass_uniform_limit:
1.464 +lemma%important Stone_Weierstrass_uniform_limit:
1.465    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.466    assumes S: "compact S"
1.467      and f: "continuous_on S f"
1.468    obtains g where "uniform_limit S g f sequentially" "\<And>n. polynomial_function (g n)"
1.469 -proof -
1.470 +proof%unimportant -
1.471    have pos: "inverse (Suc n) > 0" for n by auto
1.472    obtain g where g: "\<And>n. polynomial_function (g n)" "\<And>x n. x \<in> S \<Longrightarrow> norm(f x - g n x) < inverse (Suc n)"
1.473      using Stone_Weierstrass_polynomial_function[OF S f pos]
1.474 @@ -1175,17 +1175,17 @@
1.475  qed
1.476
1.477
1.478 -subsection\<open>Polynomial functions as paths\<close>
1.479 +subsection%important\<open>Polynomial functions as paths\<close>
1.480
1.481  text\<open>One application is to pick a smooth approximation to a path,
1.482  or just pick a smooth path anyway in an open connected set\<close>
1.483
1.484 -lemma path_polynomial_function:
1.485 +lemma%unimportant path_polynomial_function:
1.486      fixes g  :: "real \<Rightarrow> 'b::euclidean_space"
1.487      shows "polynomial_function g \<Longrightarrow> path g"
1.488    by (simp add: path_def continuous_on_polymonial_function)
1.489
1.490 -lemma path_approx_polynomial_function:
1.491 +lemma%unimportant path_approx_polynomial_function:
1.492      fixes g :: "real \<Rightarrow> 'b::euclidean_space"
1.493      assumes "path g" "0 < e"
1.494      shows "\<exists>p. polynomial_function p \<and>
1.495 @@ -1211,13 +1211,13 @@
1.496      done
1.497  qed
1.498
1.499 -lemma connected_open_polynomial_connected:
1.500 +lemma%important connected_open_polynomial_connected:
1.501    fixes S :: "'a::euclidean_space set"
1.502    assumes S: "open S" "connected S"
1.503        and "x \<in> S" "y \<in> S"
1.504      shows "\<exists>g. polynomial_function g \<and> path_image g \<subseteq> S \<and>
1.505                 pathstart g = x \<and> pathfinish g = y"
1.506 -proof -
1.507 +proof%unimportant -
1.508    have "path_connected S" using assms
1.510    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"
1.511 @@ -1247,7 +1247,7 @@
1.512      done
1.513  qed
1.514
1.515 -lemma has_derivative_componentwise_within:
1.516 +lemma%unimportant has_derivative_componentwise_within:
1.517     "(f has_derivative f') (at a within S) \<longleftrightarrow>
1.518      (\<forall>i \<in> Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. f' x \<bullet> i)) (at a within S))"
1.520 @@ -1256,7 +1256,7 @@
1.522    done
1.523
1.524 -lemma differentiable_componentwise_within:
1.525 +lemma%unimportant differentiable_componentwise_within:
1.526     "f differentiable (at a within S) \<longleftrightarrow>
1.527      (\<forall>i \<in> Basis. (\<lambda>x. f x \<bullet> i) differentiable at a within S)"
1.528  proof -
1.529 @@ -1277,7 +1277,7 @@
1.530      by blast
1.531  qed
1.532
1.533 -lemma polynomial_function_inner [intro]:
1.534 +lemma%unimportant polynomial_function_inner [intro]:
1.535    fixes i :: "'a::euclidean_space"
1.536    shows "polynomial_function g \<Longrightarrow> polynomial_function (\<lambda>x. g x \<bullet> i)"
1.537    apply (subst euclidean_representation [where x=i, symmetric])
1.538 @@ -1286,26 +1286,26 @@
1.539
1.540  text\<open> Differentiability of real and vector polynomial functions.\<close>
1.541
1.542 -lemma differentiable_at_real_polynomial_function:
1.543 +lemma%unimportant differentiable_at_real_polynomial_function:
1.544     "real_polynomial_function f \<Longrightarrow> f differentiable (at a within S)"
1.545    by (induction f rule: real_polynomial_function.induct)
1.547
1.548 -lemma differentiable_on_real_polynomial_function:
1.549 +lemma%unimportant differentiable_on_real_polynomial_function:
1.550     "real_polynomial_function p \<Longrightarrow> p differentiable_on S"
1.551  by (simp add: differentiable_at_imp_differentiable_on differentiable_at_real_polynomial_function)
1.552
1.553 -lemma differentiable_at_polynomial_function:
1.554 +lemma%unimportant differentiable_at_polynomial_function:
1.555    fixes f :: "_ \<Rightarrow> 'a::euclidean_space"
1.556    shows "polynomial_function f \<Longrightarrow> f differentiable (at a within S)"
1.557    by (metis differentiable_at_real_polynomial_function polynomial_function_iff_Basis_inner differentiable_componentwise_within)
1.558
1.559 -lemma differentiable_on_polynomial_function:
1.560 +lemma%unimportant differentiable_on_polynomial_function:
1.561    fixes f :: "_ \<Rightarrow> 'a::euclidean_space"
1.562    shows "polynomial_function f \<Longrightarrow> f differentiable_on S"
1.563  by (simp add: differentiable_at_polynomial_function differentiable_on_def)
1.564
1.565 -lemma vector_eq_dot_span:
1.566 +lemma%unimportant vector_eq_dot_span:
1.567    assumes "x \<in> span B" "y \<in> span B" and i: "\<And>i. i \<in> B \<Longrightarrow> i \<bullet> x = i \<bullet> y"
1.568    shows "x = y"
1.569  proof -
1.570 @@ -1318,7 +1318,7 @@
1.571      then show ?thesis by simp
1.572  qed
1.573
1.574 -lemma orthonormal_basis_expand:
1.575 +lemma%unimportant orthonormal_basis_expand:
1.576    assumes B: "pairwise orthogonal B"
1.577        and 1: "\<And>i. i \<in> B \<Longrightarrow> norm i = 1"
1.578        and "x \<in> span B"
1.579 @@ -1343,7 +1343,7 @@
1.580  qed
1.581
1.582
1.583 -lemma Stone_Weierstrass_polynomial_function_subspace:
1.584 +lemma%important Stone_Weierstrass_polynomial_function_subspace:
1.585    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.586    assumes "compact S"
1.587        and contf: "continuous_on S f"
1.588 @@ -1351,7 +1351,7 @@
1.589        and "subspace T" "f ` S \<subseteq> T"
1.590      obtains g where "polynomial_function g" "g ` S \<subseteq> T"
1.591                      "\<And>x. x \<in> S \<Longrightarrow> norm(f x - g x) < e"
1.592 -proof -
1.593 +proof%unimportant -
1.594    obtain B where "B \<subseteq> T" and orthB: "pairwise orthogonal B"
1.595               and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
1.596               and "independent B" and cardB: "card B = dim T"
```