# HG changeset patch # User paulson # Date 1456746135 0 # Node ID 547c5c6e66d4ecd5bbc1431d9e6093af335b943c # Parent 6dce7bf7960becde9cb44ef3b5c109d26da16f21 the integral is 0 when otherwise it would be undefined (also for contour integrals) diff -r 6dce7bf7960b -r 547c5c6e66d4 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri Feb 26 15:49:35 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Feb 29 11:42:15 2016 +0000 @@ -642,10 +642,14 @@ 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]) + where "contour_integral g f \ @i. (f has_contour_integral i) g \ ~ f contour_integrable_on g \ i=0" + +lemma not_integrable_contour_integral: "~ f contour_integrable_on g \ contour_integral g f = 0" + unfolding contour_integrable_on_def contour_integral_def by blast + +lemma contour_integral_unique: "(f has_contour_integral i) g \ contour_integral g f = i" + apply (simp add: contour_integral_def has_contour_integral_def contour_integrable_on_def) + using has_integral_unique by blast corollary has_contour_integral_eqpath: "\(f has_contour_integral y) p; f contour_integrable_on \; @@ -769,8 +773,16 @@ 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 + assumes "valid_path g" + shows "contour_integral (reversepath g) f = - (contour_integral g f)" +proof (cases "f contour_integrable_on g") + case True then show ?thesis + by (simp add: assms contour_integral_unique has_contour_integral_integral has_contour_integral_reversepath) +next + case False then have "~ f contour_integrable_on (reversepath g)" + by (simp add: assms contour_integrable_reversepath_eq) + with False show ?thesis by (simp add: not_integrable_contour_integral) +qed subsection\Joining two paths together\ @@ -1093,10 +1105,16 @@ 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_integrable_on_shiftpath_eq: + assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" + shows "f contour_integrable_on (shiftpath a g) \ f contour_integrable_on g" +using assms contour_integrable_on_def has_contour_integral_shiftpath_eq by auto + lemma contour_integral_shiftpath: assumes "valid_path g" "pathfinish g = pathstart g" "a \ {0..1}" shows "contour_integral (shiftpath a g) f = contour_integral g f" - using assms by (simp add: contour_integral_def has_contour_integral_shiftpath_eq) + using assms + by (simp add: contour_integral_def contour_integrable_on_def has_contour_integral_shiftpath_eq) subsection\More about straight-line paths\ @@ -1325,8 +1343,8 @@ qed 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) + "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 contour_integrable_on) subsection\Segments via convex hulls\ @@ -1577,7 +1595,9 @@ 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) + apply (simp add: contour_integral_def) + using has_contour_integral_eq + by (metis contour_integral_unique has_contour_integral_integrable has_contour_integral_integral) lemma contour_integral_eq_0: "(\z. z \ path_image g \ f z = 0) \ contour_integral g f = 0" @@ -1877,16 +1897,16 @@ done also have "... = integral {0..1} (\y. contour_integral g (\x. f x (h y) * vector_derivative h (at y)))" - apply (simp add: contour_integral_integral) + apply (simp only: 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) + apply (rule fgh gvcon' hvcon' continuous_intros | simp add: split_def)+ + unfolding integral_mult_left [symmetric] + apply (simp only: mult_ac) done 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) + unfolding integral_mult_left [symmetric] apply (simp add: algebra_simps) done finally show ?thesis diff -r 6dce7bf7960b -r 547c5c6e66d4 src/HOL/Multivariate_Analysis/Conformal_Mappings.thy --- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Fri Feb 26 15:49:35 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Mon Feb 29 11:42:15 2016 +0000 @@ -1521,10 +1521,7 @@ then have 2: "contour_integral (linepath b c) f = contour_integral (linepath b a') f + contour_integral (linepath a' c) f" by (rule contour_integral_split_linepath [OF _ a']) - have "f contour_integrable_on linepath b' a'" - by (meson a'b' contf continuous_on_subset contour_integrable_continuous_linepath - convex_contains_segment \convex S\) - then have 3: "contour_integral (reversepath (linepath b' a')) f = + have 3: "contour_integral (reversepath (linepath b' a')) f = - contour_integral (linepath b' a') f" by (rule contour_integral_reversepath [OF valid_path_linepath]) have fcd_le: "f complex_differentiable at x" diff -r 6dce7bf7960b -r 547c5c6e66d4 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Feb 26 15:49:35 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Feb 29 11:42:15 2016 +0000 @@ -1806,10 +1806,13 @@ definition integrable_on (infixr "integrable'_on" 46) where "f integrable_on i \ (\y. (f has_integral y) i)" -definition "integral i f = (SOME y. (f has_integral y) i)" +definition "integral i f = (SOME y. (f has_integral y) i \ ~ f integrable_on i \ y=0)" lemma integrable_integral[dest]: "f integrable_on i \ (f has_integral (integral i f)) i" - unfolding integrable_on_def integral_def by (rule someI_ex) + unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex) + +lemma not_integrable_integral: "~ f integrable_on i \ integral i f = 0" + unfolding integrable_on_def integral_def by blast lemma has_integral_integrable[intro]: "(f has_integral i) s \ f integrable_on s" unfolding integrable_on_def by auto @@ -2328,6 +2331,12 @@ unfolding integral_def by (rule some_equality) (auto intro: has_integral_unique) +lemma eq_integralD: "integral k f = y \ (f has_integral y) k \ ~ f integrable_on k \ y=0" + unfolding integral_def integrable_on_def + apply (erule subst) + apply (rule someI_ex) + by blast + lemma has_integral_is_0: fixes f :: "'n::euclidean_space \ 'a::real_normed_vector" assumes "\x\s. f x = 0" @@ -2468,14 +2477,29 @@ using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def) lemma has_integral_mult_left: - fixes c :: "_ :: {real_normed_algebra}" + fixes c :: "_ :: real_normed_algebra" shows "(f has_integral y) s \ ((\x. f x * c) has_integral (y * c)) s" using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def) -corollary integral_mult_left: - fixes c:: "'a::real_normed_algebra" - shows "f integrable_on s \ integral s (\x. f x * c) = integral s f * c" - by (blast intro: has_integral_mult_left) +text\The case analysis eliminates the condition @{term "f integrable_on s"} at the cost + of the type class constraint @{text"division_ring"}\ +corollary integral_mult_left [simp]: + fixes c:: "'a::{real_normed_algebra,division_ring}" + shows "integral s (\x. f x * c) = integral s f * c" +proof (cases "f integrable_on s \ c = 0") + case True then show ?thesis + by (force intro: has_integral_mult_left) +next + case False then have "~ (\x. f x * c) integrable_on s" + using has_integral_mult_left [of "(\x. f x * c)" _ s "inverse c"] + by (force simp add: mult.assoc) + with False show ?thesis by (simp add: not_integrable_integral) +qed + +corollary integral_mult_right [simp]: + fixes c:: "'a::{real_normed_field}" + shows "integral s (\x. c * f x) = c * integral s f" +by (simp add: mult.commute [of c]) lemma has_integral_mult_right: fixes c :: "'a :: real_normed_algebra" @@ -2499,7 +2523,7 @@ unfolding real_scaleR_def . qed -lemma has_integral_neg: "(f has_integral k) s \ ((\x. -(f x)) has_integral (-k)) s" +lemma has_integral_neg: "(f has_integral k) s \ ((\x. -(f x)) has_integral -k) s" by (drule_tac c="-1" in has_integral_cmul) auto lemma has_integral_add: @@ -2608,7 +2632,7 @@ unfolding algebra_simps by auto -lemma integral_0: +lemma integral_0 [simp]: "integral s (\x::'n::euclidean_space. 0::'m::real_normed_vector) = 0" by (rule integral_unique has_integral_0)+ @@ -2616,11 +2640,26 @@ integral s (\x. f x + g x) = integral s f + integral s g" by (rule integral_unique) (metis integrable_integral has_integral_add) -lemma integral_cmul: "f integrable_on s \ integral s (\x. c *\<^sub>R f x) = c *\<^sub>R integral s f" - by (rule integral_unique) (metis integrable_integral has_integral_cmul) - -lemma integral_neg: "f integrable_on s \ integral s (\x. - f x) = - integral s f" - by (rule integral_unique) (metis integrable_integral has_integral_neg) +lemma integral_cmul [simp]: "integral s (\x. c *\<^sub>R f x) = c *\<^sub>R integral s f" +proof (cases "f integrable_on s \ c = 0") + case True with has_integral_cmul show ?thesis by force +next + case False then have "~ (\x. c *\<^sub>R f x) integrable_on s" + using has_integral_cmul [of "(\x. c *\<^sub>R f x)" _ s "inverse c"] + by force + with False show ?thesis by (simp add: not_integrable_integral) +qed + +lemma integral_neg [simp]: "integral s (\x. - f x) = - integral s f" +proof (cases "f integrable_on s") + case True then show ?thesis + by (simp add: has_integral_neg integrable_integral integral_unique) +next + case False then have "~ (\x. - f x) integrable_on s" + using has_integral_neg [of "(\x. - f x)" _ s ] + by force + with False show ?thesis by (simp add: not_integrable_integral) +qed lemma integral_diff: "f integrable_on s \ g integrable_on s \ integral s (\x. f x - g x) = integral s f - integral s g" @@ -2715,7 +2754,7 @@ assumes "\x. x \ s \ f x = g x" shows "integral s f = integral s g" unfolding integral_def - by (metis assms has_integral_cong) +by (metis (full_types, hide_lams) assms has_integral_cong integrable_eq) lemma has_integral_null [intro]: assumes "content(cbox a b) = 0" @@ -4427,12 +4466,17 @@ lemma integral_component_nonneg: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes "k \ Basis" - and "f integrable_on s" "\x\s. 0 \ (f x)\k" + and "\x\s. 0 \ (f x)\k" shows "0 \ (integral s f)\k" - apply (rule has_integral_component_nonneg) - using assms - apply auto - done +proof (cases "f integrable_on s") + case True show ?thesis + apply (rule has_integral_component_nonneg) + using assms True + apply auto + done +next + case False then show ?thesis by (simp add: not_integrable_integral) +qed lemma has_integral_component_neg: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" @@ -5345,9 +5389,7 @@ assumes "negligible s" and "\x\(t - s). g x = f x" shows "integral t f = integral t g" - unfolding integral_def - using has_integral_spike_eq[OF assms] - by auto + using has_integral_spike_eq[OF assms] by (simp add: integral_def integrable_on_def) subsection \Some other trivialities about negligible sets.\ @@ -8146,10 +8188,7 @@ using p by auto have **: "g integrable_on cbox c d" apply (rule integrable_spike_interior[where f=f]) - unfolding g_def - defer - apply (rule has_integral_integrable) - using assms(1) + unfolding g_def using assms(1) apply auto done moreover @@ -9426,12 +9465,7 @@ note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]] from this(2)[OF as(4,1)] guess u v by (elim exE) note uv=this have *: "interior (k \ l) = {}" - unfolding interior_Int - apply (rule q') - using as - unfolding r_def - apply auto - done + by (metis DiffE \T1 = qq k\ \T1 \ T2\ \T2 = qq l\ as(4) as(5) interior_Int q'(5) r_def) have "interior m = {}" unfolding subset_empty[symmetric] unfolding *[symmetric] @@ -10234,7 +10268,6 @@ apply (rule_tac x="integral s (f k)" in bexI) prefer 3 apply (rule_tac x=k in exI) - unfolding integral_neg[OF assm(1)] apply auto done have "(\x. - g x) integrable_on s \ @@ -10254,14 +10287,8 @@ done note * = conjunctD2[OF this] show ?thesis - apply rule - using integrable_neg[OF *(1)] - defer - using tendsto_minus[OF *(2)] - unfolding integral_neg[OF assm(1)] - unfolding integral_neg[OF *(1),symmetric] - apply auto - done + using integrable_neg[OF *(1)] tendsto_minus[OF *(2)] + by auto qed @@ -11402,11 +11429,9 @@ unfolding inner_minus_left[symmetric] defer apply (subst integral_neg[symmetric]) - defer apply (rule_tac[1-2] integral_component_le[OF i]) - apply (rule integrable_neg) using integrable_on_subcbox[OF assms(1),of a b] - integrable_on_subcbox[OF assms(2),of a b] i + integrable_on_subcbox[OF assms(2),of a b] i integrable_neg unfolding ab apply auto done