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