--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Oct 25 15:46:07 2016 +0100
@@ -2493,6 +2493,24 @@
by (metis assms closure_closed compact_eq_bounded_closed rel_frontier_def
rel_frontier_retract_of_punctured_affine_hull)
+lemma path_connected_sphere_gen:
+ assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
+ shows "path_connected(rel_frontier S)"
+proof (cases "rel_interior S = {}")
+ case True
+ then show ?thesis
+ by (simp add: \<open>convex S\<close> convex_imp_path_connected rel_frontier_def)
+next
+ case False
+ then show ?thesis
+ by (metis aff_dim_affine_hull affine_affine_hull affine_imp_convex all_not_in_conv assms path_connected_punctured_convex rel_frontier_retract_of_punctured_affine_hull retract_of_path_connected)
+qed
+
+lemma connected_sphere_gen:
+ assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
+ shows "connected(rel_frontier S)"
+ by (simp add: assms path_connected_imp_connected path_connected_sphere_gen)
+
subsection\<open>Borsuk-style characterization of separation\<close>
lemma continuous_on_Borsuk_map:
@@ -4326,4 +4344,5 @@
using connected_complement_homeomorphic_convex_compact [OF assms]
using \<open>compact T\<close> compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast
+
end
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Oct 25 15:46:07 2016 +0100
@@ -605,7 +605,7 @@
proposition valid_path_compose:
assumes "valid_path g"
- and der: "\<And>x. x \<in> path_image g \<Longrightarrow> \<exists>f'. (f has_field_derivative f') (at x)"
+ and der: "\<And>x. x \<in> path_image g \<Longrightarrow> f field_differentiable (at x)"
and con: "continuous_on (path_image g) (deriv f)"
shows "valid_path (f o g)"
proof -
@@ -617,11 +617,8 @@
by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
next
have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
- then obtain f' where "(f has_field_derivative f') (at (g t))"
- using der by auto
- then have " (f has_derivative op * f') (at (g t))"
- using has_field_derivative_imp_has_derivative[of f f' "at (g t)"] by auto
- then show "f differentiable at (g t)" using differentiableI by auto
+ then show "f differentiable at (g t)"
+ using der[THEN field_differentiable_imp_differentiable] by auto
qed
moreover have "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
proof (rule continuous_on_eq [where f = "\<lambda>x. vector_derivative g (at x) * deriv f (g x)"],
@@ -642,24 +639,15 @@
show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that)
next
have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
- then obtain f' where "(f has_field_derivative f') (at (g t))"
- using der by auto
- then show "\<exists>g'. (f has_field_derivative g') (at (g t))" by auto
+ then show "f field_differentiable at (g t)" using der by auto
qed
qed
ultimately have "f o g C1_differentiable_on {0..1} - s"
using C1_differentiable_on_eq by blast
- moreover have "path (f o g)"
- proof -
- have "isCont f x" when "x\<in>path_image g" for x
- proof -
- obtain f' where "(f has_field_derivative f') (at x)"
- using der[rule_format] \<open>x\<in>path_image g\<close> by auto
- thus ?thesis using DERIV_isCont by auto
- qed
- then have "continuous_on (path_image g) f" using continuous_at_imp_continuous_on by auto
- then show ?thesis using path_continuous_image \<open>valid_path g\<close> valid_path_imp_path by auto
- qed
+ moreover have "path (f \<circ> g)"
+ apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
+ using der
+ by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
using \<open>finite s\<close> by auto
qed
@@ -5730,8 +5718,8 @@
shows "valid_path (f o g)"
proof (rule valid_path_compose[OF \<open>valid_path g\<close>])
fix x assume "x \<in> path_image g"
- then show "\<exists>f'. (f has_field_derivative f') (at x)"
- using holo holomorphic_on_open[OF \<open>open s\<close>] \<open>path_image g \<subseteq> s\<close> by auto
+ then show "f field_differentiable at x"
+ using analytic_on_imp_differentiable_at analytic_on_open assms holo by blast
next
have "deriv f holomorphic_on s"
using holomorphic_deriv holo \<open>open s\<close> by auto
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Tue Oct 25 15:46:07 2016 +0100
@@ -277,144 +277,7 @@
subsection\<open>Holomorphic functions\<close>
-definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
- (infixr "(field'_differentiable)" 50)
- where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
-
-lemma field_differentiable_derivI:
- "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
-by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
-
-lemma field_differentiable_imp_continuous_at:
- "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
- by (metis DERIV_continuous field_differentiable_def)
-
-lemma field_differentiable_within_subset:
- "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
- \<Longrightarrow> f field_differentiable (at x within t)"
- by (metis DERIV_subset field_differentiable_def)
-
-lemma field_differentiable_at_within:
- "\<lbrakk>f field_differentiable (at x)\<rbrakk>
- \<Longrightarrow> f field_differentiable (at x within s)"
- unfolding field_differentiable_def
- by (metis DERIV_subset top_greatest)
-
-lemma field_differentiable_linear [simp,derivative_intros]: "(op * c) field_differentiable F"
-proof -
- show ?thesis
- unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
- by (force intro: has_derivative_mult_right)
-qed
-
-lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
- unfolding field_differentiable_def has_field_derivative_def
- by (rule exI [where x=0])
- (metis has_derivative_const lambda_zero)
-
-lemma field_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) field_differentiable F"
- unfolding field_differentiable_def has_field_derivative_def
- by (rule exI [where x=1])
- (simp add: lambda_one [symmetric])
-
-lemma field_differentiable_id [simp,derivative_intros]: "id field_differentiable F"
- unfolding id_def by (rule field_differentiable_ident)
-
-lemma field_differentiable_minus [derivative_intros]:
- "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
- unfolding field_differentiable_def
- by (metis field_differentiable_minus)
-
-lemma field_differentiable_add [derivative_intros]:
- assumes "f field_differentiable F" "g field_differentiable F"
- shows "(\<lambda>z. f z + g z) field_differentiable F"
- using assms unfolding field_differentiable_def
- by (metis field_differentiable_add)
-
-lemma field_differentiable_add_const [simp,derivative_intros]:
- "op + c field_differentiable F"
- by (simp add: field_differentiable_add)
-
-lemma field_differentiable_sum [derivative_intros]:
- "(\<And>i. i \<in> I \<Longrightarrow> (f i) field_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) field_differentiable F"
- by (induct I rule: infinite_finite_induct)
- (auto intro: field_differentiable_add field_differentiable_const)
-
-lemma field_differentiable_diff [derivative_intros]:
- assumes "f field_differentiable F" "g field_differentiable F"
- shows "(\<lambda>z. f z - g z) field_differentiable F"
- using assms unfolding field_differentiable_def
- by (metis field_differentiable_diff)
-
-lemma field_differentiable_inverse [derivative_intros]:
- assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
- shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
- using assms unfolding field_differentiable_def
- by (metis DERIV_inverse_fun)
-
-lemma field_differentiable_mult [derivative_intros]:
- assumes "f field_differentiable (at a within s)"
- "g field_differentiable (at a within s)"
- shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
- using assms unfolding field_differentiable_def
- by (metis DERIV_mult [of f _ a s g])
-
-lemma field_differentiable_divide [derivative_intros]:
- assumes "f field_differentiable (at a within s)"
- "g field_differentiable (at a within s)"
- "g a \<noteq> 0"
- shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
- using assms unfolding field_differentiable_def
- by (metis DERIV_divide [of f _ a s g])
-
-lemma field_differentiable_power [derivative_intros]:
- assumes "f field_differentiable (at a within s)"
- shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
- using assms unfolding field_differentiable_def
- by (metis DERIV_power)
-
-lemma field_differentiable_transform_within:
- "0 < d \<Longrightarrow>
- x \<in> s \<Longrightarrow>
- (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
- f field_differentiable (at x within s)
- \<Longrightarrow> g field_differentiable (at x within s)"
- unfolding field_differentiable_def has_field_derivative_def
- by (blast intro: has_derivative_transform_within)
-
-lemma field_differentiable_compose_within:
- assumes "f field_differentiable (at a within s)"
- "g field_differentiable (at (f a) within f`s)"
- shows "(g o f) field_differentiable (at a within s)"
- using assms unfolding field_differentiable_def
- by (metis DERIV_image_chain)
-
-lemma field_differentiable_compose:
- "f field_differentiable at z \<Longrightarrow> g field_differentiable at (f z)
- \<Longrightarrow> (g o f) field_differentiable at z"
-by (metis field_differentiable_at_within field_differentiable_compose_within)
-
-lemma field_differentiable_within_open:
- "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
- f field_differentiable at a"
- unfolding field_differentiable_def
- by (metis at_within_open)
-
-subsection\<open>Caratheodory characterization\<close>
-
-lemma field_differentiable_caratheodory_at:
- "f field_differentiable (at z) \<longleftrightarrow>
- (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
- using CARAT_DERIV [of f]
- by (simp add: field_differentiable_def has_field_derivative_def)
-
-lemma field_differentiable_caratheodory_within:
- "f field_differentiable (at z within s) \<longleftrightarrow>
- (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
- using DERIV_caratheodory_within [of f]
- by (simp add: field_differentiable_def has_field_derivative_def)
-
-subsection\<open>Holomorphic\<close>
+subsection\<open>Holomorphic functions\<close>
definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
(infixl "(holomorphic'_on)" 50)
@@ -428,6 +291,11 @@
lemma holomorphic_onD [dest?]: "\<lbrakk>f holomorphic_on s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x within s)"
by (simp add: holomorphic_on_def)
+lemma holomorphic_on_imp_differentiable_on:
+ "f holomorphic_on s \<Longrightarrow> f differentiable_on s"
+ unfolding holomorphic_on_def differentiable_on_def
+ by (simp add: field_differentiable_imp_differentiable)
+
lemma holomorphic_on_imp_differentiable_at:
"\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x)"
using at_within_open holomorphic_on_def by fastforce
@@ -594,6 +462,20 @@
apply (auto simp: holomorphic_derivI)
done
+subsection\<open>Caratheodory characterization\<close>
+
+lemma field_differentiable_caratheodory_at:
+ "f field_differentiable (at z) \<longleftrightarrow>
+ (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
+ using CARAT_DERIV [of f]
+ by (simp add: field_differentiable_def has_field_derivative_def)
+
+lemma field_differentiable_caratheodory_within:
+ "f field_differentiable (at z within s) \<longleftrightarrow>
+ (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
+ using DERIV_caratheodory_within [of f]
+ by (simp add: field_differentiable_def has_field_derivative_def)
+
subsection\<open>Analyticity on a set\<close>
definition analytic_on (infixl "(analytic'_on)" 50)
--- a/src/HOL/Analysis/Complex_Transcendental.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Oct 25 15:46:07 2016 +0100
@@ -693,8 +693,8 @@
and Arg_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
using Arg by auto
-lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(\<i> * of_real t))"
- using Arg [of z] by auto
+lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg z)) = z"
+ by (metis Arg_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
lemma Arg_unique: "\<lbrakk>of_real r * exp(\<i> * of_real a) = z; 0 < r; 0 \<le> a; a < 2*pi\<rbrakk> \<Longrightarrow> Arg z = a"
apply (rule Arg_unique_lemma [OF _ Arg_eq])
@@ -2300,7 +2300,7 @@
by simp
lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
- by (simp add: complex_norm_eq_1_exp)
+ by simp
lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
unfolding Arctan_def divide_complex_def
@@ -3261,4 +3261,190 @@
apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
done
+subsection\<open> Formulation of loop homotopy in terms of maps out of type complex\<close>
+
+lemma homotopic_circlemaps_imp_homotopic_loops:
+ assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+ shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))
+ (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))"
+proof -
+ have "homotopic_with (\<lambda>f. True) {z. cmod z = 1} S f g"
+ using assms by (auto simp: sphere_def)
+ moreover have "continuous_on {0..1} (exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
+ by (intro continuous_intros)
+ moreover have "(exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>)) ` {0..1} \<subseteq> {z. cmod z = 1}"
+ by (auto simp: norm_mult)
+ ultimately
+ show ?thesis
+ apply (simp add: homotopic_loops_def comp_assoc)
+ apply (rule homotopic_with_compose_continuous_right)
+ apply (auto simp: pathstart_def pathfinish_def)
+ done
+qed
+
+lemma homotopic_loops_imp_homotopic_circlemaps:
+ assumes "homotopic_loops S p q"
+ shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S
+ (p \<circ> (\<lambda>z. (Arg z / (2 * pi))))
+ (q \<circ> (\<lambda>z. (Arg z / (2 * pi))))"
+proof -
+ obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
+ and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
+ and h0: "(\<forall>x. h (0, x) = p x)"
+ and h1: "(\<forall>x. h (1, x) = q x)"
+ and h01: "(\<forall>t\<in>{0..1}. h (t, 1) = h (t, 0)) "
+ using assms
+ by (auto simp: homotopic_loops_def sphere_def homotopic_with_def pathstart_def pathfinish_def)
+ define j where "j \<equiv> \<lambda>z. if 0 \<le> Im (snd z)
+ then h (fst z, Arg (snd z) / (2 * pi))
+ else h (fst z, 1 - Arg (cnj (snd z)) / (2 * pi))"
+ have Arg_eq: "1 - Arg (cnj y) / (2 * pi) = Arg y / (2 * pi) \<or> Arg y = 0 \<and> Arg (cnj y) = 0" if "cmod y = 1" for y
+ using that Arg_eq_0_pi Arg_eq_pi by (force simp: Arg_cnj divide_simps)
+ show ?thesis
+ proof (simp add: homotopic_with; intro conjI ballI exI)
+ show "continuous_on ({0..1} \<times> sphere 0 1) (\<lambda>w. h (fst w, Arg (snd w) / (2 * pi)))"
+ proof (rule continuous_on_eq)
+ show j: "j x = h (fst x, Arg (snd x) / (2 * pi))" if "x \<in> {0..1} \<times> sphere 0 1" for x
+ using Arg_eq that h01 by (force simp: j_def)
+ have eq: "S = S \<inter> (UNIV \<times> {z. 0 \<le> Im z}) \<union> S \<inter> (UNIV \<times> {z. Im z \<le> 0})" for S :: "(real*complex)set"
+ by auto
+ have c1: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. 0 \<le> Im z}) (\<lambda>x. h (fst x, Arg (snd x) / (2 * pi)))"
+ apply (intro continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
+ apply (auto simp: Arg)
+ apply (meson Arg_lt_2pi linear not_le)
+ done
+ have c2: "continuous_on ({0..1} \<times> sphere 0 1 \<inter> UNIV \<times> {z. Im z \<le> 0}) (\<lambda>x. h (fst x, 1 - Arg (cnj (snd x)) / (2 * pi)))"
+ apply (intro continuous_intros continuous_on_compose2 [OF conth] continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
+ apply (auto simp: Arg)
+ apply (meson Arg_lt_2pi linear not_le)
+ done
+ show "continuous_on ({0..1} \<times> sphere 0 1) j"
+ apply (simp add: j_def)
+ apply (subst eq)
+ apply (rule continuous_on_cases_local)
+ apply (simp_all add: eq [symmetric] closedin_closed_Int closed_Times closed_halfspace_Im_le closed_halfspace_Im_ge c1 c2)
+ using Arg_eq h01
+ by force
+ qed
+ have "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> h ` ({0..1} \<times> {0..1})"
+ by (auto simp: Arg_ge_0 Arg_lt_2pi less_imp_le)
+ also have "... \<subseteq> S"
+ using him by blast
+ finally show "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
+ qed (auto simp: h0 h1)
+qed
+
+lemma simply_connected_homotopic_loops:
+ "simply_connected S \<longleftrightarrow>
+ (\<forall>p q. homotopic_loops S p p \<and> homotopic_loops S q q \<longrightarrow> homotopic_loops S p q)"
+unfolding simply_connected_def using homotopic_loops_refl by metis
+
+
+lemma simply_connected_eq_homotopic_circlemaps1:
+ fixes f :: "complex \<Rightarrow> 'a::topological_space" and g :: "complex \<Rightarrow> 'a"
+ assumes S: "simply_connected S"
+ and contf: "continuous_on (sphere 0 1) f" and fim: "f ` (sphere 0 1) \<subseteq> S"
+ and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
+ shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+proof -
+ have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * ii)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * ii))"
+ apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
+ apply (simp add: homotopic_circlemaps_imp_homotopic_loops homotopic_with_refl contf fim contg gim)
+ done
+ then show ?thesis
+ apply (rule homotopic_with_eq [OF homotopic_loops_imp_homotopic_circlemaps])
+ apply (auto simp: o_def complex_norm_eq_1_exp mult.commute)
+ done
+qed
+
+lemma simply_connected_eq_homotopic_circlemaps2a:
+ fixes h :: "complex \<Rightarrow> 'a::topological_space"
+ assumes conth: "continuous_on (sphere 0 1) h" and him: "h ` (sphere 0 1) \<subseteq> S"
+ and hom: "\<And>f g::complex \<Rightarrow> 'a.
+ \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
+ continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
+ \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+ shows "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
+ apply (rule_tac x="h 1" in exI)
+ apply (rule hom)
+ using assms
+ by (auto simp: continuous_on_const)
+
+lemma simply_connected_eq_homotopic_circlemaps2b:
+ fixes S :: "'a::real_normed_vector set"
+ assumes "\<And>f g::complex \<Rightarrow> 'a.
+ \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
+ continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
+ \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+ shows "path_connected S"
+proof (clarsimp simp add: path_connected_eq_homotopic_points)
+ fix a b
+ assume "a \<in> S" "b \<in> S"
+ then show "homotopic_loops S (linepath a a) (linepath b b)"
+ using homotopic_circlemaps_imp_homotopic_loops [OF assms [of "\<lambda>x. a" "\<lambda>x. b"]]
+ by (auto simp: o_def continuous_on_const linepath_def)
+qed
+
+lemma simply_connected_eq_homotopic_circlemaps3:
+ fixes h :: "complex \<Rightarrow> 'a::real_normed_vector"
+ assumes "path_connected S"
+ and hom: "\<And>f::complex \<Rightarrow> 'a.
+ \<lbrakk>continuous_on (sphere 0 1) f; f `(sphere 0 1) \<subseteq> S\<rbrakk>
+ \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)"
+ shows "simply_connected S"
+proof (clarsimp simp add: simply_connected_eq_contractible_loop_some assms)
+ fix p
+ assume p: "path p" "path_image p \<subseteq> S" "pathfinish p = pathstart p"
+ then have "homotopic_loops S p p"
+ by (simp add: homotopic_loops_refl)
+ then obtain a where homp: "homotopic_with (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg z / (2 * pi))) (\<lambda>x. a)"
+ by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom)
+ show "\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)"
+ proof (intro exI conjI)
+ show "a \<in> S"
+ using homotopic_with_imp_subset2 [OF homp]
+ by (metis dist_0_norm image_subset_iff mem_sphere norm_one)
+ have teq: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk>
+ \<Longrightarrow> t = Arg (exp (2 * of_real pi * of_real t * \<i>)) / (2 * pi) \<or> t=1 \<and> Arg (exp (2 * of_real pi * of_real t * \<i>)) = 0"
+ apply (rule disjCI)
+ using Arg_of_real [of 1] apply (auto simp: Arg_exp)
+ done
+ have "homotopic_loops S p (p \<circ> (\<lambda>z. Arg z / (2 * pi)) \<circ> exp \<circ> (\<lambda>t. 2 * complex_of_real pi * complex_of_real t * \<i>))"
+ apply (rule homotopic_loops_eq [OF p])
+ using p teq apply (fastforce simp: pathfinish_def pathstart_def)
+ done
+ then
+ show "homotopic_loops S p (linepath a a)"
+ by (simp add: linepath_refl homotopic_loops_trans [OF _ homotopic_circlemaps_imp_homotopic_loops [OF homp, simplified K_record_comp]])
+ qed
+qed
+
+
+proposition simply_connected_eq_homotopic_circlemaps:
+ fixes S :: "'a::real_normed_vector set"
+ shows "simply_connected S \<longleftrightarrow>
+ (\<forall>f g::complex \<Rightarrow> 'a.
+ continuous_on (sphere 0 1) f \<and> f ` (sphere 0 1) \<subseteq> S \<and>
+ continuous_on (sphere 0 1) g \<and> g ` (sphere 0 1) \<subseteq> S
+ \<longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g)"
+ apply (rule iffI)
+ apply (blast elim: dest: simply_connected_eq_homotopic_circlemaps1)
+ by (simp add: simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3)
+
+proposition simply_connected_eq_contractible_circlemap:
+ fixes S :: "'a::real_normed_vector set"
+ shows "simply_connected S \<longleftrightarrow>
+ path_connected S \<and>
+ (\<forall>f::complex \<Rightarrow> 'a.
+ continuous_on (sphere 0 1) f \<and> f `(sphere 0 1) \<subseteq> S
+ \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)))"
+ apply (rule iffI)
+ apply (simp add: simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b)
+ using simply_connected_eq_homotopic_circlemaps3 by blast
+
+corollary homotopy_eqv_simple_connectedness:
+ fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
+ shows "S homotopy_eqv T \<Longrightarrow> simply_connected S \<longleftrightarrow> simply_connected T"
+ by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality)
+
end
--- a/src/HOL/Analysis/Conformal_Mappings.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Oct 25 15:46:07 2016 +0100
@@ -3590,8 +3590,9 @@
using contra_subsetD path_image_def path_fg t_def that by fastforce
ultimately have "(h has_field_derivative der t) (at t)"
unfolding h_def der_def using g_holo f_holo \<open>open s\<close>
- by (auto intro!: holomorphic_derivI derivative_eq_intros )
- then show "\<exists>g'. (h has_field_derivative g') (at (\<gamma> x))" unfolding t_def by auto
+ by (auto intro!: holomorphic_derivI derivative_eq_intros)
+ then show "h field_differentiable at (\<gamma> x)"
+ unfolding t_def field_differentiable_def by blast
qed
then have " (op / 1 has_contour_integral 0) (h \<circ> \<gamma>)
= ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Oct 25 15:46:07 2016 +0100
@@ -3115,6 +3115,9 @@
lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
unfolding affine_def convex_def by auto
+lemma convex_affine_hull [simp]: "convex (affine hull S)"
+ by (simp add: affine_imp_convex)
+
lemma subspace_imp_convex: "subspace s \<Longrightarrow> convex s"
using subspace_imp_affine affine_imp_convex by auto
@@ -7662,6 +7665,12 @@
using segment_degen_1 [of "1-u" b a]
by (auto simp: algebra_simps)
+lemma add_scaleR_degen:
+ fixes a b ::"'a::real_vector"
+ assumes "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)" "u \<noteq> v"
+ shows "a=b"
+ by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms)
+
lemma closed_segment_image_interval:
"closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
by (auto simp: set_eq_iff image_iff closed_segment_def)
--- a/src/HOL/Analysis/Derivative.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Derivative.thy Tue Oct 25 15:46:07 2016 +0100
@@ -359,6 +359,23 @@
using has_derivative_compose[of f f' x UNIV g g']
by (simp add: comp_def)
+lemma field_vector_diff_chain_within:
+ assumes Df: "(f has_vector_derivative f') (at x within s)"
+ and Dg: "(g has_field_derivative g') (at (f x) within f`s)"
+ shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within s)"
+using diff_chain_within[OF Df[unfolded has_vector_derivative_def]
+ Dg [unfolded has_field_derivative_def]]
+ by (auto simp: o_def mult.commute has_vector_derivative_def)
+
+lemma vector_derivative_diff_chain_within:
+ assumes Df: "(f has_vector_derivative f') (at x within s)"
+ and Dg: "(g has_derivative g') (at (f x) within f`s)"
+ shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within s)"
+using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg]
+ linear.scaleR[OF has_derivative_linear[OF Dg]]
+ unfolding has_vector_derivative_def o_def
+ by (auto simp: o_def mult.commute has_vector_derivative_def)
+
subsection \<open>Composition rules stated just for differentiability\<close>
@@ -2563,13 +2580,149 @@
Dg [unfolded has_field_derivative_def]]
by (auto simp: o_def mult.commute has_vector_derivative_def)
-lemma vector_derivative_chain_at_general: (*thanks to Wenda Li*)
- assumes "f differentiable at x" "(\<exists>g'. (g has_field_derivative g') (at (f x)))"
- shows "vector_derivative (g \<circ> f) (at x) =
- vector_derivative f (at x) * deriv g (f x)"
-apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
-using assms
-by (auto simp: vector_derivative_works DERIV_deriv_iff_has_field_derivative)
+lemma vector_derivative_chain_within:
+ assumes "at x within s \<noteq> bot" "f differentiable (at x within s)"
+ "(g has_derivative g') (at (f x) within f ` s)"
+ shows "vector_derivative (g \<circ> f) (at x within s) =
+ g' (vector_derivative f (at x within s)) "
+ apply (rule vector_derivative_within [OF \<open>at x within s \<noteq> bot\<close>])
+ apply (rule vector_derivative_diff_chain_within)
+ using assms(2-3) vector_derivative_works
+ by auto
+
+subsection\<open>The notion of being field differentiable\<close>
+
+definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
+ (infixr "(field'_differentiable)" 50)
+ where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
+
+lemma field_differentiable_imp_differentiable:
+ "f field_differentiable F \<Longrightarrow> f differentiable F"
+ unfolding field_differentiable_def differentiable_def
+ using has_field_derivative_imp_has_derivative by auto
+
+lemma field_differentiable_derivI:
+ "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
+by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
+
+lemma field_differentiable_imp_continuous_at:
+ "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
+ by (metis DERIV_continuous field_differentiable_def)
+
+lemma field_differentiable_within_subset:
+ "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
+ \<Longrightarrow> f field_differentiable (at x within t)"
+ by (metis DERIV_subset field_differentiable_def)
+
+lemma field_differentiable_at_within:
+ "\<lbrakk>f field_differentiable (at x)\<rbrakk>
+ \<Longrightarrow> f field_differentiable (at x within s)"
+ unfolding field_differentiable_def
+ by (metis DERIV_subset top_greatest)
+
+lemma field_differentiable_linear [simp,derivative_intros]: "(op * c) field_differentiable F"
+proof -
+ show ?thesis
+ unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
+ by (force intro: has_derivative_mult_right)
+qed
+
+lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
+ unfolding field_differentiable_def has_field_derivative_def
+ using DERIV_const has_field_derivative_imp_has_derivative by blast
+
+lemma field_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) field_differentiable F"
+ unfolding field_differentiable_def has_field_derivative_def
+ using DERIV_ident has_field_derivative_def by blast
+
+lemma field_differentiable_id [simp,derivative_intros]: "id field_differentiable F"
+ unfolding id_def by (rule field_differentiable_ident)
+
+lemma field_differentiable_minus [derivative_intros]:
+ "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
+ unfolding field_differentiable_def
+ by (metis field_differentiable_minus)
+
+lemma field_differentiable_add [derivative_intros]:
+ assumes "f field_differentiable F" "g field_differentiable F"
+ shows "(\<lambda>z. f z + g z) field_differentiable F"
+ using assms unfolding field_differentiable_def
+ by (metis field_differentiable_add)
+
+lemma field_differentiable_add_const [simp,derivative_intros]:
+ "op + c field_differentiable F"
+ by (simp add: field_differentiable_add)
+
+lemma field_differentiable_sum [derivative_intros]:
+ "(\<And>i. i \<in> I \<Longrightarrow> (f i) field_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) field_differentiable F"
+ by (induct I rule: infinite_finite_induct)
+ (auto intro: field_differentiable_add field_differentiable_const)
+
+lemma field_differentiable_diff [derivative_intros]:
+ assumes "f field_differentiable F" "g field_differentiable F"
+ shows "(\<lambda>z. f z - g z) field_differentiable F"
+ using assms unfolding field_differentiable_def
+ by (metis field_differentiable_diff)
+
+lemma field_differentiable_inverse [derivative_intros]:
+ assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
+ shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
+ using assms unfolding field_differentiable_def
+ by (metis DERIV_inverse_fun)
+
+lemma field_differentiable_mult [derivative_intros]:
+ assumes "f field_differentiable (at a within s)"
+ "g field_differentiable (at a within s)"
+ shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
+ using assms unfolding field_differentiable_def
+ by (metis DERIV_mult [of f _ a s g])
+
+lemma field_differentiable_divide [derivative_intros]:
+ assumes "f field_differentiable (at a within s)"
+ "g field_differentiable (at a within s)"
+ "g a \<noteq> 0"
+ shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
+ using assms unfolding field_differentiable_def
+ by (metis DERIV_divide [of f _ a s g])
+
+lemma field_differentiable_power [derivative_intros]:
+ assumes "f field_differentiable (at a within s)"
+ shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
+ using assms unfolding field_differentiable_def
+ by (metis DERIV_power)
+
+lemma field_differentiable_transform_within:
+ "0 < d \<Longrightarrow>
+ x \<in> s \<Longrightarrow>
+ (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
+ f field_differentiable (at x within s)
+ \<Longrightarrow> g field_differentiable (at x within s)"
+ unfolding field_differentiable_def has_field_derivative_def
+ by (blast intro: has_derivative_transform_within)
+
+lemma field_differentiable_compose_within:
+ assumes "f field_differentiable (at a within s)"
+ "g field_differentiable (at (f a) within f`s)"
+ shows "(g o f) field_differentiable (at a within s)"
+ using assms unfolding field_differentiable_def
+ by (metis DERIV_image_chain)
+
+lemma field_differentiable_compose:
+ "f field_differentiable at z \<Longrightarrow> g field_differentiable at (f z)
+ \<Longrightarrow> (g o f) field_differentiable at z"
+by (metis field_differentiable_at_within field_differentiable_compose_within)
+
+lemma field_differentiable_within_open:
+ "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
+ f field_differentiable at a"
+ unfolding field_differentiable_def
+ by (metis at_within_open)
+
+lemma vector_derivative_chain_at_general:
+ assumes "f differentiable at x" "g field_differentiable at (f x)"
+ shows "vector_derivative (g \<circ> f) (at x) = vector_derivative f (at x) * deriv g (f x)"
+ apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
+ using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
lemma exp_scaleR_has_vector_derivative_right:
"((\<lambda>t. exp (t *\<^sub>R A)) has_vector_derivative exp (t *\<^sub>R A) * A) (at t within T)"
--- a/src/HOL/Analysis/Further_Topology.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Tue Oct 25 15:46:07 2016 +0100
@@ -3094,4 +3094,83 @@
qed
qed
+subsection\<open> Dimension-based conditions for various homeomorphisms.\<close>
+
+lemma homeomorphic_subspaces_eq:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "subspace S" "subspace T"
+ shows "S homeomorphic T \<longleftrightarrow> dim S = dim T"
+proof
+ assume "S homeomorphic T"
+ then obtain f g where hom: "homeomorphism S T f g"
+ using homeomorphic_def by blast
+ show "dim S = dim T"
+ proof (rule order_antisym)
+ show "dim S \<le> dim T"
+ by (metis assms dual_order.refl inj_onI homeomorphism_cont1 [OF hom] homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] continuous_injective_image_subspace_dim_le)
+ show "dim T \<le> dim S"
+ by (metis assms dual_order.refl inj_onI homeomorphism_cont2 [OF hom] homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] continuous_injective_image_subspace_dim_le)
+ qed
+next
+ assume "dim S = dim T"
+ then show "S homeomorphic T"
+ by (simp add: assms homeomorphic_subspaces)
+qed
+
+lemma homeomorphic_affine_sets_eq:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "affine S" "affine T"
+ shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
+proof (cases "S = {} \<or> T = {}")
+ case True
+ then show ?thesis
+ using assms homeomorphic_affine_sets by force
+next
+ case False
+ then obtain a b where "a \<in> S" "b \<in> T"
+ by blast
+ then have "subspace (op + (- a) ` S)" "subspace (op + (- b) ` T)"
+ using affine_diffs_subspace assms by blast+
+ then show ?thesis
+ by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
+qed
+
+
+lemma homeomorphic_hyperplanes_eq:
+ fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space"
+ assumes "a \<noteq> 0" "c \<noteq> 0"
+ shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('a) = DIM('b))"
+ apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms)
+ by (metis DIM_positive Suc_pred)
+
+lemma homeomorphic_UNIV_UNIV:
+ shows "(UNIV::'a set) homeomorphic (UNIV::'b set) \<longleftrightarrow>
+ DIM('a::euclidean_space) = DIM('b::euclidean_space)"
+ by (simp add: homeomorphic_subspaces_eq)
+
+lemma simply_connected_sphere_gen:
+ assumes "convex S" "bounded S" and 3: "3 \<le> aff_dim S"
+ shows "simply_connected(rel_frontier S)"
+proof -
+ have pa: "path_connected (rel_frontier S)"
+ using assms by (simp add: path_connected_sphere_gen)
+ show ?thesis
+ proof (clarsimp simp add: simply_connected_eq_contractible_circlemap pa)
+ fix f
+ assume f: "continuous_on (sphere (0::complex) 1) f" "f ` sphere 0 1 \<subseteq> rel_frontier S"
+ have eq: "sphere (0::complex) 1 = rel_frontier(cball 0 1)"
+ by simp
+ have "convex (cball (0::complex) 1)"
+ by (rule convex_cball)
+ then obtain c where "homotopic_with (\<lambda>z. True) (sphere (0::complex) 1) (rel_frontier S) f (\<lambda>x. c)"
+ apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball \<open>convex S\<close> \<open>bounded S\<close>, where f=f])
+ using f 3
+ apply (auto simp: aff_dim_cball)
+ done
+ then show "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) (rel_frontier S) f (\<lambda>x. a)"
+ by blast
+ qed
+qed
+
+
end
--- a/src/HOL/Analysis/Homeomorphism.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy Tue Oct 25 15:46:07 2016 +0100
@@ -129,6 +129,68 @@
by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
qed
+proposition rel_frontier_not_sing:
+ fixes a :: "'a::euclidean_space"
+ assumes "bounded S"
+ shows "rel_frontier S \<noteq> {a}"
+proof (cases "S = {}")
+ case True then show ?thesis by simp
+next
+ case False
+ then obtain z where "z \<in> S"
+ by blast
+ then show ?thesis
+ proof (cases "S = {z}")
+ case True then show ?thesis by simp
+ next
+ case False
+ then obtain w where "w \<in> S" "w \<noteq> z"
+ using \<open>z \<in> S\<close> by blast
+ show ?thesis
+ proof
+ assume "rel_frontier S = {a}"
+ then consider "w \<notin> rel_frontier S" | "z \<notin> rel_frontier S"
+ using \<open>w \<noteq> z\<close> by auto
+ then show False
+ proof cases
+ case 1
+ then have w: "w \<in> rel_interior S"
+ using \<open>w \<in> S\<close> closure_subset rel_frontier_def by fastforce
+ have "w + (w - z) \<in> affine hull S"
+ by (metis \<open>w \<in> S\<close> \<open>z \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
+ then obtain e where "0 < e" "(w + e *\<^sub>R (w - z)) \<in> rel_frontier S"
+ using \<open>w \<noteq> z\<close> \<open>z \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq w)
+ moreover obtain d where "0 < d" "(w + d *\<^sub>R (z - w)) \<in> rel_frontier S"
+ using ray_to_rel_frontier [OF \<open>bounded S\<close> w, of "1 *\<^sub>R (z - w)"] \<open>w \<noteq> z\<close> \<open>z \<in> S\<close>
+ by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
+ ultimately have "d *\<^sub>R (z - w) = e *\<^sub>R (w - z)"
+ using \<open>rel_frontier S = {a}\<close> by force
+ moreover have "e \<noteq> -d "
+ using \<open>0 < e\<close> \<open>0 < d\<close> by force
+ ultimately show False
+ by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
+ next
+ case 2
+ then have z: "z \<in> rel_interior S"
+ using \<open>z \<in> S\<close> closure_subset rel_frontier_def by fastforce
+ have "z + (z - w) \<in> affine hull S"
+ by (metis \<open>z \<in> S\<close> \<open>w \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
+ then obtain e where "0 < e" "(z + e *\<^sub>R (z - w)) \<in> rel_frontier S"
+ using \<open>w \<noteq> z\<close> \<open>w \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq z)
+ moreover obtain d where "0 < d" "(z + d *\<^sub>R (w - z)) \<in> rel_frontier S"
+ using ray_to_rel_frontier [OF \<open>bounded S\<close> z, of "1 *\<^sub>R (w - z)"] \<open>w \<noteq> z\<close> \<open>w \<in> S\<close>
+ by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
+ ultimately have "d *\<^sub>R (w - z) = e *\<^sub>R (z - w)"
+ using \<open>rel_frontier S = {a}\<close> by force
+ moreover have "e \<noteq> -d "
+ using \<open>0 < e\<close> \<open>0 < d\<close> by force
+ ultimately show False
+ by (metis (no_types, lifting) \<open>w \<noteq> z\<close> eq_iff_diff_eq_0 minus_diff_eq real_vector.scale_cancel_right real_vector.scale_minus_right scaleR_left.minus)
+ qed
+ qed
+ qed
+qed
+
proposition
fixes S :: "'a::euclidean_space set"
assumes "compact S" and 0: "0 \<in> rel_interior S"
--- a/src/HOL/Analysis/Path_Connected.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Tue Oct 25 15:46:07 2016 +0100
@@ -1205,6 +1205,9 @@
lemma linepath_trivial [simp]: "linepath a a x = a"
by (simp add: linepath_def real_vector.scale_left_diff_distrib)
+lemma linepath_refl: "linepath a a = (\<lambda>x. a)"
+ by auto
+
lemma subpath_refl: "subpath a a g = linepath (g a) (g a)"
by (simp add: subpath_def linepath_def algebra_simps)
@@ -4362,6 +4365,7 @@
by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
qed
+
subsection\<open>Contractible sets\<close>
definition contractible where
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Oct 25 15:46:07 2016 +0100
@@ -8985,6 +8985,18 @@
done
qed
+lemma homeomorphic_spheres:
+ fixes a b ::"'a::real_normed_vector"
+ assumes "0 < d" "0 < e"
+ shows "(sphere a d) homeomorphic (sphere b e)"
+unfolding homeomorphic_minimal
+ apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
+ apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
+ using assms
+ apply (auto intro!: continuous_intros
+ simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
+ done
+
subsection\<open>Inverse function property for open/closed maps\<close>
lemma continuous_on_inverse_open_map:
--- a/src/HOL/Limits.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Limits.thy Tue Oct 25 15:46:07 2016 +0100
@@ -1367,7 +1367,7 @@
lemma tendsto_mult_filterlim_at_infinity:
fixes c :: "'a::real_normed_field"
- assumes "F \<noteq> bot" "(f \<longlongrightarrow> c) F" "c \<noteq> 0"
+ assumes "(f \<longlongrightarrow> c) F" "c \<noteq> 0"
assumes "filterlim g at_infinity F"
shows "filterlim (\<lambda>x. f x * g x) at_infinity F"
proof -
@@ -1379,7 +1379,7 @@
by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
then show ?thesis
by (subst filterlim_inverse_at_iff[symmetric]) simp_all
-qed
+qed
lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
--- a/src/HOL/Topological_Spaces.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy Tue Oct 25 15:46:07 2016 +0100
@@ -855,14 +855,21 @@
lemma tendsto_imp_eventually_ne:
fixes c :: "'a::t1_space"
- assumes "F \<noteq> bot" "(f \<longlongrightarrow> c) F" "c \<noteq> c'"
+ assumes "(f \<longlongrightarrow> c) F" "c \<noteq> c'"
shows "eventually (\<lambda>z. f z \<noteq> c') F"
-proof (rule ccontr)
- assume "\<not> eventually (\<lambda>z. f z \<noteq> c') F"
- then have "frequently (\<lambda>z. f z = c') F"
- by (simp add: frequently_def)
- from limit_frequently_eq[OF assms(1) this assms(2)] and assms(3) show False
- by contradiction
+proof (cases "F=bot")
+ case True
+ thus ?thesis by auto
+next
+ case False
+ show ?thesis
+ proof (rule ccontr)
+ assume "\<not> eventually (\<lambda>z. f z \<noteq> c') F"
+ then have "frequently (\<lambda>z. f z = c') F"
+ by (simp add: frequently_def)
+ from limit_frequently_eq[OF False this \<open>(f \<longlongrightarrow> c) F\<close>] and \<open>c \<noteq> c'\<close> show False
+ by contradiction
+ qed
qed
lemma tendsto_le: