author paulson Sun, 06 Aug 2017 22:54:03 +0200 changeset 66359 8ed88442d7bb parent 66358 3817ee41236d child 66361 af5c71cffec5
more integration cleanups
```--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 06 20:41:27 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 06 22:54:03 2017 +0200
@@ -9,6 +9,10 @@
Lebesgue_Measure Tagged_Division
begin

+lemma eps_leI:
+  assumes "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> y"
+
(*FIXME DELETE*)
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto

@@ -1260,7 +1264,7 @@

lemma has_integral_separate_sides:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
-  assumes "(f has_integral i) (cbox a b)"
+  assumes f: "(f has_integral i) (cbox a b)"
and "e > 0"
and k: "k \<in> Basis"
obtains d where "gauge d"
@@ -1268,18 +1272,23 @@
p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) \<and> d fine p2 \<longrightarrow>
norm ((sum (\<lambda>(x,k). content k *\<^sub>R f x) p1 + sum (\<lambda>(x,k). content k *\<^sub>R f x) p2) - i) < e"
proof -
-  guess d using has_integralD[OF assms(1-2)] . note d=this
+  obtain \<gamma> where d: "gauge \<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) - i) < e"
+    using has_integralD[OF f \<open>e > 0\<close>] by metis
{ fix p1 p2
-    assume "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" "d fine p1"
-    note p1=tagged_division_ofD[OF this(1)] this
-    assume "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> k}" "d fine p2"
-    note p2=tagged_division_ofD[OF this(1)] this
-    note tagged_division_union_interval[OF p1(7) p2(7)] note p12 = tagged_division_ofD[OF this] this
+    assume tdiv1: "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" and "\<gamma> fine p1"
+    note p1=tagged_division_ofD[OF this(1)]
+    assume tdiv2: "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> k}" and "\<gamma> fine p2"
+    note p2=tagged_division_ofD[OF this(1)]
+    note tagged_division_union_interval[OF tdiv1 tdiv2]
+    note p12 = tagged_division_ofD[OF this] this
{ fix a b
assume ab: "(a, b) \<in> p1 \<inter> p2"
have "(a, b) \<in> p1"
using ab by auto
-      with p1 obtain u v where uv: "b = cbox u v" by auto
+      obtain u v where uv: "b = cbox u v"
+        using \<open>(a, b) \<in> p1\<close> p1(4) by moura
have "b \<subseteq> {x. x\<bullet>k = c}"
using ab p1(3)[of a b] p2(3)[of a b] by fastforce
moreover
@@ -1288,25 +1297,23 @@
assume "\<not> ?thesis"
then obtain x where x: "x \<in> interior {x::'a. x\<bullet>k = c}"
by auto
-        then guess e unfolding mem_interior .. note e=this
+        then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> {x. x \<bullet> k = c}"
+          using mem_interior by metis
have x: "x\<bullet>k = c"
using x interior_subset by fastforce
-        have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (e / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then e/2 else 0)"
-          using e k by (auto simp: inner_simps inner_not_same_Basis)
-        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (e / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
-              (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))"
+        have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (\<epsilon> / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then \<epsilon>/2 else 0)"
+          using \<open>0 < \<epsilon>\<close> k by (auto simp: inner_simps inner_not_same_Basis)
+        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon> / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
+              (\<Sum>i\<in>Basis. (if i = k then \<epsilon> / 2 else 0))"
using "*" by (blast intro: sum.cong)
-        also have "\<dots> < e"
-          apply (subst sum.delta)
-          using e
-          apply auto
-          done
-        finally have "x + (e/2) *\<^sub>R k \<in> ball x e"
+        also have "\<dots> < \<epsilon>"
+          by (subst sum.delta) (use \<open>0 < \<epsilon>\<close> in auto)
+        finally have "x + (\<epsilon>/2) *\<^sub>R k \<in> ball x \<epsilon>"
unfolding mem_ball dist_norm by(rule le_less_trans[OF norm_le_l1])
-        then have "x + (e/2) *\<^sub>R k \<in> {x. x\<bullet>k = c}"
-          using e by auto
+        then have "x + (\<epsilon>/2) *\<^sub>R k \<in> {x. x\<bullet>k = c}"
+          using \<epsilon> by auto
then show False
-          unfolding mem_Collect_eq using e x k by (auto simp: inner_simps)
+          using \<open>0 < \<epsilon>\<close> x k by (auto simp: inner_simps)
qed
ultimately have "content b = 0"
unfolding uv content_eq_0_interior
@@ -1318,11 +1325,11 @@
norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)"
by (subst sum.union_inter_neutral) (auto simp: p1 p2)
also have "\<dots> < e"
-      by (rule k d(2) p12 fine_Un p1 p2)+
+      using d(2) p12 by (simp add: fine_Un k \<open>\<gamma> fine p1\<close> \<open>\<gamma> fine p2\<close>)
finally have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" .
}
then show ?thesis
-    by (auto intro: that[of d] d elim: )
+    using d(1) that by auto
qed

lemma integrable_split [intro]:
@@ -6796,68 +6803,72 @@
and "\<forall>x\<in>s. norm (f x) \<le> g x"
shows "norm (integral s f) \<le> integral s g"
proof -
-  have *: "\<And>x y. (\<forall>e::real. 0 < e \<longrightarrow> x < y + e) \<Longrightarrow> x \<le> y"
-    apply (rule ccontr)
-    apply (erule_tac x="x - y" in allE)
-    apply auto
-    done
have norm: "norm ig < dia + e"
-    if "norm sg \<le> dsa"
-    and "\<bar>dsa - dia\<bar> < e / 2"
-    and "norm (sg - ig) < e / 2"
+    if "norm sg \<le> dsa" and "\<bar>dsa - dia\<bar> < e / 2" and "norm (sg - ig) < e / 2"
for e dsa dia and sg ig :: 'a
apply (rule le_less_trans[OF norm_triangle_sub[of ig sg]])
apply (subst real_sum_of_halves[of e,symmetric])
-    defer
-    apply (subst norm_minus_commute)
-    apply (rule that(3))
+     defer
+     apply (subst norm_minus_commute)
+     apply (rule that(3))
apply (rule order_trans[OF that(1)])
using that(2)
apply arith
done
have lem: "norm (integral(cbox a b) f) \<le> integral (cbox a b) g"
-    if "f integrable_on cbox a b"
-    and "g integrable_on cbox a b"
-    and "\<forall>x\<in>cbox a b. norm (f x) \<le> g x"
+    if f: "f integrable_on cbox a b"
+    and g: "g integrable_on cbox a b"
+    and nle: "\<And>x. x \<in> cbox a b \<Longrightarrow> norm (f x) \<le> g x"
for f :: "'n \<Rightarrow> 'a" and g a b
-  proof (rule *[rule_format])
+  proof (rule eps_leI)
fix e :: real
assume "e > 0"
-    then have *: "e/2 > 0"
+    then have e: "e/2 > 0"
by auto
-    from integrable_integral[OF that(1),unfolded has_integral[of f],rule_format,OF *]
-    guess d1 .. note d1 = conjunctD2[OF this,rule_format]
-    from integrable_integral[OF that(2),unfolded has_integral[of g],rule_format,OF *]
-    guess d2 .. note d2 = conjunctD2[OF this,rule_format]
-    note gauge_Int[OF d1(1) d2(1)]
-    from fine_division_exists[OF this, of a b] guess p . note p=this
+    with integrable_integral[OF f,unfolded has_integral[of f]]
+    obtain \<gamma> where \<gamma>: "gauge \<gamma>"
+              "\<And>p. p tagged_division_of cbox a b \<and> \<gamma> fine p
+           \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral (cbox a b) f) < e / 2"
+      by meson
+    moreover
+    from integrable_integral[OF g,unfolded has_integral[of g]] e
+    obtain \<delta> where \<delta>: "gauge \<delta>"
+              "\<And>p. p tagged_division_of cbox a b \<and> \<delta> fine p
+           \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - integral (cbox a b) g) < e / 2"
+      by meson
+    ultimately have "gauge (\<lambda>x. \<gamma> x \<inter> \<delta> x)"
+      using gauge_Int by blast
+    with fine_division_exists obtain p
+      where p: "p tagged_division_of cbox a b" "(\<lambda>x. \<gamma> x \<inter> \<delta> x) fine p"
+      by metis
+    have "\<gamma> fine p" "\<delta> fine p"
+      using fine_Int p(2) by blast+
show "norm (integral (cbox a b) f) < integral (cbox a b) g + e"
-      apply (rule norm)
-      defer
-      apply (rule d2(2)[OF conjI[OF p(1)],unfolded real_norm_def])
-      defer
-      apply (rule d1(2)[OF conjI[OF p(1)]])
-      defer
-      apply (rule sum_norm_le)
-    proof safe
-      fix x k
-      assume "(x, k) \<in> p"
-      note as = tagged_division_ofD(2-4)[OF p(1) this]
-      from this(3) guess u v by (elim exE) note uv=this
-      show "norm (content k *\<^sub>R f x) \<le> content k *\<^sub>R g x"
-        unfolding uv norm_scaleR
-        unfolding abs_of_nonneg[OF content_pos_le] real_scaleR_def
-        apply (rule mult_left_mono)
-        using that(3) as
-        apply auto
-        done
-    qed (insert p[unfolded fine_Int], auto)
+    proof (rule norm)
+      have "norm (content K *\<^sub>R f x) \<le> content K *\<^sub>R g x" if  "(x, K) \<in> p" for x K
+      proof-
+        have K: "x \<in> K" "K \<subseteq> cbox a b"
+          using \<open>(x, K) \<in> p\<close> p(1) by blast+
+        obtain u v where  "K = cbox u v"
+          using \<open>(x, K) \<in> p\<close> p(1) by blast
+        moreover have "content K * norm (f x) \<le> content K * g x"
+          by (metis K subsetD dual_order.antisym measure_nonneg mult_zero_left nle not_le real_mult_le_cancel_iff2)
+        then show ?thesis
+          by simp
+      qed
+      then show "norm (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) \<le> (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
+        by (simp add: sum_norm_le split_def)
+      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral (cbox a b) f) < e / 2"
+        using \<open>\<gamma> fine p\<close> \<gamma> p(1) by simp
+      show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - integral (cbox a b) g\<bar> < e / 2"
+        using \<open>\<delta> fine p\<close> \<delta> p(1) by simp
+    qed
qed

{ presume "\<And>e. 0 < e \<Longrightarrow> norm (integral s f) < integral s g + e"
-    then show ?thesis by (rule *[rule_format]) auto }
+    then show ?thesis by (rule eps_leI) auto }
fix e :: real
assume "e > 0"
then have e: "e/2 > 0"
@@ -6885,7 +6896,6 @@
defer
apply (rule w(2)[unfolded real_norm_def])
apply (rule z(2))
-    apply safe
apply (case_tac "x \<in> s")
unfolding if_P
apply (rule assms(3)[rule_format])
@@ -6893,6 +6903,7 @@
done
qed

+
lemma integral_norm_bound_integral_component:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
fixes g :: "'n \<Rightarrow> 'b::euclidean_space"```