src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 63956 b235e845c8e8
parent 63945 444eafb6e864
child 63957 c3da799b1b45
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 29 12:58:55 2016 +0100
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 28 16:15:51 2016 +0200
     1.3 @@ -16,6 +16,28 @@
     1.4  
     1.5  subsection \<open>Sundries\<close>
     1.6  
     1.7 +
     1.8 +text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
     1.9 +lemma wf_finite_segments:
    1.10 +  assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
    1.11 +  shows "wf (r)"
    1.12 +  apply (simp add: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
    1.13 +  using acyclic_def assms irrefl_def trans_Restr by fastforce
    1.14 +
    1.15 +text\<open>For creating values between @{term u} and @{term v}.\<close>
    1.16 +lemma scaling_mono:
    1.17 +  fixes u::"'a::linordered_field"
    1.18 +  assumes "u \<le> v" "0 \<le> r" "r \<le> s"
    1.19 +    shows "u + r * (v - u) / s \<le> v"
    1.20 +proof -
    1.21 +  have "r/s \<le> 1" using assms
    1.22 +    using divide_le_eq_1 by fastforce
    1.23 +  then have "(r/s) * (v - u) \<le> 1 * (v - u)"
    1.24 +    by (meson diff_ge_0_iff_ge mult_right_mono \<open>u \<le> v\<close>)
    1.25 +  then show ?thesis
    1.26 +    by (simp add: field_simps)
    1.27 +qed
    1.28 +
    1.29  lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
    1.30  lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
    1.31  lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
    1.32 @@ -4767,7 +4789,7 @@
    1.33  qed
    1.34  
    1.35  lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
    1.36 -  using negligible_Un negligible_subset by blast 
    1.37 +  using negligible_Un negligible_subset by blast
    1.38  
    1.39  lemma negligible_sing[intro]: "negligible {a::'a::euclidean_space}"
    1.40    using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] negligible_subset by blast
    1.41 @@ -10709,6 +10731,277 @@
    1.42         (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
    1.43  qed
    1.44  
    1.45 +subsubsection \<open>Covering lemma\<close>
    1.46 +
    1.47 +
    1.48 +text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
    1.49 +  lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
    1.50 +  "Introduction to Gauge Integrals". \<close>
    1.51 +
    1.52 +proposition covering_lemma:
    1.53 +  assumes "S \<subseteq> cbox a b" "box a b \<noteq> {}" "gauge g"
    1.54 +  obtains \<D> where
    1.55 +    "countable \<D>"  "\<Union>\<D> \<subseteq> cbox a b"
    1.56 +    "\<And>K. K \<in> \<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
    1.57 +    "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) \<D>"
    1.58 +    "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
    1.59 +    "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
    1.60 +    "S \<subseteq> \<Union>\<D>"
    1.61 +proof -
    1.62 +  have aibi: "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" and normab: "0 < norm(b - a)"
    1.63 +    using \<open>box a b \<noteq> {}\<close> box_eq_empty box_sing by fastforce+
    1.64 +  let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
    1.65 +                    cbox (\<Sum>i \<in> Basis. (a \<bullet> i + (f i / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
    1.66 +                         (\<Sum>i \<in> Basis. (a \<bullet> i + ((f i + 1) / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)"
    1.67 +  let ?D0 = "?K0 ` (SIGMA n:UNIV. PiE Basis (\<lambda>i::'a. lessThan (2^n)))"
    1.68 +  obtain \<D>0 where count: "countable \<D>0"
    1.69 +             and sub: "\<Union>\<D>0 \<subseteq> cbox a b"
    1.70 +             and int:  "\<And>K. K \<in> \<D>0 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
    1.71 +             and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>0; B \<in> \<D>0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
    1.72 +             and SK: "\<And>x. x \<in> S \<Longrightarrow> \<exists>K \<in> \<D>0. x \<in> K \<and> K \<subseteq> g x"
    1.73 +             and cbox: "\<And>u v. cbox u v \<in> \<D>0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
    1.74 +             and fin: "\<And>K. K \<in> \<D>0 \<Longrightarrow> finite {L \<in> \<D>0. K \<subseteq> L}"
    1.75 +  proof
    1.76 +    show "countable ?D0"
    1.77 +      by (simp add: countable_PiE)
    1.78 +  next
    1.79 +    show "\<Union>?D0 \<subseteq> cbox a b"
    1.80 +      apply (simp add: UN_subset_iff)
    1.81 +      apply (intro conjI allI ballI subset_box_imp)
    1.82 +       apply (simp add: divide_simps zero_le_mult_iff aibi)
    1.83 +      apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem)
    1.84 +      done
    1.85 +  next
    1.86 +    show "\<And>K. K \<in> ?D0 \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
    1.87 +      using \<open>box a b \<noteq> {}\<close>
    1.88 +      by (clarsimp simp: box_eq_empty) (fastforce simp add: divide_simps dest: PiE_mem)
    1.89 +  next
    1.90 +    have realff: "(real w) * 2^m < (real v) * 2^n \<longleftrightarrow> w * 2^m < v * 2^n" for m n v w
    1.91 +      using of_nat_less_iff less_imp_of_nat_less by fastforce
    1.92 +    have *: "\<forall>v w. ?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
    1.93 +      for m n --\<open>The symmetry argument requires a single HOL formula\<close>
    1.94 +    proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
    1.95 +      fix v w m and n::nat
    1.96 +      assume "m \<le> n" --\<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
    1.97 +      have "?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
    1.98 +        apply (simp add: subset_box disjoint_interval)
    1.99 +        apply (rule ccontr)
   1.100 +        apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le)
   1.101 +        apply (drule_tac x=i in bspec, assumption)
   1.102 +        using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
   1.103 +        apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
   1.104 +        apply (simp add: power_add, metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)+
   1.105 +        done
   1.106 +      then show "?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
   1.107 +        by meson
   1.108 +    qed auto
   1.109 +    show "\<And>A B. \<lbrakk>A \<in> ?D0; B \<in> ?D0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
   1.110 +      apply (erule imageE SigmaE)+
   1.111 +      using * by simp
   1.112 +  next
   1.113 +    show "\<exists>K \<in> ?D0. x \<in> K \<and> K \<subseteq> g x" if "x \<in> S" for x
   1.114 +    proof (simp only: bex_simps split_paired_Bex_Sigma)
   1.115 +      show "\<exists>n. \<exists>f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f) \<and> ?K0(n,f) \<subseteq> g x"
   1.116 +      proof -
   1.117 +        obtain e where "0 < e"
   1.118 +                   and e: "\<And>y. (\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> e) \<Longrightarrow> y \<in> g x"
   1.119 +        proof -
   1.120 +          have "x \<in> g x" "open (g x)"
   1.121 +            using \<open>gauge g\<close> by (auto simp: gauge_def)
   1.122 +          then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> g x"
   1.123 +            using openE by blast
   1.124 +          have "norm (x - y) < \<epsilon>"
   1.125 +               if "(\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> \<epsilon> / (2 * real DIM('a)))" for y
   1.126 +          proof -
   1.127 +            have "norm (x - y) \<le> (\<Sum>i\<in>Basis. \<bar>x \<bullet> i - y \<bullet> i\<bar>)"
   1.128 +              by (metis (no_types, lifting) inner_diff_left norm_le_l1 setsum.cong)
   1.129 +            also have "... \<le> DIM('a) * (\<epsilon> / (2 * real DIM('a)))"
   1.130 +              by (meson setsum_bounded_above that)
   1.131 +            also have "... = \<epsilon> / 2"
   1.132 +              by (simp add: divide_simps)
   1.133 +            also have "... < \<epsilon>"
   1.134 +              by (simp add: \<open>0 < \<epsilon>\<close>)
   1.135 +            finally show ?thesis .
   1.136 +          qed
   1.137 +          then show ?thesis
   1.138 +            by (rule_tac e = "\<epsilon> / 2 / DIM('a)" in that) (simp_all add:  \<open>0 < \<epsilon>\<close> dist_norm subsetD [OF \<epsilon>])
   1.139 +        qed
   1.140 +        have xab: "x \<in> cbox a b"
   1.141 +          using \<open>x \<in> S\<close> \<open>S \<subseteq> cbox a b\<close> by blast
   1.142 +        obtain n where n: "norm (b - a) / 2^n < e"
   1.143 +          using real_arch_pow_inv [of "e / norm(b - a)" "1/2"] normab \<open>0 < e\<close>
   1.144 +          by (auto simp: divide_simps)
   1.145 +        then have "norm (b - a) < e * 2^n"
   1.146 +          by (auto simp: divide_simps)
   1.147 +        then have bai: "b \<bullet> i - a \<bullet> i < e * 2 ^ n" if "i \<in> Basis" for i
   1.148 +        proof -
   1.149 +          have "b \<bullet> i - a \<bullet> i \<le> norm (b - a)"
   1.150 +            by (metis abs_of_nonneg dual_order.trans inner_diff_left linear norm_ge_zero Basis_le_norm that)
   1.151 +          also have "... < e * 2 ^ n"
   1.152 +            using \<open>norm (b - a) < e * 2 ^ n\<close> by blast
   1.153 +          finally show ?thesis .
   1.154 +        qed
   1.155 +        have D: "(a + n \<le> x \<and> x \<le> a + m) \<Longrightarrow> (a + n \<le> y \<and> y \<le> a + m) \<Longrightarrow> abs(x - y) \<le> m - n"
   1.156 +                 for a m n x and y::real
   1.157 +          by auto
   1.158 +        have "\<forall>i\<in>Basis. \<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
   1.159 +               x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
   1.160 +        proof
   1.161 +          fix i::'a assume "i \<in> Basis"
   1.162 +          consider "x \<bullet> i = b \<bullet> i" | "x \<bullet> i < b \<bullet> i"
   1.163 +            using \<open>i \<in> Basis\<close> mem_box(2) xab by force
   1.164 +          then show "\<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
   1.165 +                          x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
   1.166 +          proof cases
   1.167 +            case 1 then show ?thesis
   1.168 +              by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps divide_simps of_nat_diff \<open>i \<in> Basis\<close> aibi)
   1.169 +          next
   1.170 +            case 2
   1.171 +            then have abi_less: "a \<bullet> i < b \<bullet> i"
   1.172 +              using \<open>i \<in> Basis\<close> xab by (auto simp: mem_box)
   1.173 +            let ?k = "nat \<lfloor>2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)\<rfloor>"
   1.174 +            show ?thesis
   1.175 +            proof (intro exI conjI)
   1.176 +              show "?k < 2 ^ n"
   1.177 +                using aibi xab \<open>i \<in> Basis\<close>
   1.178 +                by (force simp: nat_less_iff floor_less_iff divide_simps 2 mem_box)
   1.179 +            next
   1.180 +              have "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le>
   1.181 +                    a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
   1.182 +                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
   1.183 +                using aibi [OF \<open>i \<in> Basis\<close>] xab 2
   1.184 +                  apply (simp_all add: \<open>i \<in> Basis\<close> mem_box divide_simps)
   1.185 +                done
   1.186 +              also have "... = x \<bullet> i"
   1.187 +                using abi_less by (simp add: divide_simps)
   1.188 +              finally show "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i" .
   1.189 +            next
   1.190 +              have "x \<bullet> i \<le> a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
   1.191 +                using abi_less by (simp add: divide_simps algebra_simps)
   1.192 +              also have "... \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
   1.193 +                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
   1.194 +                using aibi [OF \<open>i \<in> Basis\<close>] xab
   1.195 +                  apply (auto simp: \<open>i \<in> Basis\<close> mem_box divide_simps)
   1.196 +                done
   1.197 +              finally show "x \<bullet> i \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n" .
   1.198 +            qed
   1.199 +          qed
   1.200 +        qed
   1.201 +        then have "\<exists>f\<in>Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f)"
   1.202 +          apply (simp add: mem_box Bex_def)
   1.203 +          apply (clarify dest!: bchoice)
   1.204 +          apply (rule_tac x="restrict f Basis" in exI, simp)
   1.205 +          done
   1.206 +        moreover have "\<And>f. x \<in> ?K0(n,f) \<Longrightarrow> ?K0(n,f) \<subseteq> g x"
   1.207 +          apply (clarsimp simp add: mem_box)
   1.208 +          apply (rule e)
   1.209 +          apply (drule bspec D, assumption)+
   1.210 +          apply (erule order_trans)
   1.211 +          apply (simp add: divide_simps)
   1.212 +          using bai by (force simp: algebra_simps)
   1.213 +        ultimately show ?thesis by auto
   1.214 +      qed
   1.215 +    qed
   1.216 +  next
   1.217 +    show "\<And>u v. cbox u v \<in> ?D0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
   1.218 +      by (force simp: eq_cbox box_eq_empty field_simps dest!: aibi)
   1.219 +  next
   1.220 +    obtain j::'a where "j \<in> Basis"
   1.221 +      using nonempty_Basis by blast
   1.222 +    have "finite {L \<in> ?D0. ?K0(n,f) \<subseteq> L}" if "f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}" for n f
   1.223 +    proof (rule finite_subset)
   1.224 +      let ?B = "(\<lambda>(n, f::'a\<Rightarrow>nat). cbox (\<Sum>i\<in>Basis. (a \<bullet> i + (f i) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
   1.225 +                                        (\<Sum>i\<in>Basis. (a \<bullet> i + ((f i) + 1) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i))
   1.226 +                ` (SIGMA m:atMost n. PiE Basis (\<lambda>i::'a. lessThan (2^m)))"
   1.227 +      have "?K0(m,g) \<in> ?B" if "g \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ m}" "?K0(n,f) \<subseteq> ?K0(m,g)" for m g
   1.228 +      proof -
   1.229 +        have dd: "w / m \<le> v / n \<and> (v+1) / n \<le> (w+1) / m
   1.230 +                  \<Longrightarrow> inverse n \<le> inverse m" for w m v n::real
   1.231 +          by (auto simp: divide_simps algebra_simps)
   1.232 +        have bjaj: "b \<bullet> j - a \<bullet> j > 0"
   1.233 +          using \<open>j \<in> Basis\<close> \<open>box a b \<noteq> {}\<close> box_eq_empty(1) by fastforce
   1.234 +        have "((g j) / 2 ^ m) * (b \<bullet> j - a \<bullet> j) \<le> ((f j) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<and>
   1.235 +              (((f j) + 1) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<le> (((g j) + 1) / 2 ^ m) * (b \<bullet> j - a \<bullet> j)"
   1.236 +          using that \<open>j \<in> Basis\<close> by (simp add: subset_box algebra_simps divide_simps aibi)
   1.237 +        then have "((g j) / 2 ^ m) \<le> ((f j) / 2 ^ n) \<and>
   1.238 +          ((real(f j) + 1) / 2 ^ n) \<le> ((real(g j) + 1) / 2 ^ m)"
   1.239 +          by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2)
   1.240 +        then have "inverse (2^n) \<le> (inverse (2^m) :: real)"
   1.241 +          by (rule dd)
   1.242 +        then have "m \<le> n"
   1.243 +          by auto
   1.244 +        show ?thesis
   1.245 +          by (rule imageI) (simp add: \<open>m \<le> n\<close> that)
   1.246 +      qed
   1.247 +      then show "{L \<in> ?D0. ?K0(n,f) \<subseteq> L} \<subseteq> ?B"
   1.248 +        by auto
   1.249 +      show "finite ?B"
   1.250 +        by (intro finite_imageI finite_SigmaI finite_atMost finite_lessThan finite_PiE finite_Basis)
   1.251 +    qed
   1.252 +    then show "finite {L \<in> ?D0. K \<subseteq> L}" if "K \<in> ?D0" for K
   1.253 +      using that by auto
   1.254 +  qed
   1.255 +  let ?D1 = "{K \<in> \<D>0. \<exists>x \<in> S \<inter> K. K \<subseteq> g x}"
   1.256 +  obtain \<D> where count: "countable \<D>"
   1.257 +             and sub: "\<Union>\<D> \<subseteq> cbox a b"  "S \<subseteq> \<Union>\<D>"
   1.258 +             and int:  "\<And>K. K \<in> \<D> \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
   1.259 +             and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>; B \<in> \<D>\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
   1.260 +             and SK: "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
   1.261 +             and cbox: "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
   1.262 +             and fin: "\<And>K. K \<in> \<D> \<Longrightarrow> finite {L. L \<in> \<D> \<and> K \<subseteq> L}"
   1.263 +  proof
   1.264 +    show "countable ?D1" using count countable_subset
   1.265 +      by (simp add: count countable_subset)
   1.266 +    show "\<Union>?D1 \<subseteq> cbox a b"
   1.267 +      using sub by blast
   1.268 +    show "S \<subseteq> \<Union>?D1"
   1.269 +      using SK by (force simp:)
   1.270 +    show "\<And>K. K \<in> ?D1 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
   1.271 +      using int by blast
   1.272 +    show "\<And>A B. \<lbrakk>A \<in> ?D1; B \<in> ?D1\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
   1.273 +      using intdj by blast
   1.274 +    show "\<And>K. K \<in> ?D1 \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
   1.275 +      by auto
   1.276 +    show "\<And>u v. cbox u v \<in> ?D1 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
   1.277 +      using cbox by blast
   1.278 +    show "\<And>K. K \<in> ?D1 \<Longrightarrow> finite {L. L \<in> ?D1 \<and> K \<subseteq> L}"
   1.279 +      using fin by simp (metis (mono_tags, lifting) Collect_mono rev_finite_subset)
   1.280 +  qed
   1.281 +  let ?\<D> = "{K \<in> \<D>. \<forall>K'. K' \<in> \<D> \<and> K \<noteq> K' \<longrightarrow> ~(K \<subseteq> K')}"
   1.282 +  show ?thesis
   1.283 +  proof (rule that)
   1.284 +    show "countable ?\<D>"
   1.285 +      by (blast intro: countable_subset [OF _ count])
   1.286 +    show "\<Union>?\<D> \<subseteq> cbox a b"
   1.287 +      using sub by blast
   1.288 +    show "S \<subseteq> \<Union>?\<D>"
   1.289 +    proof clarsimp
   1.290 +      fix x
   1.291 +      assume "x \<in> S"
   1.292 +      then obtain X where "x \<in> X" "X \<in> \<D>" using \<open>S \<subseteq> \<Union>\<D>\<close> by blast
   1.293 +      let ?R = "{(K,L). K \<in> \<D> \<and> L \<in> \<D> \<and> L \<subset> K}"
   1.294 +      have irrR: "irrefl ?R" by (force simp: irrefl_def)
   1.295 +      have traR: "trans ?R" by (force simp: trans_def)
   1.296 +      have finR: "\<And>x. finite {y. (y, x) \<in> ?R}"
   1.297 +        by simp (metis (mono_tags, lifting) fin \<open>X \<in> \<D>\<close> finite_subset mem_Collect_eq psubset_imp_subset subsetI)
   1.298 +      have "{X \<in> \<D>. x \<in> X} \<noteq> {}"
   1.299 +        using \<open>X \<in> \<D>\<close> \<open>x \<in> X\<close> by blast
   1.300 +      then obtain Y where "Y \<in> {X \<in> \<D>. x \<in> X}" "\<And>Y'. (Y', Y) \<in> ?R \<Longrightarrow> Y' \<notin> {X \<in> \<D>. x \<in> X}"
   1.301 +        by (rule wfE_min' [OF wf_finite_segments [OF irrR traR finR]]) blast
   1.302 +      then show "\<exists>Y. Y \<in> \<D> \<and> (\<forall>K'. K' \<in> \<D> \<and> Y \<noteq> K' \<longrightarrow> \<not> Y \<subseteq> K') \<and> x \<in> Y"
   1.303 +        by blast
   1.304 +    qed
   1.305 +    show "\<And>K. K \<in> ?\<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
   1.306 +      by (blast intro: dest: int)
   1.307 +    show "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) ?\<D>"
   1.308 +      using intdj by (simp add: pairwise_def) metis
   1.309 +    show "\<And>K. K \<in> ?\<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
   1.310 +      using SK by force
   1.311 +    show "\<And>u v. cbox u v \<in> ?\<D> \<Longrightarrow> \<exists>n. \<forall>i\<in>Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
   1.312 +      using cbox by force
   1.313 +    qed
   1.314 +qed
   1.315 +
   1.316  subsubsection \<open>Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\<close>
   1.317  
   1.318  lemma integral_component_eq_cart[simp]: