author paulson Thu, 24 Aug 2017 23:04:33 +0100 changeset 66505 b81e1d194e4c parent 66504 04b3a4548323 child 66506 c1d8ab323d85
work on integrable_alt, etc.
```--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 21:41:13 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 23:04:33 2017 +0100
@@ -5034,62 +5034,56 @@
integral (cbox c d)  (\<lambda>x. if x \<in> s then f x else 0)) < e)"
(is "?l = ?r")
proof
+  let ?F = "\<lambda>x. if x \<in> s then f x else 0"
assume ?l
-  then guess y unfolding integrable_on_def..note this[unfolded has_integral_alt'[of f]]
-  note y=conjunctD2[OF this,rule_format]
+  then obtain y where intF: "\<And>a b. ?F integrable_on cbox a b"
+          and y: "\<And>e. 0 < e \<Longrightarrow>
+              \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow> norm (integral (cbox a b) ?F - y) < e"
+    unfolding integrable_on_def has_integral_alt'[of f] by auto
show ?r
-    apply safe
-    apply (rule y)
-  proof goal_cases
-    case (1 e)
+  proof (intro conjI allI impI intF)
+    fix e::real
+    assume "e > 0"
then have "e/2 > 0"
by auto
-    from y(2)[OF this] guess B..note B=conjunctD2[OF this,rule_format]
-    show ?case
-      apply rule
-      apply rule
-      apply (rule B)
-      apply safe
-    proof goal_cases
-      case prems: (1 a b c d)
-      show ?case
-        apply (rule norm_triangle_half_l)
-        using B(2)[OF prems(1)] B(2)[OF prems(2)]
-        apply auto
-        done
+    obtain B where "0 < B"
+       and B: "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> norm (integral (cbox a b) ?F - y) < e/2"
+      using \<open>0 < e/2\<close> y by blast
+    show "\<exists>B>0. \<forall>a b c d. ball 0 B \<subseteq> cbox a b \<and> ball 0 B \<subseteq> cbox c d \<longrightarrow>
+                  norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e"
+    proof (intro conjI exI impI allI, rule \<open>0 < B\<close>)
+      fix a b c d::'n
+      assume sub: "ball 0 B \<subseteq> cbox a b \<and> ball 0 B \<subseteq> cbox c d"
+      show "norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e"
+        using sub by (auto intro: norm_triangle_half_l dest: B)
qed
qed
next
-  assume ?r
+  let ?F = "\<lambda>x. if x \<in> s then f x else 0"
+  assume rhs: ?r
note as = conjunctD2[OF this,rule_format]
let ?cube = "\<lambda>n. cbox (\<Sum>i\<in>Basis. - real n *\<^sub>R i::'n) (\<Sum>i\<in>Basis. real n *\<^sub>R i)"
have "Cauchy (\<lambda>n. integral (?cube n) (\<lambda>x. if x \<in> s then f x else 0))"
proof (unfold Cauchy_def, safe, goal_cases)
case (1 e)
-    from as(2)[OF this] guess B..note B = conjunctD2[OF this,rule_format]
-    from real_arch_simple[of B] guess N..note N = this
+    with rhs obtain B where "0 < B"
+      and B: "\<And>a b c d. ball 0 B \<subseteq> cbox a b \<and> ball 0 B \<subseteq> cbox c d
+                        \<Longrightarrow> norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e"
+      by blast
+    obtain N where N: "B \<le> real N"
+      using real_arch_simple by blast
{
fix n
assume n: "n \<ge> N"
-      have "ball 0 B \<subseteq> ?cube n"
-        apply (rule subsetI)
-        unfolding mem_ball mem_box dist_norm
-      proof (rule, goal_cases)
-        case (1 x i)
-        then show ?case
-          using Basis_le_norm[of i x] \<open>i\<in>Basis\<close>
-          using n N
-          by (auto simp add: field_simps sum_negf)
-      qed
+      have "sum (op *\<^sub>R (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
+            x \<bullet> i \<le> sum (op *\<^sub>R (real n)) Basis \<bullet> i"
+        if "norm x < B" "i \<in> Basis" for x i::'n
+          using Basis_le_norm[of i x] n N that by (auto simp add: field_simps sum_negf)
+      then have "ball 0 B \<subseteq> ?cube n"
+        by (auto simp: mem_box dist_norm)
}
then show ?case
-      apply -
-      apply (rule_tac x=N in exI)
-      apply safe
-      unfolding dist_norm
-      apply (rule B(2))
-      apply auto
-      done
+      by (fastforce simp add: dist_norm intro!: B)
qed
from this[unfolded convergent_eq_Cauchy[symmetric]] guess i ..
note i = this[THEN LIMSEQ_D]
@@ -5153,15 +5147,15 @@

lemma integrable_on_subcbox:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on s"
-    and "cbox a b \<subseteq> s"
+  assumes intf: "f integrable_on S"
+    and sub: "cbox a b \<subseteq> S"
shows "f integrable_on cbox a b"
-  apply (rule integrable_eq)
-  defer
-  apply (rule integrable_altD(1)[OF assms(1)])
-  using assms(2)
-  apply auto
-  done
+proof -
+  have "(\<lambda>x. if x \<in> S then f x else 0) integrable_on cbox a b"
+    by (simp add: intf integrable_altD(1))
+then show ?thesis
+  by (metis (mono_tags) sub integrable_restrict_Int le_inf_iff order_refl subset_antisym)
+qed

subsection \<open>A straddling criterion for integrability\<close>
@@ -5993,10 +5987,10 @@
by blast
then have "abs (content K * (g x - f (m x) x)) \<le> content K * (e/(4 * content (cbox a b)))"
by (metis m[OF x] mult_nonneg_nonneg abs_of_nonneg less_eq_real_def measure_nonneg mult_left_mono order_refl)
-          then show "\<bar>content K * g x - content K * f (m x) x\<bar> \<le> content K * e / (4 * content (cbox a b))"
+          then show "\<bar>content K * g x - content K * f (m x) x\<bar> \<le> content K * e/(4 * content (cbox a b))"
by (simp add: algebra_simps)
qed
-        also have "... = (e / (4 * content (cbox a b))) * (\<Sum>(x, k)\<in>\<D>. content k)"
+        also have "... = (e/(4 * content (cbox a b))) * (\<Sum>(x, k)\<in>\<D>. content k)"
by (simp add: sum_distrib_left sum_divide_distrib split_def mult.commute)
also have "... \<le> e/4"
by (metis False additive_content_tagged_division [OF ptag] nonzero_mult_divide_mult_cancel_right order_refl times_divide_eq_left)
@@ -6070,7 +6064,7 @@
using that s xK f_le p'(3) by fastforce
qed
qed
-        moreover have "0 \<le> i - integral (cbox a b) (f r)" "i - integral (cbox a b) (f r) < e / 4"
+        moreover have "0 \<le> i - integral (cbox a b) (f r)" "i - integral (cbox a b) (f r) < e/4"
using r by auto
ultimately show "\<bar>(\<Sum>(x,K)\<in>\<D>. integral K (f (m x))) - i\<bar> < e/4"
using comb i'[of s] by auto
@@ -7042,7 +7036,7 @@
proof (rule dense_eq0_I, simp)
fix e :: real
assume "0 < e"
-    with \<open>content ?CBOX > 0\<close> have "0 < e / content ?CBOX"
+    with \<open>content ?CBOX > 0\<close> have "0 < e/content ?CBOX"
by simp
have f_int_acbd: "f integrable_on ?CBOX"
by (rule integrable_continuous [OF assms])
@@ -7050,8 +7044,8 @@
assume p: "p division_of ?CBOX"
then have "finite p"
by blast
-      define e' where "e' = e / content ?CBOX"
-      with \<open>0 < e\<close> \<open>0 < e / content ?CBOX\<close>
+      define e' where "e' = e/content ?CBOX"
+      with \<open>0 < e\<close> \<open>0 < e/content ?CBOX\<close>
have "0 < e'"
by simp
interpret operative conj True
@@ -7109,7 +7103,7 @@
\<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
-        using cbp \<open>0 < e / content ?CBOX\<close> nf'
+        using cbp \<open>0 < e/content ?CBOX\<close> nf'
apply (auto simp: integrable_diff f_int_uwvz integrable_const)
done
have int_integrable: "(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) integrable_on cbox u v"
@@ -7120,14 +7114,14 @@
\<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2"
apply (simp only: integral_diff [symmetric] f_int_uv integrable_const)
apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
-        using cbp \<open>0 < e / content ?CBOX\<close> nf'
+        using cbp \<open>0 < e/content ?CBOX\<close> nf'
apply (auto simp: integrable_diff f_int_uv integrable_const)
done
have "norm (integral (cbox u v)
(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
\<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)"
apply (rule integrable_bound [OF _ _ normint_wz])
-        using cbp \<open>0 < e / content ?CBOX\<close>
+        using cbp \<open>0 < e/content ?CBOX\<close>
apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const)
done
also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"```