--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Jan 04 16:18:50 2017 +0000
@@ -3271,165 +3271,6 @@
by (force simp: L contour_integral_integral)
qed
-subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
-
-text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
-
-lemma continuous_disconnected_range_constant:
- assumes s: "connected s"
- and conf: "continuous_on s f"
- and fim: "f ` s \<subseteq> t"
- and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
- shows "\<exists>a. \<forall>x \<in> s. f x = a"
-proof (cases "s = {}")
- case True then show ?thesis by force
-next
- case False
- { fix x assume "x \<in> s"
- then have "f ` s \<subseteq> {f x}"
- by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
- }
- with False show ?thesis
- by blast
-qed
-
-lemma discrete_subset_disconnected:
- fixes s :: "'a::topological_space set"
- fixes t :: "'b::real_normed_vector set"
- assumes conf: "continuous_on s f"
- and no: "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
- shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
-proof -
- { fix x assume x: "x \<in> s"
- then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> s; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
- using conf no [OF x] by auto
- then have e2: "0 \<le> e / 2"
- by simp
- have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
- apply (rule ccontr)
- using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
- apply (simp add: del: ex_simps)
- apply (drule spec [where x="cball (f x) (e / 2)"])
- apply (drule spec [where x="- ball(f x) e"])
- apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in)
- apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
- using centre_in_cball connected_component_refl_eq e2 x apply blast
- using ccs
- apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
- done
- moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
- by (auto simp: connected_component_in)
- ultimately have "connected_component_set (f ` s) (f x) = {f x}"
- by (auto simp: x)
- }
- with assms show ?thesis
- by blast
-qed
-
-lemma finite_implies_discrete:
- fixes s :: "'a::topological_space set"
- assumes "finite (f ` s)"
- shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
-proof -
- have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
- proof (cases "f ` s - {f x} = {}")
- case True
- with zero_less_numeral show ?thesis
- by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
- next
- case False
- then obtain z where z: "z \<in> s" "f z \<noteq> f x"
- by blast
- have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
- using assms by simp
- then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
- apply (rule finite_imp_less_Inf)
- using z apply force+
- done
- show ?thesis
- by (force intro!: * cInf_le_finite [OF finn])
- qed
- with assms show ?thesis
- by blast
-qed
-
-text\<open>This proof requires the existence of two separate values of the range type.\<close>
-lemma finite_range_constant_imp_connected:
- assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
- \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
- shows "connected s"
-proof -
- { fix t u
- assume clt: "closedin (subtopology euclidean s) t"
- and clu: "closedin (subtopology euclidean s) u"
- and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
- have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
- apply (subst tus [symmetric])
- apply (rule continuous_on_cases_local)
- using clt clu tue
- apply (auto simp: tus continuous_on_const)
- done
- have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
- by (rule finite_subset [of _ "{0,1}"]) auto
- have "t = {} \<or> u = {}"
- using assms [OF conif fi] tus [symmetric]
- by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
- }
- then show ?thesis
- by (simp add: connected_closedin_eq)
-qed
-
-lemma continuous_disconnected_range_constant_eq:
- "(connected s \<longleftrightarrow>
- (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
- \<forall>t. continuous_on s f \<and> f ` s \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
- \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis1)
- and continuous_discrete_range_constant_eq:
- "(connected s \<longleftrightarrow>
- (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
- continuous_on s f \<and>
- (\<forall>x \<in> s. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> s \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
- \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis2)
- and continuous_finite_range_constant_eq:
- "(connected s \<longleftrightarrow>
- (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
- continuous_on s f \<and> finite (f ` s)
- \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis3)
-proof -
- have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
- \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
- by blast
- have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
- apply (rule *)
- using continuous_disconnected_range_constant apply metis
- apply clarify
- apply (frule discrete_subset_disconnected; blast)
- apply (blast dest: finite_implies_discrete)
- apply (blast intro!: finite_range_constant_imp_connected)
- done
- then show ?thesis1 ?thesis2 ?thesis3
- by blast+
-qed
-
-lemma continuous_discrete_range_constant:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
- assumes s: "connected s"
- and "continuous_on s f"
- and "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
- shows "\<exists>a. \<forall>x \<in> s. f x = a"
- using continuous_discrete_range_constant_eq [THEN iffD1, OF s] assms
- by blast
-
-lemma continuous_finite_range_constant:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
- assumes "connected s"
- and "continuous_on s f"
- and "finite (f ` s)"
- shows "\<exists>a. \<forall>x \<in> s. f x = a"
- using assms continuous_finite_range_constant_eq
- by blast
-
-
text\<open>We can treat even non-rectifiable paths as having a "length" for bounds on analytic functions in open sets.\<close>
subsection\<open>Winding Numbers\<close>
--- a/src/HOL/Analysis/Complex_Transcendental.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Wed Jan 04 16:18:50 2017 +0000
@@ -6,6 +6,7 @@
imports
Complex_Analysis_Basics
Summation_Tests
+ "~~/src/HOL/Library/Periodic_Fun"
begin
(* TODO: Figure out what to do with Möbius transformations *)
@@ -400,6 +401,89 @@
apply (simp add: real_sqrt_mult)
done
+
+lemma complex_sin_eq:
+ fixes w :: complex
+ shows "sin w = sin z \<longleftrightarrow> (\<exists>n \<in> \<int>. w = z + of_real(2*n*pi) \<or> w = -z + of_real((2*n + 1)*pi))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "sin w - sin z = 0"
+ by (auto simp: algebra_simps)
+ then have "sin ((w - z) / 2)*cos ((w + z) / 2) = 0"
+ by (auto simp: sin_diff_sin)
+ then consider "sin ((w - z) / 2) = 0" | "cos ((w + z) / 2) = 0"
+ using mult_eq_0_iff by blast
+ then show ?rhs
+ proof cases
+ case 1
+ then show ?thesis
+ apply (auto simp: sin_eq_0 algebra_simps)
+ by (metis Ints_of_int of_real_of_int_eq)
+ next
+ case 2
+ then show ?thesis
+ apply (auto simp: cos_eq_0 algebra_simps)
+ by (metis Ints_of_int of_real_of_int_eq)
+ qed
+next
+ assume ?rhs
+ then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \<or>
+ w = -z + of_real ((2* of_int n + 1)*pi)"
+ using Ints_cases by blast
+ then show ?lhs
+ using Periodic_Fun.sin.plus_of_int [of z n]
+ apply (auto simp: algebra_simps)
+ by (metis (no_types, hide_lams) add_diff_cancel_left add_diff_cancel_left' add_minus_cancel
+ mult.commute sin.plus_of_int sin_minus sin_plus_pi)
+qed
+
+lemma complex_cos_eq:
+ fixes w :: complex
+ shows "cos w = cos z \<longleftrightarrow>
+ (\<exists>n \<in> \<int>. w = z + of_real(2*n*pi) \<or> w = -z + of_real(2*n*pi))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "cos w - cos z = 0"
+ by (auto simp: algebra_simps)
+ then have "sin ((w + z) / 2) * sin ((z - w) / 2) = 0"
+ by (auto simp: cos_diff_cos)
+ then consider "sin ((w + z) / 2) = 0" | "sin ((z - w) / 2) = 0"
+ using mult_eq_0_iff by blast
+ then show ?rhs
+ proof cases
+ case 1
+ then show ?thesis
+ apply (auto simp: sin_eq_0 algebra_simps)
+ by (metis Ints_of_int of_real_of_int_eq)
+ next
+ case 2
+ then show ?thesis
+ apply (auto simp: sin_eq_0 algebra_simps)
+ by (metis Ints_of_int add_minus_cancel distrib_right mult_of_int_commute mult_zero_right of_int_0 of_int_add of_real_of_int_eq)
+ qed
+next
+ assume ?rhs
+ then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \<or>
+ w = -z + of_real(2*n*pi)"
+ using Ints_cases by (metis of_int_mult of_int_numeral)
+ then show ?lhs
+ using Periodic_Fun.cos.plus_of_int [of z n]
+ apply (auto simp: algebra_simps)
+ by (metis cos.plus_of_int cos_minus minus_add_cancel mult.commute)
+qed
+
+lemma sin_eq:
+ "sin x = sin y \<longleftrightarrow> (\<exists>n \<in> \<int>. x = y + 2*n*pi \<or> x = -y + (2*n + 1)*pi)"
+ using complex_sin_eq [of x y]
+ by (simp only: sin_of_real Re_complex_of_real of_real_add [symmetric] of_real_minus [symmetric] of_real_mult [symmetric] of_real_eq_iff)
+
+lemma cos_eq:
+ "cos x = cos y \<longleftrightarrow> (\<exists>n \<in> \<int>. x = y + 2*n*pi \<or> x = -y + 2*n*pi)"
+ using complex_cos_eq [of x y]
+ by (simp only: cos_of_real Re_complex_of_real of_real_add [symmetric] of_real_minus [symmetric] of_real_mult [symmetric] of_real_eq_iff)
+
lemma sinh_complex:
fixes z :: complex
shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
@@ -2837,6 +2921,19 @@
lemma Re_Arccos_bound: "\<bar>Re(Arccos z)\<bar> \<le> pi"
by (meson Re_Arccos_bounds abs_le_iff less_eq_real_def minus_less_iff)
+lemma Im_Arccos_bound: "\<bar>Im (Arccos w)\<bar> \<le> cmod w"
+proof -
+ have "(Im (Arccos w))\<^sup>2 \<le> (cmod (cos (Arccos w)))\<^sup>2 - (cos (Re (Arccos w)))\<^sup>2"
+ using norm_cos_squared [of "Arccos w"] real_le_abs_sinh [of "Im (Arccos w)"]
+ apply (simp only: abs_le_square_iff)
+ apply (simp add: divide_simps)
+ done
+ also have "... \<le> (cmod w)\<^sup>2"
+ by (auto simp: cmod_power2)
+ finally show ?thesis
+ using abs_le_square_iff by force
+qed
+
lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
unfolding Re_Arcsin
by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
@@ -2844,6 +2941,21 @@
lemma Re_Arcsin_bound: "\<bar>Re(Arcsin z)\<bar> \<le> pi"
by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
+lemma norm_Arccos_bounded:
+ fixes w :: complex
+ shows "norm (Arccos w) \<le> pi + norm w"
+proof -
+ have Re: "(Re (Arccos w))\<^sup>2 \<le> pi\<^sup>2" "(Im (Arccos w))\<^sup>2 \<le> (cmod w)\<^sup>2"
+ using Re_Arccos_bound [of w] Im_Arccos_bound [of w] abs_le_square_iff by force+
+ have "Arccos w \<bullet> Arccos w \<le> pi\<^sup>2 + (cmod w)\<^sup>2"
+ using Re by (simp add: dot_square_norm cmod_power2 [of "Arccos w"])
+ then have "cmod (Arccos w) \<le> pi + cmod (cos (Arccos w))"
+ apply (simp add: norm_le_square)
+ by (metis dot_square_norm norm_ge_zero norm_le_square pi_ge_zero triangle_lemma)
+ then show "cmod (Arccos w) \<le> pi + cmod w"
+ by auto
+qed
+
subsection\<open>Interrelations between Arcsin and Arccos\<close>
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Jan 04 16:18:50 2017 +0000
@@ -14,6 +14,20 @@
"~~/src/HOL/Library/Set_Algebras"
begin
+lemma swap_continuous: (*move to Topological_Spaces?*)
+ assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
+ shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
+proof -
+ have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
+ by auto
+ then show ?thesis
+ apply (rule ssubst)
+ apply (rule continuous_on_compose)
+ apply (simp add: split_def)
+ apply (rule continuous_intros | simp add: assms)+
+ done
+qed
+
lemma dim_image_eq:
fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
assumes lf: "linear f"
@@ -4651,7 +4665,7 @@
ultimately show ?thesis by auto
qed
-lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
+lemma interior_atLeastAtMost_real [simp]: "interior {a..b} = {a<..<b :: real}"
proof-
have "{a..b} = {a..} \<inter> {..b}" by auto
also have "interior ... = {a<..} \<inter> {..<b}"
@@ -4660,12 +4674,15 @@
finally show ?thesis .
qed
-lemma frontier_real_Iic:
+lemma interior_greaterThanLessThan_real [simp]: "interior {a<..<b} = {a<..<b :: real}"
+ by (metis interior_atLeastAtMost_real interior_interior)
+
+lemma frontier_real_Iic [simp]:
fixes a :: real
shows "frontier {..a} = {a}"
unfolding frontier_def by (auto simp add: interior_real_semiline')
-lemma rel_interior_real_box:
+lemma rel_interior_real_box [simp]:
fixes a b :: real
assumes "a < b"
shows "rel_interior {a .. b} = {a <..< b}"
@@ -4679,7 +4696,7 @@
by (simp split: if_split_asm del: box_real add: box_real[symmetric] interior_cbox)
qed
-lemma rel_interior_real_semiline:
+lemma rel_interior_real_semiline [simp]:
fixes a :: real
shows "rel_interior {a..} = {a<..}"
proof -
@@ -6596,7 +6613,7 @@
apply rule
apply rule
apply (erule conjE)
- apply (rule ccontr)
+ apply (rule ccontr)
proof -
fix a b x
assume as: "connected s" "a \<in> s" "b \<in> s" "a \<le> x" "x \<le> b" "x \<notin> s"
@@ -6630,6 +6647,10 @@
shows "is_interval s \<longleftrightarrow> convex s"
by (metis is_interval_convex convex_connected is_interval_connected_1)
+lemma connected_compact_interval_1:
+ "connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})"
+ by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
+
lemma connected_convex_1:
fixes s :: "real set"
shows "connected s \<longleftrightarrow> convex s"
@@ -7315,6 +7336,12 @@
unfolding midpoint_def scaleR_2 [symmetric] by simp
qed
+lemma
+ fixes a::real
+ assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
+ and le_midpoint_1: "midpoint a b \<le> b"
+ by (simp_all add: midpoint_def assms)
+
lemma dist_midpoint:
fixes a b :: "'a::real_normed_vector" shows
"dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
@@ -7535,7 +7562,7 @@
proof -
have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
using \<open>u \<le> 1\<close> by force
- then show ?thesis
+ then show ?thesis
by (simp add: dist_norm real_vector.scale_right_diff_distrib)
qed
also have "... \<le> dist a b"
@@ -7639,6 +7666,19 @@
shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b"
by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
+lemma segment_to_closest_point:
+ fixes S :: "'a :: euclidean_space set"
+ shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}"
+ apply (subst disjoint_iff_not_equal)
+ apply (clarify dest!: dist_in_open_segment)
+ by (metis closest_point_le dist_commute le_less_trans less_irrefl)
+
+lemma segment_to_point_exists:
+ fixes S :: "'a :: euclidean_space set"
+ assumes "closed S" "S \<noteq> {}"
+ obtains b where "b \<in> S" "open_segment a b \<inter> S = {}"
+ by (metis assms segment_to_closest_point closest_point_exists that)
+
subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
lemma segment_eq_compose:
@@ -8243,6 +8283,71 @@
finally show "(1 - u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" .
qed
+lemma closure_open_Int_superset:
+ assumes "open S" "S \<subseteq> closure T"
+ shows "closure(S \<inter> T) = closure S"
+proof -
+ have "closure S \<subseteq> closure(S \<inter> T)"
+ by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
+ then show ?thesis
+ by (simp add: closure_mono dual_order.antisym)
+qed
+
+lemma convex_closure_interior:
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S" and int: "interior S \<noteq> {}"
+ shows "closure(interior S) = closure S"
+proof -
+ obtain a where a: "a \<in> interior S"
+ using int by auto
+ have "closure S \<subseteq> closure(interior S)"
+ proof
+ fix x
+ assume x: "x \<in> closure S"
+ show "x \<in> closure (interior S)"
+ proof (cases "x=a")
+ case True
+ then show ?thesis
+ using \<open>a \<in> interior S\<close> closure_subset by blast
+ next
+ case False
+ show ?thesis
+ proof (clarsimp simp add: closure_def islimpt_approachable)
+ fix e::real
+ assume xnotS: "x \<notin> interior S" and "0 < e"
+ show "\<exists>x'\<in>interior S. x' \<noteq> x \<and> dist x' x < e"
+ proof (intro bexI conjI)
+ show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<noteq> x"
+ using False \<open>0 < e\<close> by (auto simp: algebra_simps min_def)
+ show "dist (x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a)) x < e"
+ using \<open>0 < e\<close> by (auto simp: dist_norm min_def)
+ show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<in> interior S"
+ apply (clarsimp simp add: min_def a)
+ apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x])
+ using \<open>0 < e\<close> False apply (auto simp: divide_simps)
+ done
+ qed
+ qed
+ qed
+ qed
+ then show ?thesis
+ by (simp add: closure_mono interior_subset subset_antisym)
+qed
+
+lemma closure_convex_Int_superset:
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S" "interior S \<noteq> {}" "interior S \<subseteq> closure T"
+ shows "closure(S \<inter> T) = closure S"
+proof -
+ have "closure S \<subseteq> closure(interior S)"
+ by (simp add: convex_closure_interior assms)
+ also have "... \<subseteq> closure (S \<inter> T)"
+ using interior_subset [of S] assms
+ by (metis (no_types, lifting) Int_assoc Int_lower2 closure_mono closure_open_Int_superset inf.orderE open_interior)
+ finally show ?thesis
+ by (simp add: closure_mono dual_order.antisym)
+qed
+
subsection \<open>Some obvious but surprisingly hard simplex lemmas\<close>
@@ -14406,4 +14511,78 @@
using paracompact_closedin [of UNIV S \<C>] assms
by (auto simp: open_openin [symmetric] closed_closedin [symmetric])
+
+subsection\<open>Closed-graph characterization of continuity\<close>
+
+lemma continuous_closed_graph_gen:
+ fixes T :: "'b::real_normed_vector set"
+ assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
+ shows "closedin (subtopology euclidean (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"
+proof -
+ have eq: "((\<lambda>x. Pair x (f x)) ` S) = {z. z \<in> S \<times> T \<and> (f \<circ> fst)z - snd z \<in> {0}}"
+ using fim by auto
+ show ?thesis
+ apply (subst eq)
+ apply (intro continuous_intros continuous_closedin_preimage continuous_on_subset [OF contf])
+ by auto
+qed
+
+lemma continuous_closed_graph_eq:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "compact T" and fim: "f ` S \<subseteq> T"
+ shows "continuous_on S f \<longleftrightarrow>
+ closedin (subtopology euclidean (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"
+ (is "?lhs = ?rhs")
+proof -
+ have "?lhs" if ?rhs
+ proof (clarsimp simp add: continuous_on_closed_gen [OF fim])
+ fix U
+ assume U: "closedin (subtopology euclidean T) U"
+ have eq: "{x. x \<in> S \<and> f x \<in> U} = fst ` (((\<lambda>x. Pair x (f x)) ` S) \<inter> (S \<times> U))"
+ by (force simp: image_iff)
+ show "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
+ by (simp add: U closedin_Int closedin_Times closed_map_fst [OF \<open>compact T\<close>] that eq)
+ qed
+ with continuous_closed_graph_gen assms show ?thesis by blast
+qed
+
+lemma continuous_closed_graph:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ assumes "closed S" and contf: "continuous_on S f"
+ shows "closed ((\<lambda>x. Pair x (f x)) ` S)"
+ apply (rule closedin_closed_trans)
+ apply (rule continuous_closed_graph_gen [OF contf subset_UNIV])
+ by (simp add: \<open>closed S\<close> closed_Times)
+
+lemma continuous_from_closed_graph:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "compact T" and fim: "f ` S \<subseteq> T" and clo: "closed ((\<lambda>x. Pair x (f x)) ` S)"
+ shows "continuous_on S f"
+ using fim clo
+ by (auto intro: closed_subset simp: continuous_closed_graph_eq [OF \<open>compact T\<close> fim])
+
+lemma continuous_on_Un_local_open:
+ assumes opS: "openin (subtopology euclidean (S \<union> T)) S"
+ and opT: "openin (subtopology euclidean (S \<union> T)) T"
+ and contf: "continuous_on S f" and contg: "continuous_on T f"
+ shows "continuous_on (S \<union> T) f"
+using pasting_lemma [of "{S,T}" "S \<union> T" "\<lambda>i. i" "\<lambda>i. f" f] contf contg opS opT by blast
+
+lemma continuous_on_cases_local_open:
+ assumes opS: "openin (subtopology euclidean (S \<union> T)) S"
+ and opT: "openin (subtopology euclidean (S \<union> T)) T"
+ and contf: "continuous_on S f" and contg: "continuous_on T g"
+ and fg: "\<And>x. x \<in> S \<and> ~P x \<or> x \<in> T \<and> P x \<Longrightarrow> f x = g x"
+ shows "continuous_on (S \<union> T) (\<lambda>x. if P x then f x else g x)"
+proof -
+ have "\<And>x. x \<in> S \<Longrightarrow> (if P x then f x else g x) = f x" "\<And>x. x \<in> T \<Longrightarrow> (if P x then f x else g x) = g x"
+ by (simp_all add: fg)
+ then have "continuous_on S (\<lambda>x. if P x then f x else g x)" "continuous_on T (\<lambda>x. if P x then f x else g x)"
+ by (simp_all add: contf contg cong: continuous_on_cong)
+ then show ?thesis
+ by (rule continuous_on_Un_local_open [OF opS opT])
+qed
+
+
+
end
--- a/src/HOL/Analysis/Euclidean_Space.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy Wed Jan 04 16:18:50 2017 +0000
@@ -53,6 +53,9 @@
lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis"
by (metis ex_in_conv nonempty_Basis someI_ex)
+lemma norm_some_Basis [simp]: "norm (SOME i. i \<in> Basis) = 1"
+ by (simp add: SOME_Basis)
+
lemma (in euclidean_space) inner_sum_left_Basis[simp]:
"b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b"
by (simp add: inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.If_cases)
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jan 04 16:18:50 2017 +0000
@@ -10,21 +10,6 @@
begin
(* BEGIN MOVE *)
-lemma swap_continuous:
- assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
- shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
-proof -
- have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
- by auto
- then show ?thesis
- apply (rule ssubst)
- apply (rule continuous_on_compose)
- apply (simp add: split_def)
- apply (rule continuous_intros | simp add: assms)+
- done
-qed
-
-
lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)"
by (simp add: norm_minus_eqI)
@@ -44,10 +29,6 @@
lemma Sigma_Int_Paircomp2: "(Sigma A B) \<inter> {(x, y). P y} = Sigma A (\<lambda>z. B z \<inter> {y. P y})"
by blast
-
-lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
- using nonempty_Basis
- by (fastforce simp add: set_eq_iff mem_box)
(* END MOVE *)
subsection \<open>Content (length, area, volume...) of an interval.\<close>
@@ -6191,7 +6172,6 @@
apply (rule le_less_trans[of _ "sum (\<lambda>x. k / (real (card r) + 1)) r"])
unfolding sum_subtractf[symmetric]
apply (rule sum_norm_le)
- apply rule
apply (drule qq)
defer
unfolding divide_inverse sum_distrib_right[symmetric]
@@ -6536,7 +6516,7 @@
m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2"
apply (rule le_less_trans[of _ "sum (\<lambda>i. e / 2^(i+2)) {0..s}"])
apply (rule sum_norm_le)
- proof
+ proof -
show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
unfolding power_add divide_inverse inverse_mult_distrib
unfolding sum_distrib_left[symmetric] sum_distrib_right[symmetric]
--- a/src/HOL/Analysis/Homeomorphism.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy Wed Jan 04 16:18:50 2017 +0000
@@ -1112,19 +1112,19 @@
lemma homeomorphic_convex_compact_lemma:
- fixes s :: "'a::euclidean_space set"
- assumes "convex s"
- and "compact s"
- and "cball 0 1 \<subseteq> s"
- shows "s homeomorphic (cball (0::'a) 1)"
+ fixes S :: "'a::euclidean_space set"
+ assumes "convex S"
+ and "compact S"
+ and "cball 0 1 \<subseteq> S"
+ shows "S homeomorphic (cball (0::'a) 1)"
proof (rule starlike_compact_projective_special[OF assms(2-3)])
fix x u
- assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
+ assume "x \<in> S" and "0 \<le> u" and "u < (1::real)"
have "open (ball (u *\<^sub>R x) (1 - u))"
by (rule open_ball)
moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
unfolding centre_in_ball using \<open>u < 1\<close> by simp
- moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
+ moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> S"
proof
fix y
assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
@@ -1132,32 +1132,32 @@
unfolding mem_ball .
with \<open>u < 1\<close> have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
- with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
- with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
- using \<open>x \<in> s\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
- then show "y \<in> s" using \<open>u < 1\<close>
+ with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> S" ..
+ with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> S"
+ using \<open>x \<in> S\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
+ then show "y \<in> S" using \<open>u < 1\<close>
by simp
qed
- ultimately have "u *\<^sub>R x \<in> interior s" ..
- then show "u *\<^sub>R x \<in> s - frontier s"
+ ultimately have "u *\<^sub>R x \<in> interior S" ..
+ then show "u *\<^sub>R x \<in> S - frontier S"
using frontier_def and interior_subset by auto
qed
proposition homeomorphic_convex_compact_cball:
fixes e :: real
- and s :: "'a::euclidean_space set"
- assumes "convex s"
- and "compact s"
- and "interior s \<noteq> {}"
+ and S :: "'a::euclidean_space set"
+ assumes "convex S"
+ and "compact S"
+ and "interior S \<noteq> {}"
and "e > 0"
- shows "s homeomorphic (cball (b::'a) e)"
+ shows "S homeomorphic (cball (b::'a) e)"
proof -
- obtain a where "a \<in> interior s"
+ obtain a where "a \<in> interior S"
using assms(3) by auto
- then obtain d where "d > 0" and d: "cball a d \<subseteq> s"
+ then obtain d where "d > 0" and d: "cball a d \<subseteq> S"
unfolding mem_interior_cball by auto
let ?d = "inverse d" and ?n = "0::'a"
- have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` s"
+ have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` S"
apply rule
apply (rule_tac x="d *\<^sub>R x + a" in image_eqI)
defer
@@ -1166,25 +1166,25 @@
unfolding mem_cball dist_norm
apply (auto simp add: mult_right_le_one_le)
done
- then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` s homeomorphic cball ?n 1"
- using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
+ then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` S homeomorphic cball ?n 1"
+ using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` S",
OF convex_affinity compact_affinity]
using assms(1,2)
by (auto simp add: scaleR_right_diff_distrib)
then show ?thesis
apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
- apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
+ apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" S "?d *\<^sub>R -a"]])
using \<open>d>0\<close> \<open>e>0\<close>
apply (auto simp add: scaleR_right_diff_distrib)
done
qed
corollary homeomorphic_convex_compact:
- fixes s :: "'a::euclidean_space set"
- and t :: "'a set"
- assumes "convex s" "compact s" "interior s \<noteq> {}"
- and "convex t" "compact t" "interior t \<noteq> {}"
- shows "s homeomorphic t"
+ fixes S :: "'a::euclidean_space set"
+ and T :: "'a set"
+ assumes "convex S" "compact S" "interior S \<noteq> {}"
+ and "convex T" "compact T" "interior T \<noteq> {}"
+ shows "S homeomorphic T"
using assms
by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
@@ -1193,31 +1193,31 @@
definition covering_space
:: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
where
- "covering_space c p s \<equiv>
- continuous_on c p \<and> p ` c = s \<and>
- (\<forall>x \<in> s. \<exists>t. x \<in> t \<and> openin (subtopology euclidean s) t \<and>
- (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> t} \<and>
+ "covering_space c p S \<equiv>
+ continuous_on c p \<and> p ` c = S \<and>
+ (\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (subtopology euclidean S) T \<and>
+ (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> T} \<and>
(\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
pairwise disjnt v \<and>
- (\<forall>u \<in> v. \<exists>q. homeomorphism u t p q)))"
+ (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
-lemma covering_space_imp_continuous: "covering_space c p s \<Longrightarrow> continuous_on c p"
+lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
by (simp add: covering_space_def)
-lemma covering_space_imp_surjective: "covering_space c p s \<Longrightarrow> p ` c = s"
+lemma covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
by (simp add: covering_space_def)
-lemma homeomorphism_imp_covering_space: "homeomorphism s t f g \<Longrightarrow> covering_space s f t"
+lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
apply (simp add: homeomorphism_def covering_space_def, clarify)
- apply (rule_tac x=t in exI, simp)
- apply (rule_tac x="{s}" in exI, auto)
+ apply (rule_tac x=T in exI, simp)
+ apply (rule_tac x="{S}" in exI, auto)
done
lemma covering_space_local_homeomorphism:
- assumes "covering_space c p s" "x \<in> c"
- obtains t u q where "x \<in> t" "openin (subtopology euclidean c) t"
- "p x \<in> u" "openin (subtopology euclidean s) u"
- "homeomorphism t u p q"
+ assumes "covering_space c p S" "x \<in> c"
+ obtains T u q where "x \<in> T" "openin (subtopology euclidean c) T"
+ "p x \<in> u" "openin (subtopology euclidean S) u"
+ "homeomorphism T u p q"
using assms
apply (simp add: covering_space_def, clarify)
apply (drule_tac x="p x" in bspec, force)
@@ -1225,11 +1225,11 @@
lemma covering_space_local_homeomorphism_alt:
- assumes p: "covering_space c p s" and "y \<in> s"
- obtains x t u q where "p x = y"
- "x \<in> t" "openin (subtopology euclidean c) t"
- "y \<in> u" "openin (subtopology euclidean s) u"
- "homeomorphism t u p q"
+ assumes p: "covering_space c p S" and "y \<in> S"
+ obtains x T u q where "p x = y"
+ "x \<in> T" "openin (subtopology euclidean c) T"
+ "y \<in> u" "openin (subtopology euclidean S) u"
+ "homeomorphism T u p q"
proof -
obtain x where "p x = y" "x \<in> c"
using assms covering_space_imp_surjective by blast
@@ -1239,50 +1239,50 @@
qed
proposition covering_space_open_map:
- fixes s :: "'a :: metric_space set" and t :: "'b :: metric_space set"
- assumes p: "covering_space c p s" and t: "openin (subtopology euclidean c) t"
- shows "openin (subtopology euclidean s) (p ` t)"
+ fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set"
+ assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T"
+ shows "openin (subtopology euclidean S) (p ` T)"
proof -
- have pce: "p ` c = s"
+ have pce: "p ` c = S"
and covs:
- "\<And>x. x \<in> s \<Longrightarrow>
- \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean s) X \<and>
+ "\<And>x. x \<in> S \<Longrightarrow>
+ \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean S) X \<and>
\<Union>VS = {x. x \<in> c \<and> p x \<in> X} \<and>
(\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and>
pairwise disjnt VS \<and>
(\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
using p by (auto simp: covering_space_def)
- have "t \<subseteq> c" by (metis openin_euclidean_subtopology_iff t)
- have "\<exists>T. openin (subtopology euclidean s) T \<and> y \<in> T \<and> T \<subseteq> p ` t"
- if "y \<in> p ` t" for y
+ have "T \<subseteq> c" by (metis openin_euclidean_subtopology_iff T)
+ have "\<exists>X. openin (subtopology euclidean S) X \<and> y \<in> X \<and> X \<subseteq> p ` T"
+ if "y \<in> p ` T" for y
proof -
- have "y \<in> s" using \<open>t \<subseteq> c\<close> pce that by blast
- obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean s) U"
+ have "y \<in> S" using \<open>T \<subseteq> c\<close> pce that by blast
+ obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean S) U"
and VS: "\<Union>VS = {x. x \<in> c \<and> p x \<in> U}"
and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V"
and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
- using covs [OF \<open>y \<in> s\<close>] by auto
- obtain x where "x \<in> c" "p x \<in> U" "x \<in> t" "p x = y"
+ using covs [OF \<open>y \<in> S\<close>] by auto
+ obtain x where "x \<in> c" "p x \<in> U" "x \<in> T" "p x = y"
apply simp
- using t [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` t\<close> by blast
+ using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast
with VS obtain V where "x \<in> V" "V \<in> VS" by auto
then obtain q where q: "homeomorphism V U p q" using homVS by blast
- then have ptV: "p ` (t \<inter> V) = U \<inter> {z. q z \<in> (t \<inter> V)}"
+ then have ptV: "p ` (T \<inter> V) = U \<inter> {z. q z \<in> (T \<inter> V)}"
using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
have ocv: "openin (subtopology euclidean c) V"
by (simp add: \<open>V \<in> VS\<close> openVS)
- have "openin (subtopology euclidean U) {z \<in> U. q z \<in> t \<inter> V}"
+ have "openin (subtopology euclidean U) {z \<in> U. q z \<in> T \<inter> V}"
apply (rule continuous_on_open [THEN iffD1, rule_format])
using homeomorphism_def q apply blast
- using openin_subtopology_Int_subset [of c] q t unfolding homeomorphism_def
+ using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def
by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
- then have os: "openin (subtopology euclidean s) (U \<inter> {z. q z \<in> t \<inter> V})"
+ then have os: "openin (subtopology euclidean S) (U \<inter> {z. q z \<in> T \<inter> V})"
using openin_trans [of U] by (simp add: Collect_conj_eq U)
show ?thesis
- apply (rule_tac x = "p ` (t \<inter> V)" in exI)
+ apply (rule_tac x = "p ` (T \<inter> V)" in exI)
apply (rule conjI)
apply (simp only: ptV os)
- using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> t\<close> apply blast
+ using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> T\<close> apply blast
done
qed
with openin_subopen show ?thesis by blast
@@ -1291,73 +1291,73 @@
lemma covering_space_lift_unique_gen:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
- assumes cov: "covering_space c p s"
+ assumes cov: "covering_space c p S"
and eq: "g1 a = g2 a"
- and f: "continuous_on t f" "f ` t \<subseteq> s"
- and g1: "continuous_on t g1" "g1 ` t \<subseteq> c"
- and fg1: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
- and g2: "continuous_on t g2" "g2 ` t \<subseteq> c"
- and fg2: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
- and u_compt: "u \<in> components t" and "a \<in> u" "x \<in> u"
+ and f: "continuous_on T f" "f ` T \<subseteq> S"
+ and g1: "continuous_on T g1" "g1 ` T \<subseteq> c"
+ and fg1: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
+ and g2: "continuous_on T g2" "g2 ` T \<subseteq> c"
+ and fg2: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
+ and u_compt: "U \<in> components T" and "a \<in> U" "x \<in> U"
shows "g1 x = g2 x"
proof -
- have "u \<subseteq> t" by (rule in_components_subset [OF u_compt])
- def G12 \<equiv> "{x \<in> u. g1 x - g2 x = 0}"
- have "connected u" by (rule in_components_connected [OF u_compt])
- have contu: "continuous_on u g1" "continuous_on u g2"
- using \<open>u \<subseteq> t\<close> continuous_on_subset g1 g2 by blast+
- have o12: "openin (subtopology euclidean u) G12"
+ have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
+ def G12 \<equiv> "{x \<in> U. g1 x - g2 x = 0}"
+ have "connected U" by (rule in_components_connected [OF u_compt])
+ have contu: "continuous_on U g1" "continuous_on U g2"
+ using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+
+ have o12: "openin (subtopology euclidean U) G12"
unfolding G12_def
proof (subst openin_subopen, clarify)
fix z
- assume z: "z \<in> u" "g1 z - g2 z = 0"
+ assume z: "z \<in> U" "g1 z - g2 z = 0"
obtain v w q where "g1 z \<in> v" and ocv: "openin (subtopology euclidean c) v"
- and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean s) w"
+ and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean S) w"
and hom: "homeomorphism v w p q"
apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov])
- using \<open>u \<subseteq> t\<close> \<open>z \<in> u\<close> g1(2) apply blast+
+ using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+
done
have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
- have gg: "{x \<in> u. g x \<in> v} = {x \<in> u. g x \<in> (v \<inter> g ` u)}" for g
+ have gg: "{x \<in> U. g x \<in> v} = {x \<in> U. g x \<in> (v \<inter> g ` U)}" for g
by auto
- have "openin (subtopology euclidean (g1 ` u)) (v \<inter> g1 ` u)"
- using ocv \<open>u \<subseteq> t\<close> g1 by (fastforce simp add: openin_open)
- then have 1: "openin (subtopology euclidean u) {x \<in> u. g1 x \<in> v}"
+ have "openin (subtopology euclidean (g1 ` U)) (v \<inter> g1 ` U)"
+ using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open)
+ then have 1: "openin (subtopology euclidean U) {x \<in> U. g1 x \<in> v}"
unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
- have "openin (subtopology euclidean (g2 ` u)) (v \<inter> g2 ` u)"
- using ocv \<open>u \<subseteq> t\<close> g2 by (fastforce simp add: openin_open)
- then have 2: "openin (subtopology euclidean u) {x \<in> u. g2 x \<in> v}"
+ have "openin (subtopology euclidean (g2 ` U)) (v \<inter> g2 ` U)"
+ using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open)
+ then have 2: "openin (subtopology euclidean U) {x \<in> U. g2 x \<in> v}"
unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
- show "\<exists>T. openin (subtopology euclidean u) T \<and>
- z \<in> T \<and> T \<subseteq> {z \<in> u. g1 z - g2 z = 0}"
+ show "\<exists>T. openin (subtopology euclidean U) T \<and>
+ z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
using z
- apply (rule_tac x = "{x. x \<in> u \<and> g1 x \<in> v} \<inter> {x. x \<in> u \<and> g2 x \<in> v}" in exI)
+ apply (rule_tac x = "{x. x \<in> U \<and> g1 x \<in> v} \<inter> {x. x \<in> U \<and> g2 x \<in> v}" in exI)
apply (intro conjI)
apply (rule openin_Int [OF 1 2])
using \<open>g1 z \<in> v\<close> \<open>g2 z \<in> v\<close> apply (force simp:, clarify)
- apply (metis \<open>u \<subseteq> t\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
+ apply (metis \<open>U \<subseteq> T\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
done
qed
- have c12: "closedin (subtopology euclidean u) G12"
+ have c12: "closedin (subtopology euclidean U) G12"
unfolding G12_def
by (intro continuous_intros continuous_closedin_preimage_constant contu)
- have "G12 = {} \<or> G12 = u"
- by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected u\<close> conjI o12 c12)
- with eq \<open>a \<in> u\<close> have "\<And>x. x \<in> u \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
+ have "G12 = {} \<or> G12 = U"
+ by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected U\<close> conjI o12 c12)
+ with eq \<open>a \<in> U\<close> have "\<And>x. x \<in> U \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
then show ?thesis
- using \<open>x \<in> u\<close> by force
+ using \<open>x \<in> U\<close> by force
qed
proposition covering_space_lift_unique:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
- assumes "covering_space c p s"
+ assumes "covering_space c p S"
"g1 a = g2 a"
- "continuous_on t f" "f ` t \<subseteq> s"
- "continuous_on t g1" "g1 ` t \<subseteq> c" "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
- "continuous_on t g2" "g2 ` t \<subseteq> c" "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
- "connected t" "a \<in> t" "x \<in> t"
+ "continuous_on T f" "f ` T \<subseteq> S"
+ "continuous_on T g1" "g1 ` T \<subseteq> c" "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
+ "continuous_on T g2" "g2 ` T \<subseteq> c" "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
+ "connected T" "a \<in> T" "x \<in> T"
shows "g1 x = g2 x"
-using covering_space_lift_unique_gen [of c p s] in_components_self assms ex_in_conv by blast
+using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv by blast
end
--- a/src/HOL/Analysis/Linear_Algebra.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Wed Jan 04 16:18:50 2017 +0000
@@ -1482,14 +1482,14 @@
lemma sum_norm_le:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
+ assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
shows "norm (sum f S) \<le> sum g S"
by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
lemma sum_norm_bound:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
- assumes K: "\<forall>x \<in> S. norm (f x) \<le> K"
- shows "norm (sum f S) \<le> of_nat (card S) * K"
+ assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
+ shows "norm (sum f S) \<le> of_nat (card S)*K"
using sum_norm_le[OF K] sum_constant[symmetric]
by simp
@@ -1946,11 +1946,9 @@
also have "\<dots> = norm (sum ?g Basis)"
by (simp add: linear_sum [OF lf] linear_cmul [OF lf])
finally have th0: "norm (f x) = norm (sum ?g Basis)" .
- have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x"
- proof
- fix i :: 'a
- assume i: "i \<in> Basis"
- from Basis_le_norm[OF i, of x]
+ have th: "norm (?g i) \<le> norm (f i) * norm x" if "i \<in> Basis" for i
+ proof -
+ from Basis_le_norm[OF that, of x]
show "norm (?g i) \<le> norm (f i) * norm x"
unfolding norm_scaleR
apply (subst mult.commute)
@@ -2023,7 +2021,6 @@
show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
apply (auto simp add: sum_distrib_right th sum.cartesian_product)
apply (rule sum_norm_le)
- apply simp
apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
field_simps simp del: scaleR_scaleR)
apply (rule mult_mono)
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Jan 04 16:18:50 2017 +0000
@@ -15,6 +15,23 @@
Norm_Arith
begin
+(* FIXME: move to HOL/Real_Vector_Spaces.thy *)
+
+lemma scaleR_2:
+ fixes x :: "'a::real_vector"
+ shows "scaleR 2 x = x + x"
+ unfolding one_add_one [symmetric] scaleR_left_distrib by simp
+
+lemma scaleR_half_double [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "(1 / 2) *\<^sub>R (a + a) = a"
+proof -
+ have "\<And>r. r *\<^sub>R (a + a) = (r * 2) *\<^sub>R a"
+ by (metis scaleR_2 scaleR_scaleR)
+ then show ?thesis
+ by simp
+qed
+
(* FIXME: move elsewhere *)
@@ -1675,6 +1692,9 @@
lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
by (simp add: box_ne_empty inner_Basis inner_sum_left) (simp add: sum.remove)
+lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
+ using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
+
subsection \<open>Connectedness\<close>
@@ -4338,6 +4358,16 @@
using l unfolding islimpt_eq_acc_point
by (rule acc_point_range_imp_convergent_subsequence)
+lemma islimpt_eq_infinite_ball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> ball x e))"
+ apply (simp add: islimpt_eq_acc_point, safe)
+ apply (metis Int_commute open_ball centre_in_ball)
+ by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl)
+
+lemma islimpt_eq_infinite_cball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> cball x e))"
+ apply (simp add: islimpt_eq_infinite_ball, safe)
+ apply (meson Int_mono ball_subset_cball finite_subset order_refl)
+ by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
+
lemma sequence_unique_limpt:
fixes f :: "nat \<Rightarrow> 'a::t2_space"
assumes "(f \<longlongrightarrow> l) sequentially"
@@ -4475,6 +4505,7 @@
\<Longrightarrow> openin (subtopology euclidean u) (s - {a})"
by (metis Int_Diff open_delete openin_open)
+
text\<open>Compactness expressed with filters\<close>
lemma closure_iff_nhds_not_empty:
@@ -5032,6 +5063,7 @@
"\<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 .
+
subsection \<open>Metric spaces with the Heine-Borel property\<close>
text \<open>
@@ -5254,6 +5286,84 @@
show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
using l r by fast
qed
+
+subsubsection \<open>Intersecting chains of compact sets\<close>
+
+proposition bounded_closed_chain:
+ fixes \<F> :: "'a::heine_borel set set"
+ assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
+ and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+ shows "\<Inter>\<F> \<noteq> {}"
+proof -
+ have "B \<inter> \<Inter>\<F> \<noteq> {}"
+ proof (rule compact_imp_fip)
+ show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
+ by (simp_all add: assms compact_eq_bounded_closed)
+ show "\<lbrakk>finite \<G>; \<G> \<subseteq> \<F>\<rbrakk> \<Longrightarrow> B \<inter> \<Inter>\<G> \<noteq> {}" for \<G>
+ proof (induction \<G> rule: finite_induct)
+ case empty
+ with assms show ?case by force
+ next
+ case (insert U \<G>)
+ then have "U \<in> \<F>" and ne: "B \<inter> \<Inter>\<G> \<noteq> {}" by auto
+ then consider "B \<subseteq> U" | "U \<subseteq> B"
+ using \<open>B \<in> \<F>\<close> chain by blast
+ then show ?case
+ proof cases
+ case 1
+ then show ?thesis
+ using Int_left_commute ne by auto
+ next
+ case 2
+ have "U \<noteq> {}"
+ using \<open>U \<in> \<F>\<close> \<open>{} \<notin> \<F>\<close> by blast
+ moreover
+ have False if "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. x \<notin> Y"
+ proof -
+ have "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. Y \<subseteq> U"
+ by (metis chain contra_subsetD insert.prems insert_subset that)
+ then obtain Y where "Y \<in> \<G>" "Y \<subseteq> U"
+ by (metis all_not_in_conv \<open>U \<noteq> {}\<close>)
+ moreover obtain x where "x \<in> \<Inter>\<G>"
+ by (metis Int_emptyI ne)
+ ultimately show ?thesis
+ by (metis Inf_lower subset_eq that)
+ qed
+ with 2 show ?thesis
+ by blast
+ qed
+ qed
+ qed
+ then show ?thesis by blast
+qed
+
+corollary compact_chain:
+ fixes \<F> :: "'a::heine_borel set set"
+ assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
+ "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+ shows "\<Inter> \<F> \<noteq> {}"
+proof (cases "\<F> = {}")
+ case True
+ then show ?thesis by auto
+next
+ case False
+ show ?thesis
+ by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain)
+qed
+
+lemma compact_nest:
+ fixes F :: "'a::linorder \<Rightarrow> 'b::heine_borel set"
+ assumes F: "\<And>n. compact(F n)" "\<And>n. F n \<noteq> {}" and mono: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
+ shows "\<Inter>range F \<noteq> {}"
+proof -
+ have *: "\<And>S T. S \<in> range F \<and> T \<in> range F \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+ by (metis mono image_iff le_cases)
+ show ?thesis
+ apply (rule compact_chain [OF _ _ *])
+ using F apply (blast intro: dest: *)+
+ done
+qed
+
subsubsection \<open>Completeness\<close>
@@ -7446,7 +7556,7 @@
qed
-subsection \<open>Topological stuff lifted from and dropped to R\<close>
+subsection \<open>Topological stuff about the set of Reals\<close>
lemma open_real:
fixes s :: "real set"
@@ -7697,11 +7807,17 @@
using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
qed
-text \<open>We can state this in terms of diameter of a set.\<close>
+subsection \<open>The diameter of a set.\<close>
definition diameter :: "'a::metric_space set \<Rightarrow> real" where
"diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
+lemma diameter_empty [simp]: "diameter{} = 0"
+ by (auto simp: diameter_def)
+
+lemma diameter_singleton [simp]: "diameter{x} = 0"
+ by (auto simp: diameter_def)
+
lemma diameter_le:
assumes "S \<noteq> {} \<or> 0 \<le> d"
and no: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> norm(x - y) \<le> d"
@@ -7772,7 +7888,180 @@
by (metis b diameter_bounded_bound order_antisym xys)
qed
-text \<open>Related results with closure as the conclusion.\<close>
+lemma diameter_ge_0:
+ assumes "bounded S" shows "0 \<le> diameter S"
+ by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl)
+
+lemma diameter_subset:
+ assumes "S \<subseteq> T" "bounded T"
+ shows "diameter S \<le> diameter T"
+proof (cases "S = {} \<or> T = {}")
+ case True
+ with assms show ?thesis
+ by (force simp: diameter_ge_0)
+next
+ case False
+ then have "bdd_above ((\<lambda>x. case x of (x, xa) \<Rightarrow> dist x xa) ` (T \<times> T))"
+ using \<open>bounded T\<close> diameter_bounded_bound by (force simp: bdd_above_def)
+ with False \<open>S \<subseteq> T\<close> show ?thesis
+ apply (simp add: diameter_def)
+ apply (rule cSUP_subset_mono, auto)
+ done
+qed
+
+lemma diameter_closure:
+ assumes "bounded S"
+ shows "diameter(closure S) = diameter S"
+proof (rule order_antisym)
+ have "False" if "diameter S < diameter (closure S)"
+ proof -
+ define d where "d = diameter(closure S) - diameter(S)"
+ have "d > 0"
+ using that by (simp add: d_def)
+ then have "diameter(closure(S)) - d / 2 < diameter(closure(S))"
+ by simp
+ have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2"
+ by (simp add: d_def divide_simps)
+ have bocl: "bounded (closure S)"
+ using assms by blast
+ moreover have "0 \<le> diameter S"
+ using assms diameter_ge_0 by blast
+ ultimately obtain x y where "x \<in> closure S" "y \<in> closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y"
+ using diameter_bounded(2) [OF bocl, rule_format, of "diameter(closure(S)) - d / 2"] \<open>d > 0\<close> d_def by auto
+ then obtain x' y' where x'y': "x' \<in> S" "dist x' x < d/4" "y' \<in> S" "dist y' y < d/4"
+ using closure_approachable
+ by (metis \<open>0 < d\<close> zero_less_divide_iff zero_less_numeral)
+ then have "dist x' y' \<le> diameter S"
+ using assms diameter_bounded_bound by blast
+ with x'y' have "dist x y \<le> d / 4 + diameter S + d / 4"
+ by (meson add_mono_thms_linordered_semiring(1) dist_triangle dist_triangle3 less_eq_real_def order_trans)
+ then show ?thesis
+ using xy d_def by linarith
+ qed
+ then show "diameter (closure S) \<le> diameter S"
+ by fastforce
+ next
+ show "diameter S \<le> diameter (closure S)"
+ by (simp add: assms bounded_closure closure_subset diameter_subset)
+qed
+
+lemma diameter_cball [simp]:
+ fixes a :: "'a::euclidean_space"
+ shows "diameter(cball a r) = (if r < 0 then 0 else 2*r)"
+proof -
+ have "diameter(cball a r) = 2*r" if "r \<ge> 0"
+ proof (rule order_antisym)
+ show "diameter (cball a r) \<le> 2*r"
+ proof (rule diameter_le)
+ fix x y assume "x \<in> cball a r" "y \<in> cball a r"
+ then have "norm (x - a) \<le> r" "norm (a - y) \<le> r"
+ by (auto simp: dist_norm norm_minus_commute)
+ then have "norm (x - y) \<le> r+r"
+ using norm_diff_triangle_le by blast
+ then show "norm (x - y) \<le> 2*r" by simp
+ qed (simp add: that)
+ have "2*r = dist (a + r *\<^sub>R (SOME i. i \<in> Basis)) (a - r *\<^sub>R (SOME i. i \<in> Basis))"
+ apply (simp add: dist_norm)
+ by (metis abs_of_nonneg mult.right_neutral norm_numeral norm_scaleR norm_some_Basis real_norm_def scaleR_2 that)
+ also have "... \<le> diameter (cball a r)"
+ apply (rule diameter_bounded_bound)
+ using that by (auto simp: dist_norm)
+ finally show "2*r \<le> diameter (cball a r)" .
+ qed
+ then show ?thesis by simp
+qed
+
+lemma diameter_ball [simp]:
+ fixes a :: "'a::euclidean_space"
+ shows "diameter(ball a r) = (if r < 0 then 0 else 2*r)"
+proof -
+ have "diameter(ball a r) = 2*r" if "r > 0"
+ by (metis bounded_ball diameter_closure closure_ball diameter_cball less_eq_real_def linorder_not_less that)
+ then show ?thesis
+ by (simp add: diameter_def)
+qed
+
+lemma diameter_closed_interval [simp]: "diameter {a..b} = (if b < a then 0 else b-a)"
+proof -
+ have "{a .. b} = cball ((a+b)/2) ((b-a)/2)"
+ by (auto simp: dist_norm abs_if divide_simps split: if_split_asm)
+ then show ?thesis
+ by simp
+qed
+
+lemma diameter_open_interval [simp]: "diameter {a<..<b} = (if b < a then 0 else b-a)"
+proof -
+ have "{a <..< b} = ball ((a+b)/2) ((b-a)/2)"
+ by (auto simp: dist_norm abs_if divide_simps split: if_split_asm)
+ then show ?thesis
+ by simp
+qed
+
+proposition Lebesgue_number_lemma:
+ assumes "compact S" "\<C> \<noteq> {}" "S \<subseteq> \<Union>\<C>" and ope: "\<And>B. B \<in> \<C> \<Longrightarrow> open B"
+ obtains \<delta> where "0 < \<delta>" "\<And>T. \<lbrakk>T \<subseteq> S; diameter T < \<delta>\<rbrakk> \<Longrightarrow> \<exists>B \<in> \<C>. T \<subseteq> B"
+proof (cases "S = {}")
+ case True
+ then show ?thesis
+ by (metis \<open>\<C> \<noteq> {}\<close> zero_less_one empty_subsetI equals0I subset_trans that)
+next
+ case False
+ { fix x assume "x \<in> S"
+ then obtain C where C: "x \<in> C" "C \<in> \<C>"
+ using \<open>S \<subseteq> \<Union>\<C>\<close> by blast
+ then obtain r where r: "r>0" "ball x (2*r) \<subseteq> C"
+ by (metis mult.commute mult_2_right not_le ope openE real_sum_of_halves zero_le_numeral zero_less_mult_iff)
+ then have "\<exists>r C. r > 0 \<and> ball x (2*r) \<subseteq> C \<and> C \<in> \<C>"
+ using C by blast
+ }
+ then obtain r where r: "\<And>x. x \<in> S \<Longrightarrow> r x > 0 \<and> (\<exists>C \<in> \<C>. ball x (2*r x) \<subseteq> C)"
+ by metis
+ then have "S \<subseteq> (\<Union>x \<in> S. ball x (r x))"
+ by auto
+ then obtain \<T> where "finite \<T>" "S \<subseteq> \<Union>\<T>" and \<T>: "\<T> \<subseteq> (\<lambda>x. ball x (r x)) ` S"
+ by (rule compactE [OF \<open>compact S\<close>]) auto
+ then obtain S0 where "S0 \<subseteq> S" "finite S0" and S0: "\<T> = (\<lambda>x. ball x (r x)) ` S0"
+ by (meson finite_subset_image)
+ then have "S0 \<noteq> {}"
+ using False \<open>S \<subseteq> \<Union>\<T>\<close> by auto
+ define \<delta> where "\<delta> = Inf (r ` S0)"
+ have "\<delta> > 0"
+ using \<open>finite S0\<close> \<open>S0 \<subseteq> S\<close> \<open>S0 \<noteq> {}\<close> r by (auto simp: \<delta>_def finite_less_Inf_iff)
+ show ?thesis
+ proof
+ show "0 < \<delta>"
+ by (simp add: \<open>0 < \<delta>\<close>)
+ show "\<exists>B \<in> \<C>. T \<subseteq> B" if "T \<subseteq> S" and dia: "diameter T < \<delta>" for T
+ proof (cases "T = {}")
+ case True
+ then show ?thesis
+ using \<open>\<C> \<noteq> {}\<close> by blast
+ next
+ case False
+ then obtain y where "y \<in> T" by blast
+ then have "y \<in> S"
+ using \<open>T \<subseteq> S\<close> by auto
+ then obtain x where "x \<in> S0" and x: "y \<in> ball x (r x)"
+ using \<open>S \<subseteq> \<Union>\<T>\<close> S0 that by blast
+ have "ball y \<delta> \<subseteq> ball y (r x)"
+ by (metis \<delta>_def \<open>S0 \<noteq> {}\<close> \<open>finite S0\<close> \<open>x \<in> S0\<close> empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball)
+ also have "... \<subseteq> ball x (2*r x)"
+ by clarsimp (metis dist_commute dist_triangle_less_add mem_ball mult_2 x)
+ finally obtain C where "C \<in> \<C>" "ball y \<delta> \<subseteq> C"
+ by (meson r \<open>S0 \<subseteq> S\<close> \<open>x \<in> S0\<close> dual_order.trans subsetCE)
+ have "bounded T"
+ using \<open>compact S\<close> bounded_subset compact_imp_bounded \<open>T \<subseteq> S\<close> by blast
+ then have "T \<subseteq> ball y \<delta>"
+ using \<open>y \<in> T\<close> dia diameter_bounded_bound by fastforce
+ then show ?thesis
+ apply (rule_tac x=C in bexI)
+ using \<open>ball y \<delta> \<subseteq> C\<close> \<open>C \<in> \<C>\<close> by auto
+ qed
+ qed
+qed
+
+
+subsection \<open>Compact sets and the closure operation.\<close>
lemma closed_scaling:
fixes s :: "'a::real_normed_vector set"
@@ -8396,6 +8685,63 @@
using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
by (auto simp: compact_eq_seq_compact_metric)
+proposition is_interval_compact:
+ "is_interval S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = cbox a b)" (is "?lhs = ?rhs")
+proof (cases "S = {}")
+ case True
+ with empty_as_interval show ?thesis by auto
+next
+ case False
+ show ?thesis
+ proof
+ assume L: ?lhs
+ then have "is_interval S" "compact S" by auto
+ define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x:S. x \<bullet> i) *\<^sub>R i"
+ define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x:S. x \<bullet> i) *\<^sub>R i"
+ have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
+ by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
+ have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
+ by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
+ have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
+ and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)" for x
+ proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
+ fix i::'a
+ assume i: "i \<in> Basis"
+ have cont: "continuous_on S (\<lambda>x. x \<bullet> i)"
+ by (intro continuous_intros)
+ obtain a where "a \<in> S" and a: "\<And>y. y\<in>S \<Longrightarrow> a \<bullet> i \<le> y \<bullet> i"
+ using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
+ obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
+ using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
+ have "a \<bullet> i \<le> (INF x:S. x \<bullet> i)"
+ by (simp add: False a cINF_greatest)
+ also have "\<dots> \<le> x \<bullet> i"
+ by (simp add: i inf)
+ finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
+ have "x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
+ by (simp add: i sup)
+ also have "(SUP x:S. x \<bullet> i) \<le> b \<bullet> i"
+ by (simp add: False b cSUP_least)
+ finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
+ show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
+ apply (rule_tac x="\<Sum>j\<in>Basis. (if j = i then x \<bullet> i else a \<bullet> j) *\<^sub>R j" in image_eqI)
+ apply (simp add: i)
+ apply (rule mem_is_intervalI [OF \<open>is_interval S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>])
+ using i ai bi apply force
+ done
+ qed
+ have "S = cbox a b"
+ by (auto simp: a_def b_def mem_box intro: 1 2 3)
+ then show ?rhs
+ by blast
+ next
+ assume R: ?rhs
+ then show ?lhs
+ using compact_cbox is_interval_cbox by blast
+ qed
+qed
+
+
lemma box_midpoint:
fixes a :: "'a::euclidean_space"
assumes "box a b \<noteq> {}"
@@ -9959,6 +10305,20 @@
compact T \<and> T \<subseteq> S)"
by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
+lemma continuous_imp_closed_map:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ assumes "closedin (subtopology euclidean S) U"
+ "continuous_on S f" "image f S = T" "compact S"
+ shows "closedin (subtopology euclidean T) (image f U)"
+ by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
+
+lemma continuous_imp_quotient_map:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ assumes "continuous_on S f" "image f S = T" "compact S" "U \<subseteq> T"
+ shows "openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> U} \<longleftrightarrow>
+ openin (subtopology euclidean T) U"
+ by (metis (no_types, lifting) Collect_cong assms closed_map_imp_quotient_map continuous_imp_closed_map)
+
subsection\<open> Finite intersection property\<close>
text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
@@ -10305,6 +10665,166 @@
qed
from X0(1,2) this show ?thesis ..
qed
+
+
+subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
+
+text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
+
+lemma continuous_disconnected_range_constant:
+ assumes s: "connected s"
+ and conf: "continuous_on s f"
+ and fim: "f ` s \<subseteq> t"
+ and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
+ shows "\<exists>a. \<forall>x \<in> s. f x = a"
+proof (cases "s = {}")
+ case True then show ?thesis by force
+next
+ case False
+ { fix x assume "x \<in> s"
+ then have "f ` s \<subseteq> {f x}"
+ by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
+ }
+ with False show ?thesis
+ by blast
+qed
+
+lemma discrete_subset_disconnected:
+ fixes s :: "'a::topological_space set"
+ fixes t :: "'b::real_normed_vector set"
+ assumes conf: "continuous_on s f"
+ and no: "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
+ shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
+proof -
+ { fix x assume x: "x \<in> s"
+ then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> s; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
+ using conf no [OF x] by auto
+ then have e2: "0 \<le> e / 2"
+ by simp
+ have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
+ apply (rule ccontr)
+ using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
+ apply (simp add: del: ex_simps)
+ apply (drule spec [where x="cball (f x) (e / 2)"])
+ apply (drule spec [where x="- ball(f x) e"])
+ apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in)
+ apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
+ using centre_in_cball connected_component_refl_eq e2 x apply blast
+ using ccs
+ apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
+ done
+ moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
+ by (auto simp: connected_component_in)
+ ultimately have "connected_component_set (f ` s) (f x) = {f x}"
+ by (auto simp: x)
+ }
+ with assms show ?thesis
+ by blast
+qed
+
+lemma finite_implies_discrete:
+ fixes s :: "'a::topological_space set"
+ assumes "finite (f ` s)"
+ shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
+proof -
+ have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
+ proof (cases "f ` s - {f x} = {}")
+ case True
+ with zero_less_numeral show ?thesis
+ by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
+ next
+ case False
+ then obtain z where z: "z \<in> s" "f z \<noteq> f x"
+ by blast
+ have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
+ using assms by simp
+ then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
+ apply (rule finite_imp_less_Inf)
+ using z apply force+
+ done
+ show ?thesis
+ by (force intro!: * cInf_le_finite [OF finn])
+ qed
+ with assms show ?thesis
+ by blast
+qed
+
+text\<open>This proof requires the existence of two separate values of the range type.\<close>
+lemma finite_range_constant_imp_connected:
+ assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+ \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
+ shows "connected s"
+proof -
+ { fix t u
+ assume clt: "closedin (subtopology euclidean s) t"
+ and clu: "closedin (subtopology euclidean s) u"
+ and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
+ have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
+ apply (subst tus [symmetric])
+ apply (rule continuous_on_cases_local)
+ using clt clu tue
+ apply (auto simp: tus continuous_on_const)
+ done
+ have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
+ by (rule finite_subset [of _ "{0,1}"]) auto
+ have "t = {} \<or> u = {}"
+ using assms [OF conif fi] tus [symmetric]
+ by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
+ }
+ then show ?thesis
+ by (simp add: connected_closedin_eq)
+qed
+
+lemma continuous_disconnected_range_constant_eq:
+ "(connected s \<longleftrightarrow>
+ (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+ \<forall>t. continuous_on s f \<and> f ` s \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
+ \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis1)
+ and continuous_discrete_range_constant_eq:
+ "(connected s \<longleftrightarrow>
+ (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+ continuous_on s f \<and>
+ (\<forall>x \<in> s. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> s \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
+ \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis2)
+ and continuous_finite_range_constant_eq:
+ "(connected s \<longleftrightarrow>
+ (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
+ continuous_on s f \<and> finite (f ` s)
+ \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis3)
+proof -
+ have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
+ \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
+ by blast
+ have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
+ apply (rule *)
+ using continuous_disconnected_range_constant apply metis
+ apply clarify
+ apply (frule discrete_subset_disconnected; blast)
+ apply (blast dest: finite_implies_discrete)
+ apply (blast intro!: finite_range_constant_imp_connected)
+ done
+ then show ?thesis1 ?thesis2 ?thesis3
+ by blast+
+qed
+
+lemma continuous_discrete_range_constant:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
+ assumes s: "connected s"
+ and "continuous_on s f"
+ and "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
+ shows "\<exists>a. \<forall>x \<in> s. f x = a"
+ using continuous_discrete_range_constant_eq [THEN iffD1, OF s] assms
+ by blast
+
+lemma continuous_finite_range_constant:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
+ assumes "connected s"
+ and "continuous_on s f"
+ and "finite (f ` s)"
+ shows "\<exists>a. \<forall>x \<in> s. f x = a"
+ using assms continuous_finite_range_constant_eq
+ by blast
+
no_notation
eucl_less (infix "<e" 50)
--- a/src/HOL/Complex.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Complex.thy Wed Jan 04 16:18:50 2017 +0000
@@ -437,6 +437,14 @@
"continuous F f \<longleftrightarrow> continuous F (\<lambda>x. Re (f x)) \<and> continuous F (\<lambda>x. Im (f x))"
by (simp only: continuous_def tendsto_complex_iff)
+lemma continuous_on_of_real_o_iff [simp]:
+ "continuous_on S (\<lambda>x. complex_of_real (g x)) = continuous_on S g"
+ using continuous_on_Re continuous_on_of_real by fastforce
+
+lemma continuous_on_of_real_id [simp]:
+ "continuous_on S (of_real :: real \<Rightarrow> 'a::real_normed_algebra_1)"
+ by (rule continuous_on_of_real [OF continuous_on_id])
+
lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \<longleftrightarrow>
((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and>
((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F"
--- a/src/HOL/Number_Theory/Primes.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Number_Theory/Primes.thy Wed Jan 04 16:18:50 2017 +0000
@@ -194,6 +194,64 @@
using assms irreducible_altdef[of m]
by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
+
+subsection\<open>Largest exponent of a prime factor\<close>
+text\<open>Possibly duplicates other material, but avoid the complexities of multisets.\<close>
+
+lemma prime_power_cancel_less:
+ assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and less: "k < k'" and "\<not> p dvd m"
+ shows False
+proof -
+ obtain l where l: "k' = k + l" and "l > 0"
+ using less less_imp_add_positive by auto
+ have "m = m * (p ^ k) div (p ^ k)"
+ using \<open>prime p\<close> by simp
+ also have "\<dots> = m' * (p ^ k') div (p ^ k)"
+ using eq by simp
+ also have "\<dots> = m' * (p ^ l) * (p ^ k) div (p ^ k)"
+ by (simp add: l mult.commute mult.left_commute power_add)
+ also have "... = m' * (p ^ l)"
+ using \<open>prime p\<close> by simp
+ finally have "p dvd m"
+ using \<open>l > 0\<close> by simp
+ with assms show False
+ by simp
+qed
+
+lemma prime_power_cancel:
+ assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and "\<not> p dvd m" "\<not> p dvd m'"
+ shows "k = k'"
+ using prime_power_cancel_less [OF \<open>prime p\<close>] assms
+ by (metis linorder_neqE_nat)
+
+lemma prime_power_cancel2:
+ assumes "prime p" "m * (p ^ k) = m' * (p ^ k')" "\<not> p dvd m" "\<not> p dvd m'"
+ obtains "m = m'" "k = k'"
+ using prime_power_cancel [OF assms] assms by auto
+
+lemma prime_power_canonical:
+ fixes m::nat
+ assumes "prime p" "m > 0"
+ shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k"
+using \<open>m > 0\<close>
+proof (induction m rule: less_induct)
+ case (less m)
+ show ?case
+ proof (cases "p dvd m")
+ case True
+ then obtain m' where m': "m = p * m'"
+ using dvdE by blast
+ with \<open>prime p\<close> have "0 < m'" "m' < m"
+ using less.prems prime_nat_iff by auto
+ with m' less show ?thesis
+ by (metis power_Suc mult.left_commute)
+ next
+ case False
+ then show ?thesis
+ by (metis mult.right_neutral power_0)
+ qed
+qed
+
subsubsection \<open>Make prime naively executable\<close>
--- a/src/HOL/Set_Interval.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Set_Interval.thy Wed Jan 04 16:18:50 2017 +0000
@@ -1090,6 +1090,19 @@
"!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
+lemma bounded_Max_nat:
+ fixes P :: "nat \<Rightarrow> bool"
+ assumes x: "P x" and M: "\<And>x. P x \<Longrightarrow> x \<le> M"
+ obtains m where "P m" "\<And>x. P x \<Longrightarrow> x \<le> m"
+proof -
+ have "finite {x. P x}"
+ using M finite_nat_set_iff_bounded_le by auto
+ then have "Max {x. P x} \<in> {x. P x}"
+ using Max_in x by auto
+ then show ?thesis
+ by (simp add: \<open>finite {x. P x}\<close> that)
+qed
+
text\<open>Any subset of an interval of natural numbers the size of the
subset is exactly that interval.\<close>
--- a/src/HOL/Topological_Spaces.thy Tue Jan 03 23:21:09 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy Wed Jan 04 16:18:50 2017 +0000
@@ -1530,9 +1530,6 @@
lemma tendsto_compose: "g \<midarrow>l\<rightarrow> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
-lemma LIM_o: "g \<midarrow>l\<rightarrow> g l \<Longrightarrow> f \<midarrow>a\<rightarrow> l \<Longrightarrow> (g \<circ> f) \<midarrow>a\<rightarrow> g l"
- unfolding o_def by (rule tendsto_compose)
-
lemma tendsto_compose_eventually:
"g \<midarrow>l\<rightarrow> m \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> m) F"
by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)