--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Aug 25 23:30:36 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Aug 26 00:43:26 2017 +0100
@@ -1732,31 +1732,27 @@
then have sum_less_e2: "(\<Sum>(x,K) \<in> p'. norm (content K *\<^sub>R f x - integral K f)) < e/2"
using g(2) gp' tagged_division_of_def by blast
- have XX: "(x, I \<inter> L) \<in> p'" if "(x, L) \<in> p" "I \<in> d" "y \<in> I" "y \<in> L"
+ have "(x, I \<inter> L) \<in> p'" if x: "(x, L) \<in> p" "I \<in> d" and y: "y \<in> I" "y \<in> L"
for x I L y
proof -
have "x \<in> I"
- using fineD[OF p(3) that(1)] k(2)[OF that(2), of x] that(3-) by auto
- then have "(\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> I \<inter> L = i \<inter> l)"
- using that(1) that(2) by blast
+ using fineD[OF p(3) that(1)] k(2)[OF \<open>I \<in> d\<close>] y by auto
+ with x have "(\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> I \<inter> L = i \<inter> l)"
+ by blast
then have "(x, I \<inter> L) \<in> p'"
by (simp add: p'_def)
- then show ?thesis
- using that(3) by auto
+ with y show ?thesis by auto
qed
- have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
- proof (safe, goal_cases)
- case prems: (2 _ _ x i l)
- then show ?case
- using XX by auto
- next
- fix x K
- assume "(x, K) \<in> p'"
- then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l"
- unfolding p'_def by auto
- then show "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
+ moreover have "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
+ if xK: "(x,K) \<in> p'" for x K
+ proof -
+ obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l"
+ using xK unfolding p'_def by auto
+ then show ?thesis
using p'(2) by fastforce
qed
+ ultimately have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
+ by auto
have sum_p': "(\<Sum>(x,K) \<in> p'. norm (integral K f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
apply (subst sum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
apply (auto intro: integral_null simp: content_eq_0_interior)
@@ -2034,26 +2030,20 @@
from this[unfolded bounded_pos] obtain K where
K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
show ?case
- apply (rule_tac x="K + 1" in exI)
- apply safe
- proof -
+ proof (intro conjI impI allI exI)
fix a b :: 'n
assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
- have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> \<bar>s - ?S\<bar> < e"
+ have *: "\<And>s s1. \<lbrakk>?S - e < s1; s1 \<le> s; s < ?S + e\<rbrakk> \<Longrightarrow> \<bar>s - ?S\<bar> < e"
by arith
show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
unfolding real_norm_def
- apply (rule *[rule_format])
- apply safe
- apply (rule d)
- proof goal_cases
- case 1
+ proof (rule * [OF d])
have "(\<Sum>k\<in>d. norm (integral k f)) \<le> sum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
- apply (intro sum_mono)
- subgoal for k
- using d'(4)[of k] f_int
- by (auto simp: absolutely_integrable_on_def integral_norm_bound_integral)
- done
+ proof (intro sum_mono)
+ fix k assume "k \<in> d"
+ with d'(4) f_int show "norm (integral k f) \<le> integral k (\<lambda>x. norm (f x))"
+ by (force simp: absolutely_integrable_on_def integral_norm_bound_integral)
+ qed
also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
apply (rule integral_combine_division_bottomup[OF ddiv, symmetric])
using absolutely_integrable_on_def d'(4) f_int by blast
@@ -2065,7 +2055,8 @@
using integrable_on_subdivision[OF ddiv] f_int[of a b] unfolding absolutely_integrable_on_def
by (auto intro!: integral_subset_le)
qed
- finally show ?case .
+ finally show "(\<Sum>k\<in>d. norm (integral k f))
+ \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)" .
next
have "e/2>0"
using \<open>e > 0\<close> by auto
@@ -2101,9 +2092,7 @@
show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> ?S"
using partial_division_of_tagged_division[of p "cbox a b"] p(1)
apply (subst sum.over_tagged_division_lemma[OF p(1)])
- apply (simp add: content_eq_0_interior)
- apply (intro cSUP_upper2 D)
- apply (auto simp: tagged_partial_division_of_def)
+ apply (auto simp: content_eq_0_interior tagged_partial_division_of_def intro!: cSUP_upper2 D)
done
qed
then show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 25 23:30:36 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Aug 26 00:43:26 2017 +0100
@@ -5610,7 +5610,8 @@
note integrable_integral[OF this, unfolded has_integral[of f]]
from this[rule_format,OF *] guess dd..note dd=conjunctD2[OF this,rule_format]
note gauge_Int[OF \<open>gauge d\<close> dd(1)]
- from fine_division_exists[OF this,of u v] guess qq .
+ then obtain qq where qq: "qq tagged_division_of cbox u v" "(\<lambda>x. d x \<inter> dd x) fine qq"
+ using fine_division_exists by blast
then show ?thesis
apply (rule_tac x=qq in exI)
using dd(2)[of qq]
@@ -5674,14 +5675,15 @@
proof -
fix x l k
assume as: "(x, l) \<in> p" "(x, l) \<in> qq k" "k \<in> r"
- note qq[OF this(3)]
- note tagged_division_ofD(3,4)[OF conjunct1[OF this] as(2)]
- from this(2) guess u v by (elim exE) note uv=this
- have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto
+ then obtain u v where uv: "l = cbox u v"
+ using p'(4) by blast
+ have "l \<subseteq> k"
+ using qq[OF as(3)] tagged_division_ofD(3) \<open>(x, l) \<in> qq k\<close> by metis
+ have "l \<in> snd ` p"
+ using \<open>(x, l) \<in> p\<close> image_iff by fastforce
then have "l \<in> q" "k \<in> q" "l \<noteq> k"
using as(1,3) q(1) unfolding r_def by auto
- note q'(5)[OF this]
- then have "interior l = {}"
+ with q'(5) have "interior l = {}"
using interior_mono[OF \<open>l \<subseteq> k\<close>] by blast
then show "content l *\<^sub>R f x = 0"
unfolding uv content_eq_0_interior[symmetric] by auto
@@ -5745,45 +5747,33 @@
have "?x = norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))"
unfolding split_def sum_subtractf ..
also have "\<dots> \<le> e + k"
- apply (rule *[OF **, where ir1="sum (\<lambda>k. integral k f) r"])
- proof goal_cases
- case 1
+ proof (rule *[OF **])
have *: "k * real (card r) / (1 + real (card r)) < k"
using k by (auto simp add: field_simps)
- show ?case
- apply (rule le_less_trans[of _ "sum (\<lambda>x. k / (real (card r) + 1)) r"])
- unfolding sum_subtractf[symmetric]
- apply (rule sum_norm_le)
- apply (drule qq)
- defer
- unfolding divide_inverse sum_distrib_right[symmetric]
- unfolding divide_inverse[symmetric]
- using * apply (auto simp add: field_simps)
- done
+ have "norm (sum (sum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r - (\<Sum>k\<in>r. integral k f))
+ \<le> (\<Sum>x\<in>r. k / (real (card r) + 1))"
+ unfolding sum_subtractf[symmetric] by (force dest: qq intro!: sum_norm_le)
+ also have "... < k"
+ by (simp add: "*" add.commute mult.commute)
+ finally show "norm (sum (sum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r - (\<Sum>k\<in>r. integral k f)) < k" .
next
- case 2
- have *: "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
- apply (subst sum.reindex_nontrivial)
- apply fact
- unfolding split_paired_all snd_conv split_def o_def
+ from q(1) have [simp]: "snd ` p \<union> q = q" by auto
+ have "integral l f = 0"
+ if inp: "(x, l) \<in> p" "(y, m) \<in> p" and ne: "(x, l) \<noteq> (y, m)" and "l = m" for x l y m
proof -
- fix x l y m
- assume as: "(x, l) \<in> p" "(y, m) \<in> p" "(x, l) \<noteq> (y, m)" "l = m"
- from p'(4)[OF as(1)] guess u v by (elim exE) note uv=this
- show "integral l f = 0"
- unfolding uv
- apply (rule integral_unique)
- apply (rule has_integral_null)
- unfolding content_eq_0_interior
- using p'(5)[OF as(1-3)]
- unfolding uv as(4)[symmetric]
- apply auto
- done
- qed auto
- from q(1) have **: "snd ` p \<union> q = q" by auto
- show ?case
- unfolding integral_combine_division_topdown[OF assms(1) q(2)] * r_def
- using ** q'(1) p'(1) sum.union_disjoint [of "snd ` p" "q - snd ` p" "\<lambda>k. integral k f", symmetric]
+ obtain u v where uv: "l = cbox u v"
+ using inp p'(4) by blast
+ have "content (cbox u v) = 0"
+ unfolding content_eq_0_interior using that p(1) uv by auto
+ then show ?thesis
+ using uv by blast
+ qed
+ then have "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
+ apply (subst sum.reindex_nontrivial [OF \<open>finite p\<close>])
+ unfolding split_paired_all split_def by auto
+ then show "(\<Sum>(x, k)\<in>p. integral k f) + (\<Sum>k\<in>r. integral k f) = integral (cbox a b) f"
+ unfolding integral_combine_division_topdown[OF assms(1) q(2)] r_def
+ using q'(1) p'(1) sum.union_disjoint [of "snd ` p" "q - snd ` p", symmetric]
by simp
qed
finally show "?x \<le> e + k" .