author paulson Sat, 13 Jun 2015 00:33:14 +0100 changeset 60435 35c6e2daa397 parent 60434 b050b557dbbe child 60436 77e694c0c919 child 60440 3c6acb281c38
proof tidying
```--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jun 12 08:53:23 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sat Jun 13 00:33:14 2015 +0100
@@ -3036,18 +3036,30 @@

lemma has_integral_split:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "(f has_integral i) (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
-    and "(f has_integral j) (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
-    and k: "k \<in> Basis"
+  assumes fi: "(f has_integral i) (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
+      and fj: "(f has_integral j) (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+      and k: "k \<in> Basis"
shows "(f has_integral (i + j)) (cbox a b)"
proof (unfold has_integral, rule, rule)
case goal1
then have e: "e/2 > 0"
by auto
-  guess d1 using has_integralD[OF assms(1)[unfolded interval_split[OF k]] e] .
-  note d1=this[unfolded interval_split[symmetric,OF k]]
-  guess d2 using has_integralD[OF assms(2)[unfolded interval_split[OF k]] e] .
-  note d2=this[unfolded interval_split[symmetric,OF k]]
+    obtain d1
+    where d1: "gauge d1"
+      and d1norm:
+        "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c};
+               d1 fine p\<rbrakk> \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - i) < e / 2"
+       apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e])
+       apply (simp add: interval_split[symmetric] k)
+       done
+    obtain d2
+    where d2: "gauge d2"
+      and d2norm:
+        "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k};
+               d2 fine p\<rbrakk> \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - j) < e / 2"
+       apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e])
+       apply (simp add: interval_split[symmetric] k)
+       done
let ?d = "\<lambda>x. if x\<bullet>k = c then (d1 x \<inter> d2 x) else ball x (abs(x\<bullet>k - c)) \<inter> d1 x \<inter> d2 x"
show ?case
apply (rule_tac x="?d" in exI)
@@ -3062,57 +3074,56 @@
fix p
assume "p tagged_division_of (cbox a b)" "?d fine p"
note p = this tagged_division_ofD[OF this(1)]
-    have lem0:
-      "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<le> c"
+    have xk_le_c: "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<le> c"
+    proof -
+      fix x kk
+      assume as: "(x, kk) \<in> p" and *: "kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}"
+      show "x\<bullet>k \<le> c"
+      proof (rule ccontr)
+        assume **: "\<not> ?thesis"
+        from this[unfolded not_le]
+        have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
+          using p(2)[unfolded fine_def, rule_format,OF as,unfolded split_conv] by auto
+        with * have "\<exists>y. y \<in> ball x \<bar>x \<bullet> k - c\<bar> \<inter> {x. x \<bullet> k \<le> c}"
+          by blast
+        then guess y ..
+        then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<le> c"
+          apply -
+          apply (rule le_less_trans)
+          using Basis_le_norm[OF k, of "x - y"]
+          apply (auto simp add: dist_norm inner_diff_left)
+          done
+        then show False
+          using **[unfolded not_le] by (auto simp add: field_simps)
+      qed
+    qed
+    have xk_ge_c:
"\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<ge> c"
proof -
fix x kk
-      assume as: "(x, kk) \<in> p"
-      {
-        assume *: "kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}"
-        show "x\<bullet>k \<le> c"
-        proof (rule ccontr)
-          assume **: "\<not> ?thesis"
-          from this[unfolded not_le]
-          have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
-            using p(2)[unfolded fine_def, rule_format,OF as,unfolded split_conv] by auto
-          with * have "\<exists>y. y \<in> ball x \<bar>x \<bullet> k - c\<bar> \<inter> {x. x \<bullet> k \<le> c}"
-            by blast
-          then guess y ..
-          then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<le> c"
-            apply -
-            apply (rule le_less_trans)
-            using Basis_le_norm[OF k, of "x - y"]
-            apply (auto simp add: dist_norm inner_diff_left)
-            done
-          then show False
-            using **[unfolded not_le] by (auto simp add: field_simps)
-        qed
-      next
-        assume *: "kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}"
-        show "x\<bullet>k \<ge> c"
-        proof (rule ccontr)
-          assume **: "\<not> ?thesis"
-          from this[unfolded not_le] have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
-            using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
-          with * have "\<exists>y. y \<in> ball x \<bar>x \<bullet> k - c\<bar> \<inter> {x. x \<bullet> k \<ge> c}"
-            by blast
-          then guess y ..
-          then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<ge> c"
-            apply -
-            apply (rule le_less_trans)
-            using Basis_le_norm[OF k, of "x - y"]
-            apply (auto simp add: dist_norm inner_diff_left)
-            done
-          then show False
-            using **[unfolded not_le] by (auto simp add: field_simps)
-        qed
-      }
+      assume as: "(x, kk) \<in> p" and *: "kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}"
+      show "x\<bullet>k \<ge> c"
+      proof (rule ccontr)
+        assume **: "\<not> ?thesis"
+        from this[unfolded not_le] have "kk \<subseteq> ball x \<bar>x \<bullet> k - c\<bar>"
+          using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
+        with * have "\<exists>y. y \<in> ball x \<bar>x \<bullet> k - c\<bar> \<inter> {x. x \<bullet> k \<ge> c}"
+          by blast
+        then guess y ..
+        then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<ge> c"
+          apply -
+          apply (rule le_less_trans)
+          using Basis_le_norm[OF k, of "x - y"]
+          apply (auto simp add: dist_norm inner_diff_left)
+          done
+        then show False
+          using **[unfolded not_le] by (auto simp add: field_simps)
+      qed
qed

have lem1: "\<And>f P Q. (\<forall>x k. (x, k) \<in> {(x, f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow>
(\<forall>x k. P x k \<longrightarrow> Q x (f k))" by auto
-    have lem2: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
+    have fin_finite: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
proof -
case goal1
then have "finite ((\<lambda>(x, k). (x, f k)) ` s)"
@@ -3120,50 +3131,38 @@
then show ?case
by (rule rev_finite_subset) auto
qed
-    have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
-      setsum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} =
-      setsum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)"
-      apply (rule setsum.mono_neutral_left)
-      prefer 3
-    proof
-      fix g :: "'a set \<Rightarrow> 'a set"
+    { fix g :: "'a set \<Rightarrow> 'a set"
fix i :: "'a \<times> 'a set"
assume "i \<in> (\<lambda>(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
then obtain x k where xk:
-        "i = (x, g k)"
-        "(x, k) \<in> p"
-        "(x, g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
-        by auto
+              "i = (x, g k)"  "(x, k) \<in> p"
+              "(x, g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
+          by auto
have "content (g k) = 0"
using xk using content_empty by auto
-      then show "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0"
+      then have "(\<lambda>(x, k). content k *\<^sub>R f x) i = 0"
unfolding xk split_conv by auto
-    qed auto
-    have lem4: "\<And>g. (\<lambda>(x,l). content (g l) *\<^sub>R f x) = (\<lambda>(x,l). content l *\<^sub>R f x) \<circ> (\<lambda>(x,l). (x,g l))"
-      by auto
-
+    } note [simp] = this
+    have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
+                  setsum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} =
+                  setsum (\<lambda>(x, k). content k *\<^sub>R f x) ((\<lambda>(x, k). (x, g k)) ` p)"
+      by (rule setsum.mono_neutral_left) auto
let ?M1 = "{(x, kk \<inter> {x. x\<bullet>k \<le> c}) |x kk. (x, kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
+    have d1_fine: "d1 fine ?M1"
+      by (force intro: fineI dest: fineD[OF p(2)] simp add: split: split_if_asm)
have "norm ((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) < e/2"
-      apply (rule d1(2),rule tagged_division_ofI)
-      apply (rule lem2 p(3))+
-      prefer 6
-      apply (rule fineI)
-    proof -
+    proof (rule d1norm [OF tagged_division_ofI d1_fine])
+      show "finite ?M1"
+        by (rule fin_finite p(3))+
show "\<Union>{k. \<exists>x. (x, k) \<in> ?M1} = cbox a b \<inter> {x. x\<bullet>k \<le> c}"
unfolding p(8)[symmetric] by auto
fix x l
assume xl: "(x, l) \<in> ?M1"
then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this
-      have "l' \<subseteq> d1 x'"
-        apply (rule order_trans[OF fineD[OF p(2) xl'(3)]])
-        apply auto
-        done
-      then show "l \<subseteq> d1 x"
-        unfolding xl' by auto
show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<le> c}"
unfolding xl'
using p(4-6)[OF xl'(3)] using xl'(4)
-        using lem0(1)[OF xl'(3-4)] by auto
+        using xk_le_c[OF xl'(3-4)] by auto
show "\<exists>a b. l = cbox a b"
unfolding xl'
using p(6)[OF xl'(3)]
@@ -3188,26 +3187,20 @@
qed
moreover
let ?M2 = "{(x,kk \<inter> {x. x\<bullet>k \<ge> c}) |x kk. (x,kk) \<in> p \<and> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
+    have d2_fine: "d2 fine ?M2"
+      by (force intro: fineI dest: fineD[OF p(2)] simp add: split: split_if_asm)
have "norm ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) < e/2"
-      apply (rule d2(2),rule tagged_division_ofI)
-      apply (rule lem2 p(3))+
-      prefer 6
-      apply (rule fineI)
-    proof -
+    proof (rule d2norm [OF tagged_division_ofI d2_fine])
+      show "finite ?M2"
+        by (rule fin_finite p(3))+
show "\<Union>{k. \<exists>x. (x, k) \<in> ?M2} = cbox a b \<inter> {x. x\<bullet>k \<ge> c}"
unfolding p(8)[symmetric] by auto
fix x l
assume xl: "(x, l) \<in> ?M2"
then guess x' l' unfolding mem_Collect_eq unfolding Pair_eq by (elim exE conjE) note xl'=this
-      have "l' \<subseteq> d2 x'"
-        apply (rule order_trans[OF fineD[OF p(2) xl'(3)]])
-        apply auto
-        done
-      then show "l \<subseteq> d2 x"
-        unfolding xl' by auto
show "x \<in> l" "l \<subseteq> cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
unfolding xl'
-        using p(4-6)[OF xl'(3)] xl'(4) lem0(2)[OF xl'(3-4)]
+        using p(4-6)[OF xl'(3)] xl'(4) xk_ge_c[OF xl'(3-4)]
by auto
show "\<exists>a b. l = cbox a b"
unfolding xl'
@@ -3235,46 +3228,24 @@
have "norm (((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j)) < e/2 + e/2"
also {
-      have *: "\<And>x y. x = (0::real) \<Longrightarrow> x *\<^sub>R (y::'b) = 0"
+      have eq0: "\<And>x y. x = (0::real) \<Longrightarrow> x *\<^sub>R (y::'b) = 0"
using scaleR_zero_left by auto
+      have cont_eq: "\<And>g. (\<lambda>(x,l). content l *\<^sub>R f x) \<circ> (\<lambda>(x,l). (x,g l)) = (\<lambda>(x,l). content (g l) *\<^sub>R f x)"
+        by auto
have "((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j) =
(\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - (i + j)"
by auto
also have "\<dots> = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) +
(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) - (i + j)"
unfolding lem3[OF p(3)]
-        apply (subst setsum.reindex_nontrivial[OF p(3)])
-        defer
-        apply (subst setsum.reindex_nontrivial[OF p(3)])
-        defer
-        unfolding lem4[symmetric]
-        apply (rule refl)
-        unfolding split_paired_all split_conv
-        apply (rule_tac[!] *)
-      proof -
-        case goal1
-        then show ?case
-          apply -
-          apply (rule tagged_division_split_left_inj [OF p(1), of a b aa ba])
-          using k
-          apply auto
-          done
-      next
-        case goal2
-        then show ?case
-          apply -
-          apply (rule tagged_division_split_right_inj[OF p(1), of a b aa ba])
-          using k
-          apply auto
-          done
-      qed
+        by (subst setsum.reindex_nontrivial[OF p(3)], auto intro!: k eq0 tagged_division_split_left_inj[OF p(1)] tagged_division_split_right_inj[OF p(1)]
+              simp: cont_eq)+
also note setsum.distrib[symmetric]
-      also have *: "\<And>x. x \<in> p \<Longrightarrow>
-        (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x +
-          (\<lambda>(x,ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x =
-        (\<lambda>(x,ka). content ka *\<^sub>R f x) x"
-        unfolding split_paired_all split_conv
-      proof -
+      also have "\<And>x. x \<in> p \<Longrightarrow>
+                    (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x +
+                    (\<lambda>(x,ka). content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) x =
+                    (\<lambda>(x,ka). content ka *\<^sub>R f x) x"
+      proof clarify
fix a b
assume "(a, b) \<in> p"
from p(6)[OF this] guess u v by (elim exE) note uv=this```