more new material
authorpaulson <lp15@cam.ac.uk>
Tue Oct 25 15:46:07 2016 +0100 (2016-10-25)
changeset 64394141e1ed8d5a0
parent 64390 ad2c5f37f659
child 64395 6b57eb9e7790
more new material
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Limits.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Oct 25 11:55:38 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Oct 25 15:46:07 2016 +0100
     1.3 @@ -2493,6 +2493,24 @@
     1.4  by (metis assms closure_closed compact_eq_bounded_closed rel_frontier_def
     1.5            rel_frontier_retract_of_punctured_affine_hull)
     1.6  
     1.7 +lemma path_connected_sphere_gen:
     1.8 +  assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
     1.9 +  shows "path_connected(rel_frontier S)"
    1.10 +proof (cases "rel_interior S = {}")
    1.11 +  case True
    1.12 +  then show ?thesis
    1.13 +    by (simp add: \<open>convex S\<close> convex_imp_path_connected rel_frontier_def)
    1.14 +next
    1.15 +  case False
    1.16 +  then show ?thesis
    1.17 +    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)
    1.18 +qed
    1.19 +
    1.20 +lemma connected_sphere_gen:
    1.21 +  assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
    1.22 +  shows "connected(rel_frontier S)"
    1.23 +  by (simp add: assms path_connected_imp_connected path_connected_sphere_gen)
    1.24 +
    1.25  subsection\<open>Borsuk-style characterization of separation\<close>
    1.26  
    1.27  lemma continuous_on_Borsuk_map:
    1.28 @@ -4326,4 +4344,5 @@
    1.29    using connected_complement_homeomorphic_convex_compact [OF assms]
    1.30    using \<open>compact T\<close> compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast
    1.31  
    1.32 +
    1.33  end
     2.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Oct 25 11:55:38 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Oct 25 15:46:07 2016 +0100
     2.3 @@ -605,7 +605,7 @@
     2.4  
     2.5  proposition valid_path_compose:
     2.6    assumes "valid_path g"
     2.7 -      and der: "\<And>x. x \<in> path_image g \<Longrightarrow> \<exists>f'. (f has_field_derivative f') (at x)"
     2.8 +      and der: "\<And>x. x \<in> path_image g \<Longrightarrow> f field_differentiable (at x)"
     2.9        and con: "continuous_on (path_image g) (deriv f)"
    2.10      shows "valid_path (f o g)"
    2.11  proof -
    2.12 @@ -617,11 +617,8 @@
    2.13          by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
    2.14      next
    2.15        have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
    2.16 -      then obtain f' where "(f has_field_derivative f') (at (g t))"
    2.17 -        using der by auto
    2.18 -      then have " (f has_derivative op * f') (at (g t))"
    2.19 -        using has_field_derivative_imp_has_derivative[of f f' "at (g t)"] by auto
    2.20 -      then show "f differentiable at (g t)" using differentiableI by auto
    2.21 +      then show "f differentiable at (g t)" 
    2.22 +        using der[THEN field_differentiable_imp_differentiable] by auto
    2.23      qed
    2.24    moreover have "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (f \<circ> g) (at x))"
    2.25      proof (rule continuous_on_eq [where f = "\<lambda>x. vector_derivative g (at x) * deriv f (g x)"],
    2.26 @@ -642,24 +639,15 @@
    2.27            show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that)
    2.28          next
    2.29            have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
    2.30 -          then obtain f' where "(f has_field_derivative f') (at (g t))"
    2.31 -            using der by auto
    2.32 -          then show "\<exists>g'. (f has_field_derivative g') (at (g t))" by auto
    2.33 +          then show "f field_differentiable at (g t)" using der by auto
    2.34          qed
    2.35      qed
    2.36    ultimately have "f o g C1_differentiable_on {0..1} - s"
    2.37      using C1_differentiable_on_eq by blast
    2.38 -  moreover have "path (f o g)"
    2.39 -    proof -
    2.40 -      have "isCont f x" when "x\<in>path_image g" for x
    2.41 -        proof -
    2.42 -          obtain f' where "(f has_field_derivative f') (at x)"
    2.43 -            using der[rule_format] \<open>x\<in>path_image g\<close> by auto
    2.44 -          thus ?thesis using DERIV_isCont by auto
    2.45 -        qed
    2.46 -      then have "continuous_on (path_image g) f" using continuous_at_imp_continuous_on by auto
    2.47 -      then show ?thesis using path_continuous_image \<open>valid_path g\<close> valid_path_imp_path by auto
    2.48 -    qed
    2.49 +  moreover have "path (f \<circ> g)" 
    2.50 +    apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
    2.51 +    using der
    2.52 +    by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
    2.53    ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
    2.54      using \<open>finite s\<close> by auto
    2.55  qed
    2.56 @@ -5730,8 +5718,8 @@
    2.57    shows "valid_path (f o g)"
    2.58  proof (rule valid_path_compose[OF \<open>valid_path g\<close>])
    2.59    fix x assume "x \<in> path_image g"
    2.60 -  then show "\<exists>f'. (f has_field_derivative f') (at x)"
    2.61 -    using holo holomorphic_on_open[OF \<open>open s\<close>] \<open>path_image g \<subseteq> s\<close> by auto
    2.62 +  then show "f field_differentiable at x"
    2.63 +    using analytic_on_imp_differentiable_at analytic_on_open assms holo by blast
    2.64  next
    2.65    have "deriv f holomorphic_on s"
    2.66      using holomorphic_deriv holo \<open>open s\<close> by auto
     3.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Oct 25 11:55:38 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Oct 25 15:46:07 2016 +0100
     3.3 @@ -277,144 +277,7 @@
     3.4  
     3.5  subsection\<open>Holomorphic functions\<close>
     3.6  
     3.7 -definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
     3.8 -           (infixr "(field'_differentiable)" 50)
     3.9 -  where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
    3.10 -
    3.11 -lemma field_differentiable_derivI:
    3.12 -    "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
    3.13 -by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
    3.14 -
    3.15 -lemma field_differentiable_imp_continuous_at:
    3.16 -    "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
    3.17 -  by (metis DERIV_continuous field_differentiable_def)
    3.18 -
    3.19 -lemma field_differentiable_within_subset:
    3.20 -    "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
    3.21 -     \<Longrightarrow> f field_differentiable (at x within t)"
    3.22 -  by (metis DERIV_subset field_differentiable_def)
    3.23 -
    3.24 -lemma field_differentiable_at_within:
    3.25 -    "\<lbrakk>f field_differentiable (at x)\<rbrakk>
    3.26 -     \<Longrightarrow> f field_differentiable (at x within s)"
    3.27 -  unfolding field_differentiable_def
    3.28 -  by (metis DERIV_subset top_greatest)
    3.29 -
    3.30 -lemma field_differentiable_linear [simp,derivative_intros]: "(op * c) field_differentiable F"
    3.31 -proof -
    3.32 -  show ?thesis
    3.33 -    unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
    3.34 -    by (force intro: has_derivative_mult_right)
    3.35 -qed
    3.36 -
    3.37 -lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
    3.38 -  unfolding field_differentiable_def has_field_derivative_def
    3.39 -  by (rule exI [where x=0])
    3.40 -     (metis has_derivative_const lambda_zero)
    3.41 -
    3.42 -lemma field_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) field_differentiable F"
    3.43 -  unfolding field_differentiable_def has_field_derivative_def
    3.44 -  by (rule exI [where x=1])
    3.45 -     (simp add: lambda_one [symmetric])
    3.46 -
    3.47 -lemma field_differentiable_id [simp,derivative_intros]: "id field_differentiable F"
    3.48 -  unfolding id_def by (rule field_differentiable_ident)
    3.49 -
    3.50 -lemma field_differentiable_minus [derivative_intros]:
    3.51 -  "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
    3.52 -  unfolding field_differentiable_def
    3.53 -  by (metis field_differentiable_minus)
    3.54 -
    3.55 -lemma field_differentiable_add [derivative_intros]:
    3.56 -  assumes "f field_differentiable F" "g field_differentiable F"
    3.57 -    shows "(\<lambda>z. f z + g z) field_differentiable F"
    3.58 -  using assms unfolding field_differentiable_def
    3.59 -  by (metis field_differentiable_add)
    3.60 -
    3.61 -lemma field_differentiable_add_const [simp,derivative_intros]:
    3.62 -     "op + c field_differentiable F"
    3.63 -  by (simp add: field_differentiable_add)
    3.64 -
    3.65 -lemma field_differentiable_sum [derivative_intros]:
    3.66 -  "(\<And>i. i \<in> I \<Longrightarrow> (f i) field_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) field_differentiable F"
    3.67 -  by (induct I rule: infinite_finite_induct)
    3.68 -     (auto intro: field_differentiable_add field_differentiable_const)
    3.69 -
    3.70 -lemma field_differentiable_diff [derivative_intros]:
    3.71 -  assumes "f field_differentiable F" "g field_differentiable F"
    3.72 -    shows "(\<lambda>z. f z - g z) field_differentiable F"
    3.73 -  using assms unfolding field_differentiable_def
    3.74 -  by (metis field_differentiable_diff)
    3.75 -
    3.76 -lemma field_differentiable_inverse [derivative_intros]:
    3.77 -  assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
    3.78 -  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
    3.79 -  using assms unfolding field_differentiable_def
    3.80 -  by (metis DERIV_inverse_fun)
    3.81 -
    3.82 -lemma field_differentiable_mult [derivative_intros]:
    3.83 -  assumes "f field_differentiable (at a within s)"
    3.84 -          "g field_differentiable (at a within s)"
    3.85 -    shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
    3.86 -  using assms unfolding field_differentiable_def
    3.87 -  by (metis DERIV_mult [of f _ a s g])
    3.88 -
    3.89 -lemma field_differentiable_divide [derivative_intros]:
    3.90 -  assumes "f field_differentiable (at a within s)"
    3.91 -          "g field_differentiable (at a within s)"
    3.92 -          "g a \<noteq> 0"
    3.93 -    shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
    3.94 -  using assms unfolding field_differentiable_def
    3.95 -  by (metis DERIV_divide [of f _ a s g])
    3.96 -
    3.97 -lemma field_differentiable_power [derivative_intros]:
    3.98 -  assumes "f field_differentiable (at a within s)"
    3.99 -    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
   3.100 -  using assms unfolding field_differentiable_def
   3.101 -  by (metis DERIV_power)
   3.102 -
   3.103 -lemma field_differentiable_transform_within:
   3.104 -  "0 < d \<Longrightarrow>
   3.105 -        x \<in> s \<Longrightarrow>
   3.106 -        (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
   3.107 -        f field_differentiable (at x within s)
   3.108 -        \<Longrightarrow> g field_differentiable (at x within s)"
   3.109 -  unfolding field_differentiable_def has_field_derivative_def
   3.110 -  by (blast intro: has_derivative_transform_within)
   3.111 -
   3.112 -lemma field_differentiable_compose_within:
   3.113 -  assumes "f field_differentiable (at a within s)"
   3.114 -          "g field_differentiable (at (f a) within f`s)"
   3.115 -    shows "(g o f) field_differentiable (at a within s)"
   3.116 -  using assms unfolding field_differentiable_def
   3.117 -  by (metis DERIV_image_chain)
   3.118 -
   3.119 -lemma field_differentiable_compose:
   3.120 -  "f field_differentiable at z \<Longrightarrow> g field_differentiable at (f z)
   3.121 -          \<Longrightarrow> (g o f) field_differentiable at z"
   3.122 -by (metis field_differentiable_at_within field_differentiable_compose_within)
   3.123 -
   3.124 -lemma field_differentiable_within_open:
   3.125 -     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
   3.126 -                          f field_differentiable at a"
   3.127 -  unfolding field_differentiable_def
   3.128 -  by (metis at_within_open)
   3.129 -
   3.130 -subsection\<open>Caratheodory characterization\<close>
   3.131 -
   3.132 -lemma field_differentiable_caratheodory_at:
   3.133 -  "f field_differentiable (at z) \<longleftrightarrow>
   3.134 -         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
   3.135 -  using CARAT_DERIV [of f]
   3.136 -  by (simp add: field_differentiable_def has_field_derivative_def)
   3.137 -
   3.138 -lemma field_differentiable_caratheodory_within:
   3.139 -  "f field_differentiable (at z within s) \<longleftrightarrow>
   3.140 -         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
   3.141 -  using DERIV_caratheodory_within [of f]
   3.142 -  by (simp add: field_differentiable_def has_field_derivative_def)
   3.143 -
   3.144 -subsection\<open>Holomorphic\<close>
   3.145 +subsection\<open>Holomorphic functions\<close>
   3.146  
   3.147  definition holomorphic_on :: "[complex \<Rightarrow> complex, complex set] \<Rightarrow> bool"
   3.148             (infixl "(holomorphic'_on)" 50)
   3.149 @@ -428,6 +291,11 @@
   3.150  lemma holomorphic_onD [dest?]: "\<lbrakk>f holomorphic_on s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x within s)"
   3.151    by (simp add: holomorphic_on_def)
   3.152  
   3.153 +lemma holomorphic_on_imp_differentiable_on:
   3.154 +    "f holomorphic_on s \<Longrightarrow> f differentiable_on s"
   3.155 +  unfolding holomorphic_on_def differentiable_on_def
   3.156 +  by (simp add: field_differentiable_imp_differentiable)
   3.157 +
   3.158  lemma holomorphic_on_imp_differentiable_at:
   3.159     "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> \<Longrightarrow> f field_differentiable (at x)"
   3.160  using at_within_open holomorphic_on_def by fastforce
   3.161 @@ -594,6 +462,20 @@
   3.162      apply (auto simp: holomorphic_derivI)
   3.163      done
   3.164  
   3.165 +subsection\<open>Caratheodory characterization\<close>
   3.166 +
   3.167 +lemma field_differentiable_caratheodory_at:
   3.168 +  "f field_differentiable (at z) \<longleftrightarrow>
   3.169 +         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
   3.170 +  using CARAT_DERIV [of f]
   3.171 +  by (simp add: field_differentiable_def has_field_derivative_def)
   3.172 +
   3.173 +lemma field_differentiable_caratheodory_within:
   3.174 +  "f field_differentiable (at z within s) \<longleftrightarrow>
   3.175 +         (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z within s) g)"
   3.176 +  using DERIV_caratheodory_within [of f]
   3.177 +  by (simp add: field_differentiable_def has_field_derivative_def)
   3.178 +
   3.179  subsection\<open>Analyticity on a set\<close>
   3.180  
   3.181  definition analytic_on (infixl "(analytic'_on)" 50)
     4.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 25 11:55:38 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 25 15:46:07 2016 +0100
     4.3 @@ -693,8 +693,8 @@
     4.4      and Arg_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
     4.5    using Arg by auto
     4.6  
     4.7 -lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(\<i> * of_real t))"
     4.8 -  using Arg [of z] by auto
     4.9 +lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg z)) = z"
    4.10 +  by (metis Arg_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
    4.11  
    4.12  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"
    4.13    apply (rule Arg_unique_lemma [OF _ Arg_eq])
    4.14 @@ -2300,7 +2300,7 @@
    4.15    by simp
    4.16  
    4.17  lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
    4.18 -  by (simp add: complex_norm_eq_1_exp)
    4.19 +  by simp
    4.20  
    4.21  lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
    4.22    unfolding Arctan_def divide_complex_def
    4.23 @@ -3261,4 +3261,190 @@
    4.24    apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
    4.25    done
    4.26  
    4.27 +subsection\<open> Formulation of loop homotopy in terms of maps out of type complex\<close>
    4.28 +
    4.29 +lemma homotopic_circlemaps_imp_homotopic_loops:
    4.30 +  assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
    4.31 +   shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))
    4.32 +                            (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))"
    4.33 +proof -
    4.34 +  have "homotopic_with (\<lambda>f. True) {z. cmod z = 1} S f g"
    4.35 +    using assms by (auto simp: sphere_def)
    4.36 +  moreover have "continuous_on {0..1} (exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
    4.37 +     by (intro continuous_intros)
    4.38 +  moreover have "(exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>)) ` {0..1} \<subseteq> {z. cmod z = 1}"
    4.39 +    by (auto simp: norm_mult)
    4.40 +  ultimately
    4.41 +  show ?thesis
    4.42 +    apply (simp add: homotopic_loops_def comp_assoc)
    4.43 +    apply (rule homotopic_with_compose_continuous_right)
    4.44 +      apply (auto simp: pathstart_def pathfinish_def)
    4.45 +    done
    4.46 +qed
    4.47 +
    4.48 +lemma homotopic_loops_imp_homotopic_circlemaps:
    4.49 +  assumes "homotopic_loops S p q"
    4.50 +    shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S
    4.51 +                          (p \<circ> (\<lambda>z. (Arg z / (2 * pi))))
    4.52 +                          (q \<circ> (\<lambda>z. (Arg z / (2 * pi))))"
    4.53 +proof -
    4.54 +  obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
    4.55 +             and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
    4.56 +             and h0: "(\<forall>x. h (0, x) = p x)"
    4.57 +             and h1: "(\<forall>x. h (1, x) = q x)"
    4.58 +             and h01: "(\<forall>t\<in>{0..1}. h (t, 1) = h (t, 0)) "
    4.59 +    using assms
    4.60 +    by (auto simp: homotopic_loops_def sphere_def homotopic_with_def pathstart_def pathfinish_def)
    4.61 +  define j where "j \<equiv> \<lambda>z. if 0 \<le> Im (snd z)
    4.62 +                          then h (fst z, Arg (snd z) / (2 * pi))
    4.63 +                          else h (fst z, 1 - Arg (cnj (snd z)) / (2 * pi))"
    4.64 +  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
    4.65 +    using that Arg_eq_0_pi Arg_eq_pi by (force simp: Arg_cnj divide_simps)
    4.66 +  show ?thesis
    4.67 +  proof (simp add: homotopic_with; intro conjI ballI exI)
    4.68 +    show "continuous_on ({0..1} \<times> sphere 0 1) (\<lambda>w. h (fst w, Arg (snd w) / (2 * pi)))"
    4.69 +    proof (rule continuous_on_eq)
    4.70 +      show j: "j x = h (fst x, Arg (snd x) / (2 * pi))" if "x \<in> {0..1} \<times> sphere 0 1" for x
    4.71 +        using Arg_eq that h01 by (force simp: j_def)
    4.72 +      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"
    4.73 +        by auto
    4.74 +      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)))"
    4.75 +        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
    4.76 +            apply (auto simp: Arg)
    4.77 +        apply (meson Arg_lt_2pi linear not_le)
    4.78 +        done
    4.79 +      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)))"
    4.80 +        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
    4.81 +            apply (auto simp: Arg)
    4.82 +        apply (meson Arg_lt_2pi linear not_le)
    4.83 +        done
    4.84 +      show "continuous_on ({0..1} \<times> sphere 0 1) j"
    4.85 +        apply (simp add: j_def)
    4.86 +        apply (subst eq)
    4.87 +        apply (rule continuous_on_cases_local)
    4.88 +            apply (simp_all add: eq [symmetric] closedin_closed_Int closed_Times closed_halfspace_Im_le closed_halfspace_Im_ge c1 c2)
    4.89 +        using Arg_eq h01
    4.90 +        by force
    4.91 +    qed
    4.92 +    have "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> h ` ({0..1} \<times> {0..1})"
    4.93 +      by (auto simp: Arg_ge_0 Arg_lt_2pi less_imp_le)
    4.94 +    also have "... \<subseteq> S"
    4.95 +      using him by blast
    4.96 +    finally show "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
    4.97 +  qed (auto simp: h0 h1)
    4.98 +qed
    4.99 +
   4.100 +lemma simply_connected_homotopic_loops:
   4.101 +  "simply_connected S \<longleftrightarrow>
   4.102 +       (\<forall>p q. homotopic_loops S p p \<and> homotopic_loops S q q \<longrightarrow> homotopic_loops S p q)"
   4.103 +unfolding simply_connected_def using homotopic_loops_refl by metis
   4.104 +
   4.105 +
   4.106 +lemma simply_connected_eq_homotopic_circlemaps1:
   4.107 +  fixes f :: "complex \<Rightarrow> 'a::topological_space" and g :: "complex \<Rightarrow> 'a"
   4.108 +  assumes S: "simply_connected S"
   4.109 +      and contf: "continuous_on (sphere 0 1) f" and fim: "f ` (sphere 0 1) \<subseteq> S"
   4.110 +      and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
   4.111 +    shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
   4.112 +proof -
   4.113 +  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))"
   4.114 +    apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
   4.115 +    apply (simp add: homotopic_circlemaps_imp_homotopic_loops homotopic_with_refl contf fim contg gim)
   4.116 +    done
   4.117 +  then show ?thesis
   4.118 +    apply (rule homotopic_with_eq [OF homotopic_loops_imp_homotopic_circlemaps])
   4.119 +      apply (auto simp: o_def complex_norm_eq_1_exp mult.commute)
   4.120 +    done
   4.121 +qed
   4.122 +
   4.123 +lemma simply_connected_eq_homotopic_circlemaps2a:
   4.124 +  fixes h :: "complex \<Rightarrow> 'a::topological_space"
   4.125 +  assumes conth: "continuous_on (sphere 0 1) h" and him: "h ` (sphere 0 1) \<subseteq> S"
   4.126 +      and hom: "\<And>f g::complex \<Rightarrow> 'a.
   4.127 +                \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
   4.128 +                continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
   4.129 +                \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
   4.130 +            shows "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
   4.131 +    apply (rule_tac x="h 1" in exI)
   4.132 +    apply (rule hom)
   4.133 +    using assms
   4.134 +    by (auto simp: continuous_on_const)
   4.135 +
   4.136 +lemma simply_connected_eq_homotopic_circlemaps2b:
   4.137 +  fixes S :: "'a::real_normed_vector set"
   4.138 +  assumes "\<And>f g::complex \<Rightarrow> 'a.
   4.139 +                \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
   4.140 +                continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
   4.141 +                \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
   4.142 +  shows "path_connected S"
   4.143 +proof (clarsimp simp add: path_connected_eq_homotopic_points)
   4.144 +  fix a b
   4.145 +  assume "a \<in> S" "b \<in> S"
   4.146 +  then show "homotopic_loops S (linepath a a) (linepath b b)"
   4.147 +    using homotopic_circlemaps_imp_homotopic_loops [OF assms [of "\<lambda>x. a" "\<lambda>x. b"]]
   4.148 +    by (auto simp: o_def continuous_on_const linepath_def)
   4.149 +qed
   4.150 +
   4.151 +lemma simply_connected_eq_homotopic_circlemaps3:
   4.152 +  fixes h :: "complex \<Rightarrow> 'a::real_normed_vector"
   4.153 +  assumes "path_connected S"
   4.154 +      and hom: "\<And>f::complex \<Rightarrow> 'a.
   4.155 +                  \<lbrakk>continuous_on (sphere 0 1) f; f `(sphere 0 1) \<subseteq> S\<rbrakk>
   4.156 +                  \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)"
   4.157 +    shows "simply_connected S"
   4.158 +proof (clarsimp simp add: simply_connected_eq_contractible_loop_some assms)
   4.159 +  fix p
   4.160 +  assume p: "path p" "path_image p \<subseteq> S" "pathfinish p = pathstart p"
   4.161 +  then have "homotopic_loops S p p"
   4.162 +    by (simp add: homotopic_loops_refl)
   4.163 +  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)"
   4.164 +    by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom)
   4.165 +  show "\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)"
   4.166 +  proof (intro exI conjI)
   4.167 +    show "a \<in> S"
   4.168 +      using homotopic_with_imp_subset2 [OF homp]
   4.169 +      by (metis dist_0_norm image_subset_iff mem_sphere norm_one)
   4.170 +    have teq: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk>
   4.171 +               \<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"
   4.172 +      apply (rule disjCI)
   4.173 +      using Arg_of_real [of 1] apply (auto simp: Arg_exp)
   4.174 +      done
   4.175 +    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>))"
   4.176 +      apply (rule homotopic_loops_eq [OF p])
   4.177 +      using p teq apply (fastforce simp: pathfinish_def pathstart_def)
   4.178 +      done
   4.179 +    then
   4.180 +    show "homotopic_loops S p (linepath a a)"
   4.181 +      by (simp add: linepath_refl  homotopic_loops_trans [OF _ homotopic_circlemaps_imp_homotopic_loops [OF homp, simplified K_record_comp]])
   4.182 +  qed
   4.183 +qed
   4.184 +
   4.185 +
   4.186 +proposition simply_connected_eq_homotopic_circlemaps:
   4.187 +  fixes S :: "'a::real_normed_vector set"
   4.188 +  shows "simply_connected S \<longleftrightarrow>
   4.189 +         (\<forall>f g::complex \<Rightarrow> 'a.
   4.190 +              continuous_on (sphere 0 1) f \<and> f ` (sphere 0 1) \<subseteq> S \<and>
   4.191 +              continuous_on (sphere 0 1) g \<and> g ` (sphere 0 1) \<subseteq> S
   4.192 +              \<longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g)"
   4.193 +  apply (rule iffI)
   4.194 +   apply (blast elim: dest: simply_connected_eq_homotopic_circlemaps1)
   4.195 +  by (simp add: simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3)
   4.196 +
   4.197 +proposition simply_connected_eq_contractible_circlemap:
   4.198 +  fixes S :: "'a::real_normed_vector set"
   4.199 +  shows "simply_connected S \<longleftrightarrow>
   4.200 +         path_connected S \<and>
   4.201 +         (\<forall>f::complex \<Rightarrow> 'a.
   4.202 +              continuous_on (sphere 0 1) f \<and> f `(sphere 0 1) \<subseteq> S
   4.203 +              \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)))"
   4.204 +  apply (rule iffI)
   4.205 +   apply (simp add: simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b)
   4.206 +  using simply_connected_eq_homotopic_circlemaps3 by blast
   4.207 +
   4.208 +corollary homotopy_eqv_simple_connectedness:
   4.209 +  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
   4.210 +  shows "S homotopy_eqv T \<Longrightarrow> simply_connected S \<longleftrightarrow> simply_connected T"
   4.211 +  by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality)
   4.212 +
   4.213  end
     5.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Oct 25 11:55:38 2016 +0200
     5.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Oct 25 15:46:07 2016 +0100
     5.3 @@ -3590,8 +3590,9 @@
     5.4              using contra_subsetD path_image_def path_fg t_def that by fastforce
     5.5            ultimately have "(h has_field_derivative der t) (at t)"
     5.6              unfolding h_def der_def using g_holo f_holo \<open>open s\<close>
     5.7 -            by (auto intro!: holomorphic_derivI derivative_eq_intros )
     5.8 -          then show "\<exists>g'. (h has_field_derivative g') (at (\<gamma> x))" unfolding t_def by auto
     5.9 +            by (auto intro!: holomorphic_derivI derivative_eq_intros)
    5.10 +          then show "h field_differentiable at (\<gamma> x)" 
    5.11 +            unfolding t_def field_differentiable_def by blast
    5.12          qed
    5.13        then have " (op / 1 has_contour_integral 0) (h \<circ> \<gamma>)
    5.14            = ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"
     6.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Oct 25 11:55:38 2016 +0200
     6.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Oct 25 15:46:07 2016 +0100
     6.3 @@ -3115,6 +3115,9 @@
     6.4  lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
     6.5    unfolding affine_def convex_def by auto
     6.6  
     6.7 +lemma convex_affine_hull [simp]: "convex (affine hull S)"
     6.8 +  by (simp add: affine_imp_convex)
     6.9 +
    6.10  lemma subspace_imp_convex: "subspace s \<Longrightarrow> convex s"
    6.11    using subspace_imp_affine affine_imp_convex by auto
    6.12  
    6.13 @@ -7662,6 +7665,12 @@
    6.14    using segment_degen_1 [of "1-u" b a]
    6.15    by (auto simp: algebra_simps)
    6.16  
    6.17 +lemma add_scaleR_degen:
    6.18 +  fixes a b ::"'a::real_vector"
    6.19 +  assumes  "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)"  "u \<noteq> v"
    6.20 +  shows "a=b"
    6.21 +  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)
    6.22 +  
    6.23  lemma closed_segment_image_interval:
    6.24       "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
    6.25    by (auto simp: set_eq_iff image_iff closed_segment_def)
     7.1 --- a/src/HOL/Analysis/Derivative.thy	Tue Oct 25 11:55:38 2016 +0200
     7.2 +++ b/src/HOL/Analysis/Derivative.thy	Tue Oct 25 15:46:07 2016 +0100
     7.3 @@ -359,6 +359,23 @@
     7.4    using has_derivative_compose[of f f' x UNIV g g']
     7.5    by (simp add: comp_def)
     7.6  
     7.7 +lemma field_vector_diff_chain_within:
     7.8 + assumes Df: "(f has_vector_derivative f') (at x within s)"
     7.9 +     and Dg: "(g has_field_derivative g') (at (f x) within f`s)"
    7.10 + shows "((g \<circ> f) has_vector_derivative (f' * g')) (at x within s)"
    7.11 +using diff_chain_within[OF Df[unfolded has_vector_derivative_def]
    7.12 +                       Dg [unfolded has_field_derivative_def]]
    7.13 + by (auto simp: o_def mult.commute has_vector_derivative_def)
    7.14 +
    7.15 +lemma vector_derivative_diff_chain_within:
    7.16 +  assumes Df: "(f has_vector_derivative f') (at x within s)"
    7.17 +     and Dg: "(g has_derivative g') (at (f x) within f`s)"
    7.18 +  shows "((g \<circ> f) has_vector_derivative (g' f')) (at x within s)"
    7.19 +using diff_chain_within[OF Df[unfolded has_vector_derivative_def] Dg]
    7.20 +  linear.scaleR[OF has_derivative_linear[OF Dg]]
    7.21 +  unfolding has_vector_derivative_def o_def
    7.22 +  by (auto simp: o_def mult.commute has_vector_derivative_def)
    7.23 +
    7.24  
    7.25  subsection \<open>Composition rules stated just for differentiability\<close>
    7.26  
    7.27 @@ -2563,13 +2580,149 @@
    7.28                         Dg [unfolded has_field_derivative_def]]
    7.29   by (auto simp: o_def mult.commute has_vector_derivative_def)
    7.30  
    7.31 -lemma vector_derivative_chain_at_general:  (*thanks to Wenda Li*)
    7.32 - assumes "f differentiable at x" "(\<exists>g'. (g has_field_derivative g') (at (f x)))"
    7.33 - shows "vector_derivative (g \<circ> f) (at x) =
    7.34 -        vector_derivative f (at x) * deriv g (f x)"
    7.35 -apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
    7.36 -using assms
    7.37 -by (auto simp: vector_derivative_works DERIV_deriv_iff_has_field_derivative)
    7.38 +lemma vector_derivative_chain_within: 
    7.39 +  assumes "at x within s \<noteq> bot" "f differentiable (at x within s)" 
    7.40 +    "(g has_derivative g') (at (f x) within f ` s)" 
    7.41 +  shows "vector_derivative (g \<circ> f) (at x within s) =
    7.42 +        g' (vector_derivative f (at x within s)) "
    7.43 +  apply (rule vector_derivative_within [OF \<open>at x within s \<noteq> bot\<close>])
    7.44 +  apply (rule vector_derivative_diff_chain_within)
    7.45 +  using assms(2-3) vector_derivative_works
    7.46 +  by auto
    7.47 +
    7.48 +subsection\<open>The notion of being field differentiable\<close>
    7.49 +
    7.50 +definition field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
    7.51 +           (infixr "(field'_differentiable)" 50)
    7.52 +  where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
    7.53 +
    7.54 +lemma field_differentiable_imp_differentiable:
    7.55 +  "f field_differentiable F \<Longrightarrow> f differentiable F"
    7.56 +  unfolding field_differentiable_def differentiable_def 
    7.57 +  using has_field_derivative_imp_has_derivative by auto
    7.58 +
    7.59 +lemma field_differentiable_derivI:
    7.60 +    "f field_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
    7.61 +by (simp add: field_differentiable_def DERIV_deriv_iff_has_field_derivative)
    7.62 +
    7.63 +lemma field_differentiable_imp_continuous_at:
    7.64 +    "f field_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
    7.65 +  by (metis DERIV_continuous field_differentiable_def)
    7.66 +
    7.67 +lemma field_differentiable_within_subset:
    7.68 +    "\<lbrakk>f field_differentiable (at x within s); t \<subseteq> s\<rbrakk>
    7.69 +     \<Longrightarrow> f field_differentiable (at x within t)"
    7.70 +  by (metis DERIV_subset field_differentiable_def)
    7.71 +
    7.72 +lemma field_differentiable_at_within:
    7.73 +    "\<lbrakk>f field_differentiable (at x)\<rbrakk>
    7.74 +     \<Longrightarrow> f field_differentiable (at x within s)"
    7.75 +  unfolding field_differentiable_def
    7.76 +  by (metis DERIV_subset top_greatest)
    7.77 +
    7.78 +lemma field_differentiable_linear [simp,derivative_intros]: "(op * c) field_differentiable F"
    7.79 +proof -
    7.80 +  show ?thesis
    7.81 +    unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
    7.82 +    by (force intro: has_derivative_mult_right)
    7.83 +qed
    7.84 +
    7.85 +lemma field_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) field_differentiable F"
    7.86 +  unfolding field_differentiable_def has_field_derivative_def
    7.87 +  using DERIV_const has_field_derivative_imp_has_derivative by blast
    7.88 +
    7.89 +lemma field_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) field_differentiable F"
    7.90 +  unfolding field_differentiable_def has_field_derivative_def
    7.91 +  using DERIV_ident has_field_derivative_def by blast
    7.92 +
    7.93 +lemma field_differentiable_id [simp,derivative_intros]: "id field_differentiable F"
    7.94 +  unfolding id_def by (rule field_differentiable_ident)
    7.95 +
    7.96 +lemma field_differentiable_minus [derivative_intros]:
    7.97 +  "f field_differentiable F \<Longrightarrow> (\<lambda>z. - (f z)) field_differentiable F"
    7.98 +  unfolding field_differentiable_def
    7.99 +  by (metis field_differentiable_minus)
   7.100 +
   7.101 +lemma field_differentiable_add [derivative_intros]:
   7.102 +  assumes "f field_differentiable F" "g field_differentiable F"
   7.103 +    shows "(\<lambda>z. f z + g z) field_differentiable F"
   7.104 +  using assms unfolding field_differentiable_def
   7.105 +  by (metis field_differentiable_add)
   7.106 +
   7.107 +lemma field_differentiable_add_const [simp,derivative_intros]:
   7.108 +     "op + c field_differentiable F"
   7.109 +  by (simp add: field_differentiable_add)
   7.110 +
   7.111 +lemma field_differentiable_sum [derivative_intros]:
   7.112 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i) field_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) field_differentiable F"
   7.113 +  by (induct I rule: infinite_finite_induct)
   7.114 +     (auto intro: field_differentiable_add field_differentiable_const)
   7.115 +
   7.116 +lemma field_differentiable_diff [derivative_intros]:
   7.117 +  assumes "f field_differentiable F" "g field_differentiable F"
   7.118 +    shows "(\<lambda>z. f z - g z) field_differentiable F"
   7.119 +  using assms unfolding field_differentiable_def
   7.120 +  by (metis field_differentiable_diff)
   7.121 +
   7.122 +lemma field_differentiable_inverse [derivative_intros]:
   7.123 +  assumes "f field_differentiable (at a within s)" "f a \<noteq> 0"
   7.124 +  shows "(\<lambda>z. inverse (f z)) field_differentiable (at a within s)"
   7.125 +  using assms unfolding field_differentiable_def
   7.126 +  by (metis DERIV_inverse_fun)
   7.127 +
   7.128 +lemma field_differentiable_mult [derivative_intros]:
   7.129 +  assumes "f field_differentiable (at a within s)"
   7.130 +          "g field_differentiable (at a within s)"
   7.131 +    shows "(\<lambda>z. f z * g z) field_differentiable (at a within s)"
   7.132 +  using assms unfolding field_differentiable_def
   7.133 +  by (metis DERIV_mult [of f _ a s g])
   7.134 +
   7.135 +lemma field_differentiable_divide [derivative_intros]:
   7.136 +  assumes "f field_differentiable (at a within s)"
   7.137 +          "g field_differentiable (at a within s)"
   7.138 +          "g a \<noteq> 0"
   7.139 +    shows "(\<lambda>z. f z / g z) field_differentiable (at a within s)"
   7.140 +  using assms unfolding field_differentiable_def
   7.141 +  by (metis DERIV_divide [of f _ a s g])
   7.142 +
   7.143 +lemma field_differentiable_power [derivative_intros]:
   7.144 +  assumes "f field_differentiable (at a within s)"
   7.145 +    shows "(\<lambda>z. f z ^ n) field_differentiable (at a within s)"
   7.146 +  using assms unfolding field_differentiable_def
   7.147 +  by (metis DERIV_power)
   7.148 +
   7.149 +lemma field_differentiable_transform_within:
   7.150 +  "0 < d \<Longrightarrow>
   7.151 +        x \<in> s \<Longrightarrow>
   7.152 +        (\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x') \<Longrightarrow>
   7.153 +        f field_differentiable (at x within s)
   7.154 +        \<Longrightarrow> g field_differentiable (at x within s)"
   7.155 +  unfolding field_differentiable_def has_field_derivative_def
   7.156 +  by (blast intro: has_derivative_transform_within)
   7.157 +
   7.158 +lemma field_differentiable_compose_within:
   7.159 +  assumes "f field_differentiable (at a within s)"
   7.160 +          "g field_differentiable (at (f a) within f`s)"
   7.161 +    shows "(g o f) field_differentiable (at a within s)"
   7.162 +  using assms unfolding field_differentiable_def
   7.163 +  by (metis DERIV_image_chain)
   7.164 +
   7.165 +lemma field_differentiable_compose:
   7.166 +  "f field_differentiable at z \<Longrightarrow> g field_differentiable at (f z)
   7.167 +          \<Longrightarrow> (g o f) field_differentiable at z"
   7.168 +by (metis field_differentiable_at_within field_differentiable_compose_within)
   7.169 +
   7.170 +lemma field_differentiable_within_open:
   7.171 +     "\<lbrakk>a \<in> s; open s\<rbrakk> \<Longrightarrow> f field_differentiable at a within s \<longleftrightarrow>
   7.172 +                          f field_differentiable at a"
   7.173 +  unfolding field_differentiable_def
   7.174 +  by (metis at_within_open)
   7.175 +
   7.176 +lemma vector_derivative_chain_at_general: 
   7.177 +  assumes "f differentiable at x" "g field_differentiable at (f x)"
   7.178 +  shows "vector_derivative (g \<circ> f) (at x) = vector_derivative f (at x) * deriv g (f x)"
   7.179 +  apply (rule vector_derivative_at [OF field_vector_diff_chain_at])
   7.180 +  using assms vector_derivative_works by (auto simp: field_differentiable_derivI)
   7.181  
   7.182  lemma exp_scaleR_has_vector_derivative_right:
   7.183    "((\<lambda>t. exp (t *\<^sub>R A)) has_vector_derivative exp (t *\<^sub>R A) * A) (at t within T)"
     8.1 --- a/src/HOL/Analysis/Further_Topology.thy	Tue Oct 25 11:55:38 2016 +0200
     8.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Tue Oct 25 15:46:07 2016 +0100
     8.3 @@ -3094,4 +3094,83 @@
     8.4    qed
     8.5  qed
     8.6  
     8.7 +subsection\<open> Dimension-based conditions for various homeomorphisms.\<close>
     8.8 +
     8.9 +lemma homeomorphic_subspaces_eq:
    8.10 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
    8.11 +  assumes "subspace S" "subspace T"
    8.12 +  shows "S homeomorphic T \<longleftrightarrow> dim S = dim T"
    8.13 +proof
    8.14 +  assume "S homeomorphic T"
    8.15 +  then obtain f g where hom: "homeomorphism S T f g"
    8.16 +    using homeomorphic_def by blast
    8.17 +  show "dim S = dim T"
    8.18 +  proof (rule order_antisym)
    8.19 +    show "dim S \<le> dim T"
    8.20 +      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)
    8.21 +    show "dim T \<le> dim S"
    8.22 +      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)
    8.23 +  qed
    8.24 +next
    8.25 +  assume "dim S = dim T"
    8.26 +  then show "S homeomorphic T"
    8.27 +    by (simp add: assms homeomorphic_subspaces)
    8.28 +qed
    8.29 +
    8.30 +lemma homeomorphic_affine_sets_eq:
    8.31 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
    8.32 +  assumes "affine S" "affine T"
    8.33 +  shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
    8.34 +proof (cases "S = {} \<or> T = {}")
    8.35 +  case True
    8.36 +  then show ?thesis
    8.37 +    using assms homeomorphic_affine_sets by force
    8.38 +next
    8.39 +  case False
    8.40 +  then obtain a b where "a \<in> S" "b \<in> T"
    8.41 +    by blast
    8.42 +  then have "subspace (op + (- a) ` S)" "subspace (op + (- b) ` T)"
    8.43 +    using affine_diffs_subspace assms by blast+
    8.44 +  then show ?thesis
    8.45 +    by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
    8.46 +qed
    8.47 +
    8.48 +
    8.49 +lemma homeomorphic_hyperplanes_eq:
    8.50 +  fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space"
    8.51 +  assumes "a \<noteq> 0" "c \<noteq> 0"
    8.52 +  shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('a) = DIM('b))"
    8.53 +  apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms)
    8.54 +  by (metis DIM_positive Suc_pred)
    8.55 +
    8.56 +lemma homeomorphic_UNIV_UNIV:
    8.57 +  shows "(UNIV::'a set) homeomorphic (UNIV::'b set) \<longleftrightarrow>
    8.58 +    DIM('a::euclidean_space) = DIM('b::euclidean_space)"
    8.59 +  by (simp add: homeomorphic_subspaces_eq)
    8.60 +
    8.61 +lemma simply_connected_sphere_gen:
    8.62 +   assumes "convex S" "bounded S" and 3: "3 \<le> aff_dim S"
    8.63 +   shows "simply_connected(rel_frontier S)"
    8.64 +proof -
    8.65 +  have pa: "path_connected (rel_frontier S)"
    8.66 +    using assms by (simp add: path_connected_sphere_gen)
    8.67 +  show ?thesis
    8.68 +  proof (clarsimp simp add: simply_connected_eq_contractible_circlemap pa)
    8.69 +    fix f
    8.70 +    assume f: "continuous_on (sphere (0::complex) 1) f" "f ` sphere 0 1 \<subseteq> rel_frontier S"
    8.71 +    have eq: "sphere (0::complex) 1 = rel_frontier(cball 0 1)"
    8.72 +      by simp
    8.73 +    have "convex (cball (0::complex) 1)"
    8.74 +      by (rule convex_cball)
    8.75 +    then obtain c where "homotopic_with (\<lambda>z. True) (sphere (0::complex) 1) (rel_frontier S) f (\<lambda>x. c)"
    8.76 +      apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball \<open>convex S\<close> \<open>bounded S\<close>, where f=f])
    8.77 +      using f 3
    8.78 +         apply (auto simp: aff_dim_cball)
    8.79 +      done
    8.80 +    then show "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) (rel_frontier S) f (\<lambda>x. a)"
    8.81 +      by blast
    8.82 +  qed
    8.83 +qed
    8.84 +
    8.85 +
    8.86  end
     9.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Tue Oct 25 11:55:38 2016 +0200
     9.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Tue Oct 25 15:46:07 2016 +0100
     9.3 @@ -129,6 +129,68 @@
     9.4      by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
     9.5  qed
     9.6  
     9.7 +proposition rel_frontier_not_sing:
     9.8 +  fixes a :: "'a::euclidean_space"
     9.9 +  assumes "bounded S"
    9.10 +    shows "rel_frontier S \<noteq> {a}"
    9.11 +proof (cases "S = {}")
    9.12 +  case True  then show ?thesis  by simp
    9.13 +next
    9.14 +  case False
    9.15 +  then obtain z where "z \<in> S"
    9.16 +    by blast
    9.17 +  then show ?thesis
    9.18 +  proof (cases "S = {z}")
    9.19 +    case True then show ?thesis  by simp
    9.20 +  next
    9.21 +    case False
    9.22 +    then obtain w where "w \<in> S" "w \<noteq> z"
    9.23 +      using \<open>z \<in> S\<close> by blast
    9.24 +    show ?thesis
    9.25 +    proof
    9.26 +      assume "rel_frontier S = {a}"
    9.27 +      then consider "w \<notin> rel_frontier S" | "z \<notin> rel_frontier S"
    9.28 +        using \<open>w \<noteq> z\<close> by auto
    9.29 +      then show False
    9.30 +      proof cases
    9.31 +        case 1
    9.32 +        then have w: "w \<in> rel_interior S"
    9.33 +          using \<open>w \<in> S\<close> closure_subset rel_frontier_def by fastforce
    9.34 +        have "w + (w - z) \<in> affine hull S"
    9.35 +          by (metis \<open>w \<in> S\<close> \<open>z \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
    9.36 +        then obtain e where "0 < e" "(w + e *\<^sub>R (w - z)) \<in> rel_frontier S"
    9.37 +          using \<open>w \<noteq> z\<close>  \<open>z \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq w)
    9.38 +        moreover obtain d where "0 < d" "(w + d *\<^sub>R (z - w)) \<in> rel_frontier S"
    9.39 +          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>
    9.40 +          by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
    9.41 +        ultimately have "d *\<^sub>R (z - w) = e *\<^sub>R (w - z)"
    9.42 +          using \<open>rel_frontier S = {a}\<close> by force
    9.43 +        moreover have "e \<noteq> -d "
    9.44 +          using \<open>0 < e\<close> \<open>0 < d\<close> by force
    9.45 +        ultimately show False
    9.46 +          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)
    9.47 +      next
    9.48 +        case 2
    9.49 +        then have z: "z \<in> rel_interior S"
    9.50 +          using \<open>z \<in> S\<close> closure_subset rel_frontier_def by fastforce
    9.51 +        have "z + (z - w) \<in> affine hull S"
    9.52 +          by (metis \<open>z \<in> S\<close> \<open>w \<in> S\<close> affine_affine_hull hull_inc mem_affine_3_minus scaleR_one)
    9.53 +        then obtain e where "0 < e" "(z + e *\<^sub>R (z - w)) \<in> rel_frontier S"
    9.54 +          using \<open>w \<noteq> z\<close>  \<open>w \<in> S\<close> by (metis assms ray_to_rel_frontier right_minus_eq z)
    9.55 +        moreover obtain d where "0 < d" "(z + d *\<^sub>R (w - z)) \<in> rel_frontier S"
    9.56 +          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>
    9.57 +          by (metis add.commute add.right_neutral diff_add_cancel hull_inc scaleR_one)
    9.58 +        ultimately have "d *\<^sub>R (w - z) = e *\<^sub>R (z - w)"
    9.59 +          using \<open>rel_frontier S = {a}\<close> by force
    9.60 +        moreover have "e \<noteq> -d "
    9.61 +          using \<open>0 < e\<close> \<open>0 < d\<close> by force
    9.62 +        ultimately show False
    9.63 +          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)
    9.64 +      qed
    9.65 +    qed
    9.66 +  qed
    9.67 +qed
    9.68 +
    9.69  proposition
    9.70    fixes S :: "'a::euclidean_space set"
    9.71    assumes "compact S" and 0: "0 \<in> rel_interior S"
    10.1 --- a/src/HOL/Analysis/Path_Connected.thy	Tue Oct 25 11:55:38 2016 +0200
    10.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue Oct 25 15:46:07 2016 +0100
    10.3 @@ -1205,6 +1205,9 @@
    10.4  lemma linepath_trivial [simp]: "linepath a a x = a"
    10.5    by (simp add: linepath_def real_vector.scale_left_diff_distrib)
    10.6  
    10.7 +lemma linepath_refl: "linepath a a = (\<lambda>x. a)"
    10.8 +  by auto
    10.9 +
   10.10  lemma subpath_refl: "subpath a a g = linepath (g a) (g a)"
   10.11    by (simp add: subpath_def linepath_def algebra_simps)
   10.12  
   10.13 @@ -4362,6 +4365,7 @@
   10.14      by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
   10.15  qed
   10.16  
   10.17 +
   10.18  subsection\<open>Contractible sets\<close>
   10.19  
   10.20  definition contractible where
    11.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 25 11:55:38 2016 +0200
    11.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 25 15:46:07 2016 +0100
    11.3 @@ -8985,6 +8985,18 @@
    11.4      done
    11.5  qed
    11.6  
    11.7 +lemma homeomorphic_spheres:
    11.8 +  fixes a b ::"'a::real_normed_vector"
    11.9 +  assumes "0 < d"  "0 < e"
   11.10 +  shows "(sphere a d) homeomorphic (sphere b e)"
   11.11 +unfolding homeomorphic_minimal
   11.12 +    apply(rule_tac x="\<lambda>x. b + (e/d) *\<^sub>R (x - a)" in exI)
   11.13 +    apply(rule_tac x="\<lambda>x. a + (d/e) *\<^sub>R (x - b)" in exI)
   11.14 +    using assms
   11.15 +    apply (auto intro!: continuous_intros
   11.16 +      simp: dist_commute dist_norm pos_divide_less_eq mult_strict_left_mono)
   11.17 +    done
   11.18 +
   11.19  subsection\<open>Inverse function property for open/closed maps\<close>
   11.20  
   11.21  lemma continuous_on_inverse_open_map:
    12.1 --- a/src/HOL/Limits.thy	Tue Oct 25 11:55:38 2016 +0200
    12.2 +++ b/src/HOL/Limits.thy	Tue Oct 25 15:46:07 2016 +0100
    12.3 @@ -1367,7 +1367,7 @@
    12.4  
    12.5  lemma tendsto_mult_filterlim_at_infinity:
    12.6    fixes c :: "'a::real_normed_field"
    12.7 -  assumes "F \<noteq> bot" "(f \<longlongrightarrow> c) F" "c \<noteq> 0"
    12.8 +  assumes  "(f \<longlongrightarrow> c) F" "c \<noteq> 0"
    12.9    assumes "filterlim g at_infinity F"
   12.10    shows "filterlim (\<lambda>x. f x * g x) at_infinity F"
   12.11  proof -
   12.12 @@ -1379,7 +1379,7 @@
   12.13      by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
   12.14    then show ?thesis
   12.15      by (subst filterlim_inverse_at_iff[symmetric]) simp_all
   12.16 -qed
   12.17 +qed  
   12.18  
   12.19  lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
   12.20   by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
    13.1 --- a/src/HOL/Topological_Spaces.thy	Tue Oct 25 11:55:38 2016 +0200
    13.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Oct 25 15:46:07 2016 +0100
    13.3 @@ -855,14 +855,21 @@
    13.4  
    13.5  lemma tendsto_imp_eventually_ne:
    13.6    fixes c :: "'a::t1_space"
    13.7 -  assumes "F \<noteq> bot" "(f \<longlongrightarrow> c) F" "c \<noteq> c'"
    13.8 +  assumes  "(f \<longlongrightarrow> c) F" "c \<noteq> c'"
    13.9    shows "eventually (\<lambda>z. f z \<noteq> c') F"
   13.10 -proof (rule ccontr)
   13.11 -  assume "\<not> eventually (\<lambda>z. f z \<noteq> c') F"
   13.12 -  then have "frequently (\<lambda>z. f z = c') F"
   13.13 -    by (simp add: frequently_def)
   13.14 -  from limit_frequently_eq[OF assms(1) this assms(2)] and assms(3) show False
   13.15 -    by contradiction
   13.16 +proof (cases "F=bot")
   13.17 +  case True
   13.18 +  thus ?thesis by auto
   13.19 +next
   13.20 +  case False
   13.21 +  show ?thesis
   13.22 +  proof (rule ccontr)
   13.23 +    assume "\<not> eventually (\<lambda>z. f z \<noteq> c') F"
   13.24 +    then have "frequently (\<lambda>z. f z = c') F"
   13.25 +      by (simp add: frequently_def)
   13.26 +    from limit_frequently_eq[OF False this \<open>(f \<longlongrightarrow> c) F\<close>] and \<open>c \<noteq> c'\<close> show False
   13.27 +      by contradiction
   13.28 +  qed
   13.29  qed
   13.30  
   13.31  lemma tendsto_le: