author paulson Tue, 15 Aug 2017 22:22:34 +0100 changeset 66440 a6ec6c806a6c parent 66436 36a01c02d0ca (current diff) parent 66439 1a93b480fec8 (diff) child 66441 b9468503742a
merged
```--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Aug 15 22:23:28 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Aug 15 22:22:34 2017 +0100
@@ -2089,40 +2089,35 @@
qed
finally show ?case .
next
-        note f' = f_int[of a b, unfolded absolutely_integrable_on_def]
-        note f = f'[THEN conjunct1] f'[THEN conjunct2]
-        note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
have "e/2>0"
using \<open>e > 0\<close> by auto
-        from * [OF this] obtain d1 where
-          d1: "gauge d1" "\<forall>p. p tagged_division_of (cbox a b) \<and> d1 fine p \<longrightarrow>
+        moreover
+        have f: "f integrable_on cbox a b" "(\<lambda>x. norm (f x)) integrable_on cbox a b"
+          using f_int by (auto simp: absolutely_integrable_on_def)
+        ultimately obtain d1 where "gauge d1"
+           and d1: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d1 fine p\<rbrakk> \<Longrightarrow>
norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e/2"
-          by auto
-        from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
-          d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
-            (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2" .
-         obtain p where
+          unfolding has_integral_integral has_integral by meson
+        obtain d2 where "gauge d2"
+          and d2: "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox a b); d2 fine p\<rbrakk> \<Longrightarrow>
+            (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
+          by (blast intro: henstock_lemma [OF f(1) \<open>e/2>0\<close>])
+        obtain p where
p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
-          by (rule fine_division_exists [OF gauge_Int [OF d1(1) d2(1)], of a b])
+          by (rule fine_division_exists [OF gauge_Int [OF \<open>gauge d1\<close> \<open>gauge d2\<close>], of a b])
-        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e/2 \<longrightarrow>
-          \<bar>sf' - di\<bar> < e/2 \<longrightarrow> di < ?S + e"
+        have *: "\<And>sf sf' si di. \<lbrakk>sf' = sf; si \<le> ?S; \<bar>sf - si\<bar> < e/2;
+                      \<bar>sf' - di\<bar> < e/2\<rbrakk> \<Longrightarrow> di < ?S + e"
by arith
-        show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
-          apply (subst if_P)
-          apply rule
-        proof (rule *[rule_format])
+        have "integral (cbox a b) (\<lambda>x. norm (f x)) < ?S + e"
+        proof (rule *)
show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e/2"
unfolding split_def
apply (rule absdiff_norm_less)
-            using d2(2)[rule_format,of p]
-            using p(1,3)
-            unfolding tagged_division_of_def split_def
-            apply auto
+            using d2[of p] p(1,3) apply (auto simp: tagged_division_of_def split_def)
done
show "\<bar>(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e/2"
-            using d1(2)[rule_format,OF conjI[OF p(1,2)]]
-            by (simp only: real_norm_def)
+            using d1[OF p(1,2)] by (simp only: real_norm_def)
show "(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) = (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x))"
apply (rule sum.cong)
apply (rule refl)
@@ -2133,10 +2128,12 @@
using partial_division_of_tagged_division[of p "cbox a b"] p(1)
apply (subst sum.over_tagged_division_lemma[OF p(1)])
-            apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
+            apply (intro cSUP_upper2 D)
apply (auto simp: tagged_partial_division_of_def)
done
qed
+        then show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
+          by simp
qed
qed (insert K, auto)
qed```
```--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Aug 15 22:23:28 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Aug 15 22:22:34 2017 +0100
@@ -5670,10 +5670,10 @@
assumes "f integrable_on cbox a b"
and "e > 0"
and "gauge d"
-    and "(\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
-      norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral(cbox a b) f) < e)"
+    and less_e: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d fine p\<rbrakk> \<Longrightarrow>
+                     norm (sum (\<lambda>(x,K). content K *\<^sub>R f x) p - integral(cbox a b) f) < e"
and p: "p tagged_partial_division_of (cbox a b)" "d fine p"
-  shows "norm (sum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e"
+  shows "norm (sum (\<lambda>(x,K). content K *\<^sub>R f x - integral K f) p) \<le> e"
(is "?x \<le> e")
proof -
{ presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" then show ?thesis by (blast intro: field_le_epsilon) }
@@ -5720,15 +5720,9 @@

let ?p = "p \<union> \<Union>(qq ` r)"
have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral (cbox a b) f) < e"
-    apply (rule assms(4)[rule_format])
-  proof
+  proof (rule less_e)
show "d fine ?p"
-      apply (rule fine_Un)
-      apply (rule p)
-      apply (rule fine_Union)
-      using qq
-      apply auto
-      done
+      by (metis (mono_tags, hide_lams) qq fine_Un fine_Union imageE p(2))
note * = tagged_partial_division_of_union_self[OF p(1)]
have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
using r
@@ -5902,53 +5896,55 @@

lemma henstock_lemma_part2:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
-  assumes "f integrable_on cbox a b"
-    and "e > 0"
-    and "gauge d"
-    and "\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
-      norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral (cbox a b) f) < e"
-    and "p tagged_partial_division_of (cbox a b)"
+  assumes fed: "f integrable_on cbox a b" "e > 0" "gauge d"
+    and less_e: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d fine p\<rbrakk> \<Longrightarrow>
+                     norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral (cbox a b) f) < e"
+    and tag: "p tagged_partial_division_of (cbox a b)"
and "d fine p"
shows "sum (\<lambda>(x,k). norm (content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (DIM('n)) * e"
-  unfolding split_def
-  apply (rule sum_norm_allsubsets_bound)
-  defer
-  apply (rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)])
-  apply safe
-  apply (rule assms[rule_format,unfolded split_def])
-  defer
-  apply (rule tagged_partial_division_subset)
-  apply (rule assms)
-  apply assumption
-  apply (rule fine_subset)
-  apply assumption
-  apply (rule assms)
-  using assms(5)
-  apply auto
-  done
+proof -
+  have "finite p"
+    using tag by blast
+  then show ?thesis
+    unfolding split_def
+  proof (rule sum_norm_allsubsets_bound)
+    fix Q
+    assume Q: "Q \<subseteq> p"
+    then have fine: "d fine Q"
+      by (simp add: \<open>d fine p\<close> fine_subset)
+    show "norm (\<Sum>x\<in>Q. content (snd x) *\<^sub>R f (fst x) - integral (snd x) f) \<le> e"
+      apply (rule henstock_lemma_part1[OF fed less_e, unfolded split_def])
+      using Q tag tagged_partial_division_subset apply (force simp add: fine)+
+      done
+  qed
+qed

lemma henstock_lemma:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
-  assumes "f integrable_on cbox a b"
+  assumes intf: "f integrable_on cbox a b"
and "e > 0"
-  obtains d where "gauge d"
-    and "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d fine p \<longrightarrow>
-      sum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
+  obtains \<gamma> where "gauge \<gamma>"
+    and "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox a b); \<gamma> fine p\<rbrakk> \<Longrightarrow>
+             sum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
proof -
-  have *: "e / (2 * (real DIM('n) + 1)) > 0" using assms(2) by simp
-  from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this]
-  guess d..note d = conjunctD2[OF this]
+  have *: "e / (2 * (real DIM('n) + 1)) > 0" using \<open>e > 0\<close> by simp
+  with integrable_integral[OF intf, unfolded has_integral]
+  obtain \<gamma> where "gauge \<gamma>"
+    and \<gamma>: "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma> fine p\<rbrakk> \<Longrightarrow>
+         norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral (cbox a b) f)
+         < e / (2 * (real DIM('n) + 1))"
+    by metis
show thesis
-    apply (rule that)
-    apply (rule d)
-  proof (safe, goal_cases)
-    case (1 p)
-    note * = henstock_lemma_part2[OF assms(1) * d this]
-    show ?case
-      apply (rule le_less_trans[OF *])
-      using \<open>e > 0\<close>
-      apply (auto simp add: field_simps)
-      done
+  proof (rule that [OF \<open>gauge \<gamma>\<close>])
+    fix p
+    assume p: "p tagged_partial_division_of cbox a b" "\<gamma> fine p"
+    have "(\<Sum>(x,K)\<in>p. norm (content K *\<^sub>R f x - integral K f))
+          \<le> 2 * real DIM('n) * (e / (2 * (real DIM('n) + 1)))"
+      using henstock_lemma_part2[OF intf * \<open>gauge \<gamma>\<close> \<gamma> p] by metis
+    also have "... < e"
+      using \<open>e > 0\<close> by (auto simp add: field_simps)
+    finally
+    show "(\<Sum>(x,K)\<in>p. norm (content K *\<^sub>R f x - integral K f)) < e" .
qed
qed

@@ -6118,30 +6114,19 @@
done
fix t
assume "t \<in> {0..s}"
-            show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x -
-              integral k (f (m x))) \<le> e/2 ^ (t + 2)"
-              apply (rule order_trans
-                [of _ "norm (sum (\<lambda>(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \<in> p. m (fst xk) = t})"])
-              apply (rule eq_refl)
-              apply (rule arg_cong[where f=norm])
-              apply (rule sum.cong)
-              apply (rule refl)
-              defer
-              apply (rule henstock_lemma_part1)
-              apply (rule assms(1)[rule_format])
-              apply safe
-              apply (rule c)+
-              apply assumption+
-              apply (rule tagged_partial_division_subset[of p])
-              apply (rule p(1)[unfolded tagged_division_of_def,THEN conjunct1])
-              defer
-              unfolding fine_def
-              apply safe
-              apply (drule p(2)[unfolded fine_def,rule_format])
-              unfolding d_def
-              apply auto
-              done
+            have "norm (\<Sum>(x,k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - integral k (f (m x))) =
+                  norm (\<Sum>(x,k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f t x - integral k (f t))"
+              by (force intro!: sum.cong arg_cong[where f=norm])
+            also have "... \<le> e/2 ^ (t + 2)"
+            proof (rule henstock_lemma_part1 [OF intf _ c])
+              show "{xk \<in> p. m (fst xk) = t} tagged_partial_division_of cbox a b"
+                apply (rule tagged_partial_division_subset[of p])
+                using p by (auto simp: tagged_division_of_def)
+              show "c t fine {xk \<in> p. m (fst xk) = t}"
+                using p(2) by (auto simp: fine_def d_def)
+            qed (auto simp: e)
+            finally show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x -
+              integral k (f (m x))) \<le> e/2 ^ (t + 2)" .
qed
qed (insert s, auto)
next```