--- a/src/HOL/Limits.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Limits.thy Tue Feb 23 15:47:39 2016 +0000
@@ -1534,10 +1534,6 @@
text\<open>Transformation of limit.\<close>
-lemma eventually_at2:
- "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
- unfolding eventually_at by auto
-
lemma Lim_transform:
fixes a b :: "'a::real_normed_vector"
shows "\<lbrakk>(g \<longlongrightarrow> a) F; ((\<lambda>x. f x - g x) \<longlongrightarrow> 0) F\<rbrakk> \<Longrightarrow> (f \<longlongrightarrow> a) F"
--- a/src/HOL/Meson.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Meson.thy Tue Feb 23 15:47:39 2016 +0000
@@ -93,7 +93,7 @@
subsection \<open>Lemmas for Forward Proof\<close>
-text\<open>There is a similarity to congruence rules\<close>
+text\<open>There is a similarity to congruence rules. They are also useful in ordinary proofs.\<close>
(*NOTE: could handle conjunctions (faster?) by
nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
@@ -103,6 +103,9 @@
lemma disj_forward: "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q"
by blast
+lemma imp_forward: "[| P' \<longrightarrow> Q'; P ==> P'; Q' ==> Q |] ==> P \<longrightarrow> Q"
+by blast
+
(*Version of @{text disj_forward} for removal of duplicate literals*)
lemma disj_forward2:
"[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q"
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Feb 23 15:47:39 2016 +0000
@@ -1998,7 +1998,7 @@
apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
apply (blast intro: brouwer_ball[OF assms])
apply (intro continuous_intros)
- unfolding frontier_cball subset_eq Ball_def image_iff dist_norm
+ unfolding frontier_cball subset_eq Ball_def image_iff dist_norm sphere_def
apply (auto simp add: ** norm_minus_commute)
done
then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Feb 23 15:47:39 2016 +0000
@@ -74,7 +74,7 @@
shows "continuous_on s exp"
by (simp add: continuous_on_exp continuous_on_id)
-lemma holomorphic_on_exp: "exp holomorphic_on s"
+lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s"
by (simp add: complex_differentiable_within_exp holomorphic_on_def)
subsection\<open>Euler and de Moivre formulas.\<close>
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Feb 23 15:47:39 2016 +0000
@@ -324,10 +324,24 @@
unfolding one_add_one [symmetric] scaleR_left_distrib by simp
lemma vector_choose_size:
- "0 \<le> c \<Longrightarrow> \<exists>x::'a::euclidean_space. norm x = c"
- apply (rule exI [where x="c *\<^sub>R (SOME i. i \<in> Basis)"])
- apply (auto simp: SOME_Basis)
- done
+ assumes "0 \<le> c"
+ obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c"
+proof -
+ obtain a::'a where "a \<noteq> 0"
+ using UNIV_not_singleton UNIV_eq_I set_zero singletonI by fastforce
+ then show ?thesis
+ by (rule_tac x="scaleR (c / norm a) a" in that) (simp add: assms)
+qed
+
+lemma vector_choose_dist:
+ assumes "0 \<le> c"
+ obtains y :: "'a::{real_normed_vector, perfect_space}" where "dist x y = c"
+by (metis add_diff_cancel_left' assms dist_commute dist_norm vector_choose_size)
+
+lemma sphere_eq_empty [simp]:
+ fixes a :: "'a::{real_normed_vector, perfect_space}"
+ shows "sphere a r = {} \<longleftrightarrow> r < 0"
+by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist)
lemma setsum_delta_notmem:
assumes "x \<notin> s"
@@ -4300,8 +4314,7 @@
and "\<forall>y\<in>s. dist a (closest_point s a) \<le> dist a y"
unfolding closest_point_def
apply(rule_tac[!] someI2_ex)
- using distance_attains_inf[OF assms(1,2), of a]
- apply auto
+ apply (auto intro: distance_attains_inf[OF assms(1,2), of a])
done
lemma closest_point_in_set: "closed s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> closest_point s a \<in> s"
@@ -4446,9 +4459,8 @@
and "z \<notin> s"
shows "\<exists>a b. \<exists>y\<in>s. inner a z < b \<and> inner a y = b \<and> (\<forall>x\<in>s. inner a x \<ge> b)"
proof -
- from distance_attains_inf[OF assms(2-3)]
obtain y where "y \<in> s" and y: "\<forall>x\<in>s. dist z y \<le> dist z x"
- by auto
+ by (metis distance_attains_inf[OF assms(2-3)])
show ?thesis
apply (rule_tac x="y - z" in exI)
apply (rule_tac x="inner (y - z) y" in exI)
@@ -4497,7 +4509,7 @@
next
case False
obtain y where "y \<in> s" and y: "\<forall>x\<in>s. dist z y \<le> dist z x"
- using distance_attains_inf[OF assms(2) False] by auto
+ by (metis distance_attains_inf[OF assms(2) False])
show ?thesis
apply (rule_tac x="y - z" in exI)
apply (rule_tac x="inner (y - z) z + (norm (y - z))\<^sup>2 / 2" in exI)
@@ -4657,16 +4669,8 @@
shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>s. 0 \<le> inner a x)"
proof -
let ?k = "\<lambda>c. {x::'a. 0 \<le> inner c x}"
- have "frontier (cball 0 1) \<inter> (\<Inter>(?k ` s)) \<noteq> {}"
- apply (rule compact_imp_fip)
- apply (rule compact_frontier[OF compact_cball])
- defer
- apply rule
- apply rule
- apply (erule conjE)
+ have *: "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" if as: "f \<subseteq> ?k ` s" "finite f" for f
proof -
- fix f
- assume as: "f \<subseteq> ?k ` s" "finite f"
obtain c where c: "f = ?k ` c" "c \<subseteq> s" "finite c"
using finite_subset_image[OF as(2,1)] by auto
then obtain a b where ab: "a \<noteq> 0" "0 < b" "\<forall>x\<in>convex hull c. b < inner a x"
@@ -4680,14 +4684,17 @@
unfolding subset_eq and inner_scaleR
by (auto simp add: inner_commute del: ballE elim!: ballE)
then show "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}"
- unfolding c(1) frontier_cball dist_norm by auto
- qed (insert closed_halfspace_ge, auto)
+ unfolding c(1) frontier_cball sphere_def dist_norm by auto
+ qed
+ have "frontier (cball 0 1) \<inter> (\<Inter>(?k ` s)) \<noteq> {}"
+ apply (rule compact_imp_fip)
+ apply (rule compact_frontier[OF compact_cball])
+ using * closed_halfspace_ge
+ by auto
then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y"
- unfolding frontier_cball dist_norm by auto
+ unfolding frontier_cball dist_norm sphere_def by auto
then show ?thesis
- apply (rule_tac x=x in exI)
- apply (auto simp add: inner_commute)
- done
+ by (metis inner_commute mem_Collect_eq norm_eq_zero zero_neq_one)
qed
lemma separating_hyperplane_sets:
@@ -9928,8 +9935,9 @@
using assms by blast
then
have "\<exists>x \<in> s. \<exists>y \<in> t. dist x y \<le> setdist s t"
- using distance_attains_inf [where a=0, OF compact_closed_differences [OF s t]] assms
- apply (clarsimp simp: dist_norm le_setdist_iff, blast)
+ apply (rule distance_attains_inf [where a=0, OF compact_closed_differences [OF s t]])
+ apply (simp add: dist_norm le_setdist_iff)
+ apply blast
done
then show ?thesis
by (blast intro!: antisym [OF _ setdist_le_dist] )
@@ -10009,5 +10017,4 @@
lemma setdist_le_sing: "x \<in> s ==> setdist s t \<le> setdist {x} t"
using setdist_subset_left by auto
-
end
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Feb 23 15:47:39 2016 +0000
@@ -1697,15 +1697,15 @@
also continuous. So if we know for some other reason that the inverse
function exists, it's OK.\<close>
-lemma has_derivative_locally_injective:
+proposition has_derivative_locally_injective:
fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes "a \<in> s"
- and "open s"
- and "bounded_linear g'"
- and "g' \<circ> f' a = id"
- and "\<forall>x\<in>s. (f has_derivative f' x) (at x)"
- and "\<forall>e>0. \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < e"
- obtains t where "a \<in> t" "open t" "\<forall>x\<in>t. \<forall>x'\<in>t. f x' = f x \<longrightarrow> x' = x"
+ and "open s"
+ and "bounded_linear g'"
+ and "g' \<circ> f' a = id"
+ and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x)"
+ and "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm (\<lambda>v. f' x v - f' a v) < e"
+ obtains r where "r > 0" "ball a r \<subseteq> s" "inj_on f (ball a r)"
proof -
interpret bounded_linear g'
using assms by auto
@@ -1738,9 +1738,11 @@
using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
show ?thesis
proof
- show "a \<in> ball a d"
- using d by auto
- show "\<forall>x\<in>ball a d. \<forall>x'\<in>ball a d. f x' = f x \<longrightarrow> x' = x"
+ show "0 < d" by (fact d)
+ show "ball a d \<subseteq> s"
+ using \<open>d < d2\<close> \<open>ball a d2 \<subseteq> s\<close> by auto
+ show "inj_on f (ball a d)"
+ unfolding inj_on_def
proof (intro strip)
fix x y
assume as: "x \<in> ball a d" "y \<in> ball a d" "f x = f y"
@@ -1749,7 +1751,7 @@
unfolding ph_def o_def
unfolding diff
using f'g'
- by (auto simp add: algebra_simps)
+ by (auto simp: algebra_simps)
have "norm (ph x - ph y) \<le> (1 / 2) * norm (x - y)"
apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
apply (rule_tac[!] ballI)
@@ -1788,7 +1790,7 @@
using d1(2)[of u]
using onorm_neg[where f="\<lambda>x. f' u x - f' a x"]
using d and u and onorm_pos_le[OF assms(3)]
- apply (auto simp add: algebra_simps)
+ apply (auto simp: algebra_simps)
done
also have "\<dots> \<le> 1 / 2"
unfolding k_def by auto
@@ -1804,7 +1806,7 @@
ultimately show "x = y"
unfolding norm_minus_commute by auto
qed
- qed auto
+ qed
qed
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Tue Feb 23 15:47:39 2016 +0000
@@ -1019,7 +1019,7 @@
shows "\<exists>e > 0. ball z e \<inter> path_image g = {}"
proof -
obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y"
- using distance_attains_inf[OF _ path_image_nonempty, of g z]
+ apply (rule distance_attains_inf[OF _ path_image_nonempty, of g z])
using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto
then show ?thesis
apply (rule_tac x="dist z a" in exI)
@@ -1661,6 +1661,50 @@
apply (auto simp: cball_diff_eq_sphere dist_norm)
done
+proposition connected_open_delete:
+ assumes "open S" "connected S" and 2: "2 \<le> DIM('N::euclidean_space)"
+ shows "connected(S - {a::'N})"
+proof (cases "a \<in> S")
+ case True
+ with \<open>open S\<close> obtain \<epsilon> where "\<epsilon> > 0" and \<epsilon>: "cball a \<epsilon> \<subseteq> S"
+ using open_contains_cball_eq by blast
+ have "dist a (a + \<epsilon> *\<^sub>R (SOME i. i \<in> Basis)) = \<epsilon>"
+ by (simp add: dist_norm SOME_Basis \<open>0 < \<epsilon>\<close> less_imp_le)
+ with \<epsilon> have "\<Inter>{S - ball a r |r. 0 < r \<and> r < \<epsilon>} \<subseteq> {} \<Longrightarrow> False"
+ apply (drule_tac c="a + scaleR (\<epsilon>) ((SOME i. i \<in> Basis))" in subsetD)
+ by auto
+ then have nonemp: "(\<Inter>{S - ball a r |r. 0 < r \<and> r < \<epsilon>}) = {} \<Longrightarrow> False"
+ by auto
+ have con: "\<And>r. r < \<epsilon> \<Longrightarrow> connected (S - ball a r)"
+ using \<epsilon> by (force intro: connected_diff_ball [OF \<open>connected S\<close> _ 2])
+ have "x \<in> \<Union>{S - ball a r |r. 0 < r \<and> r < \<epsilon>}" if "x \<in> S - {a}" for x
+ apply (rule UnionI [of "S - ball a (min \<epsilon> (dist a x) / 2)"])
+ using that \<open>0 < \<epsilon>\<close> apply (simp_all add:)
+ apply (rule_tac x="min \<epsilon> (dist a x) / 2" in exI)
+ apply auto
+ done
+ then have "S - {a} = \<Union>{S - ball a r | r. 0 < r \<and> r < \<epsilon>}"
+ by auto
+ then show ?thesis
+ by (auto intro: connected_Union con dest!: nonemp)
+next
+ case False then show ?thesis
+ by (simp add: \<open>connected S\<close>)
+qed
+
+corollary path_connected_open_delete:
+ assumes "open S" "connected S" and 2: "2 \<le> DIM('N::euclidean_space)"
+ shows "path_connected(S - {a::'N})"
+by (simp add: assms connected_open_delete connected_open_path_connected open_delete)
+
+corollary path_connected_punctured_ball:
+ "2 \<le> DIM('N::euclidean_space) \<Longrightarrow> path_connected(ball a r - {a::'N})"
+by (simp add: path_connected_open_delete)
+
+lemma connected_punctured_ball:
+ "2 \<le> DIM('N::euclidean_space) \<Longrightarrow> connected(ball a r - {a::'N})"
+by (simp add: connected_open_delete)
+
subsection\<open>Relations between components and path components\<close>
lemma open_connected_component:
@@ -1961,7 +2005,10 @@
lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)"
by (simp add: Int_commute frontier_def interior_closure)
-lemma connected_inter_frontier:
+lemma frontier_interior_subset: "frontier(interior S) \<subseteq> frontier S"
+ by (simp add: Diff_mono frontier_interiors interior_mono interior_subset)
+
+lemma connected_Int_frontier:
"\<lbrakk>connected s; s \<inter> t \<noteq> {}; s - t \<noteq> {}\<rbrakk> \<Longrightarrow> (s \<inter> frontier t \<noteq> {})"
apply (simp add: frontier_interiors connected_open_in, safe)
apply (drule_tac x="s \<inter> interior t" in spec, safe)
@@ -1969,6 +2016,44 @@
apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD])
done
+lemma frontier_not_empty:
+ fixes S :: "'a :: real_normed_vector set"
+ shows "\<lbrakk>S \<noteq> {}; S \<noteq> UNIV\<rbrakk> \<Longrightarrow> frontier S \<noteq> {}"
+ using connected_Int_frontier [of UNIV S] by auto
+
+lemma frontier_eq_empty:
+ fixes S :: "'a :: real_normed_vector set"
+ shows "frontier S = {} \<longleftrightarrow> S = {} \<or> S = UNIV"
+using frontier_UNIV frontier_empty frontier_not_empty by blast
+
+lemma frontier_of_connected_component_subset:
+ fixes S :: "'a::real_normed_vector set"
+ shows "frontier(connected_component_set S x) \<subseteq> frontier S"
+proof -
+ { fix y
+ assume y1: "y \<in> closure (connected_component_set S x)"
+ and y2: "y \<notin> interior (connected_component_set S x)"
+ have 1: "y \<in> closure S"
+ using y1 closure_mono connected_component_subset by blast
+ have "z \<in> interior (connected_component_set S x)"
+ if "0 < e" "ball y e \<subseteq> interior S" "dist y z < e" for e z
+ proof -
+ have "ball y e \<subseteq> connected_component_set S y"
+ apply (rule connected_component_maximal)
+ using that interior_subset mem_ball apply auto
+ done
+ then show ?thesis
+ using y1 apply (simp add: closure_approachable open_contains_ball_eq [OF open_interior])
+ by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in subsetD
+ dist_commute mem_Collect_eq mem_ball mem_interior \<open>0 < e\<close> y2)
+ qed
+ then have 2: "y \<notin> interior S"
+ using y2 by (force simp: open_contains_ball_eq [OF open_interior])
+ note 1 2
+ }
+ then show ?thesis by (auto simp: frontier_def)
+qed
+
lemma connected_component_UNIV:
fixes x :: "'a::real_normed_vector"
shows "connected_component_set UNIV x = UNIV"
@@ -1992,7 +2077,7 @@
assume x: "x \<in> interior s" and y: "y \<notin> s"
and cc: "connected_component (- frontier s) x y"
have "connected_component_set (- frontier s) x \<inter> frontier s \<noteq> {}"
- apply (rule connected_inter_frontier, simp)
+ apply (rule connected_Int_frontier, simp)
apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq set_rev_mp x)
using y cc
by blast
--- a/src/HOL/Multivariate_Analysis/Summation.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Summation.thy Tue Feb 23 15:47:39 2016 +0000
@@ -583,7 +583,6 @@
"conv_radius f = liminf (\<lambda>n. inverse (ereal (root n (norm (f n)))))"
by (subst Liminf_inverse_ereal) (simp_all add: real_root_ge_zero conv_radius_def)
-
lemma abs_summable_in_conv_radius:
fixes f :: "nat \<Rightarrow> 'a :: {banach, real_normed_div_algebra}"
assumes "ereal (norm z) < conv_radius f"
@@ -905,7 +904,16 @@
from r have "summable (\<lambda>n. (\<Sum>i\<le>n. (f i * of_real r^i) * (g (n - i) * of_real r^(n - i))))"
by (intro summable_Cauchy_product abs_summable_in_conv_radius) simp_all
thus "summable (\<lambda>n. (\<Sum>i\<le>n. f i * g (n - i)) * of_real r ^ n)"
- by (simp add: algebra_simps of_real_def scaleR_power power_add [symmetric] scaleR_setsum_right)
+ by (simp add: algebra_simps of_real_def power_add [symmetric] scaleR_setsum_right)
qed
+lemma le_conv_radius_iff:
+ fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
+ shows "r \<le> conv_radius a \<longleftrightarrow> (\<forall>x. norm (x-\<xi>) < r \<longrightarrow> summable (\<lambda>i. a i * (x - \<xi>) ^ i))"
+apply (intro iffI allI impI summable_in_conv_radius conv_radius_geI_ex)
+apply (meson less_ereal.simps(1) not_le order_trans)
+apply (rule_tac x="of_real ra" in exI, simp)
+apply (metis abs_of_nonneg add_diff_cancel_left' less_eq_real_def norm_of_real)
+done
+
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Feb 23 15:47:39 2016 +0000
@@ -897,12 +897,15 @@
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
+lemma openI [intro?]: "(\<And>x. x\<in>S \<Longrightarrow> \<exists>e>0. ball x e \<subseteq> S) \<Longrightarrow> open S"
+ by (auto simp: open_contains_ball)
+
lemma openE[elim?]:
assumes "open S" "x\<in>S"
obtains e where "e>0" "ball x e \<subseteq> S"
using assms unfolding open_contains_ball by auto
-lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
+lemma open_contains_ball_eq: "open S \<Longrightarrow> x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
by (metis open_contains_ball subset_eq centre_in_ball)
lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
@@ -2251,6 +2254,9 @@
using frontier_complement frontier_subset_eq[of "- S"]
unfolding open_closed by auto
+lemma frontier_UNIV [simp]: "frontier UNIV = {}"
+ using frontier_complement frontier_empty by fastforce
+
subsection \<open>Filters and the ``eventually true'' quantifier\<close>
@@ -2339,7 +2345,7 @@
lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
- by (auto simp add: tendsto_iff eventually_at2)
+ by (auto simp add: tendsto_iff eventually_at)
lemma Lim_at_infinity:
"(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
@@ -2355,6 +2361,23 @@
lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f \<longlongrightarrow> l) net"
by (rule topological_tendstoI, auto elim: eventually_mono)
+lemma Lim_transform_within_set:
+ fixes a l :: "'a::real_normed_vector"
+ shows "\<lbrakk>(f \<longlongrightarrow> l) (at a within s); eventually (\<lambda>x. x \<in> s \<longleftrightarrow> x \<in> t) (at a)\<rbrakk>
+ \<Longrightarrow> (f \<longlongrightarrow> l) (at a within t)"
+apply (clarsimp simp: eventually_at Lim_within)
+apply (drule_tac x=e in spec, clarify)
+apply (rename_tac k)
+apply (rule_tac x="min d k" in exI)
+apply (simp add:)
+done
+
+lemma Lim_transform_within_set_eq:
+ fixes a l :: "'a::real_normed_vector"
+ shows "eventually (\<lambda>x. x \<in> s \<longleftrightarrow> x \<in> t) (at a)
+ \<Longrightarrow> ((f \<longlongrightarrow> l) (at a within s) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within t))"
+by (force intro: Lim_transform_within_set elim: eventually_mono)
+
text\<open>The expected monotonicity property.\<close>
lemma Lim_Un:
@@ -2514,6 +2537,36 @@
using assms(1) tendsto_norm_zero [OF assms(2)]
by (rule Lim_null_comparison)
+lemma lim_null_mult_right_bounded:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra"
+ assumes f: "(f \<longlongrightarrow> 0) F" and g: "eventually (\<lambda>x. norm(g x) \<le> B) F"
+ shows "((\<lambda>z. f z * g z) \<longlongrightarrow> 0) F"
+proof -
+ have *: "((\<lambda>x. norm (f x) * B) \<longlongrightarrow> 0) F"
+ by (simp add: f tendsto_mult_left_zero tendsto_norm_zero)
+ have "((\<lambda>x. norm (f x) * norm (g x)) \<longlongrightarrow> 0) F"
+ apply (rule Lim_null_comparison [OF _ *])
+ apply (simp add: eventually_mono [OF g] mult_left_mono)
+ done
+ then show ?thesis
+ by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult)
+qed
+
+lemma lim_null_mult_left_bounded:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_div_algebra"
+ assumes g: "eventually (\<lambda>x. norm(g x) \<le> B) F" and f: "(f \<longlongrightarrow> 0) F"
+ shows "((\<lambda>z. g z * f z) \<longlongrightarrow> 0) F"
+proof -
+ have *: "((\<lambda>x. B * norm (f x)) \<longlongrightarrow> 0) F"
+ by (simp add: f tendsto_mult_right_zero tendsto_norm_zero)
+ have "((\<lambda>x. norm (g x) * norm (f x)) \<longlongrightarrow> 0) F"
+ apply (rule Lim_null_comparison [OF _ *])
+ apply (simp add: eventually_mono [OF g] mult_right_mono)
+ done
+ then show ?thesis
+ by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult)
+qed
+
text\<open>Deducing things about the limit from the elements.\<close>
lemma Lim_in_closed_set:
@@ -3149,21 +3202,18 @@
by auto
qed
-lemma frontier_ball:
+lemma interior_ball [simp]: "interior (ball x e) = ball x e"
+ by (simp add: interior_open)
+
+lemma frontier_ball [simp]:
fixes a :: "'a::real_normed_vector"
- shows "0 < e \<Longrightarrow> frontier(ball a e) = {x. dist a x = e}"
- apply (simp add: frontier_def closure_ball interior_open order_less_imp_le)
- apply (simp add: set_eq_iff)
- apply arith
- done
-
-lemma frontier_cball:
+ shows "0 < e \<Longrightarrow> frontier (ball a e) = sphere a e"
+ by (force simp: frontier_def)
+
+lemma frontier_cball [simp]:
fixes a :: "'a::{real_normed_vector, perfect_space}"
- shows "frontier (cball a e) = {x. dist a x = e}"
- apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le)
- apply (simp add: set_eq_iff)
- apply arith
- done
+ shows "frontier (cball a e) = sphere a e"
+ by (force simp: frontier_def)
lemma cball_eq_empty [simp]: "cball x e = {} \<longleftrightarrow> e < 0"
apply (simp add: set_eq_iff not_le)
@@ -3340,7 +3390,7 @@
lemma bounded_diff[intro]: "bounded S \<Longrightarrow> bounded (S - T)"
by (metis Diff_subset bounded_subset)
-lemma not_bounded_UNIV[simp, intro]:
+lemma not_bounded_UNIV[simp]:
"\<not> bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)"
proof (auto simp add: bounded_pos not_le)
obtain x :: 'a where "x \<noteq> 0"
@@ -4446,6 +4496,11 @@
shows "\<lbrakk>compact s; c \<in> components s\<rbrakk> \<Longrightarrow> compact c"
by (meson bounded_subset closed_components in_components_subset compact_eq_bounded_closed)
+lemma not_compact_UNIV[simp]:
+ fixes s :: "'a::{real_normed_vector,perfect_space,heine_borel} set"
+ shows "~ compact (UNIV::'a set)"
+ by (simp add: compact_eq_bounded_closed)
+
(* TODO: is this lemma necessary? *)
lemma bounded_increasing_convergent:
fixes s :: "nat \<Rightarrow> real"
@@ -4927,12 +4982,17 @@
using compact_eq_bounded_closed compact_frontier_bounded
by blast
+corollary compact_sphere:
+ fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}"
+ shows "compact (sphere a r)"
+using compact_frontier [of "cball a r"] by simp
+
lemma frontier_subset_compact:
fixes s :: "'a::heine_borel set"
shows "compact s \<Longrightarrow> frontier s \<subseteq> s"
using frontier_subset_closed compact_eq_bounded_closed
by blast
-
+
subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
lemma summable_imp_bounded:
@@ -5757,11 +5817,12 @@
lemma continuous_constant_on_closure:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
- assumes "continuous_on (closure s) f"
- and "\<forall>x \<in> s. f x = a"
- shows "\<forall>x \<in> (closure s). f x = a"
- using continuous_closed_preimage_constant[of "closure s" f a]
- assms closure_minimal[of s "{x \<in> closure s. f x = a}"] closure_subset
+ assumes "continuous_on (closure S) f"
+ and "\<And>x. x \<in> S \<Longrightarrow> f x = a"
+ and "x \<in> closure S"
+ shows "f x = a"
+ using continuous_closed_preimage_constant[of "closure S" f a]
+ assms closure_minimal[of S "{x \<in> closure S. f x = a}"] closure_subset
unfolding subset_eq
by auto
@@ -5851,6 +5912,27 @@
qed
qed
+subsection \<open>A function constant on a set\<close>
+
+definition constant_on (infixl "(constant'_on)" 50)
+ where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
+
+lemma constant_on_subset: "\<lbrakk>f constant_on A; B \<subseteq> A\<rbrakk> \<Longrightarrow> f constant_on B"
+ unfolding constant_on_def by blast
+
+lemma injective_not_constant:
+ fixes S :: "'a::{perfect_space} set"
+ shows "\<lbrakk>open S; inj_on f S; f constant_on S\<rbrakk> \<Longrightarrow> S = {}"
+unfolding constant_on_def
+by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)
+
+lemma constant_on_closureI:
+ fixes f :: "_ \<Rightarrow> 'b::t1_space"
+ assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"
+ shows "f constant_on (closure S)"
+using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
+by metis
+
text \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
lemma continuous_within_avoid:
@@ -6317,25 +6399,24 @@
lemma distance_attains_inf:
fixes a :: "'a::heine_borel"
- assumes "closed s"
- and "s \<noteq> {}"
- shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a x \<le> dist a y"
+ assumes "closed s" and "s \<noteq> {}"
+ obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
proof -
- from assms(2) obtain b where "b \<in> s" by auto
+ from assms obtain b where "b \<in> s" by auto
let ?B = "s \<inter> cball a (dist b a)"
have "?B \<noteq> {}" using \<open>b \<in> s\<close>
- by (auto simp add: dist_commute)
+ by (auto simp: dist_commute)
moreover have "continuous_on ?B (dist a)"
by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_at_id continuous_const)
moreover have "compact ?B"
by (intro closed_inter_compact \<open>closed s\<close> compact_cball)
ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
by (metis continuous_attains_inf)
- then show ?thesis by fastforce
-qed
-
-
-subsection \<open>Pasted sets\<close>
+ with that show ?thesis by fastforce
+qed
+
+
+subsection \<open>Cartesian products\<close>
lemma bounded_Times:
assumes "bounded s" "bounded t"
@@ -6746,8 +6827,7 @@
lemma separate_point_closed:
fixes s :: "'a::heine_borel set"
- assumes "closed s"
- and "a \<notin> s"
+ assumes "closed s" and "a \<notin> s"
shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"
proof (cases "s = {}")
case True
@@ -6755,7 +6835,7 @@
next
case False
from assms obtain x where "x\<in>s" "\<forall>y\<in>s. dist a x \<le> dist a y"
- using \<open>s \<noteq> {}\<close> distance_attains_inf [of s a] by blast
+ using \<open>s \<noteq> {}\<close> by (blast intro: distance_attains_inf [of s a])
with \<open>x\<in>s\<close> show ?thesis using dist_pos_lt[of a x] and\<open>a \<notin> s\<close>
by blast
qed
@@ -7893,9 +7973,8 @@
let ?S'' = "{x::'a. norm x = norm a}"
have "?S'' = frontier(cball 0 (norm a))"
- unfolding frontier_cball and dist_norm by auto
- then have "compact ?S''"
- using compact_frontier[OF compact_cball, of 0 "norm a"] by auto
+ by (simp add: sphere_def dist_norm)
+ then have "compact ?S''" by (metis compact_cball compact_frontier)
moreover have "?S' = s \<inter> ?S''" by auto
ultimately have "compact ?S'"
using closed_inter_compact[of s ?S''] using s(1) by auto
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Tue Feb 23 15:47:39 2016 +0000
@@ -6,7 +6,7 @@
section \<open>Uniform Limit and Uniform Convergence\<close>
theory Uniform_Limit
-imports Topology_Euclidean_Space
+imports Topology_Euclidean_Space Summation
begin
definition uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
@@ -45,12 +45,12 @@
lemma uniform_limit_at_iff:
"uniform_limit S f l (at x) \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>z. 0 < dist z x \<and> dist z x < d \<longrightarrow> (\<forall>x\<in>S. dist (f z x) (l x) < e))"
- unfolding uniform_limit_iff eventually_at2 ..
+ unfolding uniform_limit_iff eventually_at by simp
lemma uniform_limit_at_le_iff:
"uniform_limit S f l (at x) \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>z. 0 < dist z x \<and> dist z x < d \<longrightarrow> (\<forall>x\<in>S. dist (f z x) (l x) \<le> e))"
- unfolding uniform_limit_iff eventually_at2
+ unfolding uniform_limit_iff eventually_at
by (fastforce dest: spec[where x = "e / 2" for e])
lemma swap_uniform_limit:
@@ -189,6 +189,9 @@
lemma uniformly_convergentI: "uniform_limit X f l sequentially \<Longrightarrow> uniformly_convergent_on X f"
unfolding uniformly_convergent_on_def by blast
+lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
+ by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)
+
lemma Cauchy_uniformly_convergent:
fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: complete_space"
assumes "uniformly_Cauchy_on X f"
@@ -472,7 +475,7 @@
"uniform_limit I f g F \<Longrightarrow> uniform_limit J f g F \<Longrightarrow> uniform_limit (I \<union> J) f g F"
by (auto intro!: uniform_limitI dest!: uniform_limitD elim: eventually_elim2)
-lemma uniform_limit_on_empty:
+lemma uniform_limit_on_empty [iff]:
"uniform_limit {} f g F"
by (auto intro!: uniform_limitI)
@@ -509,4 +512,46 @@
unfolding uniformly_convergent_on_def
by (blast dest: bounded_linear_uniform_limit_intros(13))
+subsection\<open>Power series and uniform convergence\<close>
+
+proposition powser_uniformly_convergent:
+ fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
+ assumes "r < conv_radius a"
+ shows "uniformly_convergent_on (cball \<xi> r) (\<lambda>n x. \<Sum>i<n. a i * (x - \<xi>) ^ i)"
+proof (cases "0 \<le> r")
+ case True
+ then have *: "summable (\<lambda>n. norm (a n) * r ^ n)"
+ 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
+ mult_left_mono power_mono dist_norm norm_minus_commute)
+next
+ case False then show ?thesis by (simp add: not_le)
+qed
+
+lemma powser_uniform_limit:
+ fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
+ assumes "r < conv_radius a"
+ shows "uniform_limit (cball \<xi> r) (\<lambda>n x. \<Sum>i<n. a i * (x - \<xi>) ^ i) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i)) sequentially"
+using powser_uniformly_convergent [OF assms]
+by (simp add: Uniform_Limit.uniformly_convergent_uniform_limit_iff Series.suminf_eq_lim)
+
+lemma powser_continuous_suminf:
+ fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
+ assumes "r < conv_radius a"
+ shows "continuous_on (cball \<xi> r) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i))"
+apply (rule uniform_limit_theorem [OF _ powser_uniform_limit])
+apply (rule eventuallyI continuous_intros assms)+
+apply (simp add:)
+done
+
+lemma powser_continuous_sums:
+ fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
+ assumes r: "r < conv_radius a"
+ and sm: "\<And>x. x \<in> cball \<xi> r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
+ shows "continuous_on (cball \<xi> r) f"
+apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
+using sm sums_unique by fastforce
+
end
\ No newline at end of file
--- a/src/HOL/NthRoot.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/NthRoot.thy Tue Feb 23 15:47:39 2016 +0000
@@ -405,6 +405,9 @@
lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
+lemma real_less_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y\<^sup>2 \<Longrightarrow> sqrt x < y"
+ using real_sqrt_less_iff[of x "y\<^sup>2"] by simp
+
lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y"
using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
--- a/src/HOL/Series.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Series.thy Tue Feb 23 15:47:39 2016 +0000
@@ -357,9 +357,12 @@
thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast
qed (auto simp: sums_Suc_iff summable_def)
+lemma sums_Suc_imp: "f 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
+ using sums_Suc_iff by simp
+
end
-context
+context --\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
begin
@@ -393,6 +396,11 @@
corollary sums_iff_shift': "(\<lambda>i. f (i + n)) sums (s - (\<Sum>i<n. f i)) \<longleftrightarrow> f sums s"
by (simp add: sums_iff_shift)
+lemma sums_zero_iff_shift:
+ assumes "\<And>i. i < n \<Longrightarrow> f i = 0"
+ shows "(\<lambda>i. f (i+n)) sums s \<longleftrightarrow> (\<lambda>i. f i) sums s"
+by (simp add: assms sums_iff_shift)
+
lemma summable_iff_shift: "summable (\<lambda>n. f (n + k)) \<longleftrightarrow> summable f"
by (metis diff_add_cancel summable_def sums_iff_shift[abs_def])
--- a/src/HOL/Topological_Spaces.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Topological_Spaces.thy Tue Feb 23 15:47:39 2016 +0000
@@ -194,6 +194,9 @@
class perfect_space = topological_space +
assumes not_open_singleton: "\<not> open {x}"
+lemma UNIV_not_singleton: "UNIV \<noteq> {x::'a::perfect_space}"
+ by (metis open_UNIV not_open_singleton)
+
subsection \<open>Generators for toplogies\<close>
--- a/src/HOL/Transcendental.thy Mon Feb 22 14:37:56 2016 +0000
+++ b/src/HOL/Transcendental.thy Tue Feb 23 15:47:39 2016 +0000
@@ -472,10 +472,6 @@
lemma diffs_minus: "diffs (\<lambda>n. - c n) = (\<lambda>n. - diffs c n)"
by (simp add: diffs_def)
-lemma sums_Suc_imp:
- "(f::nat \<Rightarrow> 'a::real_normed_vector) 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
- using sums_Suc_iff[of f] by simp
-
lemma diffs_equiv:
fixes x :: "'a::{real_normed_vector, ring_1}"
shows "summable (\<lambda>n. diffs c n * x^n) \<Longrightarrow>