equal
deleted
inserted
replaced
1363 by (simp add: valid_path_imp_path) |
1363 by (simp add: valid_path_imp_path) |
1364 then obtain d::real and p |
1364 then obtain d::real and p |
1365 where d: "0 < d" |
1365 where d: "0 < d" |
1366 and p: "polynomial_function p" "path_image p \<subseteq> S" |
1366 and p: "polynomial_function p" "path_image p \<subseteq> S" |
1367 and pi: "\<And>f. f holomorphic_on S \<Longrightarrow> contour_integral g f = contour_integral p f" |
1367 and pi: "\<And>f. f holomorphic_on S \<Longrightarrow> contour_integral g f = contour_integral p f" |
1368 using contour_integral_nearby_ends [OF S \<open>path g\<close> pag] assms |
1368 using contour_integral_nearby_ends [OF S \<open>path g\<close> pag] |
1369 apply clarify |
1369 apply clarify |
1370 apply (drule_tac x=g in spec) |
1370 apply (drule_tac x=g in spec) |
1371 apply (simp only: assms) |
1371 apply (simp only: assms) |
1372 apply (force simp: valid_path_polynomial_function elim: path_approx_polynomial_function) |
1372 apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function) |
1373 done |
1373 done |
1374 then obtain p' where p': "polynomial_function p'" |
1374 then obtain p' where p': "polynomial_function p'" |
1375 "\<And>x. (p has_vector_derivative (p' x)) (at x)" |
1375 "\<And>x. (p has_vector_derivative (p' x)) (at x)" |
1376 by (blast intro: has_vector_derivative_polynomial_function that) |
1376 by (blast intro: has_vector_derivative_polynomial_function that) |
1377 then have "bounded(p' ` {0..1})" |
1377 then have "bounded(p' ` {0..1})" |