author haftmann Mon, 17 Mar 2014 18:06:59 +0100 changeset 56180 fae7a45d0fef parent 56179 6b5c46582260 child 56181 2aa0b19e74f3
tuned proofs
```--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 17 17:35:39 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 17 18:06:59 2014 +0100
@@ -11679,13 +11679,18 @@
then show False
using goal2 by auto
qed
-    then guess K .. note * = this[unfolded image_iff not_le]
-    from this(1) guess d .. note this[unfolded mem_Collect_eq]
+    then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
+      "SUPR {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
+      by (auto simp add: image_iff not_le)
+    from this(1) obtain d where "d division_of \<Union>d"
+      and "K = (\<Sum>k\<in>d. norm (integral k f))"
+      by auto
note d = this(1) *(2)[unfolded this(2)]
note d'=division_ofD[OF this(1)]
have "bounded (\<Union>d)"
by (rule elementary_bounded,fact)
-    from this[unfolded bounded_pos] guess K .. note K=conjunctD2[OF this]
+    from this[unfolded bounded_pos] obtain K where
+       K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
show ?case
apply (rule_tac x="K + 1" in exI)
apply safe
@@ -11742,10 +11747,18 @@
note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
have "e/2>0"
using `e > 0` by auto
-        from *[OF this] guess d1 .. note d1=conjunctD2[OF this]
-        from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this
-        from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p .
-        note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
+        from * [OF this] obtain d1 where
+          d1: "gauge d1" "\<forall>p. p tagged_division_of {a..b} \<and> d1 fine p \<longrightarrow>
+            norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral {a..b} (\<lambda>x. norm (f x))) < e / 2"
+          by auto
+        from henstock_lemma [OF f(1) `e/2>0`] obtain d2 where
+          d2: "gauge d2" "\<forall>p. p tagged_partial_division_of {a..b} \<and> d2 fine p \<longrightarrow>
+            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
+          by blast
+        obtain p where
+          p: "p tagged_division_of {a..b}" "d1 fine p" "d2 fine p"
+          by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])