src/HOL/Analysis/Weierstrass_Theorems.thy

 
 theory Weierstrass_Theorems
 imports Uniform_Limit Path_Connected Derivative
 begin
 
-subsection%important \<open>Bernstein polynomials\<close>
+subsection \<open>Bernstein polynomials\<close>
 
 definition%important Bernstein :: "[nat,nat,real] \<Rightarrow> real" where
   "Bernstein n k x \<equiv> of_nat (n choose k) * x ^ k * (1 - x) ^ (n - k)"
 
 lemma%unimportant Bernstein_nonneg: "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> Bernstein n k x"

     by auto
   finally show ?thesis
     by auto
 qed
 
-subsection%important \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
+subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
 
 lemma%important Bernstein_Weierstrass:
   fixes f :: "real \<Rightarrow> real"
   assumes contf: "continuous_on {0..1} f" and e: "0 < e"
     shows "\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> {0..1}

   then show ?thesis
     by auto
 qed
 
 
-subsection%important \<open>General Stone-Weierstrass theorem\<close>
+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

     using PR.Stone_Weierstrass_basic [OF \<open>continuous_on S f\<close> \<open>0 < e\<close>]
     by blast
 qed
 
 
-subsection%important \<open>Polynomial functions\<close>
+subsection \<open>Polynomial functions\<close>
 
 inductive real_polynomial_function :: "('a::real_normed_vector \<Rightarrow> real) \<Rightarrow> bool" where
     linear: "bounded_linear f \<Longrightarrow> real_polynomial_function f"
   | const: "real_polynomial_function (\<lambda>x. c)"
   | add:   "\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x + g x)"

     done
   then show "real_polynomial_function (h \<circ> f)"
     by (simp add: euclidean_representation_sum_fun)
 qed
 
-subsection%important \<open>Stone-Weierstrass theorem for polynomial functions\<close>
+subsection \<open>Stone-Weierstrass theorem for polynomial functions\<close>
 
 text\<open>First, we need to show that they are continous, differentiable and separable.\<close>
 
 lemma%unimportant continuous_real_polymonial_function:
   assumes "real_polynomial_function f"

   qed
   then show ?thesis using g(1) ..
 qed
 
 
-subsection%important\<open>Polynomial functions as paths\<close>
+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%unimportant path_polynomial_function: