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.16    by (simp add: Bernstein_def)
    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.20    by (simp add: Bernstein_def)
    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.25    by (simp add: Bernstein_def)
    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.47    apply (simp add: sum_distrib_right)
    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.104      unfolding diff_conv_add_uminus by (metis add minus)
   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.112      by (induct I rule: finite_induct; simp add: const add)
   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.124      apply (simp add: normf_def)
   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.244      by (simp add: o_def)
   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.258    by (simp add: polynomial_function_bounded_linear)
   1.259  
   1.260 -lemma polynomial_function_add [intro]:
   1.261 +lemma%unimportant polynomial_function_add [intro]:
   1.262      "\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x + g x)"
   1.263    by (auto simp: polynomial_function_def bounded_linear_def linear_add real_polynomial_function.add o_def)
   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.289    unfolding add_uminus_conv_diff [symmetric]
   1.290    by (metis polynomial_function_add polynomial_function_minus)
   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.301    by (simp add: real_polynomial_function_eq)
   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.307    by (simp add: real_polynomial_function_eq)
   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.313    by (simp add: real_polynomial_function_eq)
   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.326    apply (simp_all add: polynomial_function_def o_def const add mult)
   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.374      by (simp add: euclidean_representation_sum_fun)
   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.509      by (simp add: connected_open_path_connected)
   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.519    apply (simp add: has_derivative_within)
   1.520 @@ -1256,7 +1256,7 @@
   1.521    apply (simp add: algebra_simps)
   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.546       (simp_all add: bounded_linear_imp_differentiable)
   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"