author  Manuel Eberl <eberlm@in.tum.de> 
Thu, 25 Aug 2016 15:50:43 +0200  
changeset 63721  492bb53c3420 
parent 63680  6e1e8b5abbfa 
child 63886  685fb01256af 
permissions  rwrr 
53399  1 
(* Author: John Harrison 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

2 
Author: Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP 
53399  3 
*) 
4 

63594
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63593
diff
changeset

5 
section \<open>HenstockKurzweil gauge integration in many dimensions.\<close> 
bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63593
diff
changeset

6 

bd218a9320b5
HOLMultivariate_Analysis: rename theories for more descriptive names
hoelzl
parents:
63593
diff
changeset

7 
theory Henstock_Kurzweil_Integration 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40513
diff
changeset

8 
imports 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40513
diff
changeset

9 
Derivative 
61243  10 
Uniform_Limit 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40513
diff
changeset

11 
"~~/src/HOL/Library/Indicator_Function" 
35172  12 
begin 
13 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

14 
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

15 
scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44176
diff
changeset

16 
scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36899
diff
changeset

17 

49675  18 

60420  19 
subsection \<open>Sundries\<close> 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

20 

35172  21 
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto 
22 
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto 

23 
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto 

24 

53399  25 
declare norm_triangle_ineq4[intro] 
26 

27 
lemma simple_image: "{f x x . x \<in> s} = f ` s" 

28 
by blast 

36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

29 

49970  30 
lemma linear_simps: 
31 
assumes "bounded_linear f" 

32 
shows 

33 
"f (a + b) = f a + f b" 

34 
"f (a  b) = f a  f b" 

35 
"f 0 = 0" 

36 
"f ( a) =  f a" 

37 
"f (s *\<^sub>R v) = s *\<^sub>R (f v)" 

53600
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53597
diff
changeset

38 
proof  
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53597
diff
changeset

39 
interpret f: bounded_linear f by fact 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53597
diff
changeset

40 
show "f (a + b) = f a + f b" by (rule f.add) 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53597
diff
changeset

41 
show "f (a  b) = f a  f b" by (rule f.diff) 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53597
diff
changeset

42 
show "f 0 = 0" by (rule f.zero) 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53597
diff
changeset

43 
show "f ( a) =  f a" by (rule f.minus) 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53597
diff
changeset

44 
show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR) 
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53597
diff
changeset

45 
qed 
49675  46 

47 
lemma bounded_linearI: 

48 
assumes "\<And>x y. f (x + y) = f x + f y" 

53399  49 
and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x" 
50 
and "\<And>x. norm (f x) \<le> norm x * K" 

36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

51 
shows "bounded_linear f" 
53600
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53597
diff
changeset

52 
using assms by (rule bounded_linear_intro) (* FIXME: duplicate *) 
51348  53 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

54 
lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

55 
by (rule bounded_linear_inner_left) 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

56 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

57 
lemma transitive_stepwise_lt_eq: 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

58 
assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)" 
53399  59 
shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))" 
60 
(is "?l = ?r") 

53408  61 
proof safe 
49675  62 
assume ?r 
63 
fix n m :: nat 

64 
assume "m < n" 

65 
then show "R m n" 

66 
proof (induct n arbitrary: m) 

53399  67 
case 0 
68 
then show ?case by auto 

69 
next 

49675  70 
case (Suc n) 
53399  71 
show ?case 
49675  72 
proof (cases "m < n") 
73 
case True 

74 
show ?thesis 

75 
apply (rule assms[OF Suc(1)[OF True]]) 

60420  76 
using \<open>?r\<close> 
50945  77 
apply auto 
49675  78 
done 
79 
next 

80 
case False 

53408  81 
then have "m = n" 
82 
using Suc(2) by auto 

83 
then show ?thesis 

60420  84 
using \<open>?r\<close> by auto 
49675  85 
qed 
53399  86 
qed 
49675  87 
qed auto 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

88 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

89 
lemma transitive_stepwise_gt: 
53408  90 
assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n)" 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

91 
shows "\<forall>n>m. R m n" 
49675  92 
proof  
93 
have "\<forall>m. \<forall>n>m. R m n" 

94 
apply (subst transitive_stepwise_lt_eq) 

60384  95 
apply (blast intro: assms)+ 
49675  96 
done 
49970  97 
then show ?thesis by auto 
49675  98 
qed 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

99 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

100 
lemma transitive_stepwise_le_eq: 
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

101 
assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" 
53399  102 
shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))" 
103 
(is "?l = ?r") 

49675  104 
proof safe 
105 
assume ?r 

106 
fix m n :: nat 

107 
assume "m \<le> n" 

53408  108 
then show "R m n" 
49675  109 
proof (induct n arbitrary: m) 
49970  110 
case 0 
111 
with assms show ?case by auto 

112 
next 

49675  113 
case (Suc n) 
114 
show ?case 

115 
proof (cases "m \<le> n") 

116 
case True 

60420  117 
with Suc.hyps \<open>\<forall>n. R n (Suc n)\<close> assms show ?thesis 
60384  118 
by blast 
49675  119 
next 
120 
case False 

53408  121 
then have "m = Suc n" 
122 
using Suc(2) by auto 

123 
then show ?thesis 

124 
using assms(1) by auto 

49675  125 
qed 
49970  126 
qed 
49675  127 
qed auto 
36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

128 

027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

129 
lemma transitive_stepwise_le: 
53408  130 
assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" 
131 
and "\<And>n. R n (Suc n)" 

36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

132 
shows "\<forall>n\<ge>m. R m n" 
49675  133 
proof  
134 
have "\<forall>m. \<forall>n\<ge>m. R m n" 

135 
apply (subst transitive_stepwise_le_eq) 

60384  136 
apply (blast intro: assms)+ 
49675  137 
done 
49970  138 
then show ?thesis by auto 
49675  139 
qed 
140 

36243
027ae62681be
Translated remaining theorems about integration from HOL light.
himmelma
parents:
36081
diff
changeset

141 

60420  142 
subsection \<open>Some useful lemmas about intervals.\<close> 
35172  143 

56188  144 
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)" 
145 
using nonempty_Basis 

146 
by (fastforce simp add: set_eq_iff mem_box) 

35172  147 

53399  148 
lemma interior_subset_union_intervals: 
56188  149 
assumes "i = cbox a b" 
150 
and "j = cbox c d" 

53399  151 
and "interior j \<noteq> {}" 
152 
and "i \<subseteq> j \<union> s" 

153 
and "interior i \<inter> interior j = {}" 

49675  154 
shows "interior i \<subseteq> interior s" 
155 
proof  

56188  156 
have "box a b \<inter> cbox c d = {}" 
157 
using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5) 

158 
unfolding assms(1,2) interior_cbox by auto 

49675  159 
moreover 
56188  160 
have "box a b \<subseteq> cbox c d \<union> s" 
161 
apply (rule order_trans,rule box_subset_cbox) 

49970  162 
using assms(4) unfolding assms(1,2) 
163 
apply auto 

164 
done 

49675  165 
ultimately 
166 
show ?thesis 

60384  167 
unfolding assms interior_cbox 
168 
by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI) 

49675  169 
qed 
170 

63595
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

171 
lemma interior_Union_subset_cbox: 
53399  172 
assumes "finite f" 
63595
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

173 
assumes f: "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a b" "\<And>s. s \<in> f \<Longrightarrow> interior s \<subseteq> t" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

174 
and t: "closed t" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

175 
shows "interior (\<Union>f) \<subseteq> t" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

176 
proof  
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

177 
have [simp]: "s \<in> f \<Longrightarrow> closed s" for s 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

178 
using f by auto 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

179 
define E where "E = {s\<in>f. interior s = {}}" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

180 
then have "finite E" "E \<subseteq> {s\<in>f. interior s = {}}" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

181 
using \<open>finite f\<close> by auto 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

182 
then have "interior (\<Union>f) = interior (\<Union>(f  E))" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

183 
proof (induction E rule: finite_subset_induct') 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

184 
case (insert s f') 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

185 
have "interior (\<Union>(f  insert s f') \<union> s) = interior (\<Union>(f  insert s f'))" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

186 
using insert.hyps \<open>finite f\<close> by (intro interior_closed_Un_empty_interior) auto 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

187 
also have "\<Union>(f  insert s f') \<union> s = \<Union>(f  f')" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

188 
using insert.hyps by auto 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

189 
finally show ?case 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

190 
by (simp add: insert.IH) 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

191 
qed simp 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

192 
also have "\<dots> \<subseteq> \<Union>(f  E)" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

193 
by (rule interior_subset) 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

194 
also have "\<dots> \<subseteq> t" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

195 
proof (rule Union_least) 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

196 
fix s assume "s \<in> f  E" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

197 
with f[of s] obtain a b where s: "s \<in> f" "s = cbox a b" "box a b \<noteq> {}" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

198 
by (fastforce simp: E_def) 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

199 
have "closure (interior s) \<subseteq> closure t" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

200 
by (intro closure_mono f \<open>s \<in> f\<close>) 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

201 
with s \<open>closed t\<close> show "s \<subseteq> t" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

202 
by (simp add: closure_box) 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

203 
qed 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

204 
finally show ?thesis . 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

205 
qed 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

206 

aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

207 
lemma inter_interior_unions_intervals: 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

208 
"finite f \<Longrightarrow> open s \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = cbox a b \<Longrightarrow> \<forall>t\<in>f. s \<inter> (interior t) = {} \<Longrightarrow> s \<inter> interior (\<Union>f) = {}" 
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

209 
using interior_Union_subset_cbox[of f "UNIV  s"] by auto 
60420  210 

211 
subsection \<open>Bounds on intervals where they exist.\<close> 

56188  212 

213 
definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a" 

214 
where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)" 

215 

216 
definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a" 

217 
where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)" 

218 

219 
lemma interval_upperbound[simp]: 

220 
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> 

221 
interval_upperbound (cbox a b) = (b::'a::euclidean_space)" 

62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62207
diff
changeset

222 
unfolding interval_upperbound_def euclidean_representation_setsum cbox_def 
56188  223 
by (safe intro!: cSup_eq) auto 
224 

225 
lemma interval_lowerbound[simp]: 

226 
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> 

227 
interval_lowerbound (cbox a b) = (a::'a::euclidean_space)" 

62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62207
diff
changeset

228 
unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def 
56188  229 
by (safe intro!: cInf_eq) auto 
230 

231 
lemmas interval_bounds = interval_upperbound interval_lowerbound 

232 

233 
lemma 

234 
fixes X::"real set" 

235 
shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X" 

236 
and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X" 

62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62207
diff
changeset

237 
by (auto simp: interval_upperbound_def interval_lowerbound_def) 
56188  238 

239 
lemma interval_bounds'[simp]: 

240 
assumes "cbox a b \<noteq> {}" 

241 
shows "interval_upperbound (cbox a b) = b" 

242 
and "interval_lowerbound (cbox a b) = a" 

243 
using assms unfolding box_ne_empty by auto 

53399  244 

59425  245 

60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

246 
lemma interval_upperbound_Times: 
59425  247 
assumes "A \<noteq> {}" and "B \<noteq> {}" 
248 
shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)" 

249 
proof 

250 
from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp 

251 
have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:A. x \<bullet> i) *\<^sub>R i)" 

252 
by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0) 

253 
moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp 

254 
have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:B. x \<bullet> i) *\<^sub>R i)" 

255 
by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0) 

256 
ultimately show ?thesis unfolding interval_upperbound_def 

257 
by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod) 

258 
qed 

259 

60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

260 
lemma interval_lowerbound_Times: 
59425  261 
assumes "A \<noteq> {}" and "B \<noteq> {}" 
262 
shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)" 

263 
proof 

264 
from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp 

265 
have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:A. x \<bullet> i) *\<^sub>R i)" 

266 
by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0) 

267 
moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp 

268 
have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:B. x \<bullet> i) *\<^sub>R i)" 

269 
by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0) 

270 
ultimately show ?thesis unfolding interval_lowerbound_def 

271 
by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod) 

272 
qed 

273 

60420  274 
subsection \<open>Content (length, area, volume...) of an interval.\<close> 
35172  275 

56188  276 
definition "content (s::('a::euclidean_space) set) = 
277 
(if s = {} then 0 else (\<Prod>i\<in>Basis. (interval_upperbound s)\<bullet>i  (interval_lowerbound s)\<bullet>i))" 

278 

279 
lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}" 

280 
unfolding box_eq_empty unfolding not_ex not_less by auto 

281 

282 
lemma content_cbox: 

283 
fixes a :: "'a::euclidean_space" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

284 
assumes "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i" 
56188  285 
shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i  a\<bullet>i)" 
49970  286 
using interval_not_empty[OF assms] 
54777  287 
unfolding content_def 
60384  288 
by auto 
56188  289 

290 
lemma content_cbox': 

291 
fixes a :: "'a::euclidean_space" 

292 
assumes "cbox a b \<noteq> {}" 

293 
shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i  a\<bullet>i)" 

60384  294 
using assms box_ne_empty(1) content_cbox by blast 
49970  295 

53408  296 
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b  a" 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62207
diff
changeset

297 
by (auto simp: interval_upperbound_def interval_lowerbound_def content_def) 
56188  298 

61945  299 
lemma abs_eq_content: "\<bar>y  x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})" 
61204  300 
by (auto simp: content_real) 
301 

50104  302 
lemma content_singleton[simp]: "content {a} = 0" 
303 
proof  

56188  304 
have "content (cbox a a) = 0" 
305 
by (subst content_cbox) (auto simp: ex_in_conv) 

306 
then show ?thesis by (simp add: cbox_sing) 

307 
qed 

308 

60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

309 
lemma content_unit[iff]: "content(cbox 0 (One::'a::euclidean_space)) = 1" 
56188  310 
proof  
311 
have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i" 

312 
by auto 

313 
have "0 \<in> cbox 0 (One::'a)" 

314 
unfolding mem_box by auto 

315 
then show ?thesis 

57418  316 
unfolding content_def interval_bounds[OF *] using setprod.neutral_const by auto 
56188  317 
qed 
49970  318 

319 
lemma content_pos_le[intro]: 

56188  320 
fixes a::"'a::euclidean_space" 
321 
shows "0 \<le> content (cbox a b)" 

322 
proof (cases "cbox a b = {}") 

323 
case False 

324 
then have *: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i" 

325 
unfolding box_ne_empty . 

326 
have "0 \<le> (\<Prod>i\<in>Basis. interval_upperbound (cbox a b) \<bullet> i  interval_lowerbound (cbox a b) \<bullet> i)" 

327 
apply (rule setprod_nonneg) 

328 
unfolding interval_bounds[OF *] 

329 
using * 

330 
apply auto 

331 
done 

332 
also have "\<dots> = content (cbox a b)" using False by (simp add: content_def) 

333 
finally show ?thesis . 

334 
qed (simp add: content_def) 

49970  335 

60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

336 
corollary content_nonneg [simp]: 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

337 
fixes a::"'a::euclidean_space" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

338 
shows "~ content (cbox a b) < 0" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

339 
using not_le by blast 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

340 

49970  341 
lemma content_pos_lt: 
56188  342 
fixes a :: "'a::euclidean_space" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

343 
assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" 
56188  344 
shows "0 < content (cbox a b)" 
54777  345 
using assms 
56188  346 
by (auto simp: content_def box_eq_empty intro!: setprod_pos) 
49970  347 

53408  348 
lemma content_eq_0: 
56188  349 
"content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)" 
350 
by (auto simp: content_def box_eq_empty intro!: setprod_pos bexI) 

35172  351 

53408  352 
lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)" 
53399  353 
by auto 
35172  354 

56188  355 
lemma content_cbox_cases: 
356 
"content (cbox a (b::'a::euclidean_space)) = 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

357 
(if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i  a\<bullet>i) Basis else 0)" 
56188  358 
by (auto simp: not_le content_eq_0 intro: less_imp_le content_cbox) 
359 

360 
lemma content_eq_0_interior: "content (cbox a b) = 0 \<longleftrightarrow> interior(cbox a b) = {}" 

361 
unfolding content_eq_0 interior_cbox box_eq_empty 

53408  362 
by auto 
35172  363 

53399  364 
lemma content_pos_lt_eq: 
56188  365 
"0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)" 
60394  366 
proof (rule iffI) 
56188  367 
assume "0 < content (cbox a b)" 
368 
then have "content (cbox a b) \<noteq> 0" by auto 

53399  369 
then show "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" 
49970  370 
unfolding content_eq_0 not_ex not_le by fastforce 
60394  371 
next 
372 
assume "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i" 

373 
then show "0 < content (cbox a b)" 

374 
by (metis content_pos_lt) 

49970  375 
qed 
376 

53399  377 
lemma content_empty [simp]: "content {} = 0" 
378 
unfolding content_def by auto 

35172  379 

60762  380 
lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b  a else 0)" 
381 
by (simp add: content_real) 

382 

49698  383 
lemma content_subset: 
56188  384 
assumes "cbox a b \<subseteq> cbox c d" 
385 
shows "content (cbox a b) \<le> content (cbox c d)" 

386 
proof (cases "cbox a b = {}") 

387 
case True 

388 
then show ?thesis 

389 
using content_pos_le[of c d] by auto 

390 
next 

391 
case False 

392 
then have ab_ne: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i" 

393 
unfolding box_ne_empty by auto 

394 
then have ab_ab: "a\<in>cbox a b" "b\<in>cbox a b" 

395 
unfolding mem_box by auto 

396 
have "cbox c d \<noteq> {}" using assms False by auto 

397 
then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i" 

398 
using assms unfolding box_ne_empty by auto 

60394  399 
have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i  a \<bullet> i" 
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61736
diff
changeset

400 
using ab_ne by auto 
60394  401 
moreover 
402 
have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i  a \<bullet> i \<le> d \<bullet> i  c \<bullet> i" 

403 
using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)] 

404 
assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(1)] 

405 
by (metis diff_mono) 

406 
ultimately show ?thesis 

407 
unfolding content_def interval_bounds[OF ab_ne] interval_bounds[OF cd_ne] 

60420  408 
by (simp add: setprod_mono if_not_P[OF False] if_not_P[OF \<open>cbox c d \<noteq> {}\<close>]) 
56188  409 
qed 
410 

411 
lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

412 
unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce 
35172  413 

59425  414 
lemma content_times[simp]: "content (A \<times> B) = content A * content B" 
415 
proof (cases "A \<times> B = {}") 

416 
let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound" 

417 
let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound" 

418 
assume nonempty: "A \<times> B \<noteq> {}" 

60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

419 
hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i  (?lb1 A, ?lb2 B) \<bullet> i)" 
59425  420 
unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times) 
421 
also have "... = content A * content B" unfolding content_def using nonempty 

422 
apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp) 

423 
apply (subst (1 2) setprod.reindex, auto intro: inj_onI) 

424 
done 

425 
finally show ?thesis . 

426 
qed (auto simp: content_def) 

427 

60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

428 
lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

429 
by (simp add: cbox_Pair_eq) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

430 

e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

431 
lemma content_cbox_pair_eq0_D: 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

432 
"content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

433 
by (simp add: content_Pair) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

434 

e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

435 
lemma content_eq_0_gen: 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

436 
fixes s :: "'a::euclidean_space set" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

437 
assumes "bounded s" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

438 
shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)" (is "_ = ?rhs") 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

439 
proof safe 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

440 
assume "content s = 0" then show ?rhs 
62390  441 
apply (clarsimp simp: ex_in_conv content_def split: if_split_asm) 
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

442 
apply (rule_tac x=a in bexI) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

443 
apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

444 
apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

445 
apply (drule cSUP_eq_cINF_D) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

446 
apply (auto simp: bounded_inner_imp_bdd_above [OF assms] bounded_inner_imp_bdd_below [OF assms]) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

447 
done 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

448 
next 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

449 
fix i a 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

450 
assume "i \<in> Basis" "\<forall>x\<in>s. x \<bullet> i = a" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

451 
then show "content s = 0" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

452 
apply (clarsimp simp: content_def) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

453 
apply (rule_tac x=i in bexI) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

454 
apply (auto simp: interval_upperbound_def interval_lowerbound_def) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

455 
done 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

456 
qed 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

457 

e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

458 
lemma content_0_subset_gen: 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

459 
fixes a :: "'a::euclidean_space" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

460 
assumes "content t = 0" "s \<subseteq> t" "bounded t" shows "content s = 0" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

461 
proof  
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

462 
have "bounded s" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

463 
using assms by (metis bounded_subset) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

464 
then show ?thesis 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

465 
using assms 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

466 
by (auto simp: content_eq_0_gen) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

467 
qed 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

468 

e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

469 
lemma content_0_subset: "\<lbrakk>content(cbox a b) = 0; s \<subseteq> cbox a b\<rbrakk> \<Longrightarrow> content s = 0" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

470 
by (simp add: content_0_subset_gen bounded_cbox) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

471 

49698  472 

63593
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

473 
lemma interval_split: 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

474 
fixes a :: "'a::euclidean_space" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

475 
assumes "k \<in> Basis" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

476 
shows 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

477 
"cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

478 
"cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

479 
apply (rule_tac[!] set_eqI) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

480 
unfolding Int_iff mem_box mem_Collect_eq 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

481 
using assms 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

482 
apply auto 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

483 
done 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

484 

bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

485 
lemma content_split: 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

486 
fixes a :: "'a::euclidean_space" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

487 
assumes "k \<in> Basis" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

488 
shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

489 
proof cases 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

490 
note simps = interval_split[OF assms] content_cbox_cases 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

491 
have *: "Basis = insert k (Basis  {k})" "\<And>x. finite (Basis{x})" "\<And>x. x\<notin>Basis{x}" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

492 
using assms by auto 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

493 
have *: "\<And>X Y Z. (\<Prod>i\<in>Basis. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>Basis{k}. Z i (Y i))" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

494 
"(\<Prod>i\<in>Basis. b\<bullet>i  a\<bullet>i) = (\<Prod>i\<in>Basis{k}. b\<bullet>i  a\<bullet>i) * (b\<bullet>k  a\<bullet>k)" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

495 
apply (subst *(1)) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

496 
defer 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

497 
apply (subst *(1)) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

498 
unfolding setprod.insert[OF *(2)] 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

499 
apply auto 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

500 
done 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

501 
assume as: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

502 
moreover 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

503 
have "\<And>x. min (b \<bullet> k) c = max (a \<bullet> k) c \<Longrightarrow> 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

504 
x * (b\<bullet>k  a\<bullet>k) = x * (max (a \<bullet> k) c  a \<bullet> k) + x * (b \<bullet> k  max (a \<bullet> k) c)" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

505 
by (auto simp add: field_simps) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

506 
moreover 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

507 
have **: "(\<Prod>i\<in>Basis. ((\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i  a \<bullet> i)) = 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

508 
(\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i)  a \<bullet> i)" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

509 
"(\<Prod>i\<in>Basis. b \<bullet> i  ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) = 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

510 
(\<Prod>i\<in>Basis. b \<bullet> i  (if i = k then max (a \<bullet> k) c else a \<bullet> i))" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

511 
by (auto intro!: setprod.cong) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

512 
have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

513 
unfolding not_le 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

514 
using as[unfolded ,rule_format,of k] assms 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

515 
by auto 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

516 
ultimately show ?thesis 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

517 
using assms 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

518 
unfolding simps ** 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

519 
unfolding *(1)[of "\<lambda>i x. b\<bullet>i  x"] *(1)[of "\<lambda>i x. x  a\<bullet>i"] 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

520 
unfolding *(2) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

521 
by auto 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

522 
next 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

523 
assume "\<not> (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

524 
then have "cbox a b = {}" 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

525 
unfolding box_eq_empty by (auto simp: not_le) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

526 
then show ?thesis 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

527 
by (auto simp: not_le) 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

528 
qed 
bbcb05504fdc
HOLMultivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
hoelzl
parents:
63540
diff
changeset

529 

60420  530 
subsection \<open>The notion of a gauge  simply an open set containing the point.\<close> 
35172  531 

53408  532 
definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))" 
53399  533 

534 
lemma gaugeI: 

535 
assumes "\<And>x. x \<in> g x" 

536 
and "\<And>x. open (g x)" 

537 
shows "gauge g" 

35172  538 
using assms unfolding gauge_def by auto 
539 

53399  540 
lemma gaugeD[dest]: 
541 
assumes "gauge d" 

542 
shows "x \<in> d x" 

543 
and "open (d x)" 

49698  544 
using assms unfolding gauge_def by auto 
35172  545 

546 
lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))" 

53399  547 
unfolding gauge_def by auto 
548 

549 
lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)" 

550 
unfolding gauge_def by auto 

35172  551 

60466  552 
lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)" 
49698  553 
by (rule gauge_ball) auto 
35172  554 

53408  555 
lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)" 
53399  556 
unfolding gauge_def by auto 
35172  557 

49698  558 
lemma gauge_inters: 
53399  559 
assumes "finite s" 
560 
and "\<forall>d\<in>s. gauge (f d)" 

60585  561 
shows "gauge (\<lambda>x. \<Inter>{f d x  d. d \<in> s})" 
49698  562 
proof  
53399  563 
have *: "\<And>x. {f d x d. d \<in> s} = (\<lambda>d. f d x) ` s" 
564 
by auto 

49698  565 
show ?thesis 
53399  566 
unfolding gauge_def unfolding * 
49698  567 
using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto 
568 
qed 

569 

53399  570 
lemma gauge_existence_lemma: 
53408  571 
"(\<forall>x. \<exists>d :: real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)" 
53399  572 
by (metis zero_less_one) 
49698  573 

35172  574 

60420  575 
subsection \<open>Divisions.\<close> 
35172  576 

53408  577 
definition division_of (infixl "division'_of" 40) 
578 
where 

53399  579 
"s division_of i \<longleftrightarrow> 
580 
finite s \<and> 

56188  581 
(\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = cbox a b)) \<and> 
53399  582 
(\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and> 
583 
(\<Union>s = i)" 

35172  584 

49698  585 
lemma division_ofD[dest]: 
586 
assumes "s division_of i" 

53408  587 
shows "finite s" 
588 
and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i" 

589 
and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}" 

56188  590 
and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b" 
53408  591 
and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" 
592 
and "\<Union>s = i" 

49698  593 
using assms unfolding division_of_def by auto 
35172  594 

595 
lemma division_ofI: 

53408  596 
assumes "finite s" 
597 
and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i" 

598 
and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}" 

56188  599 
and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b" 
53408  600 
and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}" 
53399  601 
and "\<Union>s = i" 
602 
shows "s division_of i" 

603 
using assms unfolding division_of_def by auto 

35172  604 

605 
lemma division_of_finite: "s division_of i \<Longrightarrow> finite s" 

606 
unfolding division_of_def by auto 

607 

56188  608 
lemma division_of_self[intro]: "cbox a b \<noteq> {} \<Longrightarrow> {cbox a b} division_of (cbox a b)" 
35172  609 
unfolding division_of_def by auto 
610 

53399  611 
lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}" 
612 
unfolding division_of_def by auto 

35172  613 

49698  614 
lemma division_of_sing[simp]: 
56188  615 
"s division_of cbox a (a::'a::euclidean_space) \<longleftrightarrow> s = {cbox a a}" 
53399  616 
(is "?l = ?r") 
49698  617 
proof 
618 
assume ?r 

53399  619 
moreover 
60384  620 
{ fix k 
621 
assume "s = {{a}}" "k\<in>s" 

622 
then have "\<exists>x y. k = cbox x y" 

50945  623 
apply (rule_tac x=a in exI)+ 
60384  624 
apply (force simp: cbox_sing) 
50945  625 
done 
49698  626 
} 
53399  627 
ultimately show ?l 
56188  628 
unfolding division_of_def cbox_sing by auto 
49698  629 
next 
630 
assume ?l 

56188  631 
note * = conjunctD4[OF this[unfolded division_of_def cbox_sing]] 
53399  632 
{ 
633 
fix x 

634 
assume x: "x \<in> s" have "x = {a}" 

53408  635 
using *(2)[rule_format,OF x] by auto 
53399  636 
} 
53408  637 
moreover have "s \<noteq> {}" 
638 
using *(4) by auto 

639 
ultimately show ?r 

56188  640 
unfolding cbox_sing by auto 
49698  641 
qed 
35172  642 

643 
lemma elementary_empty: obtains p where "p division_of {}" 

644 
unfolding division_of_trivial by auto 

645 

56188  646 
lemma elementary_interval: obtains p where "p division_of (cbox a b)" 
49698  647 
by (metis division_of_trivial division_of_self) 
35172  648 

649 
lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k" 

650 
unfolding division_of_def by auto 

651 

652 
lemma forall_in_division: 

56188  653 
"d division_of i \<Longrightarrow> (\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. cbox a b \<in> d \<longrightarrow> P (cbox a b))" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44522
diff
changeset

654 
unfolding division_of_def by fastforce 
35172  655 

53399  656 
lemma division_of_subset: 
657 
assumes "p division_of (\<Union>p)" 

658 
and "q \<subseteq> p" 

659 
shows "q division_of (\<Union>q)" 

53408  660 
proof (rule division_ofI) 
661 
note * = division_ofD[OF assms(1)] 

49698  662 
show "finite q" 
60384  663 
using "*"(1) assms(2) infinite_super by auto 
53399  664 
{ 
665 
fix k 

49698  666 
assume "k \<in> q" 
53408  667 
then have kp: "k \<in> p" 
668 
using assms(2) by auto 

669 
show "k \<subseteq> \<Union>q" 

60420  670 
using \<open>k \<in> q\<close> by auto 
56188  671 
show "\<exists>a b. k = cbox a b" 
53408  672 
using *(4)[OF kp] by auto 
673 
show "k \<noteq> {}" 

674 
using *(3)[OF kp] by auto 

53399  675 
} 
49698  676 
fix k1 k2 
677 
assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2" 

53408  678 
then have **: "k1 \<in> p" "k2 \<in> p" "k1 \<noteq> k2" 
53399  679 
using assms(2) by auto 
680 
show "interior k1 \<inter> interior k2 = {}" 

53408  681 
using *(5)[OF **] by auto 
49698  682 
qed auto 
683 

684 
lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)" 

685 
unfolding division_of_def by auto 

35172  686 

49970  687 
lemma division_of_content_0: 
56188  688 
assumes "content (cbox a b) = 0" "d division_of (cbox a b)" 
49970  689 
shows "\<forall>k\<in>d. content k = 0" 
690 
unfolding forall_in_division[OF assms(2)] 

60384  691 
by (metis antisym_conv assms content_pos_le content_subset division_ofD(2)) 
49970  692 

693 
lemma division_inter: 

56188  694 
fixes s1 s2 :: "'a::euclidean_space set" 
53408  695 
assumes "p1 division_of s1" 
696 
and "p2 division_of s2" 

63595
aca2659ebba7
clean up prove for inter_interior_unions_intervals
hoelzl
parents:
63594
diff
changeset

697 
shows "{k1 \<inter> k2  k1 k2. k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)" 
49970  698 
(is "?A' division_of _") 
699 
proof  

700 
let ?A = "{s. s \<in> (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}" 

53408  701 
have *: "?A' = ?A" by auto 
53399  702 
show ?thesis 
703 
unfolding * 

49970  704 
proof (rule division_ofI) 
53399  705 
have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)" 
706 
by auto 

707 
moreover have "finite (p1 \<times> p2)" 

708 
using assms unfolding division_of_def by auto 

49970  709 
ultimately show "finite ?A" by auto 
53399  710 
have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s" 
711 
by auto 

49970  712 
show "\<Union>?A = s1 \<inter> s2" 
713 
apply (rule set_eqI) 

62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62207
diff
changeset

714 
unfolding * and UN_iff 
49970  715 
using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] 
716 
apply auto 

717 
done 

53399  718 
{ 
719 
fix k 

720 
assume "k \<in> ?A" 

53408  721 
then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1 \<in> p1" "k2 \<in> p2" "k \<noteq> {}" 
53399  722 
by auto 
53408  723 
then show "k \<noteq> {}" 
724 
by auto 

49970  725 
show "k \<subseteq> s1 \<inter> s2" 
726 
using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)] 

727 
unfolding k by auto 

56188  728 
obtain a1 b1 where k1: "k1 = cbox a1 b1" 
53408  729 
using division_ofD(4)[OF assms(1) k(2)] by blast 
56188  730 
obtain a2 b2 where k2: "k2 = cbox a2 b2" 
53408  731 
using division_ofD(4)[OF assms(2) k(3)] by blast 
56188  732 
show "\<exists>a b. k = cbox a b" 
53408  733 
unfolding k k1 k2 unfolding inter_interval by auto 
734 
} 

49970  735 
fix k1 k2 
53408  736 
assume "k1 \<in> ?A" 
737 
then obtain x1 y1 where k1: "k1 = x1 \<inter> y1" "x1 \<in> p1" "y1 \<in> p2" "k1 \<noteq> {}" 

738 
by auto 

739 
assume "k2 \<in> ?A" 

740 
then obtain x2 y2 where k2: "k2 = x2 \<inter> y2" "x2 \<in> p1" "y2 \<in> p2" "k2 \<noteq> {}" 

741 
by auto 

49970  742 
assume "k1 \<noteq> k2" 
53399  743 
then have th: "x1 \<noteq> x2 \<or> y1 \<noteq> y2" 
744 
unfolding k1 k2 by auto 

53408  745 
have *: "interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {} \<Longrightarrow> 
746 
interior (x1 \<inter> y1) \<subseteq> interior x1 \<Longrightarrow> interior (x1 \<inter> y1) \<subseteq> interior y1 \<Longrightarrow> 

747 
interior (x2 \<inter> y2) \<subseteq> interior x2 \<Longrightarrow> interior (x2 \<inter> y2) \<subseteq> interior y2 \<Longrightarrow> 

748 
interior (x1 \<inter> y1) \<inter> interior (x2 \<inter> y2) = {}" by auto 

49970  749 
show "interior k1 \<inter> interior k2 = {}" 
750 
unfolding k1 k2 

751 
apply (rule *) 

60384  752 
using assms division_ofD(5) k1 k2(2) k2(3) th apply auto 
53399  753 
done 
49970  754 
qed 
755 
qed 

756 

757 
lemma division_inter_1: 

53408  758 
assumes "d division_of i" 
56188  759 
and "cbox a (b::'a::euclidean_space) \<subseteq> i" 
760 
shows "{cbox a b \<inter> k  k. k \<in> d \<and> cbox a b \<inter> k \<noteq> {}} division_of (cbox a b)" 

761 
proof (cases "cbox a b = {}") 

49970  762 
case True 
53399  763 
show ?thesis 
764 
unfolding True and division_of_trivial by auto 

49970  765 
next 
766 
case False 

56188  767 
have *: "cbox a b \<inter> i = cbox a b" using assms(2) by auto 
53399  768 
show ?thesis 
769 
using division_inter[OF division_of_self[OF False] assms(1)] 

770 
unfolding * by auto 

49970  771 
qed 
772 

773 
lemma elementary_inter: 

56188  774 
fixes s t :: "'a::euclidean_space set" 
53408  775 
assumes "p1 division_of s" 
776 
and "p2 division_of t" 

35172  777 
shows "\<exists>p. p division_of (s \<inter> t)" 
60384  778 
using assms division_inter by blast 
49970  779 

780 
lemma elementary_inters: 

53408  781 
assumes "finite f" 
782 
and "f \<noteq> {}" 

56188  783 
and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)" 
60585  784 
shows "\<exists>p. p division_of (\<Inter>f)" 
49970  785 
using assms 
786 
proof (induct f rule: finite_induct) 

787 
case (insert x f) 

788 
show ?case 

789 
proof (cases "f = {}") 

790 
case True 

53399  791 
then show ?thesis 
792 
unfolding True using insert by auto 

49970  793 
next 
794 
case False 

53408  795 
obtain p where "p division_of \<Inter>f" 
796 
using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] .. 

797 
moreover obtain px where "px division_of x" 

798 
using insert(5)[rule_format,OF insertI1] .. 

49970  799 
ultimately show ?thesis 
60384  800 
by (simp add: elementary_inter Inter_insert) 
49970  801 
qed 
802 
qed auto 

35172  803 

804 
lemma division_disjoint_union: 

53408  805 
assumes "p1 division_of s1" 
806 
and "p2 division_of s2" 

807 
and "interior s1 \<inter> interior s2 = {}" 

50945  808 
shows "(p1 \<union> p2) division_of (s1 \<union> s2)" 
809 
proof (rule division_ofI) 

53408  810 
note d1 = division_ofD[OF assms(1)] 
811 
note d2 = division_ofD[OF assms(2)] 

812 
show "finite (p1 \<union> p2)" 

813 
using d1(1) d2(1) by auto 

814 
show "\<Union>(p1 \<union> p2) = s1 \<union> s2" 

815 
using d1(6) d2(6) by auto 

50945  816 
{ 
817 
fix k1 k2 

818 
assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" 

819 
moreover 

820 
let ?g="interior k1 \<inter> interior k2 = {}" 

821 
{ 

822 
assume as: "k1\<in>p1" "k2\<in>p2" 

823 
have ?g 

824 
using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]] 

825 
using assms(3) by blast 

826 
} 

827 
moreover 

828 
{ 

829 
assume as: "k1\<in>p2" "k2\<in>p1" 

830 
have ?g 

831 
using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]] 

832 
using assms(3) by blast 

833 
} 

53399  834 
ultimately show ?g 
835 
using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto 

50945  836 
} 
837 
fix k 

838 
assume k: "k \<in> p1 \<union> p2" 

53408  839 
show "k \<subseteq> s1 \<union> s2" 
840 
using k d1(2) d2(2) by auto 

841 
show "k \<noteq> {}" 

842 
using k d1(3) d2(3) by auto 

56188  843 
show "\<exists>a b. k = cbox a b" 
53408  844 
using k d1(4) d2(4) by auto 
50945  845 
qed 
35172  846 

847 
lemma partial_division_extend_1: 

56188  848 
fixes a b c d :: "'a::euclidean_space" 
849 
assumes incl: "cbox c d \<subseteq> cbox a b" 

850 
and nonempty: "cbox c d \<noteq> {}" 

851 
obtains p where "p division_of (cbox a b)" "cbox c d \<in> p" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

852 
proof 
53408  853 
let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a. 
56188  854 
cbox (\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)" 
63040  855 
define p where "p = ?B ` (Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)})" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

856 

56188  857 
show "cbox c d \<in> p" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

858 
unfolding p_def 
56188  859 
by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"]) 
50945  860 
{ 
861 
fix i :: 'a 

862 
assume "i \<in> Basis" 

50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

863 
with incl nonempty have "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i" 
56188  864 
unfolding box_eq_empty subset_box by (auto simp: not_le) 
50945  865 
} 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

866 
note ord = this 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

867 

56188  868 
show "p division_of (cbox a b)" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

869 
proof (rule division_ofI) 
53399  870 
show "finite p" 
871 
unfolding p_def by (auto intro!: finite_PiE) 

50945  872 
{ 
873 
fix k 

874 
assume "k \<in> p" 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52141
diff
changeset

875 
then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

876 
by (auto simp: p_def) 
56188  877 
then show "\<exists>a b. k = cbox a b" 
53408  878 
by auto 
56188  879 
have "k \<subseteq> cbox a b \<and> k \<noteq> {}" 
880 
proof (simp add: k box_eq_empty subset_box not_less, safe) 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

881 
fix i :: 'a 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

882 
assume i: "i \<in> Basis" 
50945  883 
with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

884 
by (auto simp: PiE_iff) 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

885 
with i ord[of i] 
50945  886 
show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i" 
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset

887 
by auto 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

888 
qed 
56188  889 
then show "k \<noteq> {}" "k \<subseteq> cbox a b" 
53408  890 
by auto 
50945  891 
{ 
53408  892 
fix l 
893 
assume "l \<in> p" 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52141
diff
changeset

894 
then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g" 
50945  895 
by (auto simp: p_def) 
896 
assume "l \<noteq> k" 

897 
have "\<exists>i\<in>Basis. f i \<noteq> g i" 

898 
proof (rule ccontr) 

53408  899 
assume "\<not> ?thesis" 
50945  900 
with f g have "f = g" 
901 
by (auto simp: PiE_iff extensional_def intro!: ext) 

60420  902 
with \<open>l \<noteq> k\<close> show False 
50945  903 
by (simp add: l k) 
904 
qed 

53408  905 
then obtain i where *: "i \<in> Basis" "f i \<noteq> g i" .. 
906 
then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)" 

60384  907 
"g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)" 
50945  908 
using f g by (auto simp: PiE_iff) 
53408  909 
with * ord[of i] show "interior l \<inter> interior k = {}" 
56188  910 
by (auto simp add: l k interior_cbox disjoint_interval intro!: bexI[of _ i]) 
50945  911 
} 
60420  912 
note \<open>k \<subseteq> cbox a b\<close> 
50945  913 
} 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

914 
moreover 
50945  915 
{ 
56188  916 
fix x assume x: "x \<in> cbox a b" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

917 
have "\<forall>i\<in>Basis. \<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

918 
proof 
53408  919 
fix i :: 'a 
920 
assume "i \<in> Basis" 

53399  921 
with x ord[of i] 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

922 
have "(a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> c \<bullet> i) \<or> (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i) \<or> 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

923 
(d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)" 
56188  924 
by (auto simp: cbox_def) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

925 
then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

926 
by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

927 
qed 
53408  928 
then obtain f where 
929 
f: "\<forall>i\<in>Basis. x \<bullet> i \<in> {fst (f i) \<bullet> i..snd (f i) \<bullet> i} \<and> f i \<in> {(a, c), (c, d), (d, b)}" 

930 
unfolding bchoice_iff .. 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset

931 
moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

932 
by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

933 
moreover from f have "x \<in> ?B (restrict f Basis)" 
56188  934 
by (auto simp: mem_box) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

935 
ultimately have "\<exists>k\<in>p. x \<in> k" 
53408  936 
unfolding p_def by blast 
937 
} 

56188  938 
ultimately show "\<Union>p = cbox a b" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

939 
by auto 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

940 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50348
diff
changeset

941 
qed 
35172  942 

50945  943 
lemma partial_division_extend_interval: 
56188  944 
assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> cbox a b" 
945 
obtains q where "p \<subseteq> q" "q division_of cbox a (b::'a::euclidean_space)" 

50945  946 
proof (cases "p = {}") 
947 
case True 

56188  948 
obtain q where "q division_of (cbox a b)" 
53408  949 
by (rule elementary_interval) 
53399  950 
then show ?thesis 
60384  951 
using True that by blast 
50945  952 
next 
953 
case False 

954 
note p = division_ofD[OF assms(1)] 

60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

955 
have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q" 
50945  956 
proof 
61165  957 
fix k 
958 
assume kp: "k \<in> p" 

56188  959 
obtain c d where k: "k = cbox c d" 
61165  960 
using p(4)[OF kp] by blast 
56188  961 
have *: "cbox c d \<subseteq> cbox a b" "cbox c d \<noteq> {}" 
61165  962 
using p(2,3)[OF kp, unfolded k] using assms(2) 
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset

963 
by (blast intro: order.trans)+ 
56188  964 
obtain q where "q division_of cbox a b" "cbox c d \<in> q" 
53408  965 
by (rule partial_division_extend_1[OF *]) 
61165  966 
then show "\<exists>q. q division_of cbox a b \<and> k \<in> q" 
53408  967 
unfolding k by auto 
50945  968 
qed 
56188  969 
obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x" 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

970 
using bchoice[OF div_cbox] by blast 
60394  971 
{ fix x 
53408  972 
assume x: "x \<in> p" 
60394  973 
have "q x division_of \<Union>q x" 
50945  974 
apply (rule division_ofI) 
975 
using division_ofD[OF q(1)[OF x]] 

976 
apply auto 

60394  977 
done } 
978 
then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x  {x})" 

979 
by (meson Diff_subset division_of_subset) 

60585  980 
then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i  {i})) ` p)" 
50945  981 
apply  
60394  982 
apply (rule elementary_inters [OF finite_imageI[OF p(1)]]) 
983 
apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]]) 

50945  984 
done 
53408  985 
then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i  {i})) ` p)" .. 
60394  986 
have "d \<union> p division_of cbox a b" 
50945  987 
proof  
60394  988 
have te: "\<And>s f t. s \<noteq> {} \<Longrightarrow> \<forall>i\<in>s. f i \<union> i = t \<Longrightarrow> t = \<Inter>(f ` s) \<union> \<Union>s" by auto 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

989 
have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i  {i})) ` p) \<union> \<Union>p" 
60394  990 
proof (rule te[OF False], clarify) 
50945  991 
fix i 
53408  992 
assume i: "i \<in> p" 
56188  993 
show "\<Union>(q i  {i}) \<union> i = cbox a b" 
50945  994 
using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto 
995 
qed 

60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

996 
{ fix k 
53408  997 
assume k: "k \<in> p" 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

998 
have *: "\<And>u t s. t \<inter> s = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<inter> t = {}" 
53408  999 
by auto 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1000 
have "interior (\<Inter>i\<in>p. \<Union>(q i  {i})) \<inter> interior k = {}" 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1001 
proof (rule *[OF inter_interior_unions_intervals]) 
50945  1002 
note qk=division_ofD[OF q(1)[OF k]] 
56188  1003 
show "finite (q k  {k})" "open (interior k)" "\<forall>t\<in>q k  {k}. \<exists>a b. t = cbox a b" 
53408  1004 
using qk by auto 
50945  1005 
show "\<forall>t\<in>q k  {k}. interior k \<inter> interior t = {}" 
1006 
using qk(5) using q(2)[OF k] by auto 

60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1007 
show "interior (\<Inter>i\<in>p. \<Union>(q i  {i})) \<subseteq> interior (\<Union>(q k  {k}))" 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1008 
apply (rule interior_mono)+ 
53408  1009 
using k 
1010 
apply auto 

1011 
done 

60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1012 
qed } note [simp] = this 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1013 
show "d \<union> p division_of (cbox a b)" 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1014 
unfolding cbox_eq 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1015 
apply (rule division_disjoint_union[OF d assms(1)]) 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1016 
apply (rule inter_interior_unions_intervals) 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1017 
apply (rule p open_interior ballI)+ 
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

1018 
apply simp_all 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1019 
done 
60394  1020 
qed 
1021 
then show ?thesis 

1022 
by (meson Un_upper2 that) 

50945  1023 
qed 
35172  1024 

53399  1025 
lemma elementary_bounded[dest]: 
56188  1026 
fixes s :: "'a::euclidean_space set" 
53408  1027 
shows "p division_of s \<Longrightarrow> bounded s" 
56189
c4daa97ac57a
removed dependencies on theory Ordered_Euclidean_Space
immler
parents:
56188
diff
changeset

1028 
unfolding division_of_def by (metis bounded_Union bounded_cbox) 
53399  1029 

56188  1030 
lemma elementary_subset_cbox: 
1031 
"p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a (b::'a::euclidean_space)" 

1032 
by (meson elementary_bounded bounded_subset_cbox) 

50945  1033 

1034 
lemma division_union_intervals_exists: 

56188  1035 
fixes a b :: "'a::euclidean_space" 
1036 
assumes "cbox a b \<noteq> {}" 

1037 
obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)" 

1038 
proof (cases "cbox c d = {}") 

50945  1039 
case True 
1040 
show ?thesis 

1041 
apply (rule that[of "{}"]) 

1042 
unfolding True 

1043 
using assms 

1044 
apply auto 

1045 
done 

1046 
next 

1047 
case False 

1048 
show ?thesis 

56188  1049 
proof (cases "cbox a b \<inter> cbox c d = {}") 
50945  1050 
case True 
62618
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

1051 
then show ?thesis 
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

1052 
by (metis that False assms division_disjoint_union division_of_self insert_is_Un interior_Int interior_empty) 
50945  1053 
next 
1054 
case False 

56188  1055 
obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v" 
50945  1056 
unfolding inter_interval by auto 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1057 
have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto 
56188  1058 
obtain p where "p division_of cbox c d" "cbox u v \<in> p" 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1059 
by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]]) 
53408  1060 
note p = this division_ofD[OF this(1)] 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1061 
have "interior (cbox a b \<inter> \<Union>(p  {cbox u v})) = interior(cbox u v \<inter> \<Union>(p  {cbox u v}))" 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1062 
apply (rule arg_cong[of _ _ interior]) 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1063 
using p(8) uv by auto 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1064 
also have "\<dots> = {}" 
61518
ff12606337e9
new lemmas about topology, etc., for Cauchy integral formula
paulson
parents:
61424
diff
changeset

1065 
unfolding interior_Int 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1066 
apply (rule inter_interior_unions_intervals) 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1067 
using p(6) p(7)[OF p(2)] p(3) 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1068 
apply auto 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1069 
done 
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1070 
finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p  {cbox u v})) = {}" by simp 
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

1071 
have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p  {cbox u v})" 
53399  1072 
using p(8) unfolding uv[symmetric] by auto 
62618
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

1073 
have "insert (cbox a b) (p  {cbox u v}) division_of cbox a b \<union> \<Union>(p  {cbox u v})" 
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

1074 
proof  
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

1075 
have "{cbox a b} division_of cbox a b" 
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

1076 
by (simp add: assms division_of_self) 
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

1077 
then show "insert (cbox a b) (p  {cbox u v}) division_of cbox a b \<union> \<Union>(p  {cbox u v})" 
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

1078 
by (metis (no_types) Diff_subset \<open>interior (cbox a b) \<inter> interior (\<Union>(p  {cbox u v})) = {}\<close> division_disjoint_union division_of_subset insert_is_Un p(1) p(8)) 
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

1079 
qed 
f7f2467ab854
Refactoring (moving theorems into better locations), plus a bit of new material
paulson <lp15@cam.ac.uk>
parents:
62533
diff
changeset

1080 
with that[of "p  {cbox u v}"] show ?thesis by (simp add: cbe) 
50945  1081 
qed 
1082 
qed 

35172  1083 

53399  1084 
lemma division_of_unions: 
1085 
assumes "finite f" 

53408  1086 
and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)" 
53399  1087 
and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}" 
1088 
shows "\<Union>f division_of \<Union>\<Union>f" 

60384  1089 
using assms 
1090 
by (auto intro!: division_ofI) 

53399  1091 

1092 
lemma elementary_union_interval: 

56188  1093 
fixes a b :: "'a::euclidean_space" 
53399  1094 
assumes "p division_of \<Union>p" 
56188  1095 
obtains q where "q division_of (cbox a b \<union> \<Union>p)" 
53399  1096 
proof  
1097 
note assm = division_ofD[OF assms] 

53408  1098 
have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)" 
53399  1099 
by auto 
1100 
have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t t. t \<in> f} = s \<union> \<Union>f" 

1101 
by auto 

1102 
{ 

1103 
presume "p = {} \<Longrightarrow> thesis" 

56188  1104 
"cbox a b = {} \<Longrightarrow> thesis" 
1105 
"cbox a b \<noteq> {} \<Longrightarrow> interior (cbox a b) = {} \<Longrightarrow> thesis" 

1106 
"p \<noteq> {} \<Longrightarrow> interior (cbox a b)\<noteq>{} \<Longrightarrow> cbox a b \<noteq> {} \<Longrightarrow> thesis" 

53399  1107 
then show thesis by auto 
1108 
next 

1109 
assume as: "p = {}" 

56188  1110 
obtain p where "p division_of (cbox a b)" 
53408  1111 
by (rule elementary_interval) 
53399  1112 
then show thesis 
60384  1113 
using as that by auto 
53399  1114 
next 
56188  1115 
assume as: "cbox a b = {}" 
53399  1116 
show thesis 
60384  1117 
using as assms that by auto 
53399  1118 
next 
56188  1119 
assume as: "interior (cbox a b) = {}" "cbox a b \<noteq> {}" 
53399  1120 
show thesis 
56188  1121 
apply (rule that[of "insert (cbox a b) p"],rule division_ofI) 
53399  1122 
unfolding finite_insert 
1123 
apply (rule assm(1)) unfolding Union_insert 

1124 
using assm(24) as 

1125 
apply  

54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54411
diff
changeset

1126 
apply (fast dest: assm(5))+ 
53399  1127 
done 
1128 
next 

56188  1129 
assume as: "p \<noteq> {}" "interior (cbox a b) \<noteq> {}" "cbox a b \<noteq> {}" 
1130 
have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)" 

60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

1131 
proof 
61165  1132 
fix k 
1133 
assume kp: "k \<in> p" 

1134 
from assm(4)[OF kp] obtain c d where "k = cbox c d" by blast 

1135 
then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)" 

60384  1136 
by (meson as(3) division_union_intervals_exists) 
53399  1137 
qed 
56188  1138 
from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" .. 
53408  1139 
note q = division_ofD[OF this[rule_format]] 
56188  1140 
let ?D = "\<Union>{insert (cbox a b) (q k)  k. k \<in> p}" 
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60585
diff
changeset

1141 
show thesis 
60428
5e9de4faef98
fixed several "insideout" proofs
paulson <lp15@cam.ac.uk>
parents:
60425
diff
changeset

1142 
proof (rule that[OF division_ofI]) 
56188  1143 
have *: "{insert (cbox a b) (q k) k. k \<in> p} = (\<lambda>k. insert (cbox a b) (q k)) ` p" 
53399  1144 
by auto 
1145 
show "finite ?D" 

60384  1146 
using "*" assm(1) q(1) by auto 
56188  1147 
show "\<Union>?D = cbox a b \<union> \<Union>p" 
53399 < 