merged
authorpaulson
Sun Aug 06 22:54:17 2017 +0200 (2017-08-06)
changeset 66360af5c71cffec5
parent 66358 fab9a53158f8
parent 66359 8ed88442d7bb
child 66361 5deeb0dbccb4
child 66365 d77a4ab4fe59
child 66367 b60afdf1177d
merged
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 06 21:49:25 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 06 22:54:17 2017 +0200
     1.3 @@ -9,6 +9,10 @@
     1.4    Lebesgue_Measure Tagged_Division
     1.5  begin
     1.6  
     1.7 +lemma eps_leI: 
     1.8 +  assumes "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> y"
     1.9 +  by (metis add_diff_eq assms diff_diff_add diff_gt_0_iff_gt linorder_not_less order_less_irrefl)
    1.10 +
    1.11  (*FIXME DELETE*)
    1.12  lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
    1.13  
    1.14 @@ -1260,7 +1264,7 @@
    1.15  
    1.16  lemma has_integral_separate_sides:
    1.17    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
    1.18 -  assumes "(f has_integral i) (cbox a b)"
    1.19 +  assumes f: "(f has_integral i) (cbox a b)"
    1.20      and "e > 0"
    1.21      and k: "k \<in> Basis"
    1.22    obtains d where "gauge d"
    1.23 @@ -1268,18 +1272,23 @@
    1.24          p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) \<and> d fine p2 \<longrightarrow>
    1.25          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"
    1.26  proof -
    1.27 -  guess d using has_integralD[OF assms(1-2)] . note d=this
    1.28 +  obtain \<gamma> where d: "gauge \<gamma>"
    1.29 +      "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma> fine p\<rbrakk>
    1.30 +            \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) < e"
    1.31 +    using has_integralD[OF f \<open>e > 0\<close>] by metis
    1.32    { fix p1 p2
    1.33 -    assume "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" "d fine p1"
    1.34 -    note p1=tagged_division_ofD[OF this(1)] this
    1.35 -    assume "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> k}" "d fine p2"
    1.36 -    note p2=tagged_division_ofD[OF this(1)] this
    1.37 -    note tagged_division_union_interval[OF p1(7) p2(7)] note p12 = tagged_division_ofD[OF this] this
    1.38 +    assume tdiv1: "p1 tagged_division_of (cbox a b) \<inter> {x. x \<bullet> k \<le> c}" and "\<gamma> fine p1"
    1.39 +    note p1=tagged_division_ofD[OF this(1)] 
    1.40 +    assume tdiv2: "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> k}" and "\<gamma> fine p2"
    1.41 +    note p2=tagged_division_ofD[OF this(1)] 
    1.42 +    note tagged_division_union_interval[OF tdiv1 tdiv2] 
    1.43 +    note p12 = tagged_division_ofD[OF this] this
    1.44      { fix a b
    1.45        assume ab: "(a, b) \<in> p1 \<inter> p2"
    1.46        have "(a, b) \<in> p1"
    1.47          using ab by auto
    1.48 -      with p1 obtain u v where uv: "b = cbox u v" by auto
    1.49 +      obtain u v where uv: "b = cbox u v"
    1.50 +        using \<open>(a, b) \<in> p1\<close> p1(4) by moura
    1.51        have "b \<subseteq> {x. x\<bullet>k = c}"
    1.52          using ab p1(3)[of a b] p2(3)[of a b] by fastforce
    1.53        moreover
    1.54 @@ -1288,25 +1297,23 @@
    1.55          assume "\<not> ?thesis"
    1.56          then obtain x where x: "x \<in> interior {x::'a. x\<bullet>k = c}"
    1.57            by auto
    1.58 -        then guess e unfolding mem_interior .. note e=this
    1.59 +        then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> {x. x \<bullet> k = c}"
    1.60 +          using mem_interior by metis
    1.61          have x: "x\<bullet>k = c"
    1.62            using x interior_subset by fastforce
    1.63 -        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)"
    1.64 -          using e k by (auto simp: inner_simps inner_not_same_Basis)
    1.65 -        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (e / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
    1.66 -              (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))"
    1.67 +        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)"
    1.68 +          using \<open>0 < \<epsilon>\<close> k by (auto simp: inner_simps inner_not_same_Basis)
    1.69 +        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon> / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
    1.70 +              (\<Sum>i\<in>Basis. (if i = k then \<epsilon> / 2 else 0))"
    1.71            using "*" by (blast intro: sum.cong)
    1.72 -        also have "\<dots> < e"
    1.73 -          apply (subst sum.delta)
    1.74 -          using e
    1.75 -          apply auto
    1.76 -          done
    1.77 -        finally have "x + (e/2) *\<^sub>R k \<in> ball x e"
    1.78 +        also have "\<dots> < \<epsilon>"
    1.79 +          by (subst sum.delta) (use \<open>0 < \<epsilon>\<close> in auto)
    1.80 +        finally have "x + (\<epsilon>/2) *\<^sub>R k \<in> ball x \<epsilon>"
    1.81            unfolding mem_ball dist_norm by(rule le_less_trans[OF norm_le_l1])
    1.82 -        then have "x + (e/2) *\<^sub>R k \<in> {x. x\<bullet>k = c}"
    1.83 -          using e by auto
    1.84 +        then have "x + (\<epsilon>/2) *\<^sub>R k \<in> {x. x\<bullet>k = c}"
    1.85 +          using \<epsilon> by auto
    1.86          then show False
    1.87 -          unfolding mem_Collect_eq using e x k by (auto simp: inner_simps)
    1.88 +          using \<open>0 < \<epsilon>\<close> x k by (auto simp: inner_simps)
    1.89        qed
    1.90        ultimately have "content b = 0"
    1.91          unfolding uv content_eq_0_interior
    1.92 @@ -1318,11 +1325,11 @@
    1.93                 norm ((\<Sum>(x, k)\<in>p1 \<union> p2. content k *\<^sub>R f x) - i)"
    1.94        by (subst sum.union_inter_neutral) (auto simp: p1 p2)
    1.95      also have "\<dots> < e"
    1.96 -      by (rule k d(2) p12 fine_Un p1 p2)+
    1.97 +      using d(2) p12 by (simp add: fine_Un k \<open>\<gamma> fine p1\<close> \<open>\<gamma> fine p2\<close>)
    1.98      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" .
    1.99     }
   1.100    then show ?thesis
   1.101 -    by (auto intro: that[of d] d elim: )
   1.102 +    using d(1) that by auto
   1.103  qed
   1.104  
   1.105  lemma integrable_split [intro]:
   1.106 @@ -6796,68 +6803,72 @@
   1.107      and "\<forall>x\<in>s. norm (f x) \<le> g x"
   1.108    shows "norm (integral s f) \<le> integral s g"
   1.109  proof -
   1.110 -  have *: "\<And>x y. (\<forall>e::real. 0 < e \<longrightarrow> x < y + e) \<Longrightarrow> x \<le> y"
   1.111 -    apply (rule ccontr)
   1.112 -    apply (erule_tac x="x - y" in allE)
   1.113 -    apply auto
   1.114 -    done
   1.115    have norm: "norm ig < dia + e"
   1.116 -    if "norm sg \<le> dsa"
   1.117 -    and "\<bar>dsa - dia\<bar> < e / 2"
   1.118 -    and "norm (sg - ig) < e / 2"
   1.119 +    if "norm sg \<le> dsa" and "\<bar>dsa - dia\<bar> < e / 2" and "norm (sg - ig) < e / 2"
   1.120      for e dsa dia and sg ig :: 'a
   1.121      apply (rule le_less_trans[OF norm_triangle_sub[of ig sg]])
   1.122      apply (subst real_sum_of_halves[of e,symmetric])
   1.123      unfolding add.assoc[symmetric]
   1.124      apply (rule add_le_less_mono)
   1.125 -    defer
   1.126 -    apply (subst norm_minus_commute)
   1.127 -    apply (rule that(3))
   1.128 +     defer
   1.129 +     apply (subst norm_minus_commute)
   1.130 +     apply (rule that(3))
   1.131      apply (rule order_trans[OF that(1)])
   1.132      using that(2)
   1.133      apply arith
   1.134      done
   1.135    have lem: "norm (integral(cbox a b) f) \<le> integral (cbox a b) g"
   1.136 -    if "f integrable_on cbox a b"
   1.137 -    and "g integrable_on cbox a b"
   1.138 -    and "\<forall>x\<in>cbox a b. norm (f x) \<le> g x"
   1.139 +    if f: "f integrable_on cbox a b"
   1.140 +    and g: "g integrable_on cbox a b"
   1.141 +    and nle: "\<And>x. x \<in> cbox a b \<Longrightarrow> norm (f x) \<le> g x"
   1.142      for f :: "'n \<Rightarrow> 'a" and g a b
   1.143 -  proof (rule *[rule_format])
   1.144 +  proof (rule eps_leI)
   1.145      fix e :: real
   1.146      assume "e > 0"
   1.147 -    then have *: "e/2 > 0"
   1.148 +    then have e: "e/2 > 0"
   1.149        by auto
   1.150 -    from integrable_integral[OF that(1),unfolded has_integral[of f],rule_format,OF *]
   1.151 -    guess d1 .. note d1 = conjunctD2[OF this,rule_format]
   1.152 -    from integrable_integral[OF that(2),unfolded has_integral[of g],rule_format,OF *]
   1.153 -    guess d2 .. note d2 = conjunctD2[OF this,rule_format]
   1.154 -    note gauge_Int[OF d1(1) d2(1)]
   1.155 -    from fine_division_exists[OF this, of a b] guess p . note p=this
   1.156 +    with integrable_integral[OF f,unfolded has_integral[of f]]
   1.157 +    obtain \<gamma> where \<gamma>: "gauge \<gamma>"
   1.158 +              "\<And>p. p tagged_division_of cbox a b \<and> \<gamma> fine p 
   1.159 +           \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral (cbox a b) f) < e / 2"
   1.160 +      by meson 
   1.161 +    moreover
   1.162 +    from integrable_integral[OF g,unfolded has_integral[of g]] e
   1.163 +    obtain \<delta> where \<delta>: "gauge \<delta>"
   1.164 +              "\<And>p. p tagged_division_of cbox a b \<and> \<delta> fine p 
   1.165 +           \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - integral (cbox a b) g) < e / 2"
   1.166 +      by meson
   1.167 +    ultimately have "gauge (\<lambda>x. \<gamma> x \<inter> \<delta> x)"
   1.168 +      using gauge_Int by blast
   1.169 +    with fine_division_exists obtain p 
   1.170 +      where p: "p tagged_division_of cbox a b" "(\<lambda>x. \<gamma> x \<inter> \<delta> x) fine p" 
   1.171 +      by metis
   1.172 +    have "\<gamma> fine p" "\<delta> fine p"
   1.173 +      using fine_Int p(2) by blast+
   1.174      show "norm (integral (cbox a b) f) < integral (cbox a b) g + e"
   1.175 -      apply (rule norm)
   1.176 -      defer
   1.177 -      apply (rule d2(2)[OF conjI[OF p(1)],unfolded real_norm_def])
   1.178 -      defer
   1.179 -      apply (rule d1(2)[OF conjI[OF p(1)]])
   1.180 -      defer
   1.181 -      apply (rule sum_norm_le)
   1.182 -    proof safe
   1.183 -      fix x k
   1.184 -      assume "(x, k) \<in> p"
   1.185 -      note as = tagged_division_ofD(2-4)[OF p(1) this]
   1.186 -      from this(3) guess u v by (elim exE) note uv=this
   1.187 -      show "norm (content k *\<^sub>R f x) \<le> content k *\<^sub>R g x"
   1.188 -        unfolding uv norm_scaleR
   1.189 -        unfolding abs_of_nonneg[OF content_pos_le] real_scaleR_def
   1.190 -        apply (rule mult_left_mono)
   1.191 -        using that(3) as
   1.192 -        apply auto
   1.193 -        done
   1.194 -    qed (insert p[unfolded fine_Int], auto)
   1.195 +    proof (rule norm)
   1.196 +      have "norm (content K *\<^sub>R f x) \<le> content K *\<^sub>R g x" if  "(x, K) \<in> p" for x K
   1.197 +      proof-
   1.198 +        have K: "x \<in> K" "K \<subseteq> cbox a b"
   1.199 +          using \<open>(x, K) \<in> p\<close> p(1) by blast+
   1.200 +        obtain u v where  "K = cbox u v"
   1.201 +          using \<open>(x, K) \<in> p\<close> p(1) by blast
   1.202 +        moreover have "content K * norm (f x) \<le> content K * g x"
   1.203 +          by (metis K subsetD dual_order.antisym measure_nonneg mult_zero_left nle not_le real_mult_le_cancel_iff2)
   1.204 +        then show ?thesis
   1.205 +          by simp
   1.206 +      qed
   1.207 +      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)"
   1.208 +        by (simp add: sum_norm_le split_def)
   1.209 +      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral (cbox a b) f) < e / 2"
   1.210 +        using \<open>\<gamma> fine p\<close> \<gamma> p(1) by simp
   1.211 +      show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - integral (cbox a b) g\<bar> < e / 2"
   1.212 +        using \<open>\<delta> fine p\<close> \<delta> p(1) by simp
   1.213 +    qed
   1.214    qed
   1.215  
   1.216    { presume "\<And>e. 0 < e \<Longrightarrow> norm (integral s f) < integral s g + e"
   1.217 -    then show ?thesis by (rule *[rule_format]) auto }
   1.218 +    then show ?thesis by (rule eps_leI) auto }
   1.219    fix e :: real
   1.220    assume "e > 0"
   1.221    then have e: "e/2 > 0"
   1.222 @@ -6885,7 +6896,6 @@
   1.223      defer
   1.224      apply (rule w(2)[unfolded real_norm_def])
   1.225      apply (rule z(2))
   1.226 -    apply safe
   1.227      apply (case_tac "x \<in> s")
   1.228      unfolding if_P
   1.229      apply (rule assms(3)[rule_format])
   1.230 @@ -6893,6 +6903,7 @@
   1.231      done
   1.232  qed
   1.233  
   1.234 +
   1.235  lemma integral_norm_bound_integral_component:
   1.236    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.237    fixes g :: "'n \<Rightarrow> 'b::euclidean_space"