equal
deleted
inserted
replaced
1139 apply (rule mult_right_mono [OF \<delta>]) |
1139 apply (rule mult_right_mono [OF \<delta>]) |
1140 apply (auto simp: dist_commute Rings.ordered_semiring_class.mult_right_mono \<delta>) |
1140 apply (auto simp: dist_commute Rings.ordered_semiring_class.mult_right_mono \<delta>) |
1141 done |
1141 done |
1142 with \<open>e>0\<close> show ?thesis by force |
1142 with \<open>e>0\<close> show ?thesis by force |
1143 qed |
1143 qed |
1144 have "inj (op * (deriv f \<xi>))" |
1144 have "inj (( * ) (deriv f \<xi>))" |
1145 using dnz by simp |
1145 using dnz by simp |
1146 then obtain g' where g': "linear g'" "g' \<circ> op * (deriv f \<xi>) = id" |
1146 then obtain g' where g': "linear g'" "g' \<circ> ( * ) (deriv f \<xi>) = id" |
1147 using linear_injective_left_inverse [of "op * (deriv f \<xi>)"] |
1147 using linear_injective_left_inverse [of "( * ) (deriv f \<xi>)"] |
1148 by (auto simp: linear_times) |
1148 by (auto simp: linear_times) |
1149 show ?thesis |
1149 show ?thesis |
1150 apply (rule has_derivative_locally_injective [OF S, where f=f and f' = "\<lambda>z h. deriv f z * h" and g' = g']) |
1150 apply (rule has_derivative_locally_injective [OF S, where f=f and f' = "\<lambda>z h. deriv f z * h" and g' = g']) |
1151 using g' * |
1151 using g' * |
1152 apply (simp_all add: linear_conv_bounded_linear that) |
1152 apply (simp_all add: linear_conv_bounded_linear that) |
2091 apply (rule derivative_eq_intros | simp add: C_def False fo)+ |
2091 apply (rule derivative_eq_intros | simp add: C_def False fo)+ |
2092 using \<open>0 < r\<close> |
2092 using \<open>0 < r\<close> |
2093 apply (simp add: C_def False fo) |
2093 apply (simp add: C_def False fo) |
2094 apply (simp add: derivative_intros dfa complex_derivative_chain) |
2094 apply (simp add: derivative_intros dfa complex_derivative_chain) |
2095 done |
2095 done |
2096 have sb1: "op * (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1 |
2096 have sb1: "( * ) (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1 |
2097 \<subseteq> f ` ball a r" |
2097 \<subseteq> f ` ball a r" |
2098 using \<open>0 < r\<close> by (auto simp: dist_norm norm_mult C_def False) |
2098 using \<open>0 < r\<close> by (auto simp: dist_norm norm_mult C_def False) |
2099 have sb2: "ball (C * r * b) r' \<subseteq> op * (C * r) ` ball b t" |
2099 have sb2: "ball (C * r * b) r' \<subseteq> ( * ) (C * r) ` ball b t" |
2100 if "1 / 12 < t" for b t |
2100 if "1 / 12 < t" for b t |
2101 proof - |
2101 proof - |
2102 have *: "r * cmod (deriv f a) / 12 \<le> r * (t * cmod (deriv f a))" |
2102 have *: "r * cmod (deriv f a) / 12 \<le> r * (t * cmod (deriv f a))" |
2103 using that \<open>0 < r\<close> less_eq_real_def mult.commute mult.right_neutral mult_left_mono norm_ge_zero times_divide_eq_right |
2103 using that \<open>0 < r\<close> less_eq_real_def mult.commute mult.right_neutral mult_left_mono norm_ge_zero times_divide_eq_right |
2104 by auto |
2104 by auto |
2600 obtain n::int where "n=winding_number g p" |
2600 obtain n::int where "n=winding_number g p" |
2601 using integer_winding_number[OF _ g_loop,of p] valid path_img |
2601 using integer_winding_number[OF _ g_loop,of p] valid path_img |
2602 by (metis DiffD2 Ints_cases insertI1 subset_eq valid_path_imp_path) |
2602 by (metis DiffD2 Ints_cases insertI1 subset_eq valid_path_imp_path) |
2603 define p_circ where "p_circ \<equiv> circlepath p (h p)" |
2603 define p_circ where "p_circ \<equiv> circlepath p (h p)" |
2604 define p_circ_pt where "p_circ_pt \<equiv> linepath (p+h p) (p+h p)" |
2604 define p_circ_pt where "p_circ_pt \<equiv> linepath (p+h p) (p+h p)" |
2605 define n_circ where "n_circ \<equiv> \<lambda>n. (op +++ p_circ ^^ n) p_circ_pt" |
2605 define n_circ where "n_circ \<equiv> \<lambda>n. ((+++) p_circ ^^ n) p_circ_pt" |
2606 define cp where "cp \<equiv> if n\<ge>0 then reversepath (n_circ (nat n)) else n_circ (nat (- n))" |
2606 define cp where "cp \<equiv> if n\<ge>0 then reversepath (n_circ (nat n)) else n_circ (nat (- n))" |
2607 have n_circ:"valid_path (n_circ k)" |
2607 have n_circ:"valid_path (n_circ k)" |
2608 "winding_number (n_circ k) p = k" |
2608 "winding_number (n_circ k) p = k" |
2609 "pathstart (n_circ k) = p + h p" "pathfinish (n_circ k) = p + h p" |
2609 "pathstart (n_circ k) = p + h p" "pathfinish (n_circ k) = p + h p" |
2610 "path_image (n_circ k) = (if k=0 then {p + h p} else sphere p (h p))" |
2610 "path_image (n_circ k) = (if k=0 then {p + h p} else sphere p (h p))" |
3859 unfolding h_def der_def using g_holo f_holo \<open>open s\<close> |
3859 unfolding h_def der_def using g_holo f_holo \<open>open s\<close> |
3860 by (auto intro!: holomorphic_derivI derivative_eq_intros) |
3860 by (auto intro!: holomorphic_derivI derivative_eq_intros) |
3861 then show "h field_differentiable at (\<gamma> x)" |
3861 then show "h field_differentiable at (\<gamma> x)" |
3862 unfolding t_def field_differentiable_def by blast |
3862 unfolding t_def field_differentiable_def by blast |
3863 qed |
3863 qed |
3864 then have " (op / 1 has_contour_integral 0) (h \<circ> \<gamma>) |
3864 then have " ((/) 1 has_contour_integral 0) (h \<circ> \<gamma>) |
3865 = ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>" |
3865 = ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>" |
3866 unfolding has_contour_integral |
3866 unfolding has_contour_integral |
3867 apply (intro has_integral_spike_eq[OF negligible_finite, OF \<open>finite spikes\<close>]) |
3867 apply (intro has_integral_spike_eq[OF negligible_finite, OF \<open>finite spikes\<close>]) |
3868 by auto |
3868 by auto |
3869 ultimately show ?thesis by auto |
3869 ultimately show ?thesis by auto |