--- 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: "((\<lambda>x. - f x) has_integral k) S \<longleftrightarrow> (f has_integral - k) S"
using has_integral_neg[of f "- k"] has_integral_neg[of "\<lambda>x. - f x" k] by auto
+lemma has_integral_add_cbox:
+ fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
+ assumes "(f has_integral k) (cbox a b)" "(g has_integral l) (cbox a b)"
+ shows "((\<lambda>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 \<Rightarrow> '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 "((\<lambda>x. f x + g x) has_integral (k + l)) S"
-proof -
- have lem: "(f has_integral k) (cbox a b) \<Longrightarrow> (g has_integral l) (cbox a b) \<Longrightarrow>
- ((\<lambda>x. f x + g x) has_integral (k + l)) (cbox a b)"
- for f :: "'n \<Rightarrow> '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 "\<not> (\<exists>a b. S = cbox a b) \<Longrightarrow> ?thesis"
- then show ?thesis
- using assms lem by force
- }
- assume nonbox: "\<not> (\<exists>a b. S = cbox a b)"
+proof (cases "\<exists>a b. S = cbox a b")
+ case True with has_integral_add_cbox assms show ?thesis
+ by blast
+next
+ let ?S = "\<lambda>f x. if x \<in> 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"
- "\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
- \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and> norm (z - k) < e/2"
- by blast
- from has_integral_altD[OF assms(2) nonbox *]
- obtain B2 where B2:
- "0 < B2"
- "\<And>a b. ball 0 B2 \<subseteq> (cbox a b) \<Longrightarrow>
- \<exists>z. ((\<lambda>x. if x \<in> S then g x else 0) has_integral z) (cbox a b) \<and> norm (z - l) < e/2"
- by blast
+ obtain Bf where "0 < Bf"
+ and Bf: "\<And>a b. ball 0 Bf \<subseteq> cbox a b \<Longrightarrow>
+ \<exists>z. (?S f has_integral z) (cbox a b) \<and> norm (z - k) < e/2"
+ using has_integral_altD[OF f False e2] by blast
+ obtain Bg where "0 < Bg"
+ and Bg: "\<And>a b. ball 0 Bg \<subseteq> (cbox a b) \<Longrightarrow>
+ \<exists>z. (?S g has_integral z) (cbox a b) \<and> 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 \<open>0 < Bf\<close>)
fix a b
- assume "ball 0 (max B1 B2) \<subseteq> cbox a (b::'n)"
- then have *: "ball 0 B1 \<subseteq> cbox a (b::'n)" "ball 0 B2 \<subseteq> cbox a (b::'n)"
+ assume "ball 0 (max Bf Bg) \<subseteq> cbox a (b::'n)"
+ then have fs: "ball 0 Bf \<subseteq> cbox a (b::'n)" and gs: "ball 0 Bg \<subseteq> cbox a (b::'n)"
by auto
- obtain w where w:
- "((\<lambda>x. if x \<in> 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:
- "((\<lambda>x. if x \<in> 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 *: "\<And>x. (if x \<in> S then f x + g x else 0) =
- (if x \<in> S then f x else 0) + (if x \<in> 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 *: "\<And>x. (if x \<in> S then f x + g x else 0) = (?S f x) + (?S g x)"
by auto
- show "\<exists>z. ((\<lambda>x. if x \<in> S then f x + g x else 0) has_integral z) (cbox a b) \<and> norm (z - (k + l)) < e"
+ show "\<exists>z. (?S(\<lambda>x. f x + g x) has_integral z) (cbox a b) \<and> 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) \<noteq> 0"
shows "{k. k \<in> s \<and> content k \<noteq> 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)"
- "\<forall>m<card s. \<forall>x. m = card x \<longrightarrow>
- x division_of (cbox a b) \<longrightarrow> {k \<in> x. content k \<noteq> 0} division_of (cbox a b)"
- note s = division_ofD[OF assm(1)]
- let ?thesis = "{k \<in> s. content k \<noteq> 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 \<in> s. content k \<noteq> 0} \<noteq> s \<Longrightarrow> ?thesis"
- show ?thesis
- apply cases
- defer
- apply (rule *)
- apply assumption
- using assm(1)
- apply auto
- done
+ presume *: "{k \<in> s. content k \<noteq> 0} \<noteq> s \<Longrightarrow> ?case"
+ then show ?case
+ using less.prems by fastforce
}
assume noteq: "{k \<in> s. content k \<noteq> 0} \<noteq> s"
- then obtain k c d where k: "k \<in> s" "content k = 0" "k = cbox c d"
- using s(4) by blast
+ then obtain k c d where "k \<in> 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 (\<Union>(s - {k}))"
- apply (rule closed_Union)
- defer
- apply rule
- apply (drule DiffD1,drule s(4))
- using assm(1)
- apply auto
- done
+ using less \<open>k \<in> s\<close> by (simp add: s(1))
+ have closed: "closed (\<Union>(s - {k}))"
+ using less.prems by auto
have "k \<subseteq> \<Union>(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 \<in> k" "e > 0"
+ fix x and e :: real
+ assume "x \<in> k" "e > 0"
obtain i where i: "c\<bullet>i = d\<bullet>i" "i\<in>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 \<open>k \<in> s\<close>] unfolding box_ne_empty keq
+ by (meson content_eq_0 dual_order.antisym)
then have xi: "x\<bullet>i = d\<bullet>i"
- using as unfolding k mem_box by (metis antisym)
+ using \<open>x \<in> k\<close> unfolding keq mem_box by (metis antisym)
define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i +
min e (b\<bullet>i - c\<bullet>i) / 2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i) / 2 else x\<bullet>j) *\<^sub>R j)"
show "\<exists>x'\<in>\<Union>(s - {k}). x' \<noteq> x \<and> dist x' x < e"
apply (rule_tac x=y in bexI)
proof
have "d \<in> 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 \<open>k \<in> s\<close>] by (simp add: box_ne_empty(1) keq mem_box(2))
then have "d \<in> cbox a b"
- using s(2)[OF k(1)]
- unfolding k
+ using s(2)[OF \<open>k \<in> s\<close>]
+ unfolding keq
by auto
note di = this[unfolded mem_box,THEN bspec[where x=i]]
then have xyi: "y\<bullet>i \<noteq> x\<bullet>i"
unfolding y_def i xi
- using as(2) assms(2)[unfolded content_eq_0] i(2)
+ using \<open>e > 0\<close> assms(2)[unfolded content_eq_0] i(2)
by (auto elim!: ballE[of _ _ i])
then show "y \<noteq> 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 (\<lambda>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) \<le> (\<Sum>b\<in>Basis. \<bar>(y - x) \<bullet> b\<bar>)"
+ by (rule norm_le_l1)
+ also have "... = \<bar>(y - x) \<bullet> i\<bar> + (\<Sum>b \<in> Basis - {i}. \<bar>(y - x) \<bullet> b\<bar>)"
+ by (meson finite_Basis i(2) sum.remove)
+ also have "... < e + sum (\<lambda>i. 0) Basis"
+ proof (rule add_less_le_mono)
show "\<bar>(y-x) \<bullet> i\<bar> < e"
- using di as(2) y_def i xi by (auto simp: inner_simps)
+ using di \<open>e > 0\<close> y_def i xi by (auto simp: inner_simps)
show "(\<Sum>i\<in>Basis - {i}. \<bar>(y-x) \<bullet> i\<bar>) \<le> (\<Sum>i\<in>Basis. 0)"
unfolding y_def by (auto simp: inner_simps)
- qed auto
+ qed
+ finally have "norm (y-x) < e + sum (\<lambda>i. 0) Basis" .
then show "dist y x < e"
unfolding dist_norm by auto
have "y \<notin> 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 \<in> \<Union>s"
- using set_rev_mp[OF as(1) s(2)[OF k(1)]] as(2) di i
+ using subsetD[OF s(2)[OF \<open>k \<in> s\<close>] \<open>x \<in> k\<close>] \<open>e > 0\<close> 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 "\<Union>(s - {k}) = cbox a b"
unfolding s(6)[symmetric] by auto
- then have "{ka \<in> s - {k}. content ka \<noteq> 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 \<in> s - {k}. content ka \<noteq> 0} division_of (cbox a b)"
+ using card less.hyps by blast
moreover
have "{ka \<in> s - {k}. content ka \<noteq> 0} = {k \<in> s. content k \<noteq> 0}"
- using k by auto
- ultimately show ?thesis by auto
+ using contk by auto
+ ultimately show ?case by auto
qed