src/HOL/Analysis/Complex_Transcendental.thy
 changeset 64394 141e1ed8d5a0 parent 64287 d85d88722745 child 64508 874555896035
```     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 25 11:55:38 2016 +0200
1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 25 15:46:07 2016 +0100
1.3 @@ -693,8 +693,8 @@
1.4      and Arg_eq: "z = of_real(norm z) * exp(\<i> * of_real(Arg z))"
1.5    using Arg by auto
1.6
1.7 -lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> (\<exists>t. z = exp(\<i> * of_real t))"
1.8 -  using Arg [of z] by auto
1.9 +lemma complex_norm_eq_1_exp: "norm z = 1 \<longleftrightarrow> exp(\<i> * of_real (Arg z)) = z"
1.10 +  by (metis Arg_eq cis_conv_exp mult.left_neutral norm_cis of_real_1)
1.11
1.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"
1.13    apply (rule Arg_unique_lemma [OF _ Arg_eq])
1.14 @@ -2300,7 +2300,7 @@
1.15    by simp
1.16
1.17  lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
1.18 -  by (simp add: complex_norm_eq_1_exp)
1.19 +  by simp
1.20
1.21  lemma Im_Arctan_of_real [simp]: "Im (Arctan (of_real x)) = 0"
1.22    unfolding Arctan_def divide_complex_def
1.23 @@ -3261,4 +3261,190 @@
1.24    apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
1.25    done
1.26
1.27 +subsection\<open> Formulation of loop homotopy in terms of maps out of type complex\<close>
1.28 +
1.29 +lemma homotopic_circlemaps_imp_homotopic_loops:
1.30 +  assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
1.31 +   shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))
1.32 +                            (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))"
1.33 +proof -
1.34 +  have "homotopic_with (\<lambda>f. True) {z. cmod z = 1} S f g"
1.35 +    using assms by (auto simp: sphere_def)
1.36 +  moreover have "continuous_on {0..1} (exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
1.37 +     by (intro continuous_intros)
1.38 +  moreover have "(exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>)) ` {0..1} \<subseteq> {z. cmod z = 1}"
1.39 +    by (auto simp: norm_mult)
1.40 +  ultimately
1.41 +  show ?thesis
1.42 +    apply (simp add: homotopic_loops_def comp_assoc)
1.43 +    apply (rule homotopic_with_compose_continuous_right)
1.44 +      apply (auto simp: pathstart_def pathfinish_def)
1.45 +    done
1.46 +qed
1.47 +
1.48 +lemma homotopic_loops_imp_homotopic_circlemaps:
1.49 +  assumes "homotopic_loops S p q"
1.50 +    shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S
1.51 +                          (p \<circ> (\<lambda>z. (Arg z / (2 * pi))))
1.52 +                          (q \<circ> (\<lambda>z. (Arg z / (2 * pi))))"
1.53 +proof -
1.54 +  obtain h where conth: "continuous_on ({0..1::real} \<times> {0..1}) h"
1.55 +             and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
1.56 +             and h0: "(\<forall>x. h (0, x) = p x)"
1.57 +             and h1: "(\<forall>x. h (1, x) = q x)"
1.58 +             and h01: "(\<forall>t\<in>{0..1}. h (t, 1) = h (t, 0)) "
1.59 +    using assms
1.60 +    by (auto simp: homotopic_loops_def sphere_def homotopic_with_def pathstart_def pathfinish_def)
1.61 +  define j where "j \<equiv> \<lambda>z. if 0 \<le> Im (snd z)
1.62 +                          then h (fst z, Arg (snd z) / (2 * pi))
1.63 +                          else h (fst z, 1 - Arg (cnj (snd z)) / (2 * pi))"
1.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
1.65 +    using that Arg_eq_0_pi Arg_eq_pi by (force simp: Arg_cnj divide_simps)
1.66 +  show ?thesis
1.67 +  proof (simp add: homotopic_with; intro conjI ballI exI)
1.68 +    show "continuous_on ({0..1} \<times> sphere 0 1) (\<lambda>w. h (fst w, Arg (snd w) / (2 * pi)))"
1.69 +    proof (rule continuous_on_eq)
1.70 +      show j: "j x = h (fst x, Arg (snd x) / (2 * pi))" if "x \<in> {0..1} \<times> sphere 0 1" for x
1.71 +        using Arg_eq that h01 by (force simp: j_def)
1.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"
1.73 +        by auto
1.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)))"
1.75 +        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
1.76 +            apply (auto simp: Arg)
1.77 +        apply (meson Arg_lt_2pi linear not_le)
1.78 +        done
1.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)))"
1.80 +        apply (intro continuous_intros continuous_on_compose2 [OF conth]  continuous_on_compose2 [OF continuous_on_upperhalf_Arg])
1.81 +            apply (auto simp: Arg)
1.82 +        apply (meson Arg_lt_2pi linear not_le)
1.83 +        done
1.84 +      show "continuous_on ({0..1} \<times> sphere 0 1) j"
1.85 +        apply (simp add: j_def)
1.86 +        apply (subst eq)
1.87 +        apply (rule continuous_on_cases_local)
1.88 +            apply (simp_all add: eq [symmetric] closedin_closed_Int closed_Times closed_halfspace_Im_le closed_halfspace_Im_ge c1 c2)
1.89 +        using Arg_eq h01
1.90 +        by force
1.91 +    qed
1.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})"
1.93 +      by (auto simp: Arg_ge_0 Arg_lt_2pi less_imp_le)
1.94 +    also have "... \<subseteq> S"
1.95 +      using him by blast
1.96 +    finally show "(\<lambda>w. h (fst w, Arg (snd w) / (2 * pi))) ` ({0..1} \<times> sphere 0 1) \<subseteq> S" .
1.97 +  qed (auto simp: h0 h1)
1.98 +qed
1.99 +
1.100 +lemma simply_connected_homotopic_loops:
1.101 +  "simply_connected S \<longleftrightarrow>
1.102 +       (\<forall>p q. homotopic_loops S p p \<and> homotopic_loops S q q \<longrightarrow> homotopic_loops S p q)"
1.103 +unfolding simply_connected_def using homotopic_loops_refl by metis
1.104 +
1.105 +
1.106 +lemma simply_connected_eq_homotopic_circlemaps1:
1.107 +  fixes f :: "complex \<Rightarrow> 'a::topological_space" and g :: "complex \<Rightarrow> 'a"
1.108 +  assumes S: "simply_connected S"
1.109 +      and contf: "continuous_on (sphere 0 1) f" and fim: "f ` (sphere 0 1) \<subseteq> S"
1.110 +      and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
1.111 +    shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
1.112 +proof -
1.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))"
1.114 +    apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
1.115 +    apply (simp add: homotopic_circlemaps_imp_homotopic_loops homotopic_with_refl contf fim contg gim)
1.116 +    done
1.117 +  then show ?thesis
1.118 +    apply (rule homotopic_with_eq [OF homotopic_loops_imp_homotopic_circlemaps])
1.119 +      apply (auto simp: o_def complex_norm_eq_1_exp mult.commute)
1.120 +    done
1.121 +qed
1.122 +
1.123 +lemma simply_connected_eq_homotopic_circlemaps2a:
1.124 +  fixes h :: "complex \<Rightarrow> 'a::topological_space"
1.125 +  assumes conth: "continuous_on (sphere 0 1) h" and him: "h ` (sphere 0 1) \<subseteq> S"
1.126 +      and hom: "\<And>f g::complex \<Rightarrow> 'a.
1.127 +                \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
1.128 +                continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
1.129 +                \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
1.130 +            shows "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
1.131 +    apply (rule_tac x="h 1" in exI)
1.132 +    apply (rule hom)
1.133 +    using assms
1.134 +    by (auto simp: continuous_on_const)
1.135 +
1.136 +lemma simply_connected_eq_homotopic_circlemaps2b:
1.137 +  fixes S :: "'a::real_normed_vector set"
1.138 +  assumes "\<And>f g::complex \<Rightarrow> 'a.
1.139 +                \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
1.140 +                continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
1.141 +                \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
1.142 +  shows "path_connected S"
1.143 +proof (clarsimp simp add: path_connected_eq_homotopic_points)
1.144 +  fix a b
1.145 +  assume "a \<in> S" "b \<in> S"
1.146 +  then show "homotopic_loops S (linepath a a) (linepath b b)"
1.147 +    using homotopic_circlemaps_imp_homotopic_loops [OF assms [of "\<lambda>x. a" "\<lambda>x. b"]]
1.148 +    by (auto simp: o_def continuous_on_const linepath_def)
1.149 +qed
1.150 +
1.151 +lemma simply_connected_eq_homotopic_circlemaps3:
1.152 +  fixes h :: "complex \<Rightarrow> 'a::real_normed_vector"
1.153 +  assumes "path_connected S"
1.154 +      and hom: "\<And>f::complex \<Rightarrow> 'a.
1.155 +                  \<lbrakk>continuous_on (sphere 0 1) f; f `(sphere 0 1) \<subseteq> S\<rbrakk>
1.156 +                  \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)"
1.157 +    shows "simply_connected S"
1.158 +proof (clarsimp simp add: simply_connected_eq_contractible_loop_some assms)
1.159 +  fix p
1.160 +  assume p: "path p" "path_image p \<subseteq> S" "pathfinish p = pathstart p"
1.161 +  then have "homotopic_loops S p p"
1.162 +    by (simp add: homotopic_loops_refl)
1.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)"
1.164 +    by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom)
1.165 +  show "\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)"
1.166 +  proof (intro exI conjI)
1.167 +    show "a \<in> S"
1.168 +      using homotopic_with_imp_subset2 [OF homp]
1.169 +      by (metis dist_0_norm image_subset_iff mem_sphere norm_one)
1.170 +    have teq: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk>
1.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"
1.172 +      apply (rule disjCI)
1.173 +      using Arg_of_real [of 1] apply (auto simp: Arg_exp)
1.174 +      done
1.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>))"
1.176 +      apply (rule homotopic_loops_eq [OF p])
1.177 +      using p teq apply (fastforce simp: pathfinish_def pathstart_def)
1.178 +      done
1.179 +    then
1.180 +    show "homotopic_loops S p (linepath a a)"
1.181 +      by (simp add: linepath_refl  homotopic_loops_trans [OF _ homotopic_circlemaps_imp_homotopic_loops [OF homp, simplified K_record_comp]])
1.182 +  qed
1.183 +qed
1.184 +
1.185 +
1.186 +proposition simply_connected_eq_homotopic_circlemaps:
1.187 +  fixes S :: "'a::real_normed_vector set"
1.188 +  shows "simply_connected S \<longleftrightarrow>
1.189 +         (\<forall>f g::complex \<Rightarrow> 'a.
1.190 +              continuous_on (sphere 0 1) f \<and> f ` (sphere 0 1) \<subseteq> S \<and>
1.191 +              continuous_on (sphere 0 1) g \<and> g ` (sphere 0 1) \<subseteq> S
1.192 +              \<longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g)"
1.193 +  apply (rule iffI)
1.194 +   apply (blast elim: dest: simply_connected_eq_homotopic_circlemaps1)
1.195 +  by (simp add: simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3)
1.196 +
1.197 +proposition simply_connected_eq_contractible_circlemap:
1.198 +  fixes S :: "'a::real_normed_vector set"
1.199 +  shows "simply_connected S \<longleftrightarrow>
1.200 +         path_connected S \<and>
1.201 +         (\<forall>f::complex \<Rightarrow> 'a.
1.202 +              continuous_on (sphere 0 1) f \<and> f `(sphere 0 1) \<subseteq> S
1.203 +              \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)))"
1.204 +  apply (rule iffI)
1.205 +   apply (simp add: simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b)
1.206 +  using simply_connected_eq_homotopic_circlemaps3 by blast
1.207 +
1.208 +corollary homotopy_eqv_simple_connectedness:
1.209 +  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
1.210 +  shows "S homotopy_eqv T \<Longrightarrow> simply_connected S \<longleftrightarrow> simply_connected T"
1.211 +  by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality)
1.212 +
1.213  end
```