|
1 section \<open>Winding Numbers\<close> |
|
2 |
|
3 text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2017)\<close> |
|
4 |
|
5 theory Winding_Numbers |
|
6 imports Polytope Jordan_Curve Cauchy_Integral_Theorem |
|
7 begin |
|
8 |
|
9 subsection\<open>Winding number for a triangle\<close> |
|
10 |
|
11 lemma wn_triangle1: |
|
12 assumes "0 \<in> interior(convex hull {a,b,c})" |
|
13 shows "~ (Im(a/b) \<le> 0 \<and> 0 \<le> Im(b/c))" |
|
14 proof - |
|
15 { assume 0: "Im(a/b) \<le> 0" "0 \<le> Im(b/c)" |
|
16 have "0 \<notin> interior (convex hull {a,b,c})" |
|
17 proof (cases "a=0 \<or> b=0 \<or> c=0") |
|
18 case True then show ?thesis |
|
19 by (auto simp: not_in_interior_convex_hull_3) |
|
20 next |
|
21 case False |
|
22 then have "b \<noteq> 0" by blast |
|
23 { fix x y::complex and u::real |
|
24 assume eq_f': "Im x * Re b \<le> Im b * Re x" "Im y * Re b \<le> Im b * Re y" "0 \<le> u" "u \<le> 1" |
|
25 then have "((1 - u) * Im x) * Re b \<le> Im b * ((1 - u) * Re x)" |
|
26 by (simp add: mult_left_mono mult.assoc mult.left_commute [of "Im b"]) |
|
27 then have "((1 - u) * Im x + u * Im y) * Re b \<le> Im b * ((1 - u) * Re x + u * Re y)" |
|
28 using eq_f' ordered_comm_semiring_class.comm_mult_left_mono |
|
29 by (fastforce simp add: algebra_simps) |
|
30 } |
|
31 with False 0 have "convex hull {a,b,c} \<le> {z. Im z * Re b \<le> Im b * Re z}" |
|
32 apply (simp add: Complex.Im_divide divide_simps complex_neq_0 [symmetric]) |
|
33 apply (simp add: algebra_simps) |
|
34 apply (rule hull_minimal) |
|
35 apply (auto simp: algebra_simps convex_alt) |
|
36 done |
|
37 moreover have "0 \<notin> interior({z. Im z * Re b \<le> Im b * Re z})" |
|
38 proof |
|
39 assume "0 \<in> interior {z. Im z * Re b \<le> Im b * Re z}" |
|
40 then obtain e where "e>0" and e: "ball 0 e \<subseteq> {z. Im z * Re b \<le> Im b * Re z}" |
|
41 by (meson mem_interior) |
|
42 def z \<equiv> "- sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * ii" |
|
43 have "z \<in> ball 0 e" |
|
44 using `e>0` |
|
45 apply (simp add: z_def dist_norm) |
|
46 apply (rule le_less_trans [OF norm_triangle_ineq4]) |
|
47 apply (simp add: norm_mult abs_sgn_eq) |
|
48 done |
|
49 then have "z \<in> {z. Im z * Re b \<le> Im b * Re z}" |
|
50 using e by blast |
|
51 then show False |
|
52 using `e>0` `b \<noteq> 0` |
|
53 apply (simp add: z_def dist_norm sgn_if less_eq_real_def mult_less_0_iff complex.expand split: if_split_asm) |
|
54 apply (auto simp: algebra_simps) |
|
55 apply (meson less_asym less_trans mult_pos_pos neg_less_0_iff_less) |
|
56 by (metis less_asym mult_pos_pos neg_less_0_iff_less) |
|
57 qed |
|
58 ultimately show ?thesis |
|
59 using interior_mono by blast |
|
60 qed |
|
61 } with assms show ?thesis by blast |
|
62 qed |
|
63 |
|
64 lemma wn_triangle2_0: |
|
65 assumes "0 \<in> interior(convex hull {a,b,c})" |
|
66 shows |
|
67 "0 < Im((b - a) * cnj (b)) \<and> |
|
68 0 < Im((c - b) * cnj (c)) \<and> |
|
69 0 < Im((a - c) * cnj (a)) |
|
70 \<or> |
|
71 Im((b - a) * cnj (b)) < 0 \<and> |
|
72 0 < Im((b - c) * cnj (b)) \<and> |
|
73 0 < Im((a - b) * cnj (a)) \<and> |
|
74 0 < Im((c - a) * cnj (c))" |
|
75 proof - |
|
76 have [simp]: "{b,c,a} = {a,b,c}" "{c,a,b} = {a,b,c}" by auto |
|
77 show ?thesis |
|
78 using wn_triangle1 [OF assms] wn_triangle1 [of b c a] wn_triangle1 [of c a b] assms |
|
79 by (auto simp: algebra_simps Im_complex_div_gt_0 Im_complex_div_lt_0 not_le not_less) |
|
80 qed |
|
81 |
|
82 lemma wn_triangle2: |
|
83 assumes "z \<in> interior(convex hull {a,b,c})" |
|
84 shows "0 < Im((b - a) * cnj (b - z)) \<and> |
|
85 0 < Im((c - b) * cnj (c - z)) \<and> |
|
86 0 < Im((a - c) * cnj (a - z)) |
|
87 \<or> |
|
88 Im((b - a) * cnj (b - z)) < 0 \<and> |
|
89 0 < Im((b - c) * cnj (b - z)) \<and> |
|
90 0 < Im((a - b) * cnj (a - z)) \<and> |
|
91 0 < Im((c - a) * cnj (c - z))" |
|
92 proof - |
|
93 have 0: "0 \<in> interior(convex hull {a-z, b-z, c-z})" |
|
94 using assms convex_hull_translation [of "-z" "{a,b,c}"] |
|
95 interior_translation [of "-z"] |
|
96 by simp |
|
97 show ?thesis using wn_triangle2_0 [OF 0] |
|
98 by simp |
|
99 qed |
|
100 |
|
101 lemma wn_triangle3: |
|
102 assumes z: "z \<in> interior(convex hull {a,b,c})" |
|
103 and "0 < Im((b-a) * cnj (b-z))" |
|
104 "0 < Im((c-b) * cnj (c-z))" |
|
105 "0 < Im((a-c) * cnj (a-z))" |
|
106 shows "winding_number (linepath a b +++ linepath b c +++ linepath c a) z = 1" |
|
107 proof - |
|
108 have znot[simp]: "z \<notin> closed_segment a b" "z \<notin> closed_segment b c" "z \<notin> closed_segment c a" |
|
109 using z interior_of_triangle [of a b c] |
|
110 by (auto simp: closed_segment_def) |
|
111 have gt0: "0 < Re (winding_number (linepath a b +++ linepath b c +++ linepath c a) z)" |
|
112 using assms |
|
113 by (simp add: winding_number_linepath_pos_lt path_image_join winding_number_join_pos_combined) |
|
114 have lt2: "Re (winding_number (linepath a b +++ linepath b c +++ linepath c a) z) < 2" |
|
115 using winding_number_lt_half_linepath [of _ a b] |
|
116 using winding_number_lt_half_linepath [of _ b c] |
|
117 using winding_number_lt_half_linepath [of _ c a] znot |
|
118 apply (fastforce simp add: winding_number_join path_image_join) |
|
119 done |
|
120 show ?thesis |
|
121 by (rule winding_number_eq_1) (simp_all add: path_image_join gt0 lt2) |
|
122 qed |
|
123 |
|
124 proposition winding_number_triangle: |
|
125 assumes z: "z \<in> interior(convex hull {a,b,c})" |
|
126 shows "winding_number(linepath a b +++ linepath b c +++ linepath c a) z = |
|
127 (if 0 < Im((b - a) * cnj (b - z)) then 1 else -1)" |
|
128 proof - |
|
129 have [simp]: "{a,c,b} = {a,b,c}" by auto |
|
130 have znot[simp]: "z \<notin> closed_segment a b" "z \<notin> closed_segment b c" "z \<notin> closed_segment c a" |
|
131 using z interior_of_triangle [of a b c] |
|
132 by (auto simp: closed_segment_def) |
|
133 then have [simp]: "z \<notin> closed_segment b a" "z \<notin> closed_segment c b" "z \<notin> closed_segment a c" |
|
134 using closed_segment_commute by blast+ |
|
135 have *: "winding_number (linepath a b +++ linepath b c +++ linepath c a) z = |
|
136 winding_number (reversepath (linepath a c +++ linepath c b +++ linepath b a)) z" |
|
137 by (simp add: reversepath_joinpaths winding_number_join not_in_path_image_join) |
|
138 show ?thesis |
|
139 using wn_triangle2 [OF z] apply (rule disjE) |
|
140 apply (simp add: wn_triangle3 z) |
|
141 apply (simp add: path_image_join winding_number_reversepath * wn_triangle3 z) |
|
142 done |
|
143 qed |
|
144 |
|
145 subsection\<open>Winding numbers for simple closed paths\<close> |
|
146 |
|
147 lemma winding_number_from_innerpath: |
|
148 assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b" |
|
149 and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b" |
|
150 and "simple_path c" and c: "pathstart c = a" "pathfinish c = b" |
|
151 and c1c2: "path_image c1 \<inter> path_image c2 = {a,b}" |
|
152 and c1c: "path_image c1 \<inter> path_image c = {a,b}" |
|
153 and c2c: "path_image c2 \<inter> path_image c = {a,b}" |
|
154 and ne_12: "path_image c \<inter> inside(path_image c1 \<union> path_image c2) \<noteq> {}" |
|
155 and z: "z \<in> inside(path_image c1 \<union> path_image c)" |
|
156 and wn_d: "winding_number (c1 +++ reversepath c) z = d" |
|
157 and "a \<noteq> b" "d \<noteq> 0" |
|
158 obtains "z \<in> inside(path_image c1 \<union> path_image c2)" "winding_number (c1 +++ reversepath c2) z = d" |
|
159 proof - |
|
160 obtain 0: "inside(path_image c1 \<union> path_image c) \<inter> inside(path_image c2 \<union> path_image c) = {}" |
|
161 and 1: "inside(path_image c1 \<union> path_image c) \<union> inside(path_image c2 \<union> path_image c) \<union> |
|
162 (path_image c - {a,b}) = inside(path_image c1 \<union> path_image c2)" |
|
163 by (rule split_inside_simple_closed_curve |
|
164 [OF \<open>simple_path c1\<close> c1 \<open>simple_path c2\<close> c2 \<open>simple_path c\<close> c \<open>a \<noteq> b\<close> c1c2 c1c c2c ne_12]) |
|
165 have znot: "z \<notin> path_image c" "z \<notin> path_image c1" "z \<notin> path_image c2" |
|
166 using union_with_outside z 1 by auto |
|
167 have wn_cc2: "winding_number (c +++ reversepath c2) z = 0" |
|
168 apply (rule winding_number_zero_in_outside) |
|
169 apply (simp_all add: \<open>simple_path c2\<close> c c2 \<open>simple_path c\<close> simple_path_imp_path path_image_join) |
|
170 by (metis "0" ComplI UnE disjoint_iff_not_equal sup.commute union_with_inside z znot) |
|
171 show ?thesis |
|
172 proof |
|
173 show "z \<in> inside (path_image c1 \<union> path_image c2)" |
|
174 using "1" z by blast |
|
175 have "winding_number c1 z - winding_number c z = d " |
|
176 using assms znot |
|
177 by (metis wn_d winding_number_join simple_path_imp_path winding_number_reversepath add.commute path_image_reversepath path_reversepath pathstart_reversepath uminus_add_conv_diff) |
|
178 then show "winding_number (c1 +++ reversepath c2) z = d" |
|
179 using wn_cc2 by (simp add: winding_number_join simple_path_imp_path assms znot winding_number_reversepath) |
|
180 qed |
|
181 qed |
|
182 |
|
183 |
|
184 |
|
185 lemma simple_closed_path_wn1: |
|
186 fixes a::complex and e::real |
|
187 assumes "0 < e" |
|
188 and sp_pl: "simple_path(p +++ linepath (a - e) (a + e))" |
|
189 and psp: "pathstart p = a + e" |
|
190 and pfp: "pathfinish p = a - e" |
|
191 and disj: "ball a e \<inter> path_image p = {}" |
|
192 obtains z where "z \<in> inside (path_image (p +++ linepath (a - e) (a + e)))" |
|
193 "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) = 1" |
|
194 proof - |
|
195 have "arc p" and arc_lp: "arc (linepath (a - e) (a + e))" |
|
196 and pap: "path_image p \<inter> path_image (linepath (a - e) (a + e)) \<subseteq> {pathstart p, a-e}" |
|
197 using simple_path_join_loop_eq [of "linepath (a - e) (a + e)" p] assms by auto |
|
198 have mid_eq_a: "midpoint (a - e) (a + e) = a" |
|
199 by (simp add: midpoint_def) |
|
200 then have "a \<in> path_image(p +++ linepath (a - e) (a + e))" |
|
201 apply (simp add: assms path_image_join) |
|
202 by (metis midpoint_in_closed_segment) |
|
203 have "a \<in> frontier(inside (path_image(p +++ linepath (a - e) (a + e))))" |
|
204 apply (simp add: assms Jordan_inside_outside) |
|
205 apply (simp_all add: assms path_image_join) |
|
206 by (metis mid_eq_a midpoint_in_closed_segment) |
|
207 with \<open>0 < e\<close> obtain c where c: "c \<in> inside (path_image(p +++ linepath (a - e) (a + e)))" |
|
208 and dac: "dist a c < e" |
|
209 by (auto simp: frontier_straddle) |
|
210 then have "c \<notin> path_image(p +++ linepath (a - e) (a + e))" |
|
211 using inside_no_overlap by blast |
|
212 then have "c \<notin> path_image p" |
|
213 "c \<notin> closed_segment (a - of_real e) (a + of_real e)" |
|
214 by (simp_all add: assms path_image_join) |
|
215 with \<open>0 < e\<close> dac have "c \<notin> affine hull {a - of_real e, a + of_real e}" |
|
216 by (simp add: segment_as_ball not_le) |
|
217 with \<open>0 < e\<close> have *: "~collinear{a - e, c,a + e}" |
|
218 using collinear_3_affine_hull [of "a-e" "a+e"] by (auto simp: insert_commute) |
|
219 have 13: "1/3 + 1/3 + 1/3 = (1::real)" by simp |
|
220 have "(1/3) *\<^sub>R (a - of_real e) + (1/3) *\<^sub>R c + (1/3) *\<^sub>R (a + of_real e) \<in> interior(convex hull {a - e, c, a + e})" |
|
221 using interior_convex_hull_3_minimal [OF * DIM_complex] |
|
222 by clarsimp (metis 13 zero_less_divide_1_iff zero_less_numeral) |
|
223 then obtain z where z: "z \<in> interior(convex hull {a - e, c, a + e})" by force |
|
224 have [simp]: "z \<notin> closed_segment (a - e) c" |
|
225 by (metis DIM_complex Diff_iff IntD2 inf_sup_absorb interior_of_triangle z) |
|
226 have [simp]: "z \<notin> closed_segment (a + e) (a - e)" |
|
227 by (metis DIM_complex DiffD2 Un_iff interior_of_triangle z) |
|
228 have [simp]: "z \<notin> closed_segment c (a + e)" |
|
229 by (metis (no_types, lifting) DIM_complex DiffD2 Un_insert_right inf_sup_aci(5) insertCI interior_of_triangle mk_disjoint_insert z) |
|
230 show thesis |
|
231 proof |
|
232 have "norm (winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z) = 1" |
|
233 using winding_number_triangle [OF z] by simp |
|
234 have zin: "z \<in> inside (path_image (linepath (a + e) (a - e)) \<union> path_image p)" |
|
235 and zeq: "winding_number (linepath (a + e) (a - e) +++ reversepath p) z = |
|
236 winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z" |
|
237 proof (rule winding_number_from_innerpath |
|
238 [of "linepath (a + e) (a - e)" "a+e" "a-e" p |
|
239 "linepath (a + e) c +++ linepath c (a - e)" z |
|
240 "winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"]) |
|
241 show sp_aec: "simple_path (linepath (a + e) c +++ linepath c (a - e))" |
|
242 proof (rule arc_imp_simple_path [OF arc_join]) |
|
243 show "arc (linepath (a + e) c)" |
|
244 by (metis \<open>c \<notin> path_image p\<close> arc_linepath pathstart_in_path_image psp) |
|
245 show "arc (linepath c (a - e))" |
|
246 by (metis \<open>c \<notin> path_image p\<close> arc_linepath pathfinish_in_path_image pfp) |
|
247 show "path_image (linepath (a + e) c) \<inter> path_image (linepath c (a - e)) \<subseteq> {pathstart (linepath c (a - e))}" |
|
248 by clarsimp (metis "*" IntI Int_closed_segment closed_segment_commute singleton_iff) |
|
249 qed auto |
|
250 show "simple_path p" |
|
251 using \<open>arc p\<close> arc_simple_path by blast |
|
252 show sp_ae2: "simple_path (linepath (a + e) (a - e))" |
|
253 using \<open>arc p\<close> arc_distinct_ends pfp psp by fastforce |
|
254 show pa: "pathfinish (linepath (a + e) (a - e)) = a - e" |
|
255 "pathstart (linepath (a + e) c +++ linepath c (a - e)) = a + e" |
|
256 "pathfinish (linepath (a + e) c +++ linepath c (a - e)) = a - e" |
|
257 "pathstart p = a + e" "pathfinish p = a - e" |
|
258 "pathstart (linepath (a + e) (a - e)) = a + e" |
|
259 by (simp_all add: assms) |
|
260 show 1: "path_image (linepath (a + e) (a - e)) \<inter> path_image p = {a + e, a - e}" |
|
261 proof |
|
262 show "path_image (linepath (a + e) (a - e)) \<inter> path_image p \<subseteq> {a + e, a - e}" |
|
263 using pap closed_segment_commute psp segment_convex_hull by fastforce |
|
264 show "{a + e, a - e} \<subseteq> path_image (linepath (a + e) (a - e)) \<inter> path_image p" |
|
265 using pap pathfinish_in_path_image pathstart_in_path_image pfp psp by fastforce |
|
266 qed |
|
267 show 2: "path_image (linepath (a + e) (a - e)) \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) = |
|
268 {a + e, a - e}" (is "?lhs = ?rhs") |
|
269 proof |
|
270 have "\<not> collinear {c, a + e, a - e}" |
|
271 using * by (simp add: insert_commute) |
|
272 then have "convex hull {a + e, a - e} \<inter> convex hull {a + e, c} = {a + e}" |
|
273 "convex hull {a + e, a - e} \<inter> convex hull {c, a - e} = {a - e}" |
|
274 by (metis (full_types) Int_closed_segment insert_commute segment_convex_hull)+ |
|
275 then show "?lhs \<subseteq> ?rhs" |
|
276 by (metis Int_Un_distrib equalityD1 insert_is_Un path_image_join path_image_linepath path_join_eq path_linepath segment_convex_hull simple_path_def sp_aec) |
|
277 show "?rhs \<subseteq> ?lhs" |
|
278 using segment_convex_hull by (simp add: path_image_join) |
|
279 qed |
|
280 have "path_image p \<inter> path_image (linepath (a + e) c) \<subseteq> {a + e}" |
|
281 proof (clarsimp simp: path_image_join) |
|
282 fix x |
|
283 assume "x \<in> path_image p" and x_ac: "x \<in> closed_segment (a + e) c" |
|
284 then have "dist x a \<ge> e" |
|
285 by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less) |
|
286 with x_ac dac \<open>e > 0\<close> show "x = a + e" |
|
287 by (auto simp: norm_minus_commute dist_norm closed_segment_eq_open dest: open_segment_furthest_le [where y=a]) |
|
288 qed |
|
289 moreover |
|
290 have "path_image p \<inter> path_image (linepath c (a - e)) \<subseteq> {a - e}" |
|
291 proof (clarsimp simp: path_image_join) |
|
292 fix x |
|
293 assume "x \<in> path_image p" and x_ac: "x \<in> closed_segment c (a - e)" |
|
294 then have "dist x a \<ge> e" |
|
295 by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less) |
|
296 with x_ac dac \<open>e > 0\<close> show "x = a - e" |
|
297 by (auto simp: norm_minus_commute dist_norm closed_segment_eq_open dest: open_segment_furthest_le [where y=a]) |
|
298 qed |
|
299 ultimately |
|
300 have "path_image p \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) \<subseteq> {a + e, a - e}" |
|
301 by (force simp: path_image_join) |
|
302 then show 3: "path_image p \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) = {a + e, a - e}" |
|
303 apply (rule equalityI) |
|
304 apply (clarsimp simp: path_image_join) |
|
305 apply (metis pathstart_in_path_image psp pathfinish_in_path_image pfp) |
|
306 done |
|
307 show 4: "path_image (linepath (a + e) c +++ linepath c (a - e)) \<inter> |
|
308 inside (path_image (linepath (a + e) (a - e)) \<union> path_image p) \<noteq> {}" |
|
309 apply (clarsimp simp: path_image_join segment_convex_hull disjoint_iff_not_equal) |
|
310 by (metis (no_types, hide_lams) UnI1 Un_commute c closed_segment_commute ends_in_segment(1) path_image_join |
|
311 path_image_linepath pathstart_linepath pfp segment_convex_hull) |
|
312 show zin_inside: "z \<in> inside (path_image (linepath (a + e) (a - e)) \<union> |
|
313 path_image (linepath (a + e) c +++ linepath c (a - e)))" |
|
314 apply (simp add: path_image_join) |
|
315 by (metis z inside_of_triangle DIM_complex Un_commute closed_segment_commute) |
|
316 show 5: "winding_number |
|
317 (linepath (a + e) (a - e) +++ reversepath (linepath (a + e) c +++ linepath c (a - e))) z = |
|
318 winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z" |
|
319 by (simp add: reversepath_joinpaths path_image_join winding_number_join) |
|
320 show 6: "winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z \<noteq> 0" |
|
321 by (simp add: winding_number_triangle z) |
|
322 show "winding_number (linepath (a + e) (a - e) +++ reversepath p) z = |
|
323 winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z" |
|
324 by (metis 1 2 3 4 5 6 pa sp_aec sp_ae2 \<open>arc p\<close> \<open>simple_path p\<close> arc_distinct_ends winding_number_from_innerpath zin_inside) |
|
325 qed (use assms \<open>e > 0\<close> in auto) |
|
326 show "z \<in> inside (path_image (p +++ linepath (a - e) (a + e)))" |
|
327 using zin by (simp add: assms path_image_join Un_commute closed_segment_commute) |
|
328 then have "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) = |
|
329 cmod ((winding_number(reversepath (p +++ linepath (a - e) (a + e))) z))" |
|
330 apply (subst winding_number_reversepath) |
|
331 using simple_path_imp_path sp_pl apply blast |
|
332 apply (metis IntI emptyE inside_no_overlap) |
|
333 by (simp add: inside_def) |
|
334 also have "... = cmod (winding_number(linepath (a + e) (a - e) +++ reversepath p) z)" |
|
335 by (simp add: pfp reversepath_joinpaths) |
|
336 also have "... = cmod (winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z)" |
|
337 by (simp add: zeq) |
|
338 also have "... = 1" |
|
339 using z by (simp add: interior_of_triangle winding_number_triangle) |
|
340 finally show "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) = 1" . |
|
341 qed |
|
342 qed |
|
343 |
|
344 |
|
345 |
|
346 lemma simple_closed_path_wn2: |
|
347 fixes a::complex and d e::real |
|
348 assumes "0 < d" "0 < e" |
|
349 and sp_pl: "simple_path(p +++ linepath (a - d) (a + e))" |
|
350 and psp: "pathstart p = a + e" |
|
351 and pfp: "pathfinish p = a - d" |
|
352 obtains z where "z \<in> inside (path_image (p +++ linepath (a - d) (a + e)))" |
|
353 "cmod (winding_number (p +++ linepath (a - d) (a + e)) z) = 1" |
|
354 proof - |
|
355 have [simp]: "a + of_real x \<in> closed_segment (a - \<alpha>) (a - \<beta>) \<longleftrightarrow> x \<in> closed_segment (-\<alpha>) (-\<beta>)" for x \<alpha> \<beta>::real |
|
356 using closed_segment_translation_eq [of a] |
|
357 by (metis (no_types, hide_lams) add_uminus_conv_diff of_real_minus of_real_closed_segment) |
|
358 have [simp]: "a - of_real x \<in> closed_segment (a + \<alpha>) (a + \<beta>) \<longleftrightarrow> -x \<in> closed_segment \<alpha> \<beta>" for x \<alpha> \<beta>::real |
|
359 by (metis closed_segment_translation_eq diff_conv_add_uminus of_real_closed_segment of_real_minus) |
|
360 have "arc p" and arc_lp: "arc (linepath (a - d) (a + e))" and "path p" |
|
361 and pap: "path_image p \<inter> closed_segment (a - d) (a + e) \<subseteq> {a+e, a-d}" |
|
362 using simple_path_join_loop_eq [of "linepath (a - d) (a + e)" p] assms arc_imp_path by auto |
|
363 have "0 \<in> closed_segment (-d) e" |
|
364 using \<open>0 < d\<close> \<open>0 < e\<close> closed_segment_eq_real_ivl by auto |
|
365 then have "a \<in> path_image (linepath (a - d) (a + e))" |
|
366 using of_real_closed_segment [THEN iffD2] |
|
367 by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment) |
|
368 then have "a \<notin> path_image p" |
|
369 using \<open>0 < d\<close> \<open>0 < e\<close> pap by auto |
|
370 then obtain k where "0 < k" and k: "ball a k \<inter> (path_image p) = {}" |
|
371 using \<open>0 < e\<close> \<open>path p\<close> not_on_path_ball by blast |
|
372 define kde where "kde \<equiv> (min k (min d e)) / 2" |
|
373 have "0 < kde" "kde < k" "kde < d" "kde < e" |
|
374 using \<open>0 < k\<close> \<open>0 < d\<close> \<open>0 < e\<close> by (auto simp: kde_def) |
|
375 let ?q = "linepath (a + kde) (a + e) +++ p +++ linepath (a - d) (a - kde)" |
|
376 have "- kde \<in> closed_segment (-d) e" |
|
377 using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto |
|
378 then have a_diff_kde: "a - kde \<in> closed_segment (a - d) (a + e)" |
|
379 using of_real_closed_segment [THEN iffD2] |
|
380 by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment) |
|
381 then have clsub2: "closed_segment (a - d) (a - kde) \<subseteq> closed_segment (a - d) (a + e)" |
|
382 by (simp add: subset_closed_segment) |
|
383 then have "path_image p \<inter> closed_segment (a - d) (a - kde) \<subseteq> {a + e, a - d}" |
|
384 using pap by force |
|
385 moreover |
|
386 have "a + e \<notin> path_image p \<inter> closed_segment (a - d) (a - kde)" |
|
387 using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>0 < e\<close> by (auto simp: closed_segment_eq_real_ivl) |
|
388 ultimately have sub_a_diff_d: "path_image p \<inter> closed_segment (a - d) (a - kde) \<subseteq> {a - d}" |
|
389 by blast |
|
390 have "kde \<in> closed_segment (-d) e" |
|
391 using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto |
|
392 then have a_diff_kde: "a + kde \<in> closed_segment (a - d) (a + e)" |
|
393 using of_real_closed_segment [THEN iffD2] |
|
394 by (force dest: closed_segment_translation_eq [of "a", THEN iffD2] simp del: of_real_closed_segment) |
|
395 then have clsub1: "closed_segment (a + kde) (a + e) \<subseteq> closed_segment (a - d) (a + e)" |
|
396 by (simp add: subset_closed_segment) |
|
397 then have "closed_segment (a + kde) (a + e) \<inter> path_image p \<subseteq> {a + e, a - d}" |
|
398 using pap by force |
|
399 moreover |
|
400 have "closed_segment (a + kde) (a + e) \<inter> closed_segment (a - d) (a - kde) = {}" |
|
401 proof (clarsimp intro!: equals0I) |
|
402 fix y |
|
403 assume y1: "y \<in> closed_segment (a + kde) (a + e)" |
|
404 and y2: "y \<in> closed_segment (a - d) (a - kde)" |
|
405 obtain u where u: "y = a + of_real u" and "0 < u" |
|
406 using y1 \<open>0 < kde\<close> \<open>kde < e\<close> \<open>0 < e\<close> apply (clarsimp simp: in_segment) |
|
407 apply (rule_tac u = "(1 - u)*kde + u*e" in that) |
|
408 apply (auto simp: scaleR_conv_of_real algebra_simps) |
|
409 by (meson le_less_trans less_add_same_cancel2 less_eq_real_def mult_left_mono) |
|
410 moreover |
|
411 obtain v where v: "y = a + of_real v" and "v \<le> 0" |
|
412 using y2 \<open>0 < kde\<close> \<open>0 < d\<close> \<open>0 < e\<close> apply (clarsimp simp: in_segment) |
|
413 apply (rule_tac v = "- ((1 - u)*d + u*kde)" in that) |
|
414 apply (force simp: scaleR_conv_of_real algebra_simps) |
|
415 by (meson less_eq_real_def neg_le_0_iff_le segment_bound_lemma) |
|
416 ultimately show False |
|
417 by auto |
|
418 qed |
|
419 moreover have "a - d \<notin> closed_segment (a + kde) (a + e)" |
|
420 using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>0 < e\<close> by (auto simp: closed_segment_eq_real_ivl) |
|
421 ultimately have sub_a_plus_e: |
|
422 "closed_segment (a + kde) (a + e) \<inter> (path_image p \<union> closed_segment (a - d) (a - kde)) |
|
423 \<subseteq> {a + e}" |
|
424 by auto |
|
425 have "kde \<in> closed_segment (-kde) e" |
|
426 using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto |
|
427 then have a_add_kde: "a + kde \<in> closed_segment (a - kde) (a + e)" |
|
428 using of_real_closed_segment [THEN iffD2] |
|
429 by (force dest: closed_segment_translation_eq [of "a", THEN iffD2] simp del: of_real_closed_segment) |
|
430 have "closed_segment (a - kde) (a + kde) \<inter> closed_segment (a + kde) (a + e) = {a + kde}" |
|
431 by (metis a_add_kde Int_closed_segment) |
|
432 moreover |
|
433 have "path_image p \<inter> closed_segment (a - kde) (a + kde) = {}" |
|
434 proof (rule equals0I, clarify) |
|
435 fix y assume "y \<in> path_image p" "y \<in> closed_segment (a - kde) (a + kde)" |
|
436 with equals0D [OF k, of y] \<open>0 < kde\<close> \<open>kde < k\<close> show False |
|
437 by (auto simp: dist_norm dest: dist_decreases_closed_segment [where c=a]) |
|
438 qed |
|
439 moreover |
|
440 have "- kde \<in> closed_segment (-d) kde" |
|
441 using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto |
|
442 then have a_diff_kde': "a - kde \<in> closed_segment (a - d) (a + kde)" |
|
443 using of_real_closed_segment [THEN iffD2] |
|
444 by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment) |
|
445 then have "closed_segment (a - d) (a - kde) \<inter> closed_segment (a - kde) (a + kde) = {a - kde}" |
|
446 by (metis Int_closed_segment) |
|
447 ultimately |
|
448 have pa_subset_pm_kde: "path_image ?q \<inter> closed_segment (a - kde) (a + kde) \<subseteq> {a - kde, a + kde}" |
|
449 by (auto simp: path_image_join assms) |
|
450 have ge_kde1: "\<exists>y. x = a + y \<and> y \<ge> kde" if "x \<in> closed_segment (a + kde) (a + e)" for x |
|
451 using that \<open>kde < e\<close> mult_le_cancel_left |
|
452 apply (auto simp: in_segment) |
|
453 apply (rule_tac x="(1-u)*kde + u*e" in exI) |
|
454 apply (fastforce simp: algebra_simps scaleR_conv_of_real) |
|
455 done |
|
456 have ge_kde2: "\<exists>y. x = a + y \<and> y \<le> -kde" if "x \<in> closed_segment (a - d) (a - kde)" for x |
|
457 using that \<open>kde < d\<close> affine_ineq |
|
458 apply (auto simp: in_segment) |
|
459 apply (rule_tac x="- ((1-u)*d + u*kde)" in exI) |
|
460 apply (fastforce simp: algebra_simps scaleR_conv_of_real) |
|
461 done |
|
462 have notin_paq: "x \<notin> path_image ?q" if "dist a x < kde" for x |
|
463 using that using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < k\<close> |
|
464 apply (auto simp: path_image_join assms dist_norm dest!: ge_kde1 ge_kde2) |
|
465 by (meson k disjoint_iff_not_equal le_less_trans less_eq_real_def mem_ball that) |
|
466 obtain z where zin: "z \<in> inside (path_image (?q +++ linepath (a - kde) (a + kde)))" |
|
467 and z1: "cmod (winding_number (?q +++ linepath (a - kde) (a + kde)) z) = 1" |
|
468 proof (rule simple_closed_path_wn1 [of kde ?q a]) |
|
469 show "simple_path (?q +++ linepath (a - kde) (a + kde))" |
|
470 proof (intro simple_path_join_loop conjI) |
|
471 show "arc ?q" |
|
472 proof (rule arc_join) |
|
473 show "arc (linepath (a + kde) (a + e))" |
|
474 using \<open>kde < e\<close> \<open>arc p\<close> by (force simp: pfp) |
|
475 show "arc (p +++ linepath (a - d) (a - kde))" |
|
476 using \<open>kde < d\<close> \<open>kde < e\<close> \<open>arc p\<close> sub_a_diff_d by (force simp: pfp intro: arc_join) |
|
477 qed (auto simp: psp pfp path_image_join sub_a_plus_e) |
|
478 show "arc (linepath (a - kde) (a + kde))" |
|
479 using \<open>0 < kde\<close> by auto |
|
480 qed (use pa_subset_pm_kde in auto) |
|
481 qed (use \<open>0 < kde\<close> notin_paq in auto) |
|
482 have eq: "path_image (?q +++ linepath (a - kde) (a + kde)) = path_image (p +++ linepath (a - d) (a + e))" |
|
483 (is "?lhs = ?rhs") |
|
484 proof |
|
485 show "?lhs \<subseteq> ?rhs" |
|
486 using clsub1 clsub2 apply (auto simp: path_image_join assms) |
|
487 by (meson subsetCE subset_closed_segment) |
|
488 show "?rhs \<subseteq> ?lhs" |
|
489 apply (simp add: path_image_join assms Un_ac) |
|
490 by (metis Un_closed_segment Un_assoc a_diff_kde a_diff_kde' le_supI2 subset_refl) |
|
491 qed |
|
492 show thesis |
|
493 proof |
|
494 show zzin: "z \<in> inside (path_image (p +++ linepath (a - d) (a + e)))" |
|
495 by (metis eq zin) |
|
496 then have znotin: "z \<notin> path_image p" |
|
497 by (metis ComplD Un_iff inside_Un_outside path_image_join pathfinish_linepath pathstart_reversepath pfp reversepath_linepath) |
|
498 have znotin_de: "z \<notin> closed_segment (a - d) (a + kde)" |
|
499 by (metis ComplD Un_iff Un_closed_segment a_diff_kde inside_Un_outside path_image_join path_image_linepath pathstart_linepath pfp zzin) |
|
500 have "winding_number (linepath (a - d) (a + e)) z = |
|
501 winding_number (linepath (a - d) (a + kde)) z + winding_number (linepath (a + kde) (a + e)) z" |
|
502 apply (rule winding_number_split_linepath) |
|
503 apply (simp add: a_diff_kde) |
|
504 by (metis ComplD Un_iff inside_Un_outside path_image_join path_image_linepath pathstart_linepath pfp zzin) |
|
505 also have "... = winding_number (linepath (a + kde) (a + e)) z + |
|
506 (winding_number (linepath (a - d) (a - kde)) z + |
|
507 winding_number (linepath (a - kde) (a + kde)) z)" |
|
508 by (simp add: winding_number_split_linepath [of "a-kde", symmetric] znotin_de a_diff_kde') |
|
509 finally have "winding_number (p +++ linepath (a - d) (a + e)) z = |
|
510 winding_number p z + winding_number (linepath (a + kde) (a + e)) z + |
|
511 (winding_number (linepath (a - d) (a - kde)) z + |
|
512 winding_number (linepath (a - kde) (a + kde)) z)" |
|
513 by (metis (no_types, lifting) ComplD Un_iff \<open>arc p\<close> add.assoc arc_imp_path eq path_image_join path_join_path_ends path_linepath simple_path_imp_path sp_pl union_with_outside winding_number_join zin) |
|
514 also have "... = winding_number ?q z + winding_number (linepath (a - kde) (a + kde)) z" |
|
515 using \<open>path p\<close> znotin assms zzin clsub1 |
|
516 apply (subst winding_number_join, auto) |
|
517 apply (metis (no_types, hide_lams) ComplD Un_iff contra_subsetD inside_Un_outside path_image_join path_image_linepath pathstart_linepath) |
|
518 apply (metis Un_iff Un_closed_segment a_diff_kde' not_in_path_image_join path_image_linepath znotin_de) |
|
519 by (metis Un_iff Un_closed_segment a_diff_kde' path_image_linepath path_linepath pathstart_linepath winding_number_join znotin_de) |
|
520 also have "... = winding_number (?q +++ linepath (a - kde) (a + kde)) z" |
|
521 using \<open>path p\<close> assms zin |
|
522 apply (subst winding_number_join [symmetric], auto) |
|
523 apply (metis ComplD Un_iff path_image_join pathfinish_join pathfinish_linepath pathstart_linepath union_with_outside) |
|
524 by (metis Un_iff Un_closed_segment a_diff_kde' znotin_de) |
|
525 finally have "winding_number (p +++ linepath (a - d) (a + e)) z = |
|
526 winding_number (?q +++ linepath (a - kde) (a + kde)) z" . |
|
527 then show "cmod (winding_number (p +++ linepath (a - d) (a + e)) z) = 1" |
|
528 by (simp add: z1) |
|
529 qed |
|
530 qed |
|
531 |
|
532 |
|
533 proposition simple_closed_path_wn3: |
|
534 fixes p :: "real \<Rightarrow> complex" |
|
535 assumes "simple_path p" and loop: "pathfinish p = pathstart p" |
|
536 obtains z where "z \<in> inside (path_image p)" "cmod (winding_number p z) = 1" |
|
537 proof - |
|
538 have ins: "inside(path_image p) \<noteq> {}" "open(inside(path_image p))" |
|
539 "connected(inside(path_image p))" |
|
540 and out: "outside(path_image p) \<noteq> {}" "open(outside(path_image p))" |
|
541 "connected(outside(path_image p))" |
|
542 and bo: "bounded(inside(path_image p))" "\<not> bounded(outside(path_image p))" |
|
543 and ins_out: "inside(path_image p) \<inter> outside(path_image p) = {}" |
|
544 "inside(path_image p) \<union> outside(path_image p) = - path_image p" |
|
545 and fro: "frontier(inside(path_image p)) = path_image p" |
|
546 "frontier(outside(path_image p)) = path_image p" |
|
547 using Jordan_inside_outside [OF assms] by auto |
|
548 obtain a where a: "a \<in> inside(path_image p)" |
|
549 using \<open>inside (path_image p) \<noteq> {}\<close> by blast |
|
550 obtain d::real where "0 < d" and d_fro: "a - d \<in> frontier (inside (path_image p))" |
|
551 and d_int: "\<And>\<epsilon>. \<lbrakk>0 \<le> \<epsilon>; \<epsilon> < d\<rbrakk> \<Longrightarrow> (a - \<epsilon>) \<in> inside (path_image p)" |
|
552 apply (rule ray_to_frontier [of "inside (path_image p)" a "-1"]) |
|
553 using \<open>bounded (inside (path_image p))\<close> \<open>open (inside (path_image p))\<close> a interior_eq |
|
554 apply (auto simp: of_real_def) |
|
555 done |
|
556 obtain e::real where "0 < e" and e_fro: "a + e \<in> frontier (inside (path_image p))" |
|
557 and e_int: "\<And>\<epsilon>. \<lbrakk>0 \<le> \<epsilon>; \<epsilon> < e\<rbrakk> \<Longrightarrow> (a + \<epsilon>) \<in> inside (path_image p)" |
|
558 apply (rule ray_to_frontier [of "inside (path_image p)" a 1]) |
|
559 using \<open>bounded (inside (path_image p))\<close> \<open>open (inside (path_image p))\<close> a interior_eq |
|
560 apply (auto simp: of_real_def) |
|
561 done |
|
562 obtain t0 where "0 \<le> t0" "t0 \<le> 1" and pt: "p t0 = a - d" |
|
563 using a d_fro fro by (auto simp: path_image_def) |
|
564 obtain q where "simple_path q" and q_ends: "pathstart q = a - d" "pathfinish q = a - d" |
|
565 and q_eq_p: "path_image q = path_image p" |
|
566 and wn_q_eq_wn_p: "\<And>z. z \<in> inside(path_image p) \<Longrightarrow> winding_number q z = winding_number p z" |
|
567 proof |
|
568 show "simple_path (shiftpath t0 p)" |
|
569 by (simp add: pathstart_shiftpath pathfinish_shiftpath |
|
570 simple_path_shiftpath path_image_shiftpath \<open>0 \<le> t0\<close> \<open>t0 \<le> 1\<close> assms) |
|
571 show "pathstart (shiftpath t0 p) = a - d" |
|
572 using pt by (simp add: \<open>t0 \<le> 1\<close> pathstart_shiftpath) |
|
573 show "pathfinish (shiftpath t0 p) = a - d" |
|
574 by (simp add: \<open>0 \<le> t0\<close> loop pathfinish_shiftpath pt) |
|
575 show "path_image (shiftpath t0 p) = path_image p" |
|
576 by (simp add: \<open>0 \<le> t0\<close> \<open>t0 \<le> 1\<close> loop path_image_shiftpath) |
|
577 show "winding_number (shiftpath t0 p) z = winding_number p z" |
|
578 if "z \<in> inside (path_image p)" for z |
|
579 by (metis ComplD Un_iff \<open>0 \<le> t0\<close> \<open>t0 \<le> 1\<close> \<open>simple_path p\<close> atLeastAtMost_iff inside_Un_outside |
|
580 loop simple_path_imp_path that winding_number_shiftpath) |
|
581 qed |
|
582 have ad_not_ae: "a - d \<noteq> a + e" |
|
583 by (metis \<open>0 < d\<close> \<open>0 < e\<close> add.left_inverse add_left_cancel add_uminus_conv_diff |
|
584 le_add_same_cancel2 less_eq_real_def not_less of_real_add of_real_def of_real_eq_0_iff pt) |
|
585 have ad_ae_q: "{a - d, a + e} \<subseteq> path_image q" |
|
586 using \<open>path_image q = path_image p\<close> d_fro e_fro fro(1) by auto |
|
587 have ada: "open_segment (a - d) a \<subseteq> inside (path_image p)" |
|
588 proof (clarsimp simp: in_segment) |
|
589 fix u::real assume "0 < u" "u < 1" |
|
590 with d_int have "a - (1 - u) * d \<in> inside (path_image p)" |
|
591 by (metis \<open>0 < d\<close> add.commute diff_add_cancel left_diff_distrib' less_add_same_cancel2 less_eq_real_def mult.left_neutral zero_less_mult_iff) |
|
592 then show "(1 - u) *\<^sub>R (a - d) + u *\<^sub>R a \<in> inside (path_image p)" |
|
593 by (simp add: diff_add_eq of_real_def real_vector.scale_right_diff_distrib) |
|
594 qed |
|
595 have aae: "open_segment a (a + e) \<subseteq> inside (path_image p)" |
|
596 proof (clarsimp simp: in_segment) |
|
597 fix u::real assume "0 < u" "u < 1" |
|
598 with e_int have "a + u * e \<in> inside (path_image p)" |
|
599 by (meson \<open>0 < e\<close> less_eq_real_def mult_less_cancel_right2 not_less zero_less_mult_iff) |
|
600 then show "(1 - u) *\<^sub>R a + u *\<^sub>R (a + e) \<in> inside (path_image p)" |
|
601 apply (simp add: algebra_simps) |
|
602 by (simp add: diff_add_eq of_real_def real_vector.scale_right_diff_distrib) |
|
603 qed |
|
604 have "complex_of_real (d * d + (e * e + d * (e + e))) \<noteq> 0" |
|
605 using ad_not_ae |
|
606 by (metis \<open>0 < d\<close> \<open>0 < e\<close> add_strict_left_mono less_add_same_cancel1 not_sum_squares_lt_zero |
|
607 of_real_eq_0_iff zero_less_double_add_iff_zero_less_single_add zero_less_mult_iff) |
|
608 then have a_in_de: "a \<in> open_segment (a - d) (a + e)" |
|
609 using ad_not_ae \<open>0 < d\<close> \<open>0 < e\<close> |
|
610 apply (auto simp: in_segment algebra_simps scaleR_conv_of_real) |
|
611 apply (rule_tac x="d / (d+e)" in exI) |
|
612 apply (auto simp: field_simps) |
|
613 done |
|
614 then have "open_segment (a - d) (a + e) \<subseteq> inside (path_image p)" |
|
615 using ada a aae Un_open_segment [of a "a-d" "a+e"] by blast |
|
616 then have "path_image q \<inter> open_segment (a - d) (a + e) = {}" |
|
617 using inside_no_overlap by (fastforce simp: q_eq_p) |
|
618 with ad_ae_q have paq_Int_cs: "path_image q \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}" |
|
619 by (simp add: closed_segment_eq_open) |
|
620 obtain t where "0 \<le> t" "t \<le> 1" and qt: "q t = a + e" |
|
621 using a e_fro fro ad_ae_q by (auto simp: path_defs) |
|
622 then have "t \<noteq> 0" |
|
623 by (metis ad_not_ae pathstart_def q_ends(1)) |
|
624 then have "t \<noteq> 1" |
|
625 by (metis ad_not_ae pathfinish_def q_ends(2) qt) |
|
626 have q01: "q 0 = a - d" "q 1 = a - d" |
|
627 using q_ends by (auto simp: pathstart_def pathfinish_def) |
|
628 obtain z where zin: "z \<in> inside (path_image (subpath t 0 q +++ linepath (a - d) (a + e)))" |
|
629 and z1: "cmod (winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z) = 1" |
|
630 proof (rule simple_closed_path_wn2 [of d e "subpath t 0 q" a], simp_all add: q01) |
|
631 show "simple_path (subpath t 0 q +++ linepath (a - d) (a + e))" |
|
632 proof (rule simple_path_join_loop, simp_all add: qt q01) |
|
633 have "inj_on q (closed_segment t 0)" |
|
634 using \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> \<open>t \<noteq> 0\<close> \<open>t \<noteq> 1\<close> |
|
635 by (fastforce simp: simple_path_def inj_on_def closed_segment_eq_real_ivl) |
|
636 then show "arc (subpath t 0 q)" |
|
637 using \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> \<open>t \<noteq> 0\<close> |
|
638 by (simp add: arc_subpath_eq simple_path_imp_path) |
|
639 show "arc (linepath (a - d) (a + e))" |
|
640 by (simp add: ad_not_ae) |
|
641 show "path_image (subpath t 0 q) \<inter> closed_segment (a - d) (a + e) \<subseteq> {a + e, a - d}" |
|
642 using qt paq_Int_cs \<open>simple_path q\<close> \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> |
|
643 by (force simp: dest: rev_subsetD [OF _ path_image_subpath_subset] intro: simple_path_imp_path) |
|
644 qed |
|
645 qed (auto simp: \<open>0 < d\<close> \<open>0 < e\<close> qt) |
|
646 have pa01_Un: "path_image (subpath 0 t q) \<union> path_image (subpath 1 t q) = path_image q" |
|
647 unfolding path_image_subpath |
|
648 using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> by (force simp: path_image_def image_iff) |
|
649 with paq_Int_cs have pa_01q: |
|
650 "(path_image (subpath 0 t q) \<union> path_image (subpath 1 t q)) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}" |
|
651 by metis |
|
652 have z_notin_ed: "z \<notin> closed_segment (a + e) (a - d)" |
|
653 using zin q01 by (simp add: path_image_join closed_segment_commute inside_def) |
|
654 have z_notin_0t: "z \<notin> path_image (subpath 0 t q)" |
|
655 by (metis (no_types, hide_lams) IntI Un_upper1 subsetD empty_iff inside_no_overlap path_image_join |
|
656 path_image_subpath_commute pathfinish_subpath pathstart_def pathstart_linepath q_ends(1) qt subpath_trivial zin) |
|
657 have [simp]: "- winding_number (subpath t 0 q) z = winding_number (subpath 0 t q) z" |
|
658 by (metis \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> atLeastAtMost_iff zero_le_one |
|
659 path_image_subpath_commute path_subpath real_eq_0_iff_le_ge_0 |
|
660 reversepath_subpath simple_path_imp_path winding_number_reversepath z_notin_0t) |
|
661 obtain z_in_q: "z \<in> inside(path_image q)" |
|
662 and wn_q: "winding_number (subpath 0 t q +++ subpath t 1 q) z = - winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z" |
|
663 proof (rule winding_number_from_innerpath |
|
664 [of "subpath 0 t q" "a-d" "a+e" "subpath 1 t q" "linepath (a - d) (a + e)" |
|
665 z "- winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"], |
|
666 simp_all add: q01 qt pa01_Un reversepath_subpath) |
|
667 show "simple_path (subpath 0 t q)" "simple_path (subpath 1 t q)" |
|
668 by (simp_all add: \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> \<open>t \<noteq> 0\<close> \<open>t \<noteq> 1\<close> simple_path_subpath) |
|
669 show "simple_path (linepath (a - d) (a + e))" |
|
670 using ad_not_ae by blast |
|
671 show "path_image (subpath 0 t q) \<inter> path_image (subpath 1 t q) = {a - d, a + e}" (is "?lhs = ?rhs") |
|
672 proof |
|
673 show "?lhs \<subseteq> ?rhs" |
|
674 using \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> \<open>t \<noteq> 1\<close> q_ends qt q01 |
|
675 by (force simp: pathfinish_def qt simple_path_def path_image_subpath) |
|
676 show "?rhs \<subseteq> ?lhs" |
|
677 using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath) |
|
678 qed |
|
679 show "path_image (subpath 0 t q) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs") |
|
680 proof |
|
681 show "?lhs \<subseteq> ?rhs" using paq_Int_cs pa01_Un by fastforce |
|
682 show "?rhs \<subseteq> ?lhs" using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath) |
|
683 qed |
|
684 show "path_image (subpath 1 t q) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs") |
|
685 proof |
|
686 show "?lhs \<subseteq> ?rhs" by (auto simp: pa_01q [symmetric]) |
|
687 show "?rhs \<subseteq> ?lhs" using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath) |
|
688 qed |
|
689 show "closed_segment (a - d) (a + e) \<inter> inside (path_image q) \<noteq> {}" |
|
690 using a a_in_de open_closed_segment pa01_Un q_eq_p by fastforce |
|
691 show "z \<in> inside (path_image (subpath 0 t q) \<union> closed_segment (a - d) (a + e))" |
|
692 by (metis path_image_join path_image_linepath path_image_subpath_commute pathfinish_subpath pathstart_linepath q01(1) zin) |
|
693 show "winding_number (subpath 0 t q +++ linepath (a + e) (a - d)) z = |
|
694 - winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z" |
|
695 using z_notin_ed z_notin_0t \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> |
|
696 by (simp add: simple_path_imp_path qt q01 path_image_subpath_commute closed_segment_commute winding_number_join winding_number_reversepath [symmetric]) |
|
697 show "- complex_of_real d \<noteq> complex_of_real e" |
|
698 using ad_not_ae by auto |
|
699 show "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z \<noteq> 0" |
|
700 using z1 by auto |
|
701 qed |
|
702 show ?thesis |
|
703 proof |
|
704 show "z \<in> inside (path_image p)" |
|
705 using q_eq_p z_in_q by auto |
|
706 then have [simp]: "z \<notin> path_image q" |
|
707 by (metis disjoint_iff_not_equal inside_no_overlap q_eq_p) |
|
708 have [simp]: "z \<notin> path_image (subpath 1 t q)" |
|
709 using inside_def pa01_Un z_in_q by fastforce |
|
710 have "winding_number(subpath 0 t q +++ subpath t 1 q) z = winding_number(subpath 0 1 q) z" |
|
711 using z_notin_0t \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> |
|
712 by (simp add: simple_path_imp_path qt path_image_subpath_commute winding_number_join winding_number_subpath_combine) |
|
713 with wn_q have "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z = - winding_number q z" |
|
714 by auto |
|
715 with z1 have "cmod (winding_number q z) = 1" |
|
716 by simp |
|
717 with z1 wn_q_eq_wn_p show "cmod (winding_number p z) = 1" |
|
718 using z1 wn_q_eq_wn_p by (simp add: \<open>z \<in> inside (path_image p)\<close>) |
|
719 qed |
|
720 qed |
|
721 |
|
722 |
|
723 theorem simple_closed_path_winding_number_inside: |
|
724 assumes "simple_path \<gamma>" |
|
725 obtains "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = 1" |
|
726 | "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = -1" |
|
727 proof (cases "pathfinish \<gamma> = pathstart \<gamma>") |
|
728 case True |
|
729 have "path \<gamma>" |
|
730 by (simp add: assms simple_path_imp_path) |
|
731 then obtain k where k: "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = k" |
|
732 proof (rule winding_number_constant) |
|
733 show "connected (inside(path_image \<gamma>))" |
|
734 by (simp add: Jordan_inside_outside True assms) |
|
735 qed (use inside_no_overlap True in auto) |
|
736 obtain z where zin: "z \<in> inside (path_image \<gamma>)" and z1: "cmod (winding_number \<gamma> z) = 1" |
|
737 using simple_closed_path_wn3 [of \<gamma>] True assms by blast |
|
738 with k have "winding_number \<gamma> z = k" |
|
739 by blast |
|
740 have "winding_number \<gamma> z \<in> \<int>" |
|
741 using zin integer_winding_number [OF \<open>path \<gamma>\<close> True] inside_def by blast |
|
742 with z1 consider "winding_number \<gamma> z = 1" | "winding_number \<gamma> z = -1" |
|
743 apply (auto simp: Ints_def abs_if split: if_split_asm) |
|
744 by (metis of_int_1 of_int_eq_iff of_int_minus) |
|
745 then show ?thesis |
|
746 using that \<open>winding_number \<gamma> z = k\<close> k by auto |
|
747 next |
|
748 case False |
|
749 then show ?thesis |
|
750 using inside_simple_curve_imp_closed assms that(2) by blast |
|
751 qed |
|
752 |
|
753 corollary simple_closed_path_abs_winding_number_inside: |
|
754 assumes "simple_path \<gamma>" "z \<in> inside(path_image \<gamma>)" |
|
755 shows "\<bar>Re (winding_number \<gamma> z)\<bar> = 1" |
|
756 by (metis assms norm_minus_cancel norm_one one_complex.simps(1) real_norm_def simple_closed_path_winding_number_inside uminus_complex.simps(1)) |
|
757 |
|
758 corollary simple_closed_path_norm_winding_number_inside: |
|
759 assumes "simple_path \<gamma>" "z \<in> inside(path_image \<gamma>)" |
|
760 shows "norm (winding_number \<gamma> z) = 1" |
|
761 proof - |
|
762 have "pathfinish \<gamma> = pathstart \<gamma>" |
|
763 using assms inside_simple_curve_imp_closed by blast |
|
764 with assms integer_winding_number have "winding_number \<gamma> z \<in> \<int>" |
|
765 by (simp add: inside_def simple_path_def) |
|
766 then show ?thesis |
|
767 by (metis assms norm_minus_cancel norm_one simple_closed_path_winding_number_inside) |
|
768 qed |
|
769 |
|
770 corollary simple_closed_path_winding_number_cases: |
|
771 "\<lbrakk>simple_path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> path_image \<gamma>\<rbrakk> \<Longrightarrow> winding_number \<gamma> z \<in> {-1,0,1}" |
|
772 apply (simp add: inside_Un_outside [of "path_image \<gamma>", symmetric, unfolded set_eq_iff Set.Compl_iff] del: inside_Un_outside) |
|
773 apply (rule simple_closed_path_winding_number_inside) |
|
774 using simple_path_def winding_number_zero_in_outside by blast+ |
|
775 |
|
776 corollary simple_closed_path_winding_number_pos: |
|
777 "\<lbrakk>simple_path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> path_image \<gamma>; 0 < Re(winding_number \<gamma> z)\<rbrakk> |
|
778 \<Longrightarrow> winding_number \<gamma> z = 1" |
|
779 using simple_closed_path_winding_number_cases |
|
780 by fastforce |
|
781 |
|
782 end |
|
783 |