# HG changeset patch # User paulson # Date 1448297874 0 # Node ID c4f6031f131054fe62e5d62f845598e2c9c533a6 # Parent d6b2d638af231aa96fb863a797a2e7d9937d2e4d New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning. diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Archimedean_Field.thy Mon Nov 23 16:57:54 2015 +0000 @@ -657,7 +657,7 @@ proof (cases "of_int m \ z") case True hence "\z - of_int (round z)\ \ \of_int (ceiling z) - z\" - unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith? + unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith? also have "of_int \z\ - z \ 0" by linarith with True have "\of_int (ceiling z) - z\ \ \z - of_int m\" by (simp add: ceiling_le_iff) @@ -665,7 +665,7 @@ next case False hence "\z - of_int (round z)\ \ \of_int (floor z) - z\" - unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith? + unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith? also have "z - of_int \z\ \ 0" by linarith with False have "\of_int (floor z) - z\ \ \z - of_int m\" by (simp add: le_floor_iff) diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Binomial.thy Mon Nov 23 16:57:54 2015 +0000 @@ -842,7 +842,7 @@ next case (Suc m) from Suc show ?case - by (simp add: algebra_simps distrib gbinomial_mult_1) + by (simp add: field_simps distrib gbinomial_mult_1) qed lemma binomial_symmetric: @@ -1131,7 +1131,7 @@ proof (induction m) case (Suc mm) hence "(\k\Suc mm. (r gchoose k) * (r / 2 - of_nat k)) = - (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: algebra_simps) + (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: field_simps) also have "\ = r * (r - 1 gchoose Suc mm) / 2" by (subst gbinomial_absorb_comp) (rule refl) also have "\ = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))" by (subst gbinomial_absorption [symmetric]) simp diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Int.thy --- a/src/HOL/Int.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Int.thy Mon Nov 23 16:57:54 2015 +0000 @@ -1263,27 +1263,29 @@ text \Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\"} and @{text "="})\ -lemmas le_divide_eq_numeral1 [simp] = +named_theorems divide_const_simps "simplification rules to simplify comparisons involving constant divisors" + +lemmas le_divide_eq_numeral1 [simp,divide_const_simps] = pos_le_divide_eq [of "numeral w", OF zero_less_numeral] neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w -lemmas divide_le_eq_numeral1 [simp] = +lemmas divide_le_eq_numeral1 [simp,divide_const_simps] = pos_divide_le_eq [of "numeral w", OF zero_less_numeral] neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w -lemmas less_divide_eq_numeral1 [simp] = +lemmas less_divide_eq_numeral1 [simp,divide_const_simps] = pos_less_divide_eq [of "numeral w", OF zero_less_numeral] neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w -lemmas divide_less_eq_numeral1 [simp] = +lemmas divide_less_eq_numeral1 [simp,divide_const_simps] = pos_divide_less_eq [of "numeral w", OF zero_less_numeral] neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w -lemmas eq_divide_eq_numeral1 [simp] = +lemmas eq_divide_eq_numeral1 [simp,divide_const_simps] = eq_divide_eq [of _ _ "numeral w"] eq_divide_eq [of _ _ "- numeral w"] for w -lemmas divide_eq_eq_numeral1 [simp] = +lemmas divide_eq_eq_numeral1 [simp,divide_const_simps] = divide_eq_eq [of _ "numeral w"] divide_eq_eq [of _ "- numeral w"] for w @@ -1292,36 +1294,33 @@ text\Simplify quotients that are compared with a literal constant.\ -lemmas le_divide_eq_numeral = +lemmas le_divide_eq_numeral [divide_const_simps] = le_divide_eq [of "numeral w"] le_divide_eq [of "- numeral w"] for w -lemmas divide_le_eq_numeral = +lemmas divide_le_eq_numeral [divide_const_simps] = divide_le_eq [of _ _ "numeral w"] divide_le_eq [of _ _ "- numeral w"] for w -lemmas less_divide_eq_numeral = +lemmas less_divide_eq_numeral [divide_const_simps] = less_divide_eq [of "numeral w"] less_divide_eq [of "- numeral w"] for w -lemmas divide_less_eq_numeral = +lemmas divide_less_eq_numeral [divide_const_simps] = divide_less_eq [of _ _ "numeral w"] divide_less_eq [of _ _ "- numeral w"] for w -lemmas eq_divide_eq_numeral = +lemmas eq_divide_eq_numeral [divide_const_simps] = eq_divide_eq [of "numeral w"] eq_divide_eq [of "- numeral w"] for w -lemmas divide_eq_eq_numeral = +lemmas divide_eq_eq_numeral [divide_const_simps] = divide_eq_eq [of _ _ "numeral w"] divide_eq_eq [of _ _ "- numeral w"] for w text\Not good as automatic simprules because they cause case splits.\ -lemmas divide_const_simps = - le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral - divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral - le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 +lemmas [divide_const_simps] = le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 subsection \The divides relation\ diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Library/Extended_Real.thy Mon Nov 23 16:57:54 2015 +0000 @@ -36,7 +36,7 @@ assume "x = bot" then show ?thesis by (simp add: trivial_limit_at_left_bot) next - assume x: "x \ bot" + assume x: "x \ bot" show ?thesis unfolding continuous_within proof (intro tendsto_at_left_sequentially[of bot]) @@ -54,7 +54,7 @@ shows "sup_continuous f \ (\x. continuous (at_left x) f) \ mono f" using sup_continuous_at_left[of f] continuous_at_left_imp_sup_continuous[of f] sup_continuous_mono[of f] by auto - + lemma continuous_at_right_imp_inf_continuous: fixes f :: "'a \ 'a::{complete_linorder, linorder_topology}" assumes "mono f" "\x. continuous (at_right x) f" @@ -73,7 +73,7 @@ assume "x = top" then show ?thesis by (simp add: trivial_limit_at_right_top) next - assume x: "x \ top" + assume x: "x \ top" show ?thesis unfolding continuous_within proof (intro tendsto_at_right_sequentially[of _ top]) @@ -593,7 +593,7 @@ by (cases x) auto lemma ereal_abs_leI: - fixes x y :: ereal + fixes x y :: ereal shows "\ x \ y; -x \ y \ \ \x\ \ y" by(cases x y rule: ereal2_cases)(simp_all) @@ -881,7 +881,7 @@ end -lemma [simp]: +lemma [simp]: shows ereal_1_times: "ereal 1 * x = x" and times_ereal_1: "x * ereal 1 = x" by(simp_all add: one_ereal_def[symmetric]) @@ -1034,7 +1034,7 @@ shows "c = d \ (d \ 0 \ a = b) \ a * c = b * d" by (cases "c = 0") simp_all -lemma ereal_right_mult_cong: +lemma ereal_right_mult_cong: fixes a b c :: ereal shows "c = d \ (d \ 0 \ a = b) \ c * a = d * b" by (cases "c = 0") simp_all @@ -1402,7 +1402,7 @@ by (cases x y rule: ereal2_cases) simp_all lemma ereal_diff_add_eq_diff_diff_swap: - fixes x y z :: ereal + fixes x y z :: ereal shows "\y\ \ \ \ x - (y + z) = x - y - z" by(cases x y z rule: ereal3_cases) simp_all @@ -1414,8 +1414,8 @@ lemma ereal_add_uminus_conv_diff: fixes x y z :: ereal shows "- x + y = y - x" by(cases x y rule: ereal2_cases) simp_all -lemma ereal_minus_diff_eq: - fixes x y :: ereal +lemma ereal_minus_diff_eq: + fixes x y :: ereal shows "\ x = \ \ y \ \; x = -\ \ y \ - \ \ \ - (x - y) = y - x" by(cases x y rule: ereal2_cases) simp_all @@ -1745,13 +1745,9 @@ end -lemma continuous_on_compose': - "continuous_on s f \ continuous_on t g \ f`s \ t \ continuous_on s (\x. g (f x))" - using continuous_on_compose[of s f g] continuous_on_subset[of t g "f`s"] by auto - lemma continuous_on_ereal[continuous_intros]: assumes f: "continuous_on s f" shows "continuous_on s (\x. ereal (f x))" - by (rule continuous_on_compose'[OF f continuous_onI_mono[of ereal UNIV]]) auto + by (rule continuous_on_compose2 [OF continuous_onI_mono[of ereal UNIV] f]) auto lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \ ((\x. ereal (f x)) ---> ereal x) F" using isCont_tendsto_compose[of x ereal f F] continuous_on_ereal[of UNIV "\x. x"] @@ -1807,7 +1803,7 @@ by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0]) then have "((\x. (- c) * f x) ---> (- c) * x) F" by (rule *) - from tendsto_uminus_ereal[OF this] show ?thesis + from tendsto_uminus_ereal[OF this] show ?thesis by simp qed (auto intro!: *) qed @@ -2119,7 +2115,7 @@ intro!: ereal_mult_left_mono c) qed -lemma countable_approach: +lemma countable_approach: fixes x :: ereal assumes "x \ -\" shows "\f. incseq f \ (\i::nat. f i < x) \ (f ----> x)" @@ -2129,7 +2125,7 @@ by (intro tendsto_intros LIMSEQ_inverse_real_of_nat) ultimately show ?thesis by (intro exI[of _ "\n. x - inverse (Suc n)"]) (auto simp: incseq_def) -next +next case PInf with LIMSEQ_SUP[of "\n::nat. ereal (real n)"] show ?thesis by (intro exI[of _ "\n. ereal (real n)"]) (auto simp: incseq_def SUP_nat_Infty) qed (simp add: assms) @@ -3275,7 +3271,7 @@ next fix i j assume "i \ I" "j \ I" from directed[OF \insert n N \ A\ this] guess k .. - then show "\k\I. f n i + (\l\N. f l j) \ f n k + (\l\N. f l k)" + then show "\k\I. f n i + (\l\N. f l j) \ f n k + (\l\N. f l k)" by (intro bexI[of _ k]) (auto intro!: ereal_add_mono setsum_mono) qed ultimately show ?case @@ -3475,7 +3471,7 @@ shows "X ----> L" proof - from 1 2 have "limsup X \ liminf X" by auto - hence 3: "limsup X = liminf X" + hence 3: "limsup X = liminf X" apply (subst eq_iff, rule conjI) by (rule Liminf_le_Limsup, auto) hence 4: "convergent (\n. ereal (X n))" @@ -3486,7 +3482,7 @@ finally have "lim (\n. ereal(X n)) = L" .. hence "(\n. ereal (X n)) ----> L" apply (elim subst) - by (subst convergent_LIMSEQ_iff [symmetric], rule 4) + by (subst convergent_LIMSEQ_iff [symmetric], rule 4) thus ?thesis by simp qed @@ -3642,14 +3638,14 @@ proof - have **: "((\x. ereal (inverse x)) ---> ereal 0) at_infinity" by (intro tendsto_intros tendsto_inverse_0) - + show ?thesis by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def) (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity intro!: filterlim_mono_eventually[OF **]) qed -lemma inverse_ereal_tendsto_pos: +lemma inverse_ereal_tendsto_pos: fixes x :: ereal assumes "0 < x" shows "inverse -- x --> inverse x" proof (cases x) diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Limits.thy Mon Nov 23 16:57:54 2015 +0000 @@ -631,7 +631,7 @@ unfolding continuous_def by (rule tendsto_diff) lemma continuous_on_diff [continuous_intros]: - fixes f g :: "'a::t2_space \ 'b::real_normed_vector" + fixes f g :: "_ \ 'b::real_normed_vector" shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x - g x)" unfolding continuous_on_def by (auto intro: tendsto_diff) diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Nov 23 16:57:54 2015 +0000 @@ -3,7 +3,7 @@ text\By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\ theory Cauchy_Integral_Thm -imports Complex_Transcendental Weierstrass +imports Complex_Transcendental Weierstrass Ordered_Euclidean_Space begin subsection \Piecewise differentiable functions\ @@ -553,33 +553,33 @@ text\piecewise differentiable function on [0,1]\ -definition has_path_integral :: "(complex \ complex) \ complex \ (real \ complex) \ bool" - (infixr "has'_path'_integral" 50) - where "(f has_path_integral i) g \ +definition has_contour_integral :: "(complex \ complex) \ complex \ (real \ complex) \ bool" + (infixr "has'_contour'_integral" 50) + where "(f has_contour_integral i) g \ ((\x. f(g x) * vector_derivative g (at x within {0..1})) has_integral i) {0..1}" -definition path_integrable_on - (infixr "path'_integrable'_on" 50) - where "f path_integrable_on g \ \i. (f has_path_integral i) g" - -definition path_integral - where "path_integral g f \ @i. (f has_path_integral i) g" - -lemma path_integral_unique: "(f has_path_integral i) g \ path_integral g f = i" - by (auto simp: path_integral_def has_path_integral_def integral_def [symmetric]) - -lemma has_path_integral_integral: - "f path_integrable_on i \ (f has_path_integral (path_integral i f)) i" - by (metis path_integral_unique path_integrable_on_def) - -lemma has_path_integral_unique: - "(f has_path_integral i) g \ (f has_path_integral j) g \ i = j" +definition contour_integrable_on + (infixr "contour'_integrable'_on" 50) + where "f contour_integrable_on g \ \i. (f has_contour_integral i) g" + +definition contour_integral + where "contour_integral g f \ @i. (f has_contour_integral i) g" + +lemma contour_integral_unique: "(f has_contour_integral i) g \ contour_integral g f = i" + by (auto simp: contour_integral_def has_contour_integral_def integral_def [symmetric]) + +lemma has_contour_integral_integral: + "f contour_integrable_on i \ (f has_contour_integral (contour_integral i f)) i" + by (metis contour_integral_unique contour_integrable_on_def) + +lemma has_contour_integral_unique: + "(f has_contour_integral i) g \ (f has_contour_integral j) g \ i = j" using has_integral_unique - by (auto simp: has_path_integral_def) - -lemma has_path_integral_integrable: "(f has_path_integral i) g \ f path_integrable_on g" - using path_integrable_on_def by blast + by (auto simp: has_contour_integral_def) + +lemma has_contour_integral_integrable: "(f has_contour_integral i) g \ f contour_integrable_on g" + using contour_integrable_on_def by blast (* Show that we can forget about the localized derivative.*) @@ -607,15 +607,15 @@ (\x. f (g x) * vector_derivative g (at x)) integrable_on {a..b}" by (simp add: integrable_on_def has_integral_localized_vector_derivative) -lemma has_path_integral: - "(f has_path_integral i) g \ +lemma has_contour_integral: + "(f has_contour_integral i) g \ ((\x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" - by (simp add: has_integral_localized_vector_derivative has_path_integral_def) - -lemma path_integrable_on: - "f path_integrable_on g \ + by (simp add: has_integral_localized_vector_derivative has_contour_integral_def) + +lemma contour_integrable_on: + "f contour_integrable_on g \ (\t. f(g t) * vector_derivative g (at t)) integrable_on {0..1}" - by (simp add: has_path_integral integrable_on_def path_integrable_on_def) + by (simp add: has_contour_integral integrable_on_def contour_integrable_on_def) subsection\Reversing a path\ @@ -640,9 +640,9 @@ lemma valid_path_reversepath: "valid_path(reversepath g) \ valid_path g" using valid_path_imp_reverse by force -lemma has_path_integral_reversepath: - assumes "valid_path g" "(f has_path_integral i) g" - shows "(f has_path_integral (-i)) (reversepath g)" +lemma has_contour_integral_reversepath: + assumes "valid_path g" "(f has_contour_integral i) g" + shows "(f has_contour_integral (-i)) (reversepath g)" proof - { fix s x assume xs: "g C1_differentiable_on ({0..1} - s)" "x \ op - 1 ` s" "0 \ x" "x \ 1" @@ -667,7 +667,7 @@ have 01: "{0..1::real} = cbox 0 1" by simp show ?thesis using assms - apply (auto simp: has_path_integral_def) + apply (auto simp: has_contour_integral_def) apply (drule has_integral_affinity01 [where m= "-1" and c=1]) apply (auto simp: reversepath_def valid_path_def piecewise_C1_differentiable_on_def) apply (drule has_integral_neg) @@ -676,17 +676,17 @@ done qed -lemma path_integrable_reversepath: - "valid_path g \ f path_integrable_on g \ f path_integrable_on (reversepath g)" - using has_path_integral_reversepath path_integrable_on_def by blast - -lemma path_integrable_reversepath_eq: - "valid_path g \ (f path_integrable_on (reversepath g) \ f path_integrable_on g)" - using path_integrable_reversepath valid_path_reversepath by fastforce - -lemma path_integral_reversepath: - "\valid_path g; f path_integrable_on g\ \ path_integral (reversepath g) f = -(path_integral g f)" - using has_path_integral_reversepath path_integrable_on_def path_integral_unique by blast +lemma contour_integrable_reversepath: + "valid_path g \ f contour_integrable_on g \ f contour_integrable_on (reversepath g)" + using has_contour_integral_reversepath contour_integrable_on_def by blast + +lemma contour_integrable_reversepath_eq: + "valid_path g \ (f contour_integrable_on (reversepath g) \ f contour_integrable_on g)" + using contour_integrable_reversepath valid_path_reversepath by fastforce + +lemma contour_integral_reversepath: + "\valid_path g; f contour_integrable_on g\ \ contour_integral (reversepath g) f = -(contour_integral g f)" + using has_contour_integral_reversepath contour_integrable_on_def contour_integral_unique by blast subsection\Joining two paths together\ @@ -733,10 +733,10 @@ shows "pathfinish g1 = pathstart g2 \ (valid_path(g1 +++ g2) \ valid_path g1 \ valid_path g2)" using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast -lemma has_path_integral_join: - assumes "(f has_path_integral i1) g1" "(f has_path_integral i2) g2" +lemma has_contour_integral_join: + assumes "(f has_contour_integral i1) g1" "(f has_contour_integral i2) g2" "valid_path g1" "valid_path g2" - shows "(f has_path_integral (i1 + i2)) (g1 +++ g2)" + shows "(f has_contour_integral (i1 + i2)) (g1 +++ g2)" proof - obtain s1 s2 where s1: "finite s1" "\x\{0..1} - s1. g1 differentiable at x" @@ -746,7 +746,7 @@ have 1: "((\x. f (g1 x) * vector_derivative g1 (at x)) has_integral i1) {0..1}" and 2: "((\x. f (g2 x) * vector_derivative g2 (at x)) has_integral i2) {0..1}" using assms - by (auto simp: has_path_integral) + by (auto simp: has_contour_integral) have i1: "((\x. (2*f (g1 (2*x))) * vector_derivative g1 (at (2*x))) has_integral i1) {0..1/2}" and i2: "((\x. (2*f (g2 (2*x - 1))) * vector_derivative g2 (at (2*x - 1))) has_integral i2) {1/2..1}" using has_integral_affinity01 [OF 1, where m= 2 and c=0, THEN has_integral_cmul [where c=2]] @@ -786,28 +786,28 @@ done ultimately show ?thesis - apply (simp add: has_path_integral) + apply (simp add: has_contour_integral) apply (rule has_integral_combine [where c = "1/2"], auto) done qed -lemma path_integrable_joinI: - assumes "f path_integrable_on g1" "f path_integrable_on g2" +lemma contour_integrable_joinI: + assumes "f contour_integrable_on g1" "f contour_integrable_on g2" "valid_path g1" "valid_path g2" - shows "f path_integrable_on (g1 +++ g2)" + shows "f contour_integrable_on (g1 +++ g2)" using assms - by (meson has_path_integral_join path_integrable_on_def) - -lemma path_integrable_joinD1: - assumes "f path_integrable_on (g1 +++ g2)" "valid_path g1" - shows "f path_integrable_on g1" + by (meson has_contour_integral_join contour_integrable_on_def) + +lemma contour_integrable_joinD1: + assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g1" + shows "f contour_integrable_on g1" proof - obtain s1 where s1: "finite s1" "\x\{0..1} - s1. g1 differentiable at x" using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) have "(\x. f ((g1 +++ g2) (x/2)) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}" using assms - apply (auto simp: path_integrable_on) + apply (auto simp: contour_integrable_on) apply (drule integrable_on_subcbox [where a=0 and b="1/2"]) apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified]) done @@ -824,22 +824,22 @@ done show ?thesis using s1 - apply (auto simp: path_integrable_on) + apply (auto simp: contour_integrable_on) apply (rule integrable_spike_finite [of "{0,1} \ s1", OF _ _ *]) apply (auto simp: joinpaths_def scaleR_conv_of_real g1) done qed -lemma path_integrable_joinD2: - assumes "f path_integrable_on (g1 +++ g2)" "valid_path g2" - shows "f path_integrable_on g2" +lemma contour_integrable_joinD2: + assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g2" + shows "f contour_integrable_on g2" proof - obtain s2 where s2: "finite s2" "\x\{0..1} - s2. g2 differentiable at x" using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) have "(\x. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}" using assms - apply (auto simp: path_integrable_on) + apply (auto simp: contour_integrable_on) apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto) apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified]) apply (simp add: image_affinity_atLeastAtMost_diff) @@ -859,23 +859,23 @@ done show ?thesis using s2 - apply (auto simp: path_integrable_on) + apply (auto simp: contour_integrable_on) apply (rule integrable_spike_finite [of "{0,1} \ s2", OF _ _ *]) apply (auto simp: joinpaths_def scaleR_conv_of_real g2) done qed -lemma path_integrable_join [simp]: +lemma contour_integrable_join [simp]: shows "\valid_path g1; valid_path g2\ - \ f path_integrable_on (g1 +++ g2) \ f path_integrable_on g1 \ f path_integrable_on g2" -using path_integrable_joinD1 path_integrable_joinD2 path_integrable_joinI by blast - -lemma path_integral_join [simp]: + \ f contour_integrable_on (g1 +++ g2) \ f contour_integrable_on g1 \ f contour_integrable_on g2" +using contour_integrable_joinD1 contour_integrable_joinD2 contour_integrable_joinI by blast + +lemma contour_integral_join [simp]: shows - "\f path_integrable_on g1; f path_integrable_on g2; valid_path g1; valid_path g2\ - \ path_integral (g1 +++ g2) f = path_integral g1 f + path_integral g2 f" - by (simp add: has_path_integral_integral has_path_integral_join path_integral_unique) + "\f contour_integrable_on g1; f contour_integrable_on g2; valid_path g1; valid_path g2\ + \ contour_integral (g1 +++ g2) f = contour_integral g1 f + contour_integral g2 f" + by (simp add: has_contour_integral_integral has_contour_integral_join contour_integral_unique) subsection\Shifting the starting point of a (closed) path\ @@ -896,16 +896,16 @@ apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset) done -lemma has_path_integral_shiftpath: - assumes f: "(f has_path_integral i) g" "valid_path g" +lemma has_contour_integral_shiftpath: + assumes f: "(f has_contour_integral i) g" "valid_path g" and a: "a \ {0..1}" - shows "(f has_path_integral i) (shiftpath a g)" + shows "(f has_contour_integral i) (shiftpath a g)" proof - obtain s where s: "finite s" and g: "\x\{0..1} - s. g differentiable at x" using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) have *: "((\x. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}" - using assms by (auto simp: has_path_integral) + using assms by (auto simp: has_contour_integral) then have i: "i = integral {a..1} (\x. f (g x) * vector_derivative g (at x)) + integral {0..a} (\x. f (g x) * vector_derivative g (at x))" apply (rule has_integral_unique) @@ -967,13 +967,13 @@ done ultimately show ?thesis using a - by (auto simp: i has_path_integral intro: has_integral_combine [where c = "1-a"]) + by (auto simp: i has_contour_integral intro: has_integral_combine [where c = "1-a"]) qed -lemma has_path_integral_shiftpath_D: - assumes "(f has_path_integral i) (shiftpath a g)" +lemma has_contour_integral_shiftpath_D: + assumes "(f has_contour_integral i) (shiftpath a g)" "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" - shows "(f has_path_integral i) g" + shows "(f has_contour_integral i) g" proof - obtain s where s: "finite s" and g: "\x\{0..1} - s. g differentiable at x" @@ -994,25 +994,25 @@ apply (auto simp: dist_real_def shiftpath_shiftpath abs_if) done } note vd = this - have fi: "(f has_path_integral i) (shiftpath (1 - a) (shiftpath a g))" - using assms by (auto intro!: has_path_integral_shiftpath) + have fi: "(f has_contour_integral i) (shiftpath (1 - a) (shiftpath a g))" + using assms by (auto intro!: has_contour_integral_shiftpath) show ?thesis - apply (simp add: has_path_integral_def) - apply (rule has_integral_spike_finite [of "{0,1} \ s", OF _ _ fi [unfolded has_path_integral_def]]) + apply (simp add: has_contour_integral_def) + apply (rule has_integral_spike_finite [of "{0,1} \ s", OF _ _ fi [unfolded has_contour_integral_def]]) using s assms vd apply (auto simp: Path_Connected.shiftpath_shiftpath) done qed -lemma has_path_integral_shiftpath_eq: +lemma has_contour_integral_shiftpath_eq: assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" - shows "(f has_path_integral i) (shiftpath a g) \ (f has_path_integral i) g" - using assms has_path_integral_shiftpath has_path_integral_shiftpath_D by blast - -lemma path_integral_shiftpath: + shows "(f has_contour_integral i) (shiftpath a g) \ (f has_contour_integral i) g" + using assms has_contour_integral_shiftpath has_contour_integral_shiftpath_D by blast + +lemma contour_integral_shiftpath: assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" - shows "path_integral (shiftpath a g) f = path_integral g f" - using assms by (simp add: path_integral_def has_path_integral_shiftpath_eq) + shows "contour_integral (shiftpath a g) f = contour_integral g f" + using assms by (simp add: contour_integral_def has_contour_integral_shiftpath_eq) subsection\More about straight-line paths\ @@ -1040,10 +1040,10 @@ apply (fastforce simp add: continuous_on_eq_continuous_within) done -lemma has_path_integral_linepath: - shows "(f has_path_integral i) (linepath a b) \ +lemma has_contour_integral_linepath: + shows "(f has_contour_integral i) (linepath a b) \ ((\x. f(linepath a b x) * (b - a)) has_integral i) {0..1}" - by (simp add: has_path_integral vector_derivative_linepath_at) + by (simp add: has_contour_integral vector_derivative_linepath_at) lemma linepath_in_path: shows "x \ {0..1} \ linepath a b x \ closed_segment a b" @@ -1075,11 +1075,11 @@ lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x" by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def) -lemma has_path_integral_trivial [iff]: "(f has_path_integral 0) (linepath a a)" - by (simp add: has_path_integral_linepath) - -lemma path_integral_trivial [simp]: "path_integral (linepath a a) f = 0" - using has_path_integral_trivial path_integral_unique by blast +lemma has_contour_integral_trivial [iff]: "(f has_contour_integral 0) (linepath a a)" + by (simp add: has_contour_integral_linepath) + +lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0" + using has_contour_integral_trivial contour_integral_unique by blast subsection\Relation to subpath construction\ @@ -1108,24 +1108,24 @@ by (auto simp: o_def valid_path_def subpath_def) qed -lemma has_path_integral_subpath_refl [iff]: "(f has_path_integral 0) (subpath u u g)" - by (simp add: has_path_integral subpath_def) - -lemma path_integrable_subpath_refl [iff]: "f path_integrable_on (subpath u u g)" - using has_path_integral_subpath_refl path_integrable_on_def by blast - -lemma path_integral_subpath_refl [simp]: "path_integral (subpath u u g) f = 0" - by (simp add: has_path_integral_subpath_refl path_integral_unique) - -lemma has_path_integral_subpath: - assumes f: "f path_integrable_on g" and g: "valid_path g" +lemma has_contour_integral_subpath_refl [iff]: "(f has_contour_integral 0) (subpath u u g)" + by (simp add: has_contour_integral subpath_def) + +lemma contour_integrable_subpath_refl [iff]: "f contour_integrable_on (subpath u u g)" + using has_contour_integral_subpath_refl contour_integrable_on_def by blast + +lemma contour_integral_subpath_refl [simp]: "contour_integral (subpath u u g) f = 0" + by (simp add: has_contour_integral_subpath_refl contour_integral_unique) + +lemma has_contour_integral_subpath: + assumes f: "f contour_integrable_on g" and g: "valid_path g" and uv: "u \ {0..1}" "v \ {0..1}" "u \ v" - shows "(f has_path_integral integral {u..v} (\x. f(g x) * vector_derivative g (at x))) + shows "(f has_contour_integral integral {u..v} (\x. f(g x) * vector_derivative g (at x))) (subpath u v g)" proof (cases "v=u") case True then show ?thesis - using f by (simp add: path_integrable_on_def subpath_def has_path_integral) + using f by (simp add: contour_integrable_on_def subpath_def has_contour_integral) next case False obtain s where s: "\x. x \ {0..1} - s \ g differentiable at x" and fs: "finite s" @@ -1134,7 +1134,7 @@ has_integral (1 / (v - u)) * integral {u..v} (\t. f (g t) * vector_derivative g (at t))) {0..1}" using f uv - apply (simp add: path_integrable_on subpath_def has_path_integral) + apply (simp add: contour_integrable_on subpath_def has_contour_integral) apply (drule integrable_on_subcbox [where a=u and b=v, simplified]) apply (simp_all add: has_integral_integral) apply (drule has_integral_affinity [where m="v-u" and c=u, simplified]) @@ -1155,58 +1155,58 @@ show ?thesis apply (cut_tac has_integral_cmul [OF *, where c = "v-u"]) using fs assms - apply (simp add: False subpath_def has_path_integral) + apply (simp add: False subpath_def has_contour_integral) apply (rule_tac s = "(\t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite) apply (auto simp: inj_on_def False finite_vimageI vd scaleR_conv_of_real) done qed -lemma path_integrable_subpath: - assumes "f path_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" - shows "f path_integrable_on (subpath u v g)" +lemma contour_integrable_subpath: + assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" + shows "f contour_integrable_on (subpath u v g)" apply (cases u v rule: linorder_class.le_cases) - apply (metis path_integrable_on_def has_path_integral_subpath [OF assms]) + apply (metis contour_integrable_on_def has_contour_integral_subpath [OF assms]) apply (subst reversepath_subpath [symmetric]) - apply (rule path_integrable_reversepath) + apply (rule contour_integrable_reversepath) using assms apply (blast intro: valid_path_subpath) - apply (simp add: path_integrable_on_def) - using assms apply (blast intro: has_path_integral_subpath) + apply (simp add: contour_integrable_on_def) + using assms apply (blast intro: has_contour_integral_subpath) done lemma has_integral_integrable_integral: "(f has_integral i) s \ f integrable_on s \ integral s f = i" by blast -lemma has_integral_path_integral_subpath: - assumes "f path_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v" +lemma has_integral_contour_integral_subpath: + assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v" shows "(((\x. f(g x) * vector_derivative g (at x))) - has_integral path_integral (subpath u v g) f) {u..v}" + has_integral contour_integral (subpath u v g) f) {u..v}" using assms apply (auto simp: has_integral_integrable_integral) apply (rule integrable_on_subcbox [where a=u and b=v and s = "{0..1}", simplified]) - apply (auto simp: path_integral_unique [OF has_path_integral_subpath] path_integrable_on) + apply (auto simp: contour_integral_unique [OF has_contour_integral_subpath] contour_integrable_on) done -lemma path_integral_subpath_integral: - assumes "f path_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v" - shows "path_integral (subpath u v g) f = +lemma contour_integral_subcontour_integral: + assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "u \ v" + shows "contour_integral (subpath u v g) f = integral {u..v} (\x. f(g x) * vector_derivative g (at x))" - using assms has_path_integral_subpath path_integral_unique by blast - -lemma path_integral_subpath_combine_less: - assumes "f path_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "w \ {0..1}" + using assms has_contour_integral_subpath contour_integral_unique by blast + +lemma contour_integral_subpath_combine_less: + assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "w \ {0..1}" "u {0..1}" "v \ {0..1}" "w \ {0..1}" - shows "path_integral (subpath u v g) f + path_integral (subpath v w g) f = - path_integral (subpath u w g) f" +lemma contour_integral_subpath_combine: + assumes "f contour_integrable_on g" "valid_path g" "u \ {0..1}" "v \ {0..1}" "w \ {0..1}" + shows "contour_integral (subpath u v g) f + contour_integral (subpath v w g) f = + contour_integral (subpath u w g) f" proof (cases "u\v \ v\w \ u\w") case True have *: "subpath v u g = reversepath(subpath u v g) \ @@ -1221,28 +1221,28 @@ w < v \ v < u" using True assms by linarith with assms show ?thesis - using path_integral_subpath_combine_less [of f g u v w] - path_integral_subpath_combine_less [of f g u w v] - path_integral_subpath_combine_less [of f g v u w] - path_integral_subpath_combine_less [of f g v w u] - path_integral_subpath_combine_less [of f g w u v] - path_integral_subpath_combine_less [of f g w v u] + using contour_integral_subpath_combine_less [of f g u v w] + contour_integral_subpath_combine_less [of f g u w v] + contour_integral_subpath_combine_less [of f g v u w] + contour_integral_subpath_combine_less [of f g v w u] + contour_integral_subpath_combine_less [of f g w u v] + contour_integral_subpath_combine_less [of f g w v u] apply simp apply (elim disjE) - apply (auto simp: * path_integral_reversepath path_integrable_subpath + apply (auto simp: * contour_integral_reversepath contour_integrable_subpath valid_path_reversepath valid_path_subpath algebra_simps) done next case False then show ?thesis - apply (auto simp: path_integral_subpath_refl) + apply (auto simp: contour_integral_subpath_refl) using assms - by (metis eq_neg_iff_add_eq_0 path_integrable_subpath path_integral_reversepath reversepath_subpath valid_path_subpath) + by (metis eq_neg_iff_add_eq_0 contour_integrable_subpath contour_integral_reversepath reversepath_subpath valid_path_subpath) qed -lemma path_integral_integral: - shows "path_integral g f = integral {0..1} (\x. f (g x) * vector_derivative g (at x))" - by (simp add: path_integral_def integral_def has_path_integral) +lemma contour_integral_integral: + shows "contour_integral g f = integral {0..1} (\x. f (g x) * vector_derivative g (at x))" + by (simp add: contour_integral_def integral_def has_contour_integral) subsection\Segments via convex hulls\ @@ -1283,7 +1283,7 @@ text\Cauchy's theorem where there's a primitive\ -lemma path_integral_primitive_lemma: +lemma contour_integral_primitive_lemma: fixes f :: "complex \ complex" and g :: "real \ complex" assumes "a \ b" and "\x. x \ s \ (f has_field_derivative f' x) (at x within s)" @@ -1321,34 +1321,34 @@ done qed -lemma path_integral_primitive: +lemma contour_integral_primitive: assumes "\x. x \ s \ (f has_field_derivative f' x) (at x within s)" and "valid_path g" "path_image g \ s" - shows "(f' has_path_integral (f(pathfinish g) - f(pathstart g))) g" + shows "(f' has_contour_integral (f(pathfinish g) - f(pathstart g))) g" using assms - apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_path_integral_def) - apply (auto intro!: piecewise_C1_imp_differentiable path_integral_primitive_lemma [of 0 1 s]) + apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_contour_integral_def) + apply (auto intro!: piecewise_C1_imp_differentiable contour_integral_primitive_lemma [of 0 1 s]) done corollary Cauchy_theorem_primitive: assumes "\x. x \ s \ (f has_field_derivative f' x) (at x within s)" and "valid_path g" "path_image g \ s" "pathfinish g = pathstart g" - shows "(f' has_path_integral 0) g" + shows "(f' has_contour_integral 0) g" using assms - by (metis diff_self path_integral_primitive) + by (metis diff_self contour_integral_primitive) text\Existence of path integral for continuous function\ -lemma path_integrable_continuous_linepath: +lemma contour_integrable_continuous_linepath: assumes "continuous_on (closed_segment a b) f" - shows "f path_integrable_on (linepath a b)" + shows "f contour_integrable_on (linepath a b)" proof - have "continuous_on {0..1} ((\x. f x * (b - a)) o linepath a b)" apply (rule continuous_on_compose [OF continuous_on_linepath], simp add: linepath_image_01) apply (rule continuous_intros | simp add: assms)+ done then show ?thesis - apply (simp add: path_integrable_on_def has_path_integral_def integrable_on_def [symmetric]) + apply (simp add: contour_integrable_on_def has_contour_integral_def integrable_on_def [symmetric]) apply (rule integrable_continuous [of 0 "1::real", simplified]) apply (rule continuous_on_eq [where f = "\x. f(linepath a b x)*(b - a)"]) apply (auto simp: vector_derivative_linepath_within) @@ -1359,59 +1359,59 @@ by (rule has_derivative_imp_has_field_derivative) (rule derivative_intros | simp)+ -lemma path_integral_id [simp]: "path_integral (linepath a b) (\y. y) = (b^2 - a^2)/2" - apply (rule path_integral_unique) - using path_integral_primitive [of UNIV "\x. x^2/2" "\x. x" "linepath a b"] +lemma contour_integral_id [simp]: "contour_integral (linepath a b) (\y. y) = (b^2 - a^2)/2" + apply (rule contour_integral_unique) + using contour_integral_primitive [of UNIV "\x. x^2/2" "\x. x" "linepath a b"] apply (auto simp: field_simps has_field_der_id) done -lemma path_integrable_on_const [iff]: "(\x. c) path_integrable_on (linepath a b)" - by (simp add: continuous_on_const path_integrable_continuous_linepath) - -lemma path_integrable_on_id [iff]: "(\x. x) path_integrable_on (linepath a b)" - by (simp add: continuous_on_id path_integrable_continuous_linepath) +lemma contour_integrable_on_const [iff]: "(\x. c) contour_integrable_on (linepath a b)" + by (simp add: continuous_on_const contour_integrable_continuous_linepath) + +lemma contour_integrable_on_id [iff]: "(\x. x) contour_integrable_on (linepath a b)" + by (simp add: continuous_on_id contour_integrable_continuous_linepath) subsection\Arithmetical combining theorems\ -lemma has_path_integral_neg: - "(f has_path_integral i) g \ ((\x. -(f x)) has_path_integral (-i)) g" - by (simp add: has_integral_neg has_path_integral_def) - -lemma has_path_integral_add: - "\(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\ - \ ((\x. f1 x + f2 x) has_path_integral (i1 + i2)) g" - by (simp add: has_integral_add has_path_integral_def algebra_simps) - -lemma has_path_integral_diff: - "\(f1 has_path_integral i1) g; (f2 has_path_integral i2) g\ - \ ((\x. f1 x - f2 x) has_path_integral (i1 - i2)) g" - by (simp add: has_integral_sub has_path_integral_def algebra_simps) - -lemma has_path_integral_lmul: - "(f has_path_integral i) g \ ((\x. c * (f x)) has_path_integral (c*i)) g" -apply (simp add: has_path_integral_def) +lemma has_contour_integral_neg: + "(f has_contour_integral i) g \ ((\x. -(f x)) has_contour_integral (-i)) g" + by (simp add: has_integral_neg has_contour_integral_def) + +lemma has_contour_integral_add: + "\(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g\ + \ ((\x. f1 x + f2 x) has_contour_integral (i1 + i2)) g" + by (simp add: has_integral_add has_contour_integral_def algebra_simps) + +lemma has_contour_integral_diff: + "\(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g\ + \ ((\x. f1 x - f2 x) has_contour_integral (i1 - i2)) g" + by (simp add: has_integral_sub has_contour_integral_def algebra_simps) + +lemma has_contour_integral_lmul: + "(f has_contour_integral i) g \ ((\x. c * (f x)) has_contour_integral (c*i)) g" +apply (simp add: has_contour_integral_def) apply (drule has_integral_mult_right) apply (simp add: algebra_simps) done -lemma has_path_integral_rmul: - "(f has_path_integral i) g \ ((\x. (f x) * c) has_path_integral (i*c)) g" -apply (drule has_path_integral_lmul) +lemma has_contour_integral_rmul: + "(f has_contour_integral i) g \ ((\x. (f x) * c) has_contour_integral (i*c)) g" +apply (drule has_contour_integral_lmul) apply (simp add: mult.commute) done -lemma has_path_integral_div: - "(f has_path_integral i) g \ ((\x. f x/c) has_path_integral (i/c)) g" - by (simp add: field_class.field_divide_inverse) (metis has_path_integral_rmul) - -lemma has_path_integral_eq: - "\(f has_path_integral y) p; \x. x \ path_image p \ f x = g x\ \ (g has_path_integral y) p" -apply (simp add: path_image_def has_path_integral_def) +lemma has_contour_integral_div: + "(f has_contour_integral i) g \ ((\x. f x/c) has_contour_integral (i/c)) g" + by (simp add: field_class.field_divide_inverse) (metis has_contour_integral_rmul) + +lemma has_contour_integral_eq: + "\(f has_contour_integral y) p; \x. x \ path_image p \ f x = g x\ \ (g has_contour_integral y) p" +apply (simp add: path_image_def has_contour_integral_def) by (metis (no_types, lifting) image_eqI has_integral_eq) -lemma has_path_integral_bound_linepath: - assumes "(f has_path_integral i) (linepath a b)" +lemma has_contour_integral_bound_linepath: + assumes "(f has_contour_integral i) (linepath a b)" "0 \ B" "\x. x \ closed_segment a b \ norm(f x) \ B" shows "norm i \ B * norm(b - a)" proof - @@ -1424,7 +1424,7 @@ have "norm i \ (B * norm (b - a)) * content (cbox 0 (1::real))" apply (rule has_integral_bound [of _ "\x. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"]) - using assms * unfolding has_path_integral_def + using assms * unfolding has_contour_integral_def apply (auto simp: norm_mult) done then show ?thesis @@ -1432,163 +1432,163 @@ qed (*UNUSED -lemma has_path_integral_bound_linepath_strong: +lemma has_contour_integral_bound_linepath_strong: fixes a :: real and f :: "complex \ real" - assumes "(f has_path_integral i) (linepath a b)" + assumes "(f has_contour_integral i) (linepath a b)" "finite k" "0 \ B" "\x::real. x \ closed_segment a b - k \ norm(f x) \ B" shows "norm i \ B*norm(b - a)" *) -lemma has_path_integral_const_linepath: "((\x. c) has_path_integral c*(b - a))(linepath a b)" - unfolding has_path_integral_linepath +lemma has_contour_integral_const_linepath: "((\x. c) has_contour_integral c*(b - a))(linepath a b)" + unfolding has_contour_integral_linepath by (metis content_real diff_0_right has_integral_const_real lambda_one of_real_1 scaleR_conv_of_real zero_le_one) -lemma has_path_integral_0: "((\x. 0) has_path_integral 0) g" - by (simp add: has_path_integral_def) - -lemma has_path_integral_is_0: - "(\z. z \ path_image g \ f z = 0) \ (f has_path_integral 0) g" - by (rule has_path_integral_eq [OF has_path_integral_0]) auto - -lemma has_path_integral_setsum: - "\finite s; \a. a \ s \ (f a has_path_integral i a) p\ - \ ((\x. setsum (\a. f a x) s) has_path_integral setsum i s) p" - by (induction s rule: finite_induct) (auto simp: has_path_integral_0 has_path_integral_add) +lemma has_contour_integral_0: "((\x. 0) has_contour_integral 0) g" + by (simp add: has_contour_integral_def) + +lemma has_contour_integral_is_0: + "(\z. z \ path_image g \ f z = 0) \ (f has_contour_integral 0) g" + by (rule has_contour_integral_eq [OF has_contour_integral_0]) auto + +lemma has_contour_integral_setsum: + "\finite s; \a. a \ s \ (f a has_contour_integral i a) p\ + \ ((\x. setsum (\a. f a x) s) has_contour_integral setsum i s) p" + by (induction s rule: finite_induct) (auto simp: has_contour_integral_0 has_contour_integral_add) subsection \Operations on path integrals\ -lemma path_integral_const_linepath [simp]: "path_integral (linepath a b) (\x. c) = c*(b - a)" - by (rule path_integral_unique [OF has_path_integral_const_linepath]) - -lemma path_integral_neg: - "f path_integrable_on g \ path_integral g (\x. -(f x)) = -(path_integral g f)" - by (simp add: path_integral_unique has_path_integral_integral has_path_integral_neg) - -lemma path_integral_add: - "f1 path_integrable_on g \ f2 path_integrable_on g \ path_integral g (\x. f1 x + f2 x) = - path_integral g f1 + path_integral g f2" - by (simp add: path_integral_unique has_path_integral_integral has_path_integral_add) - -lemma path_integral_diff: - "f1 path_integrable_on g \ f2 path_integrable_on g \ path_integral g (\x. f1 x - f2 x) = - path_integral g f1 - path_integral g f2" - by (simp add: path_integral_unique has_path_integral_integral has_path_integral_diff) - -lemma path_integral_lmul: - shows "f path_integrable_on g - \ path_integral g (\x. c * f x) = c*path_integral g f" - by (simp add: path_integral_unique has_path_integral_integral has_path_integral_lmul) - -lemma path_integral_rmul: - shows "f path_integrable_on g - \ path_integral g (\x. f x * c) = path_integral g f * c" - by (simp add: path_integral_unique has_path_integral_integral has_path_integral_rmul) - -lemma path_integral_div: - shows "f path_integrable_on g - \ path_integral g (\x. f x / c) = path_integral g f / c" - by (simp add: path_integral_unique has_path_integral_integral has_path_integral_div) - -lemma path_integral_eq: - "(\x. x \ path_image p \ f x = g x) \ path_integral p f = path_integral p g" - by (simp add: path_integral_def) (metis has_path_integral_eq) - -lemma path_integral_eq_0: - "(\z. z \ path_image g \ f z = 0) \ path_integral g f = 0" - by (simp add: has_path_integral_is_0 path_integral_unique) - -lemma path_integral_bound_linepath: +lemma contour_integral_const_linepath [simp]: "contour_integral (linepath a b) (\x. c) = c*(b - a)" + by (rule contour_integral_unique [OF has_contour_integral_const_linepath]) + +lemma contour_integral_neg: + "f contour_integrable_on g \ contour_integral g (\x. -(f x)) = -(contour_integral g f)" + by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_neg) + +lemma contour_integral_add: + "f1 contour_integrable_on g \ f2 contour_integrable_on g \ contour_integral g (\x. f1 x + f2 x) = + contour_integral g f1 + contour_integral g f2" + by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_add) + +lemma contour_integral_diff: + "f1 contour_integrable_on g \ f2 contour_integrable_on g \ contour_integral g (\x. f1 x - f2 x) = + contour_integral g f1 - contour_integral g f2" + by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_diff) + +lemma contour_integral_lmul: + shows "f contour_integrable_on g + \ contour_integral g (\x. c * f x) = c*contour_integral g f" + by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_lmul) + +lemma contour_integral_rmul: + shows "f contour_integrable_on g + \ contour_integral g (\x. f x * c) = contour_integral g f * c" + by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_rmul) + +lemma contour_integral_div: + shows "f contour_integrable_on g + \ contour_integral g (\x. f x / c) = contour_integral g f / c" + by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_div) + +lemma contour_integral_eq: + "(\x. x \ path_image p \ f x = g x) \ contour_integral p f = contour_integral p g" + by (simp add: contour_integral_def) (metis has_contour_integral_eq) + +lemma contour_integral_eq_0: + "(\z. z \ path_image g \ f z = 0) \ contour_integral g f = 0" + by (simp add: has_contour_integral_is_0 contour_integral_unique) + +lemma contour_integral_bound_linepath: shows - "\f path_integrable_on (linepath a b); + "\f contour_integrable_on (linepath a b); 0 \ B; \x. x \ closed_segment a b \ norm(f x) \ B\ - \ norm(path_integral (linepath a b) f) \ B*norm(b - a)" - apply (rule has_path_integral_bound_linepath [of f]) - apply (auto simp: has_path_integral_integral) + \ norm(contour_integral (linepath a b) f) \ B*norm(b - a)" + apply (rule has_contour_integral_bound_linepath [of f]) + apply (auto simp: has_contour_integral_integral) done -lemma path_integral_0: "path_integral g (\x. 0) = 0" - by (simp add: path_integral_unique has_path_integral_0) - -lemma path_integral_setsum: - "\finite s; \a. a \ s \ (f a) path_integrable_on p\ - \ path_integral p (\x. setsum (\a. f a x) s) = setsum (\a. path_integral p (f a)) s" - by (auto simp: path_integral_unique has_path_integral_setsum has_path_integral_integral) - -lemma path_integrable_eq: - "\f path_integrable_on p; \x. x \ path_image p \ f x = g x\ \ g path_integrable_on p" - unfolding path_integrable_on_def - by (metis has_path_integral_eq) +lemma contour_integral_0: "contour_integral g (\x. 0) = 0" + by (simp add: contour_integral_unique has_contour_integral_0) + +lemma contour_integral_setsum: + "\finite s; \a. a \ s \ (f a) contour_integrable_on p\ + \ contour_integral p (\x. setsum (\a. f a x) s) = setsum (\a. contour_integral p (f a)) s" + by (auto simp: contour_integral_unique has_contour_integral_setsum has_contour_integral_integral) + +lemma contour_integrable_eq: + "\f contour_integrable_on p; \x. x \ path_image p \ f x = g x\ \ g contour_integrable_on p" + unfolding contour_integrable_on_def + by (metis has_contour_integral_eq) subsection \Arithmetic theorems for path integrability\ -lemma path_integrable_neg: - "f path_integrable_on g \ (\x. -(f x)) path_integrable_on g" - using has_path_integral_neg path_integrable_on_def by blast - -lemma path_integrable_add: - "\f1 path_integrable_on g; f2 path_integrable_on g\ \ (\x. f1 x + f2 x) path_integrable_on g" - using has_path_integral_add path_integrable_on_def +lemma contour_integrable_neg: + "f contour_integrable_on g \ (\x. -(f x)) contour_integrable_on g" + using has_contour_integral_neg contour_integrable_on_def by blast + +lemma contour_integrable_add: + "\f1 contour_integrable_on g; f2 contour_integrable_on g\ \ (\x. f1 x + f2 x) contour_integrable_on g" + using has_contour_integral_add contour_integrable_on_def by fastforce -lemma path_integrable_diff: - "\f1 path_integrable_on g; f2 path_integrable_on g\ \ (\x. f1 x - f2 x) path_integrable_on g" - using has_path_integral_diff path_integrable_on_def +lemma contour_integrable_diff: + "\f1 contour_integrable_on g; f2 contour_integrable_on g\ \ (\x. f1 x - f2 x) contour_integrable_on g" + using has_contour_integral_diff contour_integrable_on_def by fastforce -lemma path_integrable_lmul: - "f path_integrable_on g \ (\x. c * f x) path_integrable_on g" - using has_path_integral_lmul path_integrable_on_def +lemma contour_integrable_lmul: + "f contour_integrable_on g \ (\x. c * f x) contour_integrable_on g" + using has_contour_integral_lmul contour_integrable_on_def by fastforce -lemma path_integrable_rmul: - "f path_integrable_on g \ (\x. f x * c) path_integrable_on g" - using has_path_integral_rmul path_integrable_on_def +lemma contour_integrable_rmul: + "f contour_integrable_on g \ (\x. f x * c) contour_integrable_on g" + using has_contour_integral_rmul contour_integrable_on_def by fastforce -lemma path_integrable_div: - "f path_integrable_on g \ (\x. f x / c) path_integrable_on g" - using has_path_integral_div path_integrable_on_def +lemma contour_integrable_div: + "f contour_integrable_on g \ (\x. f x / c) contour_integrable_on g" + using has_contour_integral_div contour_integrable_on_def by fastforce -lemma path_integrable_setsum: - "\finite s; \a. a \ s \ (f a) path_integrable_on p\ - \ (\x. setsum (\a. f a x) s) path_integrable_on p" - unfolding path_integrable_on_def - by (metis has_path_integral_setsum) +lemma contour_integrable_setsum: + "\finite s; \a. a \ s \ (f a) contour_integrable_on p\ + \ (\x. setsum (\a. f a x) s) contour_integrable_on p" + unfolding contour_integrable_on_def + by (metis has_contour_integral_setsum) subsection\Reversing a path integral\ -lemma has_path_integral_reverse_linepath: - "(f has_path_integral i) (linepath a b) - \ (f has_path_integral (-i)) (linepath b a)" - using has_path_integral_reversepath valid_path_linepath by fastforce - -lemma path_integral_reverse_linepath: +lemma has_contour_integral_reverse_linepath: + "(f has_contour_integral i) (linepath a b) + \ (f has_contour_integral (-i)) (linepath b a)" + using has_contour_integral_reversepath valid_path_linepath by fastforce + +lemma contour_integral_reverse_linepath: "continuous_on (closed_segment a b) f - \ path_integral (linepath a b) f = - (path_integral(linepath b a) f)" -apply (rule path_integral_unique) -apply (rule has_path_integral_reverse_linepath) -by (simp add: closed_segment_commute path_integrable_continuous_linepath has_path_integral_integral) + \ contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)" +apply (rule contour_integral_unique) +apply (rule has_contour_integral_reverse_linepath) +by (simp add: closed_segment_commute contour_integrable_continuous_linepath has_contour_integral_integral) (* Splitting a path integral in a flat way.*) -lemma has_path_integral_split: - assumes f: "(f has_path_integral i) (linepath a c)" "(f has_path_integral j) (linepath c b)" +lemma has_contour_integral_split: + assumes f: "(f has_contour_integral i) (linepath a c)" "(f has_contour_integral j) (linepath c b)" and k: "0 \ k" "k \ 1" and c: "c - a = k *\<^sub>R (b - a)" - shows "(f has_path_integral (i + j)) (linepath a b)" + shows "(f has_contour_integral (i + j)) (linepath a b)" proof (cases "k = 0 \ k = 1") case True then show ?thesis using assms apply auto - apply (metis add.left_neutral has_path_integral_trivial has_path_integral_unique) - apply (metis add.right_neutral has_path_integral_trivial has_path_integral_unique) + apply (metis add.left_neutral has_contour_integral_trivial has_contour_integral_unique) + apply (metis add.right_neutral has_contour_integral_trivial has_contour_integral_unique) done next case False @@ -1632,7 +1632,7 @@ } note fj = this show ?thesis using f k - apply (simp add: has_path_integral_linepath) + apply (simp add: has_contour_integral_linepath) apply (simp add: linepath_def) apply (rule has_integral_combine [OF _ _ fi fj], simp_all) done @@ -1655,11 +1655,11 @@ done qed -lemma path_integral_split: +lemma contour_integral_split: assumes f: "continuous_on (closed_segment a b) f" and k: "0 \ k" "k \ 1" and c: "c - a = k *\<^sub>R (b - a)" - shows "path_integral(linepath a b) f = path_integral(linepath a c) f + path_integral(linepath c b) f" + shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f" proof - have c': "c = (1 - k) *\<^sub>R a + k *\<^sub>R b" using c by (simp add: algebra_simps) @@ -1671,35 +1671,35 @@ apply (auto simp: hull_inc c' Convex.convexD_alt) done show ?thesis - apply (rule path_integral_unique) - apply (rule has_path_integral_split [OF has_path_integral_integral has_path_integral_integral k c]) - apply (rule path_integrable_continuous_linepath *)+ + apply (rule contour_integral_unique) + apply (rule has_contour_integral_split [OF has_contour_integral_integral has_contour_integral_integral k c]) + apply (rule contour_integrable_continuous_linepath *)+ done qed -lemma path_integral_split_linepath: +lemma contour_integral_split_linepath: assumes f: "continuous_on (closed_segment a b) f" and c: "c \ closed_segment a b" - shows "path_integral(linepath a b) f = path_integral(linepath a c) f + path_integral(linepath c b) f" + shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f" using c - by (auto simp: closed_segment_def algebra_simps intro!: path_integral_split [OF f]) + by (auto simp: closed_segment_def algebra_simps intro!: contour_integral_split [OF f]) (* The special case of midpoints used in the main quadrisection.*) -lemma has_path_integral_midpoint: - assumes "(f has_path_integral i) (linepath a (midpoint a b))" - "(f has_path_integral j) (linepath (midpoint a b) b)" - shows "(f has_path_integral (i + j)) (linepath a b)" - apply (rule has_path_integral_split [where c = "midpoint a b" and k = "1/2"]) +lemma has_contour_integral_midpoint: + assumes "(f has_contour_integral i) (linepath a (midpoint a b))" + "(f has_contour_integral j) (linepath (midpoint a b) b)" + shows "(f has_contour_integral (i + j)) (linepath a b)" + apply (rule has_contour_integral_split [where c = "midpoint a b" and k = "1/2"]) using assms apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real) done -lemma path_integral_midpoint: +lemma contour_integral_midpoint: "continuous_on (closed_segment a b) f - \ path_integral (linepath a b) f = - path_integral (linepath a (midpoint a b)) f + path_integral (linepath (midpoint a b) b) f" - apply (rule path_integral_split [where c = "midpoint a b" and k = "1/2"]) + \ contour_integral (linepath a b) f = + contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f" + apply (rule contour_integral_split [where c = "midpoint a b" and k = "1/2"]) using assms apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real) done @@ -1708,16 +1708,16 @@ text\A couple of special case lemmas that are useful below\ lemma triangle_linear_has_chain_integral: - "((\x. m*x + d) has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" + "((\x. m*x + d) has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" apply (rule Cauchy_theorem_primitive [of UNIV "\x. m/2 * x^2 + d*x"]) apply (auto intro!: derivative_eq_intros) done lemma has_chain_integral_chain_integral3: - "(f has_path_integral i) (linepath a b +++ linepath b c +++ linepath c d) - \ path_integral (linepath a b) f + path_integral (linepath b c) f + path_integral (linepath c d) f = i" - apply (subst path_integral_unique [symmetric], assumption) - apply (drule has_path_integral_integrable) + "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d) + \ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f = i" + apply (subst contour_integral_unique [symmetric], assumption) + apply (drule has_contour_integral_integrable) apply (simp add: valid_path_join) done @@ -1731,13 +1731,13 @@ lemma snd_im_cbox [simp]: "cbox a b \ {} \ (snd ` cbox (a,c) (b,d)) = cbox c d" by (auto simp: cbox_Pair_eq) -lemma path_integral_swap: +lemma contour_integral_swap: assumes fcon: "continuous_on (path_image g \ path_image h) (\(y1,y2). f y1 y2)" and vp: "valid_path g" "valid_path h" and gvcon: "continuous_on {0..1} (\t. vector_derivative g (at t))" and hvcon: "continuous_on {0..1} (\t. vector_derivative h (at t))" - shows "path_integral g (\w. path_integral h (f w)) = - path_integral h (\z. path_integral g (\w. f w z))" + shows "contour_integral g (\w. contour_integral h (f w)) = + contour_integral h (\z. contour_integral g (\w. f w z))" proof - have gcon: "continuous_on {0..1} g" and hcon: "continuous_on {0..1} h" using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def) @@ -1774,31 +1774,31 @@ apply (rule gcon hcon continuous_intros | simp)+ apply (auto simp: path_image_def intro: continuous_on_subset [OF fcon]) done - have "integral {0..1} (\x. path_integral h (f (g x)) * vector_derivative g (at x)) = - integral {0..1} (\x. path_integral h (\y. f (g x) y * vector_derivative g (at x)))" - apply (rule integral_cong [OF path_integral_rmul [symmetric]]) - apply (clarsimp simp: path_integrable_on) + have "integral {0..1} (\x. contour_integral h (f (g x)) * vector_derivative g (at x)) = + integral {0..1} (\x. contour_integral h (\y. f (g x) y * vector_derivative g (at x)))" + apply (rule integral_cong [OF contour_integral_rmul [symmetric]]) + apply (clarsimp simp: contour_integrable_on) apply (rule integrable_continuous_real) apply (rule continuous_on_mult [OF _ hvcon]) apply (subst fgh1) apply (rule fcon_im1 hcon continuous_intros | simp)+ done also have "... = integral {0..1} - (\y. path_integral g (\x. f x (h y) * vector_derivative h (at y)))" - apply (simp add: path_integral_integral) + (\y. contour_integral g (\x. f x (h y) * vector_derivative h (at y)))" + apply (simp add: contour_integral_integral) apply (subst integral_swap_continuous [where 'a = real and 'b = real, of 0 0 1 1, simplified]) apply (rule fgh gvcon' hvcon' continuous_intros | simp add: split_def)+ apply (simp add: algebra_simps) done - also have "... = path_integral h (\z. path_integral g (\w. f w z))" - apply (simp add: path_integral_integral) + also have "... = contour_integral h (\z. contour_integral g (\w. f w z))" + apply (simp add: contour_integral_integral) apply (rule integral_cong) apply (subst integral_mult_left [symmetric]) apply (blast intro: vdg) apply (simp add: algebra_simps) done finally show ?thesis - by (simp add: path_integral_integral) + by (simp add: contour_integral_integral) qed @@ -1828,11 +1828,11 @@ assumes f: "continuous_on (convex hull {a,b,c}) f" and dist: "dist a b \ K" "dist b c \ K" "dist c a \ K" and e: "e * K^2 \ - norm (path_integral(linepath a b) f + path_integral(linepath b c) f + path_integral(linepath c a) f)" + norm (contour_integral(linepath a b) f + contour_integral(linepath b c) f + contour_integral(linepath c a) f)" shows "\a' b' c'. a' \ convex hull {a,b,c} \ b' \ convex hull {a,b,c} \ c' \ convex hull {a,b,c} \ dist a' b' \ K/2 \ dist b' c' \ K/2 \ dist c' a' \ K/2 \ - e * (K/2)^2 \ norm(path_integral(linepath a' b') f + path_integral(linepath b' c') f + path_integral(linepath c' a') f)" + e * (K/2)^2 \ norm(contour_integral(linepath a' b') f + contour_integral(linepath b' c') f + contour_integral(linepath c' a') f)" proof - note divide_le_eq_numeral1 [simp del] def a' \ "midpoint b c" @@ -1847,14 +1847,14 @@ apply (rule continuous_on_subset [OF f], metis midpoints_in_convex_hull convex_hull_subset hull_subset insert_subset segment_convex_hull)+ done - let ?pathint = "\x y. path_integral(linepath x y) f" + let ?pathint = "\x y. contour_integral(linepath x y) f" have *: "?pathint a b + ?pathint b c + ?pathint c a = (?pathint a c' + ?pathint c' b' + ?pathint b' a) + (?pathint a' c' + ?pathint c' b + ?pathint b a') + (?pathint a' c + ?pathint c b' + ?pathint b' a') + (?pathint a' b' + ?pathint b' c' + ?pathint c' a')" - apply (simp add: fcont' path_integral_reverse_linepath) - apply (simp add: a'_def b'_def c'_def path_integral_midpoint fabc) + apply (simp add: fcont' contour_integral_reverse_linepath) + apply (simp add: a'_def b'_def c'_def contour_integral_midpoint fabc) done have [simp]: "\x y. cmod (x * 2 - y * 2) = cmod (x - y) * 2" by (metis left_diff_distrib mult.commute norm_mult_numeral1) @@ -1926,8 +1926,8 @@ and e: "0 < e" shows "\k>0. \a b c. dist a b \ k \ dist b c \ k \ dist c a \ k \ x \ convex hull {a,b,c} \ convex hull {a,b,c} \ s - \ norm(path_integral(linepath a b) f + path_integral(linepath b c) f + - path_integral(linepath c a) f) + \ norm(contour_integral(linepath a b) f + contour_integral(linepath b c) f + + contour_integral(linepath c a) f) \ e*(dist a b + dist b c + dist c a)^2" (is "\k>0. \a b c. _ \ ?normle a b c") proof - @@ -1937,22 +1937,22 @@ have disj_le: "\x \ a \ x \ b \ x \ c; 0 \ a; 0 \ b; 0 \ c\ \ x \ a + b + c" for x::real and a b c by linarith - have fabc: "f path_integrable_on linepath a b" "f path_integrable_on linepath b c" "f path_integrable_on linepath c a" + have fabc: "f contour_integrable_on linepath a b" "f contour_integrable_on linepath b c" "f contour_integrable_on linepath c a" if "convex hull {a, b, c} \ s" for a b c using segments_subset_convex_hull that - by (metis continuous_on_subset f path_integrable_continuous_linepath)+ - note path_bound = has_path_integral_bound_linepath [simplified norm_minus_commute, OF has_path_integral_integral] + by (metis continuous_on_subset f contour_integrable_continuous_linepath)+ + note path_bound = has_contour_integral_bound_linepath [simplified norm_minus_commute, OF has_contour_integral_integral] { fix f' a b c d assume d: "0 < d" and f': "\y. \cmod (y - x) \ d; y \ s\ \ cmod (f y - f x - f' * (y - x)) \ e * cmod (y - x)" and le: "cmod (a - b) \ d" "cmod (b - c) \ d" "cmod (c - a) \ d" and xc: "x \ convex hull {a, b, c}" and s: "convex hull {a, b, c} \ s" - have pa: "path_integral (linepath a b) f + path_integral (linepath b c) f + path_integral (linepath c a) f = - path_integral (linepath a b) (\y. f y - f x - f'*(y - x)) + - path_integral (linepath b c) (\y. f y - f x - f'*(y - x)) + - path_integral (linepath c a) (\y. f y - f x - f'*(y - x))" - apply (simp add: path_integral_diff path_integral_lmul path_integrable_lmul path_integrable_diff fabc [OF s]) + have pa: "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = + contour_integral (linepath a b) (\y. f y - f x - f'*(y - x)) + + contour_integral (linepath b c) (\y. f y - f x - f'*(y - x)) + + contour_integral (linepath c a) (\y. f y - f x - f'*(y - x))" + apply (simp add: contour_integral_diff contour_integral_lmul contour_integrable_lmul contour_integrable_diff fabc [OF s]) apply (simp add: field_simps) done { fix y @@ -1971,7 +1971,7 @@ using f' xc s e apply simp_all apply (intro norm_triangle_le add_mono path_bound) - apply (simp_all add: path_integral_diff path_integral_lmul path_integrable_lmul path_integrable_diff fabc) + apply (simp_all add: contour_integral_diff contour_integral_lmul contour_integrable_lmul contour_integrable_diff fabc) apply (blast intro: cm_le elim: dest: segments_subset_convex_hull [THEN subsetD])+ done } note * = this @@ -2031,13 +2031,13 @@ lemma Cauchy_theorem_triangle: assumes "f holomorphic_on (convex hull {a,b,c})" - shows "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" + shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" proof - have contf: "continuous_on (convex hull {a,b,c}) f" by (metis assms holomorphic_on_imp_continuous_on) - let ?pathint = "\x y. path_integral(linepath x y) f" + let ?pathint = "\x y. contour_integral(linepath x y) f" { fix y::complex - assume fy: "(f has_path_integral y) (linepath a b +++ linepath b c +++ linepath c a)" + assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)" and ynz: "y \ 0" def K \ "1 + max (dist a b) (max (dist b c) (dist c a))" def e \ "norm y / K^2" @@ -2133,11 +2133,11 @@ apply (rule_tac x1="K/k" in exE [OF real_arch_pow2], blast) done } - moreover have "f path_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" - by simp (meson contf continuous_on_subset path_integrable_continuous_linepath segments_subset_convex_hull(1) + moreover have "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" + by simp (meson contf continuous_on_subset contour_integrable_continuous_linepath segments_subset_convex_hull(1) segments_subset_convex_hull(3) segments_subset_convex_hull(5)) ultimately show ?thesis - using has_path_integral_integral by fastforce + using has_contour_integral_integral by fastforce qed @@ -2147,21 +2147,21 @@ assumes f: "continuous_on (convex hull {a,b,c}) f" and c: "c - a = k *\<^sub>R (b - a)" and k: "0 \ k" - shows "path_integral (linepath a b) f + path_integral (linepath b c) f + - path_integral (linepath c a) f = 0" + shows "contour_integral (linepath a b) f + contour_integral (linepath b c) f + + contour_integral (linepath c a) f = 0" proof - have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" using f continuous_on_subset segments_subset_convex_hull by metis+ show ?thesis proof (cases "k \ 1") case True show ?thesis - by (simp add: path_integral_split [OF fabc(1) k True c] path_integral_reverse_linepath fabc) + by (simp add: contour_integral_split [OF fabc(1) k True c] contour_integral_reverse_linepath fabc) next case False then show ?thesis using fabc c - apply (subst path_integral_split [of a c f "1/k" b, symmetric]) + apply (subst contour_integral_split [of a c f "1/k" b, symmetric]) apply (metis closed_segment_commute fabc(3)) - apply (auto simp: k path_integral_reverse_linepath) + apply (auto simp: k contour_integral_reverse_linepath) done qed qed @@ -2169,9 +2169,9 @@ lemma Cauchy_theorem_flat: assumes f: "continuous_on (convex hull {a,b,c}) f" and c: "c - a = k *\<^sub>R (b - a)" - shows "path_integral (linepath a b) f + - path_integral (linepath b c) f + - path_integral (linepath c a) f = 0" + shows "contour_integral (linepath a b) f + + contour_integral (linepath b c) f + + contour_integral (linepath c a) f = 0" proof (cases "0 \ k") case True with assms show ?thesis by (blast intro: Cauchy_theorem_flat_lemma) @@ -2179,14 +2179,14 @@ case False have "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" using f continuous_on_subset segments_subset_convex_hull by metis+ - moreover have "path_integral (linepath b a) f + path_integral (linepath a c) f + - path_integral (linepath c b) f = 0" + moreover have "contour_integral (linepath b a) f + contour_integral (linepath a c) f + + contour_integral (linepath c b) f = 0" apply (rule Cauchy_theorem_flat_lemma [of b a c f "1-k"]) using False c apply (auto simp: f insert_commute scaleR_conv_of_real algebra_simps) done ultimately show ?thesis - apply (auto simp: path_integral_reverse_linepath) + apply (auto simp: contour_integral_reverse_linepath) using add_eq_0_iff by force qed @@ -2194,7 +2194,7 @@ lemma 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_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" + shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" proof - have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" using contf continuous_on_subset segments_subset_convex_hull by metis+ @@ -2219,16 +2219,16 @@ have contf': "continuous_on (convex hull {b,a,c}) f" using contf by (simp add: insert_commute) { fix y::complex - assume fy: "(f has_path_integral y) (linepath a b +++ linepath b c +++ linepath c a)" + assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)" and ynz: "y \ 0" - have pi_eq_y: "path_integral (linepath a b) f + path_integral (linepath b c) f + path_integral (linepath c a) f = y" + have pi_eq_y: "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = y" by (rule has_chain_integral_chain_integral3 [OF fy]) have ?thesis proof (cases "c=a \ a=b \ b=c") case True then show ?thesis using Cauchy_theorem_flat [OF contf, of 0] using has_chain_integral_chain_integral3 [OF fy] ynz - by (force simp: fabc path_integral_reverse_linepath) + by (force simp: fabc contour_integral_reverse_linepath) next case False then have car3: "card {a, b, c} = Suc (DIM(complex))" @@ -2242,7 +2242,7 @@ apply (clarsimp simp add: collinear_3 collinear_lemma) apply (drule Cauchy_theorem_flat [OF contf']) using pi_eq_y ynz - apply (simp add: fabc add_eq_0_iff path_integral_reverse_linepath) + apply (simp add: fabc add_eq_0_iff contour_integral_reverse_linepath) done } then obtain d where d: "d \ interior (convex hull {a, b, c})" @@ -2253,7 +2253,7 @@ \ cmod (f x' - f x) < cmod y / (24 * C)" def e \ "min 1 (min (d1/(4*C)) ((norm y / 24 / C) / B))" def shrink \ "\x. x - e *\<^sub>R (x - d)" - let ?pathint = "\x y. path_integral(linepath x y) f" + let ?pathint = "\x y. contour_integral(linepath x y) f" have e: "0 < e" "e \ 1" "e \ d1 / (4 * C)" "e \ cmod y / 24 / C / B" using d1_pos \C>0\ \B>0\ ynz by (simp_all add: e_def) then have eCB: "24 * e * C * B \ cmod y" @@ -2264,15 +2264,15 @@ "shrink b \ interior(convex hull {a,b,c})" "shrink c \ interior(convex hull {a,b,c})" using d e by (auto simp: hull_inc mem_interior_convex_shrink shrink_def) - then have fhp0: "(f has_path_integral 0) + 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) 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 path_integrable_on linepath (shrink a) (shrink b)" - "f path_integrable_on linepath (shrink b) (shrink c)" - "f path_integrable_on linepath (shrink c) (shrink a)" - using fhp0 by (auto simp: valid_path_join dest: has_path_integral_integrable) + have fpi_abc: "f contour_integrable_on linepath (shrink a) (shrink b)" + "f contour_integrable_on linepath (shrink b) (shrink c)" + "f contour_integrable_on linepath (shrink c) (shrink a)" + using fhp0 by (auto simp: valid_path_join dest: has_contour_integral_integrable) have cmod_shr: "\x y. cmod (shrink y - shrink x - (y - x)) = e * cmod (x - y)" using e by (simp add: shrink_def real_vector.scale_right_diff_distrib [symmetric]) have sh_eq: "\a b d::complex. (b - e *\<^sub>R (b - d)) - (a - e *\<^sub>R (a - d)) - (b - a) = e *\<^sub>R (a - b)" @@ -2285,7 +2285,7 @@ using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast { fix u v assume uv: "u \ convex hull {a, b, c}" "v \ convex hull {a, b, c}" "u\v" - and fpi_uv: "f path_integrable_on linepath (shrink u) (shrink v)" + and fpi_uv: "f contour_integrable_on linepath (shrink u) (shrink v)" have shr_uv: "shrink u \ interior(convex hull {a,b,c})" "shrink v \ interior(convex hull {a,b,c})" using d e uv @@ -2343,8 +2343,8 @@ _ 0 1 ]) using ynz \0 < B\ \0 < C\ apply (simp_all del: le_divide_eq_numeral1) - apply (simp add: has_integral_sub has_path_integral_linepath [symmetric] has_path_integral_integral - fpi_uv f_uv path_integrable_continuous_linepath, clarify) + apply (simp add: has_integral_sub 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) done @@ -2382,10 +2382,10 @@ then show ?thesis .. qed } - moreover have "f path_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" - using fabc path_integrable_continuous_linepath by auto + moreover have "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" + using fabc contour_integrable_continuous_linepath by auto ultimately show ?thesis - using has_path_integral_integral by fastforce + using has_contour_integral_integral by fastforce qed @@ -2395,7 +2395,7 @@ assumes "continuous_on (convex hull {a,b,c}) f" and "finite s" and "(\x. x \ interior(convex hull {a,b,c}) - s \ f complex_differentiable (at x))" - shows "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" + 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) @@ -2411,7 +2411,7 @@ then show ?thesis proof (cases "d \ convex hull {a,b,c}") case False - show "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" + 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) @@ -2420,7 +2420,7 @@ 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_path_integral 0) (linepath a b +++ linepath b d +++ linepath d a)" + 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 _ *]) @@ -2428,7 +2428,7 @@ done 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_path_integral 0) (linepath b c +++ linepath c d +++ linepath d b)" + 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 _ *]) @@ -2436,25 +2436,25 @@ done 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_path_integral 0) (linepath c a +++ linepath a d +++ linepath d c)" + 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 - have "f path_integrable_on linepath a b" + have "f contour_integrable_on linepath a b" using less.prems - by (metis continuous_on_subset insert_commute path_integrable_continuous_linepath segments_subset_convex_hull(3)) - moreover have "f path_integrable_on linepath b c" + by (metis continuous_on_subset insert_commute contour_integrable_continuous_linepath segments_subset_convex_hull(3)) + moreover have "f contour_integrable_on linepath b c" using less.prems - by (metis continuous_on_subset path_integrable_continuous_linepath segments_subset_convex_hull(3)) - moreover have "f path_integrable_on linepath c a" + by (metis continuous_on_subset contour_integrable_continuous_linepath segments_subset_convex_hull(3)) + moreover have "f contour_integrable_on linepath c a" using less.prems - by (metis continuous_on_subset insert_commute path_integrable_continuous_linepath segments_subset_convex_hull(3)) - ultimately have fpi: "f path_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" + by (metis continuous_on_subset insert_commute contour_integrable_continuous_linepath segments_subset_convex_hull(3)) + ultimately have fpi: "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" by auto { fix y::complex - assume fy: "(f has_path_integral y) (linepath a b +++ linepath b c +++ linepath c a)" + assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)" and ynz: "y \ 0" have cont_ad: "continuous_on (closed_segment a d) f" by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(3)) @@ -2462,18 +2462,18 @@ by (meson True closed_segment_subset_convex_hull continuous_on_subset hull_subset insert_subset less.prems(1)) have cont_cd: "continuous_on (closed_segment c d) f" by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(2)) - have "path_integral (linepath a b) f = - (path_integral (linepath b d) f + (path_integral (linepath d a) f))" - "path_integral (linepath b c) f = - (path_integral (linepath c d) f + (path_integral (linepath d b) f))" - "path_integral (linepath c a) f = - (path_integral (linepath a d) f + path_integral (linepath d c) f)" + 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)" using has_chain_integral_chain_integral3 [OF abd] has_chain_integral_chain_integral3 [OF bcd] has_chain_integral_chain_integral3 [OF cad] by (simp_all add: algebra_simps add_eq_0_iff) then have ?thesis - using cont_ad cont_bd cont_cd fy has_chain_integral_chain_integral3 path_integral_reverse_linepath by fastforce + using cont_ad cont_bd cont_cd fy has_chain_integral_chain_integral3 contour_integral_reverse_linepath by fastforce } then show ?thesis - using fpi path_integrable_on_def by blast + using fpi contour_integrable_on_def by blast qed qed qed @@ -2489,17 +2489,17 @@ apply (meson subs convexD convex_closed_segment ends_in_segment(1) ends_in_segment(2) subsetCE) done -lemma triangle_path_integrals_starlike_primitive: +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 - \ path_integral (linepath a b) f + path_integral (linepath b c) f + - path_integral (linepath c a) f = 0" - shows "((\x. path_integral(linepath a x) f) has_field_derivative f x) (at x)" + \ 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. path_integral(linepath x y) f" + 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" @@ -2511,7 +2511,7 @@ using close by (auto simp: dist_norm ball_def norm_minus_commute dest: segment_bound) have "?pathint a y - ?pathint a x = ?pathint x y" - using zer [OF xys] path_integral_reverse_linepath [OF cont_ayf] add_eq_0_iff by force + using zer [OF xys] contour_integral_reverse_linepath [OF cont_ayf] add_eq_0_iff by force } note [simp] = this { fix e::real assume e: "0 < e" @@ -2527,18 +2527,18 @@ assume yx: "y \ x" and close: "cmod (y - x) < min d1 d2" have y: "y \ s" using d2 close by (force simp: dist_norm norm_minus_commute) - have fxy: "f path_integrable_on linepath x y" - apply (rule path_integrable_continuous_linepath) + 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 - then obtain i where i: "(f has_path_integral i) (linepath x y)" - by (auto simp: path_integrable_on_def) - then have "((\w. f w - f x) has_path_integral (i - f x * (y - x))) (linepath x y)" - by (rule has_path_integral_diff [OF _ has_path_integral_const_linepath]) + 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_path_integral_bound_linepath [where B = "e/2"]) + 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 @@ -2547,7 +2547,7 @@ 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: path_integral_unique divide_less_eq) + using i yx by (simp add: contour_integral_unique divide_less_eq) } then have "\d>0. \y. y \ x \ cmod (y-x) < d \ cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" using dpos by blast @@ -2580,7 +2580,7 @@ by (simp add: a a_cs starlike_convex_subset) then have *: "continuous_on (convex hull {a, b, c}) f" by (simp add: continuous_on_subset [OF contf]) - have "(f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" + 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) @@ -2588,7 +2588,7 @@ } note 0 = this show ?thesis apply (intro exI ballI) - apply (rule triangle_path_integrals_starlike_primitive [OF contf a os], assumption) + apply (rule triangle_contour_integrals_starlike_primitive [OF contf a os], assumption) apply (metis a_cs) apply (metis has_chain_integral_chain_integral3 0) done @@ -2598,12 +2598,12 @@ "\open s; starlike s; finite k; continuous_on s f; \x. x \ s - k \ f complex_differentiable at x; valid_path g; path_image g \ s; pathfinish g = pathstart g\ - \ (f has_path_integral 0) 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\ - \ (f has_path_integral 0) g" + \ (f has_contour_integral 0) g" apply (rule Cauchy_theorem_starlike [OF _ _ finite.emptyI]) apply (simp_all add: holomorphic_on_imp_continuous_on) apply (metis at_within_open holomorphic_on_def) @@ -2614,16 +2614,16 @@ text\For a convex set we can avoid assuming openness and boundary analyticity\ -lemma triangle_path_integrals_convex_primitive: +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\ - \ path_integral (linepath a b) f + path_integral (linepath b c) f + - path_integral (linepath c a) f = 0" - shows "((\x. path_integral(linepath a x) f) has_field_derivative f x) (at x within 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)" proof - - let ?pathint = "\x y. path_integral(linepath x y) f" + let ?pathint = "\x y. contour_integral(linepath x y) f" { fix y assume y: "y \ s" have cont_ayf: "continuous_on (closed_segment a y) f" @@ -2631,7 +2631,7 @@ 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] path_integral_reverse_linepath [OF cont_ayf] add_eq_0_iff by force + 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" @@ -2642,15 +2642,15 @@ 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" - have fxy: "f path_integrable_on linepath x y" + have fxy: "f contour_integrable_on linepath x y" using convex_contains_segment s x y - by (blast intro!: path_integrable_continuous_linepath continuous_on_subset [OF contf]) - then obtain i where i: "(f has_path_integral i) (linepath x y)" - by (auto simp: path_integrable_on_def) - then have "((\w. f w - f x) has_path_integral (i - f x * (y - x))) (linepath x y)" - by (rule has_path_integral_diff [OF _ has_path_integral_const_linepath]) + 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_path_integral_bound_linepath [where B = "e/2"]) + 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 @@ -2659,12 +2659,12 @@ 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: path_integral_unique divide_less_eq) + 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" using d1 by blast } - then have *: "((\y. (path_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) @@ -2676,11 +2676,11 @@ lemma pathintegral_convex_primitive: "\convex s; continuous_on s f; - \a b c. \a \ s; b \ s; c \ s\ \ (f has_path_integral 0) (linepath a b +++ linepath b c +++ linepath c a)\ + \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_path_integrals_convex_primitive has_chain_integral_chain_integral3) + apply (blast intro: triangle_contour_integrals_convex_primitive has_chain_integral_chain_integral3) done lemma holomorphic_convex_primitive: @@ -2694,16 +2694,16 @@ by (metis Diff_iff convex_contains_segment insert_absorb insert_subset interior_mono segment_convex_hull subset_hull) lemma Cauchy_theorem_convex: - "\continuous_on s f;convex s; finite k; + "\continuous_on s f; convex s; finite k; \x. x \ interior s - k \ f complex_differentiable at x; valid_path g; path_image g \ s; - pathfinish g = pathstart g\ \ (f has_path_integral 0) g" + 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; - pathfinish g = pathstart g\ \ (f has_path_integral 0) g" + pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" apply (rule Cauchy_theorem_convex) apply (simp_all add: holomorphic_on_imp_continuous_on) apply (rule finite.emptyI) @@ -2715,20 +2715,20 @@ "\finite k; continuous_on (cball a e) f; \x. x \ ball a e - k \ f complex_differentiable at x; valid_path g; path_image g \ cball a e; - pathfinish g = pathstart g\ \ (f has_path_integral 0) g" + 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: "\f holomorphic_on (ball a e); valid_path g; path_image g \ ball a e; - pathfinish g = pathstart g\ \ (f has_path_integral 0) g" + pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" by (simp add: Cauchy_theorem_convex_simple) subsection\Generalize integrability to local primitives\ -lemma path_integral_local_primitive_lemma: +lemma contour_integral_local_primitive_lemma: fixes f :: "complex\complex" shows "\g piecewise_differentiable_on {a..b}; @@ -2739,10 +2739,10 @@ apply (cases "cbox a b = {}", force) apply (simp add: integrable_on_def) apply (rule exI) - apply (rule path_integral_primitive_lemma, assumption+) + apply (rule contour_integral_primitive_lemma, assumption+) using atLeastAtMost_iff by blast -lemma path_integral_local_primitive_any: +lemma contour_integral_local_primitive_any: fixes f :: "complex \ complex" assumes gpd: "g piecewise_differentiable_on {a..b}" and dh: "\x. x \ s @@ -2769,7 +2769,7 @@ apply (rule_tac x=e in exI) using e apply (simp add: integrable_on_localized_vector_derivative [symmetric], clarify) - apply (rule_tac f = h and s = "g ` {u..v}" in path_integral_local_primitive_lemma) + apply (rule_tac f = h and s = "g ` {u..v}" in contour_integral_local_primitive_lemma) apply (meson atLeastatMost_subset_iff gpd piecewise_differentiable_on_subset) apply (force simp: ball_def dist_norm intro: lessd gs DERIV_subset [OF h], force) done @@ -2778,29 +2778,29 @@ by (force simp: intro!: integrable_on_little_subintervals [of a b, simplified]) qed -lemma path_integral_local_primitive: +lemma contour_integral_local_primitive: fixes f :: "complex \ complex" assumes g: "valid_path g" "path_image g \ s" and dh: "\x. x \ s \ \d h. 0 < d \ (\y. norm(y - x) < d \ (h has_field_derivative f y) (at y within s))" - shows "f path_integrable_on g" + shows "f contour_integrable_on g" using g - apply (simp add: valid_path_def path_image_def path_integrable_on_def has_path_integral_def + apply (simp add: valid_path_def path_image_def contour_integrable_on_def has_contour_integral_def has_integral_localized_vector_derivative integrable_on_def [symmetric]) - using path_integral_local_primitive_any [OF _ dh] + using contour_integral_local_primitive_any [OF _ dh] by (meson image_subset_iff piecewise_C1_imp_differentiable) text\In particular if a function is holomorphic\ -lemma path_integrable_holomorphic: +lemma contour_integrable_holomorphic: assumes contf: "continuous_on s f" and os: "open s" and k: "finite k" and g: "valid_path g" "path_image g \ s" and fcd: "\x. x \ s - k \ f complex_differentiable at x" - shows "f path_integrable_on g" + shows "f contour_integrable_on g" proof - { fix z assume z: "z \ s" @@ -2819,25 +2819,25 @@ using d by blast } then show ?thesis - by (rule path_integral_local_primitive [OF g]) + by (rule contour_integral_local_primitive [OF g]) qed -lemma path_integrable_holomorphic_simple: +lemma contour_integrable_holomorphic_simple: assumes contf: "continuous_on s f" and os: "open s" and g: "valid_path g" "path_image g \ s" and fh: "f holomorphic_on s" - shows "f path_integrable_on g" - apply (rule path_integrable_holomorphic [OF contf os Finite_Set.finite.emptyI g]) + shows "f contour_integrable_on g" + apply (rule contour_integrable_holomorphic [OF contf os Finite_Set.finite.emptyI g]) using fh by (simp add: complex_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))" by (rule continuous_intros | force)+ -corollary path_integrable_inversediff: - "\valid_path g; z \ path_image g\ \ (\w. 1 / (w-z)) path_integrable_on g" -apply (rule path_integrable_holomorphic_simple [of "UNIV-{z}", OF continuous_on_inversediff]) +corollary contour_integrable_inversediff: + "\valid_path g; z \ path_image g\ \ (\w. 1 / (w-z)) contour_integrable_on g" +apply (rule contour_integrable_holomorphic_simple [of "UNIV-{z}", OF continuous_on_inversediff]) apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros) done @@ -2858,7 +2858,7 @@ 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 path_integral_nearby: +lemma contour_integral_nearby: assumes os: "open s" and p: "path p" "path_image p \ s" shows "\d. 0 < d \ @@ -2866,7 +2866,7 @@ (\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 \ path_integral h f = path_integral g f))" + (\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" using open_contains_ball os p(2) by blast @@ -2931,8 +2931,8 @@ moreover { fix f assume fhols: "f holomorphic_on s" - then have fpa: "f path_integrable_on g" "f path_integrable_on h" - using g ghs h holomorphic_on_imp_continuous_on os path_integrable_holomorphic_simple + 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" by (simp add: fhols holomorphic_on_imp_continuous_on) @@ -2949,8 +2949,8 @@ by metis { fix n assume n: "n \ N" - then have "path_integral(subpath 0 (n/N) h) f - path_integral(subpath 0 (n/N) g) f = - path_integral(linepath (g(n/N)) (h(n/N))) f - path_integral(linepath (g 0) (h 0)) f" + then have "contour_integral(subpath 0 (n/N) h) f - contour_integral(subpath 0 (n/N) g) f = + contour_integral(linepath (g(n/N)) (h(n/N))) f - contour_integral(linepath (g 0) (h 0)) f" proof (induct n) case 0 show ?case by simp next @@ -3014,7 +3014,7 @@ using \N>0\ Suc.prems apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee) done - have pi0: "(f has_path_integral 0) + have pi0: "(f has_contour_integral 0) (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++ 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"]) @@ -3022,50 +3022,50 @@ apply (intro valid_path_join) using Suc.prems pi_subset_ball apply (simp_all add: valid_path_subpath g h) done - have fpa1: "f path_integrable_on subpath (real n / real N) (real (Suc n) / real N) g" - using Suc.prems by (simp add: path_integrable_subpath g fpa) - have fpa2: "f path_integrable_on linepath (g (real (Suc n) / real N)) (h (real (Suc n) / real N))" + 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) + have fpa2: "f contour_integrable_on linepath (g (real (Suc n) / real N)) (h (real (Suc n) / real N))" using gh_n's - by (auto intro!: path_integrable_continuous_linepath continuous_on_subset [OF contf]) - have fpa3: "f path_integrable_on linepath (h (real n / real N)) (g (real n / real N))" + by (auto intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf]) + have fpa3: "f contour_integrable_on linepath (h (real n / real N)) (g (real n / real N))" using gh_ns - by (auto simp: closed_segment_commute intro!: path_integrable_continuous_linepath continuous_on_subset [OF contf]) - have eq0: "path_integral (subpath (n/N) ((Suc n) / real N) g) f + - path_integral (linepath (g ((Suc n) / N)) (h ((Suc n) / N))) f + - path_integral (subpath ((Suc n) / N) (n/N) h) f + - path_integral (linepath (h (n/N)) (g (n/N))) f = 0" - using path_integral_unique [OF pi0] Suc.prems - by (simp add: g h fpa valid_path_subpath path_integrable_subpath + by (auto simp: closed_segment_commute intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf]) + have eq0: "contour_integral (subpath (n/N) ((Suc n) / real N) g) f + + contour_integral (linepath (g ((Suc n) / N)) (h ((Suc n) / N))) f + + contour_integral (subpath ((Suc n) / N) (n/N) h) f + + contour_integral (linepath (h (n/N)) (g (n/N))) f = 0" + using contour_integral_unique [OF pi0] Suc.prems + by (simp add: g h fpa valid_path_subpath contour_integrable_subpath fpa1 fpa2 fpa3 algebra_simps del: of_nat_Suc) have *: "\hn he hn' gn gd gn' hgn ghn gh0 ghn'. \hn - gn = ghn - gh0; gd + ghn' + he + hgn = (0::complex); hn - he = hn'; gn + gd = gn'; hgn = -ghn\ \ hn' - gn' = ghn' - gh0" by (auto simp: algebra_simps) - have "path_integral (subpath 0 (n/N) h) f - path_integral (subpath ((Suc n) / N) (n/N) h) f = - path_integral (subpath 0 (n/N) h) f + path_integral (subpath (n/N) ((Suc n) / N) h) f" + have "contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f = + contour_integral (subpath 0 (n/N) h) f + contour_integral (subpath (n/N) ((Suc n) / N) h) f" unfolding reversepath_subpath [symmetric, of "((Suc n) / N)"] - using Suc.prems by (simp add: h fpa path_integral_reversepath valid_path_subpath path_integrable_subpath) - also have "... = path_integral (subpath 0 ((Suc n) / N) h) f" - using Suc.prems by (simp add: path_integral_subpath_combine h fpa) + using Suc.prems by (simp add: h fpa contour_integral_reversepath valid_path_subpath contour_integrable_subpath) + also have "... = contour_integral (subpath 0 ((Suc n) / N) h) f" + using Suc.prems by (simp add: contour_integral_subpath_combine h fpa) finally have pi0_eq: - "path_integral (subpath 0 (n/N) h) f - path_integral (subpath ((Suc n) / N) (n/N) h) f = - path_integral (subpath 0 ((Suc n) / N) h) f" . + "contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f = + contour_integral (subpath 0 ((Suc n) / N) h) f" . show ?case apply (rule * [OF Suc.hyps eq0 pi0_eq]) using Suc.prems - apply (simp_all add: g h fpa path_integral_subpath_combine - path_integral_reversepath [symmetric] path_integrable_continuous_linepath + apply (simp_all add: g h fpa contour_integral_subpath_combine + contour_integral_reversepath [symmetric] contour_integrable_continuous_linepath continuous_on_subset [OF contf gh_ns]) done qed } note ind = this - have "path_integral h f = path_integral g f" + have "contour_integral h f = contour_integral g f" using ind [OF order_refl] N joins by (simp add: linked_paths_def pathstart_def pathfinish_def split: split_if_asm) } ultimately - have "path_image g \ s \ path_image h \ s \ (\f. f holomorphic_on s \ path_integral h f = path_integral g f)" + have "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 @@ -3080,7 +3080,7 @@ lemma assumes "open s" "path p" "path_image p \ s" - shows path_integral_nearby_ends: + 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) \ @@ -3088,8 +3088,8 @@ \ path_image g \ s \ path_image h \ s \ (\f. f holomorphic_on s - \ path_integral h f = path_integral g f))" - and path_integral_nearby_loops: + \ 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) \ @@ -3097,9 +3097,9 @@ \ path_image g \ s \ path_image h \ s \ (\f. f holomorphic_on s - \ path_integral h f = path_integral g f))" - using path_integral_nearby [OF assms, where atends=True] - using path_integral_nearby [OF assms, where atends=False] + \ 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] unfolding linked_paths_def by simp_all corollary differentiable_polynomial_function: @@ -3122,21 +3122,21 @@ shows "z \ g x \ valid_path (subpath x x g)" by (simp add: subpath_def valid_path_polynomial_function) -lemma path_integral_bound_exists: +lemma contour_integral_bound_exists: assumes s: "open s" and g: "valid_path g" and pag: "path_image g \ s" shows "\L. 0 < L \ (\f B. f holomorphic_on s \ (\z \ s. norm(f z) \ B) - \ norm(path_integral g f) \ L*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 \ path_integral g f = path_integral p f" - using path_integral_nearby_ends [OF s \path g\ pag] + 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) @@ -3153,24 +3153,24 @@ { fix f B assume f: "f holomorphic_on s" and B: "\z. z\s \ cmod (f z) \ B" - then have "f path_integrable_on p \ valid_path p" + then have "f contour_integrable_on p \ valid_path p" using p s - by (blast intro: valid_path_polynomial_function path_integrable_holomorphic_simple holomorphic_on_imp_continuous_on) + 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) done - ultimately have "cmod (path_integral g f) \ L * B" + ultimately have "cmod (contour_integral g f) \ L * B" apply (simp add: pi [OF f]) - apply (simp add: path_integral_integral) + apply (simp add: contour_integral_integral) apply (rule order_trans [OF integral_norm_bound_integral]) - apply (auto simp: mult.commute integral_norm_bound_integral path_integrable_on [symmetric] norm_mult) + apply (auto simp: mult.commute integral_norm_bound_integral contour_integrable_on [symmetric] norm_mult) done } then show ?thesis - by (force simp: L path_integral_integral) + by (force simp: L contour_integral_integral) qed subsection\Constancy of a function from a connected set into a finite, disconnected or discrete set\ @@ -3343,7 +3343,7 @@ pathstart p = pathstart \ \ pathfinish p = pathfinish \ \ (\t \ {0..1}. norm(\ t - p t) < e) \ - path_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" lemma winding_number: assumes "path \" "z \ path_image \" "0 < e" @@ -3351,7 +3351,7 @@ pathstart p = pathstart \ \ pathfinish p = pathfinish \ \ (\t \ {0..1}. norm (\ t - p t) < e) \ - path_integral p (\w. 1/(w - z)) = 2 * pi * ii * winding_number \ z" + contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * winding_number \ z" proof - have "path_image \ \ UNIV - {z}" using assms by blast @@ -3361,16 +3361,16 @@ (\t\{0..1}. cmod (h1 t - \ t) < d \ cmod (h2 t - \ t) < d) \ pathstart h2 = pathstart h1 \ pathfinish h2 = pathfinish h1 \ path_image h1 \ UNIV - {z} \ path_image h2 \ UNIV - {z} \ - (\f. f holomorphic_on UNIV - {z} \ path_integral h2 f = path_integral h1 f)" - using path_integral_nearby_ends [of "UNIV - {z}" \] assms by (auto simp: open_delete) + (\f. f holomorphic_on UNIV - {z} \ contour_integral h2 f = contour_integral h1 f)" + using contour_integral_nearby_ends [of "UNIV - {z}" \] assms by (auto simp: open_delete) then obtain h where h: "polynomial_function h \ pathstart h = pathstart \ \ pathfinish h = pathfinish \ \ (\t \ {0..1}. norm(h t - \ t) < d/2)" using path_approx_polynomial_function [OF `path \`, of "d/2"] d by auto - def nn \ "1/(2* pi*ii) * path_integral h (\w. 1/(w - z))" + def nn \ "1/(2* pi*ii) * contour_integral h (\w. 1/(w - z))" have "\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) \ - path_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" (is "\n. \e > 0. ?PP e n") proof (rule_tac x=nn in exI, clarify) fix e::real @@ -3399,7 +3399,7 @@ "\e. e>0 \ \p. valid_path p \ z \ path_image p \ pathstart p = pathstart \ \ pathfinish p = pathfinish \ \ (\t \ {0..1}. norm (\ t - p t) < e) \ - path_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" shows "winding_number \ z = n" proof - have "path_image \ \ UNIV - {z}" @@ -3409,22 +3409,22 @@ and pi_eq: "\h1 h2 f. \valid_path h1; valid_path h2; (\t\{0..1}. cmod (h1 t - \ t) < e \ cmod (h2 t - \ t) < e); pathstart h2 = pathstart h1; pathfinish h2 = pathfinish h1; f holomorphic_on UNIV - {z}\ \ - path_integral h2 f = path_integral h1 f" - using path_integral_nearby_ends [of "UNIV - {z}" \] assms by (auto simp: open_delete) + contour_integral h2 f = contour_integral h1 f" + using contour_integral_nearby_ends [of "UNIV - {z}" \] assms by (auto simp: open_delete) obtain p where p: "valid_path p \ z \ path_image p \ pathstart p = pathstart \ \ pathfinish p = pathfinish \ \ (\t \ {0..1}. norm (\ t - p t) < e) \ - path_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" using pi [OF e] by blast obtain q where q: "valid_path q \ z \ path_image q \ pathstart q = pathstart \ \ pathfinish q = pathfinish \ \ - (\t\{0..1}. cmod (\ t - q t) < e) \ path_integral q (\w. 1 / (w - z)) = complex_of_real (2 * pi) * \ * winding_number \ z" + (\t\{0..1}. cmod (\ t - q t) < e) \ contour_integral q (\w. 1 / (w - z)) = complex_of_real (2 * pi) * \ * winding_number \ z" using winding_number [OF \ e] by blast - have "2 * complex_of_real pi * \ * n = path_integral p (\w. 1 / (w - z))" + have "2 * complex_of_real pi * \ * n = contour_integral p (\w. 1 / (w - z))" using p by auto - also have "... = path_integral q (\w. 1 / (w - z))" + 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) @@ -3442,7 +3442,7 @@ "\e. e>0 \ \p. valid_path p \ z \ path_image p \ pathfinish p = pathstart p \ (\t \ {0..1}. norm (\ t - p t) < e) \ - path_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" shows "winding_number \ z = n" proof - have "path_image \ \ UNIV - {z}" @@ -3452,22 +3452,22 @@ and pi_eq: "\h1 h2 f. \valid_path h1; valid_path h2; (\t\{0..1}. cmod (h1 t - \ t) < e \ cmod (h2 t - \ t) < e); pathfinish h1 = pathstart h1; pathfinish h2 = pathstart h2; f holomorphic_on UNIV - {z}\ \ - path_integral h2 f = path_integral h1 f" - using path_integral_nearby_loops [of "UNIV - {z}" \] assms by (auto simp: open_delete) + contour_integral h2 f = contour_integral h1 f" + using contour_integral_nearby_loops [of "UNIV - {z}" \] assms by (auto simp: open_delete) obtain p where p: "valid_path p \ z \ path_image p \ pathfinish p = pathstart p \ (\t \ {0..1}. norm (\ t - p t) < e) \ - path_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" using pi [OF e] by blast obtain q where q: "valid_path q \ z \ path_image q \ pathstart q = pathstart \ \ pathfinish q = pathfinish \ \ - (\t\{0..1}. cmod (\ t - q t) < e) \ path_integral q (\w. 1 / (w - z)) = complex_of_real (2 * pi) * \ * winding_number \ z" + (\t\{0..1}. cmod (\ t - q t) < e) \ contour_integral q (\w. 1 / (w - z)) = complex_of_real (2 * pi) * \ * winding_number \ z" using winding_number [OF \ e] by blast - have "2 * complex_of_real pi * \ * n = path_integral p (\w. 1 / (w - z))" + have "2 * complex_of_real pi * \ * n = contour_integral p (\w. 1 / (w - z))" using p by auto - also have "... = path_integral q (\w. 1 / (w - z))" + 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) @@ -3480,13 +3480,13 @@ lemma winding_number_valid_path: assumes "valid_path \" "z \ path_image \" - shows "winding_number \ z = 1/(2*pi*ii) * path_integral \ (\w. 1/(w - z))" + shows "winding_number \ z = 1/(2*pi*ii) * contour_integral \ (\w. 1/(w - z))" using assms by (auto simp: valid_path_imp_path intro!: winding_number_unique) -lemma has_path_integral_winding_number: +lemma has_contour_integral_winding_number: assumes \: "valid_path \" "z \ path_image \" - shows "((\w. 1/(w - z)) has_path_integral (2*pi*ii*winding_number \ z)) \" -by (simp add: winding_number_valid_path has_path_integral_integral path_integrable_inversediff assms) + shows "((\w. 1/(w - z)) has_contour_integral (2*pi*ii*winding_number \ z)) \" +by (simp add: winding_number_valid_path has_contour_integral_integral contour_integrable_inversediff assms) lemma winding_number_trivial [simp]: "z \ a \ winding_number(linepath a a) z = 0" by (simp add: winding_number_valid_path) @@ -3505,7 +3505,7 @@ apply (frule winding_number [OF g1], clarify) apply (rename_tac p2 p1) apply (rule_tac x="p1+++p2" in exI) - apply (simp add: not_in_path_image_join path_integrable_inversediff algebra_simps) + apply (simp add: not_in_path_image_join contour_integrable_inversediff algebra_simps) apply (auto simp: joinpaths_def) done @@ -3517,7 +3517,7 @@ apply simp_all apply (frule winding_number [OF assms], clarify) apply (rule_tac x="reversepath p" in exI) - apply (simp add: path_integral_reversepath path_integrable_inversediff valid_path_imp_reverse) + apply (simp add: contour_integral_reversepath contour_integrable_inversediff valid_path_imp_reverse) apply (auto simp: reversepath_def) done @@ -3530,7 +3530,7 @@ apply (simp_all add: path_shiftpath path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath) apply (frule winding_number [OF \], clarify) apply (rule_tac x="shiftpath a p" in exI) - apply (simp add: path_integral_shiftpath path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath valid_path_shiftpath) + apply (simp add: contour_integral_shiftpath path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath valid_path_shiftpath) apply (auto simp: shiftpath_def) done @@ -3543,7 +3543,7 @@ using assms by (meson convex_contains_segment convex_segment ends_in_segment(2) subsetCE) then show ?thesis using assms - by (simp add: winding_number_valid_path path_integral_split_linepath [symmetric] continuous_on_inversediff field_simps) + by (simp add: winding_number_valid_path contour_integral_split_linepath [symmetric] continuous_on_inversediff field_simps) qed lemma winding_number_cong: @@ -3551,7 +3551,7 @@ by (simp add: winding_number_def pathstart_def pathfinish_def) lemma winding_number_offset: "winding_number p z = winding_number (\w. p w - z) 0" - apply (simp add: winding_number_def path_integral_integral path_image_def valid_path_def pathstart_def pathfinish_def) + apply (simp add: winding_number_def contour_integral_integral path_image_def valid_path_def pathstart_def pathfinish_def) apply (intro ext arg_cong [where f = Eps] arg_cong [where f = All] imp_cong refl, safe) apply (rename_tac g) apply (rule_tac x="\t. g t - z" in exI) @@ -3574,7 +3574,7 @@ lemma Re_winding_number: "\valid_path \; z \ path_image \\ - \ Re(winding_number \ z) = Im(path_integral \ (\w. 1/(w - z))) / (2*pi)" + \ Re(winding_number \ z) = Im(contour_integral \ (\w. 1/(w - z))) / (2*pi)" by (simp add: winding_number_valid_path field_simps Re_divide power2_eq_square) lemma winding_number_pos_le: @@ -3594,9 +3594,9 @@ apply (rule has_integral_spike_interior [of 0 1 _ "\x. 1/(\ x - z) * vector_derivative \ (at x)"]) apply simp apply (simp only: box_real) - apply (subst has_path_integral [symmetric]) + apply (subst has_contour_integral [symmetric]) using \ - apply (simp add: path_integrable_inversediff has_path_integral_integral) + apply (simp add: contour_integrable_inversediff has_contour_integral_integral) done qed @@ -3606,19 +3606,19 @@ and ge: "\x. \0 < x; x < 1\ \ e \ Im (vector_derivative \ (at x) / (\ x - z))" shows "0 < Re(winding_number \ z)" proof - - have "e \ Im (path_integral \ (\w. 1 / (w - z)))" + have "e \ Im (contour_integral \ (\w. 1 / (w - z)))" apply (rule has_integral_component_le [of ii "\x. ii*e" "ii*e" "{0..1}" "\x. if x \ {0<..<1} then 1/(\ x - z) * vector_derivative \ (at x) else ii*e" - "path_integral \ (\w. 1/(w - z))", simplified]) + "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 0 1 _ "\x. 1/(\ x - z) * vector_derivative \ (at x)", simplified box_real]) apply simp - apply (subst has_path_integral [symmetric]) + apply (subst has_contour_integral [symmetric]) using \ - apply (simp_all add: path_integrable_inversediff has_path_integral_integral ge) + apply (simp_all add: contour_integrable_inversediff has_contour_integral_integral ge) done with e show ?thesis by (simp add: Re_winding_number [OF \] field_simps) @@ -3711,7 +3711,7 @@ by meson have exy: "\y. ((\x. inverse (\ x - z) * ?D\ x) has_integral y) {a..b}" unfolding integrable_on_def [symmetric] - apply (rule path_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \], of "-{z}"]) + apply (rule contour_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \], of "-{z}"]) apply (rename_tac w) apply (rule_tac x="norm(w - z)" in exI) apply (simp_all add: inverse_eq_divide) @@ -3766,7 +3766,7 @@ "\path p; z \ path_image p\ \ pathfinish p - z = exp (2 * pi * ii * winding_number p z) * (pathstart p - z)" using winding_number [of p z 1] unfolding valid_path_def path_image_def pathstart_def pathfinish_def - by (force dest: winding_number_exp_integral(2) [of _ 0 1 z] simp: field_simps path_integral_integral exp_minus) + by (force dest: winding_number_exp_integral(2) [of _ 0 1 z] simp: field_simps contour_integral_integral exp_minus) subsection\The version with complex integers and equality\ @@ -3779,15 +3779,15 @@ by (simp add: field_simps) algebra obtain p where p: "valid_path p" "z \ path_image p" "pathstart p = pathstart \" "pathfinish p = pathfinish \" - "path_integral p (\w. 1 / (w - z)) = complex_of_real (2 * pi) * \ * winding_number \ z" + "contour_integral p (\w. 1 / (w - z)) = complex_of_real (2 * pi) * \ * winding_number \ z" using winding_number [OF assms, of 1] by auto - have [simp]: "(winding_number \ z \ \) = (Exp (path_integral p (\w. 1 / (w - z))) = 1)" + have [simp]: "(winding_number \ z \ \) = (Exp (contour_integral p (\w. 1 / (w - z))) = 1)" using p by (simp add: exp_eq_1 complex_is_Int_iff) have "winding_number p z \ \ \ pathfinish p = pathstart p" using p z apply (simp add: winding_number_valid_path valid_path_def path_image_def pathstart_def pathfinish_def) using winding_number_exp_integral(2) [of p 0 1 z] - apply (simp add: field_simps path_integral_integral exp_minus) + apply (simp add: field_simps contour_integral_integral exp_minus) apply (rule *) apply (auto simp: path_image_def field_simps) done @@ -3822,7 +3822,7 @@ by (simp add: Arg less_eq_real_def) also have "... \ Im (integral {0..1} (\x. vector_derivative \ (at x) / (\ x - z)))" using 1 - apply (simp add: winding_number_valid_path [OF \ z] Cauchy_Integral_Thm.path_integral_integral) + apply (simp add: winding_number_valid_path [OF \ z] Cauchy_Integral_Thm.contour_integral_integral) apply (simp add: Complex.Re_divide field_simps power2_eq_square) done finally have "Arg r \ Im (integral {0..1} (\x. vector_derivative \ (at x) / (\ x - z)))" . @@ -3927,12 +3927,12 @@ \ path_image h1 \ - cball z (e / 2) \ path_image h2 \ - cball z (e / 2) \ - (\f. f holomorphic_on - cball z (e / 2) \ path_integral h2 f = path_integral h1 f)" - using path_integral_nearby_ends [OF oc \ ppag] by metis + (\f. f holomorphic_on - cball z (e / 2) \ contour_integral h2 f = contour_integral h1 f)" + using contour_integral_nearby_ends [OF oc \ ppag] by metis obtain p where p: "valid_path p" "z \ path_image p" "pathstart p = pathstart \ \ pathfinish p = pathfinish \" and pg: "\t. t\{0..1} \ cmod (\ t - p t) < min d e / 2" - and pi: "path_integral p (\x. 1 / (x - z)) = complex_of_real (2 * pi) * \ * winding_number \ z" + and pi: "contour_integral p (\x. 1 / (x - z)) = complex_of_real (2 * pi) * \ * winding_number \ z" using winding_number [OF \ z, of "min d e / 2"] `d>0` `e>0` by auto { fix w assume d2: "cmod (w - z) < d/2" and e2: "cmod (w - z) < e/2" @@ -3950,17 +3950,17 @@ then obtain q where q: "valid_path q" "w \ path_image q" "pathstart q = pathstart \ \ pathfinish q = pathfinish \" and qg: "\t. t \ {0..1} \ cmod (\ t - q t) < min k (min d e) / 2" - and qi: "path_integral q (\u. 1 / (u - w)) = complex_of_real (2 * pi) * \ * winding_number \ w" + and qi: "contour_integral q (\u. 1 / (u - w)) = complex_of_real (2 * pi) * \ * winding_number \ w" using winding_number [OF \ wnotg, of "min k (min d e) / 2"] `d>0` `e>0` k by (force simp: min_divide_distrib_right) - have "path_integral p (\u. 1 / (u - w)) = path_integral q (\u. 1 / (u - w))" + have "contour_integral p (\u. 1 / (u - w)) = contour_integral q (\u. 1 / (u - w))" apply (rule pi_eq [OF `valid_path q` `valid_path p`, THEN conjunct2, THEN conjunct2, rule_format]) apply (frule pg) apply (frule qg) using p q `d>0` e2 apply (auto simp: dist_norm norm_minus_commute intro!: holomorphic_intros) done - then have "path_integral p (\x. 1 / (x - w)) = complex_of_real (2 * pi) * \ * winding_number \ w" + then have "contour_integral p (\x. 1 / (x - w)) = complex_of_real (2 * pi) * \ * winding_number \ w" by (simp add: pi qi) } note pip = this have "path p" @@ -3978,16 +3978,16 @@ where "L>0" and L: "\f B. \f holomorphic_on - cball z (3 / 4 * pe); \z \ - cball z (3 / 4 * pe). cmod (f z) \ B\ \ - cmod (path_integral p f) \ L * B" - using path_integral_bound_exists [of "- cball z (3/4*pe)" p] cbp `valid_path p` by force + cmod (contour_integral p f) \ L * B" + using contour_integral_bound_exists [of "- cball z (3/4*pe)" p] cbp `valid_path p` by force { fix e::real and w::complex assume e: "0 < e" and w: "cmod (w - z) < pe/4" "cmod (w - z) < e * pe\<^sup>2 / (8 * L)" then have [simp]: "w \ path_image p" using cbp p(2) `0 < pe` by (force simp: dist_norm norm_minus_commute path_image_def cball_def) - have [simp]: "path_integral p (\x. 1/(x - w)) - path_integral p (\x. 1/(x - z)) = - path_integral p (\x. 1/(x - w) - 1/(x - z))" - by (simp add: p path_integrable_inversediff path_integral_diff) + have [simp]: "contour_integral p (\x. 1/(x - w)) - contour_integral p (\x. 1/(x - z)) = + contour_integral p (\x. 1/(x - w) - 1/(x - z))" + by (simp add: p contour_integrable_inversediff contour_integral_diff) { fix x assume pe: "3/4 * pe < cmod (z - x)" have "cmod (w - x) < pe/4 + cmod (z - x)" @@ -4025,14 +4025,14 @@ apply (auto simp: divide_simps mult_less_0_iff norm_minus_commute norm_divide norm_mult power2_eq_square) done } note L_cmod_le = this - have *: "cmod (path_integral p (\x. 1 / (x - w) - 1 / (x - z))) \ L * (e * pe\<^sup>2 / L / 4 * (inverse (pe / 2))\<^sup>2)" + have *: "cmod (contour_integral p (\x. 1 / (x - w) - 1 / (x - z))) \ L * (e * pe\<^sup>2 / L / 4 * (inverse (pe / 2))\<^sup>2)" apply (rule L) using `pe>0` w apply (force simp: dist_norm norm_minus_commute intro!: holomorphic_intros) using `pe>0` w `L>0` apply (auto simp: cball_def dist_norm field_simps L_cmod_le simp del: less_divide_eq_numeral1 le_divide_eq_numeral1) done - have "cmod (path_integral p (\x. 1 / (x - w)) - path_integral p (\x. 1 / (x - z))) < 2*e" + have "cmod (contour_integral p (\x. 1 / (x - w)) - contour_integral p (\x. 1 / (x - z))) < 2*e" apply (simp add:) apply (rule le_less_trans [OF *]) using `L>0` e @@ -4142,12 +4142,12 @@ then have "w \ path_image p" using w by blast then have "\p. valid_path p \ w \ path_image p \ pathstart p = pathstart \ \ pathfinish p = pathfinish \ \ - (\t\{0..1}. cmod (\ t - p t) < e) \ path_integral p (\wa. 1 / (wa - w)) = 0" + (\t\{0..1}. cmod (\ t - p t) < e) \ contour_integral p (\wa. 1 / (wa - w)) = 0" apply (rule_tac x=p in exI) apply (simp add: p valid_path_polynomial_function) apply (intro conjI) using pge apply (simp add: norm_minus_commute) - apply (rule path_integral_unique [OF Cauchy_theorem_convex_simple [OF _ convex_ball [of 0 "B+1"]]]) + apply (rule contour_integral_unique [OF Cauchy_theorem_convex_simple [OF _ convex_ball [of 0 "B+1"]]]) apply (rule holomorphic_intros | simp add: dist_norm)+ using mem_ball_0 w apply blast using p apply (simp_all add: valid_path_polynomial_function loop pip) @@ -4218,9 +4218,9 @@ if x: "0 \ x" "x \ 1" for x proof - have "integral {0..x} (\t. vector_derivative \ (at t) / (\ t - z)) / (2 * of_real pi * \) = - 1 / (2*pi*ii) * path_integral (subpath 0 x \) (\w. 1/(w - z))" + 1 / (2*pi*ii) * contour_integral (subpath 0 x \) (\w. 1/(w - z))" using assms x - apply (simp add: path_integral_subpath_integral [OF path_integrable_inversediff]) + apply (simp add: contour_integral_subcontour_integral [OF contour_integrable_inversediff]) done also have "... = winding_number (subpath 0 x \) z" apply (subst winding_number_valid_path) @@ -4235,7 +4235,7 @@ integral {0..x} (\t. 1/(\ t - z) * vector_derivative \ (at t))"]) apply (rule continuous_intros)+ apply (rule indefinite_integral_continuous) - apply (rule path_integrable_inversediff [OF assms, unfolded path_integrable_on]) + apply (rule contour_integrable_inversediff [OF assms, unfolded contour_integrable_on]) using assms apply (simp add: *) done @@ -4379,7 +4379,7 @@ and fcd: "(\x. x \ interior s - k \ f complex_differentiable at x)" and z: "z \ interior s - k" and vpg: "valid_path \" and pasz: "path_image \ \ s - {z}" and loop: "pathfinish \ = pathstart \" - shows "((\w. f w / (w - z)) has_path_integral (2*pi * ii * winding_number \ z * f z)) \" + shows "((\w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \ z * f z)) \" proof - obtain f' where f': "(f has_field_derivative f') (at z)" using fcd [OF z] by (auto simp: complex_differentiable_def) @@ -4404,7 +4404,7 @@ using False by auto qed have fink': "finite (insert z k)" using \finite k\ by blast - have *: "((\w. if w = z then f' else (f w - f z) / (w - z)) has_path_integral 0) \" + have *: "((\w. if w = z then f' else (f w - f z) / (w - z)) has_contour_integral 0) \" apply (rule Cauchy_theorem_convex [OF _ s fink' _ vpg pas loop]) using c apply (force simp: continuous_on_eq_continuous_within) apply (rename_tac w) @@ -4414,8 +4414,8 @@ apply (rule derivative_intros fcd | simp)+ done show ?thesis - apply (rule has_path_integral_eq) - using znotin has_path_integral_add [OF has_path_integral_lmul [OF has_path_integral_winding_number [OF vpg znotin], of "f z"] *] + apply (rule has_contour_integral_eq) + using znotin has_contour_integral_add [OF has_contour_integral_lmul [OF has_contour_integral_winding_number [OF vpg znotin], of "f z"] *] apply (auto simp: mult_ac divide_simps) done qed @@ -4423,9 +4423,309 @@ theorem Cauchy_integral_formula_convex_simple: "\convex s; f holomorphic_on s; z \ interior s; valid_path \; path_image \ \ s - {z}; pathfinish \ = pathstart \\ - \ ((\w. f w / (w - z)) has_path_integral (2*pi * ii * winding_number \ z * f z)) \" + \ ((\w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \ z * f z)) \" apply (rule Cauchy_integral_formula_weak [where k = "{}"]) using holomorphic_on_imp_continuous_on by auto (metis at_within_interior holomorphic_on_def interiorE subsetCE) + +subsection\Homotopy forms of Cauchy's theorem\ + +proposition Cauchy_theorem_homotopic: + assumes hom: "if atends then homotopic_paths s g h else homotopic_loops s g h" + and "open s" and f: "f holomorphic_on s" + and vpg: "valid_path g" and vph: "valid_path h" + shows "contour_integral g f = contour_integral h f" +proof - + have pathsf: "linked_paths atends g h" + using hom by (auto simp: linked_paths_def homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish homotopic_loops_imp_loop) + obtain k :: "real \ real \ complex" + where contk: "continuous_on ({0..1} \ {0..1}) k" + and ks: "k ` ({0..1} \ {0..1}) \ s" + and k [simp]: "\x. k (0, x) = g x" "\x. k (1, x) = h x" + and ksf: "\t\{0..1}. linked_paths atends g (\x. k (t, x))" + using hom pathsf by (auto simp: linked_paths_def homotopic_paths_def homotopic_loops_def homotopic_with_def split: split_if_asm) + have ucontk: "uniformly_continuous_on ({0..1} \ {0..1}) k" + by (blast intro: compact_Times compact_uniformly_continuous [OF contk]) + { fix t::real assume t: "t \ {0..1}" + have pak: "path (k o (\u. (t, u)))" + unfolding path_def + apply (rule continuous_intros continuous_on_subset [OF contk])+ + using t by force + have pik: "path_image (k \ Pair t) \ s" + using ks t by (auto simp: path_image_def) + obtain e where "e>0" and e: + "\g h. \valid_path g; valid_path h; + \u\{0..1}. cmod (g u - (k \ Pair t) u) < e \ cmod (h u - (k \ Pair t) u) < e; + linked_paths atends g h\ + \ contour_integral h f = contour_integral g f" + using contour_integral_nearby [OF \open s\ pak pik, of atends] f by metis + obtain d where "d>0" and d: + "\x x'. \x \ {0..1} \ {0..1}; x' \ {0..1} \ {0..1}; norm (x'-x) < d\ \ norm (k x' - k x) < e/4" + by (rule uniformly_continuous_onE [OF ucontk, of "e/4"]) (auto simp: dist_norm `e>0`) + { fix t1 t2 + assume t1: "0 \ t1" "t1 \ 1" and t2: "0 \ t2" "t2 \ 1" and ltd: "\t1 - t\ < d" "\t2 - t\ < d" + have no2: "\g1 k1 kt. \norm(g1 - k1) < e/4; norm(k1 - kt) < e/4\ \ norm(g1 - kt) < e" + using \e > 0\ + apply (rule_tac y = k1 in norm_triangle_half_l) + apply (auto simp: norm_minus_commute intro: order_less_trans) + done + have "\d>0. \g1 g2. valid_path g1 \ valid_path g2 \ + (\u\{0..1}. cmod (g1 u - k (t1, u)) < d \ cmod (g2 u - k (t2, u)) < d) \ + linked_paths atends g1 g2 \ + contour_integral g2 f = contour_integral g1 f" + apply (rule_tac x="e/4" in exI) + using t t1 t2 ltd \e > 0\ + apply (auto intro!: e simp: d no2 simp del: less_divide_eq_numeral1) + done + } + then have "\e. 0 < e \ + (\t1 t2. t1 \ {0..1} \ t2 \ {0..1} \ abs(t1 - t) < e \ abs(t2 - t) < e + \ (\d. 0 < d \ + (\g1 g2. valid_path g1 \ valid_path g2 \ + (\u \ {0..1}. + norm(g1 u - k((t1,u))) < d \ norm(g2 u - k((t2,u))) < d) \ + linked_paths atends g1 g2 + \ contour_integral g2 f = contour_integral g1 f)))" + by (rule_tac x=d in exI) (simp add: \d > 0\) + } + then obtain ee where ee: + "\t. t \ {0..1} \ ee t > 0 \ + (\t1 t2. t1 \ {0..1} \ t2 \ {0..1} \ abs(t1 - t) < ee t \ abs(t2 - t) < ee t + \ (\d. 0 < d \ + (\g1 g2. valid_path g1 \ valid_path g2 \ + (\u \ {0..1}. + norm(g1 u - k((t1,u))) < d \ norm(g2 u - k((t2,u))) < d) \ + linked_paths atends g1 g2 + \ contour_integral g2 f = contour_integral g1 f)))" + by metis + note ee_rule = ee [THEN conjunct2, rule_format] + def C \ "(\t. ball t (ee t / 3)) ` {0..1}" + have "\t \ C. open t" by (simp add: C_def) + moreover have "{0..1} \ \C" + using ee [THEN conjunct1] by (auto simp: C_def dist_norm) + ultimately obtain C' where C': "C' \ C" "finite C'" and C'01: "{0..1} \ \C'" + by (rule compactE [OF compact_interval]) + def kk \ "{t \ {0..1}. ball t (ee t / 3) \ C'}" + have kk01: "kk \ {0..1}" by (auto simp: kk_def) + def e \ "Min (ee ` kk)" + have C'_eq: "C' = (\t. ball t (ee t / 3)) ` kk" + using C' by (auto simp: kk_def C_def) + have ee_pos[simp]: "\t. t \ {0..1} \ ee t > 0" + by (simp add: kk_def ee) + moreover have "finite kk" + using \finite C'\ kk01 by (force simp: C'_eq inj_on_def ball_eq_ball_iff dest: ee_pos finite_imageD) + moreover have "kk \ {}" using \{0..1} \ \C'\ C'_eq by force + ultimately have "e > 0" + using finite_less_Inf_iff [of "ee ` kk" 0] kk01 by (force simp: e_def) + then obtain N::nat where "N > 0" and N: "1/N < e/3" + by (meson divide_pos_pos nat_approx_posE zero_less_Suc zero_less_numeral) + have e_le_ee: "\i. i \ kk \ e \ ee i" + using \finite kk\ by (simp add: e_def Min_le_iff [of "ee ` kk"]) + have plus: "\t \ kk. x \ ball t (ee t / 3)" if "x \ {0..1}" for x + using C' subsetD [OF C'01 that] unfolding C'_eq by blast + have [OF order_refl]: + "\d. 0 < d \ (\j. valid_path j \ (\u \ {0..1}. norm(j u - k (n/N, u)) < d) \ linked_paths atends g j + \ contour_integral j f = contour_integral g f)" + if "n \ N" for n + using that + proof (induct n) + case 0 show ?case using ee_rule [of 0 0 0] + apply clarsimp + apply (rule_tac x=d in exI, safe) + by (metis diff_self vpg norm_zero) + next + case (Suc n) + then have N01: "n/N \ {0..1}" "(Suc n)/N \ {0..1}" by auto + then obtain t where t: "t \ kk" "n/N \ ball t (ee t / 3)" + using plus [of "n/N"] by blast + then have nN_less: "\n/N - t\ < ee t" + by (simp add: dist_norm del: less_divide_eq_numeral1) + have n'N_less: "\real (Suc n) / real N - t\ < ee t" + using t N \N > 0\ e_le_ee [of t] + by (simp add: dist_norm add_divide_distrib abs_diff_less_iff del: less_divide_eq_numeral1) (simp add: field_simps) + have t01: "t \ {0..1}" using `kk \ {0..1}` `t \ kk` by blast + obtain d1 where "d1 > 0" and d1: + "\g1 g2. \valid_path g1; valid_path g2; + \u\{0..1}. cmod (g1 u - k (n/N, u)) < d1 \ cmod (g2 u - k ((Suc n) / N, u)) < d1; + linked_paths atends g1 g2\ + \ contour_integral g2 f = contour_integral g1 f" + using ee [THEN conjunct2, rule_format, OF t01 N01 nN_less n'N_less] by fastforce + have "n \ N" using Suc.prems by auto + with Suc.hyps + obtain d2 where "d2 > 0" + and d2: "\j. \valid_path j; \u\{0..1}. cmod (j u - k (n/N, u)) < d2; linked_paths atends g j\ + \ contour_integral j f = contour_integral g f" + by auto + have "continuous_on {0..1} (k o (\u. (n/N, u)))" + apply (rule continuous_intros continuous_on_subset [OF contk])+ + using N01 by auto + then have pkn: "path (\u. k (n/N, u))" + by (simp add: path_def) + have min12: "min d1 d2 > 0" by (simp add: `0 < d1` `0 < d2`) + obtain p where "polynomial_function p" + and psf: "pathstart p = pathstart (\u. k (n/N, u))" + "pathfinish p = pathfinish (\u. k (n/N, u))" + and pk_le: "\t. t\{0..1} \ cmod (p t - k (n/N, t)) < min d1 d2" + using path_approx_polynomial_function [OF pkn min12] by blast + then have vpp: "valid_path p" using valid_path_polynomial_function by blast + have lpa: "linked_paths atends g p" + by (metis (mono_tags, lifting) N01(1) ksf linked_paths_def pathfinish_def pathstart_def psf) + show ?case + apply (rule_tac x="min d1 d2" in exI) + apply (simp add: `0 < d1` `0 < d2`, clarify) + apply (rule_tac s="contour_integral p f" in trans) + using pk_le N01(1) ksf pathfinish_def pathstart_def + apply (force intro!: vpp d1 simp add: linked_paths_def psf ksf) + using pk_le N01 apply (force intro!: vpp d2 lpa simp add: linked_paths_def psf ksf) + done + qed + then obtain d where "0 < d" + "\j. valid_path j \ (\u \ {0..1}. norm(j u - k (1,u)) < d) \ + linked_paths atends g j + \ contour_integral j f = contour_integral g f" + using \N>0\ by auto + then have "linked_paths atends g h \ contour_integral h f = contour_integral g f" + using \N>0\ vph by fastforce + then show ?thesis + by (simp add: pathsf) +qed + +proposition Cauchy_theorem_homotopic_paths: + assumes hom: "homotopic_paths s g h" + and "open s" and f: "f holomorphic_on s" + and vpg: "valid_path g" and vph: "valid_path h" + shows "contour_integral g f = contour_integral h f" + using Cauchy_theorem_homotopic [of True s g h] assms by simp + +proposition Cauchy_theorem_homotopic_loops: + assumes hom: "homotopic_loops s g h" + and "open s" and f: "f holomorphic_on s" + and vpg: "valid_path g" and vph: "valid_path h" + shows "contour_integral g f = contour_integral h f" + using Cauchy_theorem_homotopic [of False s g h] assms by simp + +lemma has_contour_integral_newpath: + "\(f has_contour_integral y) h; f contour_integrable_on g; contour_integral g f = contour_integral h f\ + \ (f has_contour_integral y) g" + using has_contour_integral_integral contour_integral_unique by auto + +lemma Cauchy_theorem_null_homotopic: + "\f holomorphic_on s; open s; valid_path g; homotopic_loops s g (linepath a a)\ \ (f has_contour_integral 0) g" + apply (rule has_contour_integral_newpath [where h = "linepath a a"], simp) + using contour_integrable_holomorphic_simple + apply (blast dest: holomorphic_on_imp_continuous_on homotopic_loops_imp_subset) + by (simp add: Cauchy_theorem_homotopic_loops) + + + +subsection\More winding number properties\ + +text\including the fact that it's +-1 inside a simple closed curve.\ + +lemma winding_number_homotopic_paths: + assumes "homotopic_paths (-{z}) g h" + shows "winding_number g z = winding_number h z" +proof - + have "path g" "path h" using homotopic_paths_imp_path [OF assms] by auto + moreover have pag: "z \ path_image g" and pah: "z \ path_image h" + using homotopic_paths_imp_subset [OF assms] by auto + ultimately obtain d e where "d > 0" "e > 0" + and d: "\p. \path p; pathstart p = pathstart g; pathfinish p = pathfinish g; \t\{0..1}. norm (p t - g t) < d\ + \ homotopic_paths (-{z}) g p" + and e: "\q. \path q; pathstart q = pathstart h; pathfinish q = pathfinish h; \t\{0..1}. norm (q t - h t) < e\ + \ homotopic_paths (-{z}) h q" + using homotopic_nearby_paths [of g "-{z}"] homotopic_nearby_paths [of h "-{z}"] by force + obtain p where p: + "valid_path p" "z \ path_image p" + "pathstart p = pathstart g" "pathfinish p = pathfinish g" + and gp_less:"\t\{0..1}. cmod (g t - p t) < d" + and pap: "contour_integral p (\w. 1 / (w - z)) = complex_of_real (2 * pi) * \ * winding_number g z" + using winding_number [OF \path g\ pag \0 < d\] by blast + obtain q where q: + "valid_path q" "z \ path_image q" + "pathstart q = pathstart h" "pathfinish q = pathfinish h" + and hq_less: "\t\{0..1}. cmod (h t - q t) < e" + and paq: "contour_integral q (\w. 1 / (w - z)) = complex_of_real (2 * pi) * \ * winding_number h z" + using winding_number [OF \path h\ pah \0 < e\] by blast + have gp: "homotopic_paths (- {z}) g p" + by (simp add: d p valid_path_imp_path norm_minus_commute gp_less) + have hq: "homotopic_paths (- {z}) h q" + by (simp add: e q valid_path_imp_path norm_minus_commute hq_less) + have "contour_integral p (\w. 1/(w - z)) = contour_integral q (\w. 1/(w - z))" + apply (rule Cauchy_theorem_homotopic_paths [of "-{z}"]) + apply (blast intro: homotopic_paths_trans homotopic_paths_sym gp hq assms) + apply (auto intro!: holomorphic_intros simp: p q) + done + then show ?thesis + by (simp add: pap paq) +qed + +lemma winding_number_homotopic_loops: + assumes "homotopic_loops (-{z}) g h" + shows "winding_number g z = winding_number h z" +proof - + have "path g" "path h" using homotopic_loops_imp_path [OF assms] by auto + moreover have pag: "z \ path_image g" and pah: "z \ path_image h" + using homotopic_loops_imp_subset [OF assms] by auto + moreover have gloop: "pathfinish g = pathstart g" and hloop: "pathfinish h = pathstart h" + using homotopic_loops_imp_loop [OF assms] by auto + ultimately obtain d e where "d > 0" "e > 0" + and d: "\p. \path p; pathfinish p = pathstart p; \t\{0..1}. norm (p t - g t) < d\ + \ homotopic_loops (-{z}) g p" + and e: "\q. \path q; pathfinish q = pathstart q; \t\{0..1}. norm (q t - h t) < e\ + \ homotopic_loops (-{z}) h q" + using homotopic_nearby_loops [of g "-{z}"] homotopic_nearby_loops [of h "-{z}"] by force + obtain p where p: + "valid_path p" "z \ path_image p" + "pathstart p = pathstart g" "pathfinish p = pathfinish g" + and gp_less:"\t\{0..1}. cmod (g t - p t) < d" + and pap: "contour_integral p (\w. 1 / (w - z)) = complex_of_real (2 * pi) * \ * winding_number g z" + using winding_number [OF \path g\ pag \0 < d\] by blast + obtain q where q: + "valid_path q" "z \ path_image q" + "pathstart q = pathstart h" "pathfinish q = pathfinish h" + and hq_less: "\t\{0..1}. cmod (h t - q t) < e" + and paq: "contour_integral q (\w. 1 / (w - z)) = complex_of_real (2 * pi) * \ * winding_number h z" + using winding_number [OF \path h\ pah \0 < e\] by blast + have gp: "homotopic_loops (- {z}) g p" + by (simp add: gloop d gp_less norm_minus_commute p valid_path_imp_path) + 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 + then show ?thesis + by (simp add: pap paq) +qed + +lemma winding_number_paths_linear_eq: + "\path g; path h; pathstart h = pathstart g; pathfinish h = pathfinish g; + \t. t \ {0..1} \ z \ closed_segment (g t) (h t)\ + \ winding_number h z = winding_number g z" + by (blast intro: sym homotopic_paths_linear winding_number_homotopic_paths elim: ) + +lemma winding_number_loops_linear_eq: + "\path g; path h; pathfinish g = pathstart g; pathfinish h = pathstart h; + \t. t \ {0..1} \ z \ closed_segment (g t) (h t)\ + \ winding_number h z = winding_number g z" + by (blast intro: sym homotopic_loops_linear winding_number_homotopic_loops elim: ) + +lemma winding_number_nearby_paths_eq: + "\path g; path h; + pathstart h = pathstart g; pathfinish h = pathfinish g; + \t. t \ {0..1} \ norm(h t - g t) < norm(g t - z)\ + \ winding_number h z = winding_number g z" + by (metis segment_bound(2) norm_minus_commute not_le winding_number_paths_linear_eq) + +lemma winding_number_nearby_loops_eq: + "\path g; path h; + pathfinish g = pathstart g; + pathfinish h = pathstart h; + \t. t \ {0..1} \ norm(h t - g t) < norm(g t - z)\ + \ winding_number h z = winding_number g z" + by (metis segment_bound(2) norm_minus_commute not_le winding_number_loops_linear_eq) + end diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Nov 23 16:57:54 2015 +0000 @@ -6410,14 +6410,6 @@ by (auto simp add:norm_minus_commute) qed -lemma segment_bound: - fixes x a b :: "'a::euclidean_space" - assumes "x \ closed_segment a b" - shows "norm (x - a) \ norm (b - a)" "norm (x - b) \ norm (b - a)" - using segment_furthest_le[OF assms, of a] - using segment_furthest_le[OF assms, of b] - by (auto simp add:norm_minus_commute) - lemma closed_segment_commute: "closed_segment a b = closed_segment b a" proof - have "{a, b} = {b, a}" by auto @@ -6425,6 +6417,25 @@ by (simp add: segment_convex_hull) qed +lemma segment_bound1: + assumes "x \ closed_segment a b" + shows "norm (x - a) \ norm (b - a)" +proof - + obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \ u" "u \ 1" + using assms by (auto simp add: closed_segment_def) + then show "norm (x - a) \ norm (b - a)" + apply clarify + apply (auto simp: algebra_simps) + apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le) + done +qed + +lemma segment_bound: + assumes "x \ closed_segment a b" + shows "norm (x - a) \ norm (b - a)" "norm (x - b) \ norm (b - a)" +apply (simp add: assms segment_bound1) +by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1) + lemma open_segment_commute: "open_segment a b = open_segment b a" proof - have "{a, b} = {b, a}" by auto @@ -6489,6 +6500,28 @@ lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval +lemma open_segment_eq: "open_segment a b = (if a=b then {} else {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 < u \ u < 1})" + by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1) + +lemma open_segment_bound1: + assumes "x \ open_segment a b" + shows "norm (x - a) < norm (b - a)" +proof - + obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \ b" + using assms by (auto simp add: open_segment_eq split: split_if_asm) + then show "norm (x - a) < norm (b - a)" + apply clarify + apply (auto simp: algebra_simps) + apply (simp add: scaleR_diff_right [symmetric]) + done +qed + +lemma open_segment_bound: + assumes "x \ open_segment a b" + shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)" +apply (simp add: assms open_segment_bound1) +by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute) + lemma closure_closed_segment [simp]: fixes a :: "'a::euclidean_space" shows "closure(closed_segment a b) = closed_segment a b" diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Multivariate_Analysis/Path_Connected.thy --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Nov 23 16:57:54 2015 +0000 @@ -1,5 +1,5 @@ (* Title: HOL/Multivariate_Analysis/Path_Connected.thy - Author: Robert Himmelmann, TU Muenchen, and LCP with material from HOL Light + Author: Robert Himmelmann, TU Muenchen, and LC Paulson with material from HOL Light *) section \Continuous paths and path-connected sets\ @@ -8,21 +8,6 @@ imports Convex_Euclidean_Space begin -(*FIXME move up?*) -lemma image_affinity_interval: - fixes c :: "'a::ordered_real_vector" - shows "((\x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {} - else if 0 <= m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} - else {m *\<^sub>R b + c .. m *\<^sub>R a + c})" - apply (case_tac "m=0", force) - apply (auto simp: scaleR_left_mono) - apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: pos_le_divideR_eq le_diff_eq scaleR_left_mono_neg) - apply (metis diff_le_eq inverse_inverse_eq order.not_eq_order_implies_strict pos_le_divideR_eq positive_imp_inverse_positive) - apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: not_le neg_le_divideR_eq diff_le_eq) - using le_diff_eq scaleR_le_cancel_left_neg - apply fastforce - done - subsection \Paths and Arcs\ definition path :: "(real \ 'a::topological_space) \ bool" @@ -1019,7 +1004,7 @@ lemma linepath_trivial [simp]: "linepath a a x = a" by (simp add: linepath_def real_vector.scale_left_diff_distrib) - + lemma subpath_refl: "subpath a a g = linepath (g a) (g a)" by (simp add: subpath_def linepath_def algebra_simps) @@ -1333,14 +1318,7 @@ lemma homeomorphic_path_connectedness: "s homeomorphic t \ path_connected s \ path_connected t" - unfolding homeomorphic_def homeomorphism_def - apply (erule exE|erule conjE)+ - apply rule - apply (drule_tac f=f in path_connected_continuous_image) - prefer 3 - apply (drule_tac f=g in path_connected_continuous_image) - apply auto - done + unfolding homeomorphic_def homeomorphism_def by (metis path_connected_continuous_image) lemma path_connected_empty: "path_connected {}" unfolding path_connected_def by auto @@ -2809,8 +2787,11 @@ proposition homotopic_paths_refl [simp]: "homotopic_paths s p p \ path p \ path_image p \ s" by (simp add: homotopic_paths_def homotopic_with_refl path_def path_image_def) -proposition homotopic_paths_sym: "homotopic_paths s p q \ homotopic_paths s q p" - by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)+ +proposition homotopic_paths_sym: "homotopic_paths s p q \ homotopic_paths s q p" + by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD) + +proposition homotopic_paths_sym_eq: "homotopic_paths s p q \ homotopic_paths s q p" + by (metis homotopic_paths_sym) proposition homotopic_paths_trans: "\homotopic_paths s p q; homotopic_paths s q r\ \ homotopic_paths s p r" @@ -2938,7 +2919,7 @@ proposition homotopic_paths_lid: "\path p; path_image p \ s\ \ homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p" using homotopic_paths_rid [of "reversepath p" s] - by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath + by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath pathfinish_reversepath reversepath_joinpaths reversepath_linepath) proposition homotopic_paths_assoc: @@ -2961,7 +2942,7 @@ shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))" proof - have "continuous_on ({0..1} \ {0..1}) (\x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))" - using assms + using assms apply (simp add: joinpaths_def subpath_def reversepath_def path_def del: le_divide_eq_numeral1) apply (rule continuous_on_cases_le) apply (rule_tac [2] continuous_on_compose [of _ _ p, unfolded o_def]) @@ -2971,8 +2952,8 @@ done then show ?thesis using assms - apply (subst homotopic_paths_sym) - apply (simp add: homotopic_paths_def homotopic_with_def) + apply (subst homotopic_paths_sym_eq) + unfolding homotopic_paths_def homotopic_with_def apply (rule_tac x="(\y. (subpath 0 (fst y) p +++ reversepath(subpath 0 (fst y) p)) (snd y))" in exI) apply (simp add: path_defs joinpaths_def subpath_def reversepath_def) apply (force simp: mult_le_one) @@ -3009,25 +2990,22 @@ unfolding homotopic_loops_def path_def using homotopic_with_imp_continuous by blast -proposition homotopic_loops_imp_subset1: - "homotopic_loops s p q \ path_image p \ s" +proposition homotopic_loops_imp_subset: + "homotopic_loops s p q \ path_image p \ s \ path_image q \ s" unfolding homotopic_loops_def path_image_def - using homotopic_with_imp_subset1 by blast - -proposition homotopic_loops_imp_subset2: - "homotopic_loops s p q \ path_image q \ s" - unfolding homotopic_loops_def path_image_def - using homotopic_with_imp_subset2 by blast + by (metis homotopic_with_imp_subset1 homotopic_with_imp_subset2) proposition homotopic_loops_refl: "homotopic_loops s p p \ path p \ path_image p \ s \ pathfinish p = pathstart p" by (simp add: homotopic_loops_def homotopic_with_refl path_image_def path_def) -proposition homotopic_loops_sym: - "homotopic_loops s p q \ homotopic_loops s q p" +proposition homotopic_loops_sym: "homotopic_loops s p q \ homotopic_loops s q p" by (simp add: homotopic_loops_def homotopic_with_sym) +proposition homotopic_loops_sym_eq: "homotopic_loops s p q \ homotopic_loops s q p" + by (metis homotopic_loops_sym) + proposition homotopic_loops_trans: "\homotopic_loops s p q; homotopic_loops s q r\ \ homotopic_loops s p r" unfolding homotopic_loops_def by (blast intro: homotopic_with_trans) @@ -3065,7 +3043,7 @@ proof - have "path p" by (metis assms homotopic_loops_imp_path) have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop) - have pip: "path_image p \ s" by (metis assms homotopic_loops_imp_subset1) + have pip: "path_image p \ s" by (metis assms homotopic_loops_imp_subset) obtain h where conth: "continuous_on ({0..1::real} \ {0..1}) h" and hs: "h ` ({0..1} \ {0..1}) \ s" and [simp]: "\x. x \ {0..1} \ h(0,x) = p x" @@ -3105,22 +3083,22 @@ homotopic_paths_trans homotopic_paths_sym homotopic_paths_rinv) have 1: "homotopic_paths s p (p +++ linepath (pathfinish p) (pathfinish p))" using \path p\ homotopic_paths_rid homotopic_paths_sym pip by blast - moreover have "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) + moreover have "homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p))" - apply (subst homotopic_paths_sym) + apply (rule homotopic_paths_sym) using homotopic_paths_lid [of "p +++ linepath (pathfinish p) (pathfinish p)" s] by (metis 1 homotopic_paths_imp_path homotopic_paths_imp_pathstart homotopic_paths_imp_subset) - moreover have "homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p)) + moreover have "homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p +++ linepath (pathfinish p) (pathfinish p)) ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0)))" apply (simp add: homotopic_paths_def homotopic_with_def) apply (rule_tac x="\y. (subpath 0 (fst y) (\u. h (u, 0)) +++ (\u. h (Pair (fst y) u)) +++ subpath (fst y) 0 (\u. h (u, 0))) (snd y)" in exI) apply (simp add: subpath_reversepath) apply (intro conjI homotopic_join_lemma) - using ploop + using ploop apply (simp_all add: path_defs joinpaths_def o_def subpath_def conth c1 c2) apply (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] adhoc_le) done - moreover have "homotopic_paths s ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0))) + moreover have "homotopic_paths s ((\u. h (u, 0)) +++ linepath a a +++ reversepath (\u. h (u, 0))) (linepath (pathstart p) (pathstart p))" apply (rule *) apply (simp add: pih0 pathstart_def pathfinish_def conth0) @@ -3132,7 +3110,7 @@ proposition homotopic_loops_conjugate: fixes s :: "'a::real_normed_vector set" - assumes "path p" "path q" and pip: "path_image p \ s" and piq: "path_image q \ s" + assumes "path p" "path q" and pip: "path_image p \ s" and piq: "path_image q \ s" and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q" shows "homotopic_loops s (p +++ q +++ reversepath p) q" proof - @@ -3151,17 +3129,17 @@ apply (auto simp: algebra_simps add_increasing2 mult_left_le_one_le) done have ps1: "\a b. \b * 2 \ 1; 0 \ b; 0 \ a; a \ 1\ \ p ((1 - a) * (2 * b) + a) \ s" - using sum_le_prod1 + using sum_le_prod1 by (force simp: algebra_simps add_increasing2 mult_left_le intro: pip [unfolded path_image_def, THEN subsetD]) have ps2: "\a b. \\ 4 * b \ 3; b \ 1; 0 \ a; a \ 1\ \ p ((a - 1) * (4 * b - 3) + 1) \ s" apply (rule pip [unfolded path_image_def, THEN subsetD]) apply (rule image_eqI, blast) apply (simp add: algebra_simps) - by (metis add_mono_thms_linordered_semiring(1) affine_ineq linear mult.commute mult.left_neutral mult_right_mono not_le + by (metis add_mono_thms_linordered_semiring(1) affine_ineq linear mult.commute mult.left_neutral mult_right_mono not_le add.commute zero_le_numeral) have qs: "\a b. \4 * b \ 3; \ b * 2 \ 1\ \ q (4 * b - 2) \ s" using path_image_def piq by fastforce - have "homotopic_loops s (p +++ q +++ reversepath p) + have "homotopic_loops s (p +++ q +++ reversepath p) (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q))" apply (simp add: homotopic_loops_def homotopic_with_def) apply (rule_tac x="(\y. (subpath (fst y) 1 p +++ q +++ subpath 1 (fst y) p) (snd y))" in exI) @@ -3178,14 +3156,14 @@ using \path q\ homotopic_paths_lid qloop piq by auto hence 1: "\f. homotopic_paths s f q \ \ homotopic_paths s f (linepath (pathfinish q) (pathfinish q) +++ q)" using homotopic_paths_trans by blast - hence "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q" + hence "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q +++ linepath (pathfinish q) (pathfinish q)) q" proof - have "homotopic_paths s (q +++ linepath (pathfinish q) (pathfinish q)) q" by (simp add: \path q\ homotopic_paths_rid piq) thus ?thesis - by (metis (no_types) 1 \path q\ homotopic_paths_join homotopic_paths_rinv homotopic_paths_sym + by (metis (no_types) 1 \path q\ homotopic_paths_join homotopic_paths_rinv homotopic_paths_sym homotopic_paths_trans qloop pathfinish_linepath piq) - qed + qed thus ?thesis by (metis (no_types) qloop homotopic_loops_sym homotopic_paths_imp_homotopic_loops homotopic_paths_imp_pathfinish homotopic_paths_sym) qed @@ -3193,4 +3171,95 @@ by (blast intro: homotopic_loops_trans) qed + +subsection\ Homotopy of "nearby" function, paths and loops.\ + +lemma homotopic_with_linear: + fixes f g :: "_ \ 'b::real_normed_vector" + assumes contf: "continuous_on s f" + and contg:"continuous_on s g" + and sub: "\x. x \ s \ closed_segment (f x) (g x) \ t" + shows "homotopic_with (\z. True) s t f g" + apply (simp add: homotopic_with_def) + apply (rule_tac x="\y. ((1 - (fst y)) *\<^sub>R f(snd y) + (fst y) *\<^sub>R g(snd y))" in exI) + apply (intro conjI) + apply (rule subset_refl continuous_intros continuous_on_subset [OF contf] continuous_on_compose2 [where g=f] + continuous_on_subset [OF contg] continuous_on_compose2 [where g=g]| simp)+ + using sub closed_segment_def apply fastforce+ + done + +lemma homotopic_paths_linear: + fixes g h :: "real \ 'a::real_normed_vector" + assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g" + "\t x. t \ {0..1} \ closed_segment (g t) (h t) \ s" + shows "homotopic_paths s g h" + using assms + unfolding path_def + apply (simp add: pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def) + apply (rule_tac x="\y. ((1 - (fst y)) *\<^sub>R g(snd y) + (fst y) *\<^sub>R h(snd y))" in exI) + apply (auto intro!: continuous_intros intro: continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h] ) + apply (force simp: closed_segment_def) + apply (simp_all add: algebra_simps) + done + +lemma homotopic_loops_linear: + fixes g h :: "real \ 'a::real_normed_vector" + assumes "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h" + "\t x. t \ {0..1} \ closed_segment (g t) (h t) \ s" + shows "homotopic_loops s g h" + using assms + unfolding path_def + apply (simp add: pathstart_def pathfinish_def homotopic_loops_def homotopic_with_def) + apply (rule_tac x="\y. ((1 - (fst y)) *\<^sub>R g(snd y) + (fst y) *\<^sub>R h(snd y))" in exI) + apply (auto intro!: continuous_intros intro: continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h]) + apply (force simp: closed_segment_def) + done + +lemma homotopic_paths_nearby_explicit: + assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g" + and no: "\t x. \t \ {0..1}; x \ s\ \ norm(h t - g t) < norm(g t - x)" + shows "homotopic_paths s g h" + apply (rule homotopic_paths_linear [OF assms(1-4)]) + by (metis no segment_bound(1) subsetI norm_minus_commute not_le) + +lemma homotopic_loops_nearby_explicit: + assumes "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h" + and no: "\t x. \t \ {0..1}; x \ s\ \ norm(h t - g t) < norm(g t - x)" + shows "homotopic_loops s g h" + apply (rule homotopic_loops_linear [OF assms(1-4)]) + by (metis no segment_bound(1) subsetI norm_minus_commute not_le) + +lemma homotopic_nearby_paths: + fixes g h :: "real \ 'a::euclidean_space" + assumes "path g" "open s" "path_image g \ s" + shows "\e. 0 < e \ + (\h. path h \ + pathstart h = pathstart g \ pathfinish h = pathfinish g \ + (\t \ {0..1}. norm(h t - g t) < e) \ homotopic_paths s g h)" +proof - + obtain e where "e > 0" and e: "\x y. x \ path_image g \ y \ - s \ e \ dist x y" + using separate_compact_closed [of "path_image g" "-s"] assms by force + show ?thesis + apply (intro exI conjI) + using e [unfolded dist_norm] + apply (auto simp: intro!: homotopic_paths_nearby_explicit assms \e > 0\) + by (metis atLeastAtMost_iff imageI le_less_trans not_le path_image_def) +qed + +lemma homotopic_nearby_loops: + fixes g h :: "real \ 'a::euclidean_space" + assumes "path g" "open s" "path_image g \ s" "pathfinish g = pathstart g" + shows "\e. 0 < e \ + (\h. path h \ pathfinish h = pathstart h \ + (\t \ {0..1}. norm(h t - g t) < e) \ homotopic_loops s g h)" +proof - + obtain e where "e > 0" and e: "\x y. x \ path_image g \ y \ - s \ e \ dist x y" + using separate_compact_closed [of "path_image g" "-s"] assms by force + show ?thesis + apply (intro exI conjI) + using e [unfolded dist_norm] + apply (auto simp: intro!: homotopic_loops_nearby_explicit assms \e > 0\) + by (metis atLeastAtMost_iff imageI le_less_trans not_le path_image_def) +qed + end diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 23 16:57:54 2015 +0000 @@ -15,6 +15,20 @@ Norm_Arith begin +lemma image_affinity_interval: + fixes c :: "'a::ordered_real_vector" + shows "((\x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {} + else if 0 <= m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} + else {m *\<^sub>R b + c .. m *\<^sub>R a + c})" + apply (case_tac "m=0", force) + apply (auto simp: scaleR_left_mono) + apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: pos_le_divideR_eq le_diff_eq scaleR_left_mono_neg) + apply (metis diff_le_eq inverse_inverse_eq order.not_eq_order_implies_strict pos_le_divideR_eq positive_imp_inverse_positive) + apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: not_le neg_le_divideR_eq diff_le_eq) + using le_diff_eq scaleR_le_cancel_left_neg + apply fastforce + done + lemma dist_0_norm: fixes x :: "'a::real_normed_vector" shows "dist 0 x = norm x" diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Topological_Spaces.thy Mon Nov 23 16:57:54 2015 +0000 @@ -1484,13 +1484,16 @@ lemma continuous_on_const[continuous_intros]: "continuous_on s (\x. c)" unfolding continuous_on_def by auto +lemma continuous_on_subset: "continuous_on s f \ t \ s \ continuous_on t f" + unfolding continuous_on_def by (metis subset_eq tendsto_within_subset) + lemma continuous_on_compose[continuous_intros]: "continuous_on s f \ continuous_on (f ` s) g \ continuous_on s (g o f)" unfolding continuous_on_topological by simp metis lemma continuous_on_compose2: - "continuous_on t g \ continuous_on s f \ t = f ` s \ continuous_on s (\x. g (f x))" - using continuous_on_compose[of s f g] by (simp add: comp_def) + "continuous_on t g \ continuous_on s f \ f ` s \ t \ continuous_on s (\x. g (f x))" + using continuous_on_compose[of s f g] continuous_on_subset by (force simp add: comp_def) lemma continuous_on_generate_topology: assumes *: "open = generate_topology X" @@ -1601,9 +1604,6 @@ lemma continuous_on_eq_continuous_at: "open s \ continuous_on s f \ (\x\s. isCont f x)" by (simp add: continuous_on_def continuous_at at_within_open[of _ s]) -lemma continuous_on_subset: "continuous_on s f \ t \ s \ continuous_on t f" - unfolding continuous_on_def by (metis subset_eq tendsto_within_subset) - lemma continuous_at_imp_continuous_on: "\x\s. isCont f x \ continuous_on s f" by (auto intro: continuous_at_imp_continuous_at_within simp: continuous_on_eq_continuous_within) diff -r d6b2d638af23 -r c4f6031f1310 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Sun Nov 22 23:19:43 2015 +0100 +++ b/src/HOL/Transcendental.thy Mon Nov 23 16:57:54 2015 +0000 @@ -713,7 +713,7 @@ using K less_trans zero_less_norm_iff by blast then obtain r::real where r: "norm x < norm r" "norm r < K" "r>0" using K False - by (auto simp: abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"]) + by (auto simp: field_simps abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"]) have "(\n. of_nat n * (x / of_real r) ^ n) ----> 0" using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"]) then obtain N where N: "\n. n\N \ real_of_nat n * norm x ^ n < r ^ n" @@ -725,7 +725,7 @@ apply (rule summable_comparison_test' [of "\n. norm(c n * (of_real r) ^ n)" N]) apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]]) using N r norm_of_real [of "r+K", where 'a = 'a] - apply (auto simp add: norm_divide norm_mult norm_power ) + apply (auto simp add: norm_divide norm_mult norm_power field_simps) using less_eq_real_def by fastforce then have "summable (\n. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)" using summable_iff_shift [of "\n. of_nat n * c n * x ^ n" 1] @@ -754,7 +754,7 @@ proof - have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K" using K - apply (auto simp: norm_divide) + apply (auto simp: norm_divide field_simps) apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"]) apply (auto simp: mult_2_right norm_triangle_mono) done @@ -768,7 +768,7 @@ by (blast intro: sm termdiff_converges powser_inside) ultimately show ?thesis apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"]) - apply (auto simp: algebra_simps) + apply (auto simp: field_simps) using K apply (simp_all add: of_real_add [symmetric] del: of_real_add) done @@ -990,11 +990,11 @@ show "summable (\ n. \f n * real (Suc n) * R'^n\)" proof - have "(R' + R) / 2 < R" and "0 < (R' + R) / 2" - using \0 < R'\ \0 < R\ \R' < R\ by auto + using \0 < R'\ \0 < R\ \R' < R\ by (auto simp: field_simps) hence in_Rball: "(R' + R) / 2 \ {-R <..< R}" using \R' < R\ by auto have "norm R' < norm ((R' + R) / 2)" - using \0 < R'\ \0 < R\ \R' < R\ by auto + using \0 < R'\ \0 < R\ \R' < R\ by (auto simp: field_simps) from powser_insidea[OF converges[OF in_Rball] this] show ?thesis by auto qed @@ -1072,7 +1072,7 @@ qed } note for_subinterval = this let ?R = "(R + \x0\) / 2" - have "\x0\ < ?R" using assms by auto + have "\x0\ < ?R" using assms by (auto simp: field_simps) hence "- ?R < x0" proof (cases "x0 < 0") case True @@ -1085,7 +1085,7 @@ finally show ?thesis . qed hence "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R" - using assms by auto + using assms by (auto simp: field_simps) from for_subinterval[OF this] show ?thesis . qed @@ -2342,11 +2342,11 @@ lemma powr_realpow: "0 < x ==> x powr (real n) = x^n" by (induct n) (simp_all add: ac_simps powr_add of_nat_Suc) -lemma powr_realpow_numeral: "0 < x \ x powr (numeral n :: real) = x ^ (numeral n)" +lemma powr_numeral: "0 < x \ x powr (numeral n :: real) = x ^ (numeral n)" by (metis of_nat_numeral powr_realpow) lemma powr2_sqrt[simp]: "0 < x \ sqrt x powr 2 = x" -by(simp add: powr_realpow_numeral) +by(simp add: powr_numeral) lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))" apply (case_tac "x = 0", simp, simp) @@ -2378,10 +2378,6 @@ using powr_realpow [of x 1] by simp -lemma powr_numeral: - fixes x::real shows "0 < x \ x powr numeral n = x ^ numeral n" - by (fact powr_realpow_numeral) - lemma powr_neg_one: fixes x::real shows "0 < x \ x powr - 1 = 1 / x" using powr_int [of x "- 1"] by simp