exchange uniform limit and integral
authorimmler
Thu Sep 24 14:29:08 2015 +0200 (2015-09-24)
changeset 6124344b2d133063e
parent 61238 e3d8a313a649
child 61244 6026c14f5e5d
exchange uniform limit and integral
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
     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