11607 done |
11608 done |
11608 qed |
11609 qed |
11609 qed auto |
11610 qed auto |
11610 |
11611 |
11611 |
11612 |
|
11613 subsection \<open>Exchange uniform limit and integral\<close> |
|
11614 |
|
11615 lemma |
|
11616 uniform_limit_integral: |
|
11617 fixes f::"'a \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::banach" |
|
11618 assumes u: "uniform_limit (cbox a b) f g F" |
|
11619 assumes c: "\<And>n. continuous_on (cbox a b) (f n)" |
|
11620 assumes [simp]: "F \<noteq> bot" |
|
11621 obtains I J where |
|
11622 "\<And>n. (f n has_integral I n) (cbox a b)" |
|
11623 "(g has_integral J) (cbox a b)" |
|
11624 "(I ---> J) F" |
|
11625 proof - |
|
11626 have fi[simp]: "f n integrable_on (cbox a b)" for n |
|
11627 by (auto intro!: integrable_continuous assms) |
|
11628 then obtain I where I: "\<And>n. (f n has_integral I n) (cbox a b)" |
|
11629 by atomize_elim (auto simp: integrable_on_def intro!: choice) |
|
11630 |
|
11631 moreover |
|
11632 |
|
11633 have gi[simp]: "g integrable_on (cbox a b)" |
|
11634 by (auto intro!: integrable_continuous uniform_limit_theorem[OF _ u] eventuallyI c) |
|
11635 then obtain J where J: "(g has_integral J) (cbox a b)" |
|
11636 by blast |
|
11637 |
|
11638 moreover |
|
11639 |
|
11640 have "(I ---> J) F" |
|
11641 proof cases |
|
11642 assume "content (cbox a b) = 0" |
|
11643 hence "I = (\<lambda>_. 0)" "J = 0" |
|
11644 by (auto intro!: has_integral_unique I J) |
|
11645 thus ?thesis by simp |
|
11646 next |
|
11647 assume content_nonzero: "content (cbox a b) \<noteq> 0" |
|
11648 show ?thesis |
|
11649 proof (rule tendstoI) |
|
11650 fix e::real |
|
11651 assume "e > 0" |
|
11652 def e' \<equiv> "e / 2" |
|
11653 with \<open>e > 0\<close> have "e' > 0" by simp |
|
11654 then have "\<forall>\<^sub>F n in F. \<forall>x\<in>cbox a b. norm (f n x - g x) < e' / content (cbox a b)" |
|
11655 using u content_nonzero content_pos_le[of a b] |
|
11656 by (auto simp: uniform_limit_iff dist_norm) |
|
11657 then show "\<forall>\<^sub>F n in F. dist (I n) J < e" |
|
11658 proof eventually_elim |
|
11659 case (elim n) |
|
11660 have "I n = integral (cbox a b) (f n)" |
|
11661 "J = integral (cbox a b) g" |
|
11662 using I[of n] J by (simp_all add: integral_unique) |
|
11663 then have "dist (I n) J = norm (integral (cbox a b) (\<lambda>x. f n x - g x))" |
|
11664 by (simp add: integral_sub dist_norm) |
|
11665 also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. (e' / content (cbox a b)))" |
|
11666 using elim |
|
11667 by (intro integral_norm_bound_integral) |
|
11668 (auto intro!: integrable_sub absolutely_integrable_onI) |
|
11669 also have "\<dots> < e" |
|
11670 using \<open>0 < e\<close> |
|
11671 by (simp add: e'_def) |
|
11672 finally show ?case . |
|
11673 qed |
|
11674 qed |
|
11675 qed |
|
11676 ultimately show ?thesis .. |
|
11677 qed |
|
11678 |
|
11679 |
11612 subsection \<open>Dominated convergence\<close> |
11680 subsection \<open>Dominated convergence\<close> |
11613 |
11681 |
11614 (* GENERALIZE the following theorems *) |
11682 (* GENERALIZE the following theorems *) |
11615 |
11683 |
11616 lemma dominated_convergence: |
11684 lemma dominated_convergence: |