2128 done |
2130 done |
2129 qed |
2131 qed |
2130 qed |
2132 qed |
2131 qed |
2133 qed |
2132 |
2134 |
|
2135 subsection \<open>Cauchy's residue theorem\<close> |
|
2136 |
|
2137 text\<open>Wenda Li (2016)\<close> |
|
2138 |
|
2139 declare valid_path_imp_path [simp] |
|
2140 |
|
2141 lemma holomorphic_factor_zero_unique: |
|
2142 fixes f::"complex \<Rightarrow> complex" and z::complex and r::real |
|
2143 assumes "r>0" |
|
2144 and asm:"\<forall>w\<in>ball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0 \<and> f w = (w - z)^m * h w \<and> h w\<noteq>0" |
|
2145 and g_holo:"g holomorphic_on ball z r" and h_holo:"h holomorphic_on ball z r" |
|
2146 shows "n=m" |
|
2147 proof - |
|
2148 have "n>m \<Longrightarrow> False" |
|
2149 proof - |
|
2150 assume "n>m" |
|
2151 have "(h \<longlongrightarrow> 0) (at z within ball z r)" |
|
2152 proof (rule Lim_transform_within[OF _ `r>0`, where f="\<lambda>w. (w - z) ^ (n - m) * g w"]) |
|
2153 have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> h w = (w-z)^(n-m) * g w" using `n>m` asm |
|
2154 by (auto simp add:field_simps power_diff) |
|
2155 then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk> |
|
2156 \<Longrightarrow> (x' - z) ^ (n - m) * g x' = h x'" for x' by auto |
|
2157 next |
|
2158 def F\<equiv>"at z within ball z r" |
|
2159 and f'\<equiv>"\<lambda>x. (x - z) ^ (n-m)" |
|
2160 have "f' z=0" using `n>m` unfolding f'_def by auto |
|
2161 moreover have "continuous F f'" unfolding f'_def F_def |
|
2162 by (intro continuous_intros) |
|
2163 ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def |
|
2164 by (simp add: continuous_within) |
|
2165 moreover have "(g \<longlongrightarrow> g z) F" |
|
2166 using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] `r>0` |
|
2167 unfolding F_def by auto |
|
2168 ultimately show " ((\<lambda>w. f' w * g w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce |
|
2169 qed |
|
2170 moreover have "(h \<longlongrightarrow> h z) (at z within ball z r)" |
|
2171 using holomorphic_on_imp_continuous_on[OF h_holo] |
|
2172 by (auto simp add:continuous_on_def `r>0`) |
|
2173 moreover have "at z within ball z r \<noteq> bot" using `r>0` |
|
2174 by (auto simp add:trivial_limit_within islimpt_ball) |
|
2175 ultimately have "h z=0" by (auto intro: tendsto_unique) |
|
2176 thus False using asm `r>0` by auto |
|
2177 qed |
|
2178 moreover have "m>n \<Longrightarrow> False" |
|
2179 proof - |
|
2180 assume "m>n" |
|
2181 have "(g \<longlongrightarrow> 0) (at z within ball z r)" |
|
2182 proof (rule Lim_transform_within[OF _ `r>0`, where f="\<lambda>w. (w - z) ^ (m - n) * h w"]) |
|
2183 have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> g w = (w-z)^(m-n) * h w" using `m>n` asm |
|
2184 by (auto simp add:field_simps power_diff) |
|
2185 then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk> |
|
2186 \<Longrightarrow> (x' - z) ^ (m - n) * h x' = g x'" for x' by auto |
|
2187 next |
|
2188 def F\<equiv>"at z within ball z r" |
|
2189 and f'\<equiv>"\<lambda>x. (x - z) ^ (m-n)" |
|
2190 have "f' z=0" using `m>n` unfolding f'_def by auto |
|
2191 moreover have "continuous F f'" unfolding f'_def F_def |
|
2192 by (intro continuous_intros) |
|
2193 ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def |
|
2194 by (simp add: continuous_within) |
|
2195 moreover have "(h \<longlongrightarrow> h z) F" |
|
2196 using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] `r>0` |
|
2197 unfolding F_def by auto |
|
2198 ultimately show " ((\<lambda>w. f' w * h w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce |
|
2199 qed |
|
2200 moreover have "(g \<longlongrightarrow> g z) (at z within ball z r)" |
|
2201 using holomorphic_on_imp_continuous_on[OF g_holo] |
|
2202 by (auto simp add:continuous_on_def `r>0`) |
|
2203 moreover have "at z within ball z r \<noteq> bot" using `r>0` |
|
2204 by (auto simp add:trivial_limit_within islimpt_ball) |
|
2205 ultimately have "g z=0" by (auto intro: tendsto_unique) |
|
2206 thus False using asm `r>0` by auto |
|
2207 qed |
|
2208 ultimately show "n=m" by fastforce |
|
2209 qed |
|
2210 |
|
2211 lemma holomorphic_factor_zero_Ex1: |
|
2212 assumes "open s" "connected s" "z \<in> s" and |
|
2213 holo:"f holomorphic_on s" |
|
2214 and "f z = 0" and "\<exists>w\<in>s. f w \<noteq> 0" |
|
2215 shows "\<exists>!n. \<exists>g r. 0 < n \<and> 0 < r \<and> |
|
2216 g holomorphic_on cball z r |
|
2217 \<and> (\<forall>w\<in>cball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0)" |
|
2218 proof (rule ex_ex1I) |
|
2219 obtain g r n where "0 < n" "0 < r" "ball z r \<subseteq> s" and |
|
2220 g:"g holomorphic_on ball z r" |
|
2221 "\<And>w. w \<in> ball z r \<Longrightarrow> f w = (w - z) ^ n * g w" |
|
2222 "\<And>w. w \<in> ball z r \<Longrightarrow> g w \<noteq> 0" |
|
2223 using holomorphic_factor_zero_nonconstant[OF holo `open s` `connected s` `z\<in>s` `f z=0`] |
|
2224 by (metis assms(3) assms(5) assms(6)) |
|
2225 def r'\<equiv>"r/2" |
|
2226 have "cball z r' \<subseteq> ball z r" unfolding r'_def by (simp add: \<open>0 < r\<close> cball_subset_ball_iff) |
|
2227 hence "cball z r' \<subseteq> s" "g holomorphic_on cball z r'" |
|
2228 "(\<forall>w\<in>cball z r'. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)" |
|
2229 using g `ball z r \<subseteq> s` by auto |
|
2230 moreover have "r'>0" unfolding r'_def using `0<r` by auto |
|
2231 ultimately show "\<exists>n g r. 0 < n \<and> 0 < r \<and> g holomorphic_on cball z r |
|
2232 \<and> (\<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)" |
|
2233 apply (intro exI[of _ n] exI[of _ g] exI[of _ r']) |
|
2234 by (simp add:`0 < n`) |
|
2235 next |
|
2236 fix m n |
|
2237 def fac\<equiv>"\<lambda>n g r. \<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0" |
|
2238 assume n_asm:"\<exists>g r1. 0 < n \<and> 0 < r1 \<and> g holomorphic_on cball z r1 \<and> fac n g r1" |
|
2239 and m_asm:"\<exists>h r2. 0 < m \<and> 0 < r2 \<and> h holomorphic_on cball z r2 \<and> fac m h r2" |
|
2240 obtain g r1 where "0 < n" "0 < r1" and g_holo: "g holomorphic_on cball z r1" |
|
2241 and "fac n g r1" using n_asm by auto |
|
2242 obtain h r2 where "0 < m" "0 < r2" and h_holo: "h holomorphic_on cball z r2" |
|
2243 and "fac m h r2" using m_asm by auto |
|
2244 def r\<equiv>"min r1 r2" |
|
2245 have "r>0" using `r1>0` `r2>0` unfolding r_def by auto |
|
2246 moreover have "\<forall>w\<in>ball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0 \<and> f w = (w - z)^m * h w \<and> h w\<noteq>0" |
|
2247 using \<open>fac m h r2\<close> \<open>fac n g r1\<close> unfolding fac_def r_def |
|
2248 by fastforce |
|
2249 ultimately show "m=n" using g_holo h_holo |
|
2250 apply (elim holomorphic_factor_zero_unique[of r z f n g m h,symmetric,rotated]) |
|
2251 by (auto simp add:r_def) |
|
2252 qed |
|
2253 |
|
2254 lemma finite_ball_avoid: |
|
2255 assumes "open s" "finite pts" |
|
2256 shows "\<forall>p\<in>s. \<exists>e>0. \<forall>w\<in>ball p e. w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)" |
|
2257 proof |
|
2258 fix p assume "p\<in>s" |
|
2259 then obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> s" |
|
2260 using open_contains_ball_eq[OF `open s`] by auto |
|
2261 obtain e2 where "0<e2" and "\<forall>x\<in>pts. x \<noteq> p \<longrightarrow> e2 \<le> dist p x" |
|
2262 using finite_set_avoid[OF `finite pts`,of p] by auto |
|
2263 hence "\<forall>w\<in>ball p (min e1 e2). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)" using e1_b by auto |
|
2264 thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using `e2>0` `e1>0` |
|
2265 apply (rule_tac x="min e1 e2" in exI) |
|
2266 by auto |
|
2267 qed |
|
2268 |
|
2269 lemma finite_cball_avoid: |
|
2270 fixes s :: "'a :: euclidean_space set" |
|
2271 assumes "open s" "finite pts" |
|
2272 shows "\<forall>p\<in>s. \<exists>e>0. \<forall>w\<in>cball p e. w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)" |
|
2273 proof |
|
2274 fix p assume "p\<in>s" |
|
2275 then obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)" |
|
2276 using finite_ball_avoid[OF assms] by auto |
|
2277 def e2\<equiv>"e1/2" |
|
2278 have "e2>0" and "e2<e1" unfolding e2_def using `e1>0` by auto |
|
2279 then have "cball p e2 \<subseteq> ball p e1" by (subst cball_subset_ball_iff,auto) |
|
2280 then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using `e2>0` e1 by auto |
|
2281 qed |
|
2282 |
|
2283 lemma get_integrable_path: |
|
2284 assumes "open s" "connected (s-pts)" "finite pts" "f holomorphic_on (s-pts) " "a\<in>s-pts" "b\<in>s-pts" |
|
2285 obtains g where "valid_path g" "pathstart g = a" "pathfinish g = b" |
|
2286 "path_image g \<subseteq> s-pts" "f contour_integrable_on g" using assms |
|
2287 proof (induct arbitrary:s thesis a rule:finite_induct[OF `finite pts`]) print_cases |
|
2288 case 1 |
|
2289 obtain g where "valid_path g" "path_image g \<subseteq> s" "pathstart g = a" "pathfinish g = b" |
|
2290 using connected_open_polynomial_connected[OF `open s`,of a b ] `connected (s - {})` |
|
2291 valid_path_polynomial_function "1.prems"(6) "1.prems"(7) by auto |
|
2292 moreover have "f contour_integrable_on g" |
|
2293 using contour_integrable_holomorphic_simple[OF _ `open s` `valid_path g` `path_image g \<subseteq> s`,of f] |
|
2294 `f holomorphic_on s - {}` |
|
2295 by auto |
|
2296 ultimately show ?case using "1"(1)[of g] by auto |
|
2297 next |
|
2298 case idt:(2 p pts) |
|
2299 obtain e where "e>0" and e:"\<forall>w\<in>ball a e. w \<in> s \<and> (w \<noteq> a \<longrightarrow> w \<notin> insert p pts)" |
|
2300 using finite_ball_avoid[OF `open s` `finite (insert p pts)`,rule_format,of a] |
|
2301 `a \<in> s - insert p pts` |
|
2302 by auto |
|
2303 def a'\<equiv>"a+e/2" |
|
2304 have "a'\<in>s-{p} -pts" using e[rule_format,of "a+e/2"] `e>0` |
|
2305 by (auto simp add:dist_complex_def a'_def) |
|
2306 then obtain g' where g'[simp]:"valid_path g'" "pathstart g' = a'" "pathfinish g' = b" |
|
2307 "path_image g' \<subseteq> s - {p} - pts" "f contour_integrable_on g'" |
|
2308 using idt.hyps(3)[of a' "s-{p}"] idt.prems idt.hyps(1) |
|
2309 by (metis Diff_insert2 open_delete) |
|
2310 def g\<equiv>"linepath a a' +++ g'" |
|
2311 have "valid_path g" unfolding g_def by (auto intro: valid_path_join) |
|
2312 moreover have "pathstart g = a" and "pathfinish g = b" unfolding g_def by auto |
|
2313 moreover have "path_image g \<subseteq> s - insert p pts" unfolding g_def |
|
2314 proof (rule subset_path_image_join) |
|
2315 have "closed_segment a a' \<subseteq> ball a e" using `e>0` |
|
2316 by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute) |
|
2317 then show "path_image (linepath a a') \<subseteq> s - insert p pts" using e idt(9) |
|
2318 by auto |
|
2319 next |
|
2320 show "path_image g' \<subseteq> s - insert p pts" using g'(4) by blast |
|
2321 qed |
|
2322 moreover have "f contour_integrable_on g" |
|
2323 proof - |
|
2324 have "closed_segment a a' \<subseteq> ball a e" using `e>0` |
|
2325 by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute) |
|
2326 then have "continuous_on (closed_segment a a') f" |
|
2327 using e idt.prems(6) holomorphic_on_imp_continuous_on[OF idt.prems(5)] |
|
2328 apply (elim continuous_on_subset) |
|
2329 by auto |
|
2330 then have "f contour_integrable_on linepath a a'" |
|
2331 using contour_integrable_continuous_linepath by auto |
|
2332 then show ?thesis unfolding g_def |
|
2333 apply (rule contour_integrable_joinI) |
|
2334 by (auto simp add: `e>0`) |
|
2335 qed |
|
2336 ultimately show ?case using idt.prems(1)[of g] by auto |
|
2337 qed |
|
2338 |
|
2339 lemma Cauchy_theorem_aux: |
|
2340 assumes "open s" "connected (s-pts)" "finite pts" "pts \<subseteq> s" "f holomorphic_on s-pts" |
|
2341 "valid_path g" "pathfinish g = pathstart g" "path_image g \<subseteq> s-pts" |
|
2342 "\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" |
|
2343 "\<forall>p\<in>s. h p>0 \<and> (\<forall>w\<in>cball p (h p). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w \<notin> pts))" |
|
2344 shows "contour_integral g f = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)" |
|
2345 using assms |
|
2346 proof (induct arbitrary:s g rule:finite_induct[OF `finite pts`]) |
|
2347 case 1 |
|
2348 then show ?case by (simp add: Cauchy_theorem_global contour_integral_unique) |
|
2349 next |
|
2350 case (2 p pts) |
|
2351 note fin[simp] = `finite (insert p pts)` |
|
2352 and connected = `connected (s - insert p pts)` |
|
2353 and valid[simp] = `valid_path g` |
|
2354 and g_loop[simp] = `pathfinish g = pathstart g` |
|
2355 and holo[simp]= `f holomorphic_on s - insert p pts` |
|
2356 and path_img = `path_image g \<subseteq> s - insert p pts` |
|
2357 and winding = `\<forall>z. z \<notin> s \<longrightarrow> winding_number g z = 0` |
|
2358 and h = `\<forall>pa\<in>s. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s \<and> (w \<noteq> pa \<longrightarrow> w \<notin> insert p pts))` |
|
2359 have "h p>0" and "p\<in>s" |
|
2360 and h_p: "\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> insert p pts)" |
|
2361 using h `insert p pts \<subseteq> s` by auto |
|
2362 obtain pg where pg[simp]: "valid_path pg" "pathstart pg = pathstart g" "pathfinish pg=p+h p" |
|
2363 "path_image pg \<subseteq> s-insert p pts" "f contour_integrable_on pg" |
|
2364 proof - |
|
2365 have "p + h p\<in>cball p (h p)" using h[rule_format,of p] |
|
2366 by (simp add: \<open>p \<in> s\<close> dist_norm) |
|
2367 then have "p + h p \<in> s - insert p pts" using h[rule_format,of p] `insert p pts \<subseteq> s` |
|
2368 by fastforce |
|
2369 moreover have "pathstart g \<in> s - insert p pts " using path_img by auto |
|
2370 ultimately show ?thesis |
|
2371 using get_integrable_path[OF `open s` connected fin holo,of "pathstart g" "p+h p"] that |
|
2372 by blast |
|
2373 qed |
|
2374 obtain n::int where "n=winding_number g p" |
|
2375 using integer_winding_number[OF _ g_loop,of p] valid path_img |
|
2376 by (metis DiffD2 Ints_cases insertI1 subset_eq valid_path_imp_path) |
|
2377 def p_circ\<equiv>"circlepath p (h p)" and p_circ_pt\<equiv>"linepath (p+h p) (p+h p)" |
|
2378 def n_circ\<equiv>"\<lambda>n. (op +++ p_circ ^^ n) p_circ_pt" |
|
2379 def cp\<equiv>"if n\<ge>0 then reversepath (n_circ (nat n)) else n_circ (nat (- n))" |
|
2380 have n_circ:"valid_path (n_circ k)" |
|
2381 "winding_number (n_circ k) p = k" |
|
2382 "pathstart (n_circ k) = p + h p" "pathfinish (n_circ k) = p + h p" |
|
2383 "path_image (n_circ k) = (if k=0 then {p + h p} else sphere p (h p))" |
|
2384 "p \<notin> path_image (n_circ k)" |
|
2385 "\<And>p'. p'\<notin>s - pts \<Longrightarrow> winding_number (n_circ k) p'=0 \<and> p'\<notin>path_image (n_circ k)" |
|
2386 "f contour_integrable_on (n_circ k)" |
|
2387 "contour_integral (n_circ k) f = k * contour_integral p_circ f" |
|
2388 for k |
|
2389 proof (induct k) |
|
2390 case 0 |
|
2391 show "valid_path (n_circ 0)" |
|
2392 and "path_image (n_circ 0) = (if 0=0 then {p + h p} else sphere p (h p))" |
|
2393 and "winding_number (n_circ 0) p = of_nat 0" |
|
2394 and "pathstart (n_circ 0) = p + h p" |
|
2395 and "pathfinish (n_circ 0) = p + h p" |
|
2396 and "p \<notin> path_image (n_circ 0)" |
|
2397 unfolding n_circ_def p_circ_pt_def using `h p > 0` |
|
2398 by (auto simp add: dist_norm) |
|
2399 show "winding_number (n_circ 0) p'=0 \<and> p'\<notin>path_image (n_circ 0)" when "p'\<notin>s- pts" for p' |
|
2400 unfolding n_circ_def p_circ_pt_def |
|
2401 apply (auto intro!:winding_number_trivial) |
|
2402 by (metis Diff_iff pathfinish_in_path_image pg(3) pg(4) subsetCE subset_insertI that)+ |
|
2403 show "f contour_integrable_on (n_circ 0)" |
|
2404 unfolding n_circ_def p_circ_pt_def |
|
2405 by (auto intro!:contour_integrable_continuous_linepath simp add:continuous_on_sing) |
|
2406 show "contour_integral (n_circ 0) f = of_nat 0 * contour_integral p_circ f" |
|
2407 unfolding n_circ_def p_circ_pt_def by auto |
|
2408 next |
|
2409 case (Suc k) |
|
2410 have n_Suc:"n_circ (Suc k) = p_circ +++ n_circ k" unfolding n_circ_def by auto |
|
2411 have pcirc:"p \<notin> path_image p_circ" "valid_path p_circ" "pathfinish p_circ = pathstart (n_circ k)" |
|
2412 using Suc(3) unfolding p_circ_def using `h p > 0` by (auto simp add: p_circ_def) |
|
2413 have pcirc_image:"path_image p_circ \<subseteq> s - insert p pts" |
|
2414 proof - |
|
2415 have "path_image p_circ \<subseteq> cball p (h p)" using \<open>0 < h p\<close> p_circ_def by auto |
|
2416 then show ?thesis using h_p pcirc(1) by auto |
|
2417 qed |
|
2418 have pcirc_integrable:"f contour_integrable_on p_circ" |
|
2419 by (auto simp add:p_circ_def intro!: pcirc_image[unfolded p_circ_def] |
|
2420 contour_integrable_continuous_circlepath holomorphic_on_imp_continuous_on |
|
2421 holomorphic_on_subset[OF holo]) |
|
2422 show "valid_path (n_circ (Suc k))" |
|
2423 using valid_path_join[OF pcirc(2) Suc(1) pcirc(3)] unfolding n_circ_def by auto |
|
2424 show "path_image (n_circ (Suc k)) |
|
2425 = (if Suc k = 0 then {p + complex_of_real (h p)} else sphere p (h p))" |
|
2426 proof - |
|
2427 have "path_image p_circ = sphere p (h p)" |
|
2428 unfolding p_circ_def using \<open>0 < h p\<close> by auto |
|
2429 then show ?thesis unfolding n_Suc using Suc.hyps(5) `h p>0` |
|
2430 by (auto simp add: path_image_join[OF pcirc(3)] dist_norm) |
|
2431 qed |
|
2432 then show "p \<notin> path_image (n_circ (Suc k))" using `h p>0` by auto |
|
2433 show "winding_number (n_circ (Suc k)) p = of_nat (Suc k)" |
|
2434 proof - |
|
2435 have "winding_number p_circ p = 1" |
|
2436 by (simp add: `h p > 0` p_circ_def winding_number_circlepath_centre) |
|
2437 moreover have "p \<notin> path_image (n_circ k)" using Suc(5) `h p>0` by auto |
|
2438 then have "winding_number (p_circ +++ n_circ k) p |
|
2439 = winding_number p_circ p + winding_number (n_circ k) p" |
|
2440 using valid_path_imp_path Suc.hyps(1) Suc.hyps(2) pcirc |
|
2441 apply (intro winding_number_join) |
|
2442 by auto |
|
2443 ultimately show ?thesis using Suc(2) unfolding n_circ_def |
|
2444 by auto |
|
2445 qed |
|
2446 show "pathstart (n_circ (Suc k)) = p + h p" |
|
2447 by (simp add: n_circ_def p_circ_def) |
|
2448 show "pathfinish (n_circ (Suc k)) = p + h p" |
|
2449 using Suc(4) unfolding n_circ_def by auto |
|
2450 show "winding_number (n_circ (Suc k)) p'=0 \<and> p'\<notin>path_image (n_circ (Suc k))" when "p'\<notin>s-pts" for p' |
|
2451 proof - |
|
2452 have " p' \<notin> path_image p_circ" using \<open>p \<in> s\<close> h p_circ_def that using pcirc_image by blast |
|
2453 moreover have "p' \<notin> path_image (n_circ k)" |
|
2454 using Suc.hyps(7) that by blast |
|
2455 moreover have "winding_number p_circ p' = 0" |
|
2456 proof - |
|
2457 have "path_image p_circ \<subseteq> cball p (h p)" |
|
2458 using h unfolding p_circ_def using \<open>p \<in> s\<close> by fastforce |
|
2459 moreover have "p'\<notin>cball p (h p)" using \<open>p \<in> s\<close> h that "2.hyps"(2) by fastforce |
|
2460 ultimately show ?thesis unfolding p_circ_def |
|
2461 apply (intro winding_number_zero_outside) |
|
2462 by auto |
|
2463 qed |
|
2464 ultimately show ?thesis |
|
2465 unfolding n_Suc |
|
2466 apply (subst winding_number_join) |
|
2467 by (auto simp: pcirc Suc that not_in_path_image_join Suc.hyps(7)[OF that]) |
|
2468 qed |
|
2469 show "f contour_integrable_on (n_circ (Suc k))" |
|
2470 unfolding n_Suc |
|
2471 by (rule contour_integrable_joinI[OF pcirc_integrable Suc(8) pcirc(2) Suc(1)]) |
|
2472 show "contour_integral (n_circ (Suc k)) f = (Suc k) * contour_integral p_circ f" |
|
2473 unfolding n_Suc |
|
2474 by (auto simp add:contour_integral_join[OF pcirc_integrable Suc(8) pcirc(2) Suc(1)] |
|
2475 Suc(9) algebra_simps) |
|
2476 qed |
|
2477 have cp[simp]:"pathstart cp = p + h p" "pathfinish cp = p + h p" |
|
2478 "valid_path cp" "path_image cp \<subseteq> s - insert p pts" |
|
2479 "winding_number cp p = - n" |
|
2480 "\<And>p'. p'\<notin>s - pts \<Longrightarrow> winding_number cp p'=0 \<and> p' \<notin> path_image cp" |
|
2481 "f contour_integrable_on cp" |
|
2482 "contour_integral cp f = - n * contour_integral p_circ f" |
|
2483 proof - |
|
2484 show "pathstart cp = p + h p" and "pathfinish cp = p + h p" and "valid_path cp" |
|
2485 using n_circ unfolding cp_def by auto |
|
2486 next |
|
2487 have "sphere p (h p) \<subseteq> s - insert p pts" |
|
2488 using h[rule_format,of p] `insert p pts \<subseteq> s` by force |
|
2489 moreover have "p + complex_of_real (h p) \<in> s - insert p pts" |
|
2490 using pg(3) pg(4) by (metis pathfinish_in_path_image subsetCE) |
|
2491 ultimately show "path_image cp \<subseteq> s - insert p pts" unfolding cp_def |
|
2492 using n_circ(5) by auto |
|
2493 next |
|
2494 show "winding_number cp p = - n" |
|
2495 unfolding cp_def using winding_number_reversepath n_circ `h p>0` by auto |
|
2496 next |
|
2497 show "winding_number cp p'=0 \<and> p' \<notin> path_image cp" when "p'\<notin>s - pts" for p' |
|
2498 unfolding cp_def |
|
2499 apply (auto) |
|
2500 apply (subst winding_number_reversepath) |
|
2501 by (auto simp add: n_circ(7)[OF that] n_circ(1)) |
|
2502 next |
|
2503 show "f contour_integrable_on cp" unfolding cp_def |
|
2504 using contour_integrable_reversepath_eq n_circ(1,8) by auto |
|
2505 next |
|
2506 show "contour_integral cp f = - n * contour_integral p_circ f" |
|
2507 unfolding cp_def using contour_integral_reversepath[OF n_circ(1)] n_circ(9) |
|
2508 by auto |
|
2509 qed |
|
2510 def g'\<equiv>"g +++ pg +++ cp +++ (reversepath pg)" |
|
2511 have "contour_integral g' f = (\<Sum>p\<in>pts. winding_number g' p * contour_integral (circlepath p (h p)) f)" |
|
2512 proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ `finite pts` ]) |
|
2513 show "connected (s - {p} - pts)" using connected by (metis Diff_insert2) |
|
2514 show "open (s - {p})" using `open s` by auto |
|
2515 show " pts \<subseteq> s - {p}" using `insert p pts \<subseteq> s` ` p \<notin> pts` by blast |
|
2516 show "f holomorphic_on s - {p} - pts" using holo `p \<notin> pts` by (metis Diff_insert2) |
|
2517 show "valid_path g'" |
|
2518 unfolding g'_def cp_def using n_circ valid pg g_loop |
|
2519 by (auto intro!:valid_path_join ) |
|
2520 show "pathfinish g' = pathstart g'" |
|
2521 unfolding g'_def cp_def using pg(2) by simp |
|
2522 show "path_image g' \<subseteq> s - {p} - pts" |
|
2523 proof - |
|
2524 def s'\<equiv>"s - {p} - pts" |
|
2525 have s':"s' = s-insert p pts " unfolding s'_def by auto |
|
2526 then show ?thesis using path_img pg(4) cp(4) |
|
2527 unfolding g'_def |
|
2528 apply (fold s'_def s') |
|
2529 apply (intro subset_path_image_join) |
|
2530 by auto |
|
2531 qed |
|
2532 note path_join_imp[simp] |
|
2533 show "\<forall>z. z \<notin> s - {p} \<longrightarrow> winding_number g' z = 0" |
|
2534 proof clarify |
|
2535 fix z assume z:"z\<notin>s - {p}" |
|
2536 have "winding_number (g +++ pg +++ cp +++ reversepath pg) z = winding_number g z |
|
2537 + winding_number (pg +++ cp +++ (reversepath pg)) z" |
|
2538 proof (rule winding_number_join) |
|
2539 show "path g" using `valid_path g` by simp |
|
2540 show "z \<notin> path_image g" using z path_img by auto |
|
2541 show "path (pg +++ cp +++ reversepath pg)" using pg(3) cp by auto |
|
2542 next |
|
2543 have "path_image (pg +++ cp +++ reversepath pg) \<subseteq> s - insert p pts" |
|
2544 using pg(4) cp(4) by (auto simp:subset_path_image_join) |
|
2545 then show "z \<notin> path_image (pg +++ cp +++ reversepath pg)" using z by auto |
|
2546 next |
|
2547 show "pathfinish g = pathstart (pg +++ cp +++ reversepath pg)" using g_loop by auto |
|
2548 qed |
|
2549 also have "... = winding_number g z + (winding_number pg z |
|
2550 + winding_number (cp +++ (reversepath pg)) z)" |
|
2551 proof (subst add_left_cancel,rule winding_number_join) |
|
2552 show "path pg" and "path (cp +++ reversepath pg)" |
|
2553 and "pathfinish pg = pathstart (cp +++ reversepath pg)" by auto |
|
2554 show "z \<notin> path_image pg" using pg(4) z by blast |
|
2555 show "z \<notin> path_image (cp +++ reversepath pg)" using z |
|
2556 by (metis Diff_iff \<open>z \<notin> path_image pg\<close> contra_subsetD cp(4) insertI1 |
|
2557 not_in_path_image_join path_image_reversepath singletonD) |
|
2558 qed |
|
2559 also have "... = winding_number g z + (winding_number pg z |
|
2560 + (winding_number cp z + winding_number (reversepath pg) z))" |
|
2561 apply (auto intro!:winding_number_join ) |
|
2562 apply (metis Diff_iff contra_subsetD cp(4) insertI1 singletonD z) |
|
2563 by (metis Diff_insert2 Diff_subset contra_subsetD pg(4) z) |
|
2564 also have "... = winding_number g z + winding_number cp z" |
|
2565 apply (subst winding_number_reversepath) |
|
2566 apply auto |
|
2567 by (metis Diff_iff contra_subsetD insertI1 pg(4) singletonD z) |
|
2568 finally have "winding_number g' z = winding_number g z + winding_number cp z" |
|
2569 unfolding g'_def . |
|
2570 moreover have "winding_number g z + winding_number cp z = 0" |
|
2571 using winding z `n=winding_number g p` by auto |
|
2572 ultimately show "winding_number g' z = 0" unfolding g'_def by auto |
|
2573 qed |
|
2574 show "\<forall>pa\<in>s - {p}. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s - {p} \<and> (w \<noteq> pa \<longrightarrow> w \<notin> pts))" |
|
2575 using h by fastforce |
|
2576 qed |
|
2577 moreover have "contour_integral g' f = contour_integral g f |
|
2578 - winding_number g p * contour_integral p_circ f" |
|
2579 proof - |
|
2580 have "contour_integral g' f = contour_integral g f |
|
2581 + contour_integral (pg +++ cp +++ reversepath pg) f" |
|
2582 unfolding g'_def |
|
2583 apply (subst Cauchy_Integral_Thm.contour_integral_join) |
|
2584 by (auto simp add:open_Diff[OF `open s`,OF finite_imp_closed[OF fin]] |
|
2585 intro!: contour_integrable_holomorphic_simple[OF holo _ _ path_img] |
|
2586 contour_integrable_reversepath) |
|
2587 also have "... = contour_integral g f + contour_integral pg f |
|
2588 + contour_integral (cp +++ reversepath pg) f" |
|
2589 apply (subst Cauchy_Integral_Thm.contour_integral_join) |
|
2590 by (auto simp add:contour_integrable_reversepath) |
|
2591 also have "... = contour_integral g f + contour_integral pg f |
|
2592 + contour_integral cp f + contour_integral (reversepath pg) f" |
|
2593 apply (subst Cauchy_Integral_Thm.contour_integral_join) |
|
2594 by (auto simp add:contour_integrable_reversepath) |
|
2595 also have "... = contour_integral g f + contour_integral cp f" |
|
2596 using contour_integral_reversepath |
|
2597 by (auto simp add:contour_integrable_reversepath) |
|
2598 also have "... = contour_integral g f - winding_number g p * contour_integral p_circ f" |
|
2599 using `n=winding_number g p` by auto |
|
2600 finally show ?thesis . |
|
2601 qed |
|
2602 moreover have "winding_number g' p' = winding_number g p'" when "p'\<in>pts" for p' |
|
2603 proof - |
|
2604 have [simp]: "p' \<notin> path_image g" "p' \<notin> path_image pg" "p'\<notin>path_image cp" |
|
2605 using "2.prems"(8) that |
|
2606 apply blast |
|
2607 apply (metis Diff_iff Diff_insert2 contra_subsetD pg(4) that) |
|
2608 by (meson DiffD2 cp(4) set_rev_mp subset_insertI that) |
|
2609 have "winding_number g' p' = winding_number g p' |
|
2610 + winding_number (pg +++ cp +++ reversepath pg) p'" unfolding g'_def |
|
2611 apply (subst winding_number_join) |
|
2612 apply simp_all |
|
2613 apply (intro not_in_path_image_join) |
|
2614 by auto |
|
2615 also have "... = winding_number g p' + winding_number pg p' |
|
2616 + winding_number (cp +++ reversepath pg) p'" |
|
2617 apply (subst winding_number_join) |
|
2618 apply simp_all |
|
2619 apply (intro not_in_path_image_join) |
|
2620 by auto |
|
2621 also have "... = winding_number g p' + winding_number pg p'+ winding_number cp p' |
|
2622 + winding_number (reversepath pg) p'" |
|
2623 apply (subst winding_number_join) |
|
2624 by simp_all |
|
2625 also have "... = winding_number g p' + winding_number cp p'" |
|
2626 apply (subst winding_number_reversepath) |
|
2627 by auto |
|
2628 also have "... = winding_number g p'" using that by auto |
|
2629 finally show ?thesis . |
|
2630 qed |
|
2631 ultimately show ?case unfolding p_circ_def |
|
2632 apply (subst (asm) setsum.cong[OF refl, |
|
2633 of pts _ "\<lambda>p. winding_number g p * contour_integral (circlepath p (h p)) f"]) |
|
2634 by (auto simp add:setsum.insert[OF `finite pts` `p\<notin>pts`] algebra_simps) |
|
2635 qed |
|
2636 |
|
2637 |
|
2638 lemma Cauchy_theorem_singularities: |
|
2639 assumes "open s" "connected (s-pts)" "finite pts" and |
|
2640 holo:"f holomorphic_on s-pts" and |
|
2641 "valid_path g" and |
|
2642 loop:"pathfinish g = pathstart g" and |
|
2643 "path_image g \<subseteq> s-pts" and |
|
2644 homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and |
|
2645 avoid:"\<forall>p\<in>s. h p>0 \<and> (\<forall>w\<in>cball p (h p). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w \<notin> pts))" |
|
2646 shows "contour_integral g f = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)" |
|
2647 (is "?L=?R") |
|
2648 proof - |
|
2649 def circ\<equiv>"\<lambda>p. winding_number g p * contour_integral (circlepath p (h p)) f" |
|
2650 def pts1\<equiv>"pts \<inter> s" |
|
2651 def pts2\<equiv>"pts - pts1" |
|
2652 have "pts=pts1 \<union> pts2" "pts1 \<inter> pts2 = {}" "pts2 \<inter> s={}" "pts1\<subseteq>s" |
|
2653 unfolding pts1_def pts2_def by auto |
|
2654 have "contour_integral g f = (\<Sum>p\<in>pts1. circ p)" unfolding circ_def |
|
2655 proof (rule Cauchy_theorem_aux[OF `open s` _ _ `pts1\<subseteq>s` _ `valid_path g` loop _ homo]) |
|
2656 show "connected (s - pts1)" by (metis Diff_Int2 Int_absorb assms(2) pts1_def) |
|
2657 show "finite pts1" using \<open>pts = pts1 \<union> pts2\<close> assms(3) by auto |
|
2658 show "f holomorphic_on s - pts1" by (metis Diff_Int2 Int_absorb holo pts1_def) |
|
2659 show "path_image g \<subseteq> s - pts1" using assms(7) pts1_def by auto |
|
2660 show "\<forall>p\<in>s. 0 < h p \<and> (\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts1))" |
|
2661 by (simp add: avoid pts1_def) |
|
2662 qed |
|
2663 moreover have "setsum circ pts2=0" |
|
2664 proof - |
|
2665 have "winding_number g p=0" when "p\<in>pts2" for p |
|
2666 using `pts2 \<inter> s={}` that homo[rule_format,of p] by auto |
|
2667 thus ?thesis unfolding circ_def |
|
2668 apply (intro setsum.neutral) |
|
2669 by auto |
|
2670 qed |
|
2671 moreover have "?R=setsum circ pts1 + setsum circ pts2" |
|
2672 unfolding circ_def |
|
2673 using setsum.union_disjoint[OF _ _ `pts1 \<inter> pts2 = {}`] `finite pts` `pts=pts1 \<union> pts2` |
|
2674 by blast |
|
2675 ultimately show ?thesis |
|
2676 apply (fold circ_def) |
|
2677 by auto |
|
2678 qed |
|
2679 |
|
2680 |
|
2681 |
|
2682 |
|
2683 (*order of the zero of f at z*) |
|
2684 definition zorder::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> nat" where |
|
2685 "zorder f z = (THE n. n>0 \<and> (\<exists>h r. r>0 \<and> h holomorphic_on cball z r |
|
2686 \<and> (\<forall>w\<in>cball z r. f w = h w * (w-z)^n \<and> h w \<noteq>0)))" |
|
2687 |
|
2688 definition zer_poly::"[complex \<Rightarrow> complex,complex]\<Rightarrow>complex \<Rightarrow> complex" where |
|
2689 "zer_poly f z = (SOME h. \<exists>r . r>0 \<and> h holomorphic_on cball z r |
|
2690 \<and> (\<forall>w\<in>cball z r. f w = h w * (w-z)^(zorder f z) \<and> h w \<noteq>0))" |
|
2691 |
|
2692 (*order of the pole of f at z*) |
|
2693 definition porder::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> nat" where |
|
2694 "porder f z = zorder (inverse o f) z" |
|
2695 |
|
2696 definition pol_poly::"[complex \<Rightarrow> complex,complex]\<Rightarrow>complex \<Rightarrow> complex" where |
|
2697 "pol_poly f z = inverse o zer_poly (inverse o f) z" |
|
2698 |
|
2699 definition residue::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where |
|
2700 "residue f z = (let n=porder f z;h=pol_poly f z in (deriv ^^ (n - 1)) h z / fact (n-1))" |
|
2701 |
|
2702 definition is_pole:: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow>bool" where |
|
2703 "is_pole f p \<equiv> isCont (inverse o f) p \<and> f p = 0" |
|
2704 |
|
2705 |
|
2706 lemma zorder_exist: |
|
2707 fixes f::"complex \<Rightarrow> complex" and z::complex |
|
2708 defines "n\<equiv>zorder f z" and "h\<equiv>zer_poly f z" |
|
2709 assumes "open s" "connected s" "z\<in>s" |
|
2710 and holo: "f holomorphic_on s" |
|
2711 and "f z=0" "\<exists>w\<in>s. f w\<noteq>0" |
|
2712 shows "\<exists>r. n>0 \<and> r>0 \<and> cball z r \<subseteq> s \<and> h holomorphic_on cball z r |
|
2713 \<and> (\<forall>w\<in>cball z r. f w = h w * (w-z)^n \<and> h w \<noteq>0) " |
|
2714 proof - |
|
2715 def P\<equiv>"\<lambda>h r n. r>0 \<and> h holomorphic_on cball z r |
|
2716 \<and> (\<forall>w\<in>cball z r. ( f w = h w * (w-z)^n) \<and> h w \<noteq>0)" |
|
2717 have "(\<exists>!n. n>0 \<and> (\<exists> h r. P h r n))" |
|
2718 proof - |
|
2719 have "\<exists>!n. \<exists>h r. n>0 \<and> P h r n" |
|
2720 using holomorphic_factor_zero_Ex1[OF `open s` `connected s` `z\<in>s` holo `f z=0` |
|
2721 `\<exists>w\<in>s. f w\<noteq>0`] unfolding P_def |
|
2722 apply (subst mult.commute) |
|
2723 by auto |
|
2724 thus ?thesis by auto |
|
2725 qed |
|
2726 moreover have n:"n=(THE n. n>0 \<and> (\<exists>h r. P h r n))" |
|
2727 unfolding n_def zorder_def P_def by simp |
|
2728 ultimately have "n>0 \<and> (\<exists>h r. P h r n)" |
|
2729 apply (drule_tac theI') |
|
2730 by simp |
|
2731 then have "n>0" and "\<exists>h r. P h r n" by auto |
|
2732 moreover have "h=(SOME h. \<exists>r. P h r n)" |
|
2733 unfolding h_def P_def zer_poly_def[of f z,folded n_def P_def] by simp |
|
2734 ultimately have "\<exists>r. P h r n" |
|
2735 apply (drule_tac someI_ex) |
|
2736 by simp |
|
2737 then obtain r1 where "P h r1 n" by auto |
|
2738 obtain r2 where "r2>0" "cball z r2 \<subseteq> s" |
|
2739 using assms(3) assms(5) open_contains_cball_eq by blast |
|
2740 def r3\<equiv>"min r1 r2" |
|
2741 have "P h r3 n" using `P h r1 n` `r2>0` unfolding P_def r3_def |
|
2742 by auto |
|
2743 moreover have "cball z r3 \<subseteq> s" using `cball z r2 \<subseteq> s` unfolding r3_def by auto |
|
2744 ultimately show ?thesis using `n>0` unfolding P_def by auto |
|
2745 qed |
|
2746 |
|
2747 lemma porder_exist: |
|
2748 fixes f::"complex \<Rightarrow> complex" and z::complex |
|
2749 defines "n\<equiv>porder f z" and "h\<equiv>pol_poly f z" |
|
2750 assumes "open s" "connected s" "z\<in>s" |
|
2751 and holo:"(inverse o f) holomorphic_on s" |
|
2752 and "f z=0" "\<exists>w\<in>s. f w\<noteq>0" |
|
2753 shows "\<exists>r. n>0 \<and> r>0 \<and> cball z r \<subseteq> s \<and> h holomorphic_on cball z r |
|
2754 \<and> (\<forall>w\<in>cball z r. f w = h w / (w-z)^n \<and> h w \<noteq>0)" |
|
2755 proof - |
|
2756 def zo\<equiv>"zorder (inverse \<circ> f) z" and zp\<equiv>"zer_poly (inverse \<circ> f) z" |
|
2757 obtain r where "0 < zo" "0 < r" "cball z r \<subseteq> s" and zp_holo: "zp holomorphic_on cball z r" and |
|
2758 zp_fac: "\<forall>w\<in>cball z r. (inverse \<circ> f) w = zp w * (w - z) ^ zo \<and> zp w \<noteq> 0" |
|
2759 using zorder_exist[OF `open s` `connected s` `z\<in>s` holo,folded zo_def zp_def] |
|
2760 `f z=0` `\<exists>w\<in>s. f w\<noteq>0` |
|
2761 by auto |
|
2762 have n:"n=zo" and h:"h=inverse o zp" |
|
2763 unfolding n_def zo_def porder_def h_def zp_def pol_poly_def by simp_all |
|
2764 have "h holomorphic_on cball z r" |
|
2765 using zp_holo zp_fac holomorphic_on_inverse unfolding h comp_def by blast |
|
2766 moreover have "\<forall>w\<in>cball z r. f w = h w / (w-z)^n \<and> h w \<noteq>0" |
|
2767 using zp_fac unfolding h n comp_def |
|
2768 by (metis divide_inverse_commute field_class.field_inverse_zero inverse_inverse_eq |
|
2769 inverse_mult_distrib mult.commute) |
|
2770 moreover have "0 < n" unfolding n using `zo>0` by simp |
|
2771 ultimately show ?thesis using `0 < r` `cball z r \<subseteq> s` by auto |
|
2772 qed |
|
2773 |
|
2774 lemma base_residue: |
|
2775 fixes f::"complex \<Rightarrow> complex" and z::complex |
|
2776 assumes "open s" "connected s" "z\<in>s" |
|
2777 and holo: "(inverse o f) holomorphic_on s" |
|
2778 and "f z=0" |
|
2779 and non_c:"\<exists>w\<in>s. f w\<noteq>0" |
|
2780 shows "\<exists>r>0. cball z r \<subseteq> s |
|
2781 \<and> (f has_contour_integral complex_of_real (2 * pi) * \<i> * residue f z) (circlepath z r)" |
|
2782 proof - |
|
2783 def n\<equiv>"porder f z" and h\<equiv>"pol_poly f z" |
|
2784 obtain r where "n>0" "0 < r" and |
|
2785 r_b:"cball z r \<subseteq> s" and |
|
2786 h_holo:"h holomorphic_on cball z r" |
|
2787 and h:"(\<forall>w\<in>cball z r. f w = h w / (w - z) ^ n \<and> h w \<noteq> 0)" |
|
2788 using porder_exist[OF `open s` `connected s` `z\<in>s` holo `f z=0` non_c] |
|
2789 unfolding n_def h_def by auto |
|
2790 def c\<equiv>"complex_of_real (2 * pi) * \<i>" |
|
2791 have "residue f z = (deriv ^^ (n - 1)) h z / fact (n-1)" |
|
2792 unfolding residue_def |
|
2793 apply (fold n_def h_def) |
|
2794 by simp |
|
2795 then have "((\<lambda>u. h u / (u - z) ^ n) has_contour_integral c * residue f z) |
|
2796 (circlepath z r)" |
|
2797 using Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n -1" |
|
2798 ,unfolded Suc_diff_1[OF `n>0`],folded c_def] h_holo r_b |
|
2799 by (auto simp add:`r>0` holomorphic_on_imp_continuous_on holomorphic_on_subset) |
|
2800 then have "(f has_contour_integral c * residue f z) (circlepath z r)" |
|
2801 proof (elim has_contour_integral_eq) |
|
2802 fix x assume "x \<in> path_image (circlepath z r)" |
|
2803 hence "x\<in>cball z r" using \<open>0 < r\<close> by auto |
|
2804 then show "h x / (x - z) ^ n = f x" using h by auto |
|
2805 qed |
|
2806 then show ?thesis using `r>0` `cball z r \<subseteq> s` unfolding c_def by auto |
|
2807 qed |
|
2808 |
|
2809 theorem residue_theorem: |
|
2810 assumes "open s" "connected (s-poles)" and |
|
2811 holo:"f holomorphic_on s-poles" and |
|
2812 "valid_path \<gamma>" and |
|
2813 loop:"pathfinish \<gamma> = pathstart \<gamma>" and |
|
2814 "path_image \<gamma> \<subseteq> s-poles" and |
|
2815 homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number \<gamma> z = 0" and |
|
2816 "finite {p. f p=0}" and |
|
2817 poles:"\<forall>p\<in>poles. is_pole f p" |
|
2818 shows "contour_integral \<gamma> f = 2 * pi * \<i> *(\<Sum>p\<in>poles. winding_number \<gamma> p * residue f p)" |
|
2819 proof - |
|
2820 def pts\<equiv>"{p. f p=0}" |
|
2821 def c\<equiv>"2 * complex_of_real pi * \<i> " |
|
2822 def contour\<equiv>"\<lambda>p e. (f has_contour_integral c * residue f p) (circlepath p e)" |
|
2823 def avoid\<equiv>"\<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" |
|
2824 have "poles \<subseteq> pts" and "finite pts" |
|
2825 using poles `finite {p. f p=0}` unfolding pts_def is_pole_def by auto |
|
2826 have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> contour p e)" |
|
2827 when "p\<in>s" for p |
|
2828 proof - |
|
2829 obtain e1 where e:"e1>0" and e:"avoid p e1" |
|
2830 using finite_cball_avoid[OF `open s` `finite pts`] `p\<in>s` unfolding avoid_def by auto |
|
2831 have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> contour p e2" |
|
2832 when "p\<in>poles" unfolding c_def contour_def |
|
2833 proof (rule base_residue[of "ball p e1" p f,simplified,OF `e1>0`]) |
|
2834 show "inverse \<circ> f holomorphic_on ball p e1" |
|
2835 proof - |
|
2836 def f'\<equiv>"inverse o f" |
|
2837 have "f holomorphic_on ball p e1 - {p}" |
|
2838 using holo e `poles \<subseteq> pts` unfolding avoid_def |
|
2839 apply (elim holomorphic_on_subset) |
|
2840 by auto |
|
2841 then have f'_holo:"f' holomorphic_on ball p e1 - {p}" unfolding f'_def comp_def |
|
2842 apply (elim holomorphic_on_inverse) |
|
2843 using e pts_def ball_subset_cball unfolding avoid_def by blast |
|
2844 moreover have "isCont f' p" using `p\<in>poles` poles unfolding f'_def is_pole_def by auto |
|
2845 ultimately show "f' holomorphic_on ball p e1" |
|
2846 apply (elim no_isolated_singularity[rotated]) |
|
2847 apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified]) |
|
2848 using field_differentiable_imp_continuous_at f'_holo |
|
2849 holomorphic_on_imp_differentiable_at by fastforce |
|
2850 qed |
|
2851 next |
|
2852 show "f p = 0" using `p\<in>poles` poles unfolding is_pole_def by auto |
|
2853 next |
|
2854 def p'\<equiv>"p+e1/2" |
|
2855 have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm) |
|
2856 then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def |
|
2857 apply (rule_tac x=p' in bexI) |
|
2858 by (auto simp add:pts_def) |
|
2859 qed |
|
2860 then obtain e2 where e2:"p\<in>poles \<longrightarrow> e2>0 \<and> cball p e2 \<subseteq> ball p e1 \<and> contour p e2" by auto |
|
2861 def e3\<equiv>"if p\<in>poles then e2 else e1" |
|
2862 have "avoid p e3" |
|
2863 using e2 e that avoid_def e3_def by auto |
|
2864 moreover have "e3>0" using `e1>0` e2 unfolding e3_def by auto |
|
2865 moreover have " p\<in>poles \<longrightarrow> contour p e3" using e2 unfolding e3_def by auto |
|
2866 ultimately show ?thesis by auto |
|
2867 qed |
|
2868 then obtain h where h:"\<forall>p\<in>s. h p>0 \<and> (avoid p (h p) \<and> (p\<in>poles \<longrightarrow> contour p (h p)))" |
|
2869 by metis |
|
2870 def cont\<equiv>"\<lambda>p. contour_integral (circlepath p (h p)) f" |
|
2871 have "contour_integral \<gamma> f = (\<Sum>p\<in>poles. winding_number \<gamma> p * cont p)" |
|
2872 unfolding cont_def |
|
2873 proof (rule Cauchy_theorem_singularities[OF `open s` `connected (s-poles)` _ holo `valid_path \<gamma>` |
|
2874 loop `path_image \<gamma> \<subseteq> s-poles` homo]) |
|
2875 show "finite poles" using `poles \<subseteq> pts` and `finite pts` by (simp add: finite_subset) |
|
2876 next |
|
2877 show "\<forall>p\<in>s. 0 < h p \<and> (\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> poles))" |
|
2878 using `poles \<subseteq> pts` h unfolding avoid_def by blast |
|
2879 qed |
|
2880 also have "... = (\<Sum>p\<in>poles. c * (winding_number \<gamma> p * residue f p))" |
|
2881 proof (rule setsum.cong[of poles poles,simplified]) |
|
2882 fix p assume "p \<in> poles" |
|
2883 show "winding_number \<gamma> p * cont p = c * (winding_number \<gamma> p * residue f p)" |
|
2884 proof (cases "p\<in>s") |
|
2885 assume "p \<in> s" |
|
2886 then have "cont p=c*residue f p" |
|
2887 unfolding cont_def |
|
2888 apply (intro contour_integral_unique) |
|
2889 using h[unfolded contour_def] `p \<in> poles` by blast |
|
2890 then show ?thesis by auto |
|
2891 next |
|
2892 assume "p\<notin>s" |
|
2893 then have "winding_number \<gamma> p=0" using homo by auto |
|
2894 then show ?thesis by auto |
|
2895 qed |
|
2896 qed |
|
2897 also have "... = c * (\<Sum>p\<in>poles. winding_number \<gamma> p * residue f p)" |
|
2898 apply (subst setsum_right_distrib) |
|
2899 by simp |
|
2900 finally show ?thesis unfolding c_def by auto |
|
2901 qed |
|
2902 |
|
2903 theorem argument_principle: |
|
2904 fixes f::"complex \<Rightarrow> complex" and poles s:: "complex set" |
|
2905 defines "pts\<equiv>{p. f p=0}" |
|
2906 defines "zeros\<equiv>pts - poles" |
|
2907 assumes "open s" and |
|
2908 connected:"connected (s- pts)" and |
|
2909 f_holo:"f holomorphic_on s-poles" and |
|
2910 h_holo:"h holomorphic_on s" and |
|
2911 "valid_path g" and |
|
2912 loop:"pathfinish g = pathstart g" and |
|
2913 path_img:"path_image g \<subseteq> s - pts" and |
|
2914 homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and |
|
2915 finite:"finite pts" and |
|
2916 poles:"\<forall>p\<in>poles. is_pole f p" |
|
2917 shows "contour_integral g (\<lambda>x. deriv f x * h x / f x) = 2 * pi * \<i> * |
|
2918 ((\<Sum>p\<in>zeros. winding_number g p * h p * zorder f p) |
|
2919 - (\<Sum>p\<in>poles. winding_number g p * h p * porder f p))" |
|
2920 (is "?L=?R") |
|
2921 proof - |
|
2922 def c\<equiv>"2 * complex_of_real pi * \<i> " |
|
2923 def ff\<equiv>"(\<lambda>x. deriv f x * h x / f x)" |
|
2924 def cont_pole\<equiv>"\<lambda>ff p e. (ff has_contour_integral - c * porder f p * h p) (circlepath p e)" |
|
2925 def cont_zero\<equiv>"\<lambda>ff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)" |
|
2926 def avoid\<equiv>"\<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" |
|
2927 have "poles \<subseteq> pts" and "zeros \<subseteq> pts" and "finite zeros" and "pts=zeros \<union> poles" |
|
2928 using poles `finite pts` unfolding pts_def zeros_def is_pole_def by auto |
|
2929 have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> cont_pole ff p e) \<and> (p\<in>zeros \<longrightarrow> cont_zero ff p e)" |
|
2930 when "p\<in>s" for p |
|
2931 proof - |
|
2932 obtain e1 where e:"e1>0" and e:"avoid p e1" |
|
2933 using finite_cball_avoid[OF `open s` `finite pts`] `p\<in>s` unfolding avoid_def by auto |
|
2934 have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2" |
|
2935 when "p\<in>poles" |
|
2936 proof - |
|
2937 def po\<equiv>"porder f p" |
|
2938 def pp\<equiv>"pol_poly f p" |
|
2939 def f'\<equiv>"\<lambda>w. pp w / (w - p) ^ po" |
|
2940 def ff'\<equiv>"(\<lambda>x. deriv f' x * h x / f' x)" |
|
2941 have "inverse \<circ> f holomorphic_on ball p e1" |
|
2942 proof - |
|
2943 have "f holomorphic_on ball p e1 - {p}" |
|
2944 using f_holo e `poles \<subseteq> pts` unfolding avoid_def |
|
2945 apply (elim holomorphic_on_subset) |
|
2946 by auto |
|
2947 then have inv_holo:"(inverse o f) holomorphic_on ball p e1 - {p}" |
|
2948 unfolding comp_def |
|
2949 apply (elim holomorphic_on_inverse) |
|
2950 using e pts_def ball_subset_cball unfolding avoid_def by blast |
|
2951 moreover have "isCont (inverse o f) p" |
|
2952 using `p\<in>poles` poles unfolding is_pole_def by auto |
|
2953 ultimately show "(inverse o f) holomorphic_on ball p e1" |
|
2954 apply (elim no_isolated_singularity[rotated]) |
|
2955 apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified]) |
|
2956 using field_differentiable_imp_continuous_at inv_holo |
|
2957 holomorphic_on_imp_differentiable_at unfolding comp_def |
|
2958 by fastforce |
|
2959 qed |
|
2960 moreover have "f p = 0" using `p\<in>poles` poles unfolding is_pole_def by auto |
|
2961 moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0" |
|
2962 proof - |
|
2963 def p'\<equiv>"p+e1/2" |
|
2964 have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm) |
|
2965 then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def |
|
2966 apply (rule_tac x=p' in bexI) |
|
2967 by (auto simp add:pts_def) |
|
2968 qed |
|
2969 ultimately obtain r where |
|
2970 "0 < po" "r>0" |
|
2971 "cball p r \<subseteq> ball p e1" and |
|
2972 pp_holo:"pp holomorphic_on cball p r" and |
|
2973 pp_po:"(\<forall>w\<in>cball p r. f w = pp w / (w - p) ^ po \<and> pp w \<noteq> 0)" |
|
2974 using porder_exist[of "ball p e1" p f,simplified,OF `e1>0`] unfolding po_def pp_def |
|
2975 by auto |
|
2976 def e2\<equiv>"r/2" |
|
2977 have "e2>0" using `r>0` unfolding e2_def by auto |
|
2978 def anal\<equiv>"\<lambda>w. deriv pp w * h w / pp w" and prin\<equiv>"\<lambda>w. - of_nat po * h w / (w - p)" |
|
2979 have "((\<lambda>w. prin w + anal w) has_contour_integral - c * po * h p) (circlepath p e2)" |
|
2980 proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified]) |
|
2981 have "ball p r \<subseteq> s" |
|
2982 using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e by blast |
|
2983 then have "cball p e2 \<subseteq> s" |
|
2984 using `r>0` unfolding e2_def by auto |
|
2985 then have "(\<lambda>w. - of_nat po * h w) holomorphic_on cball p e2" |
|
2986 using h_holo |
|
2987 by (auto intro!: holomorphic_intros) |
|
2988 then show "(prin has_contour_integral - c * of_nat po * h p ) (circlepath p e2)" |
|
2989 using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. - of_nat po * h w"] |
|
2990 `e2>0` |
|
2991 unfolding prin_def |
|
2992 by (auto simp add: mult.assoc) |
|
2993 have "anal holomorphic_on ball p r" unfolding anal_def |
|
2994 using pp_holo h_holo pp_po `ball p r \<subseteq> s` |
|
2995 by (auto intro!: holomorphic_intros) |
|
2996 then show "(anal has_contour_integral 0) (circlepath p e2)" |
|
2997 using e2_def `r>0` |
|
2998 by (auto elim!: Cauchy_theorem_disc_simple) |
|
2999 qed |
|
3000 then have "cont_pole ff' p e2" unfolding cont_pole_def po_def |
|
3001 proof (elim has_contour_integral_eq) |
|
3002 fix w assume "w \<in> path_image (circlepath p e2)" |
|
3003 then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto |
|
3004 def wp\<equiv>"w-p" |
|
3005 have "wp\<noteq>0" and "pp w \<noteq>0" |
|
3006 unfolding wp_def using `w\<noteq>p` `w\<in>ball p r` pp_po by auto |
|
3007 moreover have der_f':"deriv f' w = - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po" |
|
3008 proof (rule DERIV_imp_deriv) |
|
3009 def der \<equiv> "- po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po" |
|
3010 have po:"po = Suc (po - Suc 0) " using `po>0` by auto |
|
3011 have "(pp has_field_derivative (deriv pp w)) (at w)" |
|
3012 using DERIV_deriv_iff_field_differentiable `w\<in>ball p r` |
|
3013 holomorphic_on_imp_differentiable_at[of _ "ball p r"] |
|
3014 holomorphic_on_subset [OF pp_holo ball_subset_cball] |
|
3015 by (metis open_ball) |
|
3016 then show "(f' has_field_derivative der) (at w)" |
|
3017 using `w\<noteq>p` `po>0` unfolding der_def f'_def |
|
3018 apply (auto intro!: derivative_eq_intros simp add:field_simps) |
|
3019 apply (subst (4) po) |
|
3020 apply (subst power_Suc) |
|
3021 by (auto simp add:field_simps) |
|
3022 qed |
|
3023 ultimately show "prin w + anal w = ff' w" |
|
3024 unfolding ff'_def prin_def anal_def |
|
3025 apply simp |
|
3026 apply (unfold f'_def) |
|
3027 apply (fold wp_def) |
|
3028 by (auto simp add:field_simps) |
|
3029 qed |
|
3030 then have "cont_pole ff p e2" unfolding cont_pole_def |
|
3031 proof (elim has_contour_integral_eq) |
|
3032 fix w assume "w \<in> path_image (circlepath p e2)" |
|
3033 then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto |
|
3034 have "deriv f' w = deriv f w" |
|
3035 proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"]) |
|
3036 show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo |
|
3037 by (auto intro!: holomorphic_intros) |
|
3038 next |
|
3039 have "ball p e1 - {p} \<subseteq> s - poles" |
|
3040 using avoid_def ball_subset_cball e \<open>poles \<subseteq> pts\<close> by auto |
|
3041 then have "ball p r - {p} \<subseteq> s - poles" using `cball p r \<subseteq> ball p e1` |
|
3042 using ball_subset_cball by blast |
|
3043 then show "f holomorphic_on ball p r - {p}" using f_holo |
|
3044 by auto |
|
3045 next |
|
3046 show "open (ball p r - {p})" by auto |
|
3047 next |
|
3048 show "w \<in> ball p r - {p}" using `w\<in>ball p r` `w\<noteq>p` by auto |
|
3049 next |
|
3050 fix x assume "x \<in> ball p r - {p}" |
|
3051 then show "f' x = f x" |
|
3052 using pp_po unfolding f'_def by auto |
|
3053 qed |
|
3054 moreover have " f' w = f w " |
|
3055 using \<open>w \<in> ball p r\<close> ball_subset_cball subset_iff pp_po unfolding f'_def by auto |
|
3056 ultimately show "ff' w = ff w" |
|
3057 unfolding ff'_def ff_def by simp |
|
3058 qed |
|
3059 moreover have "cball p e2 \<subseteq> ball p e1" |
|
3060 using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto |
|
3061 ultimately show ?thesis using `e2>0` by auto |
|
3062 qed |
|
3063 then obtain e2 where e2:"p\<in>poles \<longrightarrow> e2>0 \<and> cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2" |
|
3064 by auto |
|
3065 have "\<exists>e3>0. cball p e3 \<subseteq> ball p e1 \<and> cont_zero ff p e3" |
|
3066 when "p\<in>zeros" |
|
3067 proof - |
|
3068 def zo\<equiv>"zorder f p" |
|
3069 def zp\<equiv>"zer_poly f p" |
|
3070 def f'\<equiv>"\<lambda>w. zp w * (w - p) ^ zo" |
|
3071 def ff'\<equiv>"(\<lambda>x. deriv f' x * h x / f' x)" |
|
3072 have "f holomorphic_on ball p e1" |
|
3073 proof - |
|
3074 have "ball p e1 \<subseteq> s - poles" |
|
3075 using \<open>poles \<subseteq> pts\<close> avoid_def ball_subset_cball e that zeros_def by fastforce |
|
3076 thus ?thesis using f_holo by auto |
|
3077 qed |
|
3078 moreover have "f p = 0" using `p\<in>zeros` |
|
3079 using DiffD1 mem_Collect_eq pts_def zeros_def by blast |
|
3080 moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0" |
|
3081 proof - |
|
3082 def p'\<equiv>"p+e1/2" |
|
3083 have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm) |
|
3084 then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def |
|
3085 apply (rule_tac x=p' in bexI) |
|
3086 by (auto simp add:pts_def) |
|
3087 qed |
|
3088 ultimately obtain r where |
|
3089 "0 < zo" "r>0" |
|
3090 "cball p r \<subseteq> ball p e1" and |
|
3091 pp_holo:"zp holomorphic_on cball p r" and |
|
3092 pp_po:"(\<forall>w\<in>cball p r. f w = zp w * (w - p) ^ zo \<and> zp w \<noteq> 0)" |
|
3093 using zorder_exist[of "ball p e1" p f,simplified,OF `e1>0`] unfolding zo_def zp_def |
|
3094 by auto |
|
3095 def e2\<equiv>"r/2" |
|
3096 have "e2>0" using `r>0` unfolding e2_def by auto |
|
3097 def anal\<equiv>"\<lambda>w. deriv zp w * h w / zp w" and prin\<equiv>"\<lambda>w. of_nat zo * h w / (w - p)" |
|
3098 have "((\<lambda>w. prin w + anal w) has_contour_integral c * zo * h p) (circlepath p e2)" |
|
3099 proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified]) |
|
3100 have "ball p r \<subseteq> s" |
|
3101 using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e by blast |
|
3102 then have "cball p e2 \<subseteq> s" |
|
3103 using `r>0` unfolding e2_def by auto |
|
3104 then have "(\<lambda>w. of_nat zo * h w) holomorphic_on cball p e2" |
|
3105 using h_holo |
|
3106 by (auto intro!: holomorphic_intros) |
|
3107 then show "(prin has_contour_integral c * of_nat zo * h p ) (circlepath p e2)" |
|
3108 using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. of_nat zo * h w"] |
|
3109 `e2>0` |
|
3110 unfolding prin_def |
|
3111 by (auto simp add: mult.assoc) |
|
3112 have "anal holomorphic_on ball p r" unfolding anal_def |
|
3113 using pp_holo h_holo pp_po `ball p r \<subseteq> s` |
|
3114 by (auto intro!: holomorphic_intros) |
|
3115 then show "(anal has_contour_integral 0) (circlepath p e2)" |
|
3116 using e2_def `r>0` |
|
3117 by (auto elim!: Cauchy_theorem_disc_simple) |
|
3118 qed |
|
3119 then have "cont_zero ff' p e2" unfolding cont_zero_def zo_def |
|
3120 proof (elim has_contour_integral_eq) |
|
3121 fix w assume "w \<in> path_image (circlepath p e2)" |
|
3122 then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto |
|
3123 def wp\<equiv>"w-p" |
|
3124 have "wp\<noteq>0" and "zp w \<noteq>0" |
|
3125 unfolding wp_def using `w\<noteq>p` `w\<in>ball p r` pp_po by auto |
|
3126 moreover have der_f':"deriv f' w = zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo" |
|
3127 proof (rule DERIV_imp_deriv) |
|
3128 def der\<equiv>"zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo" |
|
3129 have po:"zo = Suc (zo - Suc 0) " using `zo>0` by auto |
|
3130 have "(zp has_field_derivative (deriv zp w)) (at w)" |
|
3131 using DERIV_deriv_iff_field_differentiable `w\<in>ball p r` |
|
3132 holomorphic_on_imp_differentiable_at[of _ "ball p r"] |
|
3133 holomorphic_on_subset [OF pp_holo ball_subset_cball] |
|
3134 by (metis open_ball) |
|
3135 then show "(f' has_field_derivative der) (at w)" |
|
3136 using `w\<noteq>p` `zo>0` unfolding der_def f'_def |
|
3137 by (auto intro!: derivative_eq_intros simp add:field_simps) |
|
3138 qed |
|
3139 ultimately show "prin w + anal w = ff' w" |
|
3140 unfolding ff'_def prin_def anal_def |
|
3141 apply simp |
|
3142 apply (unfold f'_def) |
|
3143 apply (fold wp_def) |
|
3144 apply (auto simp add:field_simps) |
|
3145 by (metis Suc_diff_Suc minus_nat.diff_0 power_Suc) |
|
3146 qed |
|
3147 then have "cont_zero ff p e2" unfolding cont_zero_def |
|
3148 proof (elim has_contour_integral_eq) |
|
3149 fix w assume "w \<in> path_image (circlepath p e2)" |
|
3150 then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto |
|
3151 have "deriv f' w = deriv f w" |
|
3152 proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"]) |
|
3153 show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo |
|
3154 by (auto intro!: holomorphic_intros) |
|
3155 next |
|
3156 have "ball p e1 - {p} \<subseteq> s - poles" |
|
3157 using avoid_def ball_subset_cball e \<open>poles \<subseteq> pts\<close> by auto |
|
3158 then have "ball p r - {p} \<subseteq> s - poles" using `cball p r \<subseteq> ball p e1` |
|
3159 using ball_subset_cball by blast |
|
3160 then show "f holomorphic_on ball p r - {p}" using f_holo |
|
3161 by auto |
|
3162 next |
|
3163 show "open (ball p r - {p})" by auto |
|
3164 next |
|
3165 show "w \<in> ball p r - {p}" using `w\<in>ball p r` `w\<noteq>p` by auto |
|
3166 next |
|
3167 fix x assume "x \<in> ball p r - {p}" |
|
3168 then show "f' x = f x" |
|
3169 using pp_po unfolding f'_def by auto |
|
3170 qed |
|
3171 moreover have " f' w = f w " |
|
3172 using \<open>w \<in> ball p r\<close> ball_subset_cball subset_iff pp_po unfolding f'_def by auto |
|
3173 ultimately show "ff' w = ff w" |
|
3174 unfolding ff'_def ff_def by simp |
|
3175 qed |
|
3176 moreover have "cball p e2 \<subseteq> ball p e1" |
|
3177 using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto |
|
3178 ultimately show ?thesis using `e2>0` by auto |
|
3179 qed |
|
3180 then obtain e3 where e3:"p\<in>zeros \<longrightarrow> e3>0 \<and> cball p e3 \<subseteq> ball p e1 \<and> cont_zero ff p e3" |
|
3181 by auto |
|
3182 def e4\<equiv>"if p\<in>poles then e2 else if p\<in>zeros then e3 else e1" |
|
3183 have "e4>0" using e2 e3 `e1>0` unfolding e4_def by auto |
|
3184 moreover have "avoid p e4" using e2 e3 `e1>0` e unfolding e4_def avoid_def by auto |
|
3185 moreover have "p\<in>poles \<longrightarrow> cont_pole ff p e4" and "p\<in>zeros \<longrightarrow> cont_zero ff p e4" |
|
3186 by (auto simp add: e2 e3 e4_def pts_def zeros_def) |
|
3187 ultimately show ?thesis by auto |
|
3188 qed |
|
3189 then obtain get_e where get_e:"\<forall>p\<in>s. get_e p>0 \<and> avoid p (get_e p) |
|
3190 \<and> (p\<in>poles \<longrightarrow> cont_pole ff p (get_e p)) \<and> (p\<in>zeros \<longrightarrow> cont_zero ff p (get_e p))" |
|
3191 by metis |
|
3192 def cont\<equiv>"\<lambda>p. contour_integral (circlepath p (get_e p)) ff" |
|
3193 def w\<equiv>"\<lambda>p. winding_number g p" |
|
3194 have "contour_integral g ff = (\<Sum>p\<in>pts. w p * cont p)" |
|
3195 unfolding cont_def w_def |
|
3196 proof (rule Cauchy_theorem_singularities[OF `open s` connected finite _ `valid_path g` loop |
|
3197 path_img homo]) |
|
3198 have "open (s - pts)" using open_Diff[OF _ finite_imp_closed[OF finite]] `open s` by auto |
|
3199 then show "ff holomorphic_on s - pts" unfolding ff_def using f_holo `poles \<subseteq> pts` h_holo |
|
3200 by (auto intro!: holomorphic_intros simp add:pts_def) |
|
3201 next |
|
3202 show "\<forall>p\<in>s. 0 < get_e p \<and> (\<forall>w\<in>cball p (get_e p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts))" |
|
3203 using get_e using avoid_def by blast |
|
3204 qed |
|
3205 also have "... = (\<Sum>p\<in>zeros. w p * cont p) + (\<Sum>p\<in>poles. w p * cont p)" |
|
3206 using `finite pts` unfolding `pts=zeros \<union> poles` |
|
3207 apply (subst setsum.union_disjoint) |
|
3208 by (auto simp add:zeros_def) |
|
3209 also have "... = c * ((\<Sum>p\<in>zeros. w p * h p * zorder f p) - (\<Sum>p\<in>poles. w p * h p * porder f p))" |
|
3210 proof - |
|
3211 have "(\<Sum>p\<in>zeros. w p * cont p) = (\<Sum>p\<in>zeros. c * w p * h p * zorder f p)" |
|
3212 proof (rule setsum.cong[of zeros zeros,simplified]) |
|
3213 fix p assume "p \<in> zeros" |
|
3214 show "w p * cont p = c * w p * h p * (zorder f p)" |
|
3215 proof (cases "p\<in>s") |
|
3216 assume "p \<in> s" |
|
3217 have "cont p = c * h p * (zorder f p)" unfolding cont_def |
|
3218 apply (rule contour_integral_unique) |
|
3219 using get_e `p\<in>s` `p\<in>zeros` unfolding cont_zero_def |
|
3220 by (metis mult.assoc mult.commute) |
|
3221 thus ?thesis by auto |
|
3222 next |
|
3223 assume "p\<notin>s" |
|
3224 then have "w p=0" using homo unfolding w_def by auto |
|
3225 then show ?thesis by auto |
|
3226 qed |
|
3227 qed |
|
3228 then have "(\<Sum>p\<in>zeros. w p * cont p) = c * (\<Sum>p\<in>zeros. w p * h p * zorder f p)" |
|
3229 apply (subst setsum_right_distrib) |
|
3230 by (simp add:algebra_simps) |
|
3231 moreover have "(\<Sum>p\<in>poles. w p * cont p) = (\<Sum>p\<in>poles. - c * w p * h p * porder f p)" |
|
3232 proof (rule setsum.cong[of poles poles,simplified]) |
|
3233 fix p assume "p \<in> poles" |
|
3234 show "w p * cont p = - c * w p * h p * (porder f p)" |
|
3235 proof (cases "p\<in>s") |
|
3236 assume "p \<in> s" |
|
3237 have "cont p = - c * h p * (porder f p)" unfolding cont_def |
|
3238 apply (rule contour_integral_unique) |
|
3239 using get_e `p\<in>s` `p\<in>poles` unfolding cont_pole_def |
|
3240 by (metis mult.assoc mult.commute) |
|
3241 thus ?thesis by auto |
|
3242 next |
|
3243 assume "p\<notin>s" |
|
3244 then have "w p=0" using homo unfolding w_def by auto |
|
3245 then show ?thesis by auto |
|
3246 qed |
|
3247 qed |
|
3248 then have "(\<Sum>p\<in>poles. w p * cont p) = - c * (\<Sum>p\<in>poles. w p * h p * porder f p)" |
|
3249 apply (subst setsum_right_distrib) |
|
3250 by (simp add:algebra_simps) |
|
3251 ultimately show ?thesis by (simp add: right_diff_distrib) |
|
3252 qed |
|
3253 finally show ?thesis unfolding w_def ff_def c_def by auto |
|
3254 qed |
|
3255 |
|
3256 lemma holomorphic_imp_diff_on: |
|
3257 assumes f_holo:"f holomorphic_on s" and "open s" |
|
3258 shows "f differentiable_on s" |
|
3259 proof (rule differentiable_at_imp_differentiable_on) |
|
3260 fix x assume "x\<in>s" |
|
3261 obtain f' where "(f has_field_derivative f') (at x) " |
|
3262 using holomorphic_on_imp_differentiable_at[OF f_holo `open s` `x\<in>s`] |
|
3263 unfolding field_differentiable_def by auto |
|
3264 then have " (f has_derivative op * f') (at x)" |
|
3265 using has_field_derivative_imp_has_derivative[of f f' "at x"] by auto |
|
3266 then show "f differentiable at x" using differentiableI by auto |
|
3267 qed |
|
3268 |
|
3269 theorem Rouche_theorem: |
|
3270 fixes f g::"complex \<Rightarrow> complex" and s:: "complex set" |
|
3271 defines "fg\<equiv>(\<lambda>p. f p+ g p)" |
|
3272 defines "zeros_fg\<equiv>{p. fg p =0}" and "zeros_f\<equiv>{p. f p=0}" |
|
3273 assumes |
|
3274 "open s" and |
|
3275 connected_fg:"connected (s- zeros_fg)" and |
|
3276 connected_f:"connected (s- zeros_f)" and |
|
3277 "finite zeros_fg" and |
|
3278 "finite zeros_f" and |
|
3279 f_holo:"f holomorphic_on s" and |
|
3280 g_holo:"g holomorphic_on s" and |
|
3281 "valid_path \<gamma>" and |
|
3282 loop:"pathfinish \<gamma> = pathstart \<gamma>" and |
|
3283 path_img:"path_image \<gamma> \<subseteq> s " and |
|
3284 path_less:"\<forall>z\<in>path_image \<gamma>. cmod(f z) > cmod(g z)" and |
|
3285 homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number \<gamma> z = 0" |
|
3286 shows "(\<Sum>p\<in>zeros_fg. winding_number \<gamma> p * zorder fg p) |
|
3287 = (\<Sum>p\<in>zeros_f. winding_number \<gamma> p * zorder f p)" |
|
3288 proof - |
|
3289 have path_fg:"path_image \<gamma> \<subseteq> s - zeros_fg" |
|
3290 proof - |
|
3291 have False when "z\<in>path_image \<gamma>" and "f z + g z=0" for z |
|
3292 proof - |
|
3293 have "cmod (f z) > cmod (g z)" using `z\<in>path_image \<gamma>` path_less by auto |
|
3294 moreover have "f z = - g z" using `f z + g z =0` by (simp add: eq_neg_iff_add_eq_0) |
|
3295 then have "cmod (f z) = cmod (g z)" by auto |
|
3296 ultimately show False by auto |
|
3297 qed |
|
3298 then show ?thesis unfolding zeros_fg_def fg_def using path_img by auto |
|
3299 qed |
|
3300 have path_f:"path_image \<gamma> \<subseteq> s - zeros_f" |
|
3301 proof - |
|
3302 have False when "z\<in>path_image \<gamma>" and "f z =0" for z |
|
3303 proof - |
|
3304 have "cmod (g z) < cmod (f z) " using `z\<in>path_image \<gamma>` path_less by auto |
|
3305 then have "cmod (g z) < 0" using `f z=0` by auto |
|
3306 then show False by auto |
|
3307 qed |
|
3308 then show ?thesis unfolding zeros_f_def using path_img by auto |
|
3309 qed |
|
3310 def w\<equiv>"\<lambda>p. winding_number \<gamma> p" |
|
3311 def c\<equiv>"2 * complex_of_real pi * \<i>" |
|
3312 def h\<equiv>"\<lambda>p. g p / f p + 1" |
|
3313 obtain spikes |
|
3314 where "finite spikes" and spikes: "\<forall>x\<in>{0..1} - spikes. \<gamma> differentiable at x" |
|
3315 using `valid_path \<gamma>` |
|
3316 by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
|
3317 have h_contour:"((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>" |
|
3318 proof - |
|
3319 have outside_img:"0 \<in> outside (path_image (h o \<gamma>))" |
|
3320 proof - |
|
3321 have "h p \<in> ball 1 1" when "p\<in>path_image \<gamma>" for p |
|
3322 proof - |
|
3323 have "cmod (g p/f p) <1" using path_less[rule_format,OF that] |
|
3324 apply (cases "cmod (f p) = 0") |
|
3325 by (auto simp add: norm_divide) |
|
3326 then show ?thesis unfolding h_def by (auto simp add:dist_complex_def) |
|
3327 qed |
|
3328 then have "path_image (h o \<gamma>) \<subseteq> ball 1 1" |
|
3329 by (simp add: image_subset_iff path_image_compose) |
|
3330 moreover have " (0::complex) \<notin> ball 1 1" by (simp add: dist_norm) |
|
3331 ultimately show "?thesis" |
|
3332 using convex_in_outside[of "ball 1 1" "0::complex"] |
|
3333 apply (drule_tac outside_mono) |
|
3334 by auto |
|
3335 qed |
|
3336 have valid_h:"valid_path (h \<circ> \<gamma>)" |
|
3337 proof (rule valid_path_compose_holomorphic[OF `valid_path \<gamma>` _ _ path_f]) |
|
3338 show "h holomorphic_on s - zeros_f" |
|
3339 unfolding h_def using f_holo g_holo |
|
3340 by (auto intro!: holomorphic_intros simp add:zeros_f_def) |
|
3341 next |
|
3342 show "open (s - zeros_f)" using `finite zeros_f` `open s` finite_imp_closed |
|
3343 by auto |
|
3344 qed |
|
3345 have "((\<lambda>z. 1/z) has_contour_integral 0) (h \<circ> \<gamma>)" |
|
3346 proof - |
|
3347 have "0 \<notin> path_image (h \<circ> \<gamma>)" using outside_img by (simp add: outside_def) |
|
3348 then have "((\<lambda>z. 1/z) has_contour_integral c * winding_number (h \<circ> \<gamma>) 0) (h \<circ> \<gamma>)" |
|
3349 using has_contour_integral_winding_number[of "h o \<gamma>" 0,simplified] valid_h |
|
3350 unfolding c_def by auto |
|
3351 moreover have "winding_number (h o \<gamma>) 0 = 0" |
|
3352 proof - |
|
3353 have "0 \<in> outside (path_image (h \<circ> \<gamma>))" using outside_img . |
|
3354 moreover have "path (h o \<gamma>)" |
|
3355 using valid_h by auto |
|
3356 moreover have "pathfinish (h o \<gamma>) = pathstart (h o \<gamma>)" |
|
3357 by (simp add: loop pathfinish_compose pathstart_compose) |
|
3358 ultimately show ?thesis using winding_number_zero_in_outside by auto |
|
3359 qed |
|
3360 ultimately show ?thesis by auto |
|
3361 qed |
|
3362 moreover have "vector_derivative (h \<circ> \<gamma>) (at x) = vector_derivative \<gamma> (at x) * deriv h (\<gamma> x)" |
|
3363 when "x\<in>{0..1} - spikes" for x |
|
3364 proof (rule vector_derivative_chain_at_general) |
|
3365 show "\<gamma> differentiable at x" using that `valid_path \<gamma>` spikes by auto |
|
3366 next |
|
3367 def der\<equiv>"\<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)" |
|
3368 def t\<equiv>"\<gamma> x" |
|
3369 have "f t\<noteq>0" unfolding zeros_f_def t_def |
|
3370 by (metis DiffD1 image_eqI norm_not_less_zero norm_zero path_defs(4) path_less that) |
|
3371 moreover have "t\<in>s" |
|
3372 using contra_subsetD path_image_def path_fg t_def that by fastforce |
|
3373 ultimately have "(h has_field_derivative der t) (at t)" |
|
3374 unfolding h_def der_def using g_holo f_holo |
|
3375 apply (auto intro!: derivative_eq_intros) |
|
3376 by (auto simp add: DERIV_deriv_iff_field_differentiable |
|
3377 holomorphic_on_imp_differentiable_at[OF _ `open s`]) |
|
3378 then show "\<exists>g'. (h has_field_derivative g') (at (\<gamma> x))" unfolding t_def by auto |
|
3379 qed |
|
3380 then have " (op / 1 has_contour_integral 0) (h \<circ> \<gamma>) |
|
3381 = ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>" |
|
3382 unfolding has_contour_integral |
|
3383 apply (intro has_integral_spike_eq[OF negligible_finite, OF `finite spikes`]) |
|
3384 by auto |
|
3385 ultimately show ?thesis by auto |
|
3386 qed |
|
3387 then have "contour_integral \<gamma> (\<lambda>x. deriv h x / h x) = 0" |
|
3388 using contour_integral_unique by simp |
|
3389 moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = contour_integral \<gamma> (\<lambda>x. deriv f x / f x) |
|
3390 + contour_integral \<gamma> (\<lambda>p. deriv h p / h p)" |
|
3391 proof - |
|
3392 have "(\<lambda>p. deriv f p / f p) contour_integrable_on \<gamma>" |
|
3393 proof (rule contour_integrable_holomorphic_simple[OF _ _ `valid_path \<gamma>` path_f]) |
|
3394 show "open (s - zeros_f)" using finite_imp_closed[OF `finite zeros_f`] `open s` |
|
3395 by auto |
|
3396 then show "(\<lambda>p. deriv f p / f p) holomorphic_on s - zeros_f" |
|
3397 using f_holo |
|
3398 by (auto intro!: holomorphic_intros simp add:zeros_f_def) |
|
3399 qed |
|
3400 moreover have "(\<lambda>p. deriv h p / h p) contour_integrable_on \<gamma>" |
|
3401 using h_contour |
|
3402 by (simp add: has_contour_integral_integrable) |
|
3403 ultimately have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x + deriv h x / h x) = |
|
3404 contour_integral \<gamma> (\<lambda>p. deriv f p / f p) + contour_integral \<gamma> (\<lambda>p. deriv h p / h p)" |
|
3405 using contour_integral_add[of "(\<lambda>p. deriv f p / f p)" \<gamma> "(\<lambda>p. deriv h p / h p)" ] |
|
3406 by auto |
|
3407 moreover have "deriv fg p / fg p = deriv f p / f p + deriv h p / h p" |
|
3408 when "p\<in> path_image \<gamma>" for p |
|
3409 proof - |
|
3410 have "fg p\<noteq>0" and "f p\<noteq>0" using path_f path_fg that unfolding zeros_f_def zeros_fg_def |
|
3411 by auto |
|
3412 have "h p\<noteq>0" |
|
3413 proof (rule ccontr) |
|
3414 assume "\<not> h p \<noteq> 0" |
|
3415 then have "g p / f p= -1" unfolding h_def by (simp add: add_eq_0_iff2) |
|
3416 then have "cmod (g p/f p) = 1" by auto |
|
3417 moreover have "cmod (g p/f p) <1" using path_less[rule_format,OF that] |
|
3418 apply (cases "cmod (f p) = 0") |
|
3419 by (auto simp add: norm_divide) |
|
3420 ultimately show False by auto |
|
3421 qed |
|
3422 have der_fg:"deriv fg p = deriv f p + deriv g p" unfolding fg_def |
|
3423 using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _ `open s`] path_img that |
|
3424 by (auto intro!: deriv_add) |
|
3425 have der_h:"deriv h p = (deriv g p * f p - g p * deriv f p)/(f p * f p)" |
|
3426 proof - |
|
3427 def der\<equiv>"\<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)" |
|
3428 have "p\<in>s" using path_img that by auto |
|
3429 then have "(h has_field_derivative der p) (at p)" |
|
3430 unfolding h_def der_def using g_holo f_holo `f p\<noteq>0` |
|
3431 apply (auto intro!: derivative_eq_intros) |
|
3432 by (auto simp add: DERIV_deriv_iff_field_differentiable |
|
3433 holomorphic_on_imp_differentiable_at[OF _ `open s`]) |
|
3434 then show ?thesis unfolding der_def using DERIV_imp_deriv by auto |
|
3435 qed |
|
3436 show ?thesis |
|
3437 apply (simp only:der_fg der_h) |
|
3438 apply (auto simp add:field_simps `h p\<noteq>0` `f p\<noteq>0` `fg p\<noteq>0`) |
|
3439 by (auto simp add:field_simps h_def `f p\<noteq>0` fg_def) |
|
3440 qed |
|
3441 then have "contour_integral \<gamma> (\<lambda>p. deriv fg p / fg p) |
|
3442 = contour_integral \<gamma> (\<lambda>p. deriv f p / f p + deriv h p / h p)" |
|
3443 by (elim contour_integral_eq) |
|
3444 ultimately show ?thesis by auto |
|
3445 qed |
|
3446 moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)" |
|
3447 unfolding c_def zeros_fg_def w_def |
|
3448 proof (rule argument_principle[OF `open s` _ _ _ `valid_path \<gamma>` loop _ homo, of _ "{}" "\<lambda>_. 1",simplified]) |
|
3449 show "connected (s - {p. fg p = 0})" using connected_fg unfolding zeros_fg_def . |
|
3450 show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto |
|
3451 show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def . |
|
3452 show " finite {p. fg p = 0}" using `finite zeros_fg` unfolding zeros_fg_def . |
|
3453 qed |
|
3454 moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)" |
|
3455 unfolding c_def zeros_f_def w_def |
|
3456 proof (rule argument_principle[OF `open s` _ _ _ `valid_path \<gamma>` loop _ homo, of _ "{}" "\<lambda>_. 1",simplified]) |
|
3457 show "connected (s - {p. f p = 0})" using connected_f unfolding zeros_f_def . |
|
3458 show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto |
|
3459 show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def . |
|
3460 show "finite {p. f p = 0}" using `finite zeros_f` unfolding zeros_f_def . |
|
3461 qed |
|
3462 ultimately have "c * (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))" |
|
3463 by auto |
|
3464 then show ?thesis unfolding c_def using w_def by auto |
|
3465 qed |
|
3466 |
2133 end |
3467 end |