equal
deleted
inserted
replaced
3010 "path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++ |
3010 "path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++ |
3011 subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N))) |
3011 subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N))) |
3012 \<subseteq> ball (p t) (ee (p t))" |
3012 \<subseteq> ball (p t) (ee (p t))" |
3013 apply (intro subset_path_image_join pi_hgn pi_ghn') |
3013 apply (intro subset_path_image_join pi_hgn pi_ghn') |
3014 using \<open>N>0\<close> Suc.prems |
3014 using \<open>N>0\<close> Suc.prems |
3015 apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee) |
3015 apply (auto simp: path_image_subpath dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee) |
3016 done |
3016 done |
3017 have pi0: "(f has_contour_integral 0) |
3017 have pi0: "(f has_contour_integral 0) |
3018 (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++ |
3018 (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++ |
3019 subpath ((Suc n) / N) (n/N) h +++ linepath(h (n/N)) (g (n/N)))" |
3019 subpath ((Suc n) / N) (n/N) h +++ linepath(h (n/N)) (g (n/N)))" |
3020 apply (rule Cauchy_theorem_primitive [of "ball(p t) (ee(p t))" "ff (p t)" "f"]) |
3020 apply (rule Cauchy_theorem_primitive [of "ball(p t) (ee(p t))" "ff (p t)" "f"]) |
3490 |
3490 |
3491 lemma winding_number_trivial [simp]: "z \<noteq> a \<Longrightarrow> winding_number(linepath a a) z = 0" |
3491 lemma winding_number_trivial [simp]: "z \<noteq> a \<Longrightarrow> winding_number(linepath a a) z = 0" |
3492 by (simp add: winding_number_valid_path) |
3492 by (simp add: winding_number_valid_path) |
3493 |
3493 |
3494 lemma winding_number_subpath_trivial [simp]: "z \<noteq> g x \<Longrightarrow> winding_number (subpath x x g) z = 0" |
3494 lemma winding_number_subpath_trivial [simp]: "z \<noteq> g x \<Longrightarrow> winding_number (subpath x x g) z = 0" |
3495 by (simp add: winding_number_valid_path) |
3495 by (simp add: path_image_subpath winding_number_valid_path) |
3496 |
3496 |
3497 lemma winding_number_join: |
3497 lemma winding_number_join: |
3498 assumes g1: "path g1" "z \<notin> path_image g1" |
3498 assumes g1: "path g1" "z \<notin> path_image g1" |
3499 and g2: "path g2" "z \<notin> path_image g2" |
3499 and g2: "path g2" "z \<notin> path_image g2" |
3500 and "pathfinish g1 = pathstart g2" |
3500 and "pathfinish g1 = pathstart g2" |
3740 using g_C1_diff x by (auto simp: C1_differentiable_on_eq intro: continuous_on_interior) |
3740 using g_C1_diff x by (auto simp: C1_differentiable_on_eq intro: continuous_on_interior) |
3741 then have con_vd: "continuous (at x within {a..b}) (\<lambda>x. ?D\<gamma> x)" |
3741 then have con_vd: "continuous (at x within {a..b}) (\<lambda>x. ?D\<gamma> x)" |
3742 by (rule continuous_at_imp_continuous_within) |
3742 by (rule continuous_at_imp_continuous_within) |
3743 have gdx: "\<gamma> differentiable at x" |
3743 have gdx: "\<gamma> differentiable at x" |
3744 using x by (simp add: g_diff_at) |
3744 using x by (simp add: g_diff_at) |
3745 have "((\<lambda>c. Exp (- integral {a..c} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0)) |
3745 have "((\<lambda>c. exp (- integral {a..c} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0)) |
3746 (at x within {a..b})" |
3746 (at x within {a..b})" |
3747 using x gdx t |
3747 using x gdx t |
3748 apply (clarsimp simp add: differentiable_iff_scaleR) |
3748 apply (clarsimp simp add: differentiable_iff_scaleR) |
3749 apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_within) |
3749 apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_within) |
3750 apply (simp_all add: has_vector_derivative_def [symmetric]) |
3750 apply (simp_all add: has_vector_derivative_def [symmetric]) |
3779 by (simp add: field_simps) algebra |
3779 by (simp add: field_simps) algebra |
3780 obtain p where p: "valid_path p" "z \<notin> path_image p" |
3780 obtain p where p: "valid_path p" "z \<notin> path_image p" |
3781 "pathstart p = pathstart \<gamma>" "pathfinish p = pathfinish \<gamma>" |
3781 "pathstart p = pathstart \<gamma>" "pathfinish p = pathfinish \<gamma>" |
3782 "contour_integral p (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z" |
3782 "contour_integral p (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z" |
3783 using winding_number [OF assms, of 1] by auto |
3783 using winding_number [OF assms, of 1] by auto |
3784 have [simp]: "(winding_number \<gamma> z \<in> \<int>) = (Exp (contour_integral p (\<lambda>w. 1 / (w - z))) = 1)" |
3784 have [simp]: "(winding_number \<gamma> z \<in> \<int>) = (exp (contour_integral p (\<lambda>w. 1 / (w - z))) = 1)" |
3785 using p by (simp add: exp_eq_1 complex_is_Int_iff) |
3785 using p by (simp add: exp_eq_1 complex_is_Int_iff) |
3786 have "winding_number p z \<in> \<int> \<longleftrightarrow> pathfinish p = pathstart p" |
3786 have "winding_number p z \<in> \<int> \<longleftrightarrow> pathfinish p = pathstart p" |
3787 using p z |
3787 using p z |
3788 apply (simp add: winding_number_valid_path valid_path_def path_image_def pathstart_def pathfinish_def) |
3788 apply (simp add: winding_number_valid_path valid_path_def path_image_def pathstart_def pathfinish_def) |
3789 using winding_number_exp_integral(2) [of p 0 1 z] |
3789 using winding_number_exp_integral(2) [of p 0 1 z] |
3838 def i \<equiv> "integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))" |
3838 def i \<equiv> "integral {0..t} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))" |
3839 have iArg: "Arg r = Im i" |
3839 have iArg: "Arg r = Im i" |
3840 using eqArg by (simp add: i_def) |
3840 using eqArg by (simp add: i_def) |
3841 have gpdt: "\<gamma> piecewise_C1_differentiable_on {0..t}" |
3841 have gpdt: "\<gamma> piecewise_C1_differentiable_on {0..t}" |
3842 by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl piecewise_C1_differentiable_on_subset gpd t) |
3842 by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl piecewise_C1_differentiable_on_subset gpd t) |
3843 have "Exp (- i) * (\<gamma> t - z) = \<gamma> 0 - z" |
3843 have "exp (- i) * (\<gamma> t - z) = \<gamma> 0 - z" |
3844 unfolding i_def |
3844 unfolding i_def |
3845 apply (rule winding_number_exp_integral [OF gpdt]) |
3845 apply (rule winding_number_exp_integral [OF gpdt]) |
3846 using t z unfolding path_image_def |
3846 using t z unfolding path_image_def |
3847 apply force+ |
3847 apply force+ |
3848 done |
3848 done |
3853 then have "z + complex_of_real (exp (Re i)) * (w - z) / complex_of_real (cmod r) = \<gamma> t" |
3853 then have "z + complex_of_real (exp (Re i)) * (w - z) / complex_of_real (cmod r) = \<gamma> t" |
3854 apply (simp add:) |
3854 apply (simp add:) |
3855 apply (subst Complex_Transcendental.Arg_eq [of r]) |
3855 apply (subst Complex_Transcendental.Arg_eq [of r]) |
3856 apply (simp add: iArg) |
3856 apply (simp add: iArg) |
3857 using * |
3857 using * |
3858 apply (simp add: Exp_eq_polar field_simps) |
3858 apply (simp add: exp_eq_polar field_simps) |
3859 done |
3859 done |
3860 with t show ?thesis |
3860 with t show ?thesis |
3861 by (rule_tac x="exp(Re i) / norm r" in exI) (auto simp: path_image_def) |
3861 by (rule_tac x="exp(Re i) / norm r" in exI) (auto simp: path_image_def) |
3862 qed |
3862 qed |
3863 |
3863 |
4223 apply (simp add: contour_integral_subcontour_integral [OF contour_integrable_inversediff]) |
4223 apply (simp add: contour_integral_subcontour_integral [OF contour_integrable_inversediff]) |
4224 done |
4224 done |
4225 also have "... = winding_number (subpath 0 x \<gamma>) z" |
4225 also have "... = winding_number (subpath 0 x \<gamma>) z" |
4226 apply (subst winding_number_valid_path) |
4226 apply (subst winding_number_valid_path) |
4227 using assms x |
4227 using assms x |
4228 apply (simp_all add: valid_path_subpath) |
4228 apply (simp_all add: path_image_subpath valid_path_subpath) |
4229 by (force simp: closed_segment_eq_real_ivl path_image_def) |
4229 by (force simp: path_image_def) |
4230 finally show ?thesis . |
4230 finally show ?thesis . |
4231 qed |
4231 qed |
4232 show ?thesis |
4232 show ?thesis |
4233 apply (rule continuous_on_eq |
4233 apply (rule continuous_on_eq |
4234 [where f = "\<lambda>x. 1 / (2*pi*ii) * |
4234 [where f = "\<lambda>x. 1 / (2*pi*ii) * |
4275 then obtain t::real where t: "0 \<le> t" "t \<le> 1" and sub12: "Re (winding_number (subpath 0 t \<gamma>) z) = 1/2" |
4275 then obtain t::real where t: "0 \<le> t" "t \<le> 1" and sub12: "Re (winding_number (subpath 0 t \<gamma>) z) = 1/2" |
4276 using winding_number_ivt_pos [OF \<gamma> z, of "1/2"] by auto |
4276 using winding_number_ivt_pos [OF \<gamma> z, of "1/2"] by auto |
4277 have gt: "\<gamma> t - z = - (of_real (exp (- (2 * pi * Im (winding_number (subpath 0 t \<gamma>) z)))) * (\<gamma> 0 - z))" |
4277 have gt: "\<gamma> t - z = - (of_real (exp (- (2 * pi * Im (winding_number (subpath 0 t \<gamma>) z)))) * (\<gamma> 0 - z))" |
4278 using winding_number_exp_2pi [of "subpath 0 t \<gamma>" z] |
4278 using winding_number_exp_2pi [of "subpath 0 t \<gamma>" z] |
4279 apply (simp add: t \<gamma> valid_path_imp_path) |
4279 apply (simp add: t \<gamma> valid_path_imp_path) |
4280 using closed_segment_eq_real_ivl path_image_def t z by (fastforce simp add: Euler sub12) |
4280 using closed_segment_eq_real_ivl path_image_def t z by (fastforce simp: path_image_subpath Euler sub12) |
4281 have "b < a \<bullet> \<gamma> 0" |
4281 have "b < a \<bullet> \<gamma> 0" |
4282 proof - |
4282 proof - |
4283 have "\<gamma> 0 \<in> {c. b < a \<bullet> c}" |
4283 have "\<gamma> 0 \<in> {c. b < a \<bullet> c}" |
4284 by (metis (no_types) pag atLeastAtMost_iff image_subset_iff order_refl path_image_def zero_le_one) |
4284 by (metis (no_types) pag atLeastAtMost_iff image_subset_iff order_refl path_image_def zero_le_one) |
4285 thus ?thesis |
4285 thus ?thesis |
4319 proof - |
4319 proof - |
4320 { assume wnz_12: "\<bar>Re (winding_number \<gamma> z)\<bar> > 1/2" |
4320 { assume wnz_12: "\<bar>Re (winding_number \<gamma> z)\<bar> > 1/2" |
4321 have "isCont (winding_number \<gamma>) z" |
4321 have "isCont (winding_number \<gamma>) z" |
4322 by (metis continuous_at_winding_number valid_path_imp_path \<gamma> z) |
4322 by (metis continuous_at_winding_number valid_path_imp_path \<gamma> z) |
4323 then obtain d where "d>0" and d: "\<And>x'. dist x' z < d \<Longrightarrow> dist (winding_number \<gamma> x') (winding_number \<gamma> z) < abs(Re(winding_number \<gamma> z)) - 1/2" |
4323 then obtain d where "d>0" and d: "\<And>x'. dist x' z < d \<Longrightarrow> dist (winding_number \<gamma> x') (winding_number \<gamma> z) < abs(Re(winding_number \<gamma> z)) - 1/2" |
4324 using continuous_at_eps_delta wnz_12 diff_less_iff(1) by blast |
4324 using continuous_at_eps_delta wnz_12 diff_gt_0_iff_gt by blast |
4325 def z' \<equiv> "z - (d / (2 * cmod a)) *\<^sub>R a" |
4325 def z' \<equiv> "z - (d / (2 * cmod a)) *\<^sub>R a" |
4326 have *: "a \<bullet> z' \<le> b - d / 3 * cmod a" |
4326 have *: "a \<bullet> z' \<le> b - d / 3 * cmod a" |
4327 unfolding z'_def inner_mult_right' divide_inverse |
4327 unfolding z'_def inner_mult_right' divide_inverse |
4328 apply (simp add: divide_simps algebra_simps dot_square_norm power2_eq_square anz) |
4328 apply (simp add: divide_simps algebra_simps dot_square_norm power2_eq_square anz) |
4329 apply (metis `0 < d` add_increasing azb less_eq_real_def mult_nonneg_nonneg mult_right_mono norm_ge_zero norm_numeral) |
4329 apply (metis `0 < d` add_increasing azb less_eq_real_def mult_nonneg_nonneg mult_right_mono norm_ge_zero norm_numeral) |