# HG changeset patch # User paulson # Date 1502487513 -7200 # Node ID 5198edd9facc81146405f5c41eccaa58f27370e0 # Parent b4b3e9918d62f8116d27e0fb3f491171125e1ab9 more Henstock_Kurzweil_Integration cleanup diff -r b4b3e9918d62 -r 5198edd9facc src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Aug 10 23:08:55 2017 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 11 23:38:33 2017 +0200 @@ -72,7 +72,7 @@ lemma content_real: "a \ b \ content {a..b} = b - a" by simp -lemma abs_eq_content: "\y - x\ = (if x\y then content {x .. y} else content {y..x})" +lemma abs_eq_content: "\y - x\ = (if x\y then content {x..y} else content {y..x})" by (auto simp: content_real) lemma content_singleton: "content {a} = 0" @@ -223,7 +223,7 @@ finally show ?thesis . qed -lemma content_real_eq_0: "content {a .. b::real} = 0 \ a \ b" +lemma content_real_eq_0: "content {a..b::real} = 0 \ a \ b" by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0) lemma property_empty_interval: "\a b. content (cbox a b) = 0 \ P (cbox a b) \ P {}" @@ -261,9 +261,9 @@ by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff) lemma has_integral_real: - "(f has_integral y) {a .. b::real} \ + "(f has_integral y) {a..b::real} \ (\e>0. \d. gauge d \ - (\p. p tagged_division_of {a .. b} \ d fine p \ + (\p. p tagged_division_of {a..b} \ d fine p \ norm (sum (\(x,k). content(k) *\<^sub>R f x) p - y) < e))" unfolding box_real[symmetric] by (rule has_integral) @@ -394,7 +394,7 @@ lemma has_integral_const_real [intro]: fixes a b :: real - shows "((\x. c) has_integral (content {a .. b} *\<^sub>R c)) {a .. b}" + shows "((\x. c) has_integral (content {a..b} *\<^sub>R c)) {a..b}" by (metis box_real(2) has_integral_const) lemma has_integral_integrable_integral: "(f has_integral i) s \ f integrable_on s \ integral s f = i" @@ -407,7 +407,7 @@ lemma integral_const_real [simp]: fixes a b :: real - shows "integral {a .. b} (\x. c) = content {a .. b} *\<^sub>R c" + shows "integral {a..b} (\x. c) = content {a..b} *\<^sub>R c" by (metis box_real(2) integral_const) lemma has_integral_is_0: @@ -793,7 +793,7 @@ using eventually_division_filter_tagged_division[of "cbox a b"] by (subst tendsto_cong[where g="\_. 0"]) (auto elim: eventually_mono intro: sum_content_null) -lemma has_integral_null_real [intro]: "content {a .. b::real} = 0 \ (f has_integral 0) {a .. b}" +lemma has_integral_null_real [intro]: "content {a..b::real} = 0 \ (f has_integral 0) {a..b}" by (metis box_real(2) has_integral_null) lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \ (f has_integral i) (cbox a b) \ i = 0" @@ -1561,9 +1561,9 @@ corollary has_integral_bound_real: fixes f :: "real \ 'b::real_normed_vector" assumes "0 \ B" - and "(f has_integral i) {a .. b}" - and "\x\{a .. b}. norm (f x) \ B" - shows "norm i \ B * content {a .. b}" + and "(f has_integral i) {a..b}" + and "\x\{a..b}. norm (f x) \ B" + shows "norm i \ B * content {a..b}" by (metis assms box_real(2) has_integral_bound) corollary integrable_bound: @@ -1749,10 +1749,10 @@ done lemma integral_component_lbound_real: - assumes "f integrable_on {a ::real .. b}" - and "\x\{a .. b}. B \ f(x)\k" + assumes "f integrable_on {a ::real..b}" + and "\x\{a..b}. B \ f(x)\k" and "k \ Basis" - shows "B * content {a .. b} \ (integral {a .. b} f)\k" + shows "B * content {a..b} \ (integral {a..b} f)\k" using assms by (metis box_real(2) integral_component_lbound) @@ -1770,10 +1770,10 @@ lemma integral_component_ubound_real: fixes f :: "real \ 'a::euclidean_space" - assumes "f integrable_on {a .. b}" - and "\x\{a .. b}. f x\k \ B" + assumes "f integrable_on {a..b}" + and "\x\{a..b}. f x\k \ B" and "k \ Basis" - shows "(integral {a .. b} f)\k \ B * content {a .. b}" + shows "(integral {a..b} f)\k \ B * content {a..b}" using assms by (metis box_real(2) integral_component_ubound) @@ -2578,8 +2578,8 @@ lemma integrable_continuous_interval: fixes f :: "'b::ordered_euclidean_space \ 'a::banach" - assumes "continuous_on {a .. b} f" - shows "f integrable_on {a .. b}" + assumes "continuous_on {a..b} f" + shows "f integrable_on {a..b}" by (metis assms integrable_continuous interval_cbox) lemmas integrable_continuous_real = integrable_continuous_interval[where 'b=real] @@ -2647,9 +2647,9 @@ qed lemma has_integral_factor_content_real: - "(f has_integral i) {a .. b::real} \ - (\e>0. \d. gauge d \ (\p. p tagged_division_of {a .. b} \ d fine p \ - norm (sum (\(x,k). content k *\<^sub>R f x) p - i) \ e * content {a .. b} ))" + "(f has_integral i) {a..b::real} \ + (\e>0. \d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ + norm (sum (\(x,k). content k *\<^sub>R f x) p - i) \ e * content {a..b} ))" unfolding box_real[symmetric] by (rule has_integral_factor_content) @@ -2666,8 +2666,8 @@ lemma fundamental_theorem_of_calculus: fixes f :: "real \ 'a::banach" assumes "a \ b" - and vecd: "\x\{a .. b}. (f has_vector_derivative f' x) (at x within {a .. b})" - shows "(f' has_integral (f b - f a)) {a .. b}" + and vecd: "\x\{a..b}. (f has_vector_derivative f' x) (at x within {a..b})" + shows "(f' has_integral (f b - f a)) {a..b}" unfolding has_integral_factor_content box_real[symmetric] proof safe fix e :: real @@ -2770,15 +2770,15 @@ assumes "p>0" and f0: "Df 0 = f" and Df: "\m t. m < p \ a \ t \ t \ b \ - (Df m has_vector_derivative Df (Suc m) t) (at t within {a .. b})" + (Df m has_vector_derivative Df (Suc m) t) (at t within {a..b})" and g0: "Dg 0 = g" and Dg: "\m t. m < p \ a \ t \ t \ b \ - (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a .. b})" + (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a..b})" and ivl: "a \ t" "t \ b" shows "((\t. \iR prod (Df i t) (Dg (p - Suc i) t)) has_vector_derivative prod (f t) (Dg p t) - (-1)^p *\<^sub>R prod (Df p t) (g t)) - (at t within {a .. b})" + (at t within {a..b})" using assms proof cases assume p: "p \ 1" @@ -2809,7 +2809,7 @@ assumes "p>0" and f0: "Df 0 = f" and Df: "\m t. m < p \ a \ t \ t \ b \ - (Df m has_vector_derivative Df (Suc m) t) (at t within {a .. b})" + (Df m has_vector_derivative Df (Suc m) t) (at t within {a..b})" and ivl: "a \ b" defines "i \ \x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x" shows taylor_has_integral: @@ -2817,7 +2817,7 @@ and taylor_integral: "f b = (\iR Df i a) + integral {a..b} i" and taylor_integrable: - "i integrable_on {a .. b}" + "i integrable_on {a..b}" proof goal_cases case 1 interpret bounded_bilinear "scaleR::real\'a\'a" @@ -2837,7 +2837,7 @@ by auto } note fact_eq = this have Dg: "\m t. m < p \ a \ t \ t \ b \ - (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a .. b})" + (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a..b})" unfolding Dg_def by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def fact_eq divide_simps) let ?sum = "\t. \iR Dg i t *\<^sub>R Df (p - Suc i) t" @@ -2848,7 +2848,7 @@ g t *\<^sub>R Df p t - (- 1) ^ p *\<^sub>R Dg p t *\<^sub>R f t) (at t within {a..b})" by auto from fundamental_theorem_of_calculus[rule_format, OF \a \ b\ deriv] - have "(i has_integral ?sum b - ?sum a) {a .. b}" + have "(i has_integral ?sum b - ?sum a) {a..b}" using atLeastatMost_empty'[simp del] by (simp add: i_def g_def Dg_def) also @@ -3038,9 +3038,9 @@ lemma integrable_subinterval_real: fixes f :: "real \ 'a::banach" - assumes "f integrable_on {a .. b}" - and "{c .. d} \ {a .. b}" - shows "f integrable_on {c .. d}" + assumes "f integrable_on {a..b}" + and "{c..d} \ {a..b}" + shows "f integrable_on {c..d}" by (metis assms(1) assms(2) box_real(2) integrable_subinterval) @@ -3050,9 +3050,9 @@ fixes a b c :: real assumes "a \ c" and "c \ b" - and "(f has_integral i) {a .. c}" - and "(f has_integral (j::'a::banach)) {c .. b}" - shows "(f has_integral (i + j)) {a .. b}" + and "(f has_integral i) {a..c}" + and "(f has_integral (j::'a::banach)) {c..b}" + shows "(f has_integral (i + j)) {a..b}" proof - interpret comm_monoid "lift_option plus" "Some (0::'a)" by (rule comm_monoid_lift_option) @@ -3087,8 +3087,8 @@ fixes f :: "real \ 'a::banach" assumes "a \ c" and "c \ b" - and "f integrable_on {a .. b}" - shows "integral {a .. c} f + integral {c .. b} f = integral {a .. b} f" + and "f integrable_on {a..b}" + shows "integral {a..c} f + integral {c..b} f = integral {a..b} f" apply (rule integral_unique[symmetric]) apply (rule has_integral_combine[OF assms(1-2)]) apply (metis assms(2) assms(3) atLeastatMost_subset_iff box_real(2) content_pos_le content_real_eq_0 integrable_integral integrable_subinterval le_add_same_cancel2 monoid_add_class.add.left_neutral) @@ -3098,9 +3098,9 @@ fixes f :: "real \ 'a::banach" assumes "a \ c" and "c \ b" - and "f integrable_on {a .. c}" - and "f integrable_on {c .. b}" - shows "f integrable_on {a .. b}" + and "f integrable_on {a..c}" + and "f integrable_on {c..b}" + shows "f integrable_on {a..b}" using assms unfolding integrable_on_def by (auto intro!:has_integral_combine) @@ -3201,9 +3201,9 @@ lemma integral_has_vector_derivative: fixes f :: "real \ 'a::banach" - assumes "continuous_on {a .. b} f" - and "x \ {a .. b}" - shows "((\u. integral {a .. u} f) has_vector_derivative f(x)) (at x within {a .. b})" + assumes "continuous_on {a..b} f" + and "x \ {a..b}" + shows "((\u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})" apply (rule integral_has_vector_derivative_continuous_at [OF integrable_continuous_real]) using assms apply (auto simp: continuous_on_eq_continuous_within) @@ -3211,8 +3211,8 @@ lemma antiderivative_continuous: fixes q b :: real - assumes "continuous_on {a .. b} f" - obtains g where "\x\{a .. b}. (g has_vector_derivative (f x::_::banach)) (at x within {a .. b})" + assumes "continuous_on {a..b} f" + obtains g where "\x\{a..b}. (g has_vector_derivative (f x::_::banach)) (at x within {a..b})" apply (rule that) apply rule using integral_has_vector_derivative[OF assms] @@ -3224,8 +3224,8 @@ lemma antiderivative_integral_continuous: fixes f :: "real \ 'a::banach" - assumes "continuous_on {a .. b} f" - obtains g where "\u\{a .. b}. \v \ {a .. b}. u \ v \ (f has_integral (g v - g u)) {u .. v}" + assumes "continuous_on {a..b} f" + obtains g where "\u\{a..b}. \v \ {a..b}. u \ v \ (f has_integral (g v - g u)) {u..v}" proof - obtain g where g: "\x. x \ {a..b} \ (g has_vector_derivative f x) (at x within {a..b})" @@ -3556,7 +3556,7 @@ by auto lemma has_integral_reflect_lemma_real[intro]: - assumes "(f has_integral i) {a .. b::real}" + assumes "(f has_integral i) {a..b::real}" shows "((\x. f(-x)) has_integral i) {-b .. -a}" using assms unfolding box_real[symmetric] @@ -3572,14 +3572,14 @@ lemma integrable_reflect[simp]: "(\x. f(-x)) integrable_on cbox (-b) (-a) \ f integrable_on cbox a b" unfolding integrable_on_def by auto -lemma integrable_reflect_real[simp]: "(\x. f(-x)) integrable_on {-b .. -a} \ f integrable_on {a .. b::real}" +lemma integrable_reflect_real[simp]: "(\x. f(-x)) integrable_on {-b .. -a} \ f integrable_on {a..b::real}" unfolding box_real[symmetric] by (rule integrable_reflect) lemma integral_reflect[simp]: "integral (cbox (-b) (-a)) (\x. f (-x)) = integral (cbox a b) f" unfolding integral_def by auto -lemma integral_reflect_real[simp]: "integral {-b .. -a} (\x. f (-x)) = integral {a .. b::real} f" +lemma integral_reflect_real[simp]: "integral {-b .. -a} (\x. f (-x)) = integral {a..b::real} f" unfolding box_real[symmetric] by (rule integral_reflect) @@ -3592,9 +3592,9 @@ theorem fundamental_theorem_of_calculus_interior: fixes f :: "real \ 'a::real_normed_vector" assumes "a \ b" - and contf: "continuous_on {a .. b} f" + and contf: "continuous_on {a..b} f" and derf: "\x. x \ {a <..< b} \ (f has_vector_derivative f'(x)) (at x)" - shows "(f' has_integral (f b - f a)) {a .. b}" + shows "(f' has_integral (f b - f a)) {a..b}" proof (cases "a = b") case True then have *: "cbox a b = {b}" "f b - f a = 0" @@ -3603,18 +3603,18 @@ next case False with \a \ b\ have ab: "a < b" by arith - let ?P = "\e. \d. gauge d \ (\p. p tagged_division_of {a .. b} \ d fine p \ - norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content {a .. b})" + let ?P = "\e. \d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ + norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content {a..b})" { presume "\e. e > 0 \ ?P e" then show ?thesis unfolding has_integral_factor_content_real by force } fix e :: real assume e: "e > 0" then have eba8: "(e * (b - a)) / 8 > 0" - using ab by (auto simp add: field_simps) + using ab by (auto simp add: field_simps) note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt] have bounded: "\x. x \ {a<.. bounded_linear (\u. u *\<^sub>R f' x)" using derf_exp by simp have "\x \ box a b. \d>0. \y. norm (y-x) < d \ norm (f y - f x - (y-x) *\<^sub>R f' x) \ e/2 * norm (y-x)" - (is "\x \ box a b. ?Q x") + (is "\x \ box a b. ?Q x") proof fix x assume x: "x \ box a b" show "?Q x" @@ -3623,7 +3623,7 @@ qed from this [unfolded bgauge_existence_lemma] obtain d where d: "\x. 0 < d x" - "\x y. \x \ box a b; norm (y-x) < d x\ + "\x y. \x \ box a b; norm (y-x) < d x\ \ norm (f y - f x - (y-x) *\<^sub>R f' x) \ e / 2 * norm (y-x)" by metis have "bounded (f ` cbox a b)" @@ -3633,19 +3633,18 @@ where "0 < B" and B: "\x. x \ f ` cbox a b \ norm x \ B" unfolding bounded_pos by metis obtain da where "0 < da" - and da: "\c. \a \ c; {a .. c} \ {a .. b}; {a .. c} \ ball a da\ - \ norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \ (e * (b - a)) / 4" + and da: "\c. \a \ c; {a..c} \ {a..b}; {a..c} \ ball a da\ + \ norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \ (e * (b - a)) / 4" proof - have "continuous (at a within {a..b}) f" using contf continuous_on_eq_continuous_within by force with eba8 obtain k where "0 < k" - and k: "\x. \x \ {a..b}; 0 < norm (x-a); norm (x-a) < k\ + and k: "\x. \x \ {a..b}; 0 < norm (x-a); norm (x-a) < k\ \ norm (f x - f a) < e * (b - a) / 8" unfolding continuous_within Lim_within dist_norm by metis obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \ e * (b - a) / 8" proof (cases "f' a = 0") - case True - thus ?thesis using ab e that by auto + case True with ab e that show ?thesis by auto next case False then show ?thesis @@ -3653,8 +3652,8 @@ using ab e apply (auto simp add: field_simps) done qed - have "norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \ e * (b - a) / 4" - if "a \ c" "{a .. c} \ {a .. b}" and bmin: "{a .. c} \ ball a (min k l)" for c + have "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \ e * (b - a) / 4" + if "a \ c" "{a..c} \ {a..b}" and bmin: "{a..c} \ ball a (min k l)" for c proof - have minkl: "\a - x\ < min k l" if "x \ {a..c}" for x using bmin dist_real_def that by auto @@ -3680,16 +3679,15 @@ qed then show "norm (f c - f a) \ e * (b - a) / 8" by simp qed - finally show "norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \ e * (b - a) / 4" + finally show "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \ e * (b - a) / 4" unfolding content_real[OF \a \ c\] by auto qed then show ?thesis by (rule_tac da="min k l" in that) (auto simp: l \0 < k\) qed - obtain db where "0 < db" - and db: "\c. \c \ b; {c .. b} \ {a .. b}; {c .. b} \ ball b db\ - \ norm (content {c .. b} *\<^sub>R f' b - (f b - f c)) \ (e * (b - a)) / 4" + and db: "\c. \c \ b; {c..b} \ {a..b}; {c..b} \ ball b db\ + \ norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \ (e * (b - a)) / 4" proof - have "continuous (at b within {a..b}) f" using contf continuous_on_eq_continuous_within by force @@ -3726,22 +3724,20 @@ next have "norm (f b - f c) < e * (b - a) / 8" proof (cases "b = c") - case True - then show ?thesis - using eba8 by auto + case True with eba8 show ?thesis + by auto next case False show ?thesis by (rule k) (use minkl \c \ b\ that False in auto) qed then show "norm (f b - f c) \ e * (b - a) / 8" by simp qed - finally show "norm (content {c .. b} *\<^sub>R f' b - (f b - f c)) \ e * (b - a) / 4" + finally show "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \ e * (b - a) / 4" unfolding content_real[OF \c \ b\] by auto qed then show ?thesis by (rule_tac db="min k l" in that) (auto simp: l \0 < k\) qed - let ?d = "(\x. ball x (if x=a then da else if x=b then db else d x))" show "?P e" proof (intro exI conjI allI impI) @@ -3757,9 +3753,8 @@ note * = additive_tagged_division_1[OF assms(1) ptag, symmetric] have **: "\n1 s1 n2 s2::real. n2 \ s2 / 2 \ n1 - s1 \ s2 / 2 \ n1 + n2 \ s1 + s2" by arith - have XX: False if xk: "(x,K) \ p" + have non: False if xk: "(x,K) \ p" and "x \ a" "x \ b" and less: "e * (Sup K - Inf K) / 2 < norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))" - and "x \ a" "x \ b" for x K proof - obtain u v where k: "K = cbox u v" @@ -3793,12 +3788,12 @@ \ (\(x, K)\p - ?A. norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))" by (auto intro: sum_norm_le) also have "... \ (\n\p - ?A. e * (case n of (x, k) \ Sup k - Inf k) / 2)" - using XX by (force intro: sum_mono) - finally have 1: "norm (\(x, k)\p - ?A. + using non by (force intro: sum_mono) + finally have I: "norm (\(x, k)\p - ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \ (\n\p - ?A. e * (case n of (x, k) \ Sup k - Inf k)) / 2" by (simp add: sum_divide_distrib) - have 2: "norm (\(x, k)\p \ ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) - + have II: "norm (\(x, k)\p \ ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) - (\n\p \ ?A. e * (case n of (x, k) \ Sup k - Inf k)) \ (\n\p - ?A. e * (case n of (x, k) \ Sup k - Inf k)) / 2" proof - @@ -3817,7 +3812,6 @@ proof - have *: "\s f e. sum f s = sum f (p \ ?C) \ norm (sum f (p \ ?C)) \ e \ norm (sum f s) \ e" by auto - have 1: "content K *\<^sub>R (f' (x)) - (f ((Sup K)) - f ((Inf K))) = 0" if "(x,K) \ p \ {t. fst t \ {a, b}} - p \ ?C" for x K proof - @@ -3967,7 +3961,7 @@ qed show "norm (\(x, k)\p \ ?A. content k *\<^sub>R f' x - (f ((Sup k)) - f ((Inf k)))) \ e * (b - a) / 2" apply (rule * [OF sum.mono_neutral_right[OF pA(2)]]) - using 1 2 by (auto simp: split_paired_all) + using 1 2 by (auto simp: split_paired_all) qed also have "... = (\n\p. e * (case n of (x, k) \ Sup k - Inf k)) / 2" unfolding sum_distrib_left[symmetric] @@ -3983,13 +3977,14 @@ unfolding sum.union_disjoint[OF pA(2-), symmetric] pA(1)[symmetric] by (metis norm_le) qed - show "norm ((\(x, k)\p. content k *\<^sub>R f' x) - (f b - f a)) \ e * content {a..b}" - unfolding content_real[OF assms(1)] and *[of "\x. x"] *[of f] sum_subtractf[symmetric] split_minus + have "norm (\(x,K)\p \ ?A \ (p - ?A). content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) + \ e * (\(x,K)\p \ ?A \ (p - ?A). Sup K - Inf K)" unfolding sum_distrib_left - apply (subst(2) pA) - apply (subst pA) unfolding sum.union_disjoint[OF pA(2-)] - using ** norm_triangle_le 1 2 by blast + using ** norm_triangle_le I II by blast + then + show "norm ((\(x,K)\p. content K *\<^sub>R f' x) - (f b - f a)) \ e * content {a..b}" + by (simp only: content_real[OF \a \ b\] *[of "\x. x"] *[of f] sum_subtractf[symmetric] split_minus pA(1) [symmetric]) qed qed @@ -4000,144 +3995,95 @@ fixes f :: "real \ 'a::banach" assumes "finite s" and "a \ b" - and "continuous_on {a .. b} f" + and "continuous_on {a..b} f" and "\x\{a <..< b} - s. (f has_vector_derivative f'(x)) (at x)" - shows "(f' has_integral (f b - f a)) {a .. b}" + shows "(f' has_integral (f b - f a)) {a..b}" using assms proof (induct "card s" arbitrary: s a b) case 0 - show ?case - apply (rule fundamental_theorem_of_calculus_interior) - using 0 - apply auto - done + then show ?case + by (force simp add: intro: fundamental_theorem_of_calculus_interior) next case (Suc n) - from this(2) guess c s' - apply - - apply (subst(asm) eq_commute) - unfolding card_Suc_eq - apply (subst(asm)(2) eq_commute) - apply (elim exE conjE) - done - note cs = this[rule_format] + then obtain c s' where cs: "s = insert c s'" and n: "n = card s'" + by (metis card_eq_SucD) + then have "finite s'" + using \finite s\ by force show ?case proof (cases "c \ box a b") case False - then show ?thesis - apply - - apply (rule Suc(1)[OF cs(3) _ Suc(4,5)]) - apply safe - defer - apply (rule Suc(6)[rule_format]) - using Suc(3) - unfolding cs - apply auto - done + with \finite s'\ show ?thesis + using cs n Suc + by (metis Diff_iff box_real(1) insert_iff) next - have *: "f b - f a = (f c - f a) + (f b - f c)" - by auto + let ?P = "\i j. \x\{i <..< j} - s'. (f has_vector_derivative f' x) (at x)" case True then have "a \ c" "c \ b" by (auto simp: mem_box) - then show ?thesis - apply (subst *) - apply (rule has_integral_combine) - apply assumption+ - apply (rule_tac[!] Suc(1)[OF cs(3)]) - using Suc(3) - unfolding cs - proof - - show "continuous_on {a .. c} f" "continuous_on {c .. b} f" - apply (rule_tac[!] continuous_on_subset[OF Suc(5)]) - using True - apply (auto simp: mem_box) - done - let ?P = "\i j. \x\{i <..< j} - s'. (f has_vector_derivative f' x) (at x)" - show "?P a c" "?P c b" - apply safe - apply (rule_tac[!] Suc(6)[rule_format]) - using True - unfolding cs - apply (auto simp: mem_box) - done - qed auto + moreover have "?P a c" "?P c b" + using Suc.prems(4) True \a \ c\ cs(1) by auto + moreover have "continuous_on {a..c} f" "continuous_on {c..b} f" + using \continuous_on {a..b} f\ \a \ c\ \c \ b\ continuous_on_subset by fastforce+ + ultimately have "(f' has_integral f c - f a + (f b - f c)) {a..b}" + using Suc.hyps(1) \finite s'\ \n = card s'\ by (blast intro: has_integral_combine) + then show ?thesis + by auto qed qed -lemma fundamental_theorem_of_calculus_strong: +corollary fundamental_theorem_of_calculus_strong: fixes f :: "real \ 'a::banach" assumes "finite s" and "a \ b" - and "continuous_on {a .. b} f" - and "\x\{a .. b} - s. (f has_vector_derivative f'(x)) (at x)" - shows "(f' has_integral (f b - f a)) {a .. b}" + and "continuous_on {a..b} f" + and vec: "\x\{a..b} - s. (f has_vector_derivative f'(x)) (at x)" + shows "(f' has_integral (f b - f a)) {a..b}" apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f']) - using assms(4) - apply (auto simp: mem_box) + using vec apply (auto simp: mem_box) done lemma indefinite_integral_continuous_left: fixes f:: "real \ 'a::banach" - assumes "f integrable_on {a .. b}" + assumes intf: "f integrable_on {a..b}" and "a < c" and "c \ b" and "e > 0" obtains d where "d > 0" - and "\t. c - d < t \ t \ c \ norm (integral {a .. c} f - integral {a .. t} f) < e" + and "\t. c - d < t \ t \ c \ norm (integral {a..c} f - integral {a..t} f) < e" proof - - have "\w>0. \t. c - w < t \ t < c \ norm (f c) * norm(c - t) < e / 3" + obtain w where "w > 0" and w: "\t. \c - w < t; t < c\ \ norm (f c) * norm(c - t) < e/3" proof (cases "f c = 0") case False - hence "0 < e / 3 / norm (f c)" using \e>0\ by simp - then show ?thesis - apply - - apply rule - apply rule - apply assumption - apply safe + hence e3: "0 < e/3 / norm (f c)" using \e>0\ by simp + moreover have "norm (f c) * norm (c - t) < e/3" + if "t < c" and "c - e/3 / norm (f c) < t" for t proof - - fix t - assume as: "t < c" and "c - e / 3 / norm (f c) < t" - then have "c - t < e / 3 / norm (f c)" - by auto - then have "norm (c - t) < e / 3 / norm (f c)" - using as by auto - then show "norm (f c) * norm (c - t) < e / 3" - using False - apply - - apply (subst mult.commute) - apply (subst pos_less_divide_eq[symmetric]) - apply auto - done + have "norm (c - t) < e/3 / norm (f c)" + using that by auto + then show "norm (f c) * norm (c - t) < e/3" + by (metis e3 mult.commute norm_not_less_zero pos_less_divide_eq zero_less_divide_iff) qed + ultimately show ?thesis + using that by auto next - case True - show ?thesis - apply (rule_tac x=1 in exI) - unfolding True - using \e > 0\ - apply auto - done + case True then show ?thesis + using \e > 0\ that by auto qed - then guess w .. note w = conjunctD2[OF this,rule_format] - - have *: "e / 3 > 0" - using assms by auto - have "f integrable_on {a .. c}" - apply (rule integrable_subinterval_real[OF assms(1)]) - using assms(2-3) - apply auto - done - from integrable_integral[OF this,unfolded has_integral_real,rule_format,OF *] guess d1 .. - note d1 = conjunctD2[OF this,rule_format] + + have e3: "e/3 > 0" + using \e > 0\ by auto + have "f integrable_on {a..c}" + apply (rule integrable_subinterval_real[OF intf]) + using \a < c\ \c \ b\ by auto + then obtain d1 where "gauge d1" and d1: + "\p. \p tagged_division_of {a..c}; d1 fine p\ \ + norm ((\(x,K)\p. content K *\<^sub>R f x) - integral {a..c} f) < e/3" + using integrable_integral has_integral_real e3 by metis define d where [abs_def]: "d x = ball x w \ d1 x" for x have "gauge d" - unfolding d_def using w(1) d1 by auto - note this[unfolded gauge_def,rule_format,of c] - note conjunctD2[OF this] - from this(2)[unfolded open_contains_ball,rule_format,OF this(1)] guess k .. - note k=conjunctD2[OF this] + unfolding d_def using \w > 0\ \gauge d1\ by auto + then obtain k where "0 < k" and k: "ball c k \ d c" + by (meson gauge_def open_contains_ball) let ?d = "min k (c - a) / 2" show ?thesis @@ -4145,86 +4091,73 @@ apply safe proof - show "?d > 0" - using k(1) using assms(2) by auto + using \0 < k\ using assms(2) by auto fix t assume as: "c - ?d < t" "t \ c" - let ?thesis = "norm (integral ({a .. c}) f - integral ({a .. t}) f) < e" + let ?thesis = "norm (integral ({a..c}) f - integral ({a..t}) f) < e" { presume *: "t < c \ ?thesis" show ?thesis - apply (cases "t = c") - defer - apply (rule *) - apply (subst less_le) - using \e > 0\ as(2) - apply auto - done + proof (cases "t = c") + case True + then show ?thesis + by (simp add: \e > 0\) + next + case False + then show ?thesis + using "*" \t \ c\ by linarith + qed } assume "t < c" - have "f integrable_on {a .. t}" - apply (rule integrable_subinterval_real[OF assms(1)]) - using assms(2-3) as(2) - apply auto - done - from integrable_integral[OF this,unfolded has_integral_real,rule_format,OF *] guess d2 .. - note d2 = conjunctD2[OF this,rule_format] + have "f integrable_on {a..t}" + apply (rule integrable_subinterval_real[OF intf]) + using \t < c\ \c \ b\ by auto + then obtain d2 where d2: "gauge d2" + "\p. p tagged_division_of {a..t} \ d2 fine p \ + norm ((\(x,K)\p. content K *\<^sub>R f x) - integral {a..t} f) < e/3" + using integrable_integral has_integral_real e3 by metis define d3 where "d3 x = (if x \ t then d1 x \ d2 x else d1 x)" for x have "gauge d3" - using d2(1) d1(1) unfolding d3_def gauge_def by auto - from fine_division_exists_real[OF this, of a t] guess p . note p=this - note p'=tagged_division_ofD[OF this(1)] - have pt: "\(x,k)\p. x \ t" - proof (safe, goal_cases) - case prems: 1 - from p'(2,3)[OF prems] show ?case - by auto - qed - with p(2) have "d2 fine p" - unfolding fine_def d3_def - apply safe - apply (erule_tac x="(a,b)" in ballE)+ - apply auto - done - note d2_fin = d2(2)[OF conjI[OF p(1) this]] - - have *: "{a .. c} \ {x. x \ 1 \ t} = {a .. t}" "{a .. c} \ {x. x \ 1 \ t} = {t .. c}" - using assms(2-3) as by (auto simp add: field_simps) - have "p \ {(c, {t .. c})} tagged_division_of {a .. c} \ d1 fine p \ {(c, {t .. c})}" - apply rule + using \gauge d1\ \gauge d2\ unfolding d3_def gauge_def by auto + then obtain p where ptag: "p tagged_division_of {a..t}" and pfine: "d3 fine p" + by (metis box_real(2) fine_division_exists) + note p'=tagged_division_ofD[OF ptag] + have pt: "(x,k)\p \ x \ t" for x k + by (meson atLeastAtMost_iff p'(2) p'(3) subsetCE) + with pfine have "d2 fine p" + unfolding fine_def d3_def by fastforce + then have d2_fin: "norm ((\(x, K)\p. content K *\<^sub>R f x) - integral {a..t} f) < e/3" + using d2(2) ptag by auto + have *: "{a..c} \ {x. x \ t} = {a..t}" "{a..c} \ {x. x \ t} = {t..c}" + using as by (auto simp add: field_simps) + + have "p \ {(c, {t..c})} tagged_division_of {a..c}" apply (rule tagged_division_union_interval_real[of _ _ _ 1 "t"]) - unfolding * - apply (rule p) - apply (rule tagged_division_of_self_real) + using \t \ c\ by (auto simp: * ptag tagged_division_of_self_real) + moreover + have "d1 fine p \ {(c, {t..c})}" unfolding fine_def - apply safe - proof - - fix x k y - assume "(x,k) \ p" and "y \ k" - then show "y \ d1 x" - using p(2) pt - unfolding fine_def d3_def - apply - - apply (erule_tac x="(x,k)" in ballE)+ - apply auto - done + proof safe + fix x K y + assume "(x,K) \ p" and "y \ K" then show "y \ d1 x" + by (metis Int_iff d3_def subsetD fineD pfine) next fix x assume "x \ {t..c}" then have "dist c x < k" - unfolding dist_real_def using as(1) - by (auto simp add: field_simps) - then show "x \ d1 c" - using k(2) - unfolding d_def - by auto - qed (insert as(2), auto) note d1_fin = d1(2)[OF this] - - have *: "integral {a .. c} f - integral {a .. t} f = -(((c - t) *\<^sub>R f c + (\(x, k)\p. content k *\<^sub>R f x)) - - integral {a .. c} f) + ((\(x, k)\p. content k *\<^sub>R f x) - integral {a .. t} f) + (c - t) *\<^sub>R f c" + by (auto simp add: field_simps dist_real_def) + with k show "x \ d1 c" + unfolding d_def by auto + qed + ultimately have d1_fin: "norm ((\(x,K) \ p \ {(c, {t..c})}. content K *\<^sub>R f x) - integral {a..c} f) < e/3" + using d1 by metis + + have *: "integral {a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + (\(x, k)\p. content k *\<^sub>R f x)) - + integral {a..c} f) + ((\(x, k)\p. content k *\<^sub>R f x) - integral {a..t} f) + (c - t) *\<^sub>R f c" "e = (e/3 + e/3) + e/3" by auto - have **: "(\(x, k)\p \ {(c, {t .. c})}. content k *\<^sub>R f x) = + have **: "(\(x, k)\p \ {(c, {t..c})}. content k *\<^sub>R f x) = (c - t) *\<^sub>R f c + (\(x, k)\p. content k *\<^sub>R f x)" proof - have **: "\x F. F \ {x} = insert x F" @@ -4255,7 +4188,7 @@ using \k>0\ as(1) by (auto simp add: field_simps) moreover have "k \ w" apply (rule ccontr) - using k(2) + using k unfolding subset_eq apply (erule_tac x="c + ((k + w)/2)" in ballE) unfolding d_def @@ -4272,21 +4205,22 @@ unfolding norm_minus_cancel apply (rule d1_fin[unfolded **]) apply (rule d2_fin) - using w(2)[OF ***] + using w *** unfolding norm_scaleR apply (auto simp add: field_simps) done qed qed + lemma indefinite_integral_continuous_right: fixes f :: "real \ 'a::banach" - assumes "f integrable_on {a .. b}" + assumes "f integrable_on {a..b}" and "a \ c" and "c < b" and "e > 0" obtains d where "0 < d" - and "\t. c \ t \ t < c + d \ norm (integral {a .. c} f - integral {a .. t} f) < e" + and "\t. c \ t \ t < c + d \ norm (integral {a..c} f - integral {a..t} f) < e" proof - have *: "(\x. f (- x)) integrable_on {-b .. -a}" "- b < - c" "- c \ - a" using assms by auto @@ -4300,8 +4234,8 @@ using d(1) assms(3) by auto fix t :: real assume as: "c \ t" "t < c + ?d" - have *: "integral {a .. c} f = integral {a .. b} f - integral {c .. b} f" - "integral {a .. t} f = integral {a .. b} f - integral {t .. b} f" + have *: "integral {a..c} f = integral {a..b} f - integral {c..b} f" + "integral {a..t} f = integral {a..b} f - integral {t..b} f" apply (simp_all only: algebra_simps) apply (rule_tac[!] integral_combine) using assms as @@ -4309,7 +4243,7 @@ done have "(- c) - d < (- t) \ - t \ - c" using as by auto note d(2)[rule_format,OF this] - then show "norm (integral {a .. c} f - integral {a .. t} f) < e" + then show "norm (integral {a..c} f - integral {a..t} f) < e" unfolding * unfolding integral_reflect apply (subst norm_minus_commute) @@ -4320,8 +4254,8 @@ lemma indefinite_integral_continuous_1: fixes f :: "real \ 'a::banach" - assumes "f integrable_on {a .. b}" - shows "continuous_on {a .. b} (\x. integral {a .. x} f)" + assumes "f integrable_on {a..b}" + shows "continuous_on {a..b} (\x. integral {a..x} f)" proof - have "\d>0. \x'\{a..b}. dist x' x < d \ dist (integral {a..x'} f) (integral {a..x} f) < e" if x: "x \ {a..b}" and "e > 0" for x e :: real @@ -4378,7 +4312,7 @@ assumes "f integrable_on {a..b}" shows "continuous_on {a..b} (\x. integral {x..b} f)" proof - - have "integral {a .. b} f - integral {a .. x} f = integral {x .. b} f" if "x \ {a .. b}" for x + have "integral {a..b} f - integral {a..x} f = integral {x..b} f" if "x \ {a..b}" for x using integral_combine[OF _ _ assms, of x] that by (auto simp: algebra_simps) with _ show ?thesis @@ -4391,16 +4325,16 @@ lemma has_derivative_zero_unique_strong_interval: fixes f :: "real \ 'a::banach" assumes "finite k" - and "continuous_on {a .. b} f" + and "continuous_on {a..b} f" and "f a = y" - and "\x\({a .. b} - k). (f has_derivative (\h. 0)) (at x within {a .. b})" "x \ {a .. b}" + and "\x\({a..b} - k). (f has_derivative (\h. 0)) (at x within {a..b})" "x \ {a..b}" shows "f x = y" proof - have ab: "a \ b" using assms by auto have *: "a \ x" using assms(5) by auto - have "((\x. 0::'a) has_integral f x - f a) {a .. x}" + have "((\x. 0::'a) has_integral f x - f a) {a..x}" apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1) *]) apply (rule continuous_on_subset[OF assms(2)]) defer @@ -4409,7 +4343,7 @@ apply (subst has_derivative_within_open[symmetric]) apply assumption apply (rule open_greaterThanLessThan) - apply (rule has_derivative_within_subset[where s="{a .. b}"]) + apply (rule has_derivative_within_subset[where s="{a..b}"]) using assms(4) assms(5) apply (auto simp: mem_box) done @@ -4483,14 +4417,14 @@ apply rule proof - fix t - assume as: "t \ {0 .. 1} - {t. (1 - t) *\<^sub>R c + t *\<^sub>R x \ k}" + assume as: "t \ {0..1} - {t. (1 - t) *\<^sub>R c + t *\<^sub>R x \ k}" have *: "c - t *\<^sub>R c + t *\<^sub>R x \ s - k" apply safe apply (rule conv[unfolded scaleR_simps]) using \x \ s\ \c \ s\ as by (auto simp add: algebra_simps) have "(f \ (\t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\x. 0) \ (\z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) - (at t within {0 .. 1})" + (at t within {0..1})" apply (intro derivative_eq_intros) apply simp_all apply (simp add: field_simps) @@ -4502,7 +4436,7 @@ using \x \ s\ \c \ s\ apply auto done - then show "((\xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\h. 0)) (at t within {0 .. 1})" + then show "((\xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\h. 0)) (at t within {0..1})" unfolding o_def . qed auto then show ?thesis @@ -4535,7 +4469,7 @@ proof safe fix x assume "x \ s" - from assms(2)[unfolded open_contains_ball,rule_format,OF this] guess e .. note e=conjunctD2[OF this] + from assms(2)[unfolded open_contains_ball,rule_format,OF this] guess e..note e=conjunctD2[OF this] show "\e>0. ball x e \ {xa \ s. f xa \ {f x}}" apply rule apply rule @@ -4788,7 +4722,7 @@ qed (insert B \e>0\, auto) next assume as: "\e>0. ?r e" - from this[rule_format,OF zero_less_one] guess C .. note C=conjunctD2[OF this,rule_format] + from this[rule_format,OF zero_less_one] guess C..note C=conjunctD2[OF this,rule_format] define c :: 'n where "c = (\i\Basis. (- max B C) *\<^sub>R i)" define d :: 'n where "d = (\i\Basis. max B C *\<^sub>R i)" have c_d: "cbox a b \ cbox c d" @@ -4817,7 +4751,7 @@ unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,symmetric] unfolding s by auto - then guess y .. note y=this + then guess y..note y=this have "y = i" proof (rule ccontr) @@ -4850,7 +4784,7 @@ unfolding c_def d_def by (auto simp: sum_negf) qed - note C(2)[OF this] then guess z .. note z = conjunctD2[OF this, unfolded s] + note C(2)[OF this] then guess z..note z = conjunctD2[OF this, unfolded s] note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]] then have "z = y" and "norm (z - i) < norm (y - i)" apply - @@ -5149,7 +5083,7 @@ apply safe proof goal_cases case (1 e) - from \?r\[THEN conjunct2,rule_format,OF this] guess B .. note B=conjunctD2[OF this] + from \?r\[THEN conjunct2,rule_format,OF this] guess B..note B=conjunctD2[OF this] show ?case apply rule apply rule @@ -5167,7 +5101,7 @@ show ?r proof safe fix a b :: 'n - from as[OF zero_less_one] guess B .. note B=conjunctD2[OF this,rule_format] + from as[OF zero_less_one] guess B..note B=conjunctD2[OF this,rule_format] let ?a = "\i\Basis. min (a\i) (-B) *\<^sub>R i::'n" let ?b = "\i\Basis. max (b\i) B *\<^sub>R i::'n" show "?f integrable_on cbox a b" @@ -5180,7 +5114,7 @@ then show ?case using Basis_le_norm[of i x] by (auto simp add:field_simps) qed - from B(2)[OF this] guess z .. note conjunct1[OF this] + from B(2)[OF this] guess z..note conjunct1[OF this] then show "?f integrable_on cbox ?a ?b" unfolding integrable_on_def by auto show "cbox a b \ cbox ?a ?b" @@ -5194,7 +5128,7 @@ fix e :: real assume "e > 0" - from as[OF this] guess B .. note B=conjunctD2[OF this,rule_format] + from as[OF this] guess B..note B=conjunctD2[OF this,rule_format] show "\B>0. \a b. ball 0 B \ cbox a b \ norm (integral (cbox a b) (\x. if x \ s then f x else 0) - i) < e" apply rule @@ -5203,7 +5137,7 @@ apply safe proof goal_cases case 1 - from B(2)[OF this] guess z .. note z=conjunctD2[OF this] + from B(2)[OF this] guess z..note z=conjunctD2[OF this] from integral_unique[OF this(1)] show ?case using z(2) by auto qed @@ -5223,7 +5157,7 @@ (is "?l = ?r") proof assume ?l - then guess y unfolding integrable_on_def .. note this[unfolded has_integral_alt'[of f]] + then guess y unfolding integrable_on_def..note this[unfolded has_integral_alt'[of f]] note y=conjunctD2[OF this,rule_format] show ?r apply safe @@ -5232,7 +5166,7 @@ case (1 e) then have "e/2 > 0" by auto - from y(2)[OF this] guess B .. note B=conjunctD2[OF this,rule_format] + from y(2)[OF this] guess B..note B=conjunctD2[OF this,rule_format] show ?case apply rule apply rule @@ -5254,8 +5188,8 @@ have "Cauchy (\n. integral (?cube n) (\x. if x \ s then f x else 0))" proof (unfold Cauchy_def, safe, goal_cases) case (1 e) - from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format] - from real_arch_simple[of B] guess N .. note N = this + from as(2)[OF this] guess B..note B = conjunctD2[OF this,rule_format] + from real_arch_simple[of B] guess N..note N = this { fix n assume n: "n \ N" @@ -5289,8 +5223,8 @@ proof goal_cases case (1 e) then have *: "e/2 > 0" by auto - from i[OF this] guess N .. note N =this[rule_format] - from as(2)[OF *] guess B .. note B=conjunctD2[OF this,rule_format] + from i[OF this] guess N..note N =this[rule_format] + from as(2)[OF *] guess B..note B=conjunctD2[OF this,rule_format] let ?B = "max (real N) B" show ?case apply (rule_tac x="?B" in exI) @@ -5299,7 +5233,7 @@ using B(1) by auto fix a b :: 'n assume ab: "ball 0 ?B \ cbox a b" - from real_arch_simple[of ?B] guess n .. note n=this + from real_arch_simple[of ?B] guess n..note n=this show "norm (integral (cbox a b) (\x. if x \ s then f x else 0) - i) < e" apply (rule norm_triangle_half_l) apply (rule B(2)) @@ -5608,7 +5542,7 @@ then show ?case proof (cases "x \ \t") case True - then guess s unfolding Union_iff .. note s=this + then guess s unfolding Union_iff..note s=this then have *: "\b\t. x \ b \ b = s" using prems(3) by blast show ?thesis @@ -5835,7 +5769,7 @@ apply auto done note integrable_integral[OF this, unfolded has_integral[of f]] - from this[rule_format,OF *] guess dd .. note dd=conjunctD2[OF this,rule_format] + from this[rule_format,OF *] guess dd..note dd=conjunctD2[OF this,rule_format] note gauge_Int[OF \gauge d\ dd(1)] from fine_division_exists[OF this,of u v] guess qq . then show ?case @@ -5845,7 +5779,7 @@ apply auto done qed - from bchoice[OF this] guess qq .. note qq=this[rule_format] + from bchoice[OF this] guess qq..note qq=this[rule_format] let ?p = "p \ \(qq ` r)" have "norm ((\(x, k)\?p. content k *\<^sub>R f x) - integral (cbox a b) f) < e" @@ -6066,7 +6000,7 @@ proof - have *: "e / (2 * (real DIM('n) + 1)) > 0" using assms(2) by simp from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this] - guess d .. note d = conjunctD2[OF this] + guess d..note d = conjunctD2[OF this] show thesis apply (rule that) apply (rule d) @@ -6125,7 +6059,7 @@ using assms(4) apply auto done - then guess i .. note i=this + then guess i..note i=this have i': "\k. (integral(cbox a b) (f k)) \ i\1" apply (rule Lim_component_ge) apply (rule i) @@ -6153,7 +6087,7 @@ apply (rule assms(1)[unfolded has_integral_integral has_integral,rule_format]) apply auto done - from choice[OF this] guess c .. note c=conjunctD2[OF this[rule_format],rule_format] + from choice[OF this] guess c..note c=conjunctD2[OF this[rule_format],rule_format] have "\r. \k\r. 0 \ i\1 - (integral (cbox a b) (f k)) \ i\1 - (integral (cbox a b) (f k)) < e / 4" proof - @@ -6167,7 +6101,7 @@ subgoal for k using i'[of k] by auto done qed - then guess r .. note r=conjunctD2[OF this[rule_format]] + then guess r..note r=conjunctD2[OF this[rule_format]] have "\x\cbox a b. \n\r. \k\n. 0 \ (g x)\1 - (f k x)\1 \ (g x)\1 - (f k x)\1 < e / (4 * content(cbox a b))" @@ -6176,7 +6110,7 @@ have "e / (4 * content (cbox a b)) > 0" by (simp add: False content_lt_nz e) from assms(3)[rule_format, OF prems, THEN LIMSEQ_D, OF this] - guess n .. note n=this + guess n..note n=this then show ?case apply (rule_tac x="n + r" in exI) apply safe @@ -6186,7 +6120,7 @@ apply (auto simp add: field_simps) done qed - from bchoice[OF this] guess m .. note m=conjunctD2[OF this[rule_format],rule_format] + from bchoice[OF this] guess m..note m=conjunctD2[OF this[rule_format],rule_format] define d where "d x = c (m x) x" for x show ?case apply (rule_tac x=d in exI) @@ -6199,7 +6133,7 @@ note p'=tagged_division_ofD[OF p(1)] have "\a. \x\p. m (fst x) \ a" by (metis finite_imageI finite_nat_set_iff_bounded_le p'(1) rev_image_eqI) - then guess s .. note s=this + then guess s..note s=this have *: "\a b c d. norm(a - b) \ e / 4 \ norm(b - c) < e / 2 \ norm (c - d) < e / 4 \ norm (a - d) < e" proof (safe, goal_cases) @@ -6387,7 +6321,7 @@ using that(3) apply auto done - then guess i .. note i=this + then guess i..note i=this have "\k. \x\s. \n\k. f k x \ f n x" using assms(3) by (force intro: transitive_stepwise_le) then have i': "\k. (integral s (f k))\1 \ i\1" @@ -6477,9 +6411,9 @@ case (1 e) then have "e/4>0" by auto - from LIMSEQ_D [OF i this] guess N .. note N=this + from LIMSEQ_D [OF i this] guess N..note N=this note assms(2)[of N,unfolded has_integral_integral has_integral_alt'[of "f N"]] - from this[THEN conjunct2,rule_format,OF \e/4>0\] guess B .. note B=conjunctD2[OF this] + from this[THEN conjunct2,rule_format,OF \e/4>0\] guess B..note B=conjunctD2[OF this] show ?case apply rule apply rule @@ -6490,7 +6424,7 @@ assume ab: "ball 0 B \ cbox a b" from \e > 0\ have "e/2 > 0" by auto - from LIMSEQ_D [OF g(2)[of a b] this] guess M .. note M=this + from LIMSEQ_D [OF g(2)[of a b] this] guess M..note M=this have **: "norm (integral (cbox a b) (\x. if x \ s then f N x else 0) - i) < e/2" apply (rule norm_triangle_half_l) using B(2)[rule_format,OF ab] N[rule_format,of N] @@ -6745,18 +6679,18 @@ note assms(1)[unfolded integrable_alt[of f]] note f=this[THEN conjunct1,rule_format] note assms(2)[unfolded integrable_alt[of g]] note g=this[THEN conjunct1,rule_format] from integrable_integral[OF assms(1),unfolded has_integral'[of f],rule_format,OF e] - guess B1 .. note B1=conjunctD2[OF this[rule_format],rule_format] + guess B1..note B1=conjunctD2[OF this[rule_format],rule_format] from integrable_integral[OF assms(2),unfolded has_integral'[of g],rule_format,OF e] - guess B2 .. note B2=conjunctD2[OF this[rule_format],rule_format] + guess B2..note B2=conjunctD2[OF this[rule_format],rule_format] from bounded_subset_cbox[OF bounded_ball, of "0::'n" "max B1 B2"] guess a b by (elim exE) note ab=this[unfolded ball_max_Un] have "ball 0 B1 \ cbox a b" using ab by auto - from B1(2)[OF this] guess z .. note z=conjunctD2[OF this] + from B1(2)[OF this] guess z..note z=conjunctD2[OF this] have "ball 0 B2 \ cbox a b" using ab by auto - from B2(2)[OF this] guess w .. note w=conjunctD2[OF this] + from B2(2)[OF this] guess w..note w=conjunctD2[OF this] show "norm (integral s f) < integral s g + e" apply (rule norm) @@ -7076,12 +7010,12 @@ lemma uniform_limit_integral: fixes f::"'a \ 'b::ordered_euclidean_space \ 'c::banach" - assumes u: "uniform_limit {a .. b} f g F" - assumes c: "\n. continuous_on {a .. b} (f n)" + assumes u: "uniform_limit {a..b} f g F" + assumes c: "\n. continuous_on {a..b} (f n)" assumes [simp]: "F \ bot" obtains I J where - "\n. (f n has_integral I n) {a .. b}" - "(g has_integral J) {a .. b}" + "\n. (f n has_integral I n) {a..b}" + "(g has_integral J) {a..b}" "(I \ J) F" by (metis interval_cbox assms uniform_limit_integral_cbox) @@ -7844,21 +7778,21 @@ lemma content_closed_interval: fixes a :: "'a::ordered_euclidean_space" assumes "a \ b" - shows "content {a .. b} = (\i\Basis. b\i - a\i)" + shows "content {a..b} = (\i\Basis. b\i - a\i)" using content_cbox[of a b] assms by (simp add: cbox_interval eucl_le[where 'a='a]) lemma integrable_const_ivl[intro]: fixes a::"'a::ordered_euclidean_space" - shows "(\x. c) integrable_on {a .. b}" + shows "(\x. c) integrable_on {a..b}" unfolding cbox_interval[symmetric] by (rule integrable_const) lemma integrable_on_subinterval: fixes f :: "'n::ordered_euclidean_space \ 'a::banach" assumes "f integrable_on s" - and "{a .. b} \ s" - shows "f integrable_on {a .. b}" + and "{a..b} \ s" + shows "f integrable_on {a..b}" using integrable_on_subcbox[of f s a b] assms by (simp add: cbox_interval)