src/HOL/Analysis/Winding_Numbers.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 69918 eddcc7c726f3
child 69986 f2d327275065
permissions -rw-r--r--
more strict AFP properties;
lp15@65039
     1
section \<open>Winding Numbers\<close>
lp15@65039
     2
lp15@65039
     3
text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2017)\<close>
lp15@65039
     4
lp15@65039
     5
theory Winding_Numbers
lp15@66826
     6
imports Polytope Jordan_Curve Riemann_Mapping
lp15@65039
     7
begin
lp15@65039
     8
lp15@66826
     9
lemma simply_connected_inside_simple_path:
lp15@66826
    10
  fixes p :: "real \<Rightarrow> complex"
lp15@66826
    11
  shows "simple_path p \<Longrightarrow> simply_connected(inside(path_image p))"
lp15@66826
    12
  using Jordan_inside_outside connected_simple_path_image inside_simple_curve_imp_closed simply_connected_eq_frontier_properties
lp15@66826
    13
  by fastforce
lp15@66826
    14
lp15@66826
    15
lemma simply_connected_Int:
lp15@66826
    16
  fixes S :: "complex set"
lp15@66826
    17
  assumes "open S" "open T" "simply_connected S" "simply_connected T" "connected (S \<inter> T)"
lp15@66826
    18
  shows "simply_connected (S \<inter> T)"
lp15@66826
    19
  using assms by (force simp: simply_connected_eq_winding_number_zero open_Int)
lp15@66826
    20
lp15@65039
    21
subsection\<open>Winding number for a triangle\<close>
lp15@65039
    22
lp15@65039
    23
lemma wn_triangle1:
lp15@65039
    24
  assumes "0 \<in> interior(convex hull {a,b,c})"
nipkow@69508
    25
    shows "\<not> (Im(a/b) \<le> 0 \<and> 0 \<le> Im(b/c))"
lp15@65039
    26
proof -
lp15@65039
    27
  { assume 0: "Im(a/b) \<le> 0" "0 \<le> Im(b/c)"
lp15@65039
    28
    have "0 \<notin> interior (convex hull {a,b,c})"
lp15@65039
    29
    proof (cases "a=0 \<or> b=0 \<or> c=0")
lp15@65039
    30
      case True then show ?thesis
lp15@65039
    31
        by (auto simp: not_in_interior_convex_hull_3)
lp15@65039
    32
    next
lp15@65039
    33
      case False
lp15@65039
    34
      then have "b \<noteq> 0" by blast
lp15@65039
    35
      { fix x y::complex and u::real
lp15@65039
    36
        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"
lp15@65039
    37
        then have "((1 - u) * Im x) * Re b \<le> Im b * ((1 - u) * Re x)"
lp15@65039
    38
          by (simp add: mult_left_mono mult.assoc mult.left_commute [of "Im b"])
lp15@65039
    39
        then have "((1 - u) * Im x + u * Im y) * Re b \<le> Im b * ((1 - u) * Re x + u * Re y)"
lp15@65039
    40
          using eq_f' ordered_comm_semiring_class.comm_mult_left_mono
lp15@65039
    41
          by (fastforce simp add: algebra_simps)
lp15@65039
    42
      }
lp15@65039
    43
      with False 0 have "convex hull {a,b,c} \<le> {z. Im z * Re b \<le> Im b * Re z}"
lp15@65039
    44
        apply (simp add: Complex.Im_divide divide_simps complex_neq_0 [symmetric])
lp15@65039
    45
        apply (simp add: algebra_simps)
lp15@65039
    46
        apply (rule hull_minimal)
lp15@65039
    47
        apply (auto simp: algebra_simps convex_alt)
lp15@65039
    48
        done
lp15@65039
    49
      moreover have "0 \<notin> interior({z. Im z * Re b \<le> Im b * Re z})"
lp15@65039
    50
      proof
lp15@65039
    51
        assume "0 \<in> interior {z. Im z * Re b \<le> Im b * Re z}"
lp15@65039
    52
        then obtain e where "e>0" and e: "ball 0 e \<subseteq> {z. Im z * Re b \<le> Im b * Re z}"
lp15@65039
    53
          by (meson mem_interior)
lp15@65064
    54
        define z where "z \<equiv> - sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * \<i>"
lp15@65039
    55
        have "z \<in> ball 0 e"
wenzelm@66304
    56
          using \<open>e>0\<close>
lp15@65039
    57
          apply (simp add: z_def dist_norm)
lp15@65039
    58
          apply (rule le_less_trans [OF norm_triangle_ineq4])
lp15@65039
    59
          apply (simp add: norm_mult abs_sgn_eq)
lp15@65039
    60
          done
lp15@65039
    61
        then have "z \<in> {z. Im z * Re b \<le> Im b * Re z}"
lp15@65039
    62
          using e by blast
lp15@65039
    63
        then show False
wenzelm@66304
    64
          using \<open>e>0\<close> \<open>b \<noteq> 0\<close>
lp15@65039
    65
          apply (simp add: z_def dist_norm sgn_if less_eq_real_def mult_less_0_iff complex.expand split: if_split_asm)
lp15@65039
    66
          apply (auto simp: algebra_simps)
lp15@65039
    67
          apply (meson less_asym less_trans mult_pos_pos neg_less_0_iff_less)
lp15@65039
    68
          by (metis less_asym mult_pos_pos neg_less_0_iff_less)
lp15@65039
    69
      qed
lp15@65039
    70
      ultimately show ?thesis
lp15@65039
    71
        using interior_mono by blast
lp15@65039
    72
    qed
lp15@65039
    73
  } with assms show ?thesis by blast
lp15@65039
    74
qed
lp15@65039
    75
lp15@65039
    76
lemma wn_triangle2_0:
lp15@65039
    77
  assumes "0 \<in> interior(convex hull {a,b,c})"
lp15@65039
    78
  shows
lp15@65039
    79
       "0 < Im((b - a) * cnj (b)) \<and>
lp15@65039
    80
        0 < Im((c - b) * cnj (c)) \<and>
lp15@65039
    81
        0 < Im((a - c) * cnj (a))
lp15@65039
    82
        \<or>
lp15@65039
    83
        Im((b - a) * cnj (b)) < 0 \<and>
lp15@65039
    84
        0 < Im((b - c) * cnj (b)) \<and>
lp15@65039
    85
        0 < Im((a - b) * cnj (a)) \<and>
lp15@65039
    86
        0 < Im((c - a) * cnj (c))"
lp15@65039
    87
proof -
lp15@65039
    88
  have [simp]: "{b,c,a} = {a,b,c}" "{c,a,b} = {a,b,c}" by auto
lp15@65039
    89
  show ?thesis
lp15@65039
    90
    using wn_triangle1 [OF assms] wn_triangle1 [of b c a] wn_triangle1 [of c a b] assms
lp15@65039
    91
    by (auto simp: algebra_simps Im_complex_div_gt_0 Im_complex_div_lt_0 not_le not_less)
lp15@65039
    92
qed
lp15@65039
    93
lp15@65039
    94
lemma wn_triangle2:
lp15@65039
    95
  assumes "z \<in> interior(convex hull {a,b,c})"
lp15@65039
    96
   shows "0 < Im((b - a) * cnj (b - z)) \<and>
lp15@65039
    97
          0 < Im((c - b) * cnj (c - z)) \<and>
lp15@65039
    98
          0 < Im((a - c) * cnj (a - z))
lp15@65039
    99
          \<or>
lp15@65039
   100
          Im((b - a) * cnj (b - z)) < 0 \<and>
lp15@65039
   101
          0 < Im((b - c) * cnj (b - z)) \<and>
lp15@65039
   102
          0 < Im((a - b) * cnj (a - z)) \<and>
lp15@65039
   103
          0 < Im((c - a) * cnj (c - z))"
lp15@65039
   104
proof -
lp15@65039
   105
  have 0: "0 \<in> interior(convex hull {a-z, b-z, c-z})"
lp15@65039
   106
    using assms convex_hull_translation [of "-z" "{a,b,c}"]
lp15@65039
   107
                interior_translation [of "-z"]
haftmann@69661
   108
    by (simp cong: image_cong_simp)
lp15@65039
   109
  show ?thesis using wn_triangle2_0 [OF 0]
lp15@65039
   110
    by simp
lp15@65039
   111
qed
lp15@65039
   112
lp15@65039
   113
lemma wn_triangle3:
lp15@65039
   114
  assumes z: "z \<in> interior(convex hull {a,b,c})"
lp15@65039
   115
      and "0 < Im((b-a) * cnj (b-z))"
lp15@65039
   116
          "0 < Im((c-b) * cnj (c-z))"
lp15@65039
   117
          "0 < Im((a-c) * cnj (a-z))"
lp15@65039
   118
    shows "winding_number (linepath a b +++ linepath b c +++ linepath c a) z = 1"
lp15@65039
   119
proof -
lp15@65039
   120
  have znot[simp]: "z \<notin> closed_segment a b" "z \<notin> closed_segment b c" "z \<notin> closed_segment c a"
lp15@65039
   121
    using z interior_of_triangle [of a b c]
lp15@65039
   122
    by (auto simp: closed_segment_def)
lp15@65039
   123
  have gt0: "0 < Re (winding_number (linepath a b +++ linepath b c +++ linepath c a) z)"
lp15@65039
   124
    using assms
lp15@65039
   125
    by (simp add: winding_number_linepath_pos_lt path_image_join winding_number_join_pos_combined)
lp15@65039
   126
  have lt2: "Re (winding_number (linepath a b +++ linepath b c +++ linepath c a) z) < 2"
lp15@65039
   127
    using winding_number_lt_half_linepath [of _ a b]
lp15@65039
   128
    using winding_number_lt_half_linepath [of _ b c]
lp15@65039
   129
    using winding_number_lt_half_linepath [of _ c a] znot
lp15@65039
   130
    apply (fastforce simp add: winding_number_join path_image_join)
lp15@65039
   131
    done
lp15@65039
   132
  show ?thesis
lp15@65039
   133
    by (rule winding_number_eq_1) (simp_all add: path_image_join gt0 lt2)
lp15@65039
   134
qed
lp15@65039
   135
lp15@65039
   136
proposition winding_number_triangle:
lp15@65039
   137
  assumes z: "z \<in> interior(convex hull {a,b,c})"
lp15@65039
   138
    shows "winding_number(linepath a b +++ linepath b c +++ linepath c a) z =
lp15@65039
   139
           (if 0 < Im((b - a) * cnj (b - z)) then 1 else -1)"
lp15@65039
   140
proof -
lp15@65039
   141
  have [simp]: "{a,c,b} = {a,b,c}"  by auto
lp15@65039
   142
  have znot[simp]: "z \<notin> closed_segment a b" "z \<notin> closed_segment b c" "z \<notin> closed_segment c a"
lp15@65039
   143
    using z interior_of_triangle [of a b c]
lp15@65039
   144
    by (auto simp: closed_segment_def)
lp15@65039
   145
  then have [simp]: "z \<notin> closed_segment b a" "z \<notin> closed_segment c b" "z \<notin> closed_segment a c"
lp15@65039
   146
    using closed_segment_commute by blast+
lp15@65039
   147
  have *: "winding_number (linepath a b +++ linepath b c +++ linepath c a) z =
lp15@65039
   148
            winding_number (reversepath (linepath a c +++ linepath c b +++ linepath b a)) z"
lp15@65039
   149
    by (simp add: reversepath_joinpaths winding_number_join not_in_path_image_join)
lp15@65039
   150
  show ?thesis
lp15@65039
   151
    using wn_triangle2 [OF z] apply (rule disjE)
lp15@65039
   152
    apply (simp add: wn_triangle3 z)
lp15@65039
   153
    apply (simp add: path_image_join winding_number_reversepath * wn_triangle3 z)
lp15@65039
   154
    done
lp15@65039
   155
qed
lp15@65039
   156
lp15@65039
   157
subsection\<open>Winding numbers for simple closed paths\<close>
lp15@65039
   158
lp15@65039
   159
lemma winding_number_from_innerpath:
lp15@65039
   160
  assumes "simple_path c1" and c1: "pathstart c1 = a" "pathfinish c1 = b"
lp15@65039
   161
      and "simple_path c2" and c2: "pathstart c2 = a" "pathfinish c2 = b"
lp15@65039
   162
      and "simple_path c" and c: "pathstart c = a" "pathfinish c = b"
lp15@65039
   163
      and c1c2: "path_image c1 \<inter> path_image c2 = {a,b}"
lp15@65039
   164
      and c1c:  "path_image c1 \<inter> path_image c = {a,b}"
lp15@65039
   165
      and c2c:  "path_image c2 \<inter> path_image c = {a,b}"
lp15@65039
   166
      and ne_12: "path_image c \<inter> inside(path_image c1 \<union> path_image c2) \<noteq> {}"
lp15@65039
   167
      and z: "z \<in> inside(path_image c1 \<union> path_image c)"
lp15@65039
   168
      and wn_d: "winding_number (c1 +++ reversepath c) z = d"
lp15@65039
   169
      and "a \<noteq> b" "d \<noteq> 0"
lp15@65039
   170
  obtains "z \<in> inside(path_image c1 \<union> path_image c2)" "winding_number (c1 +++ reversepath c2) z = d"
lp15@65039
   171
proof -
lp15@65039
   172
  obtain 0: "inside(path_image c1 \<union> path_image c) \<inter> inside(path_image c2 \<union> path_image c) = {}"
lp15@65039
   173
     and 1: "inside(path_image c1 \<union> path_image c) \<union> inside(path_image c2 \<union> path_image c) \<union>
lp15@65039
   174
             (path_image c - {a,b}) = inside(path_image c1 \<union> path_image c2)"
lp15@65039
   175
    by (rule split_inside_simple_closed_curve
lp15@65039
   176
              [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])
lp15@65039
   177
  have znot: "z \<notin> path_image c"  "z \<notin> path_image c1" "z \<notin> path_image c2"
lp15@65039
   178
    using union_with_outside z 1 by auto
lp15@65039
   179
  have wn_cc2: "winding_number (c +++ reversepath c2) z = 0"
lp15@65039
   180
    apply (rule winding_number_zero_in_outside)
lp15@65039
   181
    apply (simp_all add: \<open>simple_path c2\<close> c c2 \<open>simple_path c\<close> simple_path_imp_path path_image_join)
lp15@65039
   182
    by (metis "0" ComplI UnE disjoint_iff_not_equal sup.commute union_with_inside z znot)
lp15@65039
   183
  show ?thesis
lp15@65039
   184
  proof
lp15@65039
   185
    show "z \<in> inside (path_image c1 \<union> path_image c2)"
lp15@65039
   186
      using "1" z by blast
lp15@65039
   187
    have "winding_number c1 z - winding_number c z = d "
lp15@65039
   188
      using assms znot
lp15@65039
   189
      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)
lp15@65039
   190
    then show "winding_number (c1 +++ reversepath c2) z = d"
lp15@65039
   191
      using wn_cc2 by (simp add: winding_number_join simple_path_imp_path assms znot winding_number_reversepath)
lp15@65039
   192
  qed
lp15@65039
   193
qed
lp15@65039
   194
lp15@65039
   195
lemma simple_closed_path_wn1:
lp15@65039
   196
  fixes a::complex and e::real
lp15@65039
   197
  assumes "0 < e"
lp15@65039
   198
    and sp_pl: "simple_path(p +++ linepath (a - e) (a + e))"
lp15@65039
   199
    and psp:   "pathstart p = a + e"
lp15@65039
   200
    and pfp:   "pathfinish p = a - e"
lp15@65039
   201
    and disj:  "ball a e \<inter> path_image p = {}"
lp15@65039
   202
obtains z where "z \<in> inside (path_image (p +++ linepath (a - e) (a + e)))"
lp15@65039
   203
                "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) = 1"
lp15@65039
   204
proof -
lp15@65039
   205
  have "arc p" and arc_lp: "arc (linepath (a - e) (a + e))"
lp15@65039
   206
    and pap: "path_image p \<inter> path_image (linepath (a - e) (a + e)) \<subseteq> {pathstart p, a-e}"
lp15@65039
   207
    using simple_path_join_loop_eq [of "linepath (a - e) (a + e)" p] assms by auto
lp15@65039
   208
  have mid_eq_a: "midpoint (a - e) (a + e) = a"
lp15@65039
   209
    by (simp add: midpoint_def)
lp15@65039
   210
  then have "a \<in> path_image(p +++ linepath (a - e) (a + e))"
lp15@65039
   211
    apply (simp add: assms path_image_join)
lp15@65039
   212
    by (metis midpoint_in_closed_segment)
lp15@65039
   213
  have "a \<in> frontier(inside (path_image(p +++ linepath (a - e) (a + e))))"
lp15@65039
   214
    apply (simp add: assms Jordan_inside_outside)
lp15@65039
   215
    apply (simp_all add: assms path_image_join)
lp15@65039
   216
    by (metis mid_eq_a midpoint_in_closed_segment)
lp15@65039
   217
  with \<open>0 < e\<close> obtain c where c: "c \<in> inside (path_image(p +++ linepath (a - e) (a + e)))"
lp15@65039
   218
                  and dac: "dist a c < e"
lp15@65039
   219
    by (auto simp: frontier_straddle)
lp15@65039
   220
  then have "c \<notin> path_image(p +++ linepath (a - e) (a + e))"
lp15@65039
   221
    using inside_no_overlap by blast
lp15@65039
   222
  then have "c \<notin> path_image p"
lp15@65039
   223
            "c \<notin> closed_segment (a - of_real e) (a + of_real e)"
lp15@65039
   224
    by (simp_all add: assms path_image_join)
lp15@65039
   225
  with \<open>0 < e\<close> dac have "c \<notin> affine hull {a - of_real e, a + of_real e}"
lp15@65039
   226
    by (simp add: segment_as_ball not_le)
nipkow@69508
   227
  with \<open>0 < e\<close> have *: "\<not> collinear {a - e, c,a + e}"
lp15@65039
   228
    using collinear_3_affine_hull [of "a-e" "a+e"] by (auto simp: insert_commute)
lp15@65039
   229
  have 13: "1/3 + 1/3 + 1/3 = (1::real)" by simp
lp15@65039
   230
  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})"
lp15@65039
   231
    using interior_convex_hull_3_minimal [OF * DIM_complex]
lp15@65039
   232
    by clarsimp (metis 13 zero_less_divide_1_iff zero_less_numeral)
lp15@65039
   233
  then obtain z where z: "z \<in> interior(convex hull {a - e, c, a + e})" by force
lp15@65039
   234
  have [simp]: "z \<notin> closed_segment (a - e) c"
lp15@65039
   235
    by (metis DIM_complex Diff_iff IntD2 inf_sup_absorb interior_of_triangle z)
lp15@65039
   236
  have [simp]: "z \<notin> closed_segment (a + e) (a - e)"
lp15@65039
   237
    by (metis DIM_complex DiffD2 Un_iff interior_of_triangle z)
lp15@65039
   238
  have [simp]: "z \<notin> closed_segment c (a + e)"
lp15@65039
   239
    by (metis (no_types, lifting) DIM_complex DiffD2 Un_insert_right inf_sup_aci(5) insertCI interior_of_triangle mk_disjoint_insert z)
lp15@65039
   240
  show thesis
lp15@65039
   241
  proof
lp15@65039
   242
    have "norm (winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z) = 1"
lp15@65039
   243
      using winding_number_triangle [OF z] by simp
lp15@65039
   244
    have zin: "z \<in> inside (path_image (linepath (a + e) (a - e)) \<union> path_image p)"
lp15@65039
   245
      and zeq: "winding_number (linepath (a + e) (a - e) +++ reversepath p) z =
lp15@65039
   246
                winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
lp15@65039
   247
    proof (rule winding_number_from_innerpath
lp15@65039
   248
        [of "linepath (a + e) (a - e)" "a+e" "a-e" p
lp15@65039
   249
          "linepath (a + e) c +++ linepath c (a - e)" z
lp15@65039
   250
          "winding_number (linepath (a - e)  c +++ linepath  c (a + e) +++ linepath (a + e) (a - e)) z"])
lp15@65039
   251
      show sp_aec: "simple_path (linepath (a + e) c +++ linepath c (a - e))"
lp15@65039
   252
      proof (rule arc_imp_simple_path [OF arc_join])
lp15@65039
   253
        show "arc (linepath (a + e) c)"
lp15@65039
   254
          by (metis \<open>c \<notin> path_image p\<close> arc_linepath pathstart_in_path_image psp)
lp15@65039
   255
        show "arc (linepath c (a - e))"
lp15@65039
   256
          by (metis \<open>c \<notin> path_image p\<close> arc_linepath pathfinish_in_path_image pfp)
lp15@65039
   257
        show "path_image (linepath (a + e) c) \<inter> path_image (linepath c (a - e)) \<subseteq> {pathstart (linepath c (a - e))}"
lp15@65039
   258
          by clarsimp (metis "*" IntI Int_closed_segment closed_segment_commute singleton_iff)
lp15@65039
   259
      qed auto
lp15@65039
   260
      show "simple_path p"
lp15@65039
   261
        using \<open>arc p\<close> arc_simple_path by blast
lp15@65039
   262
      show sp_ae2: "simple_path (linepath (a + e) (a - e))"
lp15@65039
   263
        using \<open>arc p\<close> arc_distinct_ends pfp psp by fastforce
lp15@65039
   264
      show pa: "pathfinish (linepath (a + e) (a - e)) = a - e"
lp15@65039
   265
           "pathstart (linepath (a + e) c +++ linepath c (a - e)) = a + e"
lp15@65039
   266
           "pathfinish (linepath (a + e) c +++ linepath c (a - e)) = a - e"
lp15@65039
   267
           "pathstart p = a + e" "pathfinish p = a - e"
lp15@65039
   268
           "pathstart (linepath (a + e) (a - e)) = a + e"
lp15@65039
   269
        by (simp_all add: assms)
lp15@65039
   270
      show 1: "path_image (linepath (a + e) (a - e)) \<inter> path_image p = {a + e, a - e}"
lp15@65039
   271
      proof
lp15@65039
   272
        show "path_image (linepath (a + e) (a - e)) \<inter> path_image p \<subseteq> {a + e, a - e}"
lp15@65039
   273
          using pap closed_segment_commute psp segment_convex_hull by fastforce
lp15@65039
   274
        show "{a + e, a - e} \<subseteq> path_image (linepath (a + e) (a - e)) \<inter> path_image p"
lp15@65039
   275
          using pap pathfinish_in_path_image pathstart_in_path_image pfp psp by fastforce
lp15@65039
   276
      qed
lp15@65039
   277
      show 2: "path_image (linepath (a + e) (a - e)) \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) =
lp15@65039
   278
               {a + e, a - e}"  (is "?lhs = ?rhs")
lp15@65039
   279
      proof
lp15@65039
   280
        have "\<not> collinear {c, a + e, a - e}"
lp15@65039
   281
          using * by (simp add: insert_commute)
lp15@65039
   282
        then have "convex hull {a + e, a - e} \<inter> convex hull {a + e, c} = {a + e}"
lp15@65039
   283
                  "convex hull {a + e, a - e} \<inter> convex hull {c, a - e} = {a - e}"
lp15@65039
   284
          by (metis (full_types) Int_closed_segment insert_commute segment_convex_hull)+
lp15@65039
   285
        then show "?lhs \<subseteq> ?rhs"
lp15@65039
   286
          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)
lp15@65039
   287
        show "?rhs \<subseteq> ?lhs"
lp15@65039
   288
          using segment_convex_hull by (simp add: path_image_join)
lp15@65039
   289
      qed
lp15@65039
   290
      have "path_image p \<inter> path_image (linepath (a + e) c) \<subseteq> {a + e}"
lp15@65039
   291
      proof (clarsimp simp: path_image_join)
lp15@65039
   292
        fix x
lp15@65039
   293
        assume "x \<in> path_image p" and x_ac: "x \<in> closed_segment (a + e) c"
lp15@65039
   294
        then have "dist x a \<ge> e"
lp15@65039
   295
          by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less)
lp15@65039
   296
        with x_ac dac \<open>e > 0\<close> show "x = a + e"
lp15@65039
   297
          by (auto simp: norm_minus_commute dist_norm closed_segment_eq_open dest: open_segment_furthest_le [where y=a])
lp15@65039
   298
      qed
lp15@65039
   299
      moreover
lp15@65039
   300
      have "path_image p \<inter> path_image (linepath c (a - e)) \<subseteq> {a - e}"
lp15@65039
   301
      proof (clarsimp simp: path_image_join)
lp15@65039
   302
        fix x
lp15@65039
   303
        assume "x \<in> path_image p" and x_ac: "x \<in> closed_segment c (a - e)"
lp15@65039
   304
        then have "dist x a \<ge> e"
lp15@65039
   305
          by (metis IntI all_not_in_conv disj dist_commute mem_ball not_less)
lp15@65039
   306
        with x_ac dac \<open>e > 0\<close> show "x = a - e"
lp15@65039
   307
          by (auto simp: norm_minus_commute dist_norm closed_segment_eq_open dest: open_segment_furthest_le [where y=a])
lp15@65039
   308
      qed
lp15@65039
   309
      ultimately
lp15@65039
   310
      have "path_image p \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) \<subseteq> {a + e, a - e}"
lp15@65039
   311
        by (force simp: path_image_join)
lp15@65039
   312
      then show 3: "path_image p \<inter> path_image (linepath (a + e) c +++ linepath c (a - e)) = {a + e, a - e}"
lp15@65039
   313
        apply (rule equalityI)
lp15@65039
   314
        apply (clarsimp simp: path_image_join)
lp15@65039
   315
        apply (metis pathstart_in_path_image psp pathfinish_in_path_image pfp)
lp15@65039
   316
        done
lp15@65039
   317
      show 4: "path_image (linepath (a + e) c +++ linepath c (a - e)) \<inter>
lp15@65039
   318
               inside (path_image (linepath (a + e) (a - e)) \<union> path_image p) \<noteq> {}"
lp15@65039
   319
        apply (clarsimp simp: path_image_join segment_convex_hull disjoint_iff_not_equal)
lp15@65039
   320
        by (metis (no_types, hide_lams) UnI1 Un_commute c closed_segment_commute ends_in_segment(1) path_image_join
lp15@65039
   321
                  path_image_linepath pathstart_linepath pfp segment_convex_hull)
lp15@65039
   322
      show zin_inside: "z \<in> inside (path_image (linepath (a + e) (a - e)) \<union>
lp15@65039
   323
                                    path_image (linepath (a + e) c +++ linepath c (a - e)))"
lp15@65039
   324
        apply (simp add: path_image_join)
lp15@65039
   325
        by (metis z inside_of_triangle DIM_complex Un_commute closed_segment_commute)
lp15@65039
   326
      show 5: "winding_number
lp15@65039
   327
             (linepath (a + e) (a - e) +++ reversepath (linepath (a + e) c +++ linepath c (a - e))) z =
lp15@65039
   328
            winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
lp15@65039
   329
        by (simp add: reversepath_joinpaths path_image_join winding_number_join)
lp15@65039
   330
      show 6: "winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z \<noteq> 0"
lp15@65039
   331
        by (simp add: winding_number_triangle z)
lp15@65039
   332
      show "winding_number (linepath (a + e) (a - e) +++ reversepath p) z =
lp15@65039
   333
            winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z"
lp15@65039
   334
        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)
lp15@65039
   335
    qed (use assms \<open>e > 0\<close> in auto)
lp15@65039
   336
    show "z \<in> inside (path_image (p +++ linepath (a - e) (a + e)))"
lp15@65039
   337
      using zin by (simp add: assms path_image_join Un_commute closed_segment_commute)
lp15@65039
   338
    then have "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) =
lp15@65039
   339
               cmod ((winding_number(reversepath (p +++ linepath (a - e) (a + e))) z))"
lp15@65039
   340
      apply (subst winding_number_reversepath)
lp15@65039
   341
      using simple_path_imp_path sp_pl apply blast
lp15@65039
   342
       apply (metis IntI emptyE inside_no_overlap)
lp15@65039
   343
      by (simp add: inside_def)
lp15@65039
   344
    also have "... = cmod (winding_number(linepath (a + e) (a - e) +++ reversepath p) z)"
lp15@65039
   345
      by (simp add: pfp reversepath_joinpaths)
lp15@65039
   346
    also have "... = cmod (winding_number (linepath (a - e) c +++ linepath c (a + e) +++ linepath (a + e) (a - e)) z)"
lp15@65039
   347
      by (simp add: zeq)
lp15@65039
   348
    also have "... = 1"
lp15@65039
   349
      using z by (simp add: interior_of_triangle winding_number_triangle)
lp15@65039
   350
    finally show "cmod (winding_number (p +++ linepath (a - e) (a + e)) z) = 1" .
lp15@65039
   351
  qed
lp15@65039
   352
qed
lp15@65039
   353
lp15@65039
   354
lemma simple_closed_path_wn2:
lp15@65039
   355
  fixes a::complex and d e::real
lp15@65039
   356
  assumes "0 < d" "0 < e"
lp15@65039
   357
    and sp_pl: "simple_path(p +++ linepath (a - d) (a + e))"
lp15@65039
   358
    and psp:   "pathstart p = a + e"
lp15@65039
   359
    and pfp:   "pathfinish p = a - d"
lp15@65039
   360
obtains z where "z \<in> inside (path_image (p +++ linepath (a - d) (a + e)))"
lp15@65039
   361
                "cmod (winding_number (p +++ linepath (a - d) (a + e)) z) = 1"
lp15@65039
   362
proof -
lp15@65039
   363
  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
lp15@65039
   364
    using closed_segment_translation_eq [of a]
lp15@65039
   365
    by (metis (no_types, hide_lams) add_uminus_conv_diff of_real_minus of_real_closed_segment)
lp15@65039
   366
  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
lp15@65039
   367
    by (metis closed_segment_translation_eq diff_conv_add_uminus of_real_closed_segment of_real_minus)
lp15@65039
   368
  have "arc p" and arc_lp: "arc (linepath (a - d) (a + e))" and "path p"
lp15@65039
   369
    and pap: "path_image p \<inter> closed_segment (a - d) (a + e) \<subseteq> {a+e, a-d}"
lp15@65039
   370
    using simple_path_join_loop_eq [of "linepath (a - d) (a + e)" p] assms arc_imp_path  by auto
lp15@65039
   371
  have "0 \<in> closed_segment (-d) e"
lp15@65039
   372
    using \<open>0 < d\<close> \<open>0 < e\<close> closed_segment_eq_real_ivl by auto
lp15@65039
   373
  then have "a \<in> path_image (linepath (a - d) (a + e))"
lp15@65039
   374
    using of_real_closed_segment [THEN iffD2]
lp15@65039
   375
    by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
lp15@65039
   376
  then have "a \<notin> path_image p"
lp15@65039
   377
    using \<open>0 < d\<close> \<open>0 < e\<close> pap by auto
lp15@65039
   378
  then obtain k where "0 < k" and k: "ball a k \<inter> (path_image p) = {}"
lp15@65039
   379
    using \<open>0 < e\<close> \<open>path p\<close> not_on_path_ball by blast
lp15@65039
   380
  define kde where "kde \<equiv> (min k (min d e)) / 2"
lp15@65039
   381
  have "0 < kde" "kde < k" "kde < d" "kde < e"
lp15@65039
   382
    using \<open>0 < k\<close> \<open>0 < d\<close> \<open>0 < e\<close> by (auto simp: kde_def)
lp15@65039
   383
  let ?q = "linepath (a + kde) (a + e) +++ p +++ linepath (a - d) (a - kde)"
lp15@65039
   384
  have "- kde \<in> closed_segment (-d) e"
lp15@65039
   385
    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
lp15@65039
   386
  then have a_diff_kde: "a - kde \<in> closed_segment (a - d) (a + e)"
lp15@65039
   387
    using of_real_closed_segment [THEN iffD2]
lp15@65039
   388
    by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
lp15@65039
   389
  then have clsub2: "closed_segment (a - d) (a - kde) \<subseteq> closed_segment (a - d) (a + e)"
lp15@65039
   390
    by (simp add: subset_closed_segment)
lp15@65039
   391
  then have "path_image p \<inter> closed_segment (a - d) (a - kde) \<subseteq> {a + e, a - d}"
lp15@65039
   392
    using pap by force
lp15@65039
   393
  moreover
lp15@65039
   394
  have "a + e \<notin> path_image p \<inter> closed_segment (a - d) (a - kde)"
lp15@65039
   395
    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>0 < e\<close> by (auto simp: closed_segment_eq_real_ivl)
lp15@65039
   396
  ultimately have sub_a_diff_d: "path_image p \<inter> closed_segment (a - d) (a - kde) \<subseteq> {a - d}"
lp15@65039
   397
    by blast
lp15@65039
   398
  have "kde \<in> closed_segment (-d) e"
lp15@65039
   399
    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
lp15@65039
   400
  then have a_diff_kde: "a + kde \<in> closed_segment (a - d) (a + e)"
lp15@65039
   401
    using of_real_closed_segment [THEN iffD2]
lp15@65039
   402
    by (force dest: closed_segment_translation_eq [of "a", THEN iffD2] simp del: of_real_closed_segment)
lp15@65039
   403
  then have clsub1: "closed_segment (a + kde) (a + e) \<subseteq> closed_segment (a - d) (a + e)"
lp15@65039
   404
    by (simp add: subset_closed_segment)
lp15@65039
   405
  then have "closed_segment (a + kde) (a + e) \<inter> path_image p \<subseteq> {a + e, a - d}"
lp15@65039
   406
    using pap by force
lp15@65039
   407
  moreover
lp15@65039
   408
  have "closed_segment (a + kde) (a + e) \<inter> closed_segment (a - d) (a - kde) = {}"
lp15@65039
   409
  proof (clarsimp intro!: equals0I)
lp15@65039
   410
    fix y
lp15@65039
   411
    assume y1: "y \<in> closed_segment (a + kde) (a + e)"
lp15@65039
   412
       and y2: "y \<in> closed_segment (a - d) (a - kde)"
lp15@65039
   413
    obtain u where u: "y = a + of_real u" and "0 < u"
lp15@65039
   414
      using y1 \<open>0 < kde\<close> \<open>kde < e\<close> \<open>0 < e\<close> apply (clarsimp simp: in_segment)
lp15@65039
   415
      apply (rule_tac u = "(1 - u)*kde + u*e" in that)
lp15@65039
   416
       apply (auto simp: scaleR_conv_of_real algebra_simps)
lp15@65039
   417
      by (meson le_less_trans less_add_same_cancel2 less_eq_real_def mult_left_mono)
lp15@65039
   418
    moreover
lp15@65039
   419
    obtain v where v: "y = a + of_real v" and "v \<le> 0"
lp15@65039
   420
      using y2 \<open>0 < kde\<close> \<open>0 < d\<close> \<open>0 < e\<close> apply (clarsimp simp: in_segment)
lp15@65039
   421
      apply (rule_tac v = "- ((1 - u)*d + u*kde)" in that)
lp15@65039
   422
       apply (force simp: scaleR_conv_of_real algebra_simps)
lp15@65039
   423
      by (meson less_eq_real_def neg_le_0_iff_le segment_bound_lemma)
lp15@65039
   424
    ultimately show False
lp15@65039
   425
      by auto
lp15@65039
   426
  qed
lp15@65039
   427
  moreover have "a - d \<notin> closed_segment (a + kde) (a + e)"
lp15@65039
   428
    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>0 < e\<close> by (auto simp: closed_segment_eq_real_ivl)
lp15@65039
   429
  ultimately have sub_a_plus_e:
lp15@65039
   430
    "closed_segment (a + kde) (a + e) \<inter> (path_image p \<union> closed_segment (a - d) (a - kde))
lp15@65039
   431
       \<subseteq> {a + e}"
lp15@65039
   432
    by auto
lp15@65039
   433
  have "kde \<in> closed_segment (-kde) e"
lp15@65039
   434
    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
lp15@65039
   435
  then have a_add_kde: "a + kde \<in> closed_segment (a - kde) (a + e)"
lp15@65039
   436
    using of_real_closed_segment [THEN iffD2]
lp15@65039
   437
    by (force dest: closed_segment_translation_eq [of "a", THEN iffD2] simp del: of_real_closed_segment)
lp15@65039
   438
  have "closed_segment (a - kde) (a + kde) \<inter> closed_segment (a + kde) (a + e) = {a + kde}"
lp15@65039
   439
    by (metis a_add_kde Int_closed_segment)
lp15@65039
   440
  moreover
lp15@65039
   441
  have "path_image p \<inter> closed_segment (a - kde) (a + kde) = {}"
lp15@65039
   442
  proof (rule equals0I, clarify)
lp15@65039
   443
    fix y  assume "y \<in> path_image p" "y \<in> closed_segment (a - kde) (a + kde)"
lp15@65039
   444
    with equals0D [OF k, of y] \<open>0 < kde\<close> \<open>kde < k\<close> show False
lp15@65039
   445
      by (auto simp: dist_norm dest: dist_decreases_closed_segment [where c=a])
lp15@65039
   446
  qed
lp15@65039
   447
  moreover
lp15@65039
   448
  have "- kde \<in> closed_segment (-d) kde"
lp15@65039
   449
    using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < e\<close> closed_segment_eq_real_ivl by auto
lp15@65039
   450
  then have a_diff_kde': "a - kde \<in> closed_segment (a - d) (a + kde)"
lp15@65039
   451
    using of_real_closed_segment [THEN iffD2]
lp15@65039
   452
    by (force dest: closed_segment_translation_eq [of a, THEN iffD2] simp del: of_real_closed_segment)
lp15@65039
   453
  then have "closed_segment (a - d) (a - kde) \<inter> closed_segment (a - kde) (a + kde) = {a - kde}"
lp15@65039
   454
    by (metis Int_closed_segment)
lp15@65039
   455
  ultimately
lp15@65039
   456
  have pa_subset_pm_kde: "path_image ?q \<inter> closed_segment (a - kde) (a + kde) \<subseteq> {a - kde, a + kde}"
lp15@65039
   457
    by (auto simp: path_image_join assms)
lp15@65039
   458
  have ge_kde1: "\<exists>y. x = a + y \<and> y \<ge> kde" if "x \<in> closed_segment (a + kde) (a + e)" for x
lp15@65039
   459
    using that \<open>kde < e\<close> mult_le_cancel_left
lp15@65039
   460
    apply (auto simp: in_segment)
lp15@65039
   461
    apply (rule_tac x="(1-u)*kde + u*e" in exI)
lp15@65039
   462
    apply (fastforce simp: algebra_simps scaleR_conv_of_real)
lp15@65039
   463
    done
lp15@65039
   464
  have ge_kde2: "\<exists>y. x = a + y \<and> y \<le> -kde" if "x \<in> closed_segment (a - d) (a - kde)" for x
lp15@65039
   465
    using that \<open>kde < d\<close> affine_ineq
lp15@65039
   466
    apply (auto simp: in_segment)
lp15@65039
   467
    apply (rule_tac x="- ((1-u)*d + u*kde)" in exI)
lp15@65039
   468
    apply (fastforce simp: algebra_simps scaleR_conv_of_real)
lp15@65039
   469
    done
lp15@65039
   470
  have notin_paq: "x \<notin> path_image ?q" if "dist a x < kde" for x
lp15@65039
   471
    using that using \<open>0 < kde\<close> \<open>kde < d\<close> \<open>kde < k\<close>
lp15@65039
   472
    apply (auto simp: path_image_join assms dist_norm dest!: ge_kde1 ge_kde2)
lp15@65039
   473
    by (meson k disjoint_iff_not_equal le_less_trans less_eq_real_def mem_ball that)
lp15@65039
   474
  obtain z where zin: "z \<in> inside (path_image (?q +++ linepath (a - kde) (a + kde)))"
lp15@65039
   475
           and z1: "cmod (winding_number (?q +++ linepath (a - kde) (a + kde)) z) = 1"
lp15@65039
   476
  proof (rule simple_closed_path_wn1 [of kde ?q a])
lp15@65039
   477
    show "simple_path (?q +++ linepath (a - kde) (a + kde))"
lp15@65039
   478
    proof (intro simple_path_join_loop conjI)
lp15@65039
   479
      show "arc ?q"
lp15@65039
   480
      proof (rule arc_join)
lp15@65039
   481
        show "arc (linepath (a + kde) (a + e))"
lp15@65039
   482
          using \<open>kde < e\<close> \<open>arc p\<close> by (force simp: pfp)
lp15@65039
   483
        show "arc (p +++ linepath (a - d) (a - kde))"
lp15@65039
   484
          using \<open>kde < d\<close> \<open>kde < e\<close> \<open>arc p\<close> sub_a_diff_d by (force simp: pfp intro: arc_join)
lp15@65039
   485
      qed (auto simp: psp pfp path_image_join sub_a_plus_e)
lp15@65039
   486
      show "arc (linepath (a - kde) (a + kde))"
lp15@65039
   487
        using \<open>0 < kde\<close> by auto
lp15@65039
   488
    qed (use pa_subset_pm_kde in auto)
lp15@65039
   489
  qed (use \<open>0 < kde\<close> notin_paq in auto)
lp15@65039
   490
  have eq: "path_image (?q +++ linepath (a - kde) (a + kde)) = path_image (p +++ linepath (a - d) (a + e))"
lp15@65039
   491
            (is "?lhs = ?rhs")
lp15@65039
   492
  proof
lp15@65039
   493
    show "?lhs \<subseteq> ?rhs"
lp15@65039
   494
      using clsub1 clsub2 apply (auto simp: path_image_join assms)
lp15@65039
   495
      by (meson subsetCE subset_closed_segment)
lp15@65039
   496
    show "?rhs \<subseteq> ?lhs"
lp15@65039
   497
      apply (simp add: path_image_join assms Un_ac)
lp15@65039
   498
        by (metis Un_closed_segment Un_assoc a_diff_kde a_diff_kde' le_supI2 subset_refl)
lp15@65039
   499
    qed
lp15@65039
   500
  show thesis
lp15@65039
   501
  proof
lp15@65039
   502
    show zzin: "z \<in> inside (path_image (p +++ linepath (a - d) (a + e)))"
lp15@65039
   503
      by (metis eq zin)
lp15@65039
   504
    then have znotin: "z \<notin> path_image p"
lp15@65039
   505
      by (metis ComplD Un_iff inside_Un_outside path_image_join pathfinish_linepath pathstart_reversepath pfp reversepath_linepath)
lp15@65039
   506
    have znotin_de: "z \<notin> closed_segment (a - d) (a + kde)"
lp15@65039
   507
      by (metis ComplD Un_iff Un_closed_segment a_diff_kde inside_Un_outside path_image_join path_image_linepath pathstart_linepath pfp zzin)
lp15@65039
   508
    have "winding_number (linepath (a - d) (a + e)) z =
lp15@65039
   509
          winding_number (linepath (a - d) (a + kde)) z + winding_number (linepath (a + kde) (a + e)) z"
lp15@65039
   510
      apply (rule winding_number_split_linepath)
lp15@65039
   511
      apply (simp add: a_diff_kde)
lp15@65039
   512
      by (metis ComplD Un_iff inside_Un_outside path_image_join path_image_linepath pathstart_linepath pfp zzin)
lp15@65039
   513
    also have "... = winding_number (linepath (a + kde) (a + e)) z +
lp15@65039
   514
                     (winding_number (linepath (a - d) (a - kde)) z +
lp15@65039
   515
                      winding_number (linepath (a - kde) (a + kde)) z)"
lp15@65039
   516
      by (simp add: winding_number_split_linepath [of "a-kde", symmetric] znotin_de a_diff_kde')
lp15@65039
   517
    finally have "winding_number (p +++ linepath (a - d) (a + e)) z =
lp15@65039
   518
                    winding_number p z + winding_number (linepath (a + kde) (a + e)) z +
lp15@65039
   519
                   (winding_number (linepath (a - d) (a - kde)) z +
lp15@65039
   520
                    winding_number (linepath (a - kde) (a + kde)) z)"
lp15@65039
   521
      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)
lp15@65039
   522
    also have "... = winding_number ?q z + winding_number (linepath (a - kde) (a + kde)) z"
lp15@65039
   523
      using \<open>path p\<close> znotin assms zzin clsub1
lp15@65039
   524
      apply (subst winding_number_join, auto)
lp15@65039
   525
      apply (metis (no_types, hide_lams) ComplD Un_iff contra_subsetD inside_Un_outside path_image_join path_image_linepath pathstart_linepath)
lp15@65039
   526
      apply (metis Un_iff Un_closed_segment a_diff_kde' not_in_path_image_join path_image_linepath znotin_de)
lp15@65039
   527
      by (metis Un_iff Un_closed_segment a_diff_kde' path_image_linepath path_linepath pathstart_linepath winding_number_join znotin_de)
lp15@65039
   528
    also have "... = winding_number (?q +++ linepath (a - kde) (a + kde)) z"
lp15@65039
   529
      using \<open>path p\<close> assms zin
lp15@65039
   530
      apply (subst winding_number_join [symmetric], auto)
lp15@65039
   531
      apply (metis ComplD Un_iff path_image_join pathfinish_join pathfinish_linepath pathstart_linepath union_with_outside)
lp15@65039
   532
      by (metis Un_iff Un_closed_segment a_diff_kde' znotin_de)
lp15@65039
   533
    finally have "winding_number (p +++ linepath (a - d) (a + e)) z =
lp15@65039
   534
                  winding_number (?q +++ linepath (a - kde) (a + kde)) z" .
lp15@65039
   535
    then show "cmod (winding_number (p +++ linepath (a - d) (a + e)) z) = 1"
lp15@65039
   536
      by (simp add: z1)
lp15@65039
   537
  qed
lp15@65039
   538
qed
lp15@65039
   539
wl302@69423
   540
lemma simple_closed_path_wn3:
lp15@65039
   541
  fixes p :: "real \<Rightarrow> complex"
lp15@65039
   542
  assumes "simple_path p" and loop: "pathfinish p = pathstart p"
lp15@65039
   543
  obtains z where "z \<in> inside (path_image p)" "cmod (winding_number p z) = 1"
lp15@65039
   544
proof -
lp15@65039
   545
  have ins: "inside(path_image p) \<noteq> {}" "open(inside(path_image p))"
lp15@65039
   546
            "connected(inside(path_image p))"
lp15@65039
   547
   and out: "outside(path_image p) \<noteq> {}" "open(outside(path_image p))"
lp15@65039
   548
            "connected(outside(path_image p))"
lp15@65039
   549
   and bo:  "bounded(inside(path_image p))" "\<not> bounded(outside(path_image p))"
lp15@65039
   550
   and ins_out: "inside(path_image p) \<inter> outside(path_image p) = {}"
lp15@65039
   551
                "inside(path_image p) \<union> outside(path_image p) = - path_image p"
lp15@65039
   552
   and fro: "frontier(inside(path_image p)) = path_image p"
lp15@65039
   553
            "frontier(outside(path_image p)) = path_image p"
lp15@65039
   554
    using Jordan_inside_outside [OF assms] by auto
lp15@65039
   555
  obtain a where a: "a \<in> inside(path_image p)"
lp15@65039
   556
    using \<open>inside (path_image p) \<noteq> {}\<close> by blast
lp15@65039
   557
  obtain d::real where "0 < d" and d_fro: "a - d \<in> frontier (inside (path_image p))"
lp15@65039
   558
                 and d_int: "\<And>\<epsilon>. \<lbrakk>0 \<le> \<epsilon>; \<epsilon> < d\<rbrakk> \<Longrightarrow> (a - \<epsilon>) \<in> inside (path_image p)"
lp15@65039
   559
    apply (rule ray_to_frontier [of "inside (path_image p)" a "-1"])
lp15@65039
   560
    using \<open>bounded (inside (path_image p))\<close> \<open>open (inside (path_image p))\<close> a interior_eq
lp15@65039
   561
       apply (auto simp: of_real_def)
lp15@65039
   562
    done
lp15@65039
   563
  obtain e::real where "0 < e" and e_fro: "a + e \<in> frontier (inside (path_image p))"
lp15@65039
   564
    and e_int: "\<And>\<epsilon>. \<lbrakk>0 \<le> \<epsilon>; \<epsilon> < e\<rbrakk> \<Longrightarrow> (a + \<epsilon>) \<in> inside (path_image p)"
lp15@65039
   565
    apply (rule ray_to_frontier [of "inside (path_image p)" a 1])
lp15@65039
   566
    using \<open>bounded (inside (path_image p))\<close> \<open>open (inside (path_image p))\<close> a interior_eq
lp15@65039
   567
       apply (auto simp: of_real_def)
lp15@65039
   568
    done
lp15@65039
   569
  obtain t0 where "0 \<le> t0" "t0 \<le> 1" and pt: "p t0 = a - d"
lp15@65039
   570
    using a d_fro fro by (auto simp: path_image_def)
lp15@65039
   571
  obtain q where "simple_path q" and q_ends: "pathstart q = a - d" "pathfinish q = a - d"
lp15@65039
   572
    and q_eq_p: "path_image q = path_image p"
lp15@65039
   573
    and wn_q_eq_wn_p: "\<And>z. z \<in> inside(path_image p) \<Longrightarrow> winding_number q z = winding_number p z"
lp15@65039
   574
  proof
lp15@65039
   575
    show "simple_path (shiftpath t0 p)"
lp15@65039
   576
      by (simp add: pathstart_shiftpath pathfinish_shiftpath
lp15@65039
   577
          simple_path_shiftpath path_image_shiftpath \<open>0 \<le> t0\<close> \<open>t0 \<le> 1\<close> assms)
lp15@65039
   578
    show "pathstart (shiftpath t0 p) = a - d"
lp15@65039
   579
      using pt by (simp add: \<open>t0 \<le> 1\<close> pathstart_shiftpath)
lp15@65039
   580
    show "pathfinish (shiftpath t0 p) = a - d"
lp15@65039
   581
      by (simp add: \<open>0 \<le> t0\<close> loop pathfinish_shiftpath pt)
lp15@65039
   582
    show "path_image (shiftpath t0 p) = path_image p"
lp15@65039
   583
      by (simp add: \<open>0 \<le> t0\<close> \<open>t0 \<le> 1\<close> loop path_image_shiftpath)
lp15@65039
   584
    show "winding_number (shiftpath t0 p) z = winding_number p z"
lp15@65039
   585
      if "z \<in> inside (path_image p)" for z
lp15@65039
   586
      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
lp15@65039
   587
          loop simple_path_imp_path that winding_number_shiftpath)
lp15@65039
   588
  qed
lp15@65039
   589
  have ad_not_ae: "a - d \<noteq> a + e"
lp15@65039
   590
    by (metis \<open>0 < d\<close> \<open>0 < e\<close> add.left_inverse add_left_cancel add_uminus_conv_diff
lp15@65039
   591
        le_add_same_cancel2 less_eq_real_def not_less of_real_add of_real_def of_real_eq_0_iff pt)
lp15@65039
   592
  have ad_ae_q: "{a - d, a + e} \<subseteq> path_image q"
lp15@65039
   593
    using \<open>path_image q = path_image p\<close> d_fro e_fro fro(1) by auto
lp15@65039
   594
  have ada: "open_segment (a - d) a \<subseteq> inside (path_image p)"
lp15@65039
   595
  proof (clarsimp simp: in_segment)
lp15@65039
   596
    fix u::real assume "0 < u" "u < 1"
lp15@65039
   597
    with d_int have "a - (1 - u) * d \<in> inside (path_image p)"
lp15@65039
   598
      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)
lp15@65039
   599
    then show "(1 - u) *\<^sub>R (a - d) + u *\<^sub>R a \<in> inside (path_image p)"
lp15@65039
   600
      by (simp add: diff_add_eq of_real_def real_vector.scale_right_diff_distrib)
lp15@65039
   601
  qed
lp15@65039
   602
  have aae: "open_segment a (a + e) \<subseteq> inside (path_image p)"
lp15@65039
   603
  proof (clarsimp simp: in_segment)
lp15@65039
   604
    fix u::real assume "0 < u" "u < 1"
lp15@65039
   605
    with e_int have "a + u * e \<in> inside (path_image p)"
lp15@65039
   606
      by (meson \<open>0 < e\<close> less_eq_real_def mult_less_cancel_right2 not_less zero_less_mult_iff)
lp15@65039
   607
    then show "(1 - u) *\<^sub>R a + u *\<^sub>R (a + e) \<in> inside (path_image p)"
lp15@65039
   608
      apply (simp add: algebra_simps)
lp15@65039
   609
      by (simp add: diff_add_eq of_real_def real_vector.scale_right_diff_distrib)
lp15@65039
   610
  qed
lp15@65039
   611
  have "complex_of_real (d * d + (e * e + d * (e + e))) \<noteq> 0"
lp15@65039
   612
    using ad_not_ae
lp15@65039
   613
    by (metis \<open>0 < d\<close> \<open>0 < e\<close> add_strict_left_mono less_add_same_cancel1 not_sum_squares_lt_zero
lp15@65039
   614
        of_real_eq_0_iff zero_less_double_add_iff_zero_less_single_add zero_less_mult_iff)
lp15@65039
   615
  then have a_in_de: "a \<in> open_segment (a - d) (a + e)"
lp15@65039
   616
    using ad_not_ae \<open>0 < d\<close> \<open>0 < e\<close>
lp15@65039
   617
    apply (auto simp: in_segment algebra_simps scaleR_conv_of_real)
lp15@65039
   618
    apply (rule_tac x="d / (d+e)" in exI)
lp15@65039
   619
    apply (auto simp: field_simps)
lp15@65039
   620
    done
lp15@65039
   621
  then have "open_segment (a - d) (a + e) \<subseteq> inside (path_image p)"
lp15@65039
   622
    using ada a aae Un_open_segment [of a "a-d" "a+e"] by blast
lp15@65039
   623
  then have "path_image q \<inter> open_segment (a - d) (a + e) = {}"
lp15@65039
   624
    using inside_no_overlap by (fastforce simp: q_eq_p)
lp15@65039
   625
  with ad_ae_q have paq_Int_cs: "path_image q \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}"
lp15@65039
   626
    by (simp add: closed_segment_eq_open)
lp15@65039
   627
  obtain t where "0 \<le> t" "t \<le> 1" and qt: "q t = a + e"
lp15@65039
   628
    using a e_fro fro ad_ae_q by (auto simp: path_defs)
lp15@65039
   629
  then have "t \<noteq> 0"
lp15@65039
   630
    by (metis ad_not_ae pathstart_def q_ends(1))
lp15@65039
   631
  then have "t \<noteq> 1"
lp15@65039
   632
    by (metis ad_not_ae pathfinish_def q_ends(2) qt)
lp15@65039
   633
  have q01: "q 0 = a - d" "q 1 = a - d"
lp15@65039
   634
    using q_ends by (auto simp: pathstart_def pathfinish_def)
lp15@65039
   635
  obtain z where zin: "z \<in> inside (path_image (subpath t 0 q +++ linepath (a - d) (a + e)))"
lp15@65039
   636
             and z1: "cmod (winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z) = 1"
lp15@65039
   637
  proof (rule simple_closed_path_wn2 [of d e "subpath t 0 q" a], simp_all add: q01)
lp15@65039
   638
    show "simple_path (subpath t 0 q +++ linepath (a - d) (a + e))"
lp15@65039
   639
    proof (rule simple_path_join_loop, simp_all add: qt q01)
lp15@65039
   640
      have "inj_on q (closed_segment t 0)"
lp15@65039
   641
        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>
lp15@65039
   642
        by (fastforce simp: simple_path_def inj_on_def closed_segment_eq_real_ivl)
lp15@65039
   643
      then show "arc (subpath t 0 q)"
lp15@65039
   644
        using \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> \<open>t \<noteq> 0\<close>
lp15@65039
   645
        by (simp add: arc_subpath_eq simple_path_imp_path)
lp15@65039
   646
      show "arc (linepath (a - d) (a + e))"
lp15@65039
   647
        by (simp add: ad_not_ae)
lp15@65039
   648
      show "path_image (subpath t 0 q) \<inter> closed_segment (a - d) (a + e) \<subseteq> {a + e, a - d}"
lp15@65039
   649
        using qt paq_Int_cs  \<open>simple_path q\<close> \<open>0 \<le> t\<close> \<open>t \<le> 1\<close>
lp15@65039
   650
        by (force simp: dest: rev_subsetD [OF _ path_image_subpath_subset] intro: simple_path_imp_path)
lp15@65039
   651
    qed
lp15@65039
   652
  qed (auto simp: \<open>0 < d\<close> \<open>0 < e\<close> qt)
lp15@65039
   653
  have pa01_Un: "path_image (subpath 0 t q) \<union> path_image (subpath 1 t q) = path_image q"
lp15@65039
   654
    unfolding path_image_subpath
lp15@65039
   655
    using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> by (force simp: path_image_def image_iff)
lp15@65039
   656
  with paq_Int_cs have pa_01q:
lp15@65039
   657
        "(path_image (subpath 0 t q) \<union> path_image (subpath 1 t q)) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}"
lp15@65039
   658
    by metis
lp15@65039
   659
  have z_notin_ed: "z \<notin> closed_segment (a + e) (a - d)"
lp15@65039
   660
    using zin q01 by (simp add: path_image_join closed_segment_commute inside_def)
lp15@65039
   661
  have z_notin_0t: "z \<notin> path_image (subpath 0 t q)"
lp15@65039
   662
    by (metis (no_types, hide_lams) IntI Un_upper1 subsetD empty_iff inside_no_overlap path_image_join
lp15@65039
   663
        path_image_subpath_commute pathfinish_subpath pathstart_def pathstart_linepath q_ends(1) qt subpath_trivial zin)
lp15@65039
   664
  have [simp]: "- winding_number (subpath t 0 q) z = winding_number (subpath 0 t q) z"
lp15@65039
   665
    by (metis \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close> atLeastAtMost_iff zero_le_one
lp15@65039
   666
              path_image_subpath_commute path_subpath real_eq_0_iff_le_ge_0
lp15@65039
   667
              reversepath_subpath simple_path_imp_path winding_number_reversepath z_notin_0t)
lp15@65039
   668
  obtain z_in_q: "z \<in> inside(path_image q)"
lp15@65039
   669
     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"
lp15@65039
   670
  proof (rule winding_number_from_innerpath
lp15@65039
   671
          [of "subpath 0 t q" "a-d" "a+e" "subpath 1 t q" "linepath (a - d) (a + e)"
lp15@65039
   672
            z "- winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"],
lp15@65039
   673
         simp_all add: q01 qt pa01_Un reversepath_subpath)
lp15@65039
   674
    show "simple_path (subpath 0 t q)" "simple_path (subpath 1 t q)"
lp15@65039
   675
      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)
lp15@65039
   676
    show "simple_path (linepath (a - d) (a + e))"
lp15@65039
   677
      using ad_not_ae by blast
lp15@65039
   678
    show "path_image (subpath 0 t q) \<inter> path_image (subpath 1 t q) = {a - d, a + e}"  (is "?lhs = ?rhs")
lp15@65039
   679
    proof
lp15@65039
   680
      show "?lhs \<subseteq> ?rhs"
lp15@65039
   681
        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
lp15@65039
   682
        by (force simp: pathfinish_def qt simple_path_def path_image_subpath)
lp15@65039
   683
      show "?rhs \<subseteq> ?lhs"
lp15@65039
   684
        using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath)
lp15@65039
   685
    qed
lp15@65039
   686
    show "path_image (subpath 0 t q) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs")
lp15@65039
   687
    proof
lp15@65039
   688
      show "?lhs \<subseteq> ?rhs"  using paq_Int_cs pa01_Un by fastforce
lp15@65039
   689
      show "?rhs \<subseteq> ?lhs"  using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath)
lp15@65039
   690
    qed
lp15@65039
   691
    show "path_image (subpath 1 t q) \<inter> closed_segment (a - d) (a + e) = {a - d, a + e}" (is "?lhs = ?rhs")
lp15@65039
   692
    proof
lp15@65039
   693
      show "?lhs \<subseteq> ?rhs"  by (auto simp: pa_01q [symmetric])
lp15@65039
   694
      show "?rhs \<subseteq> ?lhs"  using \<open>0 \<le> t\<close> \<open>t \<le> 1\<close> q01 qt by (force simp: path_image_subpath)
lp15@65039
   695
    qed
lp15@65039
   696
    show "closed_segment (a - d) (a + e) \<inter> inside (path_image q) \<noteq> {}"
lp15@65039
   697
      using a a_in_de open_closed_segment pa01_Un q_eq_p by fastforce
lp15@65039
   698
    show "z \<in> inside (path_image (subpath 0 t q) \<union> closed_segment (a - d) (a + e))"
lp15@65039
   699
      by (metis path_image_join path_image_linepath path_image_subpath_commute pathfinish_subpath pathstart_linepath q01(1) zin)
lp15@65039
   700
    show "winding_number (subpath 0 t q +++ linepath (a + e) (a - d)) z =
lp15@65039
   701
      - winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z"
lp15@65039
   702
      using z_notin_ed z_notin_0t \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close>
lp15@65039
   703
      by (simp add: simple_path_imp_path qt q01 path_image_subpath_commute closed_segment_commute winding_number_join winding_number_reversepath [symmetric])
eberlm@67135
   704
    show "- d \<noteq> e"
lp15@65039
   705
      using ad_not_ae by auto
lp15@65039
   706
    show "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z \<noteq> 0"
lp15@65039
   707
      using z1 by auto
lp15@65039
   708
  qed
lp15@65039
   709
  show ?thesis
lp15@65039
   710
  proof
lp15@65039
   711
    show "z \<in> inside (path_image p)"
lp15@65039
   712
      using q_eq_p z_in_q by auto
lp15@65039
   713
    then have [simp]: "z \<notin> path_image q"
lp15@65039
   714
      by (metis disjoint_iff_not_equal inside_no_overlap q_eq_p)
lp15@65039
   715
    have [simp]: "z \<notin> path_image (subpath 1 t q)"
lp15@65039
   716
      using inside_def pa01_Un z_in_q by fastforce
lp15@65039
   717
    have "winding_number(subpath 0 t q +++ subpath t 1 q) z = winding_number(subpath 0 1 q) z"
lp15@65039
   718
      using z_notin_0t \<open>0 \<le> t\<close> \<open>simple_path q\<close> \<open>t \<le> 1\<close>
lp15@65039
   719
      by (simp add: simple_path_imp_path qt path_image_subpath_commute winding_number_join winding_number_subpath_combine)
lp15@65039
   720
    with wn_q have "winding_number (subpath t 0 q +++ linepath (a - d) (a + e)) z = - winding_number q z"
lp15@65039
   721
      by auto
lp15@65039
   722
    with z1 have "cmod (winding_number q z) = 1"
lp15@65039
   723
      by simp
lp15@65039
   724
    with z1 wn_q_eq_wn_p show "cmod (winding_number p z) = 1"
lp15@65039
   725
      using z1 wn_q_eq_wn_p  by (simp add: \<open>z \<in> inside (path_image p)\<close>)
lp15@65039
   726
    qed
lp15@65039
   727
qed
lp15@65039
   728
wl302@69423
   729
proposition simple_closed_path_winding_number_inside:
lp15@65039
   730
  assumes "simple_path \<gamma>"
lp15@65039
   731
  obtains "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = 1"
lp15@65039
   732
        | "\<And>z. z \<in> inside(path_image \<gamma>) \<Longrightarrow> winding_number \<gamma> z = -1"
lp15@65039
   733
proof (cases "pathfinish \<gamma> = pathstart \<gamma>")
lp15@65039
   734
  case True
lp15@65039
   735
  have "path \<gamma>"
lp15@65039
   736
    by (simp add: assms simple_path_imp_path)
lp15@66884
   737
  then have const: "winding_number \<gamma> constant_on inside(path_image \<gamma>)"
lp15@65039
   738
  proof (rule winding_number_constant)
lp15@65039
   739
    show "connected (inside(path_image \<gamma>))"
lp15@65039
   740
      by (simp add: Jordan_inside_outside True assms)
lp15@65039
   741
  qed (use inside_no_overlap True in auto)
lp15@65039
   742
  obtain z where zin: "z \<in> inside (path_image \<gamma>)" and z1: "cmod (winding_number \<gamma> z) = 1"
lp15@65039
   743
    using simple_closed_path_wn3 [of \<gamma>] True assms by blast
lp15@65039
   744
  have "winding_number \<gamma> z \<in> \<int>"
lp15@65039
   745
    using zin integer_winding_number [OF \<open>path \<gamma>\<close> True] inside_def by blast
lp15@65039
   746
  with z1 consider "winding_number \<gamma> z = 1" | "winding_number \<gamma> z = -1"
lp15@65039
   747
    apply (auto simp: Ints_def abs_if split: if_split_asm)
lp15@65039
   748
    by (metis of_int_1 of_int_eq_iff of_int_minus)
lp15@66884
   749
  with that const zin show ?thesis
lp15@66884
   750
    unfolding constant_on_def by metis
lp15@65039
   751
next
lp15@65039
   752
  case False
lp15@65039
   753
  then show ?thesis
lp15@65039
   754
    using inside_simple_curve_imp_closed assms that(2) by blast
lp15@65039
   755
qed
lp15@65039
   756
wl302@69423
   757
lemma simple_closed_path_abs_winding_number_inside:
lp15@65039
   758
  assumes "simple_path \<gamma>" "z \<in> inside(path_image \<gamma>)"
lp15@65039
   759
    shows "\<bar>Re (winding_number \<gamma> z)\<bar> = 1"
lp15@65039
   760
  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))
lp15@65039
   761
wl302@69423
   762
lemma simple_closed_path_norm_winding_number_inside:
lp15@65039
   763
  assumes "simple_path \<gamma>" "z \<in> inside(path_image \<gamma>)"
lp15@65039
   764
  shows "norm (winding_number \<gamma> z) = 1"
lp15@65039
   765
proof -
lp15@65039
   766
  have "pathfinish \<gamma> = pathstart \<gamma>"
lp15@65039
   767
    using assms inside_simple_curve_imp_closed by blast
lp15@65039
   768
  with assms integer_winding_number have "winding_number \<gamma> z \<in> \<int>"
lp15@65039
   769
    by (simp add: inside_def simple_path_def)
lp15@65039
   770
  then show ?thesis
lp15@65039
   771
    by (metis assms norm_minus_cancel norm_one simple_closed_path_winding_number_inside)
lp15@65039
   772
qed
lp15@65039
   773
wl302@69423
   774
lemma simple_closed_path_winding_number_cases:
lp15@65039
   775
   "\<lbrakk>simple_path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> path_image \<gamma>\<rbrakk> \<Longrightarrow> winding_number \<gamma> z \<in> {-1,0,1}"
lp15@65039
   776
apply (simp add: inside_Un_outside [of "path_image \<gamma>", symmetric, unfolded set_eq_iff Set.Compl_iff] del: inside_Un_outside)
lp15@65039
   777
   apply (rule simple_closed_path_winding_number_inside)
lp15@65039
   778
  using simple_path_def winding_number_zero_in_outside by blast+
lp15@65039
   779
wl302@69423
   780
lemma simple_closed_path_winding_number_pos:
lp15@65039
   781
   "\<lbrakk>simple_path \<gamma>; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> path_image \<gamma>; 0 < Re(winding_number \<gamma> z)\<rbrakk>
lp15@65039
   782
    \<Longrightarrow> winding_number \<gamma> z = 1"
lp15@65039
   783
using simple_closed_path_winding_number_cases
lp15@65039
   784
  by fastforce
lp15@65039
   785
eberlm@66393
   786
subsection \<open>Winding number for rectangular paths\<close>
eberlm@66393
   787
eberlm@66393
   788
(* TODO: Move *)
eberlm@66393
   789
lemma closed_segmentI:
eberlm@66393
   790
  "u \<in> {0..1} \<Longrightarrow> z = (1 - u) *\<^sub>R a + u *\<^sub>R b \<Longrightarrow> z \<in> closed_segment a b"
eberlm@66393
   791
  by (auto simp: closed_segment_def)
eberlm@66393
   792
lp15@66827
   793
lemma in_cbox_complex_iff:
eberlm@66393
   794
  "x \<in> cbox a b \<longleftrightarrow> Re x \<in> {Re a..Re b} \<and> Im x \<in> {Im a..Im b}"
eberlm@66393
   795
  by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)
eberlm@66393
   796
lp15@66827
   797
lemma box_Complex_eq:
eberlm@66393
   798
  "box (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (box a b \<times> box c d)"
eberlm@66393
   799
  by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)
eberlm@66393
   800
lp15@66827
   801
lemma in_box_complex_iff:
eberlm@66393
   802
  "x \<in> box a b \<longleftrightarrow> Re x \<in> {Re a<..<Re b} \<and> Im x \<in> {Im a<..<Im b}"
eberlm@66393
   803
  by (cases x; cases a; cases b) (auto simp: box_Complex_eq)
eberlm@66393
   804
(* END TODO *)
eberlm@66393
   805
eberlm@66393
   806
lemma closed_segment_same_Re:
eberlm@66393
   807
  assumes "Re a = Re b"
eberlm@66393
   808
  shows   "closed_segment a b = {z. Re z = Re a \<and> Im z \<in> closed_segment (Im a) (Im b)}"
eberlm@66393
   809
proof safe
eberlm@66393
   810
  fix z assume "z \<in> closed_segment a b"
eberlm@66393
   811
  then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
eberlm@66393
   812
    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
eberlm@66393
   813
  from assms show "Re z = Re a" by (auto simp: u)
eberlm@66393
   814
  from u(1) show "Im z \<in> closed_segment (Im a) (Im b)"
eberlm@66393
   815
    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
eberlm@66393
   816
next
eberlm@66393
   817
  fix z assume [simp]: "Re z = Re a" and "Im z \<in> closed_segment (Im a) (Im b)"
eberlm@66393
   818
  then obtain u where u: "u \<in> {0..1}" "Im z = Im a + of_real u * (Im b - Im a)"
eberlm@66393
   819
    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
eberlm@66393
   820
  from u(1) show "z \<in> closed_segment a b" using assms
eberlm@66393
   821
    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
eberlm@66393
   822
qed
eberlm@66393
   823
eberlm@66393
   824
lemma closed_segment_same_Im:
eberlm@66393
   825
  assumes "Im a = Im b"
eberlm@66393
   826
  shows   "closed_segment a b = {z. Im z = Im a \<and> Re z \<in> closed_segment (Re a) (Re b)}"
eberlm@66393
   827
proof safe
eberlm@66393
   828
  fix z assume "z \<in> closed_segment a b"
eberlm@66393
   829
  then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
eberlm@66393
   830
    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
eberlm@66393
   831
  from assms show "Im z = Im a" by (auto simp: u)
eberlm@66393
   832
  from u(1) show "Re z \<in> closed_segment (Re a) (Re b)"
eberlm@66393
   833
    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
eberlm@66393
   834
next
eberlm@66393
   835
  fix z assume [simp]: "Im z = Im a" and "Re z \<in> closed_segment (Re a) (Re b)"
eberlm@66393
   836
  then obtain u where u: "u \<in> {0..1}" "Re z = Re a + of_real u * (Re b - Re a)"
eberlm@66393
   837
    by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
eberlm@66393
   838
  from u(1) show "z \<in> closed_segment a b" using assms
eberlm@66393
   839
    by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
eberlm@66393
   840
qed
eberlm@66393
   841
wl302@69423
   842
definition%important rectpath where
eberlm@66393
   843
  "rectpath a1 a3 = (let a2 = Complex (Re a3) (Im a1); a4 = Complex (Re a1) (Im a3)
lp15@66827
   844
                      in linepath a1 a2 +++ linepath a2 a3 +++ linepath a3 a4 +++ linepath a4 a1)"
eberlm@66393
   845
eberlm@66393
   846
lemma path_rectpath [simp, intro]: "path (rectpath a b)"
eberlm@66393
   847
  by (simp add: Let_def rectpath_def)
eberlm@66393
   848
eberlm@66393
   849
lemma valid_path_rectpath [simp, intro]: "valid_path (rectpath a b)"
eberlm@66393
   850
  by (simp add: Let_def rectpath_def)
eberlm@66393
   851
eberlm@66393
   852
lemma pathstart_rectpath [simp]: "pathstart (rectpath a1 a3) = a1"
eberlm@66393
   853
  by (simp add: rectpath_def Let_def)
eberlm@66393
   854
eberlm@66393
   855
lemma pathfinish_rectpath [simp]: "pathfinish (rectpath a1 a3) = a1"
eberlm@66393
   856
  by (simp add: rectpath_def Let_def)
eberlm@66393
   857
lp15@66827
   858
lemma simple_path_rectpath [simp, intro]:
eberlm@66393
   859
  assumes "Re a1 \<noteq> Re a3" "Im a1 \<noteq> Im a3"
eberlm@66393
   860
  shows   "simple_path (rectpath a1 a3)"
eberlm@66393
   861
  unfolding rectpath_def Let_def using assms
eberlm@66393
   862
  by (intro simple_path_join_loop arc_join arc_linepath)
eberlm@66393
   863
     (auto simp: complex_eq_iff path_image_join closed_segment_same_Re closed_segment_same_Im)
eberlm@66393
   864
lp15@66827
   865
lemma path_image_rectpath:
eberlm@66393
   866
  assumes "Re a1 \<le> Re a3" "Im a1 \<le> Im a3"
lp15@66827
   867
  shows "path_image (rectpath a1 a3) =
eberlm@66393
   868
           {z. Re z \<in> {Re a1, Re a3} \<and> Im z \<in> {Im a1..Im a3}} \<union>
eberlm@66393
   869
           {z. Im z \<in> {Im a1, Im a3} \<and> Re z \<in> {Re a1..Re a3}}" (is "?lhs = ?rhs")
eberlm@66393
   870
proof -
eberlm@66393
   871
  define a2 a4 where "a2 = Complex (Re a3) (Im a1)" and "a4 = Complex (Re a1) (Im a3)"
lp15@66827
   872
  have "?lhs = closed_segment a1 a2 \<union> closed_segment a2 a3 \<union>
eberlm@66393
   873
                  closed_segment a4 a3 \<union> closed_segment a1 a4"
eberlm@66393
   874
    by (simp_all add: rectpath_def Let_def path_image_join closed_segment_commute
eberlm@66393
   875
                      a2_def a4_def Un_assoc)
eberlm@66393
   876
  also have "\<dots> = ?rhs" using assms
eberlm@66393
   877
    by (auto simp: rectpath_def Let_def path_image_join a2_def a4_def
eberlm@66393
   878
          closed_segment_same_Re closed_segment_same_Im closed_segment_eq_real_ivl)
eberlm@66393
   879
  finally show ?thesis .
eberlm@66393
   880
qed
eberlm@66393
   881
eberlm@66393
   882
lemma path_image_rectpath_subset_cbox:
eberlm@66393
   883
  assumes "Re a \<le> Re b" "Im a \<le> Im b"
eberlm@66393
   884
  shows   "path_image (rectpath a b) \<subseteq> cbox a b"
eberlm@66393
   885
  using assms by (auto simp: path_image_rectpath in_cbox_complex_iff)
eberlm@66393
   886
eberlm@66393
   887
lemma path_image_rectpath_inter_box:
eberlm@66393
   888
  assumes "Re a \<le> Re b" "Im a \<le> Im b"
eberlm@66393
   889
  shows   "path_image (rectpath a b) \<inter> box a b = {}"
eberlm@66393
   890
  using assms by (auto simp: path_image_rectpath in_box_complex_iff)
eberlm@66393
   891
eberlm@66393
   892
lemma path_image_rectpath_cbox_minus_box:
eberlm@66393
   893
  assumes "Re a \<le> Re b" "Im a \<le> Im b"
eberlm@66393
   894
  shows   "path_image (rectpath a b) = cbox a b - box a b"
lp15@66827
   895
  using assms by (auto simp: path_image_rectpath in_cbox_complex_iff
eberlm@66393
   896
                             in_box_complex_iff)
eberlm@66393
   897
wl302@69423
   898
proposition winding_number_rectpath:
eberlm@66393
   899
  assumes "z \<in> box a1 a3"
eberlm@66393
   900
  shows   "winding_number (rectpath a1 a3) z = 1"
eberlm@66393
   901
proof -
eberlm@66393
   902
  from assms have less: "Re a1 < Re a3" "Im a1 < Im a3"
eberlm@66393
   903
    by (auto simp: in_box_complex_iff)
eberlm@66393
   904
  define a2 a4 where "a2 = Complex (Re a3) (Im a1)" and "a4 = Complex (Re a1) (Im a3)"
eberlm@66393
   905
  let ?l1 = "linepath a1 a2" and ?l2 = "linepath a2 a3"
eberlm@66393
   906
  and ?l3 = "linepath a3 a4" and ?l4 = "linepath a4 a1"
eberlm@66393
   907
  from assms and less have "z \<notin> path_image (rectpath a1 a3)"
eberlm@66393
   908
    by (auto simp: path_image_rectpath_cbox_minus_box)
lp15@66827
   909
  also have "path_image (rectpath a1 a3) =
eberlm@66393
   910
               path_image ?l1 \<union> path_image ?l2 \<union> path_image ?l3 \<union> path_image ?l4"
eberlm@66393
   911
    by (simp add: rectpath_def Let_def path_image_join Un_assoc a2_def a4_def)
eberlm@66393
   912
  finally have "z \<notin> \<dots>" .
eberlm@66393
   913
  moreover have "\<forall>l\<in>{?l1,?l2,?l3,?l4}. Re (winding_number l z) > 0"
eberlm@66393
   914
    unfolding ball_simps HOL.simp_thms a2_def a4_def
eberlm@66393
   915
    by (intro conjI; (rule winding_number_linepath_pos_lt;
eberlm@66393
   916
          (insert assms, auto simp: a2_def a4_def in_box_complex_iff mult_neg_neg))+)
eberlm@66393
   917
  ultimately have "Re (winding_number (rectpath a1 a3) z) > 0"
eberlm@66393
   918
    by (simp add: winding_number_join path_image_join rectpath_def Let_def a2_def a4_def)
eberlm@66393
   919
  thus "winding_number (rectpath a1 a3) z = 1" using assms less
eberlm@66393
   920
    by (intro simple_closed_path_winding_number_pos simple_path_rectpath)
eberlm@66393
   921
       (auto simp: path_image_rectpath_cbox_minus_box)
eberlm@66393
   922
qed
eberlm@66393
   923
wl302@69423
   924
proposition winding_number_rectpath_outside:
eberlm@66393
   925
  assumes "Re a1 \<le> Re a3" "Im a1 \<le> Im a3"
eberlm@66393
   926
  assumes "z \<notin> cbox a1 a3"
eberlm@66393
   927
  shows   "winding_number (rectpath a1 a3) z = 0"
lp15@66827
   928
  using assms by (intro winding_number_zero_outside[OF _ _ _ assms(3)]
eberlm@66393
   929
                     path_image_rectpath_subset_cbox) simp_all
eberlm@66393
   930
lp15@66826
   931
text\<open>A per-function version for continuous logs, a kind of monodromy\<close>
wl302@69423
   932
proposition%unimportant winding_number_compose_exp:
lp15@66826
   933
  assumes "path p"
lp15@66826
   934
  shows "winding_number (exp \<circ> p) 0 = (pathfinish p - pathstart p) / (2 * of_real pi * \<i>)"
lp15@66826
   935
proof -
lp15@66826
   936
  obtain e where "0 < e" and e: "\<And>t. t \<in> {0..1} \<Longrightarrow> e \<le> norm(exp(p t))"
lp15@66826
   937
  proof
lp15@69918
   938
    have "closed (path_image (exp \<circ> p))"
lp15@69918
   939
      by (simp add: assms closed_path_image holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image)
lp15@66826
   940
    then show "0 < setdist {0} (path_image (exp \<circ> p))"
lp15@69918
   941
      by (metis exp_not_eq_zero imageE image_comp infdist_eq_setdist infdist_pos_not_in_closed path_defs(4) path_image_nonempty)
lp15@66826
   942
  next
lp15@66826
   943
    fix t::real
lp15@66826
   944
    assume "t \<in> {0..1}"
lp15@66826
   945
    have "setdist {0} (path_image (exp \<circ> p)) \<le> dist 0 (exp (p t))"
lp15@66826
   946
      apply (rule setdist_le_dist)
lp15@66826
   947
      using \<open>t \<in> {0..1}\<close> path_image_def by fastforce+
lp15@66826
   948
    then show "setdist {0} (path_image (exp \<circ> p)) \<le> cmod (exp (p t))"
lp15@66826
   949
      by simp
lp15@66826
   950
  qed
lp15@66826
   951
  have "bounded (path_image p)"
lp15@66826
   952
    by (simp add: assms bounded_path_image)
lp15@66826
   953
  then obtain B where "0 < B" and B: "path_image p \<subseteq> cball 0 B"
lp15@66826
   954
    by (meson bounded_pos mem_cball_0 subsetI)
lp15@66826
   955
  let ?B = "cball (0::complex) (B+1)"
lp15@66826
   956
  have "uniformly_continuous_on ?B exp"
lp15@66826
   957
    using holomorphic_on_exp holomorphic_on_imp_continuous_on
lp15@66826
   958
    by (force intro: compact_uniformly_continuous)
lp15@66826
   959
  then obtain d where "d > 0"
lp15@66826
   960
        and d: "\<And>x x'. \<lbrakk>x\<in>?B; x'\<in>?B; dist x' x < d\<rbrakk> \<Longrightarrow> norm (exp x' - exp x) < e"
lp15@66826
   961
    using \<open>e > 0\<close> by (auto simp: uniformly_continuous_on_def dist_norm)
lp15@66826
   962
  then have "min 1 d > 0"
lp15@66826
   963
    by force
lp15@66826
   964
  then obtain g where pfg: "polynomial_function g"  and "g 0 = p 0" "g 1 = p 1"
lp15@66826
   965
           and gless: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm(g t - p t) < min 1 d"
lp15@66826
   966
    using path_approx_polynomial_function [OF \<open>path p\<close>] \<open>d > 0\<close> \<open>0 < e\<close>
lp15@66826
   967
    unfolding pathfinish_def pathstart_def by meson
lp15@66826
   968
  have "winding_number (exp \<circ> p) 0 = winding_number (exp \<circ> g) 0"
lp15@66826
   969
  proof (rule winding_number_nearby_paths_eq [symmetric])
lp15@66826
   970
    show "path (exp \<circ> p)" "path (exp \<circ> g)"
lp15@66826
   971
      by (simp_all add: pfg assms holomorphic_on_exp holomorphic_on_imp_continuous_on path_continuous_image path_polynomial_function)
lp15@66826
   972
  next
lp15@66826
   973
    fix t :: "real"
lp15@66826
   974
    assume t: "t \<in> {0..1}"
lp15@66826
   975
    with gless have "norm(g t - p t) < 1"
lp15@66826
   976
      using min_less_iff_conj by blast
lp15@66826
   977
    moreover have ptB: "norm (p t) \<le> B"
lp15@66826
   978
      using B t by (force simp: path_image_def)
lp15@66826
   979
    ultimately have "cmod (g t) \<le> B + 1"
lp15@66826
   980
      by (meson add_mono_thms_linordered_field(4) le_less_trans less_imp_le norm_triangle_sub)
lp15@66826
   981
    with ptB gless t have "cmod ((exp \<circ> g) t - (exp \<circ> p) t) < e"
lp15@66826
   982
      by (auto simp: dist_norm d)
lp15@66826
   983
    with e t show "cmod ((exp \<circ> g) t - (exp \<circ> p) t) < cmod ((exp \<circ> p) t - 0)"
lp15@66826
   984
      by fastforce
lp15@66826
   985
  qed (use \<open>g 0 = p 0\<close> \<open>g 1 = p 1\<close> in \<open>auto simp: pathfinish_def pathstart_def\<close>)
lp15@66826
   986
  also have "... = 1 / (of_real (2 * pi) * \<i>) * contour_integral (exp \<circ> g) (\<lambda>w. 1 / (w - 0))"
lp15@66826
   987
  proof (rule winding_number_valid_path)
lp15@66826
   988
    have "continuous_on (path_image g) (deriv exp)"
lp15@66826
   989
      by (metis DERIV_exp DERIV_imp_deriv continuous_on_cong holomorphic_on_exp holomorphic_on_imp_continuous_on)
lp15@66826
   990
    then show "valid_path (exp \<circ> g)"
lp15@66826
   991
      by (simp add: field_differentiable_within_exp pfg valid_path_compose valid_path_polynomial_function)
lp15@66826
   992
    show "0 \<notin> path_image (exp \<circ> g)"
lp15@66826
   993
      by (auto simp: path_image_def)
lp15@66826
   994
  qed
lp15@66826
   995
  also have "... = 1 / (of_real (2 * pi) * \<i>) * integral {0..1} (\<lambda>x. vector_derivative g (at x))"
lp15@66826
   996
  proof (simp add: contour_integral_integral, rule integral_cong)
lp15@66826
   997
    fix t :: "real"
lp15@66826
   998
    assume t: "t \<in> {0..1}"
lp15@66826
   999
    show "vector_derivative (exp \<circ> g) (at t) / exp (g t) = vector_derivative g (at t)"
lp15@66826
  1000
    proof (simp add: divide_simps, rule vector_derivative_unique_at)
lp15@66826
  1001
      show "(exp \<circ> g has_vector_derivative vector_derivative (exp \<circ> g) (at t)) (at t)"
lp15@66826
  1002
        by (meson DERIV_exp differentiable_def field_vector_diff_chain_at has_vector_derivative_def
lp15@66826
  1003
            has_vector_derivative_polynomial_function pfg vector_derivative_works)
lp15@66826
  1004
      show "(exp \<circ> g has_vector_derivative vector_derivative g (at t) * exp (g t)) (at t)"
lp15@66826
  1005
        apply (rule field_vector_diff_chain_at)
lp15@66826
  1006
        apply (metis has_vector_derivative_polynomial_function pfg vector_derivative_at)
lp15@66826
  1007
        using DERIV_exp has_field_derivative_def apply blast
lp15@66826
  1008
        done
lp15@66826
  1009
    qed
lp15@66826
  1010
  qed
lp15@66826
  1011
  also have "... = (pathfinish p - pathstart p) / (2 * of_real pi * \<i>)"
lp15@66826
  1012
  proof -
lp15@66826
  1013
    have "((\<lambda>x. vector_derivative g (at x)) has_integral g 1 - g 0) {0..1}"
lp15@66826
  1014
      apply (rule fundamental_theorem_of_calculus [OF zero_le_one])
lp15@66826
  1015
      by (metis has_vector_derivative_at_within has_vector_derivative_polynomial_function pfg vector_derivative_at)
lp15@66826
  1016
    then show ?thesis
lp15@66826
  1017
    apply (simp add: pathfinish_def pathstart_def)
lp15@66826
  1018
      using \<open>g 0 = p 0\<close> \<open>g 1 = p 1\<close> by auto
lp15@66826
  1019
  qed
lp15@66826
  1020
  finally show ?thesis .
lp15@66826
  1021
qed
lp15@66826
  1022
wl302@69423
  1023
subsection%unimportant \<open>The winding number defines a continuous logarithm for the path itself\<close>
lp15@66826
  1024
lp15@66826
  1025
lemma winding_number_as_continuous_log:
lp15@66826
  1026
  assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
lp15@66826
  1027
  obtains q where "path q"
lp15@66826
  1028
                  "pathfinish q - pathstart q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
lp15@66826
  1029
                  "\<And>t. t \<in> {0..1} \<Longrightarrow> p t = \<zeta> + exp(q t)"
lp15@66826
  1030
proof -
lp15@66826
  1031
  let ?q = "\<lambda>t. 2 * of_real pi * \<i> * winding_number(subpath 0 t p) \<zeta> + Ln(pathstart p - \<zeta>)"
lp15@66826
  1032
  show ?thesis
lp15@66826
  1033
  proof
lp15@66826
  1034
    have *: "continuous (at t within {0..1}) (\<lambda>x. winding_number (subpath 0 x p) \<zeta>)"
lp15@66826
  1035
      if t: "t \<in> {0..1}" for t
lp15@66826
  1036
    proof -
lp15@66826
  1037
      let ?B = "ball (p t) (norm(p t - \<zeta>))"
lp15@66826
  1038
      have "p t \<noteq> \<zeta>"
lp15@66826
  1039
        using path_image_def that \<zeta> by blast
lp15@66826
  1040
      then have "simply_connected ?B"
lp15@66826
  1041
        by (simp add: convex_imp_simply_connected)
lp15@66826
  1042
      then have "\<And>f::complex\<Rightarrow>complex. continuous_on ?B f \<and> (\<forall>\<zeta> \<in> ?B. f \<zeta> \<noteq> 0)
lp15@66826
  1043
                  \<longrightarrow> (\<exists>g. continuous_on ?B g \<and> (\<forall>\<zeta> \<in> ?B. f \<zeta> = exp (g \<zeta>)))"
lp15@66826
  1044
        by (simp add: simply_connected_eq_continuous_log)
lp15@66826
  1045
      moreover have "continuous_on ?B (\<lambda>w. w - \<zeta>)"
lp15@66826
  1046
        by (intro continuous_intros)
lp15@66826
  1047
      moreover have "(\<forall>z \<in> ?B. z - \<zeta> \<noteq> 0)"
lp15@66826
  1048
        by (auto simp: dist_norm)
lp15@66826
  1049
      ultimately obtain g where contg: "continuous_on ?B g"
lp15@66826
  1050
        and geq: "\<And>z. z \<in> ?B \<Longrightarrow> z - \<zeta> = exp (g z)" by blast
lp15@66826
  1051
      obtain d where "0 < d" and d:
lp15@66826
  1052
        "\<And>x. \<lbrakk>x \<in> {0..1}; dist x t < d\<rbrakk> \<Longrightarrow> dist (p x) (p t) < cmod (p t - \<zeta>)"
lp15@66826
  1053
        using \<open>path p\<close> t unfolding path_def continuous_on_iff
lp15@66826
  1054
        by (metis \<open>p t \<noteq> \<zeta>\<close> right_minus_eq zero_less_norm_iff)
lp15@66826
  1055
      have "((\<lambda>x. winding_number (\<lambda>w. subpath 0 x p w - \<zeta>) 0 -
lp15@66826
  1056
                  winding_number (\<lambda>w. subpath 0 t p w - \<zeta>) 0) \<longlongrightarrow> 0)
lp15@66826
  1057
            (at t within {0..1})"
lp15@66826
  1058
      proof (rule Lim_transform_within [OF _ \<open>d > 0\<close>])
lp15@66826
  1059
        have "continuous (at t within {0..1}) (g o p)"
lp15@68077
  1060
        proof (rule continuous_within_compose)
lp15@68077
  1061
          show "continuous (at t within {0..1}) p"
lp15@68077
  1062
            using \<open>path p\<close> continuous_on_eq_continuous_within path_def that by blast
lp15@68077
  1063
          show "continuous (at (p t) within p ` {0..1}) g"
lp15@68077
  1064
            by (metis (no_types, lifting) open_ball UNIV_I \<open>p t \<noteq> \<zeta>\<close> centre_in_ball contg continuous_on_eq_continuous_at continuous_within_topological right_minus_eq zero_less_norm_iff)
lp15@68077
  1065
        qed
lp15@66826
  1066
        with LIM_zero have "((\<lambda>u. (g (subpath t u p 1) - g (subpath t u p 0))) \<longlongrightarrow> 0) (at t within {0..1})"
lp15@66826
  1067
          by (auto simp: subpath_def continuous_within o_def)
lp15@66826
  1068
        then show "((\<lambda>u.  (g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>)) \<longlongrightarrow> 0)
lp15@66826
  1069
           (at t within {0..1})"
lp15@66826
  1070
          by (simp add: tendsto_divide_zero)
lp15@66826
  1071
        show "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>) =
lp15@66826
  1072
              winding_number (\<lambda>w. subpath 0 u p w - \<zeta>) 0 - winding_number (\<lambda>w. subpath 0 t p w - \<zeta>) 0"
lp15@66826
  1073
          if "u \<in> {0..1}" "0 < dist u t" "dist u t < d" for u
lp15@66826
  1074
        proof -
lp15@66826
  1075
          have "closed_segment t u \<subseteq> {0..1}"
lp15@66826
  1076
            using closed_segment_eq_real_ivl t that by auto
lp15@66826
  1077
          then have piB: "path_image(subpath t u p) \<subseteq> ?B"
lp15@66826
  1078
            apply (clarsimp simp add: path_image_subpath_gen)
lp15@66826
  1079
            by (metis subsetD le_less_trans \<open>dist u t < d\<close> d dist_commute dist_in_closed_segment)
lp15@66826
  1080
          have *: "path (g \<circ> subpath t u p)"
lp15@66826
  1081
            apply (rule path_continuous_image)
lp15@66826
  1082
            using \<open>path p\<close> t that apply auto[1]
lp15@66826
  1083
            using piB contg continuous_on_subset by blast
lp15@66826
  1084
          have "(g (subpath t u p 1) - g (subpath t u p 0)) / (2 * of_real pi * \<i>)
lp15@66826
  1085
              =  winding_number (exp \<circ> g \<circ> subpath t u p) 0"
lp15@66826
  1086
            using winding_number_compose_exp [OF *]
lp15@66826
  1087
            by (simp add: pathfinish_def pathstart_def o_assoc)
lp15@66826
  1088
          also have "... = winding_number (\<lambda>w. subpath t u p w - \<zeta>) 0"
lp15@66826
  1089
          proof (rule winding_number_cong)
lp15@66826
  1090
            have "exp(g y) = y - \<zeta>" if "y \<in> (subpath t u p) ` {0..1}" for y
lp15@66826
  1091
              by (metis that geq path_image_def piB subset_eq)
lp15@66826
  1092
            then show "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> (exp \<circ> g \<circ> subpath t u p) x = subpath t u p x - \<zeta>"
lp15@66826
  1093
              by auto
lp15@66826
  1094
          qed
lp15@66826
  1095
          also have "... = winding_number (\<lambda>w. subpath 0 u p w - \<zeta>) 0 -
lp15@66826
  1096
                           winding_number (\<lambda>w. subpath 0 t p w - \<zeta>) 0"
lp15@66826
  1097
            apply (simp add: winding_number_offset [symmetric])
lp15@66826
  1098
            using winding_number_subpath_combine [OF \<open>path p\<close> \<zeta>, of 0 t u] \<open>t \<in> {0..1}\<close> \<open>u \<in> {0..1}\<close>
lp15@66826
  1099
            by (simp add: add.commute eq_diff_eq)
lp15@66826
  1100
          finally show ?thesis .
lp15@66826
  1101
        qed
lp15@66826
  1102
      qed
lp15@66826
  1103
      then show ?thesis
lp15@66826
  1104
        by (subst winding_number_offset) (simp add: continuous_within LIM_zero_iff)
lp15@66826
  1105
    qed
lp15@66826
  1106
    show "path ?q"
lp15@66826
  1107
      unfolding path_def
lp15@66826
  1108
      by (intro continuous_intros) (simp add: continuous_on_eq_continuous_within *)
lp15@66826
  1109
lp15@66826
  1110
    have "\<zeta> \<noteq> p 0"
lp15@66826
  1111
      by (metis \<zeta> pathstart_def pathstart_in_path_image)
lp15@66826
  1112
    then show "pathfinish ?q - pathstart ?q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
lp15@66826
  1113
      by (simp add: pathfinish_def pathstart_def)
lp15@66826
  1114
    show "p t = \<zeta> + exp (?q t)" if "t \<in> {0..1}" for t
lp15@66826
  1115
    proof -
lp15@66826
  1116
      have "path (subpath 0 t p)"
lp15@66826
  1117
        using \<open>path p\<close> that by auto
lp15@66826
  1118
      moreover
lp15@66826
  1119
      have "\<zeta> \<notin> path_image (subpath 0 t p)"
lp15@66826
  1120
        using \<zeta> [unfolded path_image_def] that by (auto simp: path_image_subpath)
lp15@66826
  1121
      ultimately show ?thesis
lp15@66826
  1122
        using winding_number_exp_2pi [of "subpath 0 t p" \<zeta>] \<open>\<zeta> \<noteq> p 0\<close>
lp15@66826
  1123
        by (auto simp: exp_add algebra_simps pathfinish_def pathstart_def subpath_def)
lp15@66826
  1124
    qed
lp15@66826
  1125
  qed
lp15@66826
  1126
qed
lp15@66826
  1127
wl302@69423
  1128
subsection \<open>Winding number equality is the same as path/loop homotopy in C - {0}\<close>
lp15@66826
  1129
lp15@66826
  1130
lemma winding_number_homotopic_loops_null_eq:
lp15@66826
  1131
  assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
lp15@66826
  1132
  shows "winding_number p \<zeta> = 0 \<longleftrightarrow> (\<exists>a. homotopic_loops (-{\<zeta>}) p (\<lambda>t. a))"
lp15@66826
  1133
    (is "?lhs = ?rhs")
lp15@66826
  1134
proof
lp15@66826
  1135
  assume [simp]: ?lhs
lp15@66826
  1136
  obtain q where "path q"
lp15@66826
  1137
             and qeq:  "pathfinish q - pathstart q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
lp15@66826
  1138
             and peq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p t = \<zeta> + exp(q t)"
lp15@66826
  1139
    using winding_number_as_continuous_log [OF assms] by blast
lp15@66826
  1140
  have *: "homotopic_with (\<lambda>r. pathfinish r = pathstart r)
lp15@66826
  1141
                       {0..1} (-{\<zeta>}) ((\<lambda>w. \<zeta> + exp w) \<circ> q) ((\<lambda>w. \<zeta> + exp w) \<circ> (\<lambda>t. 0))"
lp15@66826
  1142
  proof (rule homotopic_with_compose_continuous_left)
lp15@66826
  1143
    show "homotopic_with (\<lambda>f. pathfinish ((\<lambda>w. \<zeta> + exp w) \<circ> f) = pathstart ((\<lambda>w. \<zeta> + exp w) \<circ> f))
lp15@66826
  1144
              {0..1} UNIV q (\<lambda>t. 0)"
lp15@66826
  1145
    proof (rule homotopic_with_mono, simp_all add: pathfinish_def pathstart_def)
lp15@66826
  1146
      have "homotopic_loops UNIV q (\<lambda>t. 0)"
lp15@66826
  1147
        by (rule homotopic_loops_linear) (use qeq \<open>path q\<close> in \<open>auto simp: continuous_on_const path_defs\<close>)
lp15@66826
  1148
      then show "homotopic_with (\<lambda>h. exp (h 1) = exp (h 0)) {0..1} UNIV q (\<lambda>t. 0)"
lp15@66826
  1149
        by (simp add: homotopic_loops_def homotopic_with_mono pathfinish_def pathstart_def)
lp15@66826
  1150
    qed
lp15@66826
  1151
    show "continuous_on UNIV (\<lambda>w. \<zeta> + exp w)"
lp15@66826
  1152
      by (rule continuous_intros)+
lp15@66826
  1153
    show "range (\<lambda>w. \<zeta> + exp w) \<subseteq> -{\<zeta>}"
lp15@66826
  1154
      by auto
lp15@66826
  1155
  qed
lp15@66826
  1156
  then have "homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} (-{\<zeta>}) p (\<lambda>x. \<zeta> + 1)"
lp15@66826
  1157
    by (rule homotopic_with_eq) (auto simp: o_def peq pathfinish_def pathstart_def)
lp15@66826
  1158
  then have "homotopic_loops (-{\<zeta>}) p (\<lambda>t. \<zeta> + 1)"
lp15@66826
  1159
    by (simp add: homotopic_loops_def)
lp15@66826
  1160
  then show ?rhs ..
lp15@66826
  1161
next
lp15@66826
  1162
  assume ?rhs
lp15@66826
  1163
  then obtain a where "homotopic_loops (-{\<zeta>}) p (\<lambda>t. a)" ..
lp15@66826
  1164
  then have "winding_number p \<zeta> = winding_number (\<lambda>t. a) \<zeta>" "a \<noteq> \<zeta>"
lp15@66826
  1165
    using winding_number_homotopic_loops homotopic_loops_imp_subset by (force simp:)+
lp15@66826
  1166
  moreover have "winding_number (\<lambda>t. a) \<zeta> = 0"
lp15@66826
  1167
    by (metis winding_number_zero_const \<open>a \<noteq> \<zeta>\<close>)
lp15@66826
  1168
  ultimately show ?lhs by metis
lp15@66826
  1169
qed
lp15@66826
  1170
lp15@66826
  1171
lemma winding_number_homotopic_paths_null_explicit_eq:
lp15@66826
  1172
  assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
lp15@66826
  1173
  shows "winding_number p \<zeta> = 0 \<longleftrightarrow> homotopic_paths (-{\<zeta>}) p (linepath (pathstart p) (pathstart p))"
lp15@66826
  1174
        (is "?lhs = ?rhs")
lp15@66826
  1175
proof
lp15@66826
  1176
  assume ?lhs
lp15@66826
  1177
  then show ?rhs
lp15@66826
  1178
    apply (auto simp: winding_number_homotopic_loops_null_eq [OF assms])
lp15@66826
  1179
    apply (rule homotopic_loops_imp_homotopic_paths_null)
lp15@66826
  1180
    apply (simp add: linepath_refl)
lp15@66826
  1181
    done
lp15@66826
  1182
next
lp15@66826
  1183
  assume ?rhs
lp15@66826
  1184
  then show ?lhs
lp15@66826
  1185
    by (metis \<zeta> pathstart_in_path_image winding_number_homotopic_paths winding_number_trivial)
lp15@66826
  1186
qed
lp15@66826
  1187
lp15@66826
  1188
lemma winding_number_homotopic_paths_null_eq:
lp15@66826
  1189
  assumes "path p" and \<zeta>: "\<zeta> \<notin> path_image p"
lp15@66826
  1190
  shows "winding_number p \<zeta> = 0 \<longleftrightarrow> (\<exists>a. homotopic_paths (-{\<zeta>}) p (\<lambda>t. a))"
lp15@66826
  1191
    (is "?lhs = ?rhs")
lp15@66826
  1192
proof
lp15@66826
  1193
  assume ?lhs
lp15@66826
  1194
  then show ?rhs
lp15@66826
  1195
    by (auto simp: winding_number_homotopic_paths_null_explicit_eq [OF assms] linepath_refl)
lp15@66826
  1196
next
lp15@66826
  1197
  assume ?rhs
lp15@66826
  1198
  then show ?lhs
lp15@66826
  1199
    by (metis \<zeta> homotopic_paths_imp_pathfinish pathfinish_def pathfinish_in_path_image winding_number_homotopic_paths winding_number_zero_const)
lp15@66826
  1200
qed
lp15@66826
  1201
wl302@69423
  1202
proposition winding_number_homotopic_paths_eq:
lp15@66826
  1203
  assumes "path p" and \<zeta>p: "\<zeta> \<notin> path_image p"
lp15@66826
  1204
      and "path q" and \<zeta>q: "\<zeta> \<notin> path_image q"
lp15@66826
  1205
      and qp: "pathstart q = pathstart p" "pathfinish q = pathfinish p"
lp15@66826
  1206
    shows "winding_number p \<zeta> = winding_number q \<zeta> \<longleftrightarrow> homotopic_paths (-{\<zeta>}) p q"
lp15@66826
  1207
    (is "?lhs = ?rhs")
lp15@66826
  1208
proof
lp15@66826
  1209
  assume ?lhs
lp15@66826
  1210
  then have "winding_number (p +++ reversepath q) \<zeta> = 0"
lp15@66826
  1211
    using assms by (simp add: winding_number_join winding_number_reversepath)
lp15@66826
  1212
  moreover
lp15@66826
  1213
  have "path (p +++ reversepath q)" "\<zeta> \<notin> path_image (p +++ reversepath q)"
lp15@66826
  1214
    using assms by (auto simp: not_in_path_image_join)
lp15@66826
  1215
  ultimately obtain a where "homotopic_paths (- {\<zeta>}) (p +++ reversepath q) (linepath a a)"
lp15@66826
  1216
    using winding_number_homotopic_paths_null_explicit_eq by blast
lp15@66826
  1217
  then show ?rhs
lp15@66826
  1218
    using homotopic_paths_imp_pathstart assms
lp15@66826
  1219
    by (fastforce simp add: dest: homotopic_paths_imp_homotopic_loops homotopic_paths_loop_parts)
lp15@66826
  1220
next
lp15@66826
  1221
  assume ?rhs
lp15@66826
  1222
  then show ?lhs
lp15@66826
  1223
    by (simp add: winding_number_homotopic_paths)
lp15@66826
  1224
qed
lp15@66826
  1225
lp15@66826
  1226
lemma winding_number_homotopic_loops_eq:
lp15@66826
  1227
  assumes "path p" and \<zeta>p: "\<zeta> \<notin> path_image p"
lp15@66826
  1228
      and "path q" and \<zeta>q: "\<zeta> \<notin> path_image q"
lp15@66826
  1229
      and loops: "pathfinish p = pathstart p" "pathfinish q = pathstart q"
lp15@66826
  1230
    shows "winding_number p \<zeta> = winding_number q \<zeta> \<longleftrightarrow> homotopic_loops (-{\<zeta>}) p q"
lp15@66826
  1231
    (is "?lhs = ?rhs")
lp15@66826
  1232
proof
lp15@66826
  1233
  assume L: ?lhs
lp15@66826
  1234
  have "pathstart p \<noteq> \<zeta>" "pathstart q \<noteq> \<zeta>"
lp15@66826
  1235
    using \<zeta>p \<zeta>q by blast+
lp15@66826
  1236
  moreover have "path_connected (-{\<zeta>})"
lp15@66826
  1237
    by (simp add: path_connected_punctured_universe)
lp15@66826
  1238
  ultimately obtain r where "path r" and rim: "path_image r \<subseteq> -{\<zeta>}"
lp15@66826
  1239
                        and pas: "pathstart r = pathstart p" and paf: "pathfinish r = pathstart q"
lp15@66826
  1240
    by (auto simp: path_connected_def)
lp15@66826
  1241
  then have "pathstart r \<noteq> \<zeta>" by blast
lp15@66826
  1242
  have "homotopic_loops (- {\<zeta>}) p (r +++ q +++ reversepath r)"
lp15@68077
  1243
  proof (rule homotopic_paths_imp_homotopic_loops)
lp15@68077
  1244
    show "homotopic_paths (- {\<zeta>}) p (r +++ q +++ reversepath r)"
lp15@68077
  1245
      by (metis (mono_tags, hide_lams) \<open>path r\<close> L \<zeta>p \<zeta>q \<open>path p\<close> \<open>path q\<close> homotopic_loops_conjugate loops not_in_path_image_join paf pas path_image_reversepath path_imp_reversepath path_join_eq pathfinish_join pathfinish_reversepath  pathstart_join pathstart_reversepath rim subset_Compl_singleton winding_number_homotopic_loops winding_number_homotopic_paths_eq)
lp15@68077
  1246
  qed (use loops pas in auto)
lp15@66826
  1247
  moreover have "homotopic_loops (- {\<zeta>}) (r +++ q +++ reversepath r) q"
lp15@66826
  1248
    using rim \<zeta>q by (auto simp: homotopic_loops_conjugate paf \<open>path q\<close> \<open>path r\<close> loops)
lp15@66826
  1249
  ultimately show ?rhs
lp15@66826
  1250
    using homotopic_loops_trans by metis
lp15@66826
  1251
next
lp15@66826
  1252
  assume ?rhs
lp15@66826
  1253
  then show ?lhs
lp15@66826
  1254
    by (simp add: winding_number_homotopic_loops)
lp15@66826
  1255
qed
lp15@66826
  1256
lp15@65039
  1257
end
lp15@65039
  1258