# HG changeset patch # User paulson # Date 1527545723 -3600 # Node ID d0a7ddf5450e4e4d92d1e0df455bc9981776f684 # Parent ce7855c7f5f46125a056e8e5b8ccfe3c3bded561 more general tidying diff -r ce7855c7f5f4 -r d0a7ddf5450e src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun May 27 22:57:06 2018 +0100 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon May 28 23:15:23 2018 +0100 @@ -2164,7 +2164,8 @@ qed -(* Hence the most basic theorem for a triangle.*) +text\Hence the most basic theorem for a triangle.\ + locale Chain = fixes x0 At Follows assumes At0: "At x0 0" @@ -2208,7 +2209,7 @@ done qed -lemma Cauchy_theorem_triangle: +proposition Cauchy_theorem_triangle: assumes "f holomorphic_on (convex hull {a,b,c})" shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" proof - @@ -2366,7 +2367,7 @@ qed -lemma Cauchy_theorem_triangle_interior: +proposition Cauchy_theorem_triangle_interior: assumes contf: "continuous_on (convex hull {a,b,c}) f" and holf: "f holomorphic_on interior (convex hull {a,b,c})" shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" @@ -2439,7 +2440,7 @@ using d e by (auto simp: hull_inc mem_interior_convex_shrink shrink_def) then have fhp0: "(f has_contour_integral 0) (linepath (shrink a) (shrink b) +++ linepath (shrink b) (shrink c) +++ linepath (shrink c) (shrink a))" - by (simp add: Cauchy_theorem_triangle holomorphic_on_subset [OF holf] hull_minimal convex_interior) + by (simp add: Cauchy_theorem_triangle holomorphic_on_subset [OF holf] hull_minimal) then have f_0_shrink: "?pathint (shrink a) (shrink b) + ?pathint (shrink b) (shrink c) + ?pathint (shrink c) (shrink a) = 0" by (simp add: has_chain_integral_chain_integral3) have fpi_abc: "f contour_integrable_on linepath (shrink a) (shrink b)" @@ -2478,9 +2479,8 @@ have ll: "linepath (shrink u) (shrink v) x - linepath u v x = -e * ((1 - x) *\<^sub>R (u - d) + x *\<^sub>R (v - d))" by (simp add: linepath_def shrink_def algebra_simps scaleR_conv_of_real) have cmod_less_dt: "cmod (linepath (shrink u) (shrink v) x - linepath u v x) < d1" - using \e>0\ apply (simp only: ll norm_mult scaleR_diff_right) - apply (rule less_le_trans [OF _ e_le_d1]) - using cmod_less_4C apply (force intro: norm_triangle_lt) + apply (simp only: ll norm_mult scaleR_diff_right) + using \e>0\ cmod_less_4C apply (force intro: norm_triangle_lt less_le_trans [OF _ e_le_d1]) done have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) < cmod y / (24 * C)" using x uv shr_uv cmod_less_dt @@ -2509,19 +2509,20 @@ by (blast intro: uv continuous_on_subset [OF contf closed_segment_subset_convex_hull]) have **: "\f' x' f x::complex. f'*x' - f*x = f'*(x' - x) + x*(f' - f)" by (simp add: algebra_simps) - have "norm (?pathint (shrink u) (shrink v) - ?pathint u v) \ norm y / 6" - apply (rule order_trans) + have "norm (?pathint (shrink u) (shrink v) - ?pathint u v) + \ (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))" apply (rule has_integral_bound - [of "B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)" - "\x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)" - _ 0 1 ]) + [of _ "\x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)" + _ 0 1]) using ynz \0 < B\ \0 < C\ - apply (simp_all del: le_divide_eq_numeral1) + apply (simp_all del: le_divide_eq_numeral1) apply (simp add: has_integral_diff has_contour_integral_linepath [symmetric] has_contour_integral_integral - fpi_uv f_uv contour_integrable_continuous_linepath, clarify) - apply (simp only: **) - apply (simp add: norm_triangle_le norm_mult cmod_diff_le del: le_divide_eq_numeral1) + fpi_uv f_uv contour_integrable_continuous_linepath) + apply (auto simp add: ** norm_triangle_le norm_mult cmod_diff_le simp del: le_divide_eq_numeral1) done + also have "... \ norm y / 6" + by simp + finally have "norm (?pathint (shrink u) (shrink v) - ?pathint u v) \ norm y / 6" . } note * = this have "norm (?pathint (shrink a) (shrink b) - ?pathint a b) \ norm y / 6" using False fpi_abc by (rule_tac *) (auto simp: hull_inc) @@ -2565,66 +2566,62 @@ subsection\Version allowing finite number of exceptional points\ -lemma Cauchy_theorem_triangle_cofinite: +proposition Cauchy_theorem_triangle_cofinite: assumes "continuous_on (convex hull {a,b,c}) f" - and "finite s" - and "(\x. x \ interior(convex hull {a,b,c}) - s \ f field_differentiable (at x))" + and "finite S" + and "(\x. x \ interior(convex hull {a,b,c}) - S \ f field_differentiable (at x))" shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" using assms -proof (induction "card s" arbitrary: a b c s rule: less_induct) - case (less s a b c) +proof (induction "card S" arbitrary: a b c S rule: less_induct) + case (less S a b c) show ?case - proof (cases "s={}") + proof (cases "S={}") case True with less show ?thesis - by (fastforce simp: holomorphic_on_def field_differentiable_at_within - Cauchy_theorem_triangle_interior) + by (fastforce simp: holomorphic_on_def field_differentiable_at_within Cauchy_theorem_triangle_interior) next case False - then obtain d s' where d: "s = insert d s'" "d \ s'" + then obtain d S' where d: "S = insert d S'" "d \ S'" by (meson Set.set_insert all_not_in_conv) then show ?thesis proof (cases "d \ convex hull {a,b,c}") case False show "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" - apply (rule less.hyps [of "s'"]) - using False d \finite s\ interior_subset - apply (auto intro!: less.prems) - done + proof (rule less.hyps) + show "\x. x \ interior (convex hull {a, b, c}) - S' \ f field_differentiable at x" + using False d interior_subset by (auto intro!: less.prems) + qed (use d less.prems in auto) next case True have *: "convex hull {a, b, d} \ convex hull {a, b, c}" by (meson True hull_subset insert_subset convex_hull_subset) have abd: "(f has_contour_integral 0) (linepath a b +++ linepath b d +++ linepath d a)" - apply (rule less.hyps [of "s'"]) - using True d \finite s\ not_in_interior_convex_hull_3 - apply (auto intro!: less.prems continuous_on_subset [OF _ *]) - apply (metis * insert_absorb insert_subset interior_mono) - done + proof (rule less.hyps) + show "\x. x \ interior (convex hull {a, b, d}) - S' \ f field_differentiable at x" + using d not_in_interior_convex_hull_3 + by (clarsimp intro!: less.prems) (metis * insert_absorb insert_subset interior_mono) + qed (use d continuous_on_subset [OF _ *] less.prems in auto) have *: "convex hull {b, c, d} \ convex hull {a, b, c}" by (meson True hull_subset insert_subset convex_hull_subset) have bcd: "(f has_contour_integral 0) (linepath b c +++ linepath c d +++ linepath d b)" - apply (rule less.hyps [of "s'"]) - using True d \finite s\ not_in_interior_convex_hull_3 - apply (auto intro!: less.prems continuous_on_subset [OF _ *]) - apply (metis * insert_absorb insert_subset interior_mono) - done + proof (rule less.hyps) + show "\x. x \ interior (convex hull {b, c, d}) - S' \ f field_differentiable at x" + using d not_in_interior_convex_hull_3 + by (clarsimp intro!: less.prems) (metis * insert_absorb insert_subset interior_mono) + qed (use d continuous_on_subset [OF _ *] less.prems in auto) have *: "convex hull {c, a, d} \ convex hull {a, b, c}" by (meson True hull_subset insert_subset convex_hull_subset) have cad: "(f has_contour_integral 0) (linepath c a +++ linepath a d +++ linepath d c)" - apply (rule less.hyps [of "s'"]) - using True d \finite s\ not_in_interior_convex_hull_3 - apply (auto intro!: less.prems continuous_on_subset [OF _ *]) - apply (metis * insert_absorb insert_subset interior_mono) - done + proof (rule less.hyps) + show "\x. x \ interior (convex hull {c, a, d}) - S' \ f field_differentiable at x" + using d not_in_interior_convex_hull_3 + by (clarsimp intro!: less.prems) (metis * insert_absorb insert_subset interior_mono) + qed (use d continuous_on_subset [OF _ *] less.prems in auto) have "f contour_integrable_on linepath a b" - using less.prems - by (metis continuous_on_subset insert_commute contour_integrable_continuous_linepath segments_subset_convex_hull(3)) + using less.prems abd contour_integrable_joinD1 contour_integrable_on_def by blast moreover have "f contour_integrable_on linepath b c" - using less.prems - by (metis continuous_on_subset contour_integrable_continuous_linepath segments_subset_convex_hull(3)) + using less.prems bcd contour_integrable_joinD1 contour_integrable_on_def by blast moreover have "f contour_integrable_on linepath c a" - using less.prems - by (metis continuous_on_subset insert_commute contour_integrable_continuous_linepath segments_subset_convex_hull(3)) + using less.prems cad contour_integrable_joinD1 contour_integrable_on_def by blast ultimately have fpi: "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" by auto { fix y::complex @@ -2637,8 +2634,8 @@ have cont_cd: "continuous_on (closed_segment c d) f" by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(2)) have "contour_integral (linepath a b) f = - (contour_integral (linepath b d) f + (contour_integral (linepath d a) f))" - "contour_integral (linepath b c) f = - (contour_integral (linepath c d) f + (contour_integral (linepath d b) f))" - "contour_integral (linepath c a) f = - (contour_integral (linepath a d) f + contour_integral (linepath d c) f)" + "contour_integral (linepath b c) f = - (contour_integral (linepath c d) f + (contour_integral (linepath d b) f))" + "contour_integral (linepath c a) f = - (contour_integral (linepath a d) f + contour_integral (linepath d c) f)" using has_chain_integral_chain_integral3 [OF abd] has_chain_integral_chain_integral3 [OF bcd] has_chain_integral_chain_integral3 [OF cad] @@ -2656,31 +2653,31 @@ subsection\Cauchy's theorem for an open starlike set\ lemma starlike_convex_subset: - assumes s: "a \ s" "closed_segment b c \ s" and subs: "\x. x \ s \ closed_segment a x \ s" - shows "convex hull {a,b,c} \ s" - using s + assumes S: "a \ S" "closed_segment b c \ S" and subs: "\x. x \ S \ closed_segment a x \ S" + shows "convex hull {a,b,c} \ S" + using S apply (clarsimp simp add: convex_hull_insert [of "{b,c}" a] segment_convex_hull) apply (meson subs convexD convex_closed_segment ends_in_segment(1) ends_in_segment(2) subsetCE) done lemma triangle_contour_integrals_starlike_primitive: - assumes contf: "continuous_on s f" - and s: "a \ s" "open s" - and x: "x \ s" - and subs: "\y. y \ s \ closed_segment a y \ s" - and zer: "\b c. closed_segment b c \ s + assumes contf: "continuous_on S f" + and S: "a \ S" "open S" + and x: "x \ S" + and subs: "\y. y \ S \ closed_segment a y \ S" + and zer: "\b c. closed_segment b c \ S \ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0" shows "((\x. contour_integral(linepath a x) f) has_field_derivative f x) (at x)" proof - let ?pathint = "\x y. contour_integral(linepath x y) f" { fix e y - assume e: "0 < e" and bxe: "ball x e \ s" and close: "cmod (y - x) < e" - have y: "y \ s" + assume e: "0 < e" and bxe: "ball x e \ S" and close: "cmod (y - x) < e" + have y: "y \ S" using bxe close by (force simp: dist_norm norm_minus_commute) have cont_ayf: "continuous_on (closed_segment a y) f" using contf continuous_on_subset subs y by blast - have xys: "closed_segment x y \ s" + have xys: "closed_segment x y \ S" apply (rule order_trans [OF _ bxe]) using close by (auto simp: dist_norm ball_def norm_minus_commute dest: segment_bound) @@ -2690,34 +2687,30 @@ { fix e::real assume e: "0 < e" have cont_atx: "continuous (at x) f" - using x s contf continuous_on_eq_continuous_at by blast + using x S contf continuous_on_eq_continuous_at by blast then obtain d1 where d1: "d1>0" and d1_less: "\y. cmod (y - x) < d1 \ cmod (f y - f x) < e/2" unfolding continuous_at Lim_at dist_norm using e by (drule_tac x="e/2" in spec) force - obtain d2 where d2: "d2>0" "ball x d2 \ s" using \open s\ x + obtain d2 where d2: "d2>0" "ball x d2 \ S" using \open S\ x by (auto simp: open_contains_ball) have dpos: "min d1 d2 > 0" using d1 d2 by simp { fix y assume yx: "y \ x" and close: "cmod (y - x) < min d1 d2" - have y: "y \ s" + have y: "y \ S" using d2 close by (force simp: dist_norm norm_minus_commute) - have fxy: "f contour_integrable_on linepath x y" - apply (rule contour_integrable_continuous_linepath) - apply (rule continuous_on_subset [OF contf]) - using close d2 - apply (auto simp: dist_norm norm_minus_commute dest!: segment_bound(1)) - done + have "closed_segment x y \ S" + using close d2 by (auto simp: dist_norm norm_minus_commute dest!: segment_bound(1)) + then have fxy: "f contour_integrable_on linepath x y" + by (metis contour_integrable_continuous_linepath continuous_on_subset [OF contf]) then obtain i where i: "(f has_contour_integral i) (linepath x y)" by (auto simp: contour_integrable_on_def) then have "((\w. f w - f x) has_contour_integral (i - f x * (y - x))) (linepath x y)" by (rule has_contour_integral_diff [OF _ has_contour_integral_const_linepath]) then have "cmod (i - f x * (y - x)) \ e / 2 * cmod (y - x)" - apply (rule has_contour_integral_bound_linepath [where B = "e/2"]) - using e apply simp - apply (rule d1_less [THEN less_imp_le]) - using close segment_bound - apply force - done + proof (rule has_contour_integral_bound_linepath) + show "\u. u \ closed_segment x y \ cmod (f u - f x) \ e / 2" + by (meson close d1_less le_less_trans less_imp_le min.strict_boundedE segment_bound1) + qed (use e in simp) also have "... < e * cmod (y - x)" by (simp add: e yx) finally have "cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" @@ -2731,9 +2724,7 @@ show ?thesis apply (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right) apply (rule Lim_transform [OF * Lim_eventually]) - apply (simp add: inverse_eq_divide [symmetric] eventually_at) - using \open s\ x - apply (force simp: dist_norm open_contains_ball) + using \open S\ x apply (force simp: dist_norm open_contains_ball inverse_eq_divide [symmetric] eventually_at) done qed @@ -2741,25 +2732,22 @@ lemma holomorphic_starlike_primitive: fixes f :: "complex \ complex" - assumes contf: "continuous_on s f" - and s: "starlike s" and os: "open s" + assumes contf: "continuous_on S f" + and S: "starlike S" and os: "open S" and k: "finite k" - and fcd: "\x. x \ s - k \ f field_differentiable at x" - shows "\g. \x \ s. (g has_field_derivative f x) (at x)" + and fcd: "\x. x \ S - k \ f field_differentiable at x" + shows "\g. \x \ S. (g has_field_derivative f x) (at x)" proof - - obtain a where a: "a\s" and a_cs: "\x. x\s \ closed_segment a x \ s" - using s by (auto simp: starlike_def) + obtain a where a: "a\S" and a_cs: "\x. x\S \ closed_segment a x \ S" + using S by (auto simp: starlike_def) { fix x b c - assume "x \ s" "closed_segment b c \ s" - then have abcs: "convex hull {a, b, c} \ s" + assume "x \ S" "closed_segment b c \ S" + then have abcs: "convex hull {a, b, c} \ S" by (simp add: a a_cs starlike_convex_subset) - then have *: "continuous_on (convex hull {a, b, c}) f" + then have "continuous_on (convex hull {a, b, c}) f" by (simp add: continuous_on_subset [OF contf]) - have "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" - apply (rule Cauchy_theorem_triangle_cofinite [OF _ k]) - using abcs apply (simp add: continuous_on_subset [OF contf]) - using * abcs interior_subset apply (auto intro: fcd) - done + then have "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" + using abcs interior_subset by (force intro: fcd Cauchy_theorem_triangle_cofinite [OF _ k]) } note 0 = this show ?thesis apply (intro exI ballI) @@ -2769,15 +2757,15 @@ done qed -lemma Cauchy_theorem_starlike: - "\open s; starlike s; finite k; continuous_on s f; - \x. x \ s - k \ f field_differentiable at x; - valid_path g; path_image g \ s; pathfinish g = pathstart g\ +corollary Cauchy_theorem_starlike: + "\open S; starlike S; finite k; continuous_on S f; + \x. x \ S - k \ f field_differentiable at x; + valid_path g; path_image g \ S; pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" by (metis holomorphic_starlike_primitive Cauchy_theorem_primitive at_within_open) -lemma Cauchy_theorem_starlike_simple: - "\open s; starlike s; f holomorphic_on s; valid_path g; path_image g \ s; pathfinish g = pathstart g\ +corollary Cauchy_theorem_starlike_simple: + "\open S; starlike S; f holomorphic_on S; valid_path g; path_image g \ S; pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" apply (rule Cauchy_theorem_starlike [OF _ _ finite.emptyI]) apply (simp_all add: holomorphic_on_imp_continuous_on) @@ -2790,56 +2778,54 @@ text\For a convex set we can avoid assuming openness and boundary analyticity\ lemma triangle_contour_integrals_convex_primitive: - assumes contf: "continuous_on s f" - and s: "a \ s" "convex s" - and x: "x \ s" - and zer: "\b c. \b \ s; c \ s\ + assumes contf: "continuous_on S f" + and S: "a \ S" "convex S" + and x: "x \ S" + and zer: "\b c. \b \ S; c \ S\ \ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0" - shows "((\x. contour_integral(linepath a x) f) has_field_derivative f x) (at x within s)" + shows "((\x. contour_integral(linepath a x) f) has_field_derivative f x) (at x within S)" proof - let ?pathint = "\x y. contour_integral(linepath x y) f" { fix y - assume y: "y \ s" + assume y: "y \ S" have cont_ayf: "continuous_on (closed_segment a y) f" - using s y by (meson contf continuous_on_subset convex_contains_segment) - have xys: "closed_segment x y \ s" (*?*) - using convex_contains_segment s x y by auto + using S y by (meson contf continuous_on_subset convex_contains_segment) + have xys: "closed_segment x y \ S" (*?*) + using convex_contains_segment S x y by auto have "?pathint a y - ?pathint a x = ?pathint x y" using zer [OF x y] contour_integral_reverse_linepath [OF cont_ayf] add_eq_0_iff by force } note [simp] = this { fix e::real assume e: "0 < e" - have cont_atx: "continuous (at x within s) f" - using x s contf by (simp add: continuous_on_eq_continuous_within) - then obtain d1 where d1: "d1>0" and d1_less: "\y. \y \ s; cmod (y - x) < d1\ \ cmod (f y - f x) < e/2" + have cont_atx: "continuous (at x within S) f" + using x S contf by (simp add: continuous_on_eq_continuous_within) + then obtain d1 where d1: "d1>0" and d1_less: "\y. \y \ S; cmod (y - x) < d1\ \ cmod (f y - f x) < e/2" unfolding continuous_within Lim_within dist_norm using e by (drule_tac x="e/2" in spec) force { fix y - assume yx: "y \ x" and close: "cmod (y - x) < d1" and y: "y \ s" + assume yx: "y \ x" and close: "cmod (y - x) < d1" and y: "y \ S" have fxy: "f contour_integrable_on linepath x y" - using convex_contains_segment s x y + using convex_contains_segment S x y by (blast intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf]) then obtain i where i: "(f has_contour_integral i) (linepath x y)" by (auto simp: contour_integrable_on_def) then have "((\w. f w - f x) has_contour_integral (i - f x * (y - x))) (linepath x y)" by (rule has_contour_integral_diff [OF _ has_contour_integral_const_linepath]) then have "cmod (i - f x * (y - x)) \ e / 2 * cmod (y - x)" - apply (rule has_contour_integral_bound_linepath [where B = "e/2"]) - using e apply simp - apply (rule d1_less [THEN less_imp_le]) - using convex_contains_segment s(2) x y apply blast - using close segment_bound(1) apply fastforce - done + proof (rule has_contour_integral_bound_linepath) + show "\u. u \ closed_segment x y \ cmod (f u - f x) \ e / 2" + by (meson assms(3) close convex_contains_segment d1_less le_less_trans less_imp_le segment_bound1 subset_iff x y) + qed (use e in simp) also have "... < e * cmod (y - x)" by (simp add: e yx) finally have "cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" using i yx by (simp add: contour_integral_unique divide_less_eq) } - then have "\d>0. \y\s. y \ x \ cmod (y-x) < d \ cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" + then have "\d>0. \y\S. y \ x \ cmod (y-x) < d \ cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" using d1 by blast } - then have *: "((\y. (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) \ 0) (at x within s)" + then have *: "((\y. (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) \ 0) (at x within S)" by (simp add: Lim_within dist_norm inverse_eq_divide) show ?thesis apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right) @@ -2850,64 +2836,64 @@ qed lemma contour_integral_convex_primitive: - "\convex s; continuous_on s f; - \a b c. \a \ s; b \ s; c \ s\ \ (f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)\ - \ \g. \x \ s. (g has_field_derivative f x) (at x within s)" - apply (cases "s={}") - apply (simp_all add: ex_in_conv [symmetric]) - apply (blast intro: triangle_contour_integrals_convex_primitive has_chain_integral_chain_integral3) - done + assumes "convex S" "continuous_on S f" + "\a b c. \a \ S; b \ S; c \ S\ \ (f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" + obtains g where "\x. x \ S \ (g has_field_derivative f x) (at x within S)" +proof (cases "S={}") + case False + with assms that show ?thesis + by (blast intro: triangle_contour_integrals_convex_primitive has_chain_integral_chain_integral3) +qed auto lemma holomorphic_convex_primitive: fixes f :: "complex \ complex" - shows - "\convex s; finite k; continuous_on s f; - \x. x \ interior s - k \ f field_differentiable at x\ - \ \g. \x \ s. (g has_field_derivative f x) (at x within s)" -apply (rule contour_integral_convex_primitive [OF _ _ Cauchy_theorem_triangle_cofinite]) -prefer 3 -apply (erule continuous_on_subset) -apply (simp add: subset_hull continuous_on_subset, assumption+) -by (metis Diff_iff convex_contains_segment insert_absorb insert_subset interior_mono segment_convex_hull subset_hull) + assumes "convex S" "finite K" and contf: "continuous_on S f" + and fd: "\x. x \ interior S - K \ f field_differentiable at x" + obtains g where "\x. x \ S \ (g has_field_derivative f x) (at x within S)" +proof (rule contour_integral_convex_primitive [OF \convex S\ contf Cauchy_theorem_triangle_cofinite]) + have *: "convex hull {a, b, c} \ S" if "a \ S" "b \ S" "c \ S" for a b c + by (simp add: \convex S\ hull_minimal that) + show "continuous_on (convex hull {a, b, c}) f" if "a \ S" "b \ S" "c \ S" for a b c + by (meson "*" contf continuous_on_subset that) + show "f field_differentiable at x" if "a \ S" "b \ S" "c \ S" "x \ interior (convex hull {a, b, c}) - K" for a b c x + by (metis "*" DiffD1 DiffD2 DiffI fd interior_mono subsetCE that) +qed (use assms in \force+\) lemma holomorphic_convex_primitive': fixes f :: "complex \ complex" - assumes "convex s" and "open s" and "f holomorphic_on s" - shows "\g. \x \ s. (g has_field_derivative f x) (at x within s)" + assumes "convex S" and "open S" and "f holomorphic_on S" + obtains g where "\x. x \ S \ (g has_field_derivative f x) (at x within S)" proof (rule holomorphic_convex_primitive) - fix x assume "x \ interior s - {}" + fix x assume "x \ interior S - {}" with assms show "f field_differentiable at x" by (auto intro!: holomorphic_on_imp_differentiable_at simp: interior_open) -qed (insert assms, auto intro: holomorphic_on_imp_continuous_on) - -lemma Cauchy_theorem_convex: - "\continuous_on s f; convex s; finite k; - \x. x \ interior s - k \ f field_differentiable at x; - valid_path g; path_image g \ s; - pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" +qed (use assms in \auto intro: holomorphic_on_imp_continuous_on\) + +corollary Cauchy_theorem_convex: + "\continuous_on S f; convex S; finite K; + \x. x \ interior S - K \ f field_differentiable at x; + valid_path g; path_image g \ S; pathfinish g = pathstart g\ + \ (f has_contour_integral 0) g" by (metis holomorphic_convex_primitive Cauchy_theorem_primitive) -lemma Cauchy_theorem_convex_simple: - "\f holomorphic_on s; convex s; - valid_path g; path_image g \ s; +corollary Cauchy_theorem_convex_simple: + "\f holomorphic_on S; convex S; + valid_path g; path_image g \ S; pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" - apply (rule Cauchy_theorem_convex) + apply (rule Cauchy_theorem_convex [where K = "{}"]) apply (simp_all add: holomorphic_on_imp_continuous_on) - apply (rule finite.emptyI) using at_within_interior holomorphic_on_def interior_subset by fastforce text\In particular for a disc\ -lemma Cauchy_theorem_disc: - "\finite k; continuous_on (cball a e) f; - \x. x \ ball a e - k \ f field_differentiable at x; +corollary Cauchy_theorem_disc: + "\finite K; continuous_on (cball a e) f; + \x. x \ ball a e - K \ f field_differentiable at x; valid_path g; path_image g \ cball a e; pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" - apply (rule Cauchy_theorem_convex) - apply (auto simp: convex_cball interior_cball) - done - -lemma Cauchy_theorem_disc_simple: + by (auto intro: Cauchy_theorem_convex) + +corollary Cauchy_theorem_disc_simple: "\f holomorphic_on (ball a e); valid_path g; path_image g \ ball a e; pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" by (simp add: Cauchy_theorem_convex_simple) @@ -2991,35 +2977,34 @@ proof - { fix z assume z: "z \ s" - obtain d where d: "d>0" "ball z d \ s" using \open s\ z + obtain d where "d>0" and d: "ball z d \ s" using \open s\ z by (auto simp: open_contains_ball) then have contfb: "continuous_on (ball z d) f" using contf continuous_on_subset by blast obtain h where "\y\ball z d. (h has_field_derivative f y) (at y within ball z d)" - using holomorphic_convex_primitive [OF convex_ball k contfb fcd] d - interior_subset by force + by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff set_mp) then have "\y\ball z d. (h has_field_derivative f y) (at y within s)" - by (metis open_ball at_within_open d(2) os subsetCE) + by (metis open_ball at_within_open d os subsetCE) then have "\h. (\y. cmod (y - z) < d \ (h has_field_derivative f y) (at y within s))" by (force simp: dist_norm norm_minus_commute) then have "\d h. 0 < d \ (\y. cmod (y - z) < d \ (h has_field_derivative f y) (at y within s))" - using d by blast + using \0 < d\ by blast } then show ?thesis by (rule contour_integral_local_primitive [OF g]) qed lemma contour_integrable_holomorphic_simple: - assumes fh: "f holomorphic_on s" - and os: "open s" - and g: "valid_path g" "path_image g \ s" + assumes fh: "f holomorphic_on S" + and os: "open S" + and g: "valid_path g" "path_image g \ S" shows "f contour_integrable_on g" apply (rule contour_integrable_holomorphic [OF _ os Finite_Set.finite.emptyI g]) apply (simp add: fh holomorphic_on_imp_continuous_on) using fh by (simp add: field_differentiable_def holomorphic_on_open os) lemma continuous_on_inversediff: - fixes z:: "'a::real_normed_field" shows "z \ s \ continuous_on s (\w. 1 / (w - z))" + fixes z:: "'a::real_normed_field" shows "z \ S \ continuous_on S (\w. 1 / (w - z))" by (rule continuous_intros | force)+ corollary contour_integrable_inversediff: @@ -3046,18 +3031,17 @@ text\This formulation covers two cases: @{term g} and @{term h} share their start and end points; @{term g} and @{term h} both loop upon themselves.\ lemma contour_integral_nearby: - assumes os: "open s" and p: "path p" "path_image p \ s" - shows - "\d. 0 < d \ + assumes os: "open S" and p: "path p" "path_image p \ S" + shows "\d. 0 < d \ (\g h. valid_path g \ valid_path h \ (\t \ {0..1}. norm(g t - p t) < d \ norm(h t - p t) < d) \ linked_paths atends g h - \ path_image g \ s \ path_image h \ s \ - (\f. f holomorphic_on s \ contour_integral h f = contour_integral g f))" + \ path_image g \ S \ path_image h \ S \ + (\f. f holomorphic_on S \ contour_integral h f = contour_integral g f))" proof - - have "\z. \e. z \ path_image p \ 0 < e \ ball z e \ s" + have "\z. \e. z \ path_image p \ 0 < e \ ball z e \ S" using open_contains_ball os p(2) by blast - then obtain ee where ee: "\z. z \ path_image p \ 0 < ee z \ ball z (ee z) \ s" + then obtain ee where ee: "\z. z \ path_image p \ 0 < ee z \ ball z (ee z) \ S" by metis define cover where "cover = (\z. ball z (ee z/3)) ` (path_image p)" have "compact (path_image p)" @@ -3081,19 +3065,23 @@ define e where "e = Min((ee o p) ` k)" have fin_eep: "finite ((ee o p) ` k)" using k by blast - have enz: "0 < e" + have "0 < e" using ee k by (simp add: kne e_def Min_gr_iff [OF fin_eep] eepi) have "uniformly_continuous_on {0..1} p" using p by (simp add: path_def compact_uniformly_continuous) then obtain d::real where d: "d>0" and de: "\x x'. \x' - x\ < d \ x\{0..1} \ x'\{0..1} \ cmod (p x' - p x) < e/3" unfolding uniformly_continuous_on_def dist_norm real_norm_def - by (metis divide_pos_pos enz zero_less_numeral) + by (metis divide_pos_pos \0 < e\ zero_less_numeral) then obtain N::nat where N: "N>0" "inverse N < d" using real_arch_inverse [of d] by auto - { fix g h - assume g: "valid_path g" and gp: "\t\{0..1}. cmod (g t - p t) < e / 3" - and h: "valid_path h" and hp: "\t\{0..1}. cmod (h t - p t) < e / 3" + show ?thesis + proof (intro exI conjI allI; clarify?) + show "e/3 > 0" + using \0 < e\ by simp + fix g h + assume g: "valid_path g" and ghp: "\t\{0..1}. cmod (g t - p t) < e / 3 \ cmod (h t - p t) < e / 3" + and h: "valid_path h" and joins: "linked_paths atends g h" { fix t::real assume t: "0 \ t" "t \ 1" @@ -3102,7 +3090,7 @@ then have ele: "e \ ee (p u)" using fin_eep by (simp add: e_def) have "cmod (g t - p t) < e / 3" "cmod (h t - p t) < e / 3" - using gp hp t by auto + using ghp t by auto with ele have "cmod (g t - p t) < ee (p u) / 3" "cmod (h t - p t) < ee (p u) / 3" by linarith+ @@ -3110,18 +3098,18 @@ using norm_diff_triangle_ineq [of "g t" "p t" "p t" "p u"] norm_diff_triangle_ineq [of "h t" "p t" "p t" "p u"] ptu eepi u by (force simp: dist_norm ball_def norm_minus_commute)+ - then have "g t \ s" "h t \ s" using ee u k + then have "g t \ S" "h t \ S" using ee u k by (auto simp: path_image_def ball_def) } - then have ghs: "path_image g \ s" "path_image h \ s" + then have ghs: "path_image g \ S" "path_image h \ S" by (auto simp: path_image_def) moreover { fix f - assume fhols: "f holomorphic_on s" + assume fhols: "f holomorphic_on S" then have fpa: "f contour_integrable_on g" "f contour_integrable_on h" using g ghs h holomorphic_on_imp_continuous_on os contour_integrable_holomorphic_simple by blast+ - have contf: "continuous_on s f" + have contf: "continuous_on S f" by (simp add: fhols holomorphic_on_imp_continuous_on) { fix z assume z: "z \ path_image p" @@ -3156,41 +3144,38 @@ then have x01: "0 \ x" "x \ 1" using x by linarith+ have "cmod (p t - p x) < ee (p t) / 3 + e/3" - apply (rule norm_diff_triangle_less [OF ptu de]) - using x N x01 Suc.prems - apply (auto simp: field_simps) - done + proof (rule norm_diff_triangle_less [OF ptu de]) + show "\real n / real N - x\ < d" + using x N by (auto simp: field_simps) + qed (use x01 Suc.prems in auto) then have ptx: "cmod (p t - p x) < 2*ee (p t)/3" using e3le eepi [OF t] by simp have "cmod (p t - g x) < 2*ee (p t)/3 + e/3 " apply (rule norm_diff_triangle_less [OF ptx]) - using gp x01 by (simp add: norm_minus_commute) + using ghp x01 by (simp add: norm_minus_commute) also have "... \ ee (p t)" using e3le eepi [OF t] by simp finally have gg: "cmod (p t - g x) < ee (p t)" . have "cmod (p t - h x) < 2*ee (p t)/3 + e/3 " apply (rule norm_diff_triangle_less [OF ptx]) - using hp x01 by (simp add: norm_minus_commute) + using ghp x01 by (simp add: norm_minus_commute) also have "... \ ee (p t)" using e3le eepi [OF t] by simp finally have "cmod (p t - g x) < ee (p t)" "cmod (p t - h x) < ee (p t)" using gg by auto } note ptgh_ee = this - have pi_hgn: "path_image (linepath (h (n/N)) (g (n/N))) \ ball (p t) (ee (p t))" + have "closed_segment (g (real n / real N)) (h (real n / real N)) = path_image (linepath (h (n/N)) (g (n/N)))" + by (simp add: closed_segment_commute) + also have pi_hgn: "\ \ ball (p t) (ee (p t))" using ptgh_ee [of "n/N"] Suc.prems by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"]) - then have gh_ns: "closed_segment (g (n/N)) (h (n/N)) \ s" - using \N>0\ Suc.prems - apply (simp add: path_image_join field_simps closed_segment_commute) - apply (erule order_trans) - apply (simp add: ee pi t) - done - have pi_ghn': "path_image (linepath (g ((1 + n) / N)) (h ((1 + n) / N))) - \ ball (p t) (ee (p t))" + finally have gh_ns: "closed_segment (g (n/N)) (h (n/N)) \ S" + using ee pi t by blast + have pi_ghn': "path_image (linepath (g ((1 + n) / N)) (h ((1 + n) / N))) \ ball (p t) (ee (p t))" using ptgh_ee [of "(1+n)/N"] Suc.prems by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"]) - then have gh_n's: "closed_segment (g ((1 + n) / N)) (h ((1 + n) / N)) \ s" + then have gh_n's: "closed_segment (g ((1 + n) / N)) (h ((1 + n) / N)) \ S" using \N>0\ Suc.prems ee pi t by (auto simp: Path_Connected.path_image_join field_simps) have pi_subset_ball: @@ -3206,8 +3191,7 @@ subpath ((Suc n) / N) (n/N) h +++ linepath(h (n/N)) (g (n/N)))" apply (rule Cauchy_theorem_primitive [of "ball(p t) (ee(p t))" "ff (p t)" "f"]) apply (metis ff open_ball at_within_open pi t) - apply (intro valid_path_join) - using Suc.prems pi_subset_ball apply (simp_all add: valid_path_subpath g h) + using Suc.prems pi_subset_ball apply (simp_all add: valid_path_join valid_path_subpath g h) done have fpa1: "f contour_integrable_on subpath (real n / real N) (real (Suc n) / real N) g" using Suc.prems by (simp add: contour_integrable_subpath g fpa) @@ -3252,38 +3236,31 @@ by (simp add: linked_paths_def pathstart_def pathfinish_def split: if_split_asm) } ultimately - have "path_image g \ s \ path_image h \ s \ (\f. f holomorphic_on s \ contour_integral h f = contour_integral g f)" + show "path_image g \ S \ path_image h \ S \ (\f. f holomorphic_on S \ contour_integral h f = contour_integral g f)" by metis - } note * = this - show ?thesis - apply (rule_tac x="e/3" in exI) - apply (rule conjI) - using enz apply simp - apply (clarsimp simp only: ball_conj_distrib) - apply (rule *; assumption) - done + qed qed lemma - assumes "open s" "path p" "path_image p \ s" + assumes "open S" "path p" "path_image p \ S" shows contour_integral_nearby_ends: "\d. 0 < d \ (\g h. valid_path g \ valid_path h \ (\t \ {0..1}. norm(g t - p t) < d \ norm(h t - p t) < d) \ pathstart h = pathstart g \ pathfinish h = pathfinish g - \ path_image g \ s \ - path_image h \ s \ - (\f. f holomorphic_on s + \ path_image g \ S \ + path_image h \ S \ + (\f. f holomorphic_on S \ contour_integral h f = contour_integral g f))" and contour_integral_nearby_loops: "\d. 0 < d \ (\g h. valid_path g \ valid_path h \ (\t \ {0..1}. norm(g t - p t) < d \ norm(h t - p t) < d) \ pathfinish g = pathstart g \ pathfinish h = pathstart h - \ path_image g \ s \ - path_image h \ s \ - (\f. f holomorphic_on s + \ path_image g \ S \ + path_image h \ S \ + (\f. f holomorphic_on S \ contour_integral h f = contour_integral g f))" using contour_integral_nearby [OF assms, where atends=True] using contour_integral_nearby [OF assms, where atends=False] @@ -3291,7 +3268,7 @@ lemma C1_differentiable_polynomial_function: fixes p :: "real \ 'a::euclidean_space" - shows "polynomial_function p \ p C1_differentiable_on s" + shows "polynomial_function p \ p C1_differentiable_on S" by (metis continuous_on_polymonial_function C1_differentiable_on_def has_vector_derivative_polynomial_function) lemma valid_path_polynomial_function: @@ -3305,54 +3282,54 @@ by (simp add: subpath_def valid_path_polynomial_function) lemma contour_integral_bound_exists: -assumes s: "open s" +assumes S: "open S" and g: "valid_path g" - and pag: "path_image g \ s" + and pag: "path_image g \ S" shows "\L. 0 < L \ - (\f B. f holomorphic_on s \ (\z \ s. norm(f z) \ B) - \ norm(contour_integral g f) \ L*B)" + (\f B. f holomorphic_on S \ (\z \ S. norm(f z) \ B) + \ norm(contour_integral g f) \ L*B)" proof - -have "path g" using g - by (simp add: valid_path_imp_path) -then obtain d::real and p - where d: "0 < d" - and p: "polynomial_function p" "path_image p \ s" - and pi: "\f. f holomorphic_on s \ contour_integral g f = contour_integral p f" - using contour_integral_nearby_ends [OF s \path g\ pag] - apply clarify - apply (drule_tac x=g in spec) - apply (simp only: assms) - apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function) - done -then obtain p' where p': "polynomial_function p'" - "\x. (p has_vector_derivative (p' x)) (at x)" - by (blast intro: has_vector_derivative_polynomial_function that elim: ) -then have "bounded(p' ` {0..1})" - using continuous_on_polymonial_function - by (force simp: intro!: compact_imp_bounded compact_continuous_image) -then obtain L where L: "L>0" and nop': "\x. x \ {0..1} \ norm (p' x) \ L" - by (force simp: bounded_pos) -{ fix f B - assume f: "f holomorphic_on s" - and B: "\z. z\s \ cmod (f z) \ B" - then have "f contour_integrable_on p \ valid_path p" - using p s - by (blast intro: valid_path_polynomial_function contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on) - moreover have "\x. x \ {0..1} \ cmod (vector_derivative p (at x)) * cmod (f (p x)) \ L * B" - apply (rule mult_mono) - apply (subst Derivative.vector_derivative_at; force intro: p' nop') - using L B p - apply (auto simp: path_image_def image_subset_iff) + have "path g" using g + by (simp add: valid_path_imp_path) + then obtain d::real and p + where d: "0 < d" + and p: "polynomial_function p" "path_image p \ S" + and pi: "\f. f holomorphic_on S \ contour_integral g f = contour_integral p f" + using contour_integral_nearby_ends [OF S \path g\ pag] + apply clarify + apply (drule_tac x=g in spec) + apply (simp only: assms) + apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function) done - ultimately have "cmod (contour_integral g f) \ L * B" - apply (simp add: pi [OF f]) - apply (simp add: contour_integral_integral) - apply (rule order_trans [OF integral_norm_bound_integral]) - apply (auto simp: mult.commute integral_norm_bound_integral contour_integrable_on [symmetric] norm_mult) - done -} then -show ?thesis - by (force simp: L contour_integral_integral) + then obtain p' where p': "polynomial_function p'" + "\x. (p has_vector_derivative (p' x)) (at x)" + by (blast intro: has_vector_derivative_polynomial_function that elim: ) + then have "bounded(p' ` {0..1})" + using continuous_on_polymonial_function + by (force simp: intro!: compact_imp_bounded compact_continuous_image) + then obtain L where L: "L>0" and nop': "\x. \0 \ x; x \ 1\ \ norm (p' x) \ L" + by (force simp: bounded_pos) + { fix f B + assume f: "f holomorphic_on S" and B: "\z. z\S \ cmod (f z) \ B" + then have "f contour_integrable_on p \ valid_path p" + using p S + by (blast intro: valid_path_polynomial_function contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on) + moreover have "cmod (vector_derivative p (at x)) * cmod (f (p x)) \ L * B" if "0 \ x" "x \ 1" for x + proof (rule mult_mono) + show "cmod (vector_derivative p (at x)) \ L" + by (metis nop' p'(2) that vector_derivative_at) + show "cmod (f (p x)) \ B" + by (metis B atLeastAtMost_iff imageI p(2) path_defs(4) subset_eq that) + qed (use \L>0\ in auto) + ultimately have "cmod (contour_integral g f) \ L * B" + apply (simp only: pi [OF f]) + apply (simp only: contour_integral_integral) + apply (rule order_trans [OF integral_norm_bound_integral]) + apply (auto simp: mult.commute integral_norm_bound_integral contour_integrable_on [symmetric] norm_mult) + done + } then + show ?thesis + by (force simp: L contour_integral_integral) qed text\We can treat even non-rectifiable paths as having a "length" for bounds on analytic functions in open sets.\ @@ -3362,10 +3339,10 @@ definition winding_number:: "[real \ complex, complex] \ complex" where "winding_number \ z \ SOME n. \e > 0. \p. valid_path p \ z \ path_image p \ - pathstart p = pathstart \ \ - pathfinish p = pathfinish \ \ - (\t \ {0..1}. norm(\ t - p t) < e) \ - contour_integral p (\w. 1/(w - z)) = 2 * pi * \ * n" + pathstart p = pathstart \ \ + pathfinish p = pathfinish \ \ + (\t \ {0..1}. norm(\ t - p t) < e) \ + contour_integral p (\w. 1/(w - z)) = 2 * pi * \ * n" lemma winding_number: assumes "path \" "z \ path_image \" "0 < e" @@ -3447,9 +3424,10 @@ have "2 * complex_of_real pi * \ * n = contour_integral p (\w. 1 / (w - z))" using p by auto also have "... = contour_integral q (\w. 1 / (w - z))" - apply (rule pi_eq) - using p q - by (auto simp: valid_path_polynomial_function norm_minus_commute intro!: holomorphic_intros) + proof (rule pi_eq) + show "(\w. 1 / (w - z)) holomorphic_on UNIV - {z}" + by (auto intro!: holomorphic_intros) + qed (use p q in \auto simp: norm_minus_commute\) also have "... = 2 * complex_of_real pi * \ * winding_number \ z" using q by auto finally have "2 * complex_of_real pi * \ * n = 2 * complex_of_real pi * \ * winding_number \ z" . @@ -3490,9 +3468,10 @@ have "2 * complex_of_real pi * \ * n = contour_integral p (\w. 1 / (w - z))" using p by auto also have "... = contour_integral q (\w. 1 / (w - z))" - apply (rule pi_eq) - using p q loop - by (auto simp: valid_path_polynomial_function norm_minus_commute intro!: holomorphic_intros) + proof (rule pi_eq) + show "(\w. 1 / (w - z)) holomorphic_on UNIV - {z}" + by (auto intro!: holomorphic_intros) + qed (use p q loop in \auto simp: norm_minus_commute\) also have "... = 2 * complex_of_real pi * \ * winding_number \ z" using q by auto finally have "2 * complex_of_real pi * \ * n = 2 * complex_of_real pi * \ * winding_number \ z" . @@ -3561,8 +3540,7 @@ shows "winding_number(linepath a b) z = winding_number(linepath a c) z + winding_number(linepath c b) z" proof - have "z \ closed_segment a c" "z \ closed_segment c b" - using assms apply (meson convex_contains_segment convex_segment ends_in_segment(1) subsetCE) - using assms by (meson convex_contains_segment convex_segment ends_in_segment(2) subsetCE) + using assms by (meson convex_contains_segment convex_segment ends_in_segment subsetCE)+ then show ?thesis using assms by (simp add: winding_number_valid_path contour_integral_split_linepath [symmetric] continuous_on_inversediff field_simps) @@ -3607,11 +3585,11 @@ if "x \ {0..1} - S" for x proof - have "vector_derivative (uminus \ \) (at x within cbox 0 1) = - vector_derivative \ (at x within cbox 0 1)" - apply (rule vector_derivative_within_cbox) - using that - apply (auto simp: o_def) - apply (rule has_vector_derivative_minus) - by (metis C1_differentiable_on_def diff has_vector_derivative_at_within that vector_derivative_at_within_ivl zero_less_one) + proof (rule vector_derivative_within_cbox) + show "(uminus \ \ has_vector_derivative - vector_derivative \ (at x within cbox 0 1)) (at x within cbox 0 1)" + using that unfolding o_def + by (metis C1_differentiable_on_eq UNIV_I diff differentiable_subset has_vector_derivative_minus subsetI that vector_derivative_works) + qed (use that in auto) then show ?thesis by simp qed @@ -3663,20 +3641,19 @@ proof - have ge0: "0 \ Im (vector_derivative \ (at x) / (\ x - z))" if x: "0 < x" "x < 1" for x using ge by (simp add: Complex.Im_divide algebra_simps x) - have hi: "((\x. 1 / (\ x - z) * vector_derivative \ (at x)) has_integral contour_integral \ (\w. 1 / (w - z))) - (cbox 0 1)" + let ?vd = "\x. 1 / (\ x - z) * vector_derivative \ (at x)" + let ?int = "\z. contour_integral \ (\w. 1 / (w - z))" + have hi: "(?vd has_integral ?int z) (cbox 0 1)" unfolding box_real apply (subst has_contour_integral [symmetric]) using \ by (simp add: contour_integrable_inversediff has_contour_integral_integral) - have "0 \ Im (contour_integral \ (\w. 1 / (w - z)))" - apply (rule has_integral_component_nonneg - [of \ "\x. if x \ {0<..<1} - then 1/(\ x - z) * vector_derivative \ (at x) else 0", simplified]) - prefer 3 apply (force simp: ge0) - apply (simp add: Basis_complex_def) - apply (rule has_integral_spike_interior [OF hi]) - apply simp - done + have "0 \ Im (?int z)" + proof (rule has_integral_component_nonneg [of \, simplified]) + show "\x. x \ cbox 0 1 \ 0 \ Im (if 0 < x \ x < 1 then ?vd x else 0)" + by (force simp: ge0) + show "((\x. if 0 < x \ x < 1 then ?vd x else 0) has_integral ?int z) (cbox 0 1)" + by (rule has_integral_spike_interior [OF hi]) simp + qed then show ?thesis by (simp add: Re_winding_number [OF \] field_simps) qed @@ -3687,21 +3664,20 @@ and ge: "\x. \0 < x; x < 1\ \ e \ Im (vector_derivative \ (at x) / (\ x - z))" shows "0 < Re(winding_number \ z)" proof - - have hi: "((\x. 1 / (\ x - z) * vector_derivative \ (at x)) has_integral contour_integral \ (\w. 1 / (w - z))) - (cbox 0 1)" - unfolding box_real + let ?vd = "\x. 1 / (\ x - z) * vector_derivative \ (at x)" + let ?int = "\z. contour_integral \ (\w. 1 / (w - z))" + have hi: "(?vd has_integral ?int z) (cbox 0 1)" + unfolding box_real apply (subst has_contour_integral [symmetric]) using \ by (simp add: contour_integrable_inversediff has_contour_integral_integral) have "e \ Im (contour_integral \ (\w. 1 / (w - z)))" - apply (rule has_integral_component_le - [of \ "\x. \*e" "\*e" "{0..1}" - "\x. if x \ {0<..<1} then 1/(\ x - z) * vector_derivative \ (at x) else \*e" - "contour_integral \ (\w. 1/(w - z))", simplified]) - using e apply (simp_all add: Basis_complex_def) - using has_integral_const_real [of _ 0 1] apply force - apply (rule has_integral_spike_interior [OF hi, simplified box_real]) - apply (simp_all add: ge) - done + proof (rule has_integral_component_le [of \ "\x. \*e" "\*e" "{0..1}", simplified]) + show "((\x. if 0 < x \ x < 1 then ?vd x else \ * complex_of_real e) has_integral ?int z) {0..1}" + by (rule has_integral_spike_interior [OF hi, simplified box_real]) (use e in simp) + show "\x. 0 \ x \ x \ 1 \ + e \ Im (if 0 < x \ x < 1 then ?vd x else \ * complex_of_real e)" + by (simp add: ge) + qed (use has_integral_const_real [of _ 0 1] in auto) with e show ?thesis by (simp add: Re_winding_number [OF \] field_simps) qed @@ -3787,7 +3763,7 @@ by (auto simp: intro!: derivative_eq_intros) ultimately have "\h. \y. norm(y - w) < norm(w - z) \ (h has_field_derivative 1/(y - z)) (at y)" using holomorphic_convex_primitive [of "ball w (norm(w - z))" "{}" "\w. 1/(w - z)"] - by (simp add: field_differentiable_def Ball_def dist_norm at_within_open_NO_MATCH norm_minus_commute) + by (force simp add: field_differentiable_def Ball_def dist_norm at_within_open_NO_MATCH norm_minus_commute) } then obtain h where h: "\w y. w \ z \ norm(y - w) < norm(w - z) \ (h w has_field_derivative 1/(y - z)) (at y)" by meson @@ -4792,10 +4768,10 @@ have hq: "homotopic_loops (- {z}) h q" by (simp add: e hloop hq_less norm_minus_commute q valid_path_imp_path) have "contour_integral p (\w. 1/(w - z)) = contour_integral q (\w. 1/(w - z))" - apply (rule Cauchy_theorem_homotopic_loops [of "-{z}"]) - apply (blast intro: homotopic_loops_trans homotopic_loops_sym gp hq assms) - apply (auto intro!: holomorphic_intros simp: p q) - done + proof (rule Cauchy_theorem_homotopic_loops) + show "homotopic_loops (- {z}) p q" + by (blast intro: homotopic_loops_trans homotopic_loops_sym gp hq assms) + qed (auto intro!: holomorphic_intros simp: p q) then show ?thesis by (simp add: pap paq) qed @@ -6043,14 +6019,14 @@ using s \z \ s\ by (force simp add: open_contains_ball) have fde: "continuous_on (ball z (min d e)) f" by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI) - have "\g. \w \ ball z (min d e). (g has_field_derivative f w) (at w within ball z (min d e))" + obtain g where "\w. w \ ball z (min d e) \ (g has_field_derivative f w) (at w within ball z (min d e))" apply (rule contour_integral_convex_primitive [OF convex_ball fde]) apply (rule Cauchy_theorem_triangle_cofinite [OF _ k]) apply (metis continuous_on_subset [OF fde] closed_segment_subset convex_ball starlike_convex_subset) apply (rule cdf) apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset interior_mono interior_subset subset_hull) - done + by auto then have "f holomorphic_on ball z (min d e)" by (metis open_ball at_within_open derivative_is_holomorphic) then show ?thesis @@ -7140,7 +7116,7 @@ by (rule no_isolated_singularity) (auto simp: u) qed have cint_fxy: "(\x. (f x - f y) / (x - y)) contour_integrable_on \" if "y \ path_image \" for y - apply (rule contour_integrable_holomorphic_simple [where s = "u-{y}"]) + apply (rule contour_integrable_holomorphic_simple [where S = "u-{y}"]) using \valid_path \\ pasz apply (auto simp: u open_delete) apply (rule continuous_intros holomorphic_intros continuous_on_subset [OF conf] holomorphic_on_subset [OF holf] | @@ -7150,7 +7126,7 @@ "h z = (if z \ u then contour_integral \ (d z) else contour_integral \ (\w. f w/(w - z)))" for z have U: "\z. z \ u \ ((d z) has_contour_integral h z) \" apply (simp add: h_def) - apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where s=u]]) + apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where S=u]]) using u pasz \valid_path \\ apply (auto intro: holomorphic_on_imp_continuous_on hol_d) done @@ -7176,7 +7152,7 @@ using * by (auto simp: divide_simps has_contour_integral_eq) moreover have "((\w. f w / (w - z)) has_contour_integral contour_integral \ (\w. f w / (w - z))) \" if "z \ u" - apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where s=u]]) + apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where S=u]]) using u pasz \valid_path \\ that apply (auto intro: holomorphic_on_imp_continuous_on hol_d) apply (rule continuous_intros conf holomorphic_intros holf | force)+ @@ -7531,7 +7507,7 @@ then have wn0: "\w. w \ S \ winding_number p w = 0" by (simp add: zero) show ?thesis - using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols + using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols by (metis wn_eq cint_eq has_contour_integral_eqpath cint_fw cint_eq) qed @@ -7599,11 +7575,11 @@ obtains g where "g holomorphic_on A" and "\x. x \ A \ exp (g x) = f x" proof - note f' = holomorphic_derivI [OF f(1) A(2)] - from A have "\g. \x\A. (g has_field_derivative (deriv f x / f x)) (at x within A)" - by (intro holomorphic_convex_primitive' holomorphic_intros f) auto - then obtain g where g: "\x. x \ A \ (g has_field_derivative deriv f x / f x) (at x)" - using A by (auto simp: at_within_open[of _ A]) - + obtain g where g: "\x. x \ A \ (g has_field_derivative deriv f x / f x) (at x)" + proof (rule holomorphic_convex_primitive' [OF A]) + show "(\x. deriv f x / f x) holomorphic_on A" + by (intro holomorphic_intros f A) + qed (auto simp: A at_within_open[of _ A]) define h where "h = (\x. -g z0 + ln (f z0) + g x)" from g and A have g_holo: "g holomorphic_on A" by (auto simp: holomorphic_on_def at_within_open[of _ A] field_differentiable_def) diff -r ce7855c7f5f4 -r d0a7ddf5450e src/HOL/Analysis/Conformal_Mappings.thy --- a/src/HOL/Analysis/Conformal_Mappings.thy Sun May 27 22:57:06 2018 +0100 +++ b/src/HOL/Analysis/Conformal_Mappings.thy Mon May 28 23:15:23 2018 +0100 @@ -1576,7 +1576,7 @@ by (simp add: continuous_on_subset) then have "(f has_contour_integral 0) (linepath a b +++ linepath b a' +++ linepath a' b' +++ linepath b' a)" - apply (rule Cauchy_theorem_convex [where k = "{}"]) + apply (rule Cauchy_theorem_convex [where K = "{}"]) apply (simp_all add: path_image_join convex_Int convex_halfspace_le \convex S\ fcd_le ab_le closed_segment_subset abc a'b' ba') by (metis \d \ a' = k\ \d \ b' = k\ convex_contains_segment convex_halfspace_le lek(1) mem_Collect_eq order_refl) @@ -1601,7 +1601,7 @@ have "continuous_on (S \ {x. k \ d \ x}) f" using contf by (simp add: continuous_on_subset) then have "(f has_contour_integral 0) (linepath a' c +++ linepath c b' +++ linepath b' a')" - apply (rule Cauchy_theorem_convex [where k = "{}"]) + apply (rule Cauchy_theorem_convex [where K = "{}"]) apply (simp_all add: path_image_join convex_Int convex_halfspace_ge \convex S\ fcd_ge closed_segment_subset abc a'b' a'c) by (metis \d \ a' = k\ b'c closed_segment_commute convex_contains_segment diff -r ce7855c7f5f4 -r d0a7ddf5450e src/HOL/Analysis/Euclidean_Space.thy --- a/src/HOL/Analysis/Euclidean_Space.thy Sun May 27 22:57:06 2018 +0100 +++ b/src/HOL/Analysis/Euclidean_Space.thy Mon May 28 23:15:23 2018 +0100 @@ -253,6 +253,12 @@ lemma DIM_complex[simp]: "DIM(complex) = 2" unfolding Basis_complex_def by simp +lemma complex_Basis_1 [iff]: "(1::complex) \ Basis" + by (simp add: Basis_complex_def) + +lemma complex_Basis_i [iff]: "\ \ Basis" + by (simp add: Basis_complex_def) + subsubsection%unimportant \Type @{typ "'a \ 'b"}\ instantiation%important prod :: (euclidean_space, euclidean_space) euclidean_space diff -r ce7855c7f5f4 -r d0a7ddf5450e src/HOL/Analysis/Fashoda_Theorem.thy --- a/src/HOL/Analysis/Fashoda_Theorem.thy Sun May 27 22:57:06 2018 +0100 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy Mon May 28 23:15:23 2018 +0100 @@ -536,17 +536,13 @@ case True then show ?L apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) - unfolding assms True - using \?R\ - apply (auto simp add: field_simps) + unfolding assms True using \?R\ apply (auto simp add: field_simps) done next case False then show ?L apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) - unfolding assms - using \?R\ - apply (auto simp add: field_simps) + unfolding assms using \?R\ apply (auto simp add: field_simps) done qed } diff -r ce7855c7f5f4 -r d0a7ddf5450e src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Sun May 27 22:57:06 2018 +0100 +++ b/src/HOL/Analysis/Path_Connected.thy Mon May 28 23:15:23 2018 +0100 @@ -2192,7 +2192,7 @@ then have "norm ((x \ b) *\<^sub>R b) = norm x" by simp with b have "\x \ b\ = norm x" - using norm_Basis by fastforce + using norm_Basis by (simp add: b) with xb show ?thesis apply (simp add: abs_if split: if_split_asm) apply (metis add.inverse_inverse real_vector.scale_minus_left xb)