author immler Thu Sep 24 14:29:08 2015 +0200 (2015-09-24) changeset 61243 44b2d133063e parent 61238 e3d8a313a649 child 61244 6026c14f5e5d
exchange uniform limit and integral
```     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Sep 23 14:11:35 2015 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Sep 24 14:29:08 2015 +0200
1.3 @@ -7,6 +7,7 @@
1.4  theory Integration
1.5  imports
1.6    Derivative
1.7 +  Uniform_Limit
1.8    "~~/src/HOL/Library/Indicator_Function"
1.9  begin
1.10
1.11 @@ -11609,6 +11610,73 @@
1.12  qed auto
1.13
1.14
1.15 +subsection \<open>Exchange uniform limit and integral\<close>
1.16 +
1.17 +lemma
1.18 +  uniform_limit_integral:
1.19 +  fixes f::"'a \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::banach"
1.20 +  assumes u: "uniform_limit (cbox a b) f g F"
1.21 +  assumes c: "\<And>n. continuous_on (cbox a b) (f n)"
1.22 +  assumes [simp]: "F \<noteq> bot"
1.23 +  obtains I J where
1.24 +    "\<And>n. (f n has_integral I n) (cbox a b)"
1.25 +    "(g has_integral J) (cbox a b)"
1.26 +    "(I ---> J) F"
1.27 +proof -
1.28 +  have fi[simp]: "f n integrable_on (cbox a b)" for n
1.29 +    by (auto intro!: integrable_continuous assms)
1.30 +  then obtain I where I: "\<And>n. (f n has_integral I n) (cbox a b)"
1.31 +    by atomize_elim (auto simp: integrable_on_def intro!: choice)
1.32 +
1.33 +  moreover
1.34 +
1.35 +  have gi[simp]: "g integrable_on (cbox a b)"
1.36 +    by (auto intro!: integrable_continuous uniform_limit_theorem[OF _ u] eventuallyI c)
1.37 +  then obtain J where J: "(g has_integral J) (cbox a b)"
1.38 +    by blast
1.39 +
1.40 +  moreover
1.41 +
1.42 +  have "(I ---> J) F"
1.43 +  proof cases
1.44 +    assume "content (cbox a b) = 0"
1.45 +    hence "I = (\<lambda>_. 0)" "J = 0"
1.46 +      by (auto intro!: has_integral_unique I J)
1.47 +    thus ?thesis by simp
1.48 +  next
1.49 +    assume content_nonzero: "content (cbox a b) \<noteq> 0"
1.50 +    show ?thesis
1.51 +    proof (rule tendstoI)
1.52 +      fix e::real
1.53 +      assume "e > 0"
1.54 +      def e' \<equiv> "e / 2"
1.55 +      with \<open>e > 0\<close> have "e' > 0" by simp
1.56 +      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)"
1.57 +        using u content_nonzero content_pos_le[of a b]
1.58 +        by (auto simp: uniform_limit_iff dist_norm)
1.59 +      then show "\<forall>\<^sub>F n in F. dist (I n) J < e"
1.60 +      proof eventually_elim
1.61 +        case (elim n)
1.62 +        have "I n = integral (cbox a b) (f n)"
1.63 +            "J = integral (cbox a b) g"
1.64 +          using I[of n] J by (simp_all add: integral_unique)
1.65 +        then have "dist (I n) J = norm (integral (cbox a b) (\<lambda>x. f n x - g x))"
1.66 +          by (simp add: integral_sub dist_norm)
1.67 +        also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. (e' / content (cbox a b)))"
1.68 +          using elim
1.69 +          by (intro integral_norm_bound_integral)
1.70 +            (auto intro!: integrable_sub absolutely_integrable_onI)
1.71 +        also have "\<dots> < e"
1.72 +          using \<open>0 < e\<close>
1.73 +          by (simp add: e'_def)
1.74 +        finally show ?case .
1.75 +      qed
1.76 +    qed
1.77 +  qed
1.78 +  ultimately show ?thesis ..
1.79 +qed
1.80 +
1.81 +
1.82  subsection \<open>Dominated convergence\<close>
1.83
1.84  (* GENERALIZE the following theorems *)
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Wed Sep 23 14:11:35 2015 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Thu Sep 24 14:29:08 2015 +0200
2.3 @@ -6,7 +6,6 @@
2.4    Ordered_Euclidean_Space
2.5    Complex_Analysis_Basics
2.6    Bounded_Continuous_Function
2.7 -  Uniform_Limit
2.8    Weierstrass
2.9  begin
2.10
```