# HG changeset patch # User paulson # Date 1503847064 -3600 # Node ID 4585bfd1907452582ea44e552f441ce6294e65e9 # Parent 5fe7ed50d096c800e706836e2bf0ade4da8fac0f# Parent 0d8dab1f6903b4c59c4ef71577e880796885fab4 merged diff -r 5fe7ed50d096 -r 4585bfd19074 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Aug 27 16:56:25 2017 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Aug 27 16:17:44 2017 +0100 @@ -548,60 +548,52 @@ lemma has_integral_neg_iff: "((\x. - f x) has_integral k) S \ (f has_integral - k) S" using has_integral_neg[of f "- k"] has_integral_neg[of "\x. - f x" k] by auto +lemma has_integral_add_cbox: + fixes f :: "'n::euclidean_space \ 'a::real_normed_vector" + assumes "(f has_integral k) (cbox a b)" "(g has_integral l) (cbox a b)" + shows "((\x. f x + g x) has_integral (k + l)) (cbox a b)" + using assms + unfolding has_integral_cbox + by (simp add: split_beta' scaleR_add_right sum.distrib[abs_def] tendsto_add) + lemma has_integral_add: fixes f :: "'n::euclidean_space \ 'a::real_normed_vector" - assumes "(f has_integral k) S" - and "(g has_integral l) S" + assumes f: "(f has_integral k) S" and g: "(g has_integral l) S" shows "((\x. f x + g x) has_integral (k + l)) S" -proof - - have lem: "(f has_integral k) (cbox a b) \ (g has_integral l) (cbox a b) \ - ((\x. f x + g x) has_integral (k + l)) (cbox a b)" - for f :: "'n \ 'a" and g a b k l - unfolding has_integral_cbox - by (simp add: split_beta' scaleR_add_right sum.distrib[abs_def] tendsto_add) - { - presume "\ (\a b. S = cbox a b) \ ?thesis" - then show ?thesis - using assms lem by force - } - assume nonbox: "\ (\a b. S = cbox a b)" +proof (cases "\a b. S = cbox a b") + case True with has_integral_add_cbox assms show ?thesis + by blast +next + let ?S = "\f x. if x \ S then f x else 0" + case False then show ?thesis proof (subst has_integral_alt, clarsimp, goal_cases) case (1 e) - then have *: "e/2 > 0" + then have e2: "e/2 > 0" by auto - from has_integral_altD[OF assms(1) nonbox *] - obtain B1 where B1: - "0 < B1" - "\a b. ball 0 B1 \ cbox a b \ - \z. ((\x. if x \ S then f x else 0) has_integral z) (cbox a b) \ norm (z - k) < e/2" - by blast - from has_integral_altD[OF assms(2) nonbox *] - obtain B2 where B2: - "0 < B2" - "\a b. ball 0 B2 \ (cbox a b) \ - \z. ((\x. if x \ S then g x else 0) has_integral z) (cbox a b) \ norm (z - l) < e/2" - by blast + obtain Bf where "0 < Bf" + and Bf: "\a b. ball 0 Bf \ cbox a b \ + \z. (?S f has_integral z) (cbox a b) \ norm (z - k) < e/2" + using has_integral_altD[OF f False e2] by blast + obtain Bg where "0 < Bg" + and Bg: "\a b. ball 0 Bg \ (cbox a b) \ + \z. (?S g has_integral z) (cbox a b) \ norm (z - l) < e/2" + using has_integral_altD[OF g False e2] by blast show ?case - proof (rule_tac x="max B1 B2" in exI, clarsimp simp add: max.strict_coboundedI1 B1) + proof (rule_tac x="max Bf Bg" in exI, clarsimp simp add: max.strict_coboundedI1 \0 < Bf\) fix a b - assume "ball 0 (max B1 B2) \ cbox a (b::'n)" - then have *: "ball 0 B1 \ cbox a (b::'n)" "ball 0 B2 \ cbox a (b::'n)" + assume "ball 0 (max Bf Bg) \ cbox a (b::'n)" + then have fs: "ball 0 Bf \ cbox a (b::'n)" and gs: "ball 0 Bg \ cbox a (b::'n)" by auto - obtain w where w: - "((\x. if x \ S then f x else 0) has_integral w) (cbox a b)" - "norm (w - k) < e/2" - using B1(2)[OF *(1)] by blast - obtain z where z: - "((\x. if x \ S then g x else 0) has_integral z) (cbox a b)" - "norm (z - l) < e/2" - using B2(2)[OF *(2)] by blast - have *: "\x. (if x \ S then f x + g x else 0) = - (if x \ S then f x else 0) + (if x \ S then g x else 0)" + obtain w where w: "(?S f has_integral w) (cbox a b)" "norm (w - k) < e/2" + using Bf[OF fs] by blast + obtain z where z: "(?S g has_integral z) (cbox a b)" "norm (z - l) < e/2" + using Bg[OF gs] by blast + have *: "\x. (if x \ S then f x + g x else 0) = (?S f x) + (?S g x)" by auto - show "\z. ((\x. if x \ S then f x + g x else 0) has_integral z) (cbox a b) \ norm (z - (k + l)) < e" + show "\z. (?S(\x. f x + g x) has_integral z) (cbox a b) \ norm (z - (k + l)) < e" apply (rule_tac x="w + z" in exI) - apply (simp add: lem[OF w(1) z(1), unfolded *[symmetric]]) + apply (simp add: has_integral_add_cbox[OF w(1) z(1), unfolded *[symmetric]]) using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2) apply (auto simp add: field_simps) done @@ -2875,129 +2867,87 @@ subsection \Only need trivial subintervals if the interval itself is trivial.\ -lemma division_of_nontrivial: - fixes s :: "'a::euclidean_space set set" - assumes "s division_of (cbox a b)" - and "content (cbox a b) \ 0" - shows "{k. k \ s \ content k \ 0} division_of (cbox a b)" - using assms(1) - apply - -proof (induct "card s" arbitrary: s rule: nat_less_induct) - fix s::"'a set set" - assume assm: "s division_of (cbox a b)" - "\mx. m = card x \ - x division_of (cbox a b) \ {k \ x. content k \ 0} division_of (cbox a b)" - note s = division_ofD[OF assm(1)] - let ?thesis = "{k \ s. content k \ 0} division_of (cbox a b)" +proposition division_of_nontrivial: + fixes \ :: "'a::euclidean_space set set" + assumes sdiv: "\ division_of (cbox a b)" + and cont0: "content (cbox a b) \ 0" + shows "{k. k \ \ \ content k \ 0} division_of (cbox a b)" + using sdiv +proof (induction "card \" arbitrary: \ rule: less_induct) + case less + note \ = division_ofD[OF less.prems] { - presume *: "{k \ s. content k \ 0} \ s \ ?thesis" - show ?thesis - apply cases - defer - apply (rule *) - apply assumption - using assm(1) - apply auto - done + presume *: "{k \ \. content k \ 0} \ \ \ ?case" + then show ?case + using less.prems by fastforce } - assume noteq: "{k \ s. content k \ 0} \ s" - then obtain k c d where k: "k \ s" "content k = 0" "k = cbox c d" - using s(4) by blast - then have "card s > 0" - unfolding card_gt_0_iff using assm(1) by auto - then have card: "card (s - {k}) < card s" - using assm(1) k(1) - apply (subst card_Diff_singleton_if) - apply auto - done - have *: "closed (\(s - {k}))" - apply (rule closed_Union) - defer - apply rule - apply (drule DiffD1,drule s(4)) - using assm(1) - apply auto - done - have "k \ \(s - {k})" - apply safe - apply (rule *[unfolded closed_limpt,rule_format]) + assume noteq: "{k \ \. content k \ 0} \ \" + then obtain K c d where "K \ \" and contk: "content K = 0" and keq: "K = cbox c d" + using \(4) by blast + then have "card \ > 0" + unfolding card_gt_0_iff using less by auto + then have card: "card (\ - {K}) < card \" + using less \K \ \\ by (simp add: \(1)) + have closed: "closed (\(\ - {K}))" + using less.prems by auto + have "x islimpt \(\ - {K})" if "x \ K" for x unfolding islimpt_approachable - proof safe - fix x - fix e :: real - assume as: "x \ k" "e > 0" + proof (intro allI impI) + fix e::real + assume "e > 0" obtain i where i: "c\i = d\i" "i\Basis" - using k(2) s(3)[OF k(1)] unfolding box_ne_empty k - by (metis dual_order.antisym content_eq_0) + using contk \(3) [OF \K \ \\] unfolding box_ne_empty keq + by (meson content_eq_0 dual_order.antisym) then have xi: "x\i = d\i" - using as unfolding k mem_box by (metis antisym) + using \x \ K\ unfolding keq mem_box by (metis antisym) define y where "y = (\j\Basis. (if j = i then if c\i \ (a\i + b\i) / 2 then c\i + min e (b\i - c\i) / 2 else c\i - min e (c\i - a\i) / 2 else x\j) *\<^sub>R j)" - show "\x'\\(s - {k}). x' \ x \ dist x' x < e" - apply (rule_tac x=y in bexI) - proof + show "\x'\\(\ - {K}). x' \ x \ dist x' x < e" + proof (intro bexI conjI) have "d \ cbox c d" - using s(3)[OF k(1)] - unfolding k box_eq_empty mem_box - by (fastforce simp add: not_less) + using \(3)[OF \K \ \\] by (simp add: box_ne_empty(1) keq mem_box(2)) then have "d \ cbox a b" - using s(2)[OF k(1)] - unfolding k - by auto - note di = this[unfolded mem_box,THEN bspec[where x=i]] + using \(2)[OF \K \ \\] by (auto simp: keq) + then have di: "a \ i \ d \ i \ d \ i \ b \ i" + using \i \ Basis\ mem_box(2) by blast then have xyi: "y\i \ x\i" - unfolding y_def i xi - using as(2) assms(2)[unfolded content_eq_0] i(2) - by (auto elim!: ballE[of _ _ i]) + unfolding y_def i xi using \e > 0\ cont0 \i \ Basis\ + by (auto simp: content_eq_0 elim!: ballE[of _ _ i]) then show "y \ x" unfolding euclidean_eq_iff[where 'a='a] using i by auto - have *: "Basis = insert i (Basis - {i})" - using i by auto - have "norm (y-x) < e + sum (\i. 0) Basis" - apply (rule le_less_trans[OF norm_le_l1]) - apply (subst *) - apply (subst sum.insert) - prefer 3 - apply (rule add_less_le_mono) - proof - + have "norm (y-x) \ (\b\Basis. \(y - x) \ b\)" + by (rule norm_le_l1) + also have "... = \(y - x) \ i\ + (\b \ Basis - {i}. \(y - x) \ b\)" + by (meson finite_Basis i(2) sum.remove) + also have "... < e + sum (\i. 0) Basis" + proof (rule add_less_le_mono) show "\(y-x) \ i\ < e" - using di as(2) y_def i xi by (auto simp: inner_simps) + using di \e > 0\ y_def i xi by (auto simp: inner_simps) show "(\i\Basis - {i}. \(y-x) \ i\) \ (\i\Basis. 0)" unfolding y_def by (auto simp: inner_simps) - qed auto + qed + finally have "norm (y-x) < e + sum (\i. 0) Basis" . then show "dist y x < e" unfolding dist_norm by auto - have "y \ k" - unfolding k mem_box - apply rule - apply (erule_tac x=i in ballE) - using xyi k i xi - apply auto - done - moreover - have "y \ \s" - using set_rev_mp[OF as(1) s(2)[OF k(1)]] as(2) di i - unfolding s mem_box y_def - by (auto simp: field_simps elim!: ballE[of _ _ i]) - ultimately - show "y \ \(s - {k})" by auto + have "y \ K" + unfolding keq mem_box using i(1) i(2) xi xyi by fastforce + moreover have "y \ \\" + using subsetD[OF \(2)[OF \K \ \\] \x \ K\] \e > 0\ di i + by (auto simp: \ mem_box y_def field_simps elim!: ballE[of _ _ i]) + ultimately show "y \ \(\ - {K})" by auto qed qed - then have "\(s - {k}) = cbox a b" - unfolding s(6)[symmetric] by auto - then have "{ka \ s - {k}. content ka \ 0} division_of (cbox a b)" - apply - - apply (rule assm(2)[rule_format,OF card refl]) - apply (rule division_ofI) - defer - apply (rule_tac[1-4] s) - using assm(1) - apply auto - done - moreover - have "{ka \ s - {k}. content ka \ 0} = {k \ s. content k \ 0}" - using k by auto - ultimately show ?thesis by auto + then have "K \ \(\ - {K})" + using closed closed_limpt by blast + then have "\(\ - {K}) = cbox a b" + unfolding \(6)[symmetric] by auto + then have "\ - {K} division_of cbox a b" + by (metis Diff_subset less.prems division_of_subset \(6)) + then have "{ka \ \ - {K}. content ka \ 0} division_of (cbox a b)" + using card less.hyps by blast + moreover have "{ka \ \ - {K}. content ka \ 0} = {K \ \. content K \ 0}" + using contk by auto + ultimately show ?case by auto qed @@ -3046,7 +2996,7 @@ 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) + by (metis assms box_real(2) integrable_subinterval) subsection \Combining adjacent intervals in 1 dimension.\ @@ -4202,11 +4152,9 @@ unfolding *(1) apply (subst *(2)) apply (rule norm_triangle_lt add_strict_mono)+ - unfolding norm_minus_cancel - apply (rule d1_fin[unfolded **]) - apply (rule d2_fin) + apply (metis "**" d1_fin norm_minus_cancel) + using d2_fin apply blast using w *** - unfolding norm_scaleR apply (auto simp add: field_simps) done qed