src/HOL/Analysis/Complex_Transcendental.thy
changeset 64790 ed38f9a834d8
parent 64773 223b2ebdda79
child 65036 ab7e11730ad8
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Jan 05 15:03:37 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Jan 05 16:03:23 2017 +0000
     1.3 @@ -3559,4 +3559,70 @@
     1.4    shows "S homotopy_eqv T \<Longrightarrow> simply_connected S \<longleftrightarrow> simply_connected T"
     1.5    by (simp add: simply_connected_eq_homotopic_circlemaps homotopy_eqv_homotopic_triviality)
     1.6  
     1.7 +
     1.8 +subsection\<open>Homeomorphism of simple closed curves to circles\<close>
     1.9 +
    1.10 +proposition homeomorphic_simple_path_image_circle:
    1.11 +  fixes a :: complex and \<gamma> :: "real \<Rightarrow> 'a::t2_space"
    1.12 +  assumes "simple_path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and "0 < r"
    1.13 +  shows "(path_image \<gamma>) homeomorphic sphere a r"
    1.14 +proof -
    1.15 +  have "homotopic_loops (path_image \<gamma>) \<gamma> \<gamma>"
    1.16 +    by (simp add: assms homotopic_loops_refl simple_path_imp_path)
    1.17 +  then have hom: "homotopic_with (\<lambda>h. True) (sphere 0 1) (path_image \<gamma>)
    1.18 +               (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi)))"
    1.19 +    by (rule homotopic_loops_imp_homotopic_circlemaps)
    1.20 +  have "\<exists>g. homeomorphism (sphere 0 1) (path_image \<gamma>) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) g"
    1.21 +  proof (rule homeomorphism_compact)
    1.22 +    show "continuous_on (sphere 0 1) (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi)))"
    1.23 +      using hom homotopic_with_imp_continuous by blast
    1.24 +    show "inj_on (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) (sphere 0 1)"
    1.25 +    proof
    1.26 +      fix x y
    1.27 +      assume xy: "x \<in> sphere 0 1" "y \<in> sphere 0 1"
    1.28 +         and eq: "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) x = (\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) y"
    1.29 +      then have "(Arg x / (2*pi)) = (Arg y / (2*pi))"
    1.30 +      proof -
    1.31 +        have "(Arg x / (2*pi)) \<in> {0..1}" "(Arg y / (2*pi)) \<in> {0..1}"
    1.32 +          using Arg_ge_0 Arg_lt_2pi dual_order.strict_iff_order by fastforce+
    1.33 +        with eq show ?thesis
    1.34 +          using \<open>simple_path \<gamma>\<close> Arg_lt_2pi unfolding simple_path_def o_def
    1.35 +          by (metis eq_divide_eq_1 not_less_iff_gr_or_eq)
    1.36 +      qed
    1.37 +      with xy show "x = y"
    1.38 +        by (metis Arg Arg_0 dist_0_norm divide_cancel_right dual_order.strict_iff_order mem_sphere)
    1.39 +    qed
    1.40 +    have "\<And>z. cmod z = 1 \<Longrightarrow> \<exists>x\<in>{0..1}. \<gamma> (Arg z / (2*pi)) = \<gamma> x"
    1.41 +       by (metis Arg_ge_0 Arg_lt_2pi atLeastAtMost_iff divide_less_eq_1 less_eq_real_def zero_less_mult_iff pi_gt_zero zero_le_divide_iff zero_less_numeral)
    1.42 +     moreover have "\<exists>z\<in>sphere 0 1. \<gamma> x = \<gamma> (Arg z / (2*pi))" if "0 \<le> x" "x \<le> 1" for x
    1.43 +     proof (cases "x=1")
    1.44 +       case True
    1.45 +       then show ?thesis
    1.46 +         apply (rule_tac x=1 in bexI)
    1.47 +         apply (metis loop Arg_of_real divide_eq_0_iff of_real_1 pathfinish_def pathstart_def \<open>0 \<le> x\<close>, auto)
    1.48 +         done
    1.49 +     next
    1.50 +       case False
    1.51 +       then have *: "(Arg (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
    1.52 +         using that by (auto simp: Arg_exp divide_simps)
    1.53 +       show ?thesis
    1.54 +         by (rule_tac x="exp(ii* of_real(2*pi*x))" in bexI) (auto simp: *)
    1.55 +    qed
    1.56 +    ultimately show "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) ` sphere 0 1 = path_image \<gamma>"
    1.57 +      by (auto simp: path_image_def image_iff)
    1.58 +    qed auto
    1.59 +    then have "path_image \<gamma> homeomorphic sphere (0::complex) 1"
    1.60 +      using homeomorphic_def homeomorphic_sym by blast
    1.61 +  also have "... homeomorphic sphere a r"
    1.62 +    by (simp add: assms homeomorphic_spheres)
    1.63 +  finally show ?thesis .
    1.64 +qed
    1.65 +
    1.66 +lemma homeomorphic_simple_path_images:
    1.67 +  fixes \<gamma>1 :: "real \<Rightarrow> 'a::t2_space" and \<gamma>2 :: "real \<Rightarrow> 'b::t2_space"
    1.68 +  assumes "simple_path \<gamma>1" and loop: "pathfinish \<gamma>1 = pathstart \<gamma>1"
    1.69 +  assumes "simple_path \<gamma>2" and loop: "pathfinish \<gamma>2 = pathstart \<gamma>2"
    1.70 +  shows "(path_image \<gamma>1) homeomorphic (path_image \<gamma>2)"
    1.71 +  by (meson assms homeomorphic_simple_path_image_circle homeomorphic_sym homeomorphic_trans loop pi_gt_zero)
    1.72 +
    1.73  end