src/HOL/Multivariate_Analysis/Integration.thy
changeset 35751 f7f8d59b60b9
parent 35540 3d073a3e1c61
child 35752 c8a8df426666
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 09 09:25:23 2010 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 09 15:39:26 2010 +0100
     1.3 @@ -211,11 +211,11 @@
     1.4  lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
     1.5    unfolding gauge_def by auto 
     1.6  
     1.7 -lemma gauge_ball[intro?]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)" unfolding gauge_def by auto 
     1.8 +lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)" unfolding gauge_def by auto 
     1.9  
    1.10  lemma gauge_trivial[intro]: "gauge (\<lambda>x. ball x 1)" apply(rule gauge_ball) by auto
    1.11  
    1.12 -lemma gauge_inter: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. (d1 x) \<inter> (d2 x))"
    1.13 +lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. (d1 x) \<inter> (d2 x))"
    1.14    unfolding gauge_def by auto 
    1.15  
    1.16  lemma gauge_inters: assumes "finite s" "\<forall>d\<in>s. gauge (f d)" shows "gauge(\<lambda>x. \<Inter> {f d x | d. d \<in> s})" proof-
    1.17 @@ -3476,4 +3476,436 @@
    1.18    apply(rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f'])
    1.19    using assms(4) by auto
    1.20  
    1.21 +lemma indefinite_integral_continuous_left: fixes f::"real^1 \<Rightarrow> 'a::banach"
    1.22 +  assumes "f integrable_on {a..b}" "a < c" "c \<le> b" "0 < e"
    1.23 +  obtains d where "0 < d" "\<forall>t. c$1 - d < t$1 \<and> t \<le> c \<longrightarrow> norm(integral {a..c} f - integral {a..t} f) < e"
    1.24 +proof- have "\<exists>w>0. \<forall>t. c$1 - w < t$1 \<and> t < c \<longrightarrow> norm(f c) * norm(c - t) < e / 3"
    1.25 +  proof(cases "f c = 0") case False hence "0 < e / 3 / norm (f c)"
    1.26 +      apply-apply(rule divide_pos_pos) using `e>0` by auto
    1.27 +    thus ?thesis apply-apply(rule,rule,assumption,safe)
    1.28 +    proof- fix t assume as:"t < c" and "c$1 - e / 3 / norm (f c) < t$(1::1)"
    1.29 +      hence "c$1 - t$1 < e / 3 / norm (f c)" by auto
    1.30 +      hence "norm (c - t) < e / 3 / norm (f c)" using as unfolding norm_vector_1 vector_less_def by auto
    1.31 +      thus "norm (f c) * norm (c - t) < e / 3" using False apply-
    1.32 +        apply(subst real_mult_commute) apply(subst pos_less_divide_eq[THEN sym]) by auto
    1.33 +    qed next case True show ?thesis apply(rule_tac x=1 in exI) unfolding True using `e>0` by auto
    1.34 +  qed then guess w .. note w = conjunctD2[OF this,rule_format]
    1.35 +  
    1.36 +  have *:"e / 3 > 0" using assms by auto
    1.37 +  have "f integrable_on {a..c}" apply(rule integrable_subinterval[OF assms(1)]) using assms(2-3) by auto
    1.38 +  from integrable_integral[OF this,unfolded has_integral,rule_format,OF *] guess d1 ..
    1.39 +  note d1 = conjunctD2[OF this,rule_format] def d \<equiv> "\<lambda>x. ball x w \<inter> d1 x"
    1.40 +  have "gauge d" unfolding d_def using w(1) d1 by auto
    1.41 +  note this[unfolded gauge_def,rule_format,of c] note conjunctD2[OF this]
    1.42 +  from this(2)[unfolded open_contains_ball,rule_format,OF this(1)] guess k .. note k=conjunctD2[OF this]
    1.43 +
    1.44 +  let ?d = "min k (c$1 - a$1)/2" show ?thesis apply(rule that[of ?d])
    1.45 +  proof safe show "?d > 0" using k(1) using assms(2) unfolding vector_less_def by auto
    1.46 +    fix t assume as:"c$1 - ?d < t$1" "t \<le> c" let ?thesis = "norm (integral {a..c} f - integral {a..t} f) < e"
    1.47 +    { presume *:"t < c \<Longrightarrow> ?thesis"
    1.48 +      show ?thesis apply(cases "t = c") defer apply(rule *)
    1.49 +        unfolding vector_less_def apply(subst less_le) using `e>0` as(2) by auto } assume "t < c"
    1.50 +
    1.51 +    have "f integrable_on {a..t}" apply(rule integrable_subinterval[OF assms(1)]) using assms(2-3) as(2) by auto
    1.52 +    from integrable_integral[OF this,unfolded has_integral,rule_format,OF *] guess d2 ..
    1.53 +    note d2 = conjunctD2[OF this,rule_format]
    1.54 +    def d3 \<equiv> "\<lambda>x. if x \<le> t then d1 x \<inter> d2 x else d1 x"
    1.55 +    have "gauge d3" using d2(1) d1(1) unfolding d3_def gauge_def by auto
    1.56 +    from fine_division_exists[OF this, of a t] guess p . note p=this
    1.57 +    note p'=tagged_division_ofD[OF this(1)]
    1.58 +    have pt:"\<forall>(x,k)\<in>p. x$1 \<le> t$1" proof safe case goal1 from p'(2,3)[OF this] show ?case by auto qed
    1.59 +    with p(2) have "d2 fine p" unfolding fine_def d3_def apply safe apply(erule_tac x="(a,b)" in ballE)+ by auto
    1.60 +    note d2_fin = d2(2)[OF conjI[OF p(1) this]]
    1.61 +    
    1.62 +    have *:"{a..c} \<inter> {x. x$1 \<le> t$1} = {a..t}" "{a..c} \<inter> {x. x$1 \<ge> t$1} = {t..c}"
    1.63 +      using assms(2-3) as by(auto simp add:field_simps)
    1.64 +    have "p \<union> {(c, {t..c})} tagged_division_of {a..c} \<and> d1 fine p \<union> {(c, {t..c})}" apply rule
    1.65 +      apply(rule tagged_division_union_interval[of _ _ _ 1 "t$1"]) unfolding * apply(rule p)
    1.66 +      apply(rule tagged_division_of_self) unfolding fine_def
    1.67 +    proof safe fix x k y assume "(x,k)\<in>p" "y\<in>k" thus "y\<in>d1 x"
    1.68 +        using p(2) pt unfolding fine_def d3_def apply- apply(erule_tac x="(x,k)" in ballE)+ by auto
    1.69 +    next fix x assume "x\<in>{t..c}" hence "dist c x < k" unfolding dist_real
    1.70 +        using as(1) by(auto simp add:field_simps) 
    1.71 +      thus "x \<in> d1 c" using k(2) unfolding d_def by auto
    1.72 +    qed(insert as(2), auto) note d1_fin = d1(2)[OF this]
    1.73 +
    1.74 +    have *:"integral{a..c} f - integral {a..t} f = -(((c$1 - t$1) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)) -
    1.75 +        integral {a..c} f) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral {a..t} f) + (c$1 - t$1) *\<^sub>R f c" 
    1.76 +      "e = (e/3 + e/3) + e/3" by auto
    1.77 +    have **:"(\<Sum>(x, k)\<in>p \<union> {(c, {t..c})}. content k *\<^sub>R f x) = (c$1 - t$1) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
    1.78 +    proof- have **:"\<And>x F. F \<union> {x} = insert x F" by auto
    1.79 +      have "(c, {t..c}) \<notin> p" proof safe case goal1 from p'(2-3)[OF this]
    1.80 +        have "c \<in> {a..t}" by auto thus False using `t<c` unfolding vector_less_def by auto
    1.81 +      qed thus ?thesis unfolding ** apply- apply(subst setsum_insert) apply(rule p')
    1.82 +        unfolding split_conv defer apply(subst content_1) using as(2) by auto qed 
    1.83 +
    1.84 +    have ***:"c$1 - w < t$1 \<and> t < c"
    1.85 +    proof- have "c$1 - k < t$1" using `k>0` as(1) by(auto simp add:field_simps)
    1.86 +      moreover have "k \<le> w" apply(rule ccontr) using k(2) 
    1.87 +        unfolding subset_eq apply(erule_tac x="c + vec ((k + w)/2)" in ballE)
    1.88 +        unfolding d_def using `k>0` `w>0` by(auto simp add:field_simps not_le not_less dist_real)
    1.89 +      ultimately show  ?thesis using `t<c` by(auto simp add:field_simps) qed
    1.90 +
    1.91 +    show ?thesis unfolding *(1) apply(subst *(2)) apply(rule norm_triangle_lt add_strict_mono)+
    1.92 +      unfolding norm_minus_cancel apply(rule d1_fin[unfolded **]) apply(rule d2_fin)
    1.93 +      using w(2)[OF ***] unfolding norm_scaleR norm_real by(auto simp add:field_simps) qed qed 
    1.94 +
    1.95 +lemma indefinite_integral_continuous_right: fixes f::"real^1 \<Rightarrow> 'a::banach"
    1.96 +  assumes "f integrable_on {a..b}" "a \<le> c" "c < b" "0 < e"
    1.97 +  obtains d where "0 < d" "\<forall>t. c \<le> t \<and> t$1 < c$1 + d \<longrightarrow> norm(integral{a..c} f - integral{a..t} f) < e"
    1.98 +proof- have *:"(\<lambda>x. f (- x)) integrable_on {- b..- a}" "- b < - c" "- c \<le> - a"
    1.99 +    using assms unfolding Cart_simps by auto
   1.100 +  from indefinite_integral_continuous_left[OF * `e>0`] guess d . note d = this let ?d = "min d (b$1 - c$1)"
   1.101 +  show ?thesis apply(rule that[of "?d"])
   1.102 +  proof safe show "0 < ?d" using d(1) assms(3) unfolding Cart_simps by auto
   1.103 +    fix t::"_^1" assume as:"c \<le> t" "t$1 < c$1 + ?d"
   1.104 +    have *:"integral{a..c} f = integral{a..b} f - integral{c..b} f"
   1.105 +      "integral{a..t} f = integral{a..b} f - integral{t..b} f" unfolding group_simps
   1.106 +      apply(rule_tac[!] integral_combine) using assms as unfolding Cart_simps by auto
   1.107 +    have "(- c)$1 - d < (- t)$1 \<and> - t \<le> - c" using as by auto note d(2)[rule_format,OF this]
   1.108 +    thus "norm (integral {a..c} f - integral {a..t} f) < e" unfolding * 
   1.109 +      unfolding integral_reflect apply-apply(subst norm_minus_commute) by(auto simp add:group_simps) qed qed
   1.110 +
   1.111 +declare dest_vec1_eq[simp del] not_less[simp] not_le[simp]
   1.112 +
   1.113 +lemma indefinite_integral_continuous: fixes f::"real^1 \<Rightarrow> 'a::banach"
   1.114 +  assumes "f integrable_on {a..b}" shows  "continuous_on {a..b} (\<lambda>x. integral {a..x} f)"
   1.115 +proof(unfold continuous_on_def, safe)  fix x e assume as:"x\<in>{a..b}" "0<(e::real)"
   1.116 +  let ?thesis = "\<exists>d>0. \<forall>x'\<in>{a..b}. dist x' x < d \<longrightarrow> dist (integral {a..x'} f) (integral {a..x} f) < e"
   1.117 +  { presume *:"a<b \<Longrightarrow> ?thesis"
   1.118 +    show ?thesis apply(cases,rule *,assumption)
   1.119 +    proof- case goal1 hence "{a..b} = {x}" using as(1) unfolding Cart_simps  
   1.120 +        by(auto simp only:field_simps not_less Cart_eq forall_1 mem_interval) 
   1.121 +      thus ?case using `e>0` by auto
   1.122 +    qed } assume "a<b"
   1.123 +  have "(x=a \<or> x=b) \<or> (a<x \<and> x<b)" using as(1) by (auto simp add: Cart_simps)
   1.124 +  thus ?thesis apply-apply(erule disjE)+
   1.125 +  proof- assume "x=a" have "a \<le> a" by auto
   1.126 +    from indefinite_integral_continuous_right[OF assms(1) this `a<b` `e>0`] guess d . note d=this
   1.127 +    show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
   1.128 +      unfolding `x=a` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
   1.129 +  next   assume "x=b" have "b \<le> b" by auto
   1.130 +    from indefinite_integral_continuous_left[OF assms(1) `a<b` this `e>0`] guess d . note d=this
   1.131 +    show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
   1.132 +      unfolding `x=b` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
   1.133 +  next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add:Cart_simps)
   1.134 +    from indefinite_integral_continuous_left [OF assms(1) xl `e>0`] guess d1 . note d1=this
   1.135 +    from indefinite_integral_continuous_right[OF assms(1) xr `e>0`] guess d2 . note d2=this
   1.136 +    show ?thesis apply(rule_tac x="min d1 d2" in exI)
   1.137 +    proof safe show "0 < min d1 d2" using d1 d2 by auto
   1.138 +      fix y assume "y\<in>{a..b}" "dist y x < min d1 d2"
   1.139 +      thus "dist (integral {a..y} f) (integral {a..x} f) < e" apply-apply(subst dist_commute)
   1.140 +        apply(cases "y < x") unfolding vector_dist_norm apply(rule d1(2)[rule_format]) defer
   1.141 +        apply(rule d2(2)[rule_format]) unfolding Cart_simps not_less norm_real by(auto simp add:field_simps)
   1.142 +    qed qed qed 
   1.143 +
   1.144 +subsection {* This doesn't directly involve integration, but that gives an easy proof. *}
   1.145 +
   1.146 +lemma has_derivative_zero_unique_strong_interval: fixes f::"real \<Rightarrow> 'a::banach"
   1.147 +  assumes "finite k" "continuous_on {a..b} f" "f a = y"
   1.148 +  "\<forall>x\<in>({a..b} - k). (f has_derivative (\<lambda>h. 0)) (at x within {a..b})" "x \<in> {a..b}"
   1.149 +  shows "f x = y"
   1.150 +proof- have ab:"a\<le>b" using assms by auto
   1.151 +  have *:"(\<lambda>x. 0\<Colon>'a) \<circ> dest_vec1 = (\<lambda>x. 0)" unfolding o_def by auto have **:"a \<le> x" using assms by auto
   1.152 +  have "((\<lambda>x. 0\<Colon>'a) \<circ> dest_vec1 has_integral f x - f a) {vec1 a..vec1 x}"
   1.153 +    apply(rule fundamental_theorem_of_calculus_interior_strong[OF assms(1) ** ])
   1.154 +    apply(rule continuous_on_subset[OF assms(2)]) defer
   1.155 +    apply safe unfolding has_vector_derivative_def apply(subst has_derivative_within_open[THEN sym])
   1.156 +    apply assumption apply(rule open_interval_real) apply(rule has_derivative_within_subset[where s="{a..b}"])
   1.157 +    using assms(4) assms(5) by auto note this[unfolded *]
   1.158 +  note has_integral_unique[OF has_integral_0 this]
   1.159 +  thus ?thesis unfolding assms by auto qed
   1.160 +
   1.161 +subsection {* Generalize a bit to any convex set. *}
   1.162 +
   1.163 +lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
   1.164 +  scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
   1.165 +  scaleR_cancel_left scaleR_cancel_right scaleR.add_right scaleR.add_left real_vector_class.scaleR_one
   1.166 +
   1.167 +lemma has_derivative_zero_unique_strong_convex: fixes f::"real^'n \<Rightarrow> 'a::banach"
   1.168 +  assumes "convex s" "finite k" "continuous_on s f" "c \<in> s" "f c = y"
   1.169 +  "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)" "x \<in> s"
   1.170 +  shows "f x = y"
   1.171 +proof- { presume *:"x \<noteq> c \<Longrightarrow> ?thesis" show ?thesis apply(cases,rule *,assumption)
   1.172 +      unfolding assms(5)[THEN sym] by auto } assume "x\<noteq>c"
   1.173 +  note conv = assms(1)[unfolded convex_alt,rule_format]
   1.174 +  have as1:"continuous_on {0..1} (f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x))"
   1.175 +    apply(rule continuous_on_intros)+ apply(rule continuous_on_subset[OF assms(3)])
   1.176 +    apply safe apply(rule conv) using assms(4,7) by auto
   1.177 +  have *:"\<And>t xa. (1 - t) *\<^sub>R c + t *\<^sub>R x = (1 - xa) *\<^sub>R c + xa *\<^sub>R x \<Longrightarrow> t = xa"
   1.178 +  proof- case goal1 hence "(t - xa) *\<^sub>R x = (t - xa) *\<^sub>R c" 
   1.179 +      unfolding scaleR_simps by(auto simp add:group_simps)
   1.180 +    thus ?case using `x\<noteq>c` by auto qed
   1.181 +  have as2:"finite {t. ((1 - t) *\<^sub>R c + t *\<^sub>R x) \<in> k}" using assms(2) 
   1.182 +    apply(rule finite_surj[where f="\<lambda>z. SOME t. (1-t) *\<^sub>R c + t *\<^sub>R x = z"])
   1.183 +    apply safe unfolding image_iff apply rule defer apply assumption
   1.184 +    apply(rule sym) apply(rule some_equality) defer apply(drule *) by auto
   1.185 +  have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x)) 1 = y"
   1.186 +    apply(rule has_derivative_zero_unique_strong_interval[OF as2 as1, of ])
   1.187 +    unfolding o_def using assms(5) defer apply-apply(rule)
   1.188 +  proof- fix t assume as:"t\<in>{0..1} - {t. (1 - t) *\<^sub>R c + t *\<^sub>R x \<in> k}"
   1.189 +    have *:"c - t *\<^sub>R c + t *\<^sub>R x \<in> s - k" apply safe apply(rule conv[unfolded scaleR_simps]) 
   1.190 +      using `x\<in>s` `c\<in>s` as by(auto simp add:scaleR_simps)
   1.191 +    have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
   1.192 +      apply(rule diff_chain_within) apply(rule has_derivative_add)
   1.193 +      unfolding scaleR_simps apply(rule has_derivative_sub) apply(rule has_derivative_const)
   1.194 +      apply(rule has_derivative_vmul_within,rule has_derivative_id)+ 
   1.195 +      apply(rule has_derivative_within_subset,rule assms(6)[rule_format])
   1.196 +      apply(rule *) apply safe apply(rule conv[unfolded scaleR_simps]) using `x\<in>s` `c\<in>s` by auto
   1.197 +    thus "((\<lambda>xa. f ((1 - xa) *\<^sub>R c + xa *\<^sub>R x)) has_derivative (\<lambda>h. 0)) (at t within {0..1})" unfolding o_def .
   1.198 +  qed auto thus ?thesis by auto qed
   1.199 +
   1.200 +subsection {* Also to any open connected set with finite set of exceptions. Could 
   1.201 + generalize to locally convex set with limpt-free set of exceptions. *}
   1.202 +
   1.203 +lemma has_derivative_zero_unique_strong_connected: fixes f::"real^'n \<Rightarrow> 'a::banach"
   1.204 +  assumes "connected s" "open s" "finite k" "continuous_on s f" "c \<in> s" "f c = y"
   1.205 +  "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)" "x\<in>s"
   1.206 +  shows "f x = y"
   1.207 +proof- have "{x \<in> s. f x \<in> {y}} = {} \<or> {x \<in> s. f x \<in> {y}} = s"
   1.208 +    apply(rule assms(1)[unfolded connected_clopen,rule_format]) apply rule defer
   1.209 +    apply(rule continuous_closed_in_preimage[OF assms(4) closed_sing])
   1.210 +    apply(rule open_openin_trans[OF assms(2)]) unfolding open_contains_ball
   1.211 +  proof safe fix x assume "x\<in>s" 
   1.212 +    from assms(2)[unfolded open_contains_ball,rule_format,OF this] guess e .. note e=conjunctD2[OF this]
   1.213 +    show "\<exists>e>0. ball x e \<subseteq> {xa \<in> s. f xa \<in> {f x}}" apply(rule,rule,rule e)
   1.214 +    proof safe fix y assume y:"y \<in> ball x e" thus "y\<in>s" using e by auto
   1.215 +      show "f y = f x" apply(rule has_derivative_zero_unique_strong_convex[OF convex_ball])
   1.216 +        apply(rule assms) apply(rule continuous_on_subset,rule assms) apply(rule e)+
   1.217 +        apply(subst centre_in_ball,rule e,rule) apply safe
   1.218 +        apply(rule has_derivative_within_subset) apply(rule assms(7)[rule_format])
   1.219 +        using y e by auto qed qed
   1.220 +  thus ?thesis using `x\<in>s` `f c = y` `c\<in>s` by auto qed
   1.221 +
   1.222 +subsection {* Integrating characteristic function of an interval. *}
   1.223 +
   1.224 +lemma has_integral_restrict_open_subinterval: fixes f::"real^'n \<Rightarrow> 'a::banach"
   1.225 +  assumes "(f has_integral i) {c..d}" "{c..d} \<subseteq> {a..b}"
   1.226 +  shows "((\<lambda>x. if x \<in> {c<..<d} then f x else 0) has_integral i) {a..b}"
   1.227 +proof- def g \<equiv> "\<lambda>x. if x \<in>{c<..<d} then f x else 0"
   1.228 +  { presume *:"{c..d}\<noteq>{} \<Longrightarrow> ?thesis"
   1.229 +    show ?thesis apply(cases,rule *,assumption)
   1.230 +    proof- case goal1 hence *:"{c<..<d} = {}" using interval_open_subset_closed by auto 
   1.231 +      show ?thesis using assms(1) unfolding * using goal1 by auto
   1.232 +    qed } assume "{c..d}\<noteq>{}"
   1.233 +  from partial_division_extend_1[OF assms(2) this] guess p . note p=this
   1.234 +  note mon = monoidal_lifted[OF monoidal_monoid] 
   1.235 +  note operat = operative_division[OF this operative_integral p(1), THEN sym]
   1.236 +  let ?P = "(if g integrable_on {a..b} then Some (integral {a..b} g) else None) = Some i"
   1.237 +  { presume "?P" hence "g integrable_on {a..b} \<and> integral {a..b} g = i"
   1.238 +      apply- apply(cases,subst(asm) if_P,assumption) by auto
   1.239 +    thus ?thesis using integrable_integral unfolding g_def by auto }
   1.240 +
   1.241 +  note iterate_eq_neutral[OF mon,unfolded neutral_lifted[OF monoidal_monoid]]
   1.242 +  note * = this[unfolded neutral_monoid]
   1.243 +  have iterate:"iterate (lifted op +) (p - {{c..d}})
   1.244 +      (\<lambda>i. if g integrable_on i then Some (integral i g) else None) = Some 0"
   1.245 +  proof(rule *,rule) case goal1 hence "x\<in>p" by auto note div = division_ofD(2-5)[OF p(1) this]
   1.246 +    from div(3) guess u v apply-by(erule exE)+ note uv=this
   1.247 +    have "interior x \<inter> interior {c..d} = {}" using div(4)[OF p(2)] goal1 by auto
   1.248 +    hence "(g has_integral 0) x" unfolding uv apply-apply(rule has_integral_spike_interior[where f="\<lambda>x. 0"])
   1.249 +      unfolding g_def interior_closed_interval by auto thus ?case by auto
   1.250 +  qed
   1.251 +
   1.252 +  have *:"p = insert {c..d} (p - {{c..d}})" using p by auto
   1.253 +  have **:"g integrable_on {c..d}" apply(rule integrable_spike_interior[where f=f])
   1.254 +    unfolding g_def defer apply(rule has_integral_integrable) using assms(1) by auto
   1.255 +  moreover have "integral {c..d} g = i" apply(rule has_integral_unique[OF _ assms(1)])
   1.256 +    apply(rule has_integral_spike_interior[where f=g]) defer
   1.257 +    apply(rule integrable_integral[OF **]) unfolding g_def by auto
   1.258 +  ultimately show ?P unfolding operat apply- apply(subst *) apply(subst iterate_insert) apply rule+
   1.259 +    unfolding iterate defer apply(subst if_not_P) defer using p by auto qed
   1.260 +
   1.261 +lemma has_integral_restrict_closed_subinterval: fixes f::"real^'n \<Rightarrow> 'a::banach"
   1.262 +  assumes "(f has_integral i) ({c..d})" "{c..d} \<subseteq> {a..b}" 
   1.263 +  shows "((\<lambda>x. if x \<in> {c..d} then f x else 0) has_integral i) {a..b}"
   1.264 +proof- note has_integral_restrict_open_subinterval[OF assms]
   1.265 +  note * = has_integral_spike[OF negligible_frontier_interval _ this]
   1.266 +  show ?thesis apply(rule *[of c d]) using interval_open_subset_closed[of c d] by auto qed
   1.267 +
   1.268 +lemma has_integral_restrict_closed_subintervals_eq: fixes f::"real^'n \<Rightarrow> 'a::banach" assumes "{c..d} \<subseteq> {a..b}" 
   1.269 +  shows "((\<lambda>x. if x \<in> {c..d} then f x else 0) has_integral i) {a..b} \<longleftrightarrow> (f has_integral i) {c..d}" (is "?l = ?r")
   1.270 +proof(cases "{c..d} = {}") case False let ?g = "\<lambda>x. if x \<in> {c..d} then f x else 0"
   1.271 +  show ?thesis apply rule defer apply(rule has_integral_restrict_closed_subinterval[OF _ assms])
   1.272 +  proof assumption assume ?l hence "?g integrable_on {c..d}"
   1.273 +      apply-apply(rule integrable_subinterval[OF _ assms]) by auto
   1.274 +    hence *:"f integrable_on {c..d}"apply-apply(rule integrable_eq) by auto
   1.275 +    hence "i = integral {c..d} f" apply-apply(rule has_integral_unique)
   1.276 +      apply(rule `?l`) apply(rule has_integral_restrict_closed_subinterval[OF _ assms]) by auto
   1.277 +    thus ?r using * by auto qed qed auto
   1.278 +
   1.279 +subsection {* Hence we can apply the limit process uniformly to all integrals. *}
   1.280 +
   1.281 +lemma has_integral': fixes f::"real^'n \<Rightarrow> 'a::banach" shows
   1.282 + "(f has_integral i) s \<longleftrightarrow> (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b}
   1.283 +  \<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> s then f(x) else 0) has_integral z) {a..b} \<and> norm(z - i) < e))" (is "?l \<longleftrightarrow> (\<forall>e>0. ?r e)")
   1.284 +proof- { presume *:"\<exists>a b. s = {a..b} \<Longrightarrow> ?thesis"
   1.285 +    show ?thesis apply(cases,rule *,assumption)
   1.286 +      apply(subst has_integral_alt) by auto }
   1.287 +  assume "\<exists>a b. s = {a..b}" then guess a b apply-by(erule exE)+ note s=this
   1.288 +  from bounded_interval[of a b, THEN conjunct1, unfolded bounded_pos] guess B ..
   1.289 +  note B = conjunctD2[OF this,rule_format] show ?thesis apply safe
   1.290 +  proof- fix e assume ?l "e>(0::real)"
   1.291 +    show "?r e" apply(rule_tac x="B+1" in exI) apply safe defer apply(rule_tac x=i in exI)
   1.292 +    proof fix c d assume as:"ball 0 (B+1) \<subseteq> {c..d::real^'n}"
   1.293 +      thus "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) {c..d}" unfolding s
   1.294 +        apply-apply(rule has_integral_restrict_closed_subinterval) apply(rule `?l`[unfolded s])
   1.295 +        apply safe apply(drule B(2)[rule_format]) unfolding subset_eq apply(erule_tac x=x in ballE)
   1.296 +        by(auto simp add:vector_dist_norm)
   1.297 +    qed(insert B `e>0`, auto)
   1.298 +  next assume as:"\<forall>e>0. ?r e" 
   1.299 +    from this[rule_format,OF zero_less_one] guess C .. note C=conjunctD2[OF this,rule_format]
   1.300 +    def c \<equiv> "(\<chi> i. - max B C)::real^'n" and d \<equiv> "(\<chi> i. max B C)::real^'n"
   1.301 +    have c_d:"{a..b} \<subseteq> {c..d}" apply safe apply(drule B(2)) unfolding mem_interval
   1.302 +    proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def
   1.303 +        by(auto simp add:field_simps) qed
   1.304 +    have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball vector_dist_norm 
   1.305 +    proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
   1.306 +    from C(2)[OF this] have "\<exists>y. (f has_integral y) {a..b}"
   1.307 +      unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,THEN sym] unfolding s by auto
   1.308 +    then guess y .. note y=this
   1.309 +
   1.310 +    have "y = i" proof(rule ccontr) assume "y\<noteq>i" hence "0 < norm (y - i)" by auto
   1.311 +      from as[rule_format,OF this] guess C ..  note C=conjunctD2[OF this,rule_format]
   1.312 +      def c \<equiv> "(\<chi> i. - max B C)::real^'n" and d \<equiv> "(\<chi> i. max B C)::real^'n"
   1.313 +      have c_d:"{a..b} \<subseteq> {c..d}" apply safe apply(drule B(2)) unfolding mem_interval
   1.314 +      proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def
   1.315 +          by(auto simp add:field_simps) qed
   1.316 +      have "ball 0 C \<subseteq> {c..d}" apply safe unfolding mem_interval mem_ball vector_dist_norm 
   1.317 +      proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
   1.318 +      note C(2)[OF this] then guess z .. note z = conjunctD2[OF this, unfolded s]
   1.319 +      note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]]
   1.320 +      hence "z = y" "norm (z - i) < norm (y - i)" apply- apply(rule has_integral_unique[OF _ y(1)]) .
   1.321 +      thus False by auto qed
   1.322 +    thus ?l using y unfolding s by auto qed qed 
   1.323 +
   1.324 +subsection {* Hence a general restriction property. *}
   1.325 +
   1.326 +lemma has_integral_restrict[simp]: assumes "s \<subseteq> t" shows
   1.327 +  "((\<lambda>x. if x \<in> s then f x else (0::'a::banach)) has_integral i) t \<longleftrightarrow> (f has_integral i) s"
   1.328 +proof- have *:"\<And>x. (if x \<in> t then if x \<in> s then f x else 0 else 0) =  (if x\<in>s then f x else 0)" using assms by auto
   1.329 +  show ?thesis apply(subst(2) has_integral') apply(subst has_integral') unfolding * by rule qed
   1.330 +
   1.331 +lemma has_integral_restrict_univ: fixes f::"real^'n \<Rightarrow> 'a::banach" shows
   1.332 +  "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) UNIV \<longleftrightarrow> (f has_integral i) s" by auto
   1.333 +
   1.334 +lemma has_integral_on_superset: fixes f::"real^'n \<Rightarrow> 'a::banach" 
   1.335 +  assumes "\<forall>x. ~(x \<in> s) \<longrightarrow> f x = 0" "s \<subseteq> t" "(f has_integral i) s"
   1.336 +  shows "(f has_integral i) t"
   1.337 +proof- have "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. if x \<in> t then f x else 0)"
   1.338 +    apply(rule) using assms(1-2) by auto
   1.339 +  thus ?thesis apply- using assms(3) apply(subst has_integral_restrict_univ[THEN sym])
   1.340 +  apply- apply(subst(asm) has_integral_restrict_univ[THEN sym]) by auto qed
   1.341 +
   1.342 +lemma integrable_on_superset: fixes f::"real^'n \<Rightarrow> 'a::banach" 
   1.343 +  assumes "\<forall>x. ~(x \<in> s) \<longrightarrow> f x = 0" "s \<subseteq> t" "f integrable_on s"
   1.344 +  shows "f integrable_on t"
   1.345 +  using assms unfolding integrable_on_def by(auto intro:has_integral_on_superset)
   1.346 +
   1.347 +lemma integral_restrict_univ[intro]: fixes f::"real^'n \<Rightarrow> 'a::banach" 
   1.348 +  shows "f integrable_on s \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> s then f x else 0) = integral s f"
   1.349 +  apply(rule integral_unique) unfolding has_integral_restrict_univ by auto
   1.350 +
   1.351 +lemma integrable_restrict_univ: fixes f::"real^'n \<Rightarrow> 'a::banach" shows
   1.352 + "(\<lambda>x. if x \<in> s then f x else 0) integrable_on UNIV \<longleftrightarrow> f integrable_on s"
   1.353 +  unfolding integrable_on_def by auto
   1.354 +
   1.355 +lemma negligible_on_intervals: "negligible s \<longleftrightarrow> (\<forall>a b. negligible(s \<inter> {a..b}))" (is "?l = ?r")
   1.356 +proof assume ?r show ?l unfolding negligible_def
   1.357 +  proof safe case goal1 show ?case apply(rule has_integral_negligible[OF `?r`[rule_format,of a b]])
   1.358 +      unfolding indicator_def by auto qed qed auto
   1.359 +
   1.360 +lemma has_integral_spike_set_eq: fixes f::"real^'n \<Rightarrow> 'a::banach" 
   1.361 +  assumes "negligible((s - t) \<union> (t - s))" shows "((f has_integral y) s \<longleftrightarrow> (f has_integral y) t)"
   1.362 +  unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by auto
   1.363 +
   1.364 +lemma has_integral_spike_set[dest]: fixes f::"real^'n \<Rightarrow> 'a::banach"
   1.365 +  assumes "negligible((s - t) \<union> (t - s))" "(f has_integral y) s"
   1.366 +  shows "(f has_integral y) t"
   1.367 +  using assms has_integral_spike_set_eq by auto
   1.368 +
   1.369 +lemma integrable_spike_set[dest]: fixes f::"real^'n \<Rightarrow> 'a::banach"
   1.370 +  assumes "negligible((s - t) \<union> (t - s))" "f integrable_on s"
   1.371 +  shows "f integrable_on t" using assms(2) unfolding integrable_on_def 
   1.372 +  unfolding has_integral_spike_set_eq[OF assms(1)] .
   1.373 +
   1.374 +lemma integrable_spike_set_eq: fixes f::"real^'n \<Rightarrow> 'a::banach"
   1.375 +  assumes "negligible((s - t) \<union> (t - s))"
   1.376 +  shows "(f integrable_on s \<longleftrightarrow> f integrable_on t)"
   1.377 +  apply(rule,rule_tac[!] integrable_spike_set) using assms by auto
   1.378 +
   1.379 +(*lemma integral_spike_set:
   1.380 + "\<forall>f:real^M->real^N g s t.
   1.381 +        negligible(s DIFF t \<union> t DIFF s)
   1.382 +        \<longrightarrow> integral s f = integral t f"
   1.383 +qed  REPEAT STRIP_TAC THEN REWRITE_TAC[integral] THEN
   1.384 +  AP_TERM_TAC THEN ABS_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN
   1.385 +  ASM_MESON_TAC[]);;
   1.386 +
   1.387 +lemma has_integral_interior:
   1.388 + "\<forall>f:real^M->real^N y s.
   1.389 +        negligible(frontier s)
   1.390 +        \<longrightarrow> ((f has_integral y) (interior s) \<longleftrightarrow> (f has_integral y) s)"
   1.391 +qed  REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN
   1.392 +  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
   1.393 +    NEGLIGIBLE_SUBSET)) THEN
   1.394 +  REWRITE_TAC[frontier] THEN
   1.395 +  MP_TAC(ISPEC `s:real^M->bool` INTERIOR_SUBSET) THEN
   1.396 +  MP_TAC(ISPEC `s:real^M->bool` CLOSURE_SUBSET) THEN
   1.397 +  SET_TAC[]);;
   1.398 +
   1.399 +lemma has_integral_closure:
   1.400 + "\<forall>f:real^M->real^N y s.
   1.401 +        negligible(frontier s)
   1.402 +        \<longrightarrow> ((f has_integral y) (closure s) \<longleftrightarrow> (f has_integral y) s)"
   1.403 +qed  REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN
   1.404 +  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
   1.405 +    NEGLIGIBLE_SUBSET)) THEN
   1.406 +  REWRITE_TAC[frontier] THEN
   1.407 +  MP_TAC(ISPEC `s:real^M->bool` INTERIOR_SUBSET) THEN
   1.408 +  MP_TAC(ISPEC `s:real^M->bool` CLOSURE_SUBSET) THEN
   1.409 +  SET_TAC[]);;*)
   1.410 +
   1.411 +subsection {* More lemmas that are useful later. *}
   1.412 +
   1.413 +lemma has_integral_subset_component_le: fixes f::"real^'n \<Rightarrow> real^'m"
   1.414 +  assumes "s \<subseteq> t" "(f has_integral i) s" "(f has_integral j) t" "\<forall>x\<in>t. 0 \<le> f(x)$k"
   1.415 +  shows "i$k \<le> j$k"
   1.416 +proof- note has_integral_restrict_univ[THEN sym, of f]
   1.417 +  note assms(2-3)[unfolded this] note * = has_integral_component_le[OF this]
   1.418 +  show ?thesis apply(rule *) using assms(1,4) by auto qed
   1.419 +
   1.420 +lemma integral_subset_component_le: fixes f::"real^'n \<Rightarrow> real^'m"
   1.421 +  assumes "s \<subseteq> t" "f integrable_on s" "f integrable_on t" "\<forall>x \<in> t. 0 \<le> f(x)$k"
   1.422 +  shows "(integral s f)$k \<le> (integral t f)$k"
   1.423 +  apply(rule has_integral_subset_component_le) using assms by auto
   1.424 +
   1.425 +lemma has_integral_alt': fixes f::"real^'n \<Rightarrow> 'a::banach"
   1.426 +  shows "(f has_integral i) s \<longleftrightarrow> (\<forall>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}) \<and>
   1.427 +  (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e)" (is "?l = ?r")
   1.428 +proof assume ?r
   1.429 +  show ?l apply- apply(subst has_integral')
   1.430 +  proof safe case goal1 from `?r`[THEN conjunct2,rule_format,OF this] guess B .. note B=conjunctD2[OF this]
   1.431 +    show ?case apply(rule,rule,rule B,safe)
   1.432 +      apply(rule_tac x="integral {a..b} (\<lambda>x. if x \<in> s then f x else 0)" in exI)
   1.433 +      apply(drule B(2)[rule_format]) using integrable_integral[OF `?r`[THEN conjunct1,rule_format]] by auto
   1.434 +  qed next
   1.435 +  assume ?l note as = this[unfolded has_integral'[of f],rule_format]
   1.436 +  let ?f = "\<lambda>x. if x \<in> s then f x else 0"
   1.437 +  show ?r proof safe fix a b::"real^'n"
   1.438 +    from as[OF zero_less_one] guess B .. note B=conjunctD2[OF this,rule_format]
   1.439 +    let ?a = "(\<chi> i. min (a$i) (-B))::real^'n" and ?b = "(\<chi> i. max (b$i) B)::real^'n"
   1.440 +    show "?f integrable_on {a..b}" apply(rule integrable_subinterval[of _ ?a ?b])
   1.441 +    proof- have "ball 0 B \<subseteq> {?a..?b}" apply safe unfolding mem_ball mem_interval vector_dist_norm
   1.442 +      proof case goal1 thus ?case using component_le_norm[of x i] by(auto simp add:field_simps) qed
   1.443 +      from B(2)[OF this] guess z .. note conjunct1[OF this]
   1.444 +      thus "?f integrable_on {?a..?b}" unfolding integrable_on_def by auto
   1.445 +      show "{a..b} \<subseteq> {?a..?b}" apply safe unfolding mem_interval apply(rule,erule_tac x=i in allE) by auto qed
   1.446 +
   1.447 +    fix e::real assume "e>0" from as[OF this] guess B .. note B=conjunctD2[OF this,rule_format]
   1.448 +    show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
   1.449 +                    norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
   1.450 +    proof(rule,rule,rule B,safe) case goal1 from B(2)[OF this] guess z .. note z=conjunctD2[OF this]
   1.451 +      from integral_unique[OF this(1)] show ?case using z(2) by auto qed qed qed 
   1.452 +
   1.453  end