--- a/src/HOL/Analysis/Abstract_Topology.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Sat Dec 29 15:43:53 2018 +0100
@@ -2433,7 +2433,7 @@
using openin_subset by fastforce
lemma compactin_euclideanreal_iff [simp]: "compactin euclideanreal S \<longleftrightarrow> compact S"
- by (simp add: compact_eq_heine_borel compactin_def) meson
+ by (simp add: compact_eq_Heine_Borel compactin_def) meson
lemma compactin_absolute [simp]:
"compactin (subtopology X S) S \<longleftrightarrow> compactin X S"
@@ -2725,7 +2725,7 @@
lemma compact_space_discrete_topology: "compact_space(discrete_topology X) \<longleftrightarrow> finite X"
by (simp add: compactin_discrete_topology compact_space_def)
-lemma compact_space_imp_bolzano_weierstrass:
+lemma compact_space_imp_Bolzano_Weierstrass:
assumes "compact_space X" "infinite S" "S \<subseteq> topspace X"
shows "X derived_set_of S \<noteq> {}"
proof
@@ -2738,19 +2738,19 @@
by (metis \<open>infinite S\<close> compactin_subspace compact_space_discrete_topology inf_bot_right subtopology_eq_discrete_topology_eq)
qed
-lemma compactin_imp_bolzano_weierstrass:
+lemma compactin_imp_Bolzano_Weierstrass:
"\<lbrakk>compactin X S; infinite T \<and> T \<subseteq> S\<rbrakk> \<Longrightarrow> S \<inter> X derived_set_of T \<noteq> {}"
- using compact_space_imp_bolzano_weierstrass [of "subtopology X S"]
+ using compact_space_imp_Bolzano_Weierstrass [of "subtopology X S"]
by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2 topspace_subtopology)
-lemma compact_closure_of_imp_bolzano_weierstrass:
+lemma compact_closure_of_imp_Bolzano_Weierstrass:
"\<lbrakk>compactin X (X closure_of S); infinite T; T \<subseteq> S; T \<subseteq> topspace X\<rbrakk> \<Longrightarrow> X derived_set_of T \<noteq> {}"
- using closure_of_mono closure_of_subset compactin_imp_bolzano_weierstrass by fastforce
+ using closure_of_mono closure_of_subset compactin_imp_Bolzano_Weierstrass by fastforce
lemma discrete_compactin_eq_finite:
"S \<inter> X derived_set_of S = {} \<Longrightarrow> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
apply (rule iffI)
- using compactin_imp_bolzano_weierstrass compactin_subset_topspace apply blast
+ using compactin_imp_Bolzano_Weierstrass compactin_subset_topspace apply blast
by (simp add: finite_imp_compactin_eq)
lemma discrete_compact_space_eq_finite:
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Sat Dec 29 15:43:53 2018 +0100
@@ -21,10 +21,12 @@
(* FIXME mv topology euclidean space *)
subsection \<open>Retractions\<close>
-definition "retraction S T r \<longleftrightarrow> T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
-
-definition retract_of (infixl "retract'_of" 50)
- where "(T retract_of S) \<longleftrightarrow> (\<exists>r. retraction S T r)"
+definition%important retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
+where "retraction S T r \<longleftrightarrow>
+ T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
+
+definition%important retract_of (infixl "retract'_of" 50) where
+"T retract_of S \<longleftrightarrow> (\<exists>r. retraction S T r)"
lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow> r (r x) = r x"
unfolding retraction_def by auto
@@ -399,7 +401,7 @@
qed
qed
-subsection \<open>Absolute retracts, absolute neighbourhood retracts (ANR) and Euclidean neighbourhood retracts (ENR)\<close>
+subsection \<open>Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts\<close>
text \<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood
retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding
@@ -410,19 +412,17 @@
definitions, but we need to split them into two implications because of the lack of type
quantifiers. Then ENR turns out to be equivalent to ANR plus local compactness."\<close>
-definition AR :: "'a::topological_space set => bool"
- where
- "AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
- \<longrightarrow> S' retract_of U"
-
-definition ANR :: "'a::topological_space set => bool"
- where
- "ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
- \<longrightarrow> (\<exists>T. openin (subtopology euclidean U) T \<and>
- S' retract_of T)"
-
-definition ENR :: "'a::topological_space set => bool"
- where "ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
+definition%important AR :: "'a::topological_space set \<Rightarrow> bool" where
+"AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set.
+ S homeomorphic S' \<and> closedin (subtopology euclidean U) S' \<longrightarrow> S' retract_of U"
+
+definition%important ANR :: "'a::topological_space set \<Rightarrow> bool" where
+"ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set.
+ S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
+ \<longrightarrow> (\<exists>T. openin (subtopology euclidean U) T \<and> S' retract_of T)"
+
+definition%important ENR :: "'a::topological_space set \<Rightarrow> bool" where
+"ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
text \<open>First, show that we do indeed get the "usual" properties of ARs and ANRs.\<close>
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sat Dec 29 15:43:53 2018 +0100
@@ -3134,7 +3134,7 @@
moreover have "path_image p \<subseteq> (\<Union>c\<in>path_image p. ball c (ee c / 3))"
using ee by auto
ultimately have "\<exists>D \<subseteq> cover. finite D \<and> path_image p \<subseteq> \<Union>D"
- by (simp add: compact_eq_heine_borel cover_def)
+ by (simp add: compact_eq_Heine_Borel cover_def)
then obtain D where D: "D \<subseteq> cover" "finite D" "path_image p \<subseteq> \<Union>D"
by blast
then obtain k where k: "k \<subseteq> {0..1}" "finite k" and D_eq: "D = ((\<lambda>z. ball z (ee z / 3)) \<circ> p) ` k"
@@ -6764,7 +6764,7 @@
obtains g g' where "\<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
proof -
obtain g where g: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f i x) g sequentially"
- using weierstrass_m_test_ev [OF to_g h] by force
+ using Weierstrass_m_test_ev [OF to_g h] by force
have *: "\<exists>d>0. cball x d \<subseteq> S \<and> uniform_limit (cball x d) (\<lambda>n x. \<Sum>i<n. f i x) g sequentially"
if "x \<in> S" for x
proof -
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Sat Dec 29 15:43:53 2018 +0100
@@ -972,7 +972,7 @@
shows "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}"
by (induct n) auto
-lemma field_taylor:
+lemma field_Taylor:
assumes S: "convex S"
and f: "\<And>i x. x \<in> S \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within S)"
and B: "\<And>x. x \<in> S \<Longrightarrow> norm (f (Suc n) x) \<le> B"
@@ -1066,7 +1066,7 @@
finally show ?thesis .
qed
-lemma complex_taylor:
+lemma complex_Taylor:
assumes S: "convex S"
and f: "\<And>i x. x \<in> S \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within S)"
and B: "\<And>x. x \<in> S \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
@@ -1074,7 +1074,7 @@
and z: "z \<in> S"
shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
\<le> B * cmod(z - w)^(Suc n) / fact n"
- using assms by (rule field_taylor)
+ using assms by (rule field_Taylor)
text\<open>Something more like the traditional MVT for real components\<close>
@@ -1099,7 +1099,7 @@
done
qed
-lemma complex_taylor_mvt:
+lemma complex_Taylor_mvt:
assumes "\<And>i x. \<lbrakk>x \<in> closed_segment w z; i \<le> n\<rbrakk> \<Longrightarrow> ((f i) has_field_derivative f (Suc i) x) (at x)"
shows "\<exists>u. u \<in> closed_segment w z \<and>
Re (f 0 z) =
--- a/src/HOL/Analysis/Complex_Transcendental.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Sat Dec 29 15:43:53 2018 +0100
@@ -700,7 +700,7 @@
lemma Taylor_exp_field:
fixes z::"'a::{banach,real_normed_field}"
shows "norm (exp z - (\<Sum>i\<le>n. z ^ i / fact i)) \<le> exp (norm z) * (norm z ^ Suc n) / fact n"
-proof (rule field_taylor[of _ n "\<lambda>k. exp" "exp (norm z)" 0 z, simplified])
+proof (rule field_Taylor[of _ n "\<lambda>k. exp" "exp (norm z)" 0 z, simplified])
show "convex (closed_segment 0 z)"
by (rule convex_closed_segment [of 0 z])
next
@@ -721,7 +721,7 @@
lemma Taylor_exp:
"norm(exp z - (\<Sum>k\<le>n. z ^ k / (fact k))) \<le> exp\<bar>Re z\<bar> * (norm z) ^ (Suc n) / (fact n)"
-proof (rule complex_taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
+proof (rule complex_Taylor [of _ n "\<lambda>k. exp" "exp\<bar>Re z\<bar>" 0 z, simplified])
show "convex (closed_segment 0 z)"
by (rule convex_closed_segment [of 0 z])
next
@@ -778,7 +778,7 @@
have *: "cmod (sin z -
(\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
\<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
- proof (rule complex_taylor [of "closed_segment 0 z" n
+ proof (rule complex_Taylor [of "closed_segment 0 z" n
"\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)"
"exp\<bar>Im z\<bar>" 0 z, simplified])
fix k x
@@ -812,7 +812,7 @@
have *: "cmod (cos z -
(\<Sum>i\<le>n. (-1) ^ (Suc i div 2) * (if even i then cos 0 else sin 0) * z ^ i / (fact i)))
\<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
- proof (rule complex_taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
+ proof (rule complex_Taylor [of "closed_segment 0 z" n "\<lambda>k x. (-1)^(Suc k div 2) * (if even k then cos x else sin x)" "exp\<bar>Im z\<bar>" 0 z,
simplified])
fix k x
assume "x \<in> closed_segment 0 z" "k \<le> n"
@@ -2567,7 +2567,7 @@
using e by (simp add: field_simps)
then have "\<exists>xo>0. \<forall>x\<ge>xo. x / e < exp (Re s * x)"
using assms
- by (force intro: less_le_trans [OF _ exp_lower_taylor_quadratic])
+ by (force intro: less_le_trans [OF _ exp_lower_Taylor_quadratic])
then obtain xo where "xo > 0" and xo: "\<And>x. x \<ge> xo \<Longrightarrow> x < e * exp (Re s * x)"
using e by (auto simp: field_simps)
have "norm (Ln (of_nat n) / of_nat n powr s) < e" if "n \<ge> nat \<lceil>exp xo\<rceil>" for n
--- a/src/HOL/Analysis/Connected.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy Sat Dec 29 15:43:53 2018 +0100
@@ -5118,7 +5118,7 @@
\<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"
by (metis Inf_greatest closed_imp_fip compact_eq_bounded_closed empty_subsetI finite.emptyI inf.orderE)
-lemma closed_fip_heine_borel:
+lemma closed_fip_Heine_Borel:
fixes \<F> :: "'a::heine_borel set set"
assumes "closed S" "T \<in> \<F>" "bounded T"
and "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
@@ -5130,12 +5130,12 @@
then show ?thesis by simp
qed
-lemma compact_fip_heine_borel:
+lemma compact_fip_Heine_Borel:
fixes \<F> :: "'a::heine_borel set set"
assumes clof: "\<And>T. T \<in> \<F> \<Longrightarrow> compact T"
and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
shows "\<Inter>\<F> \<noteq> {}"
-by (metis InterI all_not_in_conv clof closed_fip_heine_borel compact_eq_bounded_closed none)
+by (metis InterI all_not_in_conv clof closed_fip_Heine_Borel compact_eq_bounded_closed none)
lemma compact_sequence_with_limit:
fixes f :: "nat \<Rightarrow> 'a::heine_borel"
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Sat Dec 29 15:43:53 2018 +0100
@@ -5757,7 +5757,7 @@
text "Formalized by Lars Schewe."
-lemma radon_ex_lemma:
+lemma Radon_ex_lemma:
assumes "finite c" "affine_dependent c"
shows "\<exists>u. sum u c = 0 \<and> (\<exists>v\<in>c. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) c = 0"
proof -
@@ -5772,7 +5772,7 @@
done
qed
-lemma radon_s_lemma:
+lemma Radon_s_lemma:
assumes "finite s"
and "sum f s = (0::real)"
shows "sum f {x\<in>s. 0 < f x} = - sum f {x\<in>s. f x < 0}"
@@ -5786,7 +5786,7 @@
by assumption
qed
-lemma radon_v_lemma:
+lemma Radon_v_lemma:
assumes "finite s"
and "sum f s = 0"
and "\<forall>x. g x = (0::real) \<longrightarrow> f x = (0::'a::euclidean_space)"
@@ -5802,12 +5802,12 @@
done
qed
-lemma radon_partition:
+lemma Radon_partition:
assumes "finite c" "affine_dependent c"
shows "\<exists>m p. m \<inter> p = {} \<and> m \<union> p = c \<and> (convex hull m) \<inter> (convex hull p) \<noteq> {}"
proof -
obtain u v where uv: "sum u c = 0" "v\<in>c" "u v \<noteq> 0" "(\<Sum>v\<in>c. u v *\<^sub>R v) = 0"
- using radon_ex_lemma[OF assms] by auto
+ using Radon_ex_lemma[OF assms] by auto
have fin: "finite {x \<in> c. 0 < u x}" "finite {x \<in> c. 0 > u x}"
using assms(1) by auto
define z where "z = inverse (sum u {x\<in>c. u x > 0}) *\<^sub>R sum (\<lambda>x. u x *\<^sub>R x) {x\<in>c. u x > 0}"
@@ -5879,7 +5879,7 @@
done
qed
-theorem radon:
+theorem Radon:
assumes "affine_dependent c"
obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
proof -
@@ -5889,7 +5889,7 @@
by blast
then have *: "finite s" "affine_dependent s" and s: "s \<subseteq> c"
unfolding affine_dependent_explicit by auto
- from radon_partition[OF *]
+ from Radon_partition[OF *]
obtain m p where "m \<inter> p = {}" "m \<union> p = s" "convex hull m \<inter> convex hull p \<noteq> {}"
by blast
then show ?thesis
@@ -5902,7 +5902,7 @@
subsection \<open>Helly's theorem\<close>
-lemma helly_induct:
+lemma Helly_induct:
fixes f :: "'a::euclidean_space set set"
assumes "card f = n"
and "n \<ge> DIM('a) + 1"
@@ -5947,7 +5947,7 @@
next
case True
then obtain m p where mp: "m \<inter> p = {}" "m \<union> p = X ` f" "convex hull m \<inter> convex hull p \<noteq> {}"
- using radon_partition[of "X ` f"] and affine_dependent_biggerset[of "X ` f"]
+ using Radon_partition[of "X ` f"] and affine_dependent_biggerset[of "X ` f"]
unfolding card_image[OF True] and \<open>card f = Suc n\<close>
using Suc(3) \<open>finite f\<close> and False
by auto
@@ -5973,12 +5973,12 @@
qed
qed
-theorem helly:
+theorem Helly:
fixes f :: "'a::euclidean_space set set"
assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
and "\<And>t. \<lbrakk>t\<subseteq>f; card t = DIM('a) + 1\<rbrakk> \<Longrightarrow> \<Inter>t \<noteq> {}"
shows "\<Inter>f \<noteq> {}"
- apply (rule helly_induct)
+ apply (rule Helly_induct)
using assms
apply auto
done
--- a/src/HOL/Analysis/Derivative.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy Sat Dec 29 15:43:53 2018 +0100
@@ -2325,7 +2325,7 @@
\<forall>x\<in>T \<inter> {t - 1<..<t + 1}. norm (?e n x) \<le> norm (A ^ (n + 1) /\<^sub>R fact (n + 1))"
by (auto simp: divide_simps power_abs intro!: mult_left_le_one_le power_le_one eventuallyI)
then have "uniform_limit (T \<inter> {t - 1<..<t + 1}) (\<lambda>n x. \<Sum>i<n. ?e i x) (\<lambda>x. \<Sum>i. ?e i x) sequentially"
- by (rule weierstrass_m_test_ev) (intro summable_ignore_initial_segment summable_norm_exp)
+ by (rule Weierstrass_m_test_ev) (intro summable_ignore_initial_segment summable_norm_exp)
moreover
have "\<forall>\<^sub>F x in sequentially. x > 0"
by (metis eventually_gt_at_top)
@@ -2333,7 +2333,7 @@
"\<forall>\<^sub>F n in sequentially. ((\<lambda>x. \<Sum>i<n. ?e i x) \<longlongrightarrow> A) ?F"
by eventually_elim
(auto intro!: tendsto_eq_intros
- simp: power_0_left if_distrib if_distribR sum.delta
+ simp: power_0_left if_distrib if_distribR
cong: if_cong)
ultimately
have [tendsto_intros]: "((\<lambda>x. \<Sum>i. ?e i x) \<longlongrightarrow> A) ?F"
--- a/src/HOL/Analysis/Elementary_Topology.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Sat Dec 29 15:43:53 2018 +0100
@@ -3090,7 +3090,7 @@
subsubsection \<open>Bolzano-Weierstrass property\<close>
-proposition heine_borel_imp_bolzano_weierstrass:
+proposition Heine_Borel_imp_Bolzano_Weierstrass:
assumes "compact s"
and "infinite t"
and "t \<subseteq> s"
@@ -3102,7 +3102,7 @@
using bchoice[of s "\<lambda> x T. x \<in> T \<and> open T \<and> (\<forall>y\<in>t. y \<in> T \<longrightarrow> y = x)"]
by auto
obtain g where g: "g \<subseteq> {t. \<exists>x. x \<in> s \<and> t = f x}" "finite g" "s \<subseteq> \<Union>g"
- using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]]
+ using assms(1)[unfolded compact_eq_Heine_Borel, THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]]
using f by auto
from g(1,3) have g':"\<forall>x\<in>g. \<exists>xa \<in> s. x = f xa"
by auto
@@ -3336,7 +3336,7 @@
by simp
qed
-lemma bolzano_weierstrass_imp_closed:
+lemma Bolzano_Weierstrass_imp_closed:
fixes s :: "'a::{first_countable_topology,t2_space} set"
assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
shows "closed s"
@@ -3386,10 +3386,10 @@
fix f
assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
from * \<open>compact s\<close> obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
- unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
+ unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
moreover
from * \<open>compact t\<close> obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
- unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
+ unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
by (auto intro!: exI[of _ "s' \<union> t'"])
qed
@@ -3416,7 +3416,7 @@
using assms by (intro compact_Int_closed compact_imp_closed)
lemma compact_sing [simp]: "compact {a}"
- unfolding compact_eq_heine_borel by auto
+ unfolding compact_eq_Heine_Borel by auto
lemma compact_insert [simp]:
assumes "compact s"
@@ -3571,7 +3571,7 @@
using assms unfolding countably_compact_def by metis
lemma compact_imp_countably_compact: "compact U \<Longrightarrow> countably_compact U"
- by (auto simp: compact_eq_heine_borel countably_compact_def)
+ by (auto simp: compact_eq_Heine_Borel countably_compact_def)
lemma countably_compact_imp_compact:
assumes "countably_compact U"
@@ -3579,7 +3579,7 @@
and basis: "\<And>T x. open T \<Longrightarrow> x \<in> T \<Longrightarrow> x \<in> U \<Longrightarrow> \<exists>b\<in>B. x \<in> b \<and> b \<inter> U \<subseteq> T"
shows "compact U"
using \<open>countably_compact U\<close>
- unfolding compact_eq_heine_borel countably_compact_def
+ unfolding compact_eq_Heine_Borel countably_compact_def
proof safe
fix A
assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
@@ -3886,7 +3886,7 @@
shows "seq_compact U \<longleftrightarrow> compact U"
using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
-proposition bolzano_weierstrass_imp_seq_compact:
+proposition Bolzano_Weierstrass_imp_seq_compact:
fixes s :: "'a::{t1_space, first_countable_topology} set"
shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
@@ -3929,7 +3929,7 @@
subsubsection\<open>Heine-Borel theorem\<close>
-proposition seq_compact_imp_heine_borel:
+proposition seq_compact_imp_Heine_Borel:
fixes s :: "'a :: metric_space set"
assumes "seq_compact s"
shows "compact s"
@@ -3976,7 +3976,7 @@
proposition compact_eq_seq_compact_metric:
"compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
- using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
+ using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast
proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
"compact (S :: 'a::metric_space set) \<longleftrightarrow>
@@ -3985,23 +3985,23 @@
subsubsection \<open>Complete the chain of compactness variants\<close>
-proposition compact_eq_bolzano_weierstrass:
+proposition compact_eq_Bolzano_Weierstrass:
fixes s :: "'a::metric_space set"
shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
- using heine_borel_imp_bolzano_weierstrass[of s] by auto
+ using Heine_Borel_imp_Bolzano_Weierstrass[of s] by auto
next
assume ?rhs
then show ?lhs
- unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
+ unfolding compact_eq_seq_compact_metric by (rule Bolzano_Weierstrass_imp_seq_compact)
qed
-proposition bolzano_weierstrass_imp_bounded:
+proposition Bolzano_Weierstrass_imp_bounded:
"\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
- using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
+ using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass .
subsection \<open>Metric spaces with the Heine-Borel property\<close>
--- a/src/HOL/Analysis/Gamma_Function.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Sat Dec 29 15:43:53 2018 +0100
@@ -552,7 +552,7 @@
shows "uniformly_convergent_on (ball z d)
(\<lambda>k z. \<Sum>i<k. inverse (of_nat (Suc i)) - inverse (z + of_nat (Suc i)))"
(is "uniformly_convergent_on _ (\<lambda>k z. \<Sum>i<k. ?f i z)")
-proof (rule weierstrass_m_test'_ev)
+proof (rule Weierstrass_m_test'_ev)
{
fix t assume t: "t \<in> ball z d"
have "norm z = norm (t + (z - t))" by simp
@@ -665,7 +665,7 @@
fixes z :: "'a :: {real_normed_field,banach}"
assumes z: "z \<noteq> 0" and n: "n \<ge> 2"
shows "uniformly_convergent_on (ball z d) (\<lambda>k z. \<Sum>i<k. inverse ((z + of_nat i)^n))"
-proof (rule weierstrass_m_test'_ev)
+proof (rule Weierstrass_m_test'_ev)
define e where "e = (1 + d / norm z)"
define m where "m = nat \<lceil>norm z * e\<rceil>"
{
@@ -2528,29 +2528,29 @@
subsubsection \<open>Weierstrass form\<close>
-definition Gamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
- "Gamma_series_weierstrass z n =
+definition Gamma_series_Weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
+ "Gamma_series_Weierstrass z n =
exp (-euler_mascheroni * z) / z * (\<Prod>k=1..n. exp (z / of_nat k) / (1 + z / of_nat k))"
definition%unimportant
- rGamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
- "rGamma_series_weierstrass z n =
+ rGamma_series_Weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
+ "rGamma_series_Weierstrass z n =
exp (euler_mascheroni * z) * z * (\<Prod>k=1..n. (1 + z / of_nat k) * exp (-z / of_nat k))"
-lemma Gamma_series_weierstrass_nonpos_Ints:
- "eventually (\<lambda>k. Gamma_series_weierstrass (- of_nat n) k = 0) sequentially"
- using eventually_ge_at_top[of n] by eventually_elim (auto simp: Gamma_series_weierstrass_def)
-
-lemma rGamma_series_weierstrass_nonpos_Ints:
- "eventually (\<lambda>k. rGamma_series_weierstrass (- of_nat n) k = 0) sequentially"
- using eventually_ge_at_top[of n] by eventually_elim (auto simp: rGamma_series_weierstrass_def)
-
-theorem Gamma_weierstrass_complex: "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
+lemma Gamma_series_Weierstrass_nonpos_Ints:
+ "eventually (\<lambda>k. Gamma_series_Weierstrass (- of_nat n) k = 0) sequentially"
+ using eventually_ge_at_top[of n] by eventually_elim (auto simp: Gamma_series_Weierstrass_def)
+
+lemma rGamma_series_Weierstrass_nonpos_Ints:
+ "eventually (\<lambda>k. rGamma_series_Weierstrass (- of_nat n) k = 0) sequentially"
+ using eventually_ge_at_top[of n] by eventually_elim (auto simp: rGamma_series_Weierstrass_def)
+
+theorem Gamma_Weierstrass_complex: "Gamma_series_Weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
case True
then obtain n where "z = - of_nat n" by (elim nonpos_Ints_cases')
- also from True have "Gamma_series_weierstrass \<dots> \<longlonglongrightarrow> Gamma z"
- by (simp add: tendsto_cong[OF Gamma_series_weierstrass_nonpos_Ints] Gamma_nonpos_Int)
+ also from True have "Gamma_series_Weierstrass \<dots> \<longlonglongrightarrow> Gamma z"
+ by (simp add: tendsto_cong[OF Gamma_series_Weierstrass_nonpos_Ints] Gamma_nonpos_Int)
finally show ?thesis .
next
case False
@@ -2565,32 +2565,32 @@
from tendsto_exp[OF this] False z have "?f \<longlonglongrightarrow> z * exp (euler_mascheroni * z) * Gamma z"
by (simp add: exp_add exp_sum exp_diff mult_ac Gamma_complex_altdef A)
from tendsto_mult[OF tendsto_const[of "exp (-euler_mascheroni * z) / z"] this] z
- show "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma z"
- by (simp add: exp_minus divide_simps Gamma_series_weierstrass_def [abs_def])
+ show "Gamma_series_Weierstrass z \<longlonglongrightarrow> Gamma z"
+ by (simp add: exp_minus divide_simps Gamma_series_Weierstrass_def [abs_def])
qed
lemma tendsto_complex_of_real_iff: "((\<lambda>x. complex_of_real (f x)) \<longlongrightarrow> of_real c) F = (f \<longlongrightarrow> c) F"
by (rule tendsto_of_real_iff)
-lemma Gamma_weierstrass_real: "Gamma_series_weierstrass x \<longlonglongrightarrow> Gamma (x :: real)"
- using Gamma_weierstrass_complex[of "of_real x"] unfolding Gamma_series_weierstrass_def[abs_def]
+lemma Gamma_Weierstrass_real: "Gamma_series_Weierstrass x \<longlonglongrightarrow> Gamma (x :: real)"
+ using Gamma_Weierstrass_complex[of "of_real x"] unfolding Gamma_series_Weierstrass_def[abs_def]
by (subst tendsto_complex_of_real_iff [symmetric])
(simp_all add: exp_of_real[symmetric] Gamma_complex_of_real)
-lemma rGamma_weierstrass_complex: "rGamma_series_weierstrass z \<longlonglongrightarrow> rGamma (z :: complex)"
+lemma rGamma_Weierstrass_complex: "rGamma_series_Weierstrass z \<longlonglongrightarrow> rGamma (z :: complex)"
proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
case True
then obtain n where "z = - of_nat n" by (elim nonpos_Ints_cases')
- also from True have "rGamma_series_weierstrass \<dots> \<longlonglongrightarrow> rGamma z"
- by (simp add: tendsto_cong[OF rGamma_series_weierstrass_nonpos_Ints] rGamma_nonpos_Int)
+ also from True have "rGamma_series_Weierstrass \<dots> \<longlonglongrightarrow> rGamma z"
+ by (simp add: tendsto_cong[OF rGamma_series_Weierstrass_nonpos_Ints] rGamma_nonpos_Int)
finally show ?thesis .
next
case False
- have "rGamma_series_weierstrass z = (\<lambda>n. inverse (Gamma_series_weierstrass z n))"
- by (simp add: rGamma_series_weierstrass_def[abs_def] Gamma_series_weierstrass_def
+ have "rGamma_series_Weierstrass z = (\<lambda>n. inverse (Gamma_series_Weierstrass z n))"
+ by (simp add: rGamma_series_Weierstrass_def[abs_def] Gamma_series_Weierstrass_def
exp_minus divide_inverse prod_inversef[symmetric] mult_ac)
also from False have "\<dots> \<longlonglongrightarrow> inverse (Gamma z)"
- by (intro tendsto_intros Gamma_weierstrass_complex) (simp add: Gamma_eq_zero_iff)
+ by (intro tendsto_intros Gamma_Weierstrass_complex) (simp add: Gamma_eq_zero_iff)
finally show ?thesis by (simp add: Gamma_def)
qed
@@ -3175,17 +3175,17 @@
fixes z :: complex
shows "(\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k^2)) \<longlonglongrightarrow> sin (of_real pi * z)"
proof -
- let ?f = "rGamma_series_weierstrass"
+ let ?f = "rGamma_series_Weierstrass"
have "(\<lambda>n. (- of_real pi * inverse z) * (?f z n * ?f (- z) n))
\<longlonglongrightarrow> (- of_real pi * inverse z) * (rGamma z * rGamma (- z))"
- by (intro tendsto_intros rGamma_weierstrass_complex)
+ by (intro tendsto_intros rGamma_Weierstrass_complex)
also have "(\<lambda>n. (- of_real pi * inverse z) * (?f z n * ?f (-z) n)) =
(\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2))"
proof
fix n :: nat
have "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) =
of_real pi * z * (\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2)"
- by (simp add: rGamma_series_weierstrass_def mult_ac exp_minus
+ by (simp add: rGamma_series_Weierstrass_def mult_ac exp_minus
divide_simps prod.distrib[symmetric] power2_eq_square)
also have "(\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2) =
(\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2)"
@@ -3257,7 +3257,7 @@
have "continuous_on (ball 0 1) f"
proof (rule uniform_limit_theorem; (intro always_eventually allI)?)
show "uniform_limit (ball 0 1) (\<lambda>n x. \<Sum>k<n. P x k / of_nat (Suc k)^2) f sequentially"
- proof (unfold f_def, rule weierstrass_m_test)
+ proof (unfold f_def, rule Weierstrass_m_test)
fix n :: nat and x :: real assume x: "x \<in> ball 0 1"
{
fix k :: nat assume k: "k \<ge> 1"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Dec 29 15:43:53 2018 +0100
@@ -2806,11 +2806,11 @@
(Df m has_vector_derivative Df (Suc m) t) (at t within {a..b})"
and ivl: "a \<le> b"
defines "i \<equiv> \<lambda>x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x"
- shows taylor_has_integral:
+ shows Taylor_has_integral:
"(i has_integral f b - (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a)) {a..b}"
- and taylor_integral:
+ and Taylor_integral:
"f b = (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
- and taylor_integrable:
+ and Taylor_integrable:
"i integrable_on {a..b}"
proof goal_cases
case 1
--- a/src/HOL/Analysis/Infinite_Products.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy Sat Dec 29 15:43:53 2018 +0100
@@ -254,7 +254,7 @@
by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent)
qed (auto intro: abs_convergent_prodI)
-lemma weierstrass_prod_ineq:
+lemma Weierstrass_prod_ineq:
fixes f :: "'a \<Rightarrow> real"
assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> {0..1}"
shows "1 - sum f A \<le> (\<Prod>x\<in>A. 1 - f x)"
@@ -576,7 +576,7 @@
proof (rule tendsto_le)
show "eventually (\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k+M+N) - 1)) \<le>
(\<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1))) at_top"
- using M by (intro always_eventually allI weierstrass_prod_ineq) (auto intro: less_imp_le)
+ using M by (intro always_eventually allI Weierstrass_prod_ineq) (auto intro: less_imp_le)
show "(\<lambda>n. \<Prod>k\<le>n. 1 - norm (f (k+M+N) - 1)) \<longlonglongrightarrow> 0" by fact
show "(\<lambda>n. 1 - (\<Sum>k\<le>n. norm (f (k + M + N) - 1)))
\<longlonglongrightarrow> 1 - (\<Sum>i. norm (f (i + M + N) - 1))"
--- a/src/HOL/Analysis/Starlike.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy Sat Dec 29 15:43:53 2018 +0100
@@ -5261,7 +5261,7 @@
qed
have "\<Inter>{{a. a \<in> K \<and> f a \<in> insert y (range (\<lambda>i. f(X(n + i))))} |n. n \<in> UNIV}
\<noteq> {}"
- apply (rule compact_fip_heine_borel)
+ apply (rule compact_fip_Heine_Borel)
using comf apply force
using ne apply (simp add: subset_iff del: insert_iff)
done
--- a/src/HOL/Analysis/Uniform_Limit.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy Sat Dec 29 15:43:53 2018 +0100
@@ -319,7 +319,7 @@
subsection \<open>Weierstrass M-Test\<close>
-proposition weierstrass_m_test_ev:
+proposition Weierstrass_m_test_ev:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially"
assumes "summable M"
@@ -375,28 +375,28 @@
using le eventually_sequentially by auto
show ?thesis
apply (rule_tac x="(\<lambda>x. \<Sum>i. f x i)" in exI)
- apply (metis (no_types, lifting) eventually_sequentially uniform_limitD [OF weierstrass_m_test_ev [OF 1 g]])
+ apply (metis (no_types, lifting) eventually_sequentially uniform_limitD [OF Weierstrass_m_test_ev [OF 1 g]])
done
qed
-corollary%unimportant weierstrass_m_test:
+corollary%unimportant Weierstrass_m_test:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
assumes "summable M"
shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
- using assms by (intro weierstrass_m_test_ev always_eventually) auto
+ using assms by (intro Weierstrass_m_test_ev always_eventually) auto
-corollary%unimportant weierstrass_m_test'_ev:
+corollary%unimportant Weierstrass_m_test'_ev:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially" "summable M"
shows "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
- unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])
+ unfolding uniformly_convergent_on_def by (rule exI, rule Weierstrass_m_test_ev[OF assms])
-corollary%unimportant weierstrass_m_test':
+corollary%unimportant Weierstrass_m_test':
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n" "summable M"
shows "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
- unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test[OF assms])
+ unfolding uniformly_convergent_on_def by (rule exI, rule Weierstrass_m_test[OF assms])
lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
by simp
@@ -714,7 +714,7 @@
using abs_summable_in_conv_radius [of "of_real r" a] assms
by (simp add: norm_mult norm_power)
show ?thesis
- by (simp add: weierstrass_m_test'_ev [OF _ *] norm_mult norm_power
+ by (simp add: Weierstrass_m_test'_ev [OF _ *] norm_mult norm_power
mult_left_mono power_mono dist_norm norm_minus_commute)
next
case False then show ?thesis by (simp add: not_le)
--- a/src/HOL/Analysis/document/root.tex Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Analysis/document/root.tex Sat Dec 29 15:43:53 2018 +0100
@@ -26,7 +26,7 @@
\newpage
-\renewcommand{\setisabellecontext}[1]{\markright{#1.thy}}
+\renewcommand{\setisabellecontext}[1]{\markright{\href{#1.html}{#1.thy}}}
\parindent 0pt\parskip 0.5ex
\input{session}
--- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy Sat Dec 29 15:43:53 2018 +0100
@@ -234,7 +234,7 @@
using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y"]
unfolding cmod_def by simp
-lemma bolzano_weierstrass_complex_disc:
+lemma Bolzano_Weierstrass_complex_disc:
assumes r: "\<forall>n. cmod (s n) \<le> r"
shows "\<exists>f z. strict_mono (f :: nat \<Rightarrow> nat) \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
proof -
@@ -399,7 +399,7 @@
from choice[OF th] obtain g where
g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
by blast
- from bolzano_weierstrass_complex_disc[OF g(1)]
+ from Bolzano_Weierstrass_complex_disc[OF g(1)]
obtain f z where fz: "strict_mono (f :: nat \<Rightarrow> nat)" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
by blast
{
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Sat Dec 29 15:43:53 2018 +0100
@@ -1259,7 +1259,7 @@
case False
have "lx \<le> real_of_float c" "real_of_float c \<le> ux" "lx \<le> xs!x" "xs!x \<le> ux"
using Suc bnd_c \<open>bounded_by xs vs\<close>[THEN bounded_byE, OF \<open>x < length vs\<close>] bnd_x by auto
- from taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
+ from Taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \<and> t < c else c < t \<and> t < xs ! x"
and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
(\<Sum>m = 0..<Suc n'. F m c / (fact m) * (xs ! x - c) ^ m) +
--- a/src/HOL/MacLaurin.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/MacLaurin.thy Sat Dec 29 15:43:53 2018 +0100
@@ -319,14 +319,14 @@
shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n"
using Maclaurin_all_le_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
-corollary exp_lower_taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
+corollary exp_lower_Taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
for x :: real
using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square)
corollary ln_2_less_1: "ln 2 < (1::real)"
proof -
have "2 < 5/(2::real)" by simp
- also have "5/2 \<le> exp (1::real)" using exp_lower_taylor_quadratic[of 1, simplified] by simp
+ also have "5/2 \<le> exp (1::real)" using exp_lower_Taylor_quadratic[of 1, simplified] by simp
finally have "exp (ln 2) < exp (1::real)" by simp
thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
qed
@@ -530,7 +530,7 @@
to prove Taylor's theorem.
\<close>
-lemma taylor_up:
+lemma Taylor_up:
assumes INIT: "n > 0" "diff 0 = f"
and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)"
and INTERV: "a \<le> c" "c < b"
@@ -565,7 +565,7 @@
then show ?thesis by fastforce
qed
-lemma taylor_down:
+lemma Taylor_down:
fixes a :: real and n :: nat
assumes INIT: "n > 0" "diff 0 = f"
and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)"
@@ -601,7 +601,7 @@
then show ?thesis by fastforce
qed
-theorem taylor:
+theorem Taylor:
fixes a :: real and n :: nat
assumes INIT: "n > 0" "diff 0 = f"
and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
@@ -619,7 +619,7 @@
by simp
ultimately have "\<exists>t>x. t < c \<and> f x =
(\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
- by (rule taylor_down)
+ by (rule Taylor_down)
with True show ?thesis by simp
next
case False
@@ -632,7 +632,7 @@
by arith
ultimately have "\<exists>t>c. t < x \<and> f x =
(\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
- by (rule taylor_up)
+ by (rule Taylor_up)
with False show ?thesis by simp
qed
--- a/src/HOL/Probability/Probability_Mass_Function.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Sat Dec 29 15:43:53 2018 +0100
@@ -848,7 +848,7 @@
by (simp add: sums_unique)
next
show "uniform_limit A (\<lambda>n a. \<Sum>i<n. ?f i a) (\<lambda>a. (\<Sum> n. ?f n a)) sequentially"
- proof (rule weierstrass_m_test)
+ proof (rule Weierstrass_m_test)
fix n a assume "a\<in>A"
then show "norm (?f n a) \<le> pmf (map_pmf (to_nat_on M) M) n * B"
using bnd by (auto intro!: mult_mono simp: from_nat_into set_pmf_not_empty)
--- a/src/HOL/Topological_Spaces.thy Fri Dec 28 19:01:35 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy Sat Dec 29 15:43:53 2018 +0100
@@ -2314,14 +2314,14 @@
context topological_space
begin
-definition compact :: "'a set \<Rightarrow> bool"
- where compact_eq_heine_borel: (* This name is used for backwards compatibility *)
+definition compact :: "'a set \<Rightarrow> bool" where
+compact_eq_Heine_Borel: (* This name is used for backwards compatibility *)
"compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
lemma compactI:
assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union>C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union>C'"
shows "compact s"
- unfolding compact_eq_heine_borel using assms by metis
+ unfolding compact_eq_Heine_Borel using assms by metis
lemma compact_empty[simp]: "compact {}"
by (auto intro!: compactI)
@@ -2329,7 +2329,7 @@
lemma compactE: (*related to COMPACT_IMP_HEINE_BOREL in HOL Light*)
assumes "compact S" "S \<subseteq> \<Union>\<T>" "\<And>B. B \<in> \<T> \<Longrightarrow> open B"
obtains \<T>' where "\<T>' \<subseteq> \<T>" "finite \<T>'" "S \<subseteq> \<Union>\<T>'"
- by (meson assms compact_eq_heine_borel)
+ by (meson assms compact_eq_Heine_Borel)
lemma compactE_image:
assumes "compact S"
@@ -2353,7 +2353,7 @@
moreover from cover have "S \<subseteq> \<Union>(C \<union> {- T})"
by auto
ultimately have "\<exists>D\<subseteq>C \<union> {- T}. finite D \<and> S \<subseteq> \<Union>D"
- using \<open>compact S\<close> unfolding compact_eq_heine_borel by auto
+ using \<open>compact S\<close> unfolding compact_eq_Heine_Borel by auto
then obtain D where "D \<subseteq> C \<union> {- T} \<and> finite D \<and> S \<subseteq> \<Union>D" ..
then show "\<exists>D\<subseteq>C. finite D \<and> S \<inter> T \<subseteq> \<Union>D"
by (intro exI[of _ "D - {-T}"]) auto
@@ -2372,7 +2372,7 @@
"compact U \<longleftrightarrow>
(\<forall>A. (\<forall>a\<in>A. closed a) \<longrightarrow> (\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}) \<longrightarrow> U \<inter> \<Inter>A \<noteq> {})"
(is "_ \<longleftrightarrow> ?R")
-proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
+proof (safe intro!: compact_eq_Heine_Borel[THEN iffD2])
fix A
assume "compact U"
assume A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
@@ -2380,7 +2380,7 @@
from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
by auto
with \<open>compact U\<close> obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
- unfolding compact_eq_heine_borel by (metis subset_image_iff)
+ unfolding compact_eq_Heine_Borel by (metis subset_image_iff)
with fin[THEN spec, of B] show False
by (auto dest: finite_imageD intro: inj_setminus)
next