--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Aug 24 10:47:56 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Aug 24 12:45:46 2017 +0100
@@ -253,26 +253,25 @@
lemma has_integral:
"(f has_integral y) (cbox a b) \<longleftrightarrow>
- (\<forall>e>0. \<exists>d. gauge d \<and>
- (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
- norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
+ (\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
+ (\<forall>\<D>. \<D> tagged_division_of (cbox a b) \<and> \<gamma> fine \<D> \<longrightarrow>
+ norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) \<D> - y) < e))"
by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff)
lemma has_integral_real:
"(f has_integral y) {a..b::real} \<longleftrightarrow>
- (\<forall>e>0. \<exists>d. gauge d \<and>
- (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
- norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
- unfolding box_real[symmetric]
- by (rule has_integral)
+ (\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
+ (\<forall>\<D>. \<D> tagged_division_of {a..b} \<and> \<gamma> fine \<D> \<longrightarrow>
+ norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) \<D> - y) < e))"
+ unfolding box_real[symmetric] by (rule has_integral)
lemma has_integralD[dest]:
assumes "(f has_integral y) (cbox a b)"
and "e > 0"
- obtains d
- where "gauge d"
- and "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d fine p \<Longrightarrow>
- norm ((\<Sum>(x,k)\<in>p. content k *\<^sub>R f x) - y) < e"
+ obtains \<gamma>
+ where "gauge \<gamma>"
+ and "\<And>\<D>. \<D> tagged_division_of (cbox a b) \<Longrightarrow> \<gamma> fine \<D> \<Longrightarrow>
+ norm ((\<Sum>(x,k)\<in>\<D>. content k *\<^sub>R f x) - y) < e"
using assms unfolding has_integral by auto
lemma has_integral_alt:
@@ -914,28 +913,28 @@
subsection \<open>Cauchy-type criterion for integrability.\<close>
-lemma integrable_Cauchy:
+proposition integrable_Cauchy:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::{real_normed_vector,complete_space}"
shows "f integrable_on cbox a b \<longleftrightarrow>
(\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
- (\<forall>p1 p2. p1 tagged_division_of (cbox a b) \<and> \<gamma> fine p1 \<and>
- p2 tagged_division_of (cbox a b) \<and> \<gamma> fine p2 \<longrightarrow>
- norm ((\<Sum>(x,K)\<in>p1. content K *\<^sub>R f x) - (\<Sum>(x,K)\<in>p2. content K *\<^sub>R f x)) < e))"
+ (\<forall>\<D>1 \<D>2. \<D>1 tagged_division_of (cbox a b) \<and> \<gamma> fine \<D>1 \<and>
+ \<D>2 tagged_division_of (cbox a b) \<and> \<gamma> fine \<D>2 \<longrightarrow>
+ norm ((\<Sum>(x,K)\<in>\<D>1. content K *\<^sub>R f x) - (\<Sum>(x,K)\<in>\<D>2. content K *\<^sub>R f x)) < e))"
(is "?l = (\<forall>e>0. \<exists>\<gamma>. ?P e \<gamma>)")
proof (intro iffI allI impI)
assume ?l
then obtain y
where y: "\<And>e. e > 0 \<Longrightarrow>
\<exists>\<gamma>. gauge \<gamma> \<and>
- (\<forall>p. p tagged_division_of cbox a b \<and> \<gamma> fine p \<longrightarrow>
- norm ((\<Sum>(x,K) \<in> p. content K *\<^sub>R f x) - y) < e)"
+ (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
+ norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - y) < e)"
by (auto simp: integrable_on_def has_integral)
show "\<exists>\<gamma>. ?P e \<gamma>" if "e > 0" for e
proof -
have "e/2 > 0" using that by auto
with y obtain \<gamma> where "gauge \<gamma>"
- and \<gamma>: "\<And>p. p tagged_division_of cbox a b \<and> \<gamma> fine p \<Longrightarrow>
- norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - y) < e/2"
+ and \<gamma>: "\<And>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<Longrightarrow>
+ norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f x) - y) < e/2"
by meson
show ?thesis
apply (rule_tac x=\<gamma> in exI, clarsimp simp: \<open>gauge \<gamma>\<close>)
@@ -947,9 +946,9 @@
by auto
then obtain \<gamma> :: "nat \<Rightarrow> 'n \<Rightarrow> 'n set" where \<gamma>:
"\<And>m. gauge (\<gamma> m)"
- "\<And>m p1 p2. \<lbrakk>p1 tagged_division_of cbox a b;
- \<gamma> m fine p1; p2 tagged_division_of cbox a b; \<gamma> m fine p2\<rbrakk>
- \<Longrightarrow> norm ((\<Sum>(x,K) \<in> p1. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> p2. content K *\<^sub>R f x))
+ "\<And>m \<D>1 \<D>2. \<lbrakk>\<D>1 tagged_division_of cbox a b;
+ \<gamma> m fine \<D>1; \<D>2 tagged_division_of cbox a b; \<gamma> m fine \<D>2\<rbrakk>
+ \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>1. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> \<D>2. content K *\<^sub>R f x))
< 1 / (m + 1)"
by metis
have "\<And>n. gauge (\<lambda>x. \<Inter>{\<gamma> i x |i. i \<in> {0..n}})"
@@ -993,8 +992,8 @@
obtain N2::nat where N2: "\<And>n. n \<ge> N2 \<Longrightarrow> norm ((\<Sum>(x,K) \<in> p n. content K *\<^sub>R f x) - y) < e/2"
using y[OF e2] by metis
show "\<exists>\<gamma>. gauge \<gamma> \<and>
- (\<forall>p. p tagged_division_of (cbox a b) \<and> \<gamma> fine p \<longrightarrow>
- norm ((\<Sum>(x,K) \<in> p. content K *\<^sub>R f x) - y) < e)"
+ (\<forall>\<D>. \<D> tagged_division_of (cbox a b) \<and> \<gamma> fine \<D> \<longrightarrow>
+ norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - y) < e)"
proof (intro exI conjI allI impI)
show "gauge (\<gamma> (N1+N2))"
using \<gamma> by auto
@@ -1059,15 +1058,15 @@
by auto
obtain \<gamma>1 where \<gamma>1: "gauge \<gamma>1"
and \<gamma>1norm:
- "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c}; \<gamma>1 fine p\<rbrakk>
- \<Longrightarrow> norm ((\<Sum>(x,K) \<in> p. content K *\<^sub>R f x) - i) < e/2"
+ "\<And>\<D>. \<lbrakk>\<D> tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c}; \<gamma>1 fine \<D>\<rbrakk>
+ \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - i) < e/2"
apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e])
apply (simp add: interval_split[symmetric] k)
done
obtain \<gamma>2 where \<gamma>2: "gauge \<gamma>2"
and \<gamma>2norm:
- "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k}; \<gamma>2 fine p\<rbrakk>
- \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - j) < e/2"
+ "\<And>\<D>. \<lbrakk>\<D> tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k}; \<gamma>2 fine \<D>\<rbrakk>
+ \<Longrightarrow> norm ((\<Sum>(x, k) \<in> \<D>. content k *\<^sub>R f x) - j) < e/2"
apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e])
apply (simp add: interval_split[symmetric] k)
done
@@ -1075,8 +1074,8 @@
have "gauge ?\<gamma>"
using \<gamma>1 \<gamma>2 unfolding gauge_def by auto
then show "\<exists>\<gamma>. gauge \<gamma> \<and>
- (\<forall>p. p tagged_division_of cbox a b \<and> \<gamma> fine p \<longrightarrow>
- norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (i + j)) < e)"
+ (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
+ norm ((\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R f x) - (i + j)) < e)"
proof (rule_tac x="?\<gamma>" in exI, safe)
fix p
assume p: "p tagged_division_of (cbox a b)" and "?\<gamma> fine p"
@@ -1285,7 +1284,7 @@
note p1=tagged_division_ofD[OF this(1)]
assume tdiv2: "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> k}" and "\<gamma> fine p2"
note p2=tagged_division_ofD[OF this(1)]
- note tagged_division_union_interval[OF tdiv1 tdiv2]
+ note tagged_division_Un_interval[OF tdiv1 tdiv2]
note p12 = tagged_division_ofD[OF this] this
{ fix a b
assume ab: "(a, b) \<in> p1 \<inter> p2"
@@ -4140,7 +4139,7 @@
using as by (auto simp add: field_simps)
have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
- apply (rule tagged_division_union_interval_real[of _ _ _ 1 "t"])
+ apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
using \<open>t \<le> c\<close> by (auto simp: * ptag tagged_division_of_self_real)
moreover
have "d1 fine p \<union> {(c, {t..c})}"
@@ -4762,9 +4761,9 @@
lemma has_integral_le:
fixes f :: "'n::euclidean_space \<Rightarrow> real"
- assumes "(f has_integral i) s"
- and "(g has_integral j) s"
- and "\<forall>x\<in>s. f x \<le> g x"
+ assumes "(f has_integral i) S"
+ and "(g has_integral j) S"
+ and "\<And>x. x \<in> S \<Longrightarrow> f x \<le> g x"
shows "i \<le> j"
using has_integral_component_le[OF _ assms(1-2), of 1]
using assms(3)
@@ -4772,27 +4771,27 @@
lemma integral_le:
fixes f :: "'n::euclidean_space \<Rightarrow> real"
- assumes "f integrable_on s"
- and "g integrable_on s"
- and "\<forall>x\<in>s. f x \<le> g x"
- shows "integral s f \<le> integral s g"
+ assumes "f integrable_on S"
+ and "g integrable_on S"
+ and "\<And>x. x \<in> S \<Longrightarrow> f x \<le> g x"
+ shows "integral S f \<le> integral S g"
by (rule has_integral_le[OF assms(1,2)[unfolded has_integral_integral] assms(3)])
lemma has_integral_nonneg:
fixes f :: "'n::euclidean_space \<Rightarrow> real"
- assumes "(f has_integral i) s"
- and "\<forall>x\<in>s. 0 \<le> f x"
+ assumes "(f has_integral i) S"
+ and "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
shows "0 \<le> i"
- using has_integral_component_nonneg[of 1 f i s]
+ using has_integral_component_nonneg[of 1 f i S]
unfolding o_def
using assms
by auto
lemma integral_nonneg:
fixes f :: "'n::euclidean_space \<Rightarrow> real"
- assumes "f integrable_on s"
- and "\<forall>x\<in>s. 0 \<le> f x"
- shows "0 \<le> integral s f"
+ assumes "f integrable_on S"
+ and "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
+ shows "0 \<le> integral S f"
by (rule has_integral_nonneg[OF assms(1)[unfolded has_integral_integral] assms(2)])
@@ -5686,9 +5685,9 @@
subsection \<open>Henstock's lemma\<close>
-lemma henstock_lemma_part1:
+lemma Henstock_lemma_part1:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
- assumes "f integrable_on cbox a b"
+ assumes intf: "f integrable_on cbox a b"
and "e > 0"
and "gauge d"
and less_e: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d fine p\<rbrakk> \<Longrightarrow>
@@ -5711,59 +5710,52 @@
have r: "finite r"
using q' unfolding r_def by auto
- have "\<forall>i\<in>r. \<exists>p. p tagged_division_of i \<and> d fine p \<and>
- norm (sum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
- apply safe
- proof goal_cases
- case (1 i)
- then have i: "i \<in> q"
- unfolding r_def by auto
- from q'(4)[OF this] guess u v by (elim exE) note uv=this
+ have "\<exists>p. p tagged_division_of i \<and> d fine p \<and>
+ norm (sum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
+ if "i\<in>r" for i
+ proof -
have *: "k / (real (card r) + 1) > 0" using k by simp
- have "f integrable_on cbox u v"
- apply (rule integrable_subinterval[OF assms(1)])
- using q'(2)[OF i]
- unfolding uv
- apply auto
- done
+ have i: "i \<in> q"
+ using that unfolding r_def by auto
+ then obtain u v where uv: "i = cbox u v"
+ using q'(4) by blast
+ then have "cbox u v \<subseteq> cbox a b"
+ using i q'(2) by auto
+ then have "f integrable_on cbox u v"
+ by (rule integrable_subinterval[OF intf])
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 show ?case
+ then show ?thesis
apply (rule_tac x=qq in exI)
using dd(2)[of qq]
unfolding fine_Int uv
apply auto
done
qed
- from bchoice[OF this] guess qq..note qq=this[rule_format]
+ then obtain qq where qq: "\<And>i. i \<in> r \<Longrightarrow> qq i tagged_division_of i \<and>
+ d fine qq i \<and>
+ norm
+ ((\<Sum>(x, j) \<in> qq i. content j *\<^sub>R f x) -
+ integral i f)
+ < k / (real (card r) + 1)"
+ by metis
let ?p = "p \<union> \<Union>(qq ` r)"
have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral (cbox a b) f) < e"
proof (rule less_e)
show "d fine ?p"
by (metis (mono_tags, hide_lams) qq fine_Un fine_Union imageE p(2))
- note * = tagged_partial_division_of_union_self[OF p(1)]
+ note * = tagged_partial_division_of_Union_self[OF p(1)]
have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
using r
- proof (rule tagged_division_union[OF * tagged_division_unions], goal_cases)
- case 1
- then show ?case
+ proof (rule tagged_division_Un[OF * tagged_division_Union])
+ show "\<And>i. i \<in> r \<Longrightarrow> qq i tagged_division_of i"
using qq by auto
- next
- case 2
- then show ?case
- apply rule
- apply rule
- apply rule
- apply(rule q'(5))
- unfolding r_def
- apply auto
- done
- next
- case 3
- then show ?case
+ show "\<And>i1 i2. \<lbrakk>i1 \<in> r; i2 \<in> r; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior i1 \<inter> interior i2 = {}"
+ by (simp add: q'(5) r_def)
+ show "interior (UNION p snd) \<inter> interior (\<Union>r) = {}"
proof (rule Int_interior_Union_intervals [OF \<open>finite r\<close>])
show "open (interior (UNION p snd))"
by blast
@@ -5780,9 +5772,7 @@
qed
qed
moreover have "\<Union>(snd ` p) \<union> \<Union>r = cbox a b" and "{qq i |i. i \<in> r} = qq ` r"
- unfolding Union_Un_distrib[symmetric] r_def
- using q
- by auto
+ using q unfolding Union_Un_distrib[symmetric] r_def by auto
ultimately show "?p tagged_division_of (cbox a b)"
by fastforce
qed
@@ -5915,11 +5905,11 @@
finally show "?x \<le> e + k" .
qed
-lemma henstock_lemma_part2:
+lemma Henstock_lemma_part2:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
assumes fed: "f integrable_on cbox a b" "e > 0" "gauge d"
- and less_e: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d fine p\<rbrakk> \<Longrightarrow>
- norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral (cbox a b) f) < e"
+ and less_e: "\<And>\<D>. \<lbrakk>\<D> tagged_division_of (cbox a b); d fine \<D>\<rbrakk> \<Longrightarrow>
+ norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) \<D> - integral (cbox a b) f) < e"
and tag: "p tagged_partial_division_of (cbox a b)"
and "d fine p"
shows "sum (\<lambda>(x,k). norm (content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (DIM('n)) * e"
@@ -5934,13 +5924,13 @@
then have fine: "d fine Q"
by (simp add: \<open>d fine p\<close> fine_subset)
show "norm (\<Sum>x\<in>Q. content (snd x) *\<^sub>R f (fst x) - integral (snd x) f) \<le> e"
- apply (rule henstock_lemma_part1[OF fed less_e, unfolded split_def])
+ apply (rule Henstock_lemma_part1[OF fed less_e, unfolded split_def])
using Q tag tagged_partial_division_subset apply (force simp add: fine)+
done
qed
qed
-lemma henstock_lemma:
+lemma Henstock_lemma:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
assumes intf: "f integrable_on cbox a b"
and "e > 0"
@@ -5951,8 +5941,8 @@
have *: "e/(2 * (real DIM('n) + 1)) > 0" using \<open>e > 0\<close> by simp
with integrable_integral[OF intf, unfolded has_integral]
obtain \<gamma> where "gauge \<gamma>"
- and \<gamma>: "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma> fine p\<rbrakk> \<Longrightarrow>
- norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral (cbox a b) f)
+ and \<gamma>: "\<And>\<D>. \<lbrakk>\<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk> \<Longrightarrow>
+ norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f x) - integral (cbox a b) f)
< e/(2 * (real DIM('n) + 1))"
by metis
show thesis
@@ -5961,7 +5951,7 @@
assume p: "p tagged_partial_division_of cbox a b" "\<gamma> fine p"
have "(\<Sum>(x,K)\<in>p. norm (content K *\<^sub>R f x - integral K f))
\<le> 2 * real DIM('n) * (e/(2 * (real DIM('n) + 1)))"
- using henstock_lemma_part2[OF intf * \<open>gauge \<gamma>\<close> \<gamma> p] by metis
+ using Henstock_lemma_part2[OF intf * \<open>gauge \<gamma>\<close> \<gamma> p] by metis
also have "... < e"
using \<open>e > 0\<close> by (auto simp add: field_simps)
finally
@@ -5972,14 +5962,12 @@
subsection \<open>Monotone convergence (bounded interval first)\<close>
-(* TODO: is this lemma necessary? *)
lemma bounded_increasing_convergent:
fixes f :: "nat \<Rightarrow> real"
shows "\<lbrakk>bounded (range f); \<And>n. f n \<le> f (Suc n)\<rbrakk> \<Longrightarrow> \<exists>l. f \<longlonglongrightarrow> l"
using Bseq_mono_convergent[of f] incseq_Suc_iff[of f]
by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def)
-(*FIXME: why so much " \<bullet> 1"? *)
lemma monotone_convergence_interval:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
assumes intf: "\<And>k. (f k) integrable_on cbox a b"
@@ -5988,57 +5976,53 @@
and bou: "bounded (range (\<lambda>k. integral (cbox a b) (f k)))"
shows "g integrable_on cbox a b \<and> ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> integral (cbox a b) g) sequentially"
proof (cases "content (cbox a b) = 0")
- case True
- then show ?thesis
+ case True then show ?thesis
by auto
next
case False
- have fg1: "(f k x) \<bullet> 1 \<le> (g x) \<bullet> 1" if x: "x \<in> cbox a b" for x k
+ have fg1: "(f k x) \<le> (g x)" if x: "x \<in> cbox a b" for x k
proof -
- have "\<forall>\<^sub>F xa in sequentially. f k x \<bullet> 1 \<le> f xa x \<bullet> 1"
- unfolding eventually_sequentially
- apply (rule_tac x=k in exI)
+ have "\<forall>\<^sub>F j in sequentially. f k x \<le> f j x"
+ apply (rule eventually_sequentiallyI [of k])
using le x apply (force intro: transitive_stepwise_le)
done
- with Lim_component_ge [OF fg] x
- show "f k x \<bullet> 1 \<le> g x \<bullet> 1"
- using trivial_limit_sequentially by blast
+ then show "f k x \<le> g x"
+ using tendsto_lowerbound [OF fg] x trivial_limit_sequentially by blast
qed
have int_inc: "\<And>n. integral (cbox a b) (f n) \<le> integral (cbox a b) (f (Suc n))"
- by (metis integral_le assms(1-2))
+ by (metis integral_le intf le)
then obtain i where i: "(\<lambda>k. integral (cbox a b) (f k)) \<longlonglongrightarrow> i"
using bounded_increasing_convergent bou by blast
- have "\<And>k. \<forall>\<^sub>F x in sequentially. integral (cbox a b) (f k) \<le> integral (cbox a b) (f x) \<bullet> 1"
+ have "\<And>k. \<forall>\<^sub>F x in sequentially. integral (cbox a b) (f k) \<le> integral (cbox a b) (f x)"
unfolding eventually_sequentially
by (force intro: transitive_stepwise_le int_inc)
- then have i': "\<And>k. (integral(cbox a b) (f k)) \<le> i\<bullet>1"
- using Lim_component_ge [OF i] trivial_limit_sequentially by blast
+ then have i': "\<And>k. (integral(cbox a b) (f k)) \<le> i"
+ using tendsto_le [OF trivial_limit_sequentially i] by blast
have "(g has_integral i) (cbox a b)"
unfolding has_integral real_norm_def
proof clarify
fix e::real
assume e: "e > 0"
- have "\<And>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
- abs ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e/2 ^ (k + 2)))"
+ have "\<And>k. (\<exists>\<gamma>. gauge \<gamma> \<and> (\<forall>\<D>. \<D> tagged_division_of (cbox a b) \<and> \<gamma> fine \<D> \<longrightarrow>
+ abs ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f k x) - integral (cbox a b) (f k)) < e/2 ^ (k + 2)))"
using intf e by (auto simp: has_integral_integral has_integral)
- then obtain c where c:
- "\<And>x. gauge (c x)"
- "\<And>x p. \<lbrakk>p tagged_division_of cbox a b; c x fine p\<rbrakk> \<Longrightarrow>
- abs ((\<Sum>(u, ka)\<in>p. content ka *\<^sub>R f x u) - integral (cbox a b) (f x))
+ then obtain c where c: "\<And>x. gauge (c x)"
+ "\<And>x \<D>. \<lbrakk>\<D> tagged_division_of cbox a b; c x fine \<D>\<rbrakk> \<Longrightarrow>
+ abs ((\<Sum>(u,K)\<in>\<D>. content K *\<^sub>R f x u) - integral (cbox a b) (f x))
< e/2 ^ (x + 2)"
by metis
- have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i\<bullet>1 - (integral (cbox a b) (f k)) \<and> i\<bullet>1 - (integral (cbox a b) (f k)) < e/4"
+ have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i - (integral (cbox a b) (f k)) \<and> i - (integral (cbox a b) (f k)) < e/4"
proof -
have "e/4 > 0"
using e by auto
show ?thesis
using LIMSEQ_D [OF i \<open>e/4 > 0\<close>] i' by auto
qed
- then obtain r where r: "\<And>k. r \<le> k \<Longrightarrow> 0 \<le> i \<bullet> 1 - integral (cbox a b) (f k)"
- "\<And>k. r \<le> k \<Longrightarrow> i \<bullet> 1 - integral (cbox a b) (f k) < e/4"
+ then obtain r where r: "\<And>k. r \<le> k \<Longrightarrow> 0 \<le> i - integral (cbox a b) (f k)"
+ "\<And>k. r \<le> k \<Longrightarrow> i - integral (cbox a b) (f k) < e/4"
by metis
- have "\<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)\<bullet>1 - (f k x)\<bullet>1 \<and> (g x)\<bullet>1 - (f k x)\<bullet>1 < e/(4 * content(cbox a b))"
+ have "\<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x) - (f k x) \<and> (g x) - (f k x) < e/(4 * content(cbox a b))"
if "x \<in> cbox a b" for x
proof -
have "e/(4 * content (cbox a b)) > 0"
@@ -6048,8 +6032,8 @@
by metis
then show "\<exists>n\<ge>r.
\<forall>k\<ge>n.
- 0 \<le> g x \<bullet> 1 - f k x \<bullet> 1 \<and>
- g x \<bullet> 1 - f k x \<bullet> 1
+ 0 \<le> g x - f k x \<and>
+ g x - f k x
< e/(4 * content (cbox a b))"
apply (rule_tac x="N + r" in exI)
using fg1[OF that] apply (auto simp add: field_simps)
@@ -6057,127 +6041,119 @@
qed
then obtain m where r_le_m: "\<And>x. x \<in> cbox a b \<Longrightarrow> r \<le> m x"
and m: "\<And>x k. \<lbrakk>x \<in> cbox a b; m x \<le> k\<rbrakk>
- \<Longrightarrow> 0 \<le> g x \<bullet> 1 - f k x \<bullet> 1 \<and> g x \<bullet> 1 - f k x \<bullet> 1 < e/(4 * content (cbox a b))"
+ \<Longrightarrow> 0 \<le> g x - f k x \<and> g x - f k x < e/(4 * content (cbox a b))"
by metis
define d where "d x = c (m x) x" for x
show "\<exists>\<gamma>. gauge \<gamma> \<and>
- (\<forall>p. p tagged_division_of cbox a b \<and>
- \<gamma> fine p \<longrightarrow> abs ((\<Sum>(x,K)\<in>p. content K *\<^sub>R g x) - i) < e)"
+ (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and>
+ \<gamma> fine \<D> \<longrightarrow> abs ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - i) < e)"
proof (rule exI, safe)
show "gauge d"
using c(1) unfolding gauge_def d_def by auto
next
- fix p
- assume p: "p tagged_division_of (cbox a b)" "d fine p"
- note p'=tagged_division_ofD[OF p(1)]
- obtain s where s: "\<And>x. x \<in> p \<Longrightarrow> m (fst x) \<le> s"
+ fix \<D>
+ assume ptag: "\<D> tagged_division_of (cbox a b)" and "d fine \<D>"
+ note p'=tagged_division_ofD[OF ptag]
+ obtain s where s: "\<And>x. x \<in> \<D> \<Longrightarrow> m (fst x) \<le> s"
by (metis finite_imageI finite_nat_set_iff_bounded_le p'(1) rev_image_eqI)
have *: "\<bar>a - d\<bar> < e" if "\<bar>a - b\<bar> \<le> e/4" "\<bar>b - c\<bar> < e/2" "\<bar>c - d\<bar> < e/4" for a b c d
using that norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
norm_triangle_lt[of "a - b + (b - c)" "c - d" e]
by (auto simp add: algebra_simps)
- show "abs ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e"
+ show "\<bar>(\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R g x) - i\<bar> < e"
proof (rule *)
- show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - (\<Sum>(x, K)\<in>p. content K *\<^sub>R f (m x) x)\<bar>
- \<le> e/4"
- apply (rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e/(4 * content (cbox a b)))"])
- unfolding sum_subtractf[symmetric]
- apply (rule order_trans)
- apply (rule sum_abs)
- apply (rule sum_mono)
- unfolding split_paired_all split_conv
- unfolding split_def sum_distrib_right[symmetric] scaleR_diff_right[symmetric]
- unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
- proof -
+ have "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x)\<bar>
+ \<le> (\<Sum>i\<in>\<D>. \<bar>(case i of (x, K) \<Rightarrow> content K *\<^sub>R g x) - (case i of (x, K) \<Rightarrow> content K *\<^sub>R f (m x) x)\<bar>)"
+ by (metis (mono_tags) sum_subtractf sum_abs)
+ also have "... \<le> (\<Sum>(x, k)\<in>\<D>. content k * (e/(4 * content (cbox a b))))"
+ proof (rule sum_mono, simp add: split_paired_all)
fix x K
- assume xk: "(x, K) \<in> p"
- then have x: "x \<in> cbox a b"
- using p'(2-3)[OF xk] by auto
- with p'(4)[OF xk] obtain u v where "K = cbox u v" by metis
- then show "abs (content K *\<^sub>R (g x - f (m x) x)) \<le> content K * (e/(4 * content (cbox a b)))"
- unfolding abs_scaleR using m[OF x]
- by (metis real_inner_1_right real_scaleR_def abs_of_nonneg inner_real_def less_eq_real_def measure_nonneg mult_left_mono order_refl)
- qed (insert False, auto)
+ assume xk: "(x,K) \<in> \<D>"
+ with ptag have x: "x \<in> cbox a b"
+ by blast
+ then have "abs (content K * (g x - f (m x) x)) \<le> content K * (e/(4 * content (cbox a b)))"
+ by (metis m[OF x] mult_nonneg_nonneg abs_of_nonneg less_eq_real_def measure_nonneg mult_left_mono order_refl)
+ then show "\<bar>content K * g x - content K * f (m x) x\<bar> \<le> content K * e / (4 * content (cbox a b))"
+ by (simp add: algebra_simps)
+ qed
+ also have "... = (e / (4 * content (cbox a b))) * (\<Sum>(x, k)\<in>\<D>. content k)"
+ by (simp add: sum_distrib_left sum_divide_distrib split_def mult.commute)
+ also have "... \<le> e/4"
+ by (metis False additive_content_tagged_division [OF ptag] nonzero_mult_divide_mult_cancel_right order_refl times_divide_eq_left)
+ finally show "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x)\<bar> \<le> e/4" .
next
- have "norm ((\<Sum>(x, K)\<in>p. content K *\<^sub>R f (m x) x) - (\<Sum>(x, k)\<in>p. integral k (f (m x))))
- \<le> norm
- (\<Sum>j = 0..s.
- \<Sum>(x, K)\<in>{xk \<in> p. m (fst xk) = j}.
- content K *\<^sub>R f (m x) x - integral K (f (m x)))"
+ have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>\<D>. integral K (f (m x))))
+ \<le> norm (\<Sum>j = 0..s. \<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = j}. content K *\<^sub>R f (m x) x - integral K (f (m x)))"
apply (subst sum_group)
using s by (auto simp: sum_subtractf split_def p'(1))
also have "\<dots> < e/2"
proof -
- have "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))
+ have "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> \<D>. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))
\<le> (\<Sum>i = 0..s. e/2 ^ (i + 2))"
proof (rule sum_norm_le)
fix t
assume "t \<in> {0..s}"
- have "norm (\<Sum>(x,k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - integral k (f (m x))) =
- norm (\<Sum>(x,k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f t x - integral k (f t))"
+ have "norm (\<Sum>(x,k)\<in>{xk \<in> \<D>. m (fst xk) = t}. content k *\<^sub>R f (m x) x - integral k (f (m x))) =
+ norm (\<Sum>(x,k)\<in>{xk \<in> \<D>. m (fst xk) = t}. content k *\<^sub>R f t x - integral k (f t))"
by (force intro!: sum.cong arg_cong[where f=norm])
also have "... \<le> e/2 ^ (t + 2)"
- proof (rule henstock_lemma_part1 [OF intf])
- show "{xk \<in> p. m (fst xk) = t} tagged_partial_division_of cbox a b"
- apply (rule tagged_partial_division_subset[of p])
- using p by (auto simp: tagged_division_of_def)
- show "c t fine {xk \<in> p. m (fst xk) = t}"
- using p(2) by (auto simp: fine_def d_def)
+ proof (rule Henstock_lemma_part1 [OF intf])
+ show "{xk \<in> \<D>. m (fst xk) = t} tagged_partial_division_of cbox a b"
+ apply (rule tagged_partial_division_subset[of \<D>])
+ using ptag by (auto simp: tagged_division_of_def)
+ show "c t fine {xk \<in> \<D>. m (fst xk) = t}"
+ using \<open>d fine \<D>\<close> by (auto simp: fine_def d_def)
qed (use c e in auto)
- finally show "norm (\<Sum>(x,K)\<in>{xk \<in> p. m (fst xk) = t}. content K *\<^sub>R f (m x) x -
+ finally show "norm (\<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = t}. content K *\<^sub>R f (m x) x -
integral K (f (m x))) \<le> e/2 ^ (t + 2)" .
qed
also have "... = (e/2/2) * (\<Sum>i = 0..s. (1/2) ^ i)"
by (simp add: sum_distrib_left field_simps)
also have "\<dots> < e/2"
by (simp add: sum_gp mult_strict_left_mono[OF _ e])
- finally show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p.
+ finally show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> \<D>.
m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e/2" .
qed
- finally show "\<bar>(\<Sum>(x,K)\<in>p. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>p. integral K (f (m x)))\<bar> < e/2"
+ finally show "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>\<D>. integral K (f (m x)))\<bar> < e/2"
by simp
next
- note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)]
- have *: "\<And>sr sx ss ks kr. \<lbrakk>kr = sr; ks = ss;
- ks \<le> i; sr \<le> sx; sx \<le> ss; 0 \<le> i\<bullet>1 - kr\<bullet>1; i\<bullet>1 - kr\<bullet>1 < e/4\<rbrakk> \<Longrightarrow> \<bar>sx - i\<bar> < e/4"
- by auto
- show "\<bar>(\<Sum>(x, k)\<in>p. integral k (f (m x))) - i\<bar> < e/4"
- unfolding real_norm_def
- apply (rule *)
- apply (rule comb[of r])
- apply (rule comb[of s])
- apply (rule i'[unfolded real_inner_1_right])
- apply (rule_tac[1-2] sum_mono)
- unfolding split_paired_all split_conv
- apply (rule_tac[1-2] integral_le[OF ])
- proof safe
- show "0 \<le> i\<bullet>1 - (integral (cbox a b) (f r))\<bullet>1" "i\<bullet>1 - (integral (cbox a b) (f r))\<bullet>1 < e/4"
- using r by auto
+ have comb: "integral (cbox a b) (f y) = (\<Sum>(x, k)\<in>\<D>. integral k (f y))" for y
+ using integral_combine_tagged_division_topdown[OF intf ptag] by metis
+ have f_le: "\<And>y m n. \<lbrakk>y \<in> cbox a b; n\<ge>m\<rbrakk> \<Longrightarrow> f m y \<le> f n y"
+ using le by (auto intro: transitive_stepwise_le)
+ have "(\<Sum>(x, k)\<in>\<D>. integral k (f r)) \<le> (\<Sum>(x, K)\<in>\<D>. integral K (f (m x)))"
+ proof (rule sum_mono, simp add: split_paired_all)
fix x K
- assume xk: "(x, K) \<in> p"
- from p'(4)[OF this] guess u v by (elim exE) note uv=this
- show "f r integrable_on K"
- and "f s integrable_on K"
- and "f (m x) integrable_on K"
- and "f (m x) integrable_on K"
- unfolding uv
- apply (rule_tac[!] integrable_on_subcbox[OF assms(1)[rule_format]])
- using p'(3)[OF xk]
- unfolding uv
- apply auto
- done
- fix y
- assume "y \<in> K"
- then have "y \<in> cbox a b"
- using p'(3)[OF xk] by auto
- then have *: "\<And>m n. n\<ge>m \<Longrightarrow> f m y \<le> f n y"
- using assms(2) by (auto intro: transitive_stepwise_le)
- show "f r y \<le> f (m x) y" "f (m x) y \<le> f s y"
- using s[rule_format,OF xk] r_le_m[of x] p'(2-3)[OF xk]
- apply (auto intro!: *)
- done
+ assume xK: "(x, K) \<in> \<D>"
+ show "integral K (f r) \<le> integral K (f (m x))"
+ proof (rule integral_le)
+ show "f r integrable_on K"
+ by (metis integrable_on_subcbox intf p'(3) p'(4) xK)
+ show "f (m x) integrable_on K"
+ by (metis elementary_interval integrable_on_subdivision intf p'(3) p'(4) xK)
+ show "f r y \<le> f (m x) y" if "y \<in> K" for y
+ using that r_le_m[of x] p'(2-3)[OF xK] f_le by auto
+ qed
qed
+ moreover have "(\<Sum>(x, K)\<in>\<D>. integral K (f (m x))) \<le> (\<Sum>(x, k)\<in>\<D>. integral k (f s))"
+ proof (rule sum_mono, simp add: split_paired_all)
+ fix x K
+ assume xK: "(x, K) \<in> \<D>"
+ show "integral K (f (m x)) \<le> integral K (f s)"
+ proof (rule integral_le)
+ show "f (m x) integrable_on K"
+ by (metis elementary_interval integrable_on_subdivision intf p'(3) p'(4) xK)
+ show "f s integrable_on K"
+ by (metis integrable_on_subcbox intf p'(3) p'(4) xK)
+ show "f (m x) y \<le> f s y" if "y \<in> K" for y
+ using that s xK f_le p'(3) by fastforce
+ qed
+ qed
+ moreover have "0 \<le> i - integral (cbox a b) (f r)" "i - integral (cbox a b) (f r) < e / 4"
+ using r by auto
+ ultimately show "\<bar>(\<Sum>(x,K)\<in>\<D>. integral K (f (m x))) - i\<bar> < e/4"
+ using comb i'[of s] by auto
qed
qed
qed
@@ -6201,23 +6177,19 @@
and bou: "bounded (range(\<lambda>k. integral S (f k)))"
for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g S
proof -
- have fg: "(f k x)\<bullet>1 \<le> (g x)\<bullet>1" if "x \<in> S" for x k
- apply (rule Lim_component_ge [OF lim [OF that] trivial_limit_sequentially])
- unfolding eventually_sequentially
- apply (rule_tac x=k in exI)
- using le by (force intro: transitive_stepwise_le that)
-
+ have fg: "(f k x) \<le> (g x)" if "x \<in> S" for x k
+ apply (rule tendsto_lowerbound [OF lim [OF that]])
+ apply (rule eventually_sequentiallyI [of k])
+ using le by (force intro: transitive_stepwise_le that)+
obtain i where i: "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> i"
using bounded_increasing_convergent [OF bou] le int_f integral_le by blast
- have i': "(integral S (f k))\<bullet>1 \<le> i\<bullet>1" for k
+ have i': "(integral S (f k)) \<le> i" for k
proof -
- have *: "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
+ have "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
using le by (force intro: transitive_stepwise_le)
- show ?thesis
- apply (rule Lim_component_ge [OF i trivial_limit_sequentially])
- unfolding eventually_sequentially
- apply (rule_tac x=k in exI)
- using * by (simp add: int_f integral_le)
+ then show ?thesis
+ using tendsto_lowerbound [OF i eventually_sequentiallyI trivial_limit_sequentially]
+ by (meson int_f integral_le)
qed
let ?f = "(\<lambda>k x. if x \<in> S then f k x else 0)"
@@ -6277,7 +6249,7 @@
show "integral (cbox a b) (?f N) \<le> integral (cbox a b) (?f (M + N))"
proof (intro ballI integral_le[OF int int])
fix x assume "x \<in> cbox a b"
- have "(f m x)\<bullet>1 \<le> (f n x)\<bullet>1" if "x \<in> S" "n \<ge> m" for m n
+ have "(f m x) \<le> (f n x)" if "x \<in> S" "n \<ge> m" for m n
apply (rule transitive_stepwise_le [OF \<open>n \<ge> m\<close> order_refl])
using dual_order.trans apply blast
by (simp add: le \<open>x \<in> S\<close>)
@@ -6416,41 +6388,41 @@
by auto
with integrable_integral[OF f,unfolded has_integral[of f]]
obtain \<gamma> where \<gamma>: "gauge \<gamma>"
- "\<And>p. p tagged_division_of cbox a b \<and> \<gamma> fine p
- \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral (cbox a b) f) < e/2"
+ "\<And>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D>
+ \<Longrightarrow> norm ((\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R f x) - integral (cbox a b) f) < e/2"
by meson
moreover
from integrable_integral[OF g,unfolded has_integral[of g]] e
obtain \<delta> where \<delta>: "gauge \<delta>"
- "\<And>p. p tagged_division_of cbox a b \<and> \<delta> fine p
- \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - integral (cbox a b) g) < e/2"
+ "\<And>\<D>. \<D> tagged_division_of cbox a b \<and> \<delta> fine \<D>
+ \<Longrightarrow> norm ((\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R g x) - integral (cbox a b) g) < e/2"
by meson
ultimately have "gauge (\<lambda>x. \<gamma> x \<inter> \<delta> x)"
using gauge_Int by blast
- with fine_division_exists obtain p
- where p: "p tagged_division_of cbox a b" "(\<lambda>x. \<gamma> x \<inter> \<delta> x) fine p"
+ with fine_division_exists obtain \<D>
+ where p: "\<D> tagged_division_of cbox a b" "(\<lambda>x. \<gamma> x \<inter> \<delta> x) fine \<D>"
by metis
- have "\<gamma> fine p" "\<delta> fine p"
+ have "\<gamma> fine \<D>" "\<delta> fine \<D>"
using fine_Int p(2) by blast+
show "norm (integral (cbox a b) f) < integral (cbox a b) g + e"
proof (rule norm)
- have "norm (content K *\<^sub>R f x) \<le> content K *\<^sub>R g x" if "(x, K) \<in> p" for x K
+ have "norm (content K *\<^sub>R f x) \<le> content K *\<^sub>R g x" if "(x, K) \<in> \<D>" for x K
proof-
have K: "x \<in> K" "K \<subseteq> cbox a b"
- using \<open>(x, K) \<in> p\<close> p(1) by blast+
+ using \<open>(x, K) \<in> \<D>\<close> p(1) by blast+
obtain u v where "K = cbox u v"
- using \<open>(x, K) \<in> p\<close> p(1) by blast
+ using \<open>(x, K) \<in> \<D>\<close> p(1) by blast
moreover have "content K * norm (f x) \<le> content K * g x"
by (metis K subsetD dual_order.antisym measure_nonneg mult_zero_left nle not_le real_mult_le_cancel_iff2)
then show ?thesis
by simp
qed
- then show "norm (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) \<le> (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
+ then show "norm (\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R f x) \<le> (\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R g x)"
by (simp add: sum_norm_le split_def)
- show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral (cbox a b) f) < e/2"
- using \<open>\<gamma> fine p\<close> \<gamma> p(1) by simp
- show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - integral (cbox a b) g\<bar> < e/2"
- using \<open>\<delta> fine p\<close> \<delta> p(1) by simp
+ show "norm ((\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R f x) - integral (cbox a b) f) < e/2"
+ using \<open>\<gamma> fine \<D>\<close> \<gamma> p(1) by simp
+ show "\<bar>(\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R g x) - integral (cbox a b) g\<bar> < e/2"
+ using \<open>\<delta> fine \<D>\<close> \<delta> p(1) by simp
qed
qed
show ?thesis
@@ -7184,13 +7156,13 @@
\<le> e * content (cbox (u, w) (v, z)) / content ?CBOX"
using that by (simp add: e'_def)
} note op_acbd = this
- { fix k::real and p and u::'a and v w and z::'b and t1 t2 l
+ { fix k::real and \<D> and u::'a and v w and z::'b and t1 t2 l
assume k: "0 < k"
and nf: "\<And>x y u v.
\<lbrakk>x \<in> cbox a b; y \<in> cbox c d; u \<in> cbox a b; v\<in>cbox c d; norm (u-x, v-y) < k\<rbrakk>
\<Longrightarrow> norm (f(u,v) - f(x,y)) < e/(2 * (content ?CBOX))"
- and p_acbd: "p tagged_division_of cbox (a,c) (b,d)"
- and fine: "(\<lambda>x. ball x k) fine p" "((t1,t2), l) \<in> p"
+ and p_acbd: "\<D> tagged_division_of cbox (a,c) (b,d)"
+ and fine: "(\<lambda>x. ball x k) fine \<D>" "((t1,t2), l) \<in> \<D>"
and uwvz_sub: "cbox (u,w) (v,z) \<subseteq> l" "cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)"
have t: "t1 \<in> cbox a b" "t2 \<in> cbox c d"
by (meson fine p_acbd cbox_Pair_iff tag_in_interval)+
--- a/src/HOL/Analysis/Tagged_Division.thy Thu Aug 24 10:47:56 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy Thu Aug 24 12:45:46 2017 +0100
@@ -1122,7 +1122,7 @@
unfolding box_real[symmetric]
by (rule tagged_division_of_self)
-lemma tagged_division_union:
+lemma tagged_division_Un:
assumes "p1 tagged_division_of s1"
and "p2 tagged_division_of s2"
and "interior s1 \<inter> interior s2 = {}"
@@ -1150,13 +1150,13 @@
by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
qed
-lemma tagged_division_unions:
+lemma tagged_division_Union:
assumes "finite I"
- and "\<forall>i\<in>I. pfn i tagged_division_of i"
- and "\<forall>i1\<in>I. \<forall>i2\<in>I. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
+ and tag: "\<And>i. i\<in>I \<Longrightarrow> pfn i tagged_division_of i"
+ and disj: "\<And>i1 i2. \<lbrakk>i1 \<in> I; i2 \<in> I; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior(i1) \<inter> interior(i2) = {}"
shows "\<Union>(pfn ` I) tagged_division_of (\<Union>I)"
proof (rule tagged_division_ofI)
- note assm = tagged_division_ofD[OF assms(2)[rule_format]]
+ note assm = tagged_division_ofD[OF tag]
show "finite (\<Union>(pfn ` I))"
using assms by auto
have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` I)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` I)"
@@ -1175,16 +1175,18 @@
then obtain i' where i': "i' \<in> I" "(x', k') \<in> pfn i'"
by auto
have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}"
- using i(1) i'(1)
- using assms(3)[rule_format] interior_mono
- by blast
+ using i(1) i'(1) disj interior_mono by blast
show "interior k \<inter> interior k' = {}"
- apply (cases "i = i'")
- using assm(5) i' i(2) xk'(2) apply blast
+ proof (cases "i = i'")
+ case True then show ?thesis
+ using assm(5) i' i xk'(2) by blast
+ next
+ case False then show ?thesis
using "*" assm(3) i' i by auto
+ qed
qed
-lemma tagged_partial_division_of_union_self:
+lemma tagged_partial_division_of_Union_self:
assumes "p tagged_partial_division_of s"
shows "p tagged_division_of (\<Union>(snd ` p))"
apply (rule tagged_division_ofI)
@@ -1200,7 +1202,7 @@
apply auto
done
-lemma tagged_division_union_interval:
+lemma tagged_division_Un_interval:
fixes a :: "'a::euclidean_space"
assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
@@ -1211,14 +1213,14 @@
by auto
show ?thesis
apply (subst *)
- apply (rule tagged_division_union[OF assms(1-2)])
+ apply (rule tagged_division_Un[OF assms(1-2)])
unfolding interval_split[OF k] interior_cbox
using k
apply (auto simp add: box_def elim!: ballE[where x=k])
done
qed
-lemma tagged_division_union_interval_real:
+lemma tagged_division_Un_interval_real:
fixes a :: real
assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
@@ -1226,7 +1228,7 @@
shows "(p1 \<union> p2) tagged_division_of {a .. b}"
using assms
unfolding box_real[symmetric]
- by (rule tagged_division_union_interval)
+ by (rule tagged_division_Un_interval)
lemma tagged_division_split_left_inj:
assumes d: "d tagged_division_of i"
@@ -1539,7 +1541,7 @@
done
by (simp add: interval_split k interval_doublesplit)
qed
-
+
paragraph \<open>Operative\<close>
locale operative = comm_monoid_set +
@@ -1571,7 +1573,7 @@
assume "box a b = {}"
{ fix k assume "k\<in>d"
then obtain a' b' where k: "k = cbox a' b'"
- using division_ofD(4) [OF less.prems] by blast
+ using division_ofD(4)[OF less.prems] by blast
with \<open>k\<in>d\<close> division_ofD(2)[OF less.prems] have "cbox a' b' \<subseteq> cbox a b"
by auto
then have "box a' b' \<subseteq> box a b"
@@ -1754,7 +1756,7 @@
using assms box_empty_imp by (rule over_tagged_division_lemma)
then show ?thesis
unfolding assms [THEN division_of_tagged_division, THEN division] .
-qed
+ qed
end
@@ -1779,14 +1781,14 @@
from that have [simp]: "k = 1"
by simp
from neutral [of 0 1] neutral [of a a for a] coalesce_less
- have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
- "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
- by auto
+ have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
+ "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+ by auto
have "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
- by (auto simp: min_def max_def le_less)
+ by (auto simp: min_def max_def le_less)
then show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
by (simp add: atMost_def [symmetric] atLeast_def [symmetric])
- qed
+qed
qed
show "box = (greaterThanLessThan :: real \<Rightarrow> _)"
and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
@@ -1796,17 +1798,17 @@
lemma coalesce_less_eq:
"g {a..c} \<^bold>* g {c..b} = g {a..b}" if "a \<le> c" "c \<le> b"
-proof (cases "c = a \<or> c = b")
- case False
+ proof (cases "c = a \<or> c = b")
+ case False
with that have "a < c" "c < b"
by auto
- then show ?thesis
+ then show ?thesis
by (rule coalesce_less)
-next
- case True
+ next
+ case True
with that box_empty_imp [of a a] box_empty_imp [of b b] show ?thesis
by safe simp_all
-qed
+ qed
end
@@ -1823,7 +1825,7 @@
using that
using Basis_imp [of 1 a b c]
by (simp_all add: atMost_def [symmetric] atLeast_def [symmetric] max_def min_def)
- qed
+qed
qed
@@ -1901,7 +1903,7 @@
using bchoice[OF assms(2)] by auto
show thesis
apply (rule_tac p="\<Union>(pfn ` I)" in that)
- using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force
+ using assms(1) assms(3) assms(4) pfn(1) tagged_division_Union apply force
by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
qed
@@ -2252,7 +2254,7 @@
\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ False])
apply (simp add: fine_def)
- apply (metis tagged_division_union fine_Un)
+ apply (metis tagged_division_Un fine_Un)
apply auto
done
obtain e where e: "e > 0" "ball x e \<subseteq> g x"
@@ -2343,7 +2345,7 @@
have "{(x, cbox u v)} tagged_division_of cbox u v"
by (simp add: p(2) uv xk tagged_division_of_self)
then have "{(x, cbox u v)} \<union> q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> insert xk p}"
- unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_union)
+ unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_Un)
with True show ?thesis
apply (rule_tac x="{(x,cbox u v)} \<union> q1" in exI)
using \<open>d fine q1\<close> fine_def q1I uv xk apply fastforce
@@ -2356,7 +2358,7 @@
apply (rule_tac x="q2 \<union> q1" in exI)
apply (intro conjI)
unfolding * uv
- apply (rule tagged_division_union q2 q1 int fine_Un)+
+ apply (rule tagged_division_Un q2 q1 int fine_Un)+
apply (auto intro: q1 q2 fine_Un \<open>d fine q1\<close> simp add: False q1I uv xk)
done
qed