--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Jun 08 23:52:21 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Jun 09 22:48:11 2015 +0100
@@ -2089,10 +2089,7 @@
obtain n where n: "(\<Sum>i\<in>Basis. b \<bullet> i - a \<bullet> i) / e < 2 ^ n"
using real_arch_pow2[of "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] ..
show ?case
- apply (rule_tac x=n in exI)
- apply rule
- apply rule
- proof -
+ proof (rule exI [where x=n], clarify)
fix x y
assume xy: "x\<in>cbox (A n) (B n)" "y\<in>cbox (A n) (B n)"
have "dist x y \<le> setsum (\<lambda>i. abs((x - y)\<bullet>i)) Basis"
@@ -2150,25 +2147,20 @@
assume "e > 0"
from interv[OF this] obtain n
where n: "\<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e" ..
- show "\<exists>c d. x0 \<in> cbox c d \<and> cbox c d \<subseteq> ball x0 e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
+ have "\<not> P (cbox (A n) (B n))"
+ apply (cases "0 < n")
+ using AB(3)[of "n - 1"] assms(3) AB(1-2)
+ apply auto
+ done
+ moreover have "cbox (A n) (B n) \<subseteq> ball x0 e"
+ using n using x0[of n] by auto
+ moreover have "cbox (A n) (B n) \<subseteq> cbox a b"
+ unfolding AB(1-2)[symmetric] by (rule ABsubset) auto
+ ultimately show "\<exists>c d. x0 \<in> cbox c d \<and> cbox c d \<subseteq> ball x0 e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
apply (rule_tac x="A n" in exI)
apply (rule_tac x="B n" in exI)
- apply rule
- apply (rule x0)
- apply rule
- defer
- apply rule
- proof -
- show "\<not> P (cbox (A n) (B n))"
- apply (cases "0 < n")
- using AB(3)[of "n - 1"] assms(3) AB(1-2)
- apply auto
- done
- show "cbox (A n) (B n) \<subseteq> ball x0 e"
- using n using x0[of n] by auto
- show "cbox (A n) (B n) \<subseteq> cbox a b"
- unfolding AB(1-2)[symmetric] by (rule ABsubset) auto
- qed
+ apply (auto simp: x0)
+ done
qed
qed
@@ -2205,22 +2197,17 @@
assume "p tagged_division_of s" "g fine p" "p' tagged_division_of t" "g fine p'"
"interior s \<inter> interior t = {}"
then show "\<exists>p. p tagged_division_of s \<union> t \<and> g fine p"
- apply -
apply (rule_tac x="p \<union> p'" in exI)
- apply rule
- apply (rule tagged_division_union)
- prefer 4
- apply (rule fine_union)
- apply auto
+ apply (simp add: tagged_division_union fine_union)
done
qed blast
obtain e where e: "e > 0" "ball x e \<subseteq> g x"
using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
- from x(2)[OF e(1)] obtain c d where c_d:
- "x \<in> cbox c d"
- "cbox c d \<subseteq> ball x e"
- "cbox c d \<subseteq> cbox a b"
- "\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
+ from x(2)[OF e(1)]
+ obtain c d where c_d: "x \<in> cbox c d"
+ "cbox c d \<subseteq> ball x e"
+ "cbox c d \<subseteq> cbox a b"
+ "\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
by blast
have "g fine {(x, cbox c d)}"
unfolding fine_def using e using c_d(2) by auto
@@ -2281,11 +2268,7 @@
{
presume "\<not> (\<exists>a b. i = cbox a b) \<Longrightarrow> False"
then show False
- apply -
- apply (cases "\<exists>a b. i = cbox a b")
- using assms
- apply (auto simp add:has_integral intro:lem[OF _ _ as])
- done
+ using as assms lem by blast
}
assume as: "\<not> (\<exists>a b. i = cbox a b)"
obtain B1 where B1:
@@ -2339,23 +2322,11 @@
have lem: "\<And>a b. \<And>f::'n \<Rightarrow> 'a.
(\<forall>x\<in>cbox a b. f(x) = 0) \<Longrightarrow> (f has_integral 0) (cbox a b)"
unfolding has_integral
- apply rule
- apply rule
- proof -
+ proof clarify
fix a b e
fix f :: "'n \<Rightarrow> 'a"
assume as: "\<forall>x\<in>cbox a b. f x = 0" "0 < (e::real)"
- show "\<exists>d. gauge d \<and>
- (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e)"
- apply (rule_tac x="\<lambda>x. ball x 1" in exI)
- apply rule
- apply (rule gaugeI)
- unfolding centre_in_ball
- defer
- apply (rule open_ball)
- apply rule
- apply rule
- apply (erule conjE)
+ have "\<And>p. p tagged_division_of cbox a b \<Longrightarrow> (\<lambda>x. ball x 1) fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
proof -
case goal1
have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) = 0"
@@ -2372,16 +2343,15 @@
qed
then show ?case
using as by auto
- qed auto
+ qed
+ then show "\<exists>d. gauge d \<and>
+ (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e)"
+ by auto
qed
{
presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
- then show ?thesis
- apply -
- apply (cases "\<exists>a b. s = cbox a b")
- using assms
- apply (auto simp add:has_integral intro: lem)
- done
+ with assms lem show ?thesis
+ by blast
}
have *: "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. 0)"
apply (rule ext)
@@ -2390,26 +2360,8 @@
done
assume "\<not> (\<exists>a b. s = cbox a b)"
then show ?thesis
- apply (subst has_integral_alt)
- unfolding if_not_P *
- apply rule
- apply rule
- apply (rule_tac x=1 in exI)
- apply rule
- defer
- apply rule
- apply rule
- apply rule
- proof -
- fix e :: real
- fix a b
- assume "e > 0"
- then show "\<exists>z. ((\<lambda>x::'n. 0::'a) has_integral z) (cbox a b) \<and> norm (z - 0) < e"
- apply (rule_tac x=0 in exI)
- apply(rule,rule lem)
- apply auto
- done
- qed auto
+ using lem
+ by (subst has_integral_alt) (force simp add: *)
qed
lemma has_integral_0[simp]: "((\<lambda>x::'n::euclidean_space. 0) has_integral 0) s"
@@ -2430,20 +2382,17 @@
by blast
have lem: "\<And>(f :: 'n \<Rightarrow> 'a) y a b.
(f has_integral y) (cbox a b) \<Longrightarrow> ((h o f) has_integral h y) (cbox a b)"
- apply (subst has_integral)
- apply rule
- apply rule
- proof -
+ unfolding has_integral
+ proof clarify
case goal1
from pos_bounded
obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
by blast
have *: "e / B > 0" using goal1(2) B by simp
- obtain g where g:
- "gauge g"
- "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
- norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e / B"
- by (rule has_integralD[OF goal1(1) *]) blast
+ obtain g where g: "gauge g"
+ "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
+ norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e / B"
+ using "*" goal1(1) by auto
show ?case
apply (rule_tac x=g in exI)
apply rule
@@ -2472,19 +2421,11 @@
{
presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
then show ?thesis
- apply -
- apply (cases "\<exists>a b. s = cbox a b")
- using assms
- apply (auto simp add:has_integral intro!:lem)
- done
+ using assms(1) lem by blast
}
assume as: "\<not> (\<exists>a b. s = cbox a b)"
then show ?thesis
- apply (subst has_integral_alt)
- unfolding if_not_P
- apply rule
- apply rule
- proof -
+ proof (subst has_integral_alt, clarsimp)
fix e :: real
assume e: "e > 0"
have *: "0 < e/B" using e B(1) by simp
@@ -2495,34 +2436,18 @@
using has_integral_altD[OF assms(1) as *] by blast
show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
(\<exists>z. ((\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
- apply (rule_tac x=M in exI)
- apply rule
- apply (rule M(1))
- apply rule
- apply rule
- apply rule
- proof -
+ proof (rule_tac x=M in exI, clarsimp simp add: M)
case goal1
obtain z where z:
"((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b)"
"norm (z - y) < e / B"
using M(2)[OF goal1(1)] by blast
have *: "(\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> s then f x else 0)"
- unfolding o_def
- apply (rule ext)
- using zero
- apply auto
- done
+ using zero by auto
show ?case
apply (rule_tac x="h z" in exI)
- apply rule
- unfolding *
- apply (rule lem[OF z(1)])
- unfolding diff[symmetric]
- apply (rule le_less_trans[OF B(2)])
- using B(1) z(2)
- apply (auto simp add: field_simps)
- done
+ apply (simp add: "*" lem z(1))
+ by (metis B diff le_less_trans pos_less_divide_eq z(2))
qed
qed
qed
@@ -2538,9 +2463,7 @@
lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
unfolding o_def[symmetric]
- apply (rule has_integral_linear,assumption)
- apply (rule bounded_linear_scaleR_right)
- done
+ by (metis has_integral_linear bounded_linear_scaleR_right)
lemma has_integral_cmult_real:
fixes c :: real
@@ -2556,9 +2479,7 @@
qed
lemma has_integral_neg: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
- apply (drule_tac c="-1" in has_integral_cmul)
- apply auto
- done
+ by (drule_tac c="-1" in has_integral_cmul) auto
lemma has_integral_add:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
@@ -2574,9 +2495,7 @@
case goal1
show ?case
unfolding has_integral
- apply rule
- apply rule
- proof -
+ proof clarify
fix e :: real
assume e: "e > 0"
then have *: "e/2 > 0"
@@ -2592,30 +2511,23 @@
norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l) < e / 2"
using has_integralD[OF goal1(2) *] by blast
show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
- norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e)"
- apply (rule_tac x="\<lambda>x. (d1 x) \<inter> (d2 x)" in exI)
- apply rule
- apply (rule gauge_inter[OF d1(1) d2(1)])
- apply (rule,rule,erule conjE)
- proof -
+ norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e)"
+ proof (rule exI [where x="\<lambda>x. (d1 x) \<inter> (d2 x)"], clarsimp simp add: gauge_inter[OF d1(1) d2(1)])
fix p
assume as: "p tagged_division_of (cbox a b)" "(\<lambda>x. d1 x \<inter> d2 x) fine p"
have *: "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) =
(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
unfolding scaleR_right_distrib setsum.distrib[of "\<lambda>(x,k). content k *\<^sub>R f x" "\<lambda>(x,k). content k *\<^sub>R g x" p,symmetric]
by (rule setsum.cong) auto
+ from as have fine: "d1 fine p" "d2 fine p"
+ unfolding fine_inter by auto
have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) =
- norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
+ norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
unfolding * by (auto simp add: algebra_simps)
- also
- let ?res = "\<dots>"
- from as have *: "d1 fine p" "d2 fine p"
- unfolding fine_inter by auto
- have "?res < e/2 + e/2"
+ also have "\<dots> < e/2 + e/2"
apply (rule le_less_trans[OF norm_triangle_ineq])
- apply (rule add_strict_mono)
- using d1(2)[OF as(1) *(1)] and d2(2)[OF as(1) *(2)]
- apply auto
+ using as d1 d2 fine
+ apply (blast intro: add_strict_mono)
done
finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e"
by auto
@@ -2625,19 +2537,11 @@
{
presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
then show ?thesis
- apply -
- apply (cases "\<exists>a b. s = cbox a b")
- using assms
- apply (auto simp add:has_integral intro!:lem)
- done
+ using assms lem by force
}
assume as: "\<not> (\<exists>a b. s = cbox a b)"
then show ?thesis
- apply (subst has_integral_alt)
- unfolding if_not_P
- apply rule
- apply rule
- proof -
+ proof (subst has_integral_alt, clarsimp)
case goal1
then have *: "e/2 > 0"
by auto
@@ -2654,14 +2558,7 @@
\<exists>z. ((\<lambda>x. if x \<in> s then g x else 0) has_integral z) (cbox a b) \<and> norm (z - l) < e / 2"
by blast
show ?case
- apply (rule_tac x="max B1 B2" in exI)
- apply rule
- apply (rule max.strict_coboundedI1)
- apply (rule B1)
- apply rule
- apply rule
- apply rule
- proof -
+ proof (rule_tac x="max B1 B2" in exI, clarsimp simp add: max.strict_coboundedI1 B1)
fix a b
assume "ball 0 (max B1 B2) \<subseteq> cbox a (b::'n)"
then have *: "ball 0 B1 \<subseteq> cbox a (b::'n)" "ball 0 B2 \<subseteq> cbox a (b::'n)"
@@ -2679,8 +2576,7 @@
by auto
show "\<exists>z. ((\<lambda>x. if x \<in> s then f x + g x else 0) has_integral z) (cbox a b) \<and> norm (z - (k + l)) < e"
apply (rule_tac x="w + z" in exI)
- apply rule
- apply (rule lem[OF w(1) z(1), unfolded *[symmetric]])
+ apply (simp add: lem[OF w(1) z(1), unfolded *[symmetric]])
using norm_triangle_ineq[of "w - k" "z - l"] w(2) z(2)
apply (auto simp add: field_simps)
done
@@ -2701,33 +2597,17 @@
lemma integral_add: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
integral s (\<lambda>x. f x + g x) = integral s f + integral s g"
- apply (rule integral_unique)
- apply (drule integrable_integral)+
- apply (rule has_integral_add)
- apply assumption+
- done
+ by (rule integral_unique) (metis integrable_integral has_integral_add)
lemma integral_cmul: "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral s f"
- apply (rule integral_unique)
- apply (drule integrable_integral)+
- apply (rule has_integral_cmul)
- apply assumption+
- done
+ by (rule integral_unique) (metis integrable_integral has_integral_cmul)
lemma integral_neg: "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. - f x) = - integral s f"
- apply (rule integral_unique)
- apply (drule integrable_integral)+
- apply (rule has_integral_neg)
- apply assumption+
- done
+ by (rule integral_unique) (metis integrable_integral has_integral_neg)
lemma integral_sub: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
- apply (rule integral_unique)
- apply (drule integrable_integral)+
- apply (rule has_integral_sub)
- apply assumption+
- done
+ by (rule integral_unique) (metis integrable_integral has_integral_sub)
lemma integrable_0: "(\<lambda>x. 0) integrable_on s"
unfolding integrable_on_def using has_integral_0 by auto
@@ -2758,13 +2638,8 @@
lemma integral_linear:
"f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> integral s (h \<circ> f) = h (integral s f)"
- apply (rule has_integral_unique)
- defer
- unfolding has_integral_integral
- apply (drule (2) has_integral_linear)
- unfolding has_integral_integral[symmetric]
- apply (rule integrable_linear)
- apply assumption+
+ apply (rule has_integral_unique [where i=s and f = "h \<circ> f"])
+ apply (simp_all add: integrable_integral integrable_linear has_integral_linear )
done
lemma integral_component_eq[simp]:
@@ -2783,24 +2658,17 @@
then show ?case by auto
next
case (insert x F)
- show ?case
- unfolding setsum.insert[OF insert(1,3)]
- apply (rule has_integral_add)
- using insert assms
- apply auto
- done
-qed
-
-lemma integral_setsum: "finite t \<Longrightarrow> \<forall>a\<in>t. (f a) integrable_on s \<Longrightarrow>
- integral s (\<lambda>x. setsum (\<lambda>a. f a x) t) = setsum (\<lambda>a. integral s (f a)) t"
- apply (rule integral_unique)
- apply (rule has_integral_setsum)
- using integrable_integral
- apply auto
- done
+ with assms show ?case
+ by (simp add: has_integral_add)
+qed
+
+lemma integral_setsum:
+ "\<lbrakk>finite t; \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow>
+ integral s (\<lambda>x. setsum (\<lambda>a. f a x) t) = setsum (\<lambda>a. integral s (f a)) t"
+ by (auto intro: has_integral_setsum integrable_integral)
lemma integrable_setsum:
- "finite t \<Longrightarrow> \<forall>a \<in> t. (f a) integrable_on s \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) t) integrable_on s"
+ "\<lbrakk>finite t; \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) t) integrable_on s"
unfolding integrable_on_def
apply (drule bchoice)
using has_integral_setsum[of t]
@@ -2857,19 +2725,10 @@
by (metis assms box_real(2) has_integral_null)
lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \<Longrightarrow> (f has_integral i) (cbox a b) \<longleftrightarrow> i = 0"
- apply rule
- apply (rule has_integral_unique)
- apply assumption
- apply (drule (1) has_integral_null)
- apply (drule has_integral_null)
- apply auto
- done
+ by (auto simp add: has_integral_null dest!: integral_unique)
lemma integral_null[dest]: "content (cbox a b) = 0 \<Longrightarrow> integral (cbox a b) f = 0"
- apply (rule integral_unique)
- apply (drule has_integral_null)
- apply assumption
- done
+ by (metis has_integral_null integral_unique)
lemma integrable_on_null[dest]: "content (cbox a b) = 0 \<Longrightarrow> f integrable_on (cbox a b)"
unfolding integrable_on_def
@@ -2878,19 +2737,10 @@
done
lemma has_integral_empty[intro]: "(f has_integral 0) {}"
- unfolding empty_as_interval
- apply (rule has_integral_null)
- using content_empty
- unfolding empty_as_interval
- apply assumption
- done
+ by (simp add: has_integral_is_0)
lemma has_integral_empty_eq[simp]: "(f has_integral i) {} \<longleftrightarrow> i = 0"
- apply rule
- apply (rule has_integral_unique)
- apply assumption
- apply auto
- done
+ by (auto simp add: has_integral_empty has_integral_unique)
lemma integrable_on_empty[intro]: "f integrable_on {}"
unfolding integrable_on_def by auto
@@ -2954,17 +2804,10 @@
done
note d=this[rule_format]
show ?case
- apply (rule_tac x=d in exI)
- apply rule
- apply (rule d)
- apply rule
- apply rule
- apply rule
- apply (erule conjE)+
- proof -
+ proof (rule_tac x=d in exI, clarsimp simp: d)
fix p1 p2
assume as: "p1 tagged_division_of (cbox a b)" "d fine p1"
- "p2 tagged_division_of (cbox a b)" "d fine p2"
+ "p2 tagged_division_of (cbox a b)" "d fine p2"
show "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)) < e"
apply (rule dist_triangle_half_l[where y=y,unfolded dist_norm])
using d(2)[OF conjI[OF as(1-2)]] d(2)[OF conjI[OF as(3-4)]] .