(* Author: John Harrison
Author: Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
*)
section \<open>Kurzweil-Henstock Gauge Integration in many dimensions.\<close>
theory Integration
imports
Derivative
Uniform_Limit
"~~/src/HOL/Library/Indicator_Function"
begin
lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
subsection \<open>Sundries\<close>
lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
declare norm_triangle_ineq4[intro]
lemma simple_image: "{f x |x . x \<in> s} = f ` s"
by blast
lemma linear_simps:
assumes "bounded_linear f"
shows
"f (a + b) = f a + f b"
"f (a - b) = f a - f b"
"f 0 = 0"
"f (- a) = - f a"
"f (s *\<^sub>R v) = s *\<^sub>R (f v)"
proof -
interpret f: bounded_linear f by fact
show "f (a + b) = f a + f b" by (rule f.add)
show "f (a - b) = f a - f b" by (rule f.diff)
show "f 0 = 0" by (rule f.zero)
show "f (- a) = - f a" by (rule f.minus)
show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
qed
lemma bounded_linearI:
assumes "\<And>x y. f (x + y) = f x + f y"
and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
and "\<And>x. norm (f x) \<le> norm x * K"
shows "bounded_linear f"
using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
by (rule bounded_linear_inner_left)
lemma transitive_stepwise_lt_eq:
assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))"
(is "?l = ?r")
proof safe
assume ?r
fix n m :: nat
assume "m < n"
then show "R m n"
proof (induct n arbitrary: m)
case 0
then show ?case by auto
next
case (Suc n)
show ?case
proof (cases "m < n")
case True
show ?thesis
apply (rule assms[OF Suc(1)[OF True]])
using \<open>?r\<close>
apply auto
done
next
case False
then have "m = n"
using Suc(2) by auto
then show ?thesis
using \<open>?r\<close> by auto
qed
qed
qed auto
lemma transitive_stepwise_gt:
assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n)"
shows "\<forall>n>m. R m n"
proof -
have "\<forall>m. \<forall>n>m. R m n"
apply (subst transitive_stepwise_lt_eq)
apply (blast intro: assms)+
done
then show ?thesis by auto
qed
lemma transitive_stepwise_le_eq:
assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))"
(is "?l = ?r")
proof safe
assume ?r
fix m n :: nat
assume "m \<le> n"
then show "R m n"
proof (induct n arbitrary: m)
case 0
with assms show ?case by auto
next
case (Suc n)
show ?case
proof (cases "m \<le> n")
case True
with Suc.hyps \<open>\<forall>n. R n (Suc n)\<close> assms show ?thesis
by blast
next
case False
then have "m = Suc n"
using Suc(2) by auto
then show ?thesis
using assms(1) by auto
qed
qed
qed auto
lemma transitive_stepwise_le:
assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
and "\<And>n. R n (Suc n)"
shows "\<forall>n\<ge>m. R m n"
proof -
have "\<forall>m. \<forall>n\<ge>m. R m n"
apply (subst transitive_stepwise_le_eq)
apply (blast intro: assms)+
done
then show ?thesis by auto
qed
subsection \<open>Some useful lemmas about intervals.\<close>
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
using nonempty_Basis
by (fastforce simp add: set_eq_iff mem_box)
lemma interior_subset_union_intervals:
assumes "i = cbox a b"
and "j = cbox c d"
and "interior j \<noteq> {}"
and "i \<subseteq> j \<union> s"
and "interior i \<inter> interior j = {}"
shows "interior i \<subseteq> interior s"
proof -
have "box a b \<inter> cbox c d = {}"
using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
unfolding assms(1,2) interior_cbox by auto
moreover
have "box a b \<subseteq> cbox c d \<union> s"
apply (rule order_trans,rule box_subset_cbox)
using assms(4) unfolding assms(1,2)
apply auto
done
ultimately
show ?thesis
unfolding assms interior_cbox
by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
qed
lemma inter_interior_unions_intervals:
fixes f::"('a::euclidean_space) set set"
assumes "finite f"
and "open s"
and "\<forall>t\<in>f. \<exists>a b. t = cbox a b"
and "\<forall>t\<in>f. s \<inter> (interior t) = {}"
shows "s \<inter> interior (\<Union>f) = {}"
proof (clarsimp simp only: all_not_in_conv [symmetric])
fix x
assume x: "x \<in> s" "x \<in> interior (\<Union>f)"
have lem1: "\<And>x e s U. ball x e \<subseteq> s \<inter> interior U \<longleftrightarrow> ball x e \<subseteq> s \<inter> U"
using interior_subset
by auto (meson Topology_Euclidean_Space.open_ball contra_subsetD interior_maximal mem_ball)
have "\<exists>t\<in>f. \<exists>x. \<exists>e>0. ball x e \<subseteq> s \<inter> t"
if "finite f" and "\<forall>t\<in>f. \<exists>a b. t = cbox a b" and "\<exists>x. x \<in> s \<inter> interior (\<Union>f)" for f
using that
proof (induct rule: finite_induct)
case empty
obtain x where "x \<in> s \<inter> interior (\<Union>{})"
using empty(2) ..
then have False
unfolding Union_empty interior_empty by auto
then show ?case by auto
next
case (insert i f)
obtain x where x: "x \<in> s \<inter> interior (\<Union>insert i f)"
using insert(5) ..
then obtain e where e: "0 < e \<and> ball x e \<subseteq> s \<inter> interior (\<Union>insert i f)"
unfolding open_contains_ball_eq[OF open_Int[OF assms(2) open_interior], rule_format] ..
obtain a where "\<exists>b. i = cbox a b"
using insert(4)[rule_format,OF insertI1] ..
then obtain b where ab: "i = cbox a b" ..
show ?case
proof (cases "x \<in> i")
case False
then have "x \<in> UNIV - cbox a b"
unfolding ab by auto
then obtain d where "0 < d \<and> ball x d \<subseteq> UNIV - cbox a b"
unfolding open_contains_ball_eq[OF open_Diff[OF open_UNIV closed_cbox],rule_format] ..
then have "0 < d" "ball x (min d e) \<subseteq> UNIV - i"
unfolding ab ball_min_Int by auto
then have "ball x (min d e) \<subseteq> s \<inter> interior (\<Union>f)"
using e unfolding lem1 unfolding ball_min_Int by auto
then have "x \<in> s \<inter> interior (\<Union>f)" using \<open>d>0\<close> e by auto
then have "\<exists>t\<in>f. \<exists>x e. 0 < e \<and> ball x e \<subseteq> s \<inter> t"
using insert.hyps(3) insert.prems(1) by blast
then show ?thesis by auto
next
case True show ?thesis
proof (cases "x\<in>box a b")
case True
then obtain d where "0 < d \<and> ball x d \<subseteq> box a b"
unfolding open_contains_ball_eq[OF open_box,rule_format] ..
then show ?thesis
apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI)
unfolding ab
using box_subset_cbox[of a b] and e
apply fastforce+
done
next
case False
then obtain k where "x\<bullet>k \<le> a\<bullet>k \<or> x\<bullet>k \<ge> b\<bullet>k" and k: "k \<in> Basis"
unfolding mem_box by (auto simp add: not_less)
then have "x\<bullet>k = a\<bullet>k \<or> x\<bullet>k = b\<bullet>k"
using True unfolding ab and mem_box
apply (erule_tac x = k in ballE)
apply auto
done
then have "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)"
proof (rule disjE)
let ?z = "x - (e/2) *\<^sub>R k"
assume as: "x\<bullet>k = a\<bullet>k"
have "ball ?z (e / 2) \<inter> i = {}"
proof (clarsimp simp only: all_not_in_conv [symmetric])
fix y
assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
then have "dist ?z y < e/2" by auto
then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
then have "y\<bullet>k < a\<bullet>k"
using e k
by (auto simp add: field_simps abs_less_iff as inner_simps)
then have "y \<notin> i"
unfolding ab mem_box by (auto intro!: bexI[OF _ k])
then show False using yi by auto
qed
moreover
have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
proof
fix y
assume as: "y \<in> ball ?z (e/2)"
have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R k)"
apply (rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R k"])
unfolding norm_scaleR norm_Basis[OF k]
apply auto
done
also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
apply (rule add_strict_left_mono)
using as e
apply (auto simp add: field_simps dist_norm)
done
finally show "y \<in> ball x e"
unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
qed
ultimately show ?thesis
apply (rule_tac x="?z" in exI)
unfolding Union_insert
apply auto
done
next
let ?z = "x + (e/2) *\<^sub>R k"
assume as: "x\<bullet>k = b\<bullet>k"
have "ball ?z (e / 2) \<inter> i = {}"
proof (clarsimp simp only: all_not_in_conv [symmetric])
fix y
assume "y \<in> ball ?z (e / 2)" and yi: "y \<in> i"
then have "dist ?z y < e/2"
by auto
then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
using Basis_le_norm[OF k, of "?z - y"]
unfolding dist_norm by auto
then have "y\<bullet>k > b\<bullet>k"
using e k
by (auto simp add:field_simps inner_simps inner_Basis as)
then have "y \<notin> i"
unfolding ab mem_box by (auto intro!: bexI[OF _ k])
then show False using yi by auto
qed
moreover
have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)"
apply (rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]])
proof
fix y
assume as: "y\<in> ball ?z (e/2)"
have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y + (e / 2) *\<^sub>R k)"
apply (rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R k"])
unfolding norm_scaleR
apply (auto simp: k)
done
also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2"
apply (rule add_strict_left_mono)
using as unfolding mem_ball dist_norm
using e apply (auto simp add: field_simps)
done
finally show "y \<in> ball x e"
unfolding mem_ball dist_norm using e by (auto simp add:field_simps)
qed
ultimately show ?thesis
apply (rule_tac x="?z" in exI)
unfolding Union_insert
apply auto
done
qed
then obtain x where "ball x (e / 2) \<subseteq> s \<inter> \<Union>f" ..
then have "x \<in> s \<inter> interior (\<Union>f)"
unfolding lem1[where U="\<Union>f", symmetric]
using centre_in_ball e by auto
then show ?thesis
using insert.hyps(3) insert.prems(1) by blast
qed
qed
qed
from this[OF assms(1,3)] x
obtain t x e where "t \<in> f" "0 < e" "ball x e \<subseteq> s \<inter> t"
by blast
then have "x \<in> s" "x \<in> interior t"
using open_subset_interior[OF open_ball, of x e t]
by auto
then show False
using \<open>t \<in> f\<close> assms(4) by auto
qed
subsection \<open>Bounds on intervals where they exist.\<close>
definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
lemma interval_upperbound[simp]:
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
unfolding interval_upperbound_def euclidean_representation_setsum cbox_def
by (safe intro!: cSup_eq) auto
lemma interval_lowerbound[simp]:
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def
by (safe intro!: cInf_eq) auto
lemmas interval_bounds = interval_upperbound interval_lowerbound
lemma
fixes X::"real set"
shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
by (auto simp: interval_upperbound_def interval_lowerbound_def)
lemma interval_bounds'[simp]:
assumes "cbox a b \<noteq> {}"
shows "interval_upperbound (cbox a b) = b"
and "interval_lowerbound (cbox a b) = a"
using assms unfolding box_ne_empty by auto
lemma interval_upperbound_Times:
assumes "A \<noteq> {}" and "B \<noteq> {}"
shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
proof-
from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
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)"
by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
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)"
by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
ultimately show ?thesis unfolding interval_upperbound_def
by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
qed
lemma interval_lowerbound_Times:
assumes "A \<noteq> {}" and "B \<noteq> {}"
shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
proof-
from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
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)"
by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
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)"
by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
ultimately show ?thesis unfolding interval_lowerbound_def
by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
qed
subsection \<open>Content (length, area, volume...) of an interval.\<close>
definition "content (s::('a::euclidean_space) set) =
(if s = {} then 0 else (\<Prod>i\<in>Basis. (interval_upperbound s)\<bullet>i - (interval_lowerbound s)\<bullet>i))"
lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
unfolding box_eq_empty unfolding not_ex not_less by auto
lemma content_cbox:
fixes a :: "'a::euclidean_space"
assumes "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
using interval_not_empty[OF assms]
unfolding content_def
by auto
lemma content_cbox':
fixes a :: "'a::euclidean_space"
assumes "cbox a b \<noteq> {}"
shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
using assms box_ne_empty(1) content_cbox by blast
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
by (auto simp: interval_upperbound_def interval_lowerbound_def content_def)
lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
by (auto simp: content_real)
lemma content_singleton[simp]: "content {a} = 0"
proof -
have "content (cbox a a) = 0"
by (subst content_cbox) (auto simp: ex_in_conv)
then show ?thesis by (simp add: cbox_sing)
qed
lemma content_unit[iff]: "content(cbox 0 (One::'a::euclidean_space)) = 1"
proof -
have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i"
by auto
have "0 \<in> cbox 0 (One::'a)"
unfolding mem_box by auto
then show ?thesis
unfolding content_def interval_bounds[OF *] using setprod.neutral_const by auto
qed
lemma content_pos_le[intro]:
fixes a::"'a::euclidean_space"
shows "0 \<le> content (cbox a b)"
proof (cases "cbox a b = {}")
case False
then have *: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
unfolding box_ne_empty .
have "0 \<le> (\<Prod>i\<in>Basis. interval_upperbound (cbox a b) \<bullet> i - interval_lowerbound (cbox a b) \<bullet> i)"
apply (rule setprod_nonneg)
unfolding interval_bounds[OF *]
using *
apply auto
done
also have "\<dots> = content (cbox a b)" using False by (simp add: content_def)
finally show ?thesis .
qed (simp add: content_def)
corollary content_nonneg [simp]:
fixes a::"'a::euclidean_space"
shows "~ content (cbox a b) < 0"
using not_le by blast
lemma content_pos_lt:
fixes a :: "'a::euclidean_space"
assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
shows "0 < content (cbox a b)"
using assms
by (auto simp: content_def box_eq_empty intro!: setprod_pos)
lemma content_eq_0:
"content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
by (auto simp: content_def box_eq_empty intro!: setprod_pos bexI)
lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
by auto
lemma content_cbox_cases:
"content (cbox a (b::'a::euclidean_space)) =
(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)"
by (auto simp: not_le content_eq_0 intro: less_imp_le content_cbox)
lemma content_eq_0_interior: "content (cbox a b) = 0 \<longleftrightarrow> interior(cbox a b) = {}"
unfolding content_eq_0 interior_cbox box_eq_empty
by auto
lemma content_pos_lt_eq:
"0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
proof (rule iffI)
assume "0 < content (cbox a b)"
then have "content (cbox a b) \<noteq> 0" by auto
then show "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
unfolding content_eq_0 not_ex not_le by fastforce
next
assume "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
then show "0 < content (cbox a b)"
by (metis content_pos_lt)
qed
lemma content_empty [simp]: "content {} = 0"
unfolding content_def by auto
lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
by (simp add: content_real)
lemma content_subset:
assumes "cbox a b \<subseteq> cbox c d"
shows "content (cbox a b) \<le> content (cbox c d)"
proof (cases "cbox a b = {}")
case True
then show ?thesis
using content_pos_le[of c d] by auto
next
case False
then have ab_ne: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
unfolding box_ne_empty by auto
then have ab_ab: "a\<in>cbox a b" "b\<in>cbox a b"
unfolding mem_box by auto
have "cbox c d \<noteq> {}" using assms False by auto
then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i"
using assms unfolding box_ne_empty by auto
have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i - a \<bullet> i"
using ab_ne by auto
moreover
have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)]
assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(1)]
by (metis diff_mono)
ultimately show ?thesis
unfolding content_def interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
by (simp add: setprod_mono if_not_P[OF False] if_not_P[OF \<open>cbox c d \<noteq> {}\<close>])
qed
lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
lemma content_times[simp]: "content (A \<times> B) = content A * content B"
proof (cases "A \<times> B = {}")
let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
assume nonempty: "A \<times> B \<noteq> {}"
hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)"
unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
also have "... = content A * content B" unfolding content_def using nonempty
apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
apply (subst (1 2) setprod.reindex, auto intro: inj_onI)
done
finally show ?thesis .
qed (auto simp: content_def)
lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
by (simp add: cbox_Pair_eq)
lemma content_cbox_pair_eq0_D:
"content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
by (simp add: content_Pair)
lemma content_eq_0_gen:
fixes s :: "'a::euclidean_space set"
assumes "bounded s"
shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)" (is "_ = ?rhs")
proof safe
assume "content s = 0" then show ?rhs
apply (clarsimp simp: ex_in_conv content_def split: if_split_asm)
apply (rule_tac x=a in bexI)
apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI)
apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def)
apply (drule cSUP_eq_cINF_D)
apply (auto simp: bounded_inner_imp_bdd_above [OF assms] bounded_inner_imp_bdd_below [OF assms])
done
next
fix i a
assume "i \<in> Basis" "\<forall>x\<in>s. x \<bullet> i = a"
then show "content s = 0"
apply (clarsimp simp: content_def)
apply (rule_tac x=i in bexI)
apply (auto simp: interval_upperbound_def interval_lowerbound_def)
done
qed
lemma content_0_subset_gen:
fixes a :: "'a::euclidean_space"
assumes "content t = 0" "s \<subseteq> t" "bounded t" shows "content s = 0"
proof -
have "bounded s"
using assms by (metis bounded_subset)
then show ?thesis
using assms
by (auto simp: content_eq_0_gen)
qed
lemma content_0_subset: "\<lbrakk>content(cbox a b) = 0; s \<subseteq> cbox a b\<rbrakk> \<Longrightarrow> content s = 0"
by (simp add: content_0_subset_gen bounded_cbox)
subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
lemma gaugeI:
assumes "\<And>x. x \<in> g x"
and "\<And>x. open (g x)"
shows "gauge g"
using assms unfolding gauge_def by auto
lemma gaugeD[dest]:
assumes "gauge d"
shows "x \<in> d x"
and "open (d x)"
using assms unfolding gauge_def by auto
lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
unfolding gauge_def by auto
lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)"
unfolding gauge_def by auto
lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
by (rule gauge_ball) auto
lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)"
unfolding gauge_def by auto
lemma gauge_inters:
assumes "finite s"
and "\<forall>d\<in>s. gauge (f d)"
shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
proof -
have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
by auto
show ?thesis
unfolding gauge_def unfolding *
using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
qed
lemma gauge_existence_lemma:
"(\<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)"
by (metis zero_less_one)
subsection \<open>Divisions.\<close>
definition division_of (infixl "division'_of" 40)
where
"s division_of i \<longleftrightarrow>
finite s \<and>
(\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = cbox a b)) \<and>
(\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and>
(\<Union>s = i)"
lemma division_ofD[dest]:
assumes "s division_of i"
shows "finite s"
and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
and "\<Union>s = i"
using assms unfolding division_of_def by auto
lemma division_ofI:
assumes "finite s"
and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
and "\<Union>s = i"
shows "s division_of i"
using assms unfolding division_of_def by auto
lemma division_of_finite: "s division_of i \<Longrightarrow> finite s"
unfolding division_of_def by auto
lemma division_of_self[intro]: "cbox a b \<noteq> {} \<Longrightarrow> {cbox a b} division_of (cbox a b)"
unfolding division_of_def by auto
lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}"
unfolding division_of_def by auto
lemma division_of_sing[simp]:
"s division_of cbox a (a::'a::euclidean_space) \<longleftrightarrow> s = {cbox a a}"
(is "?l = ?r")
proof
assume ?r
moreover
{ fix k
assume "s = {{a}}" "k\<in>s"
then have "\<exists>x y. k = cbox x y"
apply (rule_tac x=a in exI)+
apply (force simp: cbox_sing)
done
}
ultimately show ?l
unfolding division_of_def cbox_sing by auto
next
assume ?l
note * = conjunctD4[OF this[unfolded division_of_def cbox_sing]]
{
fix x
assume x: "x \<in> s" have "x = {a}"
using *(2)[rule_format,OF x] by auto
}
moreover have "s \<noteq> {}"
using *(4) by auto
ultimately show ?r
unfolding cbox_sing by auto
qed
lemma elementary_empty: obtains p where "p division_of {}"
unfolding division_of_trivial by auto
lemma elementary_interval: obtains p where "p division_of (cbox a b)"
by (metis division_of_trivial division_of_self)
lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k"
unfolding division_of_def by auto
lemma forall_in_division:
"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))"
unfolding division_of_def by fastforce
lemma division_of_subset:
assumes "p division_of (\<Union>p)"
and "q \<subseteq> p"
shows "q division_of (\<Union>q)"
proof (rule division_ofI)
note * = division_ofD[OF assms(1)]
show "finite q"
using "*"(1) assms(2) infinite_super by auto
{
fix k
assume "k \<in> q"
then have kp: "k \<in> p"
using assms(2) by auto
show "k \<subseteq> \<Union>q"
using \<open>k \<in> q\<close> by auto
show "\<exists>a b. k = cbox a b"
using *(4)[OF kp] by auto
show "k \<noteq> {}"
using *(3)[OF kp] by auto
}
fix k1 k2
assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
then have **: "k1 \<in> p" "k2 \<in> p" "k1 \<noteq> k2"
using assms(2) by auto
show "interior k1 \<inter> interior k2 = {}"
using *(5)[OF **] by auto
qed auto
lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
unfolding division_of_def by auto
lemma division_of_content_0:
assumes "content (cbox a b) = 0" "d division_of (cbox a b)"
shows "\<forall>k\<in>d. content k = 0"
unfolding forall_in_division[OF assms(2)]
by (metis antisym_conv assms content_pos_le content_subset division_ofD(2))
lemma division_inter:
fixes s1 s2 :: "'a::euclidean_space set"
assumes "p1 division_of s1"
and "p2 division_of s2"
shows "{k1 \<inter> k2 | k1 k2 .k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
(is "?A' division_of _")
proof -
let ?A = "{s. s \<in> (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}"
have *: "?A' = ?A" by auto
show ?thesis
unfolding *
proof (rule division_ofI)
have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)"
by auto
moreover have "finite (p1 \<times> p2)"
using assms unfolding division_of_def by auto
ultimately show "finite ?A" by auto
have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
by auto
show "\<Union>?A = s1 \<inter> s2"
apply (rule set_eqI)
unfolding * and UN_iff
using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
apply auto
done
{
fix k
assume "k \<in> ?A"
then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1 \<in> p1" "k2 \<in> p2" "k \<noteq> {}"
by auto
then show "k \<noteq> {}"
by auto
show "k \<subseteq> s1 \<inter> s2"
using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
unfolding k by auto
obtain a1 b1 where k1: "k1 = cbox a1 b1"
using division_ofD(4)[OF assms(1) k(2)] by blast
obtain a2 b2 where k2: "k2 = cbox a2 b2"
using division_ofD(4)[OF assms(2) k(3)] by blast
show "\<exists>a b. k = cbox a b"
unfolding k k1 k2 unfolding inter_interval by auto
}
fix k1 k2
assume "k1 \<in> ?A"
then obtain x1 y1 where k1: "k1 = x1 \<inter> y1" "x1 \<in> p1" "y1 \<in> p2" "k1 \<noteq> {}"
by auto
assume "k2 \<in> ?A"
then obtain x2 y2 where k2: "k2 = x2 \<inter> y2" "x2 \<in> p1" "y2 \<in> p2" "k2 \<noteq> {}"
by auto
assume "k1 \<noteq> k2"
then have th: "x1 \<noteq> x2 \<or> y1 \<noteq> y2"
unfolding k1 k2 by auto
have *: "interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {} \<Longrightarrow>
interior (x1 \<inter> y1) \<subseteq> interior x1 \<Longrightarrow> interior (x1 \<inter> y1) \<subseteq> interior y1 \<Longrightarrow>
interior (x2 \<inter> y2) \<subseteq> interior x2 \<Longrightarrow> interior (x2 \<inter> y2) \<subseteq> interior y2 \<Longrightarrow>
interior (x1 \<inter> y1) \<inter> interior (x2 \<inter> y2) = {}" by auto
show "interior k1 \<inter> interior k2 = {}"
unfolding k1 k2
apply (rule *)
using assms division_ofD(5) k1 k2(2) k2(3) th apply auto
done
qed
qed
lemma division_inter_1:
assumes "d division_of i"
and "cbox a (b::'a::euclidean_space) \<subseteq> i"
shows "{cbox a b \<inter> k | k. k \<in> d \<and> cbox a b \<inter> k \<noteq> {}} division_of (cbox a b)"
proof (cases "cbox a b = {}")
case True
show ?thesis
unfolding True and division_of_trivial by auto
next
case False
have *: "cbox a b \<inter> i = cbox a b" using assms(2) by auto
show ?thesis
using division_inter[OF division_of_self[OF False] assms(1)]
unfolding * by auto
qed
lemma elementary_inter:
fixes s t :: "'a::euclidean_space set"
assumes "p1 division_of s"
and "p2 division_of t"
shows "\<exists>p. p division_of (s \<inter> t)"
using assms division_inter by blast
lemma elementary_inters:
assumes "finite f"
and "f \<noteq> {}"
and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
shows "\<exists>p. p division_of (\<Inter>f)"
using assms
proof (induct f rule: finite_induct)
case (insert x f)
show ?case
proof (cases "f = {}")
case True
then show ?thesis
unfolding True using insert by auto
next
case False
obtain p where "p division_of \<Inter>f"
using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
moreover obtain px where "px division_of x"
using insert(5)[rule_format,OF insertI1] ..
ultimately show ?thesis
by (simp add: elementary_inter Inter_insert)
qed
qed auto
lemma division_disjoint_union:
assumes "p1 division_of s1"
and "p2 division_of s2"
and "interior s1 \<inter> interior s2 = {}"
shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
proof (rule division_ofI)
note d1 = division_ofD[OF assms(1)]
note d2 = division_ofD[OF assms(2)]
show "finite (p1 \<union> p2)"
using d1(1) d2(1) by auto
show "\<Union>(p1 \<union> p2) = s1 \<union> s2"
using d1(6) d2(6) by auto
{
fix k1 k2
assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
moreover
let ?g="interior k1 \<inter> interior k2 = {}"
{
assume as: "k1\<in>p1" "k2\<in>p2"
have ?g
using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
using assms(3) by blast
}
moreover
{
assume as: "k1\<in>p2" "k2\<in>p1"
have ?g
using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
using assms(3) by blast
}
ultimately show ?g
using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
}
fix k
assume k: "k \<in> p1 \<union> p2"
show "k \<subseteq> s1 \<union> s2"
using k d1(2) d2(2) by auto
show "k \<noteq> {}"
using k d1(3) d2(3) by auto
show "\<exists>a b. k = cbox a b"
using k d1(4) d2(4) by auto
qed
lemma partial_division_extend_1:
fixes a b c d :: "'a::euclidean_space"
assumes incl: "cbox c d \<subseteq> cbox a b"
and nonempty: "cbox c d \<noteq> {}"
obtains p where "p division_of (cbox a b)" "cbox c d \<in> p"
proof
let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a.
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)"
def p \<equiv> "?B ` (Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)})"
show "cbox c d \<in> p"
unfolding p_def
by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
{
fix i :: 'a
assume "i \<in> Basis"
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"
unfolding box_eq_empty subset_box by (auto simp: not_le)
}
note ord = this
show "p division_of (cbox a b)"
proof (rule division_ofI)
show "finite p"
unfolding p_def by (auto intro!: finite_PiE)
{
fix k
assume "k \<in> p"
then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
by (auto simp: p_def)
then show "\<exists>a b. k = cbox a b"
by auto
have "k \<subseteq> cbox a b \<and> k \<noteq> {}"
proof (simp add: k box_eq_empty subset_box not_less, safe)
fix i :: 'a
assume i: "i \<in> Basis"
with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
by (auto simp: PiE_iff)
with i ord[of i]
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"
by auto
qed
then show "k \<noteq> {}" "k \<subseteq> cbox a b"
by auto
{
fix l
assume "l \<in> p"
then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
by (auto simp: p_def)
assume "l \<noteq> k"
have "\<exists>i\<in>Basis. f i \<noteq> g i"
proof (rule ccontr)
assume "\<not> ?thesis"
with f g have "f = g"
by (auto simp: PiE_iff extensional_def intro!: ext)
with \<open>l \<noteq> k\<close> show False
by (simp add: l k)
qed
then obtain i where *: "i \<in> Basis" "f i \<noteq> g i" ..
then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
"g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
using f g by (auto simp: PiE_iff)
with * ord[of i] show "interior l \<inter> interior k = {}"
by (auto simp add: l k interior_cbox disjoint_interval intro!: bexI[of _ i])
}
note \<open>k \<subseteq> cbox a b\<close>
}
moreover
{
fix x assume x: "x \<in> cbox a b"
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)}"
proof
fix i :: 'a
assume "i \<in> Basis"
with x ord[of i]
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>
(d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
by (auto simp: cbox_def)
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)}"
by auto
qed
then obtain f where
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)}"
unfolding bchoice_iff ..
moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
by auto
moreover from f have "x \<in> ?B (restrict f Basis)"
by (auto simp: mem_box)
ultimately have "\<exists>k\<in>p. x \<in> k"
unfolding p_def by blast
}
ultimately show "\<Union>p = cbox a b"
by auto
qed
qed
lemma partial_division_extend_interval:
assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> cbox a b"
obtains q where "p \<subseteq> q" "q division_of cbox a (b::'a::euclidean_space)"
proof (cases "p = {}")
case True
obtain q where "q division_of (cbox a b)"
by (rule elementary_interval)
then show ?thesis
using True that by blast
next
case False
note p = division_ofD[OF assms(1)]
have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
proof
fix k
assume kp: "k \<in> p"
obtain c d where k: "k = cbox c d"
using p(4)[OF kp] by blast
have *: "cbox c d \<subseteq> cbox a b" "cbox c d \<noteq> {}"
using p(2,3)[OF kp, unfolded k] using assms(2)
by (blast intro: order.trans)+
obtain q where "q division_of cbox a b" "cbox c d \<in> q"
by (rule partial_division_extend_1[OF *])
then show "\<exists>q. q division_of cbox a b \<and> k \<in> q"
unfolding k by auto
qed
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"
using bchoice[OF div_cbox] by blast
{ fix x
assume x: "x \<in> p"
have "q x division_of \<Union>q x"
apply (rule division_ofI)
using division_ofD[OF q(1)[OF x]]
apply auto
done }
then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
by (meson Diff_subset division_of_subset)
then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
apply -
apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
done
then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
have "d \<union> p division_of cbox a b"
proof -
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
have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
proof (rule te[OF False], clarify)
fix i
assume i: "i \<in> p"
show "\<Union>(q i - {i}) \<union> i = cbox a b"
using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
qed
{ fix k
assume k: "k \<in> p"
have *: "\<And>u t s. t \<inter> s = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<inter> t = {}"
by auto
have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior k = {}"
proof (rule *[OF inter_interior_unions_intervals])
note qk=division_ofD[OF q(1)[OF k]]
show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = cbox a b"
using qk by auto
show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
using qk(5) using q(2)[OF k] by auto
show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q k - {k}))"
apply (rule interior_mono)+
using k
apply auto
done
qed } note [simp] = this
show "d \<union> p division_of (cbox a b)"
unfolding cbox_eq
apply (rule division_disjoint_union[OF d assms(1)])
apply (rule inter_interior_unions_intervals)
apply (rule p open_interior ballI)+
apply simp_all
done
qed
then show ?thesis
by (meson Un_upper2 that)
qed
lemma elementary_bounded[dest]:
fixes s :: "'a::euclidean_space set"
shows "p division_of s \<Longrightarrow> bounded s"
unfolding division_of_def by (metis bounded_Union bounded_cbox)
lemma elementary_subset_cbox:
"p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a (b::'a::euclidean_space)"
by (meson elementary_bounded bounded_subset_cbox)
lemma division_union_intervals_exists:
fixes a b :: "'a::euclidean_space"
assumes "cbox a b \<noteq> {}"
obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)"
proof (cases "cbox c d = {}")
case True
show ?thesis
apply (rule that[of "{}"])
unfolding True
using assms
apply auto
done
next
case False
show ?thesis
proof (cases "cbox a b \<inter> cbox c d = {}")
case True
then show ?thesis
by (metis that False assms division_disjoint_union division_of_self insert_is_Un interior_Int interior_empty)
next
case False
obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
unfolding inter_interval by auto
have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
obtain p where "p division_of cbox c d" "cbox u v \<in> p"
by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
note p = this division_ofD[OF this(1)]
have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
apply (rule arg_cong[of _ _ interior])
using p(8) uv by auto
also have "\<dots> = {}"
unfolding interior_Int
apply (rule inter_interior_unions_intervals)
using p(6) p(7)[OF p(2)] p(3)
apply auto
done
finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})"
using p(8) unfolding uv[symmetric] by auto
have "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
proof -
have "{cbox a b} division_of cbox a b"
by (simp add: assms division_of_self)
then show "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
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))
qed
with that[of "p - {cbox u v}"] show ?thesis by (simp add: cbe)
qed
qed
lemma division_of_unions:
assumes "finite f"
and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
shows "\<Union>f division_of \<Union>\<Union>f"
using assms
by (auto intro!: division_ofI)
lemma elementary_union_interval:
fixes a b :: "'a::euclidean_space"
assumes "p division_of \<Union>p"
obtains q where "q division_of (cbox a b \<union> \<Union>p)"
proof -
note assm = division_ofD[OF assms]
have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
by auto
have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
by auto
{
presume "p = {} \<Longrightarrow> thesis"
"cbox a b = {} \<Longrightarrow> thesis"
"cbox a b \<noteq> {} \<Longrightarrow> interior (cbox a b) = {} \<Longrightarrow> thesis"
"p \<noteq> {} \<Longrightarrow> interior (cbox a b)\<noteq>{} \<Longrightarrow> cbox a b \<noteq> {} \<Longrightarrow> thesis"
then show thesis by auto
next
assume as: "p = {}"
obtain p where "p division_of (cbox a b)"
by (rule elementary_interval)
then show thesis
using as that by auto
next
assume as: "cbox a b = {}"
show thesis
using as assms that by auto
next
assume as: "interior (cbox a b) = {}" "cbox a b \<noteq> {}"
show thesis
apply (rule that[of "insert (cbox a b) p"],rule division_ofI)
unfolding finite_insert
apply (rule assm(1)) unfolding Union_insert
using assm(2-4) as
apply -
apply (fast dest: assm(5))+
done
next
assume as: "p \<noteq> {}" "interior (cbox a b) \<noteq> {}" "cbox a b \<noteq> {}"
have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
proof
fix k
assume kp: "k \<in> p"
from assm(4)[OF kp] obtain c d where "k = cbox c d" by blast
then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
by (meson as(3) division_union_intervals_exists)
qed
from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
note q = division_ofD[OF this[rule_format]]
let ?D = "\<Union>{insert (cbox a b) (q k) | k. k \<in> p}"
show thesis
proof (rule that[OF division_ofI])
have *: "{insert (cbox a b) (q k) |k. k \<in> p} = (\<lambda>k. insert (cbox a b) (q k)) ` p"
by auto
show "finite ?D"
using "*" assm(1) q(1) by auto
show "\<Union>?D = cbox a b \<union> \<Union>p"
unfolding * lem1
unfolding lem2[OF as(1), of "cbox a b", symmetric]
using q(6)
by auto
fix k
assume k: "k \<in> ?D"
then show "k \<subseteq> cbox a b \<union> \<Union>p"
using q(2) by auto
show "k \<noteq> {}"
using q(3) k by auto
show "\<exists>a b. k = cbox a b"
using q(4) k by auto
fix k'
assume k': "k' \<in> ?D" "k \<noteq> k'"
obtain x where x: "k \<in> insert (cbox a b) (q x)" "x\<in>p"
using k by auto
obtain x' where x': "k'\<in>insert (cbox a b) (q x')" "x'\<in>p"
using k' by auto
show "interior k \<inter> interior k' = {}"
proof (cases "x = x'")
case True
show ?thesis
using True k' q(5) x' x by auto
next
case False
{
presume "k = cbox a b \<Longrightarrow> ?thesis"
and "k' = cbox a b \<Longrightarrow> ?thesis"
and "k \<noteq> cbox a b \<Longrightarrow> k' \<noteq> cbox a b \<Longrightarrow> ?thesis"
then show ?thesis by linarith
next
assume as': "k = cbox a b"
show ?thesis
using as' k' q(5) x' by blast
next
assume as': "k' = cbox a b"
show ?thesis
using as' k'(2) q(5) x by blast
}
assume as': "k \<noteq> cbox a b" "k' \<noteq> cbox a b"
obtain c d where k: "k = cbox c d"
using q(4)[OF x(2,1)] by blast
have "interior k \<inter> interior (cbox a b) = {}"
using as' k'(2) q(5) x by blast
then have "interior k \<subseteq> interior x"
using interior_subset_union_intervals
by (metis as(2) k q(2) x interior_subset_union_intervals)
moreover
obtain c d where c_d: "k' = cbox c d"
using q(4)[OF x'(2,1)] by blast
have "interior k' \<inter> interior (cbox a b) = {}"
using as'(2) q(5) x' by blast
then have "interior k' \<subseteq> interior x'"
by (metis as(2) c_d interior_subset_union_intervals q(2) x'(1) x'(2))
ultimately show ?thesis
using assm(5)[OF x(2) x'(2) False] by auto
qed
qed
}
qed
lemma elementary_unions_intervals:
assumes fin: "finite f"
and "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a (b::'a::euclidean_space)"
obtains p where "p division_of (\<Union>f)"
proof -
have "\<exists>p. p division_of (\<Union>f)"
proof (induct_tac f rule:finite_subset_induct)
show "\<exists>p. p division_of \<Union>{}" using elementary_empty by auto
next
fix x F
assume as: "finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f"
from this(3) obtain p where p: "p division_of \<Union>F" ..
from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
have *: "\<Union>F = \<Union>p"
using division_ofD[OF p] by auto
show "\<exists>p. p division_of \<Union>insert x F"
using elementary_union_interval[OF p[unfolded *], of a b]
unfolding Union_insert x * by metis
qed (insert assms, auto)
then show ?thesis
using that by auto
qed
lemma elementary_union:
fixes s t :: "'a::euclidean_space set"
assumes "ps division_of s" "pt division_of t"
obtains p where "p division_of (s \<union> t)"
proof -
have *: "s \<union> t = \<Union>ps \<union> \<Union>pt"
using assms unfolding division_of_def by auto
show ?thesis
apply (rule elementary_unions_intervals[of "ps \<union> pt"])
using assms apply auto
by (simp add: * that)
qed
lemma partial_division_extend:
fixes t :: "'a::euclidean_space set"
assumes "p division_of s"
and "q division_of t"
and "s \<subseteq> t"
obtains r where "p \<subseteq> r" and "r division_of t"
proof -
note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
obtain a b where ab: "t \<subseteq> cbox a b"
using elementary_subset_cbox[OF assms(2)] by auto
obtain r1 where "p \<subseteq> r1" "r1 division_of (cbox a b)"
using assms
by (metis ab dual_order.trans partial_division_extend_interval divp(6))
note r1 = this division_ofD[OF this(2)]
obtain p' where "p' division_of \<Union>(r1 - p)"
apply (rule elementary_unions_intervals[of "r1 - p"])
using r1(3,6)
apply auto
done
then obtain r2 where r2: "r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)"
by (metis assms(2) divq(6) elementary_inter)
{
fix x
assume x: "x \<in> t" "x \<notin> s"
then have "x\<in>\<Union>r1"
unfolding r1 using ab by auto
then obtain r where r: "r \<in> r1" "x \<in> r"
unfolding Union_iff ..
moreover
have "r \<notin> p"
proof
assume "r \<in> p"
then have "x \<in> s" using divp(2) r by auto
then show False using x by auto
qed
ultimately have "x\<in>\<Union>(r1 - p)" by auto
}
then have *: "t = \<Union>p \<union> (\<Union>(r1 - p) \<inter> \<Union>q)"
unfolding divp divq using assms(3) by auto
show ?thesis
apply (rule that[of "p \<union> r2"])
unfolding *
defer
apply (rule division_disjoint_union)
unfolding divp(6)
apply(rule assms r2)+
proof -
have "interior s \<inter> interior (\<Union>(r1-p)) = {}"
proof (rule inter_interior_unions_intervals)
show "finite (r1 - p)" and "open (interior s)" and "\<forall>t\<in>r1-p. \<exists>a b. t = cbox a b"
using r1 by auto
have *: "\<And>s. (\<And>x. x \<in> s \<Longrightarrow> False) \<Longrightarrow> s = {}"
by auto
show "\<forall>t\<in>r1-p. interior s \<inter> interior t = {}"
proof
fix m x
assume as: "m \<in> r1 - p"
have "interior m \<inter> interior (\<Union>p) = {}"
proof (rule inter_interior_unions_intervals)
show "finite p" and "open (interior m)" and "\<forall>t\<in>p. \<exists>a b. t = cbox a b"
using divp by auto
show "\<forall>t\<in>p. interior m \<inter> interior t = {}"
by (metis DiffD1 DiffD2 as r1(1) r1(7) set_rev_mp)
qed
then show "interior s \<inter> interior m = {}"
unfolding divp by auto
qed
qed
then show "interior s \<inter> interior (\<Union>(r1-p) \<inter> (\<Union>q)) = {}"
using interior_subset by auto
qed auto
qed
subsection \<open>Tagged (partial) divisions.\<close>
definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
where "s tagged_partial_division_of i \<longleftrightarrow>
finite s \<and>
(\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = cbox a b)) \<and>
(\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
interior k1 \<inter> interior k2 = {})"
lemma tagged_partial_division_ofD[dest]:
assumes "s tagged_partial_division_of i"
shows "finite s"
and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow>
(x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
using assms unfolding tagged_partial_division_of_def by blast+
definition tagged_division_of (infixr "tagged'_division'_of" 40)
where "s tagged_division_of i \<longleftrightarrow> s tagged_partial_division_of i \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
unfolding tagged_division_of_def tagged_partial_division_of_def by auto
lemma tagged_division_of:
"s tagged_division_of i \<longleftrightarrow>
finite s \<and>
(\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = cbox a b)) \<and>
(\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
interior k1 \<inter> interior k2 = {}) \<and>
(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
unfolding tagged_division_of_def tagged_partial_division_of_def by auto
lemma tagged_division_ofI:
assumes "finite s"
and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
interior k1 \<inter> interior k2 = {}"
and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
shows "s tagged_division_of i"
unfolding tagged_division_of
using assms
apply auto
apply fastforce+
done
lemma tagged_division_ofD[dest]: (*FIXME USE A LOCALE*)
assumes "s tagged_division_of i"
shows "finite s"
and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
and "\<And>x1 k1 x2 k2. (x1, k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
interior k1 \<inter> interior k2 = {}"
and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
using assms unfolding tagged_division_of by blast+
lemma division_of_tagged_division:
assumes "s tagged_division_of i"
shows "(snd ` s) division_of i"
proof (rule division_ofI)
note assm = tagged_division_ofD[OF assms]
show "\<Union>(snd ` s) = i" "finite (snd ` s)"
using assm by auto
fix k
assume k: "k \<in> snd ` s"
then obtain xk where xk: "(xk, k) \<in> s"
by auto
then show "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = cbox a b"
using assm by fastforce+
fix k'
assume k': "k' \<in> snd ` s" "k \<noteq> k'"
from this(1) obtain xk' where xk': "(xk', k') \<in> s"
by auto
then show "interior k \<inter> interior k' = {}"
using assm(5) k'(2) xk by blast
qed
lemma partial_division_of_tagged_division:
assumes "s tagged_partial_division_of i"
shows "(snd ` s) division_of \<Union>(snd ` s)"
proof (rule division_ofI)
note assm = tagged_partial_division_ofD[OF assms]
show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)"
using assm by auto
fix k
assume k: "k \<in> snd ` s"
then obtain xk where xk: "(xk, k) \<in> s"
by auto
then show "k \<noteq> {}" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>(snd ` s)"
using assm by auto
fix k'
assume k': "k' \<in> snd ` s" "k \<noteq> k'"
from this(1) obtain xk' where xk': "(xk', k') \<in> s"
by auto
then show "interior k \<inter> interior k' = {}"
using assm(5) k'(2) xk by auto
qed
lemma tagged_partial_division_subset:
assumes "s tagged_partial_division_of i"
and "t \<subseteq> s"
shows "t tagged_partial_division_of i"
using assms
unfolding tagged_partial_division_of_def
using finite_subset[OF assms(2)]
by blast
lemma setsum_over_tagged_division_lemma:
assumes "p tagged_division_of i"
and "\<And>u v. cbox u v \<noteq> {} \<Longrightarrow> content (cbox u v) = 0 \<Longrightarrow> d (cbox u v) = 0"
shows "setsum (\<lambda>(x,k). d k) p = setsum d (snd ` p)"
proof -
have *: "(\<lambda>(x,k). d k) = d \<circ> snd"
unfolding o_def by (rule ext) auto
note assm = tagged_division_ofD[OF assms(1)]
show ?thesis
unfolding *
proof (rule setsum.reindex_nontrivial[symmetric])
show "finite p"
using assm by auto
fix x y
assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
obtain a b where ab: "snd x = cbox a b"
using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
by (metis prod.collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
by (intro assm(5)[of "fst x" _ "fst y"]) auto
then have "content (cbox a b) = 0"
unfolding \<open>snd x = snd y\<close>[symmetric] ab content_eq_0_interior by auto
then have "d (cbox a b) = 0"
using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
then show "d (snd x) = 0"
unfolding ab by auto
qed
qed
lemma tag_in_interval: "p tagged_division_of i \<Longrightarrow> (x, k) \<in> p \<Longrightarrow> x \<in> i"
by auto
lemma tagged_division_of_empty: "{} tagged_division_of {}"
unfolding tagged_division_of by auto
lemma tagged_partial_division_of_trivial[simp]: "p tagged_partial_division_of {} \<longleftrightarrow> p = {}"
unfolding tagged_partial_division_of_def by auto
lemma tagged_division_of_trivial[simp]: "p tagged_division_of {} \<longleftrightarrow> p = {}"
unfolding tagged_division_of by auto
lemma tagged_division_of_self: "x \<in> cbox a b \<Longrightarrow> {(x,cbox a b)} tagged_division_of (cbox a b)"
by (rule tagged_division_ofI) auto
lemma tagged_division_of_self_real: "x \<in> {a .. b::real} \<Longrightarrow> {(x,{a .. b})} tagged_division_of {a .. b}"
unfolding box_real[symmetric]
by (rule tagged_division_of_self)
lemma tagged_division_union:
assumes "p1 tagged_division_of s1"
and "p2 tagged_division_of s2"
and "interior s1 \<inter> interior s2 = {}"
shows "(p1 \<union> p2) tagged_division_of (s1 \<union> s2)"
proof (rule tagged_division_ofI)
note p1 = tagged_division_ofD[OF assms(1)]
note p2 = tagged_division_ofD[OF assms(2)]
show "finite (p1 \<union> p2)"
using p1(1) p2(1) by auto
show "\<Union>{k. \<exists>x. (x, k) \<in> p1 \<union> p2} = s1 \<union> s2"
using p1(6) p2(6) by blast
fix x k
assume xk: "(x, k) \<in> p1 \<union> p2"
show "x \<in> k" "\<exists>a b. k = cbox a b"
using xk p1(2,4) p2(2,4) by auto
show "k \<subseteq> s1 \<union> s2"
using xk p1(3) p2(3) by blast
fix x' k'
assume xk': "(x', k') \<in> p1 \<union> p2" "(x, k) \<noteq> (x', k')"
have *: "\<And>a b. a \<subseteq> s1 \<Longrightarrow> b \<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}"
using assms(3) interior_mono by blast
show "interior k \<inter> interior k' = {}"
apply (cases "(x, k) \<in> p1")
apply (meson "*" UnE assms(1) assms(2) p1(5) tagged_division_ofD(3) xk'(1) xk'(2))
by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
qed
lemma tagged_division_unions:
assumes "finite iset"
and "\<forall>i\<in>iset. pfn i tagged_division_of i"
and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)"
proof (rule tagged_division_ofI)
note assm = tagged_division_ofD[OF assms(2)[rule_format]]
show "finite (\<Union>(pfn ` iset))"
apply (rule finite_Union)
using assms
apply auto
done
have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)"
by blast
also have "\<dots> = \<Union>iset"
using assm(6) by auto
finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>iset" .
fix x k
assume xk: "(x, k) \<in> \<Union>(pfn ` iset)"
then obtain i where i: "i \<in> iset" "(x, k) \<in> pfn i"
by auto
show "x \<in> k" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>iset"
using assm(2-4)[OF i] using i(1) by auto
fix x' k'
assume xk': "(x', k') \<in> \<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')"
then obtain i' where i': "i' \<in> iset" "(x', k') \<in> pfn i'"
by auto
have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}"
using i(1) i'(1)
using assms(3)[rule_format] interior_mono
by blast
show "interior k \<inter> interior k' = {}"
apply (cases "i = i'")
using assm(5) i' i(2) xk'(2) apply blast
using "*" assm(3) i' i by auto
qed
lemma tagged_partial_division_of_union_self:
assumes "p tagged_partial_division_of s"
shows "p tagged_division_of (\<Union>(snd ` p))"
apply (rule tagged_division_ofI)
using tagged_partial_division_ofD[OF assms]
apply auto
done
lemma tagged_division_of_union_self:
assumes "p tagged_division_of s"
shows "p tagged_division_of (\<Union>(snd ` p))"
apply (rule tagged_division_ofI)
using tagged_division_ofD[OF assms]
apply auto
done
subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
definition fine (infixr "fine" 46)
where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
lemma fineI:
assumes "\<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x"
shows "d fine s"
using assms unfolding fine_def by auto
lemma fineD[dest]:
assumes "d fine s"
shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
using assms unfolding fine_def by auto
lemma fine_inter: "(\<lambda>x. d1 x \<inter> d2 x) fine p \<longleftrightarrow> d1 fine p \<and> d2 fine p"
unfolding fine_def by auto
lemma fine_inters:
"(\<lambda>x. \<Inter>{f d x | d. d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
unfolding fine_def by blast
lemma fine_union: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
unfolding fine_def by blast
lemma fine_unions: "(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
unfolding fine_def by auto
lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
unfolding fine_def by blast
subsection \<open>Gauge integral. Define on compact intervals first, then use a limit.\<close>
definition has_integral_compact_interval (infixr "has'_integral'_compact'_interval" 46)
where "(f has_integral_compact_interval y) i \<longleftrightarrow>
(\<forall>e>0. \<exists>d. gauge d \<and>
(\<forall>p. p tagged_division_of i \<and> d fine p \<longrightarrow>
norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - y) < e))"
definition has_integral ::
"('n::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> 'n set \<Rightarrow> bool"
(infixr "has'_integral" 46)
where "(f has_integral y) i \<longleftrightarrow>
(if \<exists>a b. i = cbox a b
then (f has_integral_compact_interval y) i
else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
(\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral_compact_interval z) (cbox a b) \<and>
norm (z - y) < e)))"
lemma has_integral:
"(f has_integral y) (cbox a b) \<longleftrightarrow>
(\<forall>e>0. \<exists>d. gauge d \<and>
(\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
unfolding has_integral_def has_integral_compact_interval_def
by auto
lemma has_integral_real:
"(f has_integral y) {a .. b::real} \<longleftrightarrow>
(\<forall>e>0. \<exists>d. gauge d \<and>
(\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow>
norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
unfolding box_real[symmetric]
by (rule has_integral)
lemma has_integralD[dest]:
assumes "(f has_integral y) (cbox a b)"
and "e > 0"
obtains d where "gauge d"
and "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d fine p \<Longrightarrow>
norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f(x)) p - y) < e"
using assms unfolding has_integral by auto
lemma has_integral_alt:
"(f has_integral y) i \<longleftrightarrow>
(if \<exists>a b. i = cbox a b
then (f has_integral y) i
else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
(\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e)))"
unfolding has_integral
unfolding has_integral_compact_interval_def has_integral_def
by auto
lemma has_integral_altD:
assumes "(f has_integral y) i"
and "\<not> (\<exists>a b. i = cbox a b)"
and "e>0"
obtains B where "B > 0"
and "\<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
(\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) (cbox a b) \<and> norm(z - y) < e)"
using assms
unfolding has_integral
unfolding has_integral_compact_interval_def has_integral_def
by auto
definition integrable_on (infixr "integrable'_on" 46)
where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)"
definition "integral i f = (SOME y. (f has_integral y) i \<or> ~ f integrable_on i \<and> y=0)"
lemma integrable_integral[dest]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)
lemma not_integrable_integral: "~ f integrable_on i \<Longrightarrow> integral i f = 0"
unfolding integrable_on_def integral_def by blast
lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
unfolding integrable_on_def by auto
lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
by auto
lemma setsum_content_null:
assumes "content (cbox a b) = 0"
and "p tagged_division_of (cbox a b)"
shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
proof (rule setsum.neutral, rule)
fix y
assume y: "y \<in> p"
obtain x k where xk: "y = (x, k)"
using surj_pair[of y] by blast
note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
from this(2) obtain c d where k: "k = cbox c d" by blast
have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
unfolding xk by auto
also have "\<dots> = 0"
using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
unfolding assms(1) k
by auto
finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
qed
subsection \<open>Some basic combining lemmas.\<close>
lemma tagged_division_unions_exists:
assumes "finite iset"
and "\<forall>i\<in>iset. \<exists>p. p tagged_division_of i \<and> d fine p"
and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
and "\<Union>iset = i"
obtains p where "p tagged_division_of i" and "d fine p"
proof -
obtain pfn where pfn:
"\<And>x. x \<in> iset \<Longrightarrow> pfn x tagged_division_of x"
"\<And>x. x \<in> iset \<Longrightarrow> d fine pfn x"
using bchoice[OF assms(2)] by auto
show thesis
apply (rule_tac p="\<Union>(pfn ` iset)" in that)
using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force
by (metis (mono_tags, lifting) fine_unions imageE pfn(2))
qed
subsection \<open>The set we're concerned with must be closed.\<close>
lemma division_of_closed:
fixes i :: "'n::euclidean_space set"
shows "s division_of i \<Longrightarrow> closed i"
unfolding division_of_def by fastforce
subsection \<open>General bisection principle for intervals; might be useful elsewhere.\<close>
lemma interval_bisection_step:
fixes type :: "'a::euclidean_space"
assumes "P {}"
and "\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P (s \<union> t)"
and "\<not> P (cbox a (b::'a))"
obtains c d where "\<not> P (cbox c d)"
and "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
proof -
have "cbox a b \<noteq> {}"
using assms(1,3) by metis
then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
by (force simp: mem_box)
{ fix f
have "\<lbrakk>finite f;
\<And>s. s\<in>f \<Longrightarrow> P s;
\<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
\<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>f)"
proof (induct f rule: finite_induct)
case empty
show ?case
using assms(1) by auto
next
case (insert x f)
show ?case
unfolding Union_insert
apply (rule assms(2)[rule_format])
using inter_interior_unions_intervals [of f "interior x"]
apply (auto simp: insert)
by (metis IntI empty_iff insert.hyps(2) insert.prems(3) insert_iff)
qed
} note UN_cases = this
let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or>
(c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
{
presume "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d) \<Longrightarrow> False"
then show thesis
unfolding atomize_not not_all
by (blast intro: that)
}
assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
have "P (\<Union>?A)"
proof (rule UN_cases)
let ?B = "(\<lambda>s. cbox (\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i::'a)
(\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
have "?A \<subseteq> ?B"
proof
fix x
assume "x \<in> ?A"
then obtain c d
where x: "x = cbox c d"
"\<And>i. i \<in> Basis \<Longrightarrow>
c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
show "x \<in> ?B"
unfolding image_iff x
apply (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in bexI)
apply (rule arg_cong2 [where f = cbox])
using x(2) ab
apply (auto simp add: euclidean_eq_iff[where 'a='a])
by fastforce
qed
then show "finite ?A"
by (rule finite_subset) auto
next
fix s
assume "s \<in> ?A"
then obtain c d
where s: "s = cbox c d"
"\<And>i. i \<in> Basis \<Longrightarrow>
c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
by blast
show "P s"
unfolding s
apply (rule as[rule_format])
using ab s(2) by force
show "\<exists>a b. s = cbox a b"
unfolding s by auto
fix t
assume "t \<in> ?A"
then obtain e f where t:
"t = cbox e f"
"\<And>i. i \<in> Basis \<Longrightarrow>
e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
e \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> f \<bullet> i = b \<bullet> i"
by blast
assume "s \<noteq> t"
then have "\<not> (c = e \<and> d = f)"
unfolding s t by auto
then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
unfolding euclidean_eq_iff[where 'a='a] by auto
then have i: "c\<bullet>i \<noteq> e\<bullet>i" "d\<bullet>i \<noteq> f\<bullet>i"
using s(2) t(2) apply fastforce
using t(2)[OF i'] \<open>c \<bullet> i \<noteq> e \<bullet> i \<or> d \<bullet> i \<noteq> f \<bullet> i\<close> i' s(2) t(2) by fastforce
have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
by auto
show "interior s \<inter> interior t = {}"
unfolding s t interior_cbox
proof (rule *)
fix x
assume "x \<in> box c d" "x \<in> box e f"
then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
unfolding mem_box using i'
by force+
show False using s(2)[OF i']
proof safe
assume as: "c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2"
show False
using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps)
next
assume as: "c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" "d \<bullet> i = b \<bullet> i"
show False
using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps)
qed
qed
qed
also have "\<Union>?A = cbox a b"
proof (rule set_eqI,rule)
fix x
assume "x \<in> \<Union>?A"
then obtain c d where x:
"x \<in> cbox c d"
"\<And>i. i \<in> Basis \<Longrightarrow>
c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
by blast
show "x\<in>cbox a b"
unfolding mem_box
proof safe
fix i :: 'a
assume i: "i \<in> Basis"
then show "a \<bullet> i \<le> x \<bullet> i" "x \<bullet> i \<le> b \<bullet> i"
using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto
qed
next
fix x
assume x: "x \<in> cbox a b"
have "\<forall>i\<in>Basis.
\<exists>c d. (c = a\<bullet>i \<and> d = (a\<bullet>i + b\<bullet>i) / 2 \<or> c = (a\<bullet>i + b\<bullet>i) / 2 \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
(is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d")
unfolding mem_box
proof
fix i :: 'a
assume i: "i \<in> Basis"
have "?P i (a\<bullet>i) ((a \<bullet> i + b \<bullet> i) / 2) \<or> ?P i ((a \<bullet> i + b \<bullet> i) / 2) (b\<bullet>i)"
using x[unfolded mem_box,THEN bspec, OF i] by auto
then show "\<exists>c d. ?P i c d"
by blast
qed
then show "x\<in>\<Union>?A"
unfolding Union_iff Bex_def mem_Collect_eq choice_Basis_iff
apply auto
apply (rule_tac x="cbox xa xaa" in exI)
unfolding mem_box
apply auto
done
qed
finally show False
using assms by auto
qed
lemma interval_bisection:
fixes type :: "'a::euclidean_space"
assumes "P {}"
and "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))"
and "\<not> P (cbox a (b::'a))"
obtains x where "x \<in> cbox a b"
and "\<forall>e>0. \<exists>c d. x \<in> cbox c d \<and> cbox c d \<subseteq> ball x e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
proof -
have "\<forall>x. \<exists>y. \<not> P (cbox (fst x) (snd x)) \<longrightarrow> (\<not> P (cbox (fst y) (snd y)) \<and>
(\<forall>i\<in>Basis. fst x\<bullet>i \<le> fst y\<bullet>i \<and> fst y\<bullet>i \<le> snd y\<bullet>i \<and> snd y\<bullet>i \<le> snd x\<bullet>i \<and>
2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))" (is "\<forall>x. ?P x")
proof
show "?P x" for x
proof (cases "P (cbox (fst x) (snd x))")
case True
then show ?thesis by auto
next
case as: False
obtain c d where "\<not> P (cbox c d)"
"\<forall>i\<in>Basis.
fst x \<bullet> i \<le> c \<bullet> i \<and>
c \<bullet> i \<le> d \<bullet> i \<and>
d \<bullet> i \<le> snd x \<bullet> i \<and>
2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i"
by (rule interval_bisection_step[of P, OF assms(1-2) as])
then show ?thesis
apply -
apply (rule_tac x="(c,d)" in exI)
apply auto
done
qed
qed
then obtain f where f:
"\<forall>x.
\<not> P (cbox (fst x) (snd x)) \<longrightarrow>
\<not> P (cbox (fst (f x)) (snd (f x))) \<and>
(\<forall>i\<in>Basis.
fst x \<bullet> i \<le> fst (f x) \<bullet> i \<and>
fst (f x) \<bullet> i \<le> snd (f x) \<bullet> i \<and>
snd (f x) \<bullet> i \<le> snd x \<bullet> i \<and>
2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i)"
apply -
apply (drule choice)
apply blast
done
def AB \<equiv> "\<lambda>n. (f ^^ n) (a,b)"
def A \<equiv> "\<lambda>n. fst(AB n)"
def B \<equiv> "\<lambda>n. snd(AB n)"
note ab_def = A_def B_def AB_def
have "A 0 = a" "B 0 = b" "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
(\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and>
2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i)" (is "\<And>n. ?P n")
proof -
show "A 0 = a" "B 0 = b"
unfolding ab_def by auto
note S = ab_def funpow.simps o_def id_apply
show "?P n" for n
proof (induct n)
case 0
then show ?case
unfolding S
apply (rule f[rule_format]) using assms(3)
apply auto
done
next
case (Suc n)
show ?case
unfolding S
apply (rule f[rule_format])
using Suc
unfolding S