# HG changeset patch # User paulson # Date 1503838223 -3600 # Node ID 5a1a2ac950c285125204fb38d354e87e4eedb6aa # Parent b6d04f487ddd68fdfc9c45204e96dca12fa9df92 division_of_nontrivial partial cleanup diff -r b6d04f487ddd -r 5a1a2ac950c2 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Aug 26 23:58:03 2017 +0100 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Aug 27 13:50:23 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 @@ -2877,106 +2869,76 @@ lemma division_of_nontrivial: fixes s :: "'a::euclidean_space set set" - assumes "s division_of (cbox a b)" + assumes s: "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)" + using s +proof (induction "card s" arbitrary: s rule: less_induct) + case less + note s = 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 \ s. content k \ 0} \ s \ ?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 obtain k c d where "k \ s" and contk: "content k = 0" and keq: "k = cbox c d" + using s(4) by blast then have "card s > 0" - unfolding card_gt_0_iff using assm(1) by auto + unfolding card_gt_0_iff using less 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 + using less \k \ s\ by (simp add: s(1)) + have closed: "closed (\(s - {k}))" + using less.prems by auto have "k \ \(s - {k})" apply safe - apply (rule *[unfolded closed_limpt,rule_format]) + apply (rule closed[unfolded closed_limpt,rule_format]) unfolding islimpt_approachable proof safe - fix x - fix e :: real - assume as: "x \ k" "e > 0" + fix x and e :: real + assume "x \ k" "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 s(3) [OF \k \ s\] 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 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 s(3)[OF \k \ s\] 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 + using s(2)[OF \k \ s\] + unfolding keq by auto note di = this[unfolded mem_box,THEN bspec[where x=i]] then have xyi: "y\i \ x\i" unfolding y_def i xi - using as(2) assms(2)[unfolded content_eq_0] i(2) + using \e > 0\ assms(2)[unfolded content_eq_0] i(2) by (auto 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 + unfolding keq mem_box using i(1) i(2) xi xyi by fastforce moreover have "y \ \s" - using set_rev_mp[OF as(1) s(2)[OF k(1)]] as(2) di i + using subsetD[OF s(2)[OF \k \ s\] \x \ k\] \e > 0\ di i unfolding s mem_box y_def by (auto simp: field_simps elim!: ballE[of _ _ i]) ultimately @@ -2985,19 +2947,14 @@ 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 + then have "s - {k} division_of cbox a b" + by (metis Diff_subset less.prems division_of_subset s(6)) + then have "{ka \ s - {k}. content ka \ 0} division_of (cbox a b)" + using card less.hyps by blast moreover have "{ka \ s - {k}. content ka \ 0} = {k \ s. content k \ 0}" - using k by auto - ultimately show ?thesis by auto + using contk by auto + ultimately show ?case by auto qed