--- a/src/HOL/Analysis/Set_Integral.thy Thu Jan 24 14:45:07 2019 +0000
+++ b/src/HOL/Analysis/Set_Integral.thy Fri Jan 25 02:38:26 2019 +0000
@@ -319,11 +319,11 @@
using ae by (auto simp: subset_eq split: split_indicator)
qed (use assms in \<open>auto simp: set_borel_measurable_def\<close>)
-lemma%important set_borel_measurable_subset:
+proposition set_borel_measurable_subset:
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
shows "set_borel_measurable M B f"
-proof%unimportant-
+proof-
have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
using assms unfolding set_borel_measurable_def
using borel_measurable_indicator borel_measurable_scaleR by blast
@@ -360,13 +360,13 @@
finally show ?thesis .
qed
-lemma%important set_integral_finite_Union:
+lemma set_integral_finite_Union:
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes "finite I" "disjoint_family_on A I"
and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
using assms
-proof%unimportant induction
+proof induction
case (insert x F)
then have "A x \<inter> \<Union>(A ` F) = {}"
by (meson disjoint_family_on_insert)
@@ -410,7 +410,7 @@
qed
(* Proof from Royden Real Analysis, p. 91. *)
-lemma%important lebesgue_integral_countable_add:
+lemma lebesgue_integral_countable_add:
fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
@@ -639,7 +639,7 @@
using * by auto
qed
-lemma nn_integral_disjoint_family:
+proposition nn_integral_disjoint_family:
assumes [measurable]: "f \<in> borel_measurable M" "\<And>(n::nat). B n \<in> sets M"
and "disjoint_family B"
shows "(\<integral>\<^sup>+x \<in> (\<Union>n. B n). f x \<partial>M) = (\<Sum>n. (\<integral>\<^sup>+x \<in> B n. f x \<partial>M))"
@@ -825,12 +825,12 @@
The formalization is more painful as one should jump back and forth between reals and ereals and justify
all the time positivity or integrability (thankfully, measurability is handled more or less automatically).\<close>
-lemma%important Scheffe_lemma1:
+proposition Scheffe_lemma1:
assumes "\<And>n. integrable M (F n)" "integrable M f"
"AE x in M. (\<lambda>n. F n x) \<longlonglongrightarrow> f x"
"limsup (\<lambda>n. \<integral>\<^sup>+ x. norm(F n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
shows "(\<lambda>n. \<integral>\<^sup>+ x. norm(F n x - f x) \<partial>M) \<longlonglongrightarrow> 0"
-proof%unimportant -
+proof -
have [measurable]: "\<And>n. F n \<in> borel_measurable M" "f \<in> borel_measurable M"
using assms(1) assms(2) by simp_all
define G where "G = (\<lambda>n x. norm(f x) + norm(F n x) - norm(F n x - f x))"
@@ -921,26 +921,26 @@
by (rule tendsto_0_if_Limsup_eq_0_ennreal)
qed
-lemma%important Scheffe_lemma2:
+proposition Scheffe_lemma2:
fixes F::"nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
assumes "\<And> n::nat. F n \<in> borel_measurable M" "integrable M f"
"AE x in M. (\<lambda>n. F n x) \<longlonglongrightarrow> f x"
"\<And>n. (\<integral>\<^sup>+ x. norm(F n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x) \<partial>M)"
shows "(\<lambda>n. \<integral>\<^sup>+ x. norm(F n x - f x) \<partial>M) \<longlonglongrightarrow> 0"
-proof%unimportant (rule Scheffe_lemma1)
+proof (rule Scheffe_lemma1)
fix n::nat
have "(\<integral>\<^sup>+ x. norm(f x) \<partial>M) < \<infinity>" using assms(2) by (metis has_bochner_integral_implies_finite_norm integrable.cases)
then have "(\<integral>\<^sup>+ x. norm(F n x) \<partial>M) < \<infinity>" using assms(4)[of n] by auto
then show "integrable M (F n)" by (subst integrable_iff_bounded, simp add: assms(1)[of n])
qed (auto simp add: assms Limsup_bounded)
-lemma%important tendsto_set_lebesgue_integral_at_right:
+lemma tendsto_set_lebesgue_integral_at_right:
fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
assumes "a < b" and sets: "\<And>a'. a' \<in> {a<..b} \<Longrightarrow> {a'..b} \<in> sets M"
and "set_integrable M {a<..b} f"
shows "((\<lambda>a'. set_lebesgue_integral M {a'..b} f) \<longlongrightarrow>
set_lebesgue_integral M {a<..b} f) (at_right a)"
-proof%unimportant (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases)
+proof (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases)
case (1 S)
have eq: "(\<Union>n. {S n..b}) = {a<..b}"
proof safe
@@ -961,13 +961,13 @@
The next lemmas relate convergence of integrals over an interval to
improper integrals.
\<close>
-lemma%important tendsto_set_lebesgue_integral_at_left:
+lemma tendsto_set_lebesgue_integral_at_left:
fixes a b :: real and f :: "real \<Rightarrow> 'a :: {banach,second_countable_topology}"
assumes "a < b" and sets: "\<And>b'. b' \<in> {a..<b} \<Longrightarrow> {a..b'} \<in> sets M"
and "set_integrable M {a..<b} f"
shows "((\<lambda>b'. set_lebesgue_integral M {a..b'} f) \<longlongrightarrow>
set_lebesgue_integral M {a..<b} f) (at_left b)"
-proof%unimportant (rule tendsto_at_left_sequentially[OF assms(1)], goal_cases)
+proof (rule tendsto_at_left_sequentially[OF assms(1)], goal_cases)
case (1 S)
have eq: "(\<Union>n. {a..S n}) = {a..<b}"
proof safe
@@ -983,12 +983,12 @@
with eq show ?case by simp
qed
-lemma%important tendsto_set_lebesgue_integral_at_top:
+proposition tendsto_set_lebesgue_integral_at_top:
fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
assumes sets: "\<And>b. b \<ge> a \<Longrightarrow> {a..b} \<in> sets M"
and int: "set_integrable M {a..} f"
shows "((\<lambda>b. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {a..} f) at_top"
-proof%unimportant (rule tendsto_at_topI_sequentially)
+proof (rule tendsto_at_topI_sequentially)
fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
show "(\<lambda>n. set_lebesgue_integral M {a..X n} f) \<longlonglongrightarrow> set_lebesgue_integral M {a..} f"
unfolding set_lebesgue_integral_def
@@ -1020,12 +1020,12 @@
qed
qed
-lemma%important tendsto_set_lebesgue_integral_at_bot:
+proposition tendsto_set_lebesgue_integral_at_bot:
fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
assumes sets: "\<And>a. a \<le> b \<Longrightarrow> {a..b} \<in> sets M"
and int: "set_integrable M {..b} f"
shows "((\<lambda>a. set_lebesgue_integral M {a..b} f) \<longlongrightarrow> set_lebesgue_integral M {..b} f) at_bot"
-proof%unimportant (rule tendsto_at_botI_sequentially)
+proof (rule tendsto_at_botI_sequentially)
fix X :: "nat \<Rightarrow> real" assume "filterlim X at_bot sequentially"
show "(\<lambda>n. set_lebesgue_integral M {X n..b} f) \<longlonglongrightarrow> set_lebesgue_integral M {..b} f"
unfolding set_lebesgue_integral_def
--- a/src/HOL/Analysis/Simplex_Content.thy Thu Jan 24 14:45:07 2019 +0000
+++ b/src/HOL/Analysis/Simplex_Content.thy Fri Jan 25 02:38:26 2019 +0000
@@ -5,7 +5,7 @@
The content of an n-dimensional simplex, including the formula for the content of a
triangle and Heron's formula.
*)
-section%important \<open>Volume of a Simplex\<close>
+section \<open>Volume of a Simplex\<close>
theory Simplex_Content
imports Change_Of_Vars
@@ -28,13 +28,13 @@
using assms sum_nonneg[of A x] unfolding S_def
by (force simp: sum_delta_notmem algebra_simps)
-lemma%important emeasure_std_simplex_aux:
+lemma emeasure_std_simplex_aux:
fixes t :: real
assumes "finite (A :: 'a set)" "t \<ge> 0"
shows "emeasure (Pi\<^sub>M A (\<lambda>_. lborel))
(S A t \<inter> space (Pi\<^sub>M A (\<lambda>_. lborel))) = t ^ card A / fact (card A)"
using assms(1,2)
-proof%unimportant (induction arbitrary: t rule: finite_induct)
+proof (induction arbitrary: t rule: finite_induct)
case (empty t)
thus ?case by (simp add: PiM_empty S_def)
next
@@ -112,18 +112,18 @@
finally show ?thesis by (simp only: std_simplex)
qed
-theorem%important content_std_simplex:
+theorem content_std_simplex:
"measure lborel (convex hull (insert 0 Basis :: 'a :: euclidean_space set)) =
1 / fact DIM('a)"
- by%unimportant (simp add: measure_def emeasure_std_simplex)
+ by (simp add: measure_def emeasure_std_simplex)
(* TODO: move to Change_of_Vars *)
-lemma%important measure_lebesgue_linear_transformation:
+proposition measure_lebesgue_linear_transformation:
fixes A :: "(real ^ 'n :: {finite, wellorder}) set"
fixes f :: "_ \<Rightarrow> real ^ 'n :: {finite, wellorder}"
assumes "bounded A" "A \<in> sets lebesgue" "linear f"
shows "measure lebesgue (f ` A) = \<bar>det (matrix f)\<bar> * measure lebesgue A"
-proof%unimportant -
+proof -
from assms have [intro]: "A \<in> lmeasurable"
by (intro bounded_set_imp_lmeasurable) auto
hence [intro]: "f ` A \<in> lmeasurable"
@@ -143,12 +143,12 @@
finally show ?thesis .
qed
-theorem%important content_simplex:
+theorem content_simplex:
fixes X :: "(real ^ 'n :: {finite, wellorder}) set" and f :: "'n :: _ \<Rightarrow> real ^ ('n :: _)"
assumes "finite X" "card X = Suc CARD('n)" and x0: "x0 \<in> X" and bij: "bij_betw f UNIV (X - {x0})"
defines "M \<equiv> (\<chi> i. \<chi> j. f j $ i - x0 $ i)"
shows "content (convex hull X) = \<bar>det M\<bar> / fact (CARD('n))"
-proof%unimportant -
+proof -
define g where "g = (\<lambda>x. M *v x)"
have [simp]: "M *v axis i 1 = f i - x0" for i :: 'n
by (simp add: M_def matrix_vector_mult_basis column_def vec_eq_iff)
@@ -184,11 +184,11 @@
using finite_imp_compact_convex_hull[OF \<open>finite X\<close>] by (auto dest: compact_imp_closed)
qed
-theorem%important content_triangle:
+theorem content_triangle:
fixes A B C :: "real ^ 2"
shows "content (convex hull {A, B, C}) =
\<bar>(C $ 1 - A $ 1) * (B $ 2 - A $ 2) - (B $ 1 - A $ 1) * (C $ 2 - A $ 2)\<bar> / 2"
-proof%unimportant -
+proof -
define M :: "real ^ 2 ^ 2" where "M \<equiv> (\<chi> i. \<chi> j. (if j = 1 then B else C) $ i - A $ i)"
define g where "g = (\<lambda>x. M *v x)"
define std where "std = (convex hull insert 0 Basis :: (real ^ 2) set)"
@@ -228,12 +228,12 @@
by (auto dest!: compact_imp_closed simp: det_2 M_def)
qed
-theorem%important heron:
+theorem heron:
fixes A B C :: "real ^ 2"
defines "a \<equiv> dist B C" and "b \<equiv> dist A C" and "c \<equiv> dist A B"
defines "s \<equiv> (a + b + c) / 2"
shows "content (convex hull {A, B, C}) = sqrt (s * (s - a) * (s - b) * (s - c))"
-proof%unimportant -
+proof -
have [simp]: "(UNIV :: 2 set) = {1, 2}"
using exhaust_2 by auto
have dist_eq: "dist (A :: real ^ 2) B ^ 2 = (A $ 1 - B $ 1) ^ 2 + (A $ 2 - B $ 2) ^ 2"
--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy Thu Jan 24 14:45:07 2019 +0000
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy Fri Jan 25 02:38:26 2019 +0000
@@ -2,29 +2,29 @@
Authors: LC Paulson, based on material from HOL Light
*)
-section%important \<open>Vitali Covering Theorem and an Application to Negligibility\<close>
+section \<open>Vitali Covering Theorem and an Application to Negligibility\<close>
theory Vitali_Covering_Theorem
imports Ball_Volume "HOL-Library.Permutations"
begin
-lemma%important stretch_Galois:
+lemma stretch_Galois:
fixes x :: "real^'n"
shows "(\<And>k. m k \<noteq> 0) \<Longrightarrow> ((y = (\<chi> k. m k * x$k)) \<longleftrightarrow> (\<chi> k. y$k / m k) = x)"
- by%unimportant auto
+ by auto
-lemma%important lambda_swap_Galois:
+lemma lambda_swap_Galois:
"(x = (\<chi> i. y $ Fun.swap m n id i) \<longleftrightarrow> (\<chi> i. x $ Fun.swap m n id i) = y)"
- by%unimportant (auto; simp add: pointfree_idE vec_eq_iff)
+ by (auto; simp add: pointfree_idE vec_eq_iff)
-lemma%important lambda_add_Galois:
+lemma lambda_add_Galois:
fixes x :: "real^'n"
shows "m \<noteq> n \<Longrightarrow> (x = (\<chi> i. if i = m then y$m + y$n else y$i) \<longleftrightarrow> (\<chi> i. if i = m then x$m - x$n else x$i) = y)"
- by%unimportant (safe; simp add: vec_eq_iff)
+ by (safe; simp add: vec_eq_iff)
-lemma%important Vitali_covering_lemma_cballs_balls:
+lemma Vitali_covering_lemma_cballs_balls:
fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
assumes "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> B"
obtains C where "countable C" "C \<subseteq> K"
@@ -32,7 +32,7 @@
"\<And>i. i \<in> K \<Longrightarrow> \<exists>j. j \<in> C \<and>
\<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
cball (a i) (r i) \<subseteq> ball (a j) (5 * r j)"
-proof%unimportant (cases "K = {}")
+proof (cases "K = {}")
case True
with that show ?thesis
by auto
@@ -236,14 +236,14 @@
subsection\<open>Vitali covering theorem\<close>
-lemma%unimportant Vitali_covering_lemma_cballs:
+lemma Vitali_covering_lemma_cballs:
fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
assumes S: "S \<subseteq> (\<Union>i\<in>K. cball (a i) (r i))"
and r: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> B"
obtains C where "countable C" "C \<subseteq> K"
"pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
"S \<subseteq> (\<Union>i\<in>C. cball (a i) (5 * r i))"
-proof%unimportant -
+proof -
obtain C where C: "countable C" "C \<subseteq> K"
"pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
and cov: "\<And>i. i \<in> K \<Longrightarrow> \<exists>j. j \<in> C \<and> \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
@@ -258,14 +258,14 @@
qed (use C in auto)
qed
-lemma%important Vitali_covering_lemma_balls:
+lemma Vitali_covering_lemma_balls:
fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
assumes S: "S \<subseteq> (\<Union>i\<in>K. ball (a i) (r i))"
and r: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i \<and> r i \<le> B"
obtains C where "countable C" "C \<subseteq> K"
"pairwise (\<lambda>i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
"S \<subseteq> (\<Union>i\<in>C. ball (a i) (5 * r i))"
-proof%unimportant -
+proof -
obtain C where C: "countable C" "C \<subseteq> K"
and pw: "pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
and cov: "\<And>i. i \<in> K \<Longrightarrow> \<exists>j. j \<in> C \<and> \<not> disjnt (cball (a i) (r i)) (cball (a j) (r j)) \<and>
@@ -285,7 +285,7 @@
qed
-proposition%important Vitali_covering_theorem_cballs:
+theorem Vitali_covering_theorem_cballs:
fixes a :: "'a \<Rightarrow> 'n::euclidean_space"
assumes r: "\<And>i. i \<in> K \<Longrightarrow> 0 < r i"
and S: "\<And>x d. \<lbrakk>x \<in> S; 0 < d\<rbrakk>
@@ -293,7 +293,7 @@
obtains C where "countable C" "C \<subseteq> K"
"pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C"
"negligible(S - (\<Union>i \<in> C. cball (a i) (r i)))"
-proof%unimportant -
+proof -
let ?\<mu> = "measure lebesgue"
have *: "\<exists>C. countable C \<and> C \<subseteq> K \<and>
pairwise (\<lambda>i j. disjnt (cball (a i) (r i)) (cball (a j) (r j))) C \<and>
@@ -493,13 +493,13 @@
qed
-proposition%important Vitali_covering_theorem_balls:
+theorem Vitali_covering_theorem_balls:
fixes a :: "'a \<Rightarrow> 'b::euclidean_space"
assumes S: "\<And>x d. \<lbrakk>x \<in> S; 0 < d\<rbrakk> \<Longrightarrow> \<exists>i. i \<in> K \<and> x \<in> ball (a i) (r i) \<and> r i < d"
obtains C where "countable C" "C \<subseteq> K"
"pairwise (\<lambda>i j. disjnt (ball (a i) (r i)) (ball (a j) (r j))) C"
"negligible(S - (\<Union>i \<in> C. ball (a i) (r i)))"
-proof%unimportant -
+proof -
have 1: "\<exists>i. i \<in> {i \<in> K. 0 < r i} \<and> x \<in> cball (a i) (r i) \<and> r i < d"
if xd: "x \<in> S" "d > 0" for x d
by (metis (mono_tags, lifting) assms ball_eq_empty less_eq_real_def mem_Collect_eq mem_ball mem_cball not_le xd(1) xd(2))
@@ -523,7 +523,7 @@
qed
-lemma%unimportant negligible_eq_zero_density_alt:
+lemma negligible_eq_zero_density_alt:
"negligible S \<longleftrightarrow>
(\<forall>x \<in> S. \<forall>e > 0.
\<exists>d U. 0 < d \<and> d \<le> e \<and> S \<inter> ball x d \<subseteq> U \<and>
@@ -635,11 +635,11 @@
by metis
qed
-proposition%important negligible_eq_zero_density:
+proposition negligible_eq_zero_density:
"negligible S \<longleftrightarrow>
(\<forall>x\<in>S. \<forall>r>0. \<forall>e>0. \<exists>d. 0 < d \<and> d \<le> r \<and>
(\<exists>U. S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and> measure lebesgue U < e * measure lebesgue (ball x d)))"
-proof%unimportant -
+proof -
let ?Q = "\<lambda>x d e. \<exists>U. S \<inter> ball x d \<subseteq> U \<and> U \<in> lmeasurable \<and> measure lebesgue U < e * content (ball x d)"
have "(\<forall>e>0. \<exists>d>0. d \<le> e \<and> ?Q x d e) = (\<forall>r>0. \<forall>e>0. \<exists>d>0. d \<le> r \<and> ?Q x d e)"
if "x \<in> S" for x
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Thu Jan 24 14:45:07 2019 +0000
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Fri Jan 25 02:38:26 2019 +0000
@@ -11,24 +11,24 @@
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"
+lemma Bernstein_nonneg: "\<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> 0 \<le> Bernstein n k x"
by (simp add: Bernstein_def)
-lemma%unimportant Bernstein_pos: "\<lbrakk>0 < x; x < 1; k \<le> n\<rbrakk> \<Longrightarrow> 0 < Bernstein n k x"
+lemma Bernstein_pos: "\<lbrakk>0 < x; x < 1; k \<le> n\<rbrakk> \<Longrightarrow> 0 < Bernstein n k x"
by (simp add: Bernstein_def)
-lemma%unimportant sum_Bernstein [simp]: "(\<Sum>k\<le>n. Bernstein n k x) = 1"
+lemma sum_Bernstein [simp]: "(\<Sum>k\<le>n. Bernstein n k x) = 1"
using binomial_ring [of x "1-x" n]
by (simp add: Bernstein_def)
-lemma%unimportant binomial_deriv1:
+lemma binomial_deriv1:
"(\<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)"
apply (rule DERIV_unique [where f = "\<lambda>a. (a+b)^n" and x=a])
apply (subst binomial_ring)
apply (rule derivative_eq_intros sum.cong | simp add: atMost_atLeast0)+
done
-lemma%unimportant binomial_deriv2:
+lemma binomial_deriv2:
"(\<Sum>k\<le>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 = "\<lambda>a. of_nat n * (a+b::real) ^ (n-1)" and x=a])
@@ -36,14 +36,14 @@
apply (rule derivative_eq_intros sum.cong | simp add: Num.numeral_2_eq_2)+
done
-lemma%important sum_k_Bernstein [simp]: "(\<Sum>k\<le>n. real k * Bernstein n k x) = of_nat n * x"
+lemma sum_k_Bernstein [simp]: "(\<Sum>k\<le>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%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"
-proof%unimportant -
+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"
+proof -
have "(\<Sum>k\<le>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)
@@ -67,12 +67,12 @@
subsection \<open>Explicit Bernstein version of the 1D Weierstrass approximation theorem\<close>
-lemma%important Bernstein_Weierstrass:
+theorem 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}
\<longrightarrow> \<bar>f x - (\<Sum>k\<le>n. f(k/n) * Bernstein n k x)\<bar> < e"
-proof%unimportant -
+proof -
have "bounded (f ` {0..1})"
using compact_continuous_image compact_imp_bounded contf by blast
then obtain M where M: "\<And>x. 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<bar>f x\<bar> \<le> M"
@@ -176,7 +176,7 @@
Volume 81, Number 1, January 1981.
DOI: 10.2307/2043993 https://www.jstor.org/stable/2043993\<close>
-locale%important function_ring_on =
+locale function_ring_on =
fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set"
assumes compact: "compact S"
assumes continuous: "f \<in> R \<Longrightarrow> continuous_on S f"
@@ -186,39 +186,39 @@
assumes separable: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> \<exists>f\<in>R. f x \<noteq> f y"
begin
- lemma%unimportant minus: "f \<in> R \<Longrightarrow> (\<lambda>x. - f x) \<in> R"
+ lemma minus: "f \<in> R \<Longrightarrow> (\<lambda>x. - f x) \<in> R"
by (frule mult [OF const [of "-1"]]) simp
- lemma%unimportant diff: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x - g x) \<in> R"
+ lemma diff: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x - g x) \<in> R"
unfolding diff_conv_add_uminus by (metis add minus)
- lemma%unimportant power: "f \<in> R \<Longrightarrow> (\<lambda>x. f x ^ n) \<in> R"
+ lemma power: "f \<in> R \<Longrightarrow> (\<lambda>x. f x ^ n) \<in> R"
by (induct n) (auto simp: const mult)
- 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"
+ 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"
by (induct I rule: finite_induct; simp add: const add)
- 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"
+ 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"
by (induct I rule: finite_induct; simp add: const mult)
definition%important normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
where "normf f \<equiv> SUP x\<in>S. \<bar>f x\<bar>"
- lemma%unimportant normf_upper: "\<lbrakk>continuous_on S f; x \<in> S\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f"
+ lemma normf_upper: "\<lbrakk>continuous_on S f; x \<in> S\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f"
apply (simp add: normf_def)
apply (rule cSUP_upper, assumption)
by (simp add: bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs)
- lemma%unimportant normf_least: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
+ lemma normf_least: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
by (simp add: normf_def cSUP_least)
end
-lemma%important (in function_ring_on) one:
+lemma (in function_ring_on) one:
assumes U: "open U" and t0: "t0 \<in> S" "t0 \<in> U" and t1: "t1 \<in> S-U"
shows "\<exists>V. open V \<and> t0 \<in> V \<and> S \<inter> V \<subseteq> U \<and>
(\<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%unimportant -
+proof -
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
proof -
have "t \<noteq> t0" using t t0 by auto
@@ -437,7 +437,7 @@
qed
text\<open>Non-trivial case, with \<^term>\<open>A\<close> and \<^term>\<open>B\<close> both non-empty\<close>
-lemma%unimportant (in function_ring_on) two_special:
+lemma (in function_ring_on) two_special:
assumes A: "closed A" "A \<subseteq> S" "a \<in> A"
and B: "closed B" "B \<subseteq> S" "b \<in> B"
and disj: "A \<inter> B = {}"
@@ -542,7 +542,7 @@
show ?thesis by blast
qed
-lemma%unimportant (in function_ring_on) two:
+lemma (in function_ring_on) two:
assumes A: "closed A" "A \<subseteq> S"
and B: "closed B" "B \<subseteq> S"
and disj: "A \<inter> B = {}"
@@ -566,11 +566,11 @@
qed
text\<open>The special case where \<^term>\<open>f\<close> is non-negative and \<^term>\<open>e<1/3\<close>\<close>
-lemma%important (in function_ring_on) Stone_Weierstrass_special:
+lemma (in function_ring_on) Stone_Weierstrass_special:
assumes f: "continuous_on S f" and fpos: "\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0"
and e: "0 < e" "e < 1/3"
shows "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>f x - g x\<bar> < 2*e"
-proof%unimportant -
+proof -
define n where "n = 1 + nat \<lceil>normf f / e\<rceil>"
define A where "A j = {x \<in> S. f x \<le> (j - 1/3)*e}" for j :: nat
define B where "B j = {x \<in> S. f x \<ge> (j + 1/3)*e}" for j :: nat
@@ -711,10 +711,10 @@
qed
text\<open>The ``unpretentious'' formulation\<close>
-lemma%important (in function_ring_on) Stone_Weierstrass_basic:
+proposition (in function_ring_on) Stone_Weierstrass_basic:
assumes f: "continuous_on S f" and e: "e > 0"
shows "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>f x - g x\<bar> < e"
-proof%unimportant -
+proof -
have "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>(f x + normf f) - g x\<bar> < 2 * min (e/2) (1/4)"
apply (rule Stone_Weierstrass_special)
apply (rule Limits.continuous_on_add [OF f Topological_Spaces.continuous_on_const])
@@ -730,10 +730,10 @@
qed
-theorem%important (in function_ring_on) Stone_Weierstrass:
+theorem (in function_ring_on) Stone_Weierstrass:
assumes f: "continuous_on S f"
shows "\<exists>F\<in>UNIV \<rightarrow> R. LIM n sequentially. F n :> uniformly_on S f"
-proof%unimportant -
+proof -
{ fix e::real
assume e: "0 < e"
then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e"
@@ -762,7 +762,7 @@
qed
text\<open>A HOL Light formulation\<close>
-corollary%important Stone_Weierstrass_HOL:
+corollary Stone_Weierstrass_HOL:
fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set"
assumes "compact S" "\<And>c. P(\<lambda>x. c::real)"
"\<And>f. P f \<Longrightarrow> continuous_on S f"
@@ -771,7 +771,7 @@
"continuous_on S f"
"0 < e"
shows "\<exists>g. P(g) \<and> (\<forall>x \<in> S. \<bar>f x - g x\<bar> < e)"
-proof%unimportant -
+proof -
interpret PR: function_ring_on "Collect P"
apply unfold_locales
using assms
@@ -796,7 +796,7 @@
where
"polynomial_function p \<equiv> (\<forall>f. bounded_linear f \<longrightarrow> real_polynomial_function (f o p))"
-lemma%unimportant real_polynomial_function_eq: "real_polynomial_function p = polynomial_function p"
+lemma real_polynomial_function_eq: "real_polynomial_function p = polynomial_function p"
unfolding polynomial_function_def
proof
assume "real_polynomial_function p"
@@ -820,21 +820,21 @@
by (simp add: o_def)
qed
-lemma%unimportant polynomial_function_const [iff]: "polynomial_function (\<lambda>x. c)"
+lemma polynomial_function_const [iff]: "polynomial_function (\<lambda>x. c)"
by (simp add: polynomial_function_def o_def const)
-lemma%unimportant polynomial_function_bounded_linear:
+lemma polynomial_function_bounded_linear:
"bounded_linear f \<Longrightarrow> polynomial_function f"
by (simp add: polynomial_function_def o_def bounded_linear_compose real_polynomial_function.linear)
-lemma%unimportant polynomial_function_id [iff]: "polynomial_function(\<lambda>x. x)"
+lemma polynomial_function_id [iff]: "polynomial_function(\<lambda>x. x)"
by (simp add: polynomial_function_bounded_linear)
-lemma%unimportant polynomial_function_add [intro]:
+lemma polynomial_function_add [intro]:
"\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x + g x)"
by (auto simp: polynomial_function_def bounded_linear_def linear_add real_polynomial_function.add o_def)
-lemma%unimportant polynomial_function_mult [intro]:
+lemma polynomial_function_mult [intro]:
assumes f: "polynomial_function f" and g: "polynomial_function g"
shows "polynomial_function (\<lambda>x. f x *\<^sub>R g x)"
using g
@@ -844,45 +844,45 @@
apply (auto simp: real_polynomial_function_eq)
done
-lemma%unimportant polynomial_function_cmul [intro]:
+lemma polynomial_function_cmul [intro]:
assumes f: "polynomial_function f"
shows "polynomial_function (\<lambda>x. c *\<^sub>R f x)"
by (rule polynomial_function_mult [OF polynomial_function_const f])
-lemma%unimportant polynomial_function_minus [intro]:
+lemma polynomial_function_minus [intro]:
assumes f: "polynomial_function f"
shows "polynomial_function (\<lambda>x. - f x)"
using polynomial_function_cmul [OF f, of "-1"] by simp
-lemma%unimportant polynomial_function_diff [intro]:
+lemma polynomial_function_diff [intro]:
"\<lbrakk>polynomial_function f; polynomial_function g\<rbrakk> \<Longrightarrow> polynomial_function (\<lambda>x. f x - g x)"
unfolding add_uminus_conv_diff [symmetric]
by (metis polynomial_function_add polynomial_function_minus)
-lemma%unimportant polynomial_function_sum [intro]:
+lemma polynomial_function_sum [intro]:
"\<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)"
by (induct I rule: finite_induct) auto
-lemma%unimportant real_polynomial_function_minus [intro]:
+lemma real_polynomial_function_minus [intro]:
"real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. - f x)"
using polynomial_function_minus [of f]
by (simp add: real_polynomial_function_eq)
-lemma%unimportant real_polynomial_function_diff [intro]:
+lemma real_polynomial_function_diff [intro]:
"\<lbrakk>real_polynomial_function f; real_polynomial_function g\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. f x - g x)"
using polynomial_function_diff [of f]
by (simp add: real_polynomial_function_eq)
-lemma%unimportant real_polynomial_function_sum [intro]:
+lemma real_polynomial_function_sum [intro]:
"\<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)"
using polynomial_function_sum [of I f]
by (simp add: real_polynomial_function_eq)
-lemma%unimportant real_polynomial_function_power [intro]:
+lemma real_polynomial_function_power [intro]:
"real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. f x ^ n)"
by (induct n) (simp_all add: const mult)
-lemma%unimportant real_polynomial_function_compose [intro]:
+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
@@ -891,13 +891,13 @@
apply (simp_all add: polynomial_function_def o_def const add mult)
done
-lemma%unimportant polynomial_function_compose [intro]:
+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%unimportant sum_max_0:
+lemma sum_max_0:
fixes x::real (*in fact "'a::comm_ring_1"*)
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)"
proof -
@@ -910,7 +910,7 @@
finally show ?thesis .
qed
-lemma%unimportant real_polynomial_function_imp_sum:
+lemma real_polynomial_function_imp_sum:
assumes "real_polynomial_function f"
shows "\<exists>a n::nat. f = (\<lambda>x. \<Sum>i\<le>n. a i * x ^ i)"
using assms
@@ -955,19 +955,19 @@
done
qed
-lemma%unimportant real_polynomial_function_iff_sum:
+lemma real_polynomial_function_iff_sum:
"real_polynomial_function f \<longleftrightarrow> (\<exists>a n::nat. f = (\<lambda>x. \<Sum>i\<le>n. a i * x ^ i))"
apply (rule iffI)
apply (erule real_polynomial_function_imp_sum)
apply (auto simp: linear mult const real_polynomial_function_power real_polynomial_function_sum)
done
-lemma%important polynomial_function_iff_Basis_inner:
+lemma polynomial_function_iff_Basis_inner:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
shows "polynomial_function f \<longleftrightarrow> (\<forall>b\<in>Basis. real_polynomial_function (\<lambda>x. inner (f x) b))"
(is "?lhs = ?rhs")
unfolding polynomial_function_def
-proof%unimportant (intro iffI allI impI)
+proof (intro iffI allI impI)
assume "\<forall>h. bounded_linear h \<longrightarrow> real_polynomial_function (h \<circ> f)"
then show ?rhs
by (force simp add: bounded_linear_inner_left o_def)
@@ -987,13 +987,13 @@
text\<open>First, we need to show that they are continous, differentiable and separable.\<close>
-lemma%unimportant continuous_real_polymonial_function:
+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%unimportant continuous_polymonial_function:
+lemma continuous_polymonial_function:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
assumes "polynomial_function f"
shows "continuous (at x) f"
@@ -1002,14 +1002,14 @@
apply (force dest: continuous_real_polymonial_function intro: isCont_scaleR)
done
-lemma%unimportant continuous_on_polymonial_function:
+lemma continuous_on_polymonial_function:
fixes f :: "'a::real_normed_vector \<Rightarrow> '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%unimportant has_real_derivative_polynomial_function:
+lemma has_real_derivative_polynomial_function:
assumes "real_polynomial_function p"
shows "\<exists>p'. real_polynomial_function p' \<and>
(\<forall>x. (p has_real_derivative (p' x)) (at x))"
@@ -1043,7 +1043,7 @@
done
qed
-lemma%unimportant has_vector_derivative_polynomial_function:
+lemma has_vector_derivative_polynomial_function:
fixes p :: "real \<Rightarrow> 'a::euclidean_space"
assumes "polynomial_function p"
obtains p' where "polynomial_function p'" "\<And>x. (p has_vector_derivative (p' x)) (at x)"
@@ -1074,7 +1074,7 @@
done
qed
-lemma%unimportant real_polynomial_function_separable:
+lemma real_polynomial_function_separable:
fixes x :: "'a::euclidean_space"
assumes "x \<noteq> y" shows "\<exists>f. real_polynomial_function f \<and> f x \<noteq> f y"
proof -
@@ -1090,11 +1090,11 @@
done
qed
-lemma%important Stone_Weierstrass_real_polynomial_function:
+lemma Stone_Weierstrass_real_polynomial_function:
fixes f :: "'a::euclidean_space \<Rightarrow> real"
assumes "compact S" "continuous_on S f" "0 < e"
obtains g where "real_polynomial_function g" "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x - g x\<bar> < e"
-proof%unimportant -
+proof -
interpret PR: function_ring_on "Collect real_polynomial_function"
apply unfold_locales
using assms continuous_on_polymonial_function real_polynomial_function_eq
@@ -1105,13 +1105,13 @@
by blast
qed
-lemma%important Stone_Weierstrass_polynomial_function:
+theorem Stone_Weierstrass_polynomial_function:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes S: "compact S"
and f: "continuous_on S f"
and e: "0 < e"
shows "\<exists>g. polynomial_function g \<and> (\<forall>x \<in> S. norm(f x - g x) < e)"
-proof%unimportant -
+proof -
{ fix b :: 'b
assume "b \<in> Basis"
have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> S. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))"
@@ -1151,12 +1151,12 @@
done
qed
-lemma%important Stone_Weierstrass_uniform_limit:
+proposition Stone_Weierstrass_uniform_limit:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes S: "compact S"
and f: "continuous_on S f"
obtains g where "uniform_limit S g f sequentially" "\<And>n. polynomial_function (g n)"
-proof%unimportant -
+proof -
have pos: "inverse (Suc n) > 0" for n by auto
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)"
using Stone_Weierstrass_polynomial_function[OF S f pos]
@@ -1180,12 +1180,12 @@
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:
+lemma path_polynomial_function:
fixes g :: "real \<Rightarrow> 'b::euclidean_space"
shows "polynomial_function g \<Longrightarrow> path g"
by (simp add: path_def continuous_on_polymonial_function)
-lemma%unimportant path_approx_polynomial_function:
+lemma path_approx_polynomial_function:
fixes g :: "real \<Rightarrow> 'b::euclidean_space"
assumes "path g" "0 < e"
shows "\<exists>p. polynomial_function p \<and>
@@ -1211,13 +1211,13 @@
done
qed
-lemma%important connected_open_polynomial_connected:
+proposition connected_open_polynomial_connected:
fixes S :: "'a::euclidean_space set"
assumes S: "open S" "connected S"
and "x \<in> S" "y \<in> S"
shows "\<exists>g. polynomial_function g \<and> path_image g \<subseteq> S \<and>
pathstart g = x \<and> pathfinish g = y"
-proof%unimportant -
+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"
@@ -1247,7 +1247,7 @@
done
qed
-lemma%unimportant has_derivative_componentwise_within:
+lemma has_derivative_componentwise_within:
"(f has_derivative f') (at a within S) \<longleftrightarrow>
(\<forall>i \<in> Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. f' x \<bullet> i)) (at a within S))"
apply (simp add: has_derivative_within)
@@ -1256,7 +1256,7 @@
apply (simp add: algebra_simps)
done
-lemma%unimportant differentiable_componentwise_within:
+lemma differentiable_componentwise_within:
"f differentiable (at a within S) \<longleftrightarrow>
(\<forall>i \<in> Basis. (\<lambda>x. f x \<bullet> i) differentiable at a within S)"
proof -
@@ -1277,7 +1277,7 @@
by blast
qed
-lemma%unimportant polynomial_function_inner [intro]:
+lemma polynomial_function_inner [intro]:
fixes i :: "'a::euclidean_space"
shows "polynomial_function g \<Longrightarrow> polynomial_function (\<lambda>x. g x \<bullet> i)"
apply (subst euclidean_representation [where x=i, symmetric])
@@ -1286,26 +1286,26 @@
text\<open> Differentiability of real and vector polynomial functions.\<close>
-lemma%unimportant differentiable_at_real_polynomial_function:
+lemma differentiable_at_real_polynomial_function:
"real_polynomial_function f \<Longrightarrow> f differentiable (at a within S)"
by (induction f rule: real_polynomial_function.induct)
(simp_all add: bounded_linear_imp_differentiable)
-lemma%unimportant differentiable_on_real_polynomial_function:
+lemma differentiable_on_real_polynomial_function:
"real_polynomial_function p \<Longrightarrow> p differentiable_on S"
by (simp add: differentiable_at_imp_differentiable_on differentiable_at_real_polynomial_function)
-lemma%unimportant differentiable_at_polynomial_function:
+lemma differentiable_at_polynomial_function:
fixes f :: "_ \<Rightarrow> 'a::euclidean_space"
shows "polynomial_function f \<Longrightarrow> f differentiable (at a within S)"
by (metis differentiable_at_real_polynomial_function polynomial_function_iff_Basis_inner differentiable_componentwise_within)
-lemma%unimportant differentiable_on_polynomial_function:
+lemma differentiable_on_polynomial_function:
fixes f :: "_ \<Rightarrow> 'a::euclidean_space"
shows "polynomial_function f \<Longrightarrow> f differentiable_on S"
by (simp add: differentiable_at_polynomial_function differentiable_on_def)
-lemma%unimportant vector_eq_dot_span:
+lemma vector_eq_dot_span:
assumes "x \<in> span B" "y \<in> span B" and i: "\<And>i. i \<in> B \<Longrightarrow> i \<bullet> x = i \<bullet> y"
shows "x = y"
proof -
@@ -1318,7 +1318,7 @@
then show ?thesis by simp
qed
-lemma%unimportant orthonormal_basis_expand:
+lemma orthonormal_basis_expand:
assumes B: "pairwise orthogonal B"
and 1: "\<And>i. i \<in> B \<Longrightarrow> norm i = 1"
and "x \<in> span B"
@@ -1343,7 +1343,7 @@
qed
-lemma%important Stone_Weierstrass_polynomial_function_subspace:
+theorem Stone_Weierstrass_polynomial_function_subspace:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "compact S"
and contf: "continuous_on S f"
@@ -1351,7 +1351,7 @@
and "subspace T" "f ` S \<subseteq> T"
obtains g where "polynomial_function g" "g ` S \<subseteq> T"
"\<And>x. x \<in> S \<Longrightarrow> norm(f x - g x) < e"
-proof%unimportant -
+proof -
obtain B where "B \<subseteq> T" and orthB: "pairwise orthogonal B"
and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
and "independent B" and cardB: "card B = dim T"