--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Aug 12 23:11:26 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Aug 13 19:24:33 2017 +0100
@@ -513,11 +513,11 @@
have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f"
proof (rule monotone_convergence_increasing)
- show "\<forall>k. U k integrable_on UNIV" using U_int by auto
- show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
- then show "bounded {integral UNIV (U k) |k. True}"
+ show "\<And>k. U k integrable_on UNIV" using U_int by auto
+ show "\<And>k x. x\<in>UNIV \<Longrightarrow> U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
+ then show "bounded (range (\<lambda>k. integral UNIV (U k)))"
using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r])
- show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
+ show "\<And>x. x\<in>UNIV \<Longrightarrow> (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
using seq by auto
qed
moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Aug 12 23:11:26 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Aug 13 19:24:33 2017 +0100
@@ -6018,12 +6018,19 @@
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)
+
lemma monotone_convergence_interval:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
assumes "\<forall>k. (f k) integrable_on cbox a b"
and "\<forall>k. \<forall>x\<in>cbox a b.(f k x) \<le> f (Suc k) x"
and "\<forall>x\<in>cbox a b. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
- and "bounded {integral (cbox a b) (f k) | k . k \<in> UNIV}"
+ and bounded: "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
@@ -6049,45 +6056,31 @@
apply auto
done
qed
- have "\<exists>i. ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> i) sequentially"
- apply (rule bounded_increasing_convergent)
- defer
- apply rule
- apply (rule integral_le)
- apply safe
- apply (rule assms(1-2)[rule_format])+
- using assms(4)
- apply auto
- done
- then guess i..note i=this
- have i': "\<And>k. (integral(cbox a b) (f k)) \<le> i\<bullet>1"
- apply (rule Lim_component_ge)
- apply (rule i)
- apply (rule trivial_limit_sequentially)
+ 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))
+ then obtain i where i: "(\<lambda>k. integral (cbox a b) (f k)) \<longlonglongrightarrow> i"
+ using bounded_increasing_convergent bounded 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"
unfolding eventually_sequentially
- apply (rule_tac x=k in exI)
- apply clarify
- apply (erule transitive_stepwise_le)
- prefer 3
- unfolding inner_simps real_inner_1_right
- apply (rule integral_le)
- apply (rule assms(1-2)[rule_format])+
- using assms(2)
- apply auto
- done
-
+ 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
have "(g has_integral i) (cbox a b)"
unfolding has_integral
proof (safe, goal_cases)
- case e: (1 e)
- then have "\<forall>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
+ 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>
norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e/2 ^ (k + 2)))"
- apply -
- apply rule
apply (rule assms(1)[unfolded has_integral_integral has_integral,rule_format])
- apply auto
+ using e apply auto
done
- from choice[OF this] guess c..note c=conjunctD2[OF this[rule_format],rule_format]
+ 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>
+ norm ((\<Sum>(u, ka)\<in>p. content ka *\<^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"
proof -
@@ -6095,11 +6088,7 @@
using e by auto
from LIMSEQ_D [OF i this] guess r ..
then show ?thesis
- apply (rule_tac x=r in exI)
- apply rule
- apply (erule_tac x=k in allE)
- subgoal for k using i'[of k] by auto
- done
+ using i' by auto
qed
then guess r..note r=conjunctD2[OF this[rule_format]]
@@ -6122,7 +6111,14 @@
qed
from bchoice[OF this] guess m..note m=conjunctD2[OF this[rule_format],rule_format]
define d where "d x = c (m x) x" for x
- show ?case
+ show "\<exists>d. gauge d \<and>
+ (\<forall>p. p tagged_division_of cbox a b \<and>
+ d fine p \<longrightarrow>
+ norm
+ ((\<Sum>(x, k)\<in>p.
+ content k *\<^sub>R g x) -
+ i)
+ < e)"
apply (rule_tac x=d in exI)
proof safe
show "gauge d"
@@ -6215,7 +6211,6 @@
apply (simp add: e)
apply safe
apply (rule c)+
- apply rule
apply assumption+
apply (rule tagged_partial_division_subset[of p])
apply (rule p(1)[unfolded tagged_division_of_def,THEN conjunct1])
@@ -6286,22 +6281,22 @@
lemma monotone_convergence_increasing:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
- assumes "\<forall>k. (f k) integrable_on s"
- and "\<forall>k. \<forall>x\<in>s. (f k x) \<le> (f (Suc k) x)"
- and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
- and "bounded {integral s (f k)| k. True}"
- shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
+ assumes "\<And>k. (f k) integrable_on S"
+ and "\<And>k x. x \<in> S \<Longrightarrow> (f k x) \<le> (f (Suc k) x)"
+ and "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
+ and "bounded (range (\<lambda>k. integral S (f k)))"
+ shows "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially"
proof -
- have lem: "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
- if "\<forall>k. \<forall>x\<in>s. 0 \<le> f k x"
- and "\<forall>k. (f k) integrable_on s"
- and "\<forall>k. \<forall>x\<in>s. f k x \<le> f (Suc k) x"
- and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
- and "bounded {integral s (f k)| k. True}"
- for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g s
+ have lem: "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially"
+ if "\<forall>k. \<forall>x\<in>S. 0 \<le> f k x"
+ and "\<forall>k. (f k) integrable_on S"
+ and "\<forall>k. \<forall>x\<in>S. f k x \<le> f (Suc k) x"
+ and "\<forall>x\<in>S. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
+ and bou: "bounded (range(\<lambda>k. integral S (f k)))"
+ for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g S
proof -
note assms=that[rule_format]
- have "\<forall>x\<in>s. \<forall>k. (f k x)\<bullet>1 \<le> (g x)\<bullet>1"
+ have "\<forall>x\<in>S. \<forall>k. (f k x)\<bullet>1 \<le> (g x)\<bullet>1"
apply safe
apply (rule Lim_component_ge)
apply (rule that(4)[rule_format])
@@ -6312,19 +6307,12 @@
using assms(3) by (force intro: transitive_stepwise_le)
note fg=this[rule_format]
- have "\<exists>i. ((\<lambda>k. integral s (f k)) \<longlongrightarrow> i) sequentially"
- apply (rule bounded_increasing_convergent)
- apply (rule that(5))
- apply rule
- apply (rule integral_le)
- apply (rule that(2)[rule_format])+
- using that(3)
- apply auto
- done
- then guess i..note i=this
- have "\<And>k. \<forall>x\<in>s. \<forall>n\<ge>k. f k x \<le> f n x"
+ obtain i where i: "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> i"
+ using bounded_increasing_convergent [OF bou]
+ using \<open>\<forall>k. \<forall>x\<in>S. f k x \<le> f (Suc k) x\<close> assms(2) integral_le by blast
+ have "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
using assms(3) by (force intro: transitive_stepwise_le)
- then have i': "\<forall>k. (integral s (f k))\<bullet>1 \<le> i\<bullet>1"
+ then have i': "\<forall>k. (integral S (f k))\<bullet>1 \<le> i\<bullet>1"
apply -
apply rule
apply (rule Lim_component_ge)
@@ -6339,45 +6327,45 @@
apply auto
done
- note int = assms(2)[unfolded integrable_alt[of _ s],THEN conjunct1,rule_format]
- have ifif: "\<And>k t. (\<lambda>x. if x \<in> t then if x \<in> s then f k x else 0 else 0) =
- (\<lambda>x. if x \<in> t \<inter> s then f k x else 0)"
+ note int = assms(2)[unfolded integrable_alt[of _ S],THEN conjunct1,rule_format]
+ have ifif: "\<And>k t. (\<lambda>x. if x \<in> t then if x \<in> S then f k x else 0 else 0) =
+ (\<lambda>x. if x \<in> t \<inter> S then f k x else 0)"
by (rule ext) auto
- have int': "\<And>k a b. f k integrable_on cbox a b \<inter> s"
+ have int': "\<And>k a b. f k integrable_on cbox a b \<inter> S"
apply (subst integrable_restrict_UNIV[symmetric])
apply (subst ifif[symmetric])
apply (subst integrable_restrict_UNIV)
apply (rule int)
done
- have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on cbox a b \<and>
- ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) \<longlongrightarrow>
- integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0)) sequentially"
+ have "\<And>a b. (\<lambda>x. if x \<in> S then g x else 0) integrable_on cbox a b \<and>
+ ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)) \<longlongrightarrow>
+ integral (cbox a b) (\<lambda>x. if x \<in> S then g x else 0)) sequentially"
proof (rule monotone_convergence_interval, safe, goal_cases)
case 1
show ?case by (rule int)
next
case (2 _ _ _ x)
then show ?case
- apply (cases "x \<in> s")
+ apply (cases "x \<in> S")
using assms(3)
apply auto
done
next
case (3 _ _ x)
then show ?case
- apply (cases "x \<in> s")
+ apply (cases "x \<in> S")
using assms(4)
apply auto
done
next
case (4 a b)
note * = integral_nonneg
- have "\<And>k. norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))"
+ have "\<And>k. norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)) \<le> norm (integral S (f k))"
unfolding real_norm_def
apply (subst abs_of_nonneg)
apply (rule *[OF int])
apply safe
- apply (case_tac "x \<in> s")
+ apply (case_tac "x \<in> S")
apply (drule assms(1))
prefer 3
apply (subst abs_of_nonneg)
@@ -6395,7 +6383,7 @@
apply safe
apply (rule_tac x=aa in exI)
apply safe
- apply (erule_tac x="integral s (f k)" in ballE)
+ apply (erule_tac x="integral S (f k)" in ballE)
apply (rule order_trans)
apply assumption
apply auto
@@ -6403,7 +6391,7 @@
qed
note g = conjunctD2[OF this]
- have "(g has_integral i) s"
+ have "(g has_integral i) S"
unfolding has_integral_alt'
apply safe
apply (rule g(1))
@@ -6425,7 +6413,7 @@
from \<open>e > 0\<close> have "e/2 > 0"
by auto
from LIMSEQ_D [OF g(2)[of a b] this] guess M..note M=this
- have **: "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f N x else 0) - i) < e/2"
+ have **: "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f N x else 0) - i) < e/2"
apply (rule norm_triangle_half_l)
using B(2)[rule_format,OF ab] N[rule_format,of N]
apply -
@@ -6436,7 +6424,7 @@
have *: "\<And>f1 f2 g. \<bar>f1 - i\<bar> < e/2 \<longrightarrow> \<bar>f2 - g\<bar> < e/2 \<longrightarrow>
f1 \<le> f2 \<longrightarrow> f2 \<le> i \<longrightarrow> \<bar>g - i\<bar> < e"
unfolding real_inner_1_right by arith
- show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0) - i) < e"
+ show "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then g x else 0) - i) < e"
unfolding real_norm_def
apply (rule *[rule_format])
apply (rule **[unfolded real_norm_def])
@@ -6447,7 +6435,7 @@
apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]])
proof (safe, goal_cases)
case (2 x)
- have "\<And>m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1"
+ have "\<And>m. x \<in> S \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1"
using assms(3) by (force intro: transitive_stepwise_le)
then show ?case
by auto
@@ -6472,16 +6460,16 @@
done
qed
- have sub: "\<And>k. integral s (\<lambda>x. f k x - f 0 x) = integral s (f k) - integral s (f 0)"
+ have sub: "\<And>k. integral S (\<lambda>x. f k x - f 0 x) = integral S (f k) - integral S (f 0)"
apply (subst integral_diff)
apply (rule assms(1)[rule_format])+
apply rule
done
- have "\<And>x m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. f m x \<le> f n x"
+ have "\<And>x m. x \<in> S \<Longrightarrow> \<forall>n\<ge>m. f m x \<le> f n x"
using assms(2) by (force intro: transitive_stepwise_le)
note * = this[rule_format]
- have "(\<lambda>x. g x - f 0 x) integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. f (Suc k) x - f 0 x)) \<longlongrightarrow>
- integral s (\<lambda>x. g x - f 0 x)) sequentially"
+ have "(\<lambda>x. g x - f 0 x) integrable_on S \<and> ((\<lambda>k. integral S (\<lambda>x. f (Suc k) x - f 0 x)) \<longlongrightarrow>
+ integral S (\<lambda>x. g x - f 0 x)) sequentially"
apply (rule lem)
apply safe
proof goal_cases
@@ -6513,16 +6501,16 @@
using assms(4)
unfolding bounded_iff
apply safe
- apply (rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
+ apply (rule_tac x="a + norm (integral S (\<lambda>x. f 0 x))" in exI)
apply safe
- apply (erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE)
+ apply (erule_tac x="integral S (\<lambda>x. f (Suc k) x)" in ballE)
unfolding sub
apply (rule order_trans[OF norm_triangle_ineq4])
apply auto
done
qed
note conjunctD2[OF this]
- note tendsto_add[OF this(2) tendsto_const[of "integral s (f 0)"]]
+ note tendsto_add[OF this(2) tendsto_const[of "integral S (f 0)"]]
integrable_add[OF this(1) assms(1)[rule_format,of 0]]
then show ?thesis
unfolding sub
@@ -6547,13 +6535,12 @@
proof -
have x_eq: "x = (\<lambda>i. integral s (f i))"
by (simp add: integral_unique[OF f])
- then have x: "{integral s (f k) |k. True} = range x"
+ then have x: "range(\<lambda>k. integral s (f k)) = range x"
by auto
-
have *: "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
proof (intro monotone_convergence_increasing allI ballI assms)
- show "bounded {integral s (f k) |k. True}"
- unfolding x by (rule convergent_imp_bounded) fact
+ show "bounded (range(\<lambda>k. integral s (f k)))"
+ using x convergent_imp_bounded assms by metis
qed (use f in auto)
then have "integral s g = x'"
by (intro LIMSEQ_unique[OF _ \<open>x \<longlonglongrightarrow> x'\<close>]) (simp add: x_eq)
@@ -6563,40 +6550,34 @@
lemma monotone_convergence_decreasing:
fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
- assumes "\<forall>k. (f k) integrable_on s"
- and "\<forall>k. \<forall>x\<in>s. f (Suc k) x \<le> f k x"
- and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
- and "bounded {integral s (f k)| k. True}"
- shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
+ assumes "\<And>k. (f k) integrable_on S"
+ and "\<And>k x. x \<in> S \<Longrightarrow> f (Suc k) x \<le> f k x"
+ and "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
+ and "bounded (range(\<lambda>k. integral S (f k)))"
+ shows "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially"
proof -
- note assm = assms[rule_format]
- have *: "{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R (- 1) ` {integral s (f k)| k. True}"
+ have *: "{integral S (\<lambda>x. - f k x) |k. True} = op *\<^sub>R (- 1) ` (range(\<lambda>k. integral S (f k)))"
apply safe
unfolding image_iff
- apply (rule_tac x="integral s (f k)" in bexI)
+ apply (rule_tac x="integral S (f k)" in bexI)
prefer 3
apply (rule_tac x=k in exI)
apply auto
done
- have "(\<lambda>x. - g x) integrable_on s \<and>
- ((\<lambda>k. integral s (\<lambda>x. - f k x)) \<longlongrightarrow> integral s (\<lambda>x. - g x)) sequentially"
- apply (rule monotone_convergence_increasing)
- apply safe
- apply (rule integrable_neg)
- apply (rule assm)
- defer
- apply (rule tendsto_minus)
- apply (rule assm)
- apply assumption
- unfolding *
- apply (rule bounded_scaling)
- using assm
- apply auto
- done
- note * = conjunctD2[OF this]
- show ?thesis
- using integrable_neg[OF *(1)] tendsto_minus[OF *(2)]
- by auto
+ have "(\<lambda>x. - g x) integrable_on S \<and>
+ ((\<lambda>k. integral S (\<lambda>x. - f k x)) \<longlongrightarrow> integral S (\<lambda>x. - g x)) sequentially"
+ proof (rule monotone_convergence_increasing)
+ show "\<And>k. (\<lambda>x. - f k x) integrable_on S"
+ by (blast intro: integrable_neg assms)
+ show "\<And>k x. x \<in> S \<Longrightarrow> - f k x \<le> - f (Suc k) x"
+ by (simp add: assms)
+ show "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. - f k x) \<longlonglongrightarrow> - g x"
+ by (simp add: assms tendsto_minus)
+ show "bounded (range(\<lambda>k. integral S (\<lambda>x. - f k x)))"
+ using "*" assms(4) bounded_scaling by auto
+ qed
+ then show ?thesis
+ by (force dest: integrable_neg tendsto_minus)
qed
lemma integral_norm_bound_integral:
@@ -7553,7 +7534,7 @@
also have "\<dots> \<le> exp (- a * c) / a" using a by simp
finally show ?thesis .
qed (insert a, simp_all add: integral_f)
- thus "bounded {integral {c..} (f k) |k. True}"
+ thus "bounded (range(\<lambda>k. integral {c..} (f k)))"
by (intro boundedI[of _ "exp (-a*c)/a"]) auto
qed (auto simp: f_def)
@@ -7646,7 +7627,7 @@
hence "F k = abs (F k)" by simp
finally have "abs (F k) \<le> c powr (a + 1) / (a + 1)" .
}
- thus "bounded {integral {0..c} (f k) |k. True}"
+ thus "bounded (range(\<lambda>k. integral {0..c} (f k)))"
by (intro boundedI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f)
qed
@@ -7732,7 +7713,7 @@
by (intro powr_mono2') simp_all
with assms show ?thesis by (auto simp: divide_simps F_def integral_f)
qed (insert assms, simp add: integral_f F_def divide_simps)
- thus "bounded {integral {a..} (f n) |n. True}"
+ thus "bounded (range(\<lambda>k. integral {a..} (f k)))"
unfolding bounded_iff by (intro exI[of _ "-F a"]) auto
qed
--- a/src/HOL/Analysis/Improper_Integral.thy Sat Aug 12 23:11:26 2017 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy Sun Aug 13 19:24:33 2017 +0100
@@ -1507,7 +1507,7 @@
let ?\<phi> = "\<lambda>k x. if x \<in> cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k))
then g x - f x \<bullet> j else 0"
have "(\<lambda>x. g x - f x \<bullet> j) integrable_on box a b"
- proof (rule monotone_convergence_increasing [of ?\<phi>, THEN conjunct1], safe)
+ proof (rule monotone_convergence_increasing [of ?\<phi>, THEN conjunct1])
have *: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) \<inter> box a b
= cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))" for k
using box_subset_cbox "1" by fastforce
@@ -1562,7 +1562,7 @@
apply (simp add: integral_restrict_Int integral_diff)
using "*" box_subset_cbox by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4])
qed
- then show "bounded {integral (box a b) (?\<phi> k)| k. True}"
+ then show "bounded (range (\<lambda>k. integral (box a b) (?\<phi> k)))"
apply (simp add: bounded_pos)
apply (rule_tac x="Bg+Bf" in exI)
using \<open>0 < Bf\<close> \<open>0 < Bg\<close> apply auto
@@ -1585,7 +1585,7 @@
let ?\<phi> = "\<lambda>k x. if x \<in> cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k))
then f x \<bullet> j - g x else 0"
have "(\<lambda>x. f x \<bullet> j - g x) integrable_on box a b"
- proof (rule monotone_convergence_increasing [of ?\<phi>, THEN conjunct1], safe)
+ proof (rule monotone_convergence_increasing [of ?\<phi>, THEN conjunct1])
have *: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) \<inter> box a b
= cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))" for k
using box_subset_cbox "1" by fastforce
@@ -1642,7 +1642,7 @@
apply (simp add: integral_restrict_Int integral_diff)
using "*" box_subset_cbox by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4])
qed
- then show "bounded {integral (box a b) (?\<phi> k)| k. True}"
+ then show "bounded (range (\<lambda>k. integral (box a b) (?\<phi> k)))"
apply (simp add: bounded_pos)
apply (rule_tac x="Bf+Bg" in exI)
using \<open>0 < Bf\<close> \<open>0 < Bg\<close> by auto
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sat Aug 12 23:11:26 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Aug 13 19:24:33 2017 +0100
@@ -5389,13 +5389,6 @@
shows "~ compact (UNIV::'a set)"
by (simp add: compact_eq_bounded_closed)
-(* TODO: is this lemma necessary? *)
-lemma bounded_increasing_convergent:
- fixes s :: "nat \<Rightarrow> real"
- shows "bounded {s n| n. True} \<Longrightarrow> \<forall>n. s n \<le> s (Suc n) \<Longrightarrow> \<exists>l. s \<longlonglongrightarrow> l"
- using Bseq_mono_convergent[of s] incseq_Suc_iff[of s]
- by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def)
-
instance real :: heine_borel
proof
fix f :: "nat \<Rightarrow> real"