6016 qed |
6016 qed |
6017 |
6017 |
6018 |
6018 |
6019 subsection \<open>Monotone convergence (bounded interval first)\<close> |
6019 subsection \<open>Monotone convergence (bounded interval first)\<close> |
6020 |
6020 |
|
6021 (* TODO: is this lemma necessary? *) |
|
6022 lemma bounded_increasing_convergent: |
|
6023 fixes f :: "nat \<Rightarrow> real" |
|
6024 shows "\<lbrakk>bounded (range f); \<And>n. f n \<le> f (Suc n)\<rbrakk> \<Longrightarrow> \<exists>l. f \<longlonglongrightarrow> l" |
|
6025 using Bseq_mono_convergent[of f] incseq_Suc_iff[of f] |
|
6026 by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def) |
|
6027 |
6021 lemma monotone_convergence_interval: |
6028 lemma monotone_convergence_interval: |
6022 fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" |
6029 fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" |
6023 assumes "\<forall>k. (f k) integrable_on cbox a b" |
6030 assumes "\<forall>k. (f k) integrable_on cbox a b" |
6024 and "\<forall>k. \<forall>x\<in>cbox a b.(f k x) \<le> f (Suc k) x" |
6031 and "\<forall>k. \<forall>x\<in>cbox a b.(f k x) \<le> f (Suc k) x" |
6025 and "\<forall>x\<in>cbox a b. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially" |
6032 and "\<forall>x\<in>cbox a b. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially" |
6026 and "bounded {integral (cbox a b) (f k) | k . k \<in> UNIV}" |
6033 and bounded: "bounded (range (\<lambda>k. integral (cbox a b) (f k)))" |
6027 shows "g integrable_on cbox a b \<and> ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> integral (cbox a b) g) sequentially" |
6034 shows "g integrable_on cbox a b \<and> ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> integral (cbox a b) g) sequentially" |
6028 proof (cases "content (cbox a b) = 0") |
6035 proof (cases "content (cbox a b) = 0") |
6029 case True |
6036 case True |
6030 show ?thesis |
6037 show ?thesis |
6031 using integrable_on_null[OF True] |
6038 using integrable_on_null[OF True] |
6047 apply (rule transitive_stepwise_le) |
6054 apply (rule transitive_stepwise_le) |
6048 using assms(2)[rule_format, OF x] |
6055 using assms(2)[rule_format, OF x] |
6049 apply auto |
6056 apply auto |
6050 done |
6057 done |
6051 qed |
6058 qed |
6052 have "\<exists>i. ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> i) sequentially" |
6059 have int_inc: "\<And>n. integral (cbox a b) (f n) \<le> integral (cbox a b) (f (Suc n))" |
6053 apply (rule bounded_increasing_convergent) |
6060 by (metis integral_le assms(1-2)) |
6054 defer |
6061 then obtain i where i: "(\<lambda>k. integral (cbox a b) (f k)) \<longlonglongrightarrow> i" |
6055 apply rule |
6062 using bounded_increasing_convergent bounded by blast |
6056 apply (rule integral_le) |
6063 have "\<And>k. \<forall>\<^sub>F x in sequentially. integral (cbox a b) (f k) \<le> integral (cbox a b) (f x) \<bullet> 1" |
6057 apply safe |
|
6058 apply (rule assms(1-2)[rule_format])+ |
|
6059 using assms(4) |
|
6060 apply auto |
|
6061 done |
|
6062 then guess i..note i=this |
|
6063 have i': "\<And>k. (integral(cbox a b) (f k)) \<le> i\<bullet>1" |
|
6064 apply (rule Lim_component_ge) |
|
6065 apply (rule i) |
|
6066 apply (rule trivial_limit_sequentially) |
|
6067 unfolding eventually_sequentially |
6064 unfolding eventually_sequentially |
6068 apply (rule_tac x=k in exI) |
6065 by (force intro: transitive_stepwise_le int_inc) |
6069 apply clarify |
6066 then have i': "\<And>k. (integral(cbox a b) (f k)) \<le> i\<bullet>1" |
6070 apply (erule transitive_stepwise_le) |
6067 using Lim_component_ge [OF i] trivial_limit_sequentially by blast |
6071 prefer 3 |
|
6072 unfolding inner_simps real_inner_1_right |
|
6073 apply (rule integral_le) |
|
6074 apply (rule assms(1-2)[rule_format])+ |
|
6075 using assms(2) |
|
6076 apply auto |
|
6077 done |
|
6078 |
|
6079 have "(g has_integral i) (cbox a b)" |
6068 have "(g has_integral i) (cbox a b)" |
6080 unfolding has_integral |
6069 unfolding has_integral |
6081 proof (safe, goal_cases) |
6070 proof (safe, goal_cases) |
6082 case e: (1 e) |
6071 fix e::real |
6083 then have "\<forall>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
6072 assume e: "e > 0" |
|
6073 have "\<And>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> |
6084 norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e/2 ^ (k + 2)))" |
6074 norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e/2 ^ (k + 2)))" |
6085 apply - |
|
6086 apply rule |
|
6087 apply (rule assms(1)[unfolded has_integral_integral has_integral,rule_format]) |
6075 apply (rule assms(1)[unfolded has_integral_integral has_integral,rule_format]) |
6088 apply auto |
6076 using e apply auto |
6089 done |
6077 done |
6090 from choice[OF this] guess c..note c=conjunctD2[OF this[rule_format],rule_format] |
6078 then obtain c where c: |
|
6079 "\<And>x. gauge (c x)" |
|
6080 "\<And>x p. \<lbrakk>p tagged_division_of cbox a b; c x fine p\<rbrakk> \<Longrightarrow> |
|
6081 norm ((\<Sum>(u, ka)\<in>p. content ka *\<^sub>R f x u) - integral (cbox a b) (f x)) |
|
6082 < e / 2 ^ (x + 2)" |
|
6083 by metis |
6091 |
6084 |
6092 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" |
6085 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" |
6093 proof - |
6086 proof - |
6094 have "e/4 > 0" |
6087 have "e/4 > 0" |
6095 using e by auto |
6088 using e by auto |
6096 from LIMSEQ_D [OF i this] guess r .. |
6089 from LIMSEQ_D [OF i this] guess r .. |
6097 then show ?thesis |
6090 then show ?thesis |
6098 apply (rule_tac x=r in exI) |
6091 using i' by auto |
6099 apply rule |
|
6100 apply (erule_tac x=k in allE) |
|
6101 subgoal for k using i'[of k] by auto |
|
6102 done |
|
6103 qed |
6092 qed |
6104 then guess r..note r=conjunctD2[OF this[rule_format]] |
6093 then guess r..note r=conjunctD2[OF this[rule_format]] |
6105 |
6094 |
6106 have "\<forall>x\<in>cbox a b. \<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)\<bullet>1 - (f k x)\<bullet>1 \<and> |
6095 have "\<forall>x\<in>cbox a b. \<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)\<bullet>1 - (f k x)\<bullet>1 \<and> |
6107 (g x)\<bullet>1 - (f k x)\<bullet>1 < e / (4 * content(cbox a b))" |
6096 (g x)\<bullet>1 - (f k x)\<bullet>1 < e / (4 * content(cbox a b))" |
6120 apply (auto simp add: field_simps) |
6109 apply (auto simp add: field_simps) |
6121 done |
6110 done |
6122 qed |
6111 qed |
6123 from bchoice[OF this] guess m..note m=conjunctD2[OF this[rule_format],rule_format] |
6112 from bchoice[OF this] guess m..note m=conjunctD2[OF this[rule_format],rule_format] |
6124 define d where "d x = c (m x) x" for x |
6113 define d where "d x = c (m x) x" for x |
6125 show ?case |
6114 show "\<exists>d. gauge d \<and> |
|
6115 (\<forall>p. p tagged_division_of cbox a b \<and> |
|
6116 d fine p \<longrightarrow> |
|
6117 norm |
|
6118 ((\<Sum>(x, k)\<in>p. |
|
6119 content k *\<^sub>R g x) - |
|
6120 i) |
|
6121 < e)" |
6126 apply (rule_tac x=d in exI) |
6122 apply (rule_tac x=d in exI) |
6127 proof safe |
6123 proof safe |
6128 show "gauge d" |
6124 show "gauge d" |
6129 using c(1) unfolding gauge_def d_def by auto |
6125 using c(1) unfolding gauge_def d_def by auto |
6130 next |
6126 next |
6284 using i * by auto |
6279 using i * by auto |
6285 qed |
6280 qed |
6286 |
6281 |
6287 lemma monotone_convergence_increasing: |
6282 lemma monotone_convergence_increasing: |
6288 fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" |
6283 fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" |
6289 assumes "\<forall>k. (f k) integrable_on s" |
6284 assumes "\<And>k. (f k) integrable_on S" |
6290 and "\<forall>k. \<forall>x\<in>s. (f k x) \<le> (f (Suc k) x)" |
6285 and "\<And>k x. x \<in> S \<Longrightarrow> (f k x) \<le> (f (Suc k) x)" |
6291 and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially" |
6286 and "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially" |
6292 and "bounded {integral s (f k)| k. True}" |
6287 and "bounded (range (\<lambda>k. integral S (f k)))" |
6293 shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially" |
6288 shows "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially" |
6294 proof - |
6289 proof - |
6295 have lem: "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially" |
6290 have lem: "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially" |
6296 if "\<forall>k. \<forall>x\<in>s. 0 \<le> f k x" |
6291 if "\<forall>k. \<forall>x\<in>S. 0 \<le> f k x" |
6297 and "\<forall>k. (f k) integrable_on s" |
6292 and "\<forall>k. (f k) integrable_on S" |
6298 and "\<forall>k. \<forall>x\<in>s. f k x \<le> f (Suc k) x" |
6293 and "\<forall>k. \<forall>x\<in>S. f k x \<le> f (Suc k) x" |
6299 and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially" |
6294 and "\<forall>x\<in>S. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially" |
6300 and "bounded {integral s (f k)| k. True}" |
6295 and bou: "bounded (range(\<lambda>k. integral S (f k)))" |
6301 for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g s |
6296 for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g S |
6302 proof - |
6297 proof - |
6303 note assms=that[rule_format] |
6298 note assms=that[rule_format] |
6304 have "\<forall>x\<in>s. \<forall>k. (f k x)\<bullet>1 \<le> (g x)\<bullet>1" |
6299 have "\<forall>x\<in>S. \<forall>k. (f k x)\<bullet>1 \<le> (g x)\<bullet>1" |
6305 apply safe |
6300 apply safe |
6306 apply (rule Lim_component_ge) |
6301 apply (rule Lim_component_ge) |
6307 apply (rule that(4)[rule_format]) |
6302 apply (rule that(4)[rule_format]) |
6308 apply assumption |
6303 apply assumption |
6309 apply (rule trivial_limit_sequentially) |
6304 apply (rule trivial_limit_sequentially) |
6310 unfolding eventually_sequentially |
6305 unfolding eventually_sequentially |
6311 apply (rule_tac x=k in exI) |
6306 apply (rule_tac x=k in exI) |
6312 using assms(3) by (force intro: transitive_stepwise_le) |
6307 using assms(3) by (force intro: transitive_stepwise_le) |
6313 note fg=this[rule_format] |
6308 note fg=this[rule_format] |
6314 |
6309 |
6315 have "\<exists>i. ((\<lambda>k. integral s (f k)) \<longlongrightarrow> i) sequentially" |
6310 obtain i where i: "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> i" |
6316 apply (rule bounded_increasing_convergent) |
6311 using bounded_increasing_convergent [OF bou] |
6317 apply (rule that(5)) |
6312 using \<open>\<forall>k. \<forall>x\<in>S. f k x \<le> f (Suc k) x\<close> assms(2) integral_le by blast |
6318 apply rule |
6313 have "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x" |
6319 apply (rule integral_le) |
|
6320 apply (rule that(2)[rule_format])+ |
|
6321 using that(3) |
|
6322 apply auto |
|
6323 done |
|
6324 then guess i..note i=this |
|
6325 have "\<And>k. \<forall>x\<in>s. \<forall>n\<ge>k. f k x \<le> f n x" |
|
6326 using assms(3) by (force intro: transitive_stepwise_le) |
6314 using assms(3) by (force intro: transitive_stepwise_le) |
6327 then have i': "\<forall>k. (integral s (f k))\<bullet>1 \<le> i\<bullet>1" |
6315 then have i': "\<forall>k. (integral S (f k))\<bullet>1 \<le> i\<bullet>1" |
6328 apply - |
6316 apply - |
6329 apply rule |
6317 apply rule |
6330 apply (rule Lim_component_ge) |
6318 apply (rule Lim_component_ge) |
6331 apply (rule i) |
6319 apply (rule i) |
6332 apply (rule trivial_limit_sequentially) |
6320 apply (rule trivial_limit_sequentially) |
6337 apply simp |
6325 apply simp |
6338 apply (rule that(2)[rule_format])+ |
6326 apply (rule that(2)[rule_format])+ |
6339 apply auto |
6327 apply auto |
6340 done |
6328 done |
6341 |
6329 |
6342 note int = assms(2)[unfolded integrable_alt[of _ s],THEN conjunct1,rule_format] |
6330 note int = assms(2)[unfolded integrable_alt[of _ S],THEN conjunct1,rule_format] |
6343 have ifif: "\<And>k t. (\<lambda>x. if x \<in> t then if x \<in> s then f k x else 0 else 0) = |
6331 have ifif: "\<And>k t. (\<lambda>x. if x \<in> t then if x \<in> S then f k x else 0 else 0) = |
6344 (\<lambda>x. if x \<in> t \<inter> s then f k x else 0)" |
6332 (\<lambda>x. if x \<in> t \<inter> S then f k x else 0)" |
6345 by (rule ext) auto |
6333 by (rule ext) auto |
6346 have int': "\<And>k a b. f k integrable_on cbox a b \<inter> s" |
6334 have int': "\<And>k a b. f k integrable_on cbox a b \<inter> S" |
6347 apply (subst integrable_restrict_UNIV[symmetric]) |
6335 apply (subst integrable_restrict_UNIV[symmetric]) |
6348 apply (subst ifif[symmetric]) |
6336 apply (subst ifif[symmetric]) |
6349 apply (subst integrable_restrict_UNIV) |
6337 apply (subst integrable_restrict_UNIV) |
6350 apply (rule int) |
6338 apply (rule int) |
6351 done |
6339 done |
6352 have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on cbox a b \<and> |
6340 have "\<And>a b. (\<lambda>x. if x \<in> S then g x else 0) integrable_on cbox a b \<and> |
6353 ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) \<longlongrightarrow> |
6341 ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)) \<longlongrightarrow> |
6354 integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0)) sequentially" |
6342 integral (cbox a b) (\<lambda>x. if x \<in> S then g x else 0)) sequentially" |
6355 proof (rule monotone_convergence_interval, safe, goal_cases) |
6343 proof (rule monotone_convergence_interval, safe, goal_cases) |
6356 case 1 |
6344 case 1 |
6357 show ?case by (rule int) |
6345 show ?case by (rule int) |
6358 next |
6346 next |
6359 case (2 _ _ _ x) |
6347 case (2 _ _ _ x) |
6360 then show ?case |
6348 then show ?case |
6361 apply (cases "x \<in> s") |
6349 apply (cases "x \<in> S") |
6362 using assms(3) |
6350 using assms(3) |
6363 apply auto |
6351 apply auto |
6364 done |
6352 done |
6365 next |
6353 next |
6366 case (3 _ _ x) |
6354 case (3 _ _ x) |
6367 then show ?case |
6355 then show ?case |
6368 apply (cases "x \<in> s") |
6356 apply (cases "x \<in> S") |
6369 using assms(4) |
6357 using assms(4) |
6370 apply auto |
6358 apply auto |
6371 done |
6359 done |
6372 next |
6360 next |
6373 case (4 a b) |
6361 case (4 a b) |
6374 note * = integral_nonneg |
6362 note * = integral_nonneg |
6375 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))" |
6363 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))" |
6376 unfolding real_norm_def |
6364 unfolding real_norm_def |
6377 apply (subst abs_of_nonneg) |
6365 apply (subst abs_of_nonneg) |
6378 apply (rule *[OF int]) |
6366 apply (rule *[OF int]) |
6379 apply safe |
6367 apply safe |
6380 apply (case_tac "x \<in> s") |
6368 apply (case_tac "x \<in> S") |
6381 apply (drule assms(1)) |
6369 apply (drule assms(1)) |
6382 prefer 3 |
6370 prefer 3 |
6383 apply (subst abs_of_nonneg) |
6371 apply (subst abs_of_nonneg) |
6384 apply (rule *[OF assms(2) that(1)[THEN spec]]) |
6372 apply (rule *[OF assms(2) that(1)[THEN spec]]) |
6385 apply (subst integral_restrict_UNIV[symmetric,OF int]) |
6373 apply (subst integral_restrict_UNIV[symmetric,OF int]) |
6423 fix a b :: 'n |
6411 fix a b :: 'n |
6424 assume ab: "ball 0 B \<subseteq> cbox a b" |
6412 assume ab: "ball 0 B \<subseteq> cbox a b" |
6425 from \<open>e > 0\<close> have "e/2 > 0" |
6413 from \<open>e > 0\<close> have "e/2 > 0" |
6426 by auto |
6414 by auto |
6427 from LIMSEQ_D [OF g(2)[of a b] this] guess M..note M=this |
6415 from LIMSEQ_D [OF g(2)[of a b] this] guess M..note M=this |
6428 have **: "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f N x else 0) - i) < e/2" |
6416 have **: "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f N x else 0) - i) < e/2" |
6429 apply (rule norm_triangle_half_l) |
6417 apply (rule norm_triangle_half_l) |
6430 using B(2)[rule_format,OF ab] N[rule_format,of N] |
6418 using B(2)[rule_format,OF ab] N[rule_format,of N] |
6431 apply - |
6419 apply - |
6432 defer |
6420 defer |
6433 apply (subst norm_minus_commute) |
6421 apply (subst norm_minus_commute) |
6434 apply auto |
6422 apply auto |
6435 done |
6423 done |
6436 have *: "\<And>f1 f2 g. \<bar>f1 - i\<bar> < e/2 \<longrightarrow> \<bar>f2 - g\<bar> < e/2 \<longrightarrow> |
6424 have *: "\<And>f1 f2 g. \<bar>f1 - i\<bar> < e/2 \<longrightarrow> \<bar>f2 - g\<bar> < e/2 \<longrightarrow> |
6437 f1 \<le> f2 \<longrightarrow> f2 \<le> i \<longrightarrow> \<bar>g - i\<bar> < e" |
6425 f1 \<le> f2 \<longrightarrow> f2 \<le> i \<longrightarrow> \<bar>g - i\<bar> < e" |
6438 unfolding real_inner_1_right by arith |
6426 unfolding real_inner_1_right by arith |
6439 show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0) - i) < e" |
6427 show "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then g x else 0) - i) < e" |
6440 unfolding real_norm_def |
6428 unfolding real_norm_def |
6441 apply (rule *[rule_format]) |
6429 apply (rule *[rule_format]) |
6442 apply (rule **[unfolded real_norm_def]) |
6430 apply (rule **[unfolded real_norm_def]) |
6443 apply (rule M[rule_format,of "M + N",unfolded real_norm_def]) |
6431 apply (rule M[rule_format,of "M + N",unfolded real_norm_def]) |
6444 apply (rule le_add1) |
6432 apply (rule le_add1) |
6445 apply (rule integral_le[OF int int]) |
6433 apply (rule integral_le[OF int int]) |
6446 defer |
6434 defer |
6447 apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]]) |
6435 apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]]) |
6448 proof (safe, goal_cases) |
6436 proof (safe, goal_cases) |
6449 case (2 x) |
6437 case (2 x) |
6450 have "\<And>m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1" |
6438 have "\<And>m. x \<in> S \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1" |
6451 using assms(3) by (force intro: transitive_stepwise_le) |
6439 using assms(3) by (force intro: transitive_stepwise_le) |
6452 then show ?case |
6440 then show ?case |
6453 by auto |
6441 by auto |
6454 next |
6442 next |
6455 case 1 |
6443 case 1 |
6470 using i |
6458 using i |
6471 apply auto |
6459 apply auto |
6472 done |
6460 done |
6473 qed |
6461 qed |
6474 |
6462 |
6475 have sub: "\<And>k. integral s (\<lambda>x. f k x - f 0 x) = integral s (f k) - integral s (f 0)" |
6463 have sub: "\<And>k. integral S (\<lambda>x. f k x - f 0 x) = integral S (f k) - integral S (f 0)" |
6476 apply (subst integral_diff) |
6464 apply (subst integral_diff) |
6477 apply (rule assms(1)[rule_format])+ |
6465 apply (rule assms(1)[rule_format])+ |
6478 apply rule |
6466 apply rule |
6479 done |
6467 done |
6480 have "\<And>x m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. f m x \<le> f n x" |
6468 have "\<And>x m. x \<in> S \<Longrightarrow> \<forall>n\<ge>m. f m x \<le> f n x" |
6481 using assms(2) by (force intro: transitive_stepwise_le) |
6469 using assms(2) by (force intro: transitive_stepwise_le) |
6482 note * = this[rule_format] |
6470 note * = this[rule_format] |
6483 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> |
6471 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> |
6484 integral s (\<lambda>x. g x - f 0 x)) sequentially" |
6472 integral S (\<lambda>x. g x - f 0 x)) sequentially" |
6485 apply (rule lem) |
6473 apply (rule lem) |
6486 apply safe |
6474 apply safe |
6487 proof goal_cases |
6475 proof goal_cases |
6488 case (1 k x) |
6476 case (1 k x) |
6489 then show ?case |
6477 then show ?case |
6545 assumes "x \<longlonglongrightarrow> x'" |
6533 assumes "x \<longlonglongrightarrow> x'" |
6546 shows "(g has_integral x') s" |
6534 shows "(g has_integral x') s" |
6547 proof - |
6535 proof - |
6548 have x_eq: "x = (\<lambda>i. integral s (f i))" |
6536 have x_eq: "x = (\<lambda>i. integral s (f i))" |
6549 by (simp add: integral_unique[OF f]) |
6537 by (simp add: integral_unique[OF f]) |
6550 then have x: "{integral s (f k) |k. True} = range x" |
6538 then have x: "range(\<lambda>k. integral s (f k)) = range x" |
6551 by auto |
6539 by auto |
6552 |
|
6553 have *: "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g" |
6540 have *: "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g" |
6554 proof (intro monotone_convergence_increasing allI ballI assms) |
6541 proof (intro monotone_convergence_increasing allI ballI assms) |
6555 show "bounded {integral s (f k) |k. True}" |
6542 show "bounded (range(\<lambda>k. integral s (f k)))" |
6556 unfolding x by (rule convergent_imp_bounded) fact |
6543 using x convergent_imp_bounded assms by metis |
6557 qed (use f in auto) |
6544 qed (use f in auto) |
6558 then have "integral s g = x'" |
6545 then have "integral s g = x'" |
6559 by (intro LIMSEQ_unique[OF _ \<open>x \<longlonglongrightarrow> x'\<close>]) (simp add: x_eq) |
6546 by (intro LIMSEQ_unique[OF _ \<open>x \<longlonglongrightarrow> x'\<close>]) (simp add: x_eq) |
6560 with * show ?thesis |
6547 with * show ?thesis |
6561 by (simp add: has_integral_integral) |
6548 by (simp add: has_integral_integral) |
6562 qed |
6549 qed |
6563 |
6550 |
6564 lemma monotone_convergence_decreasing: |
6551 lemma monotone_convergence_decreasing: |
6565 fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" |
6552 fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" |
6566 assumes "\<forall>k. (f k) integrable_on s" |
6553 assumes "\<And>k. (f k) integrable_on S" |
6567 and "\<forall>k. \<forall>x\<in>s. f (Suc k) x \<le> f k x" |
6554 and "\<And>k x. x \<in> S \<Longrightarrow> f (Suc k) x \<le> f k x" |
6568 and "\<forall>x\<in>s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially" |
6555 and "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially" |
6569 and "bounded {integral s (f k)| k. True}" |
6556 and "bounded (range(\<lambda>k. integral S (f k)))" |
6570 shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially" |
6557 shows "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially" |
6571 proof - |
6558 proof - |
6572 note assm = assms[rule_format] |
6559 have *: "{integral S (\<lambda>x. - f k x) |k. True} = op *\<^sub>R (- 1) ` (range(\<lambda>k. integral S (f k)))" |
6573 have *: "{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R (- 1) ` {integral s (f k)| k. True}" |
|
6574 apply safe |
6560 apply safe |
6575 unfolding image_iff |
6561 unfolding image_iff |
6576 apply (rule_tac x="integral s (f k)" in bexI) |
6562 apply (rule_tac x="integral S (f k)" in bexI) |
6577 prefer 3 |
6563 prefer 3 |
6578 apply (rule_tac x=k in exI) |
6564 apply (rule_tac x=k in exI) |
6579 apply auto |
6565 apply auto |
6580 done |
6566 done |
6581 have "(\<lambda>x. - g x) integrable_on s \<and> |
6567 have "(\<lambda>x. - g x) integrable_on S \<and> |
6582 ((\<lambda>k. integral s (\<lambda>x. - f k x)) \<longlongrightarrow> integral s (\<lambda>x. - g x)) sequentially" |
6568 ((\<lambda>k. integral S (\<lambda>x. - f k x)) \<longlongrightarrow> integral S (\<lambda>x. - g x)) sequentially" |
6583 apply (rule monotone_convergence_increasing) |
6569 proof (rule monotone_convergence_increasing) |
6584 apply safe |
6570 show "\<And>k. (\<lambda>x. - f k x) integrable_on S" |
6585 apply (rule integrable_neg) |
6571 by (blast intro: integrable_neg assms) |
6586 apply (rule assm) |
6572 show "\<And>k x. x \<in> S \<Longrightarrow> - f k x \<le> - f (Suc k) x" |
6587 defer |
6573 by (simp add: assms) |
6588 apply (rule tendsto_minus) |
6574 show "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>k. - f k x) \<longlonglongrightarrow> - g x" |
6589 apply (rule assm) |
6575 by (simp add: assms tendsto_minus) |
6590 apply assumption |
6576 show "bounded (range(\<lambda>k. integral S (\<lambda>x. - f k x)))" |
6591 unfolding * |
6577 using "*" assms(4) bounded_scaling by auto |
6592 apply (rule bounded_scaling) |
6578 qed |
6593 using assm |
6579 then show ?thesis |
6594 apply auto |
6580 by (force dest: integrable_neg tendsto_minus) |
6595 done |
|
6596 note * = conjunctD2[OF this] |
|
6597 show ?thesis |
|
6598 using integrable_neg[OF *(1)] tendsto_minus[OF *(2)] |
|
6599 by auto |
|
6600 qed |
6581 qed |
6601 |
6582 |
6602 lemma integral_norm_bound_integral: |
6583 lemma integral_norm_bound_integral: |
6603 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
6584 fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach" |
6604 assumes int_f: "f integrable_on S" |
6585 assumes int_f: "f integrable_on S" |
7551 exp (- (a * c)) / a - exp (- (a * real k)) / a" |
7532 exp (- (a * c)) / a - exp (- (a * real k)) / a" |
7552 using False a by (intro abs_of_nonneg) (simp_all add: field_simps) |
7533 using False a by (intro abs_of_nonneg) (simp_all add: field_simps) |
7553 also have "\<dots> \<le> exp (- a * c) / a" using a by simp |
7534 also have "\<dots> \<le> exp (- a * c) / a" using a by simp |
7554 finally show ?thesis . |
7535 finally show ?thesis . |
7555 qed (insert a, simp_all add: integral_f) |
7536 qed (insert a, simp_all add: integral_f) |
7556 thus "bounded {integral {c..} (f k) |k. True}" |
7537 thus "bounded (range(\<lambda>k. integral {c..} (f k)))" |
7557 by (intro boundedI[of _ "exp (-a*c)/a"]) auto |
7538 by (intro boundedI[of _ "exp (-a*c)/a"]) auto |
7558 qed (auto simp: f_def) |
7539 qed (auto simp: f_def) |
7559 |
7540 |
7560 from eventually_gt_at_top[of "nat \<lceil>c\<rceil>"] have "eventually (\<lambda>k. of_nat k > c) sequentially" |
7541 from eventually_gt_at_top[of "nat \<lceil>c\<rceil>"] have "eventually (\<lambda>k. of_nat k > c) sequentially" |
7561 by eventually_elim linarith |
7542 by eventually_elim linarith |
7644 also from a have "F k \<ge> 0" |
7625 also from a have "F k \<ge> 0" |
7645 by (auto simp: F_def divide_simps simp del: of_nat_Suc intro!: powr_mono2) |
7626 by (auto simp: F_def divide_simps simp del: of_nat_Suc intro!: powr_mono2) |
7646 hence "F k = abs (F k)" by simp |
7627 hence "F k = abs (F k)" by simp |
7647 finally have "abs (F k) \<le> c powr (a + 1) / (a + 1)" . |
7628 finally have "abs (F k) \<le> c powr (a + 1) / (a + 1)" . |
7648 } |
7629 } |
7649 thus "bounded {integral {0..c} (f k) |k. True}" |
7630 thus "bounded (range(\<lambda>k. integral {0..c} (f k)))" |
7650 by (intro boundedI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f) |
7631 by (intro boundedI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f) |
7651 qed |
7632 qed |
7652 |
7633 |
7653 from False c have "c > 0" by simp |
7634 from False c have "c > 0" by simp |
7654 from order_tendstoD(2)[OF LIMSEQ_inverse_real_of_nat this] |
7635 from order_tendstoD(2)[OF LIMSEQ_inverse_real_of_nat this] |
7730 case True |
7711 case True |
7731 with assms have "a powr (e + 1) \<ge> n powr (e + 1)" |
7712 with assms have "a powr (e + 1) \<ge> n powr (e + 1)" |
7732 by (intro powr_mono2') simp_all |
7713 by (intro powr_mono2') simp_all |
7733 with assms show ?thesis by (auto simp: divide_simps F_def integral_f) |
7714 with assms show ?thesis by (auto simp: divide_simps F_def integral_f) |
7734 qed (insert assms, simp add: integral_f F_def divide_simps) |
7715 qed (insert assms, simp add: integral_f F_def divide_simps) |
7735 thus "bounded {integral {a..} (f n) |n. True}" |
7716 thus "bounded (range(\<lambda>k. integral {a..} (f k)))" |
7736 unfolding bounded_iff by (intro exI[of _ "-F a"]) auto |
7717 unfolding bounded_iff by (intro exI[of _ "-F a"]) auto |
7737 qed |
7718 qed |
7738 |
7719 |
7739 from filterlim_real_sequentially |
7720 from filterlim_real_sequentially |
7740 have "eventually (\<lambda>n. real n \<ge> a) at_top" |
7721 have "eventually (\<lambda>n. real n \<ge> a) at_top" |