Theory Tagged_Division
section ‹Tagged Divisions for Henstock-Kurzweil Integration›
theory Tagged_Division
imports Topology_Euclidean_Space
begin
lemma sum_Sigma_product:
assumes "finite S"
and "⋀i. i ∈ S ⟹ finite (T i)"
shows "(∑i∈S. sum (x i) (T i)) = (∑(i, j)∈Sigma S T. x i j)"
using assms
proof induct
case empty
then show ?case
by simp
next
case (insert a S)
show ?case
by (simp add: insert.hyps(1) insert.prems sum.Sigma)
qed
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 ‹Sundries›
text‹A transitive relation is well-founded if all initial segments are finite.›
lemma wf_finite_segments:
assumes "irrefl r" and "trans r" and "⋀x. finite {y. (y, x) ∈ r}"
shows "wf (r)"
apply (simp add: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
using acyclic_def assms irrefl_def trans_Restr by fastforce
text‹For creating values between \<^term>‹u› and \<^term>‹v›.›
lemma scaling_mono:
fixes u::"'a::linordered_field"
assumes "u ≤ v" "0 ≤ r" "r ≤ s"
shows "u + r * (v - u) / s ≤ v"
proof -
have "r/s ≤ 1" using assms
using divide_le_eq_1 by fastforce
then have "(r/s) * (v - u) ≤ 1 * (v - u)"
by (meson diff_ge_0_iff_ge mult_right_mono ‹u ≤ v›)
then show ?thesis
by (simp add: field_simps)
qed
subsection ‹Some useful lemmas about intervals›
lemma interior_subset_union_intervals:
assumes "i = cbox a b"
and "j = cbox c d"
and "interior j ≠ {}"
and "i ⊆ j ∪ S"
and "interior i ∩ interior j = {}"
shows "interior i ⊆ interior S"
proof -
have "box a b ∩ cbox c d = {}"
using Int_interval_mixed_eq_empty[of c d a b] assms
unfolding interior_cbox by auto
moreover
have "box a b ⊆ cbox c d ∪ S"
apply (rule order_trans,rule box_subset_cbox)
using assms by auto
ultimately
show ?thesis
unfolding assms interior_cbox
by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
qed
lemma interior_Union_subset_cbox:
assumes "finite f"
assumes f: "⋀s. s ∈ f ⟹ ∃a b. s = cbox a b" "⋀s. s ∈ f ⟹ interior s ⊆ t"
and t: "closed t"
shows "interior (⋃f) ⊆ t"
proof -
have [simp]: "s ∈ f ⟹ closed s" for s
using f by auto
define E where "E = {s∈f. interior s = {}}"
then have "finite E" "E ⊆ {s∈f. interior s = {}}"
using ‹finite f› by auto
then have "interior (⋃f) = interior (⋃(f - E))"
proof (induction E rule: finite_subset_induct')
case (insert s f')
have "interior (⋃(f - insert s f') ∪ s) = interior (⋃(f - insert s f'))"
using insert.hyps ‹finite f› by (intro interior_closed_Un_empty_interior) auto
also have "⋃(f - insert s f') ∪ s = ⋃(f - f')"
using insert.hyps by auto
finally show ?case
by (simp add: insert.IH)
qed simp
also have "… ⊆ ⋃(f - E)"
by (rule interior_subset)
also have "… ⊆ t"
proof (rule Union_least)
fix s assume "s ∈ f - E"
with f[of s] obtain a b where s: "s ∈ f" "s = cbox a b" "box a b ≠ {}"
by (fastforce simp: E_def)
have "closure (interior s) ⊆ closure t"
by (intro closure_mono f ‹s ∈ f›)
with s ‹closed t› show "s ⊆ t"
by simp
qed
finally show ?thesis .
qed
lemma Int_interior_Union_intervals:
"⟦finite ℱ; open S; ⋀T. T∈ℱ ⟹ ∃a b. T = cbox a b; ⋀T. T∈ℱ ⟹ S ∩ (interior T) = {}⟧
⟹ S ∩ interior (⋃ℱ) = {}"
using interior_Union_subset_cbox[of ℱ "UNIV - S"] by auto
lemma interval_split:
fixes a :: "'a::euclidean_space"
assumes "k ∈ Basis"
shows
"cbox a b ∩ {x. x∙k ≤ c} = cbox a (∑i∈Basis. (if i = k then min (b∙k) c else b∙i) *⇩R i)"
"cbox a b ∩ {x. x∙k ≥ c} = cbox (∑i∈Basis. (if i = k then max (a∙k) c else a∙i) *⇩R i) b"
using assms by (rule_tac set_eqI; auto simp: mem_box)+
lemma interval_not_empty: "∀i∈Basis. a∙i ≤ b∙i ⟹ cbox a b ≠ {}"
by (simp add: box_ne_empty)
subsection ‹Bounds on intervals where they exist›
definition interval_upperbound :: "('a::euclidean_space) set ⇒ 'a"
where "interval_upperbound s = (∑i∈Basis. (SUP x∈s. x∙i) *⇩R i)"
definition interval_lowerbound :: "('a::euclidean_space) set ⇒ 'a"
where "interval_lowerbound s = (∑i∈Basis. (INF x∈s. x∙i) *⇩R i)"
lemma interval_upperbound[simp]:
"∀i∈Basis. a∙i ≤ b∙i ⟹
interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
unfolding interval_upperbound_def euclidean_representation_sum cbox_def
by (safe intro!: cSup_eq) auto
lemma interval_lowerbound[simp]:
"∀i∈Basis. a∙i ≤ b∙i ⟹
interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
unfolding interval_lowerbound_def euclidean_representation_sum 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 ≠ {}"
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 ≠ {}" and "B ≠ {}"
shows "interval_upperbound (A × B) = (interval_upperbound A, interval_upperbound B)"
proof-
from assms have fst_image_times': "A = fst ` (A × B)" by simp
have "(∑i∈Basis. (SUP x∈A × B. x ∙ (i, 0)) *⇩R i) = (∑i∈Basis. (SUP x∈A. x ∙ i) *⇩R i)"
by (subst (2) fst_image_times') (simp del: fst_image_times add: image_comp inner_Pair_0)
moreover from assms have snd_image_times': "B = snd ` (A × B)" by simp
have "(∑i∈Basis. (SUP x∈A × B. x ∙ (0, i)) *⇩R i) = (∑i∈Basis. (SUP x∈B. x ∙ i) *⇩R i)"
by (subst (2) snd_image_times') (simp del: snd_image_times add: image_comp inner_Pair_0)
ultimately show ?thesis unfolding interval_upperbound_def
by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
qed
lemma interval_lowerbound_Times:
assumes "A ≠ {}" and "B ≠ {}"
shows "interval_lowerbound (A × B) = (interval_lowerbound A, interval_lowerbound B)"
proof-
from assms have fst_image_times': "A = fst ` (A × B)" by simp
have "(∑i∈Basis. (INF x∈A × B. x ∙ (i, 0)) *⇩R i) = (∑i∈Basis. (INF x∈A. x ∙ i) *⇩R i)"
by (subst (2) fst_image_times') (simp del: fst_image_times add: image_comp inner_Pair_0)
moreover from assms have snd_image_times': "B = snd ` (A × B)" by simp
have "(∑i∈Basis. (INF x∈A × B. x ∙ (0, i)) *⇩R i) = (∑i∈Basis. (INF x∈B. x ∙ i) *⇩R i)"
by (subst (2) snd_image_times') (simp del: snd_image_times add: image_comp inner_Pair_0)
ultimately show ?thesis unfolding interval_lowerbound_def
by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
qed
subsection ‹The notion of a gauge --- simply an open set containing the point›
definition "gauge γ ⟷ (∀x. x ∈ γ x ∧ open (γ x))"
lemma gaugeI:
assumes "⋀x. x ∈ γ x"
and "⋀x. open (γ x)"
shows "gauge γ"
using assms unfolding gauge_def by auto
lemma gaugeD[dest]:
assumes "gauge γ"
shows "x ∈ γ x"
and "open (γ x)"
using assms unfolding gauge_def by auto
lemma gauge_ball_dependent: "∀x. 0 < e x ⟹ gauge (λx. ball x (e x))"
unfolding gauge_def by auto
lemma gauge_ball[intro]: "0 < e ⟹ gauge (λx. ball x e)"
unfolding gauge_def by auto
lemma gauge_trivial[intro!]: "gauge (λx. ball x 1)"
by (rule gauge_ball) auto
lemma gauge_Int[intro]: "gauge γ1 ⟹ gauge γ2 ⟹ gauge (λx. γ1 x ∩ γ2 x)"
unfolding gauge_def by auto
lemma gauge_reflect:
fixes γ :: "'a::euclidean_space ⇒ 'a set"
shows "gauge γ ⟹ gauge (λx. uminus ` γ (- x))"
using equation_minus_iff
by (auto simp: gauge_def surj_def intro!: open_surjective_linear_image linear_uminus)
lemma gauge_Inter:
assumes "finite S"
and "⋀u. u∈S ⟹ gauge (f u)"
shows "gauge (λx. ⋂{f u x | u. u ∈ S})"
proof -
have *: "⋀x. {f u x |u. u ∈ S} = (λu. f u 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:
"(∀x. ∃d :: real. p x ⟶ 0 < d ∧ q d x) ⟷ (∀x. ∃d>0. p x ⟶ q d x)"
by (metis zero_less_one)
subsection ‹Attempt a systematic general set of "offset" results for components›
lemma gauge_modify:
assumes "(∀S. open S ⟶ open {x. f(x) ∈ S})" "gauge d"
shows "gauge (λx. {y. f y ∈ d (f x)})"
using assms unfolding gauge_def by force
subsection ‹Divisions›
definition division_of (infixl "division'_of" 40)
where
"s division_of i ⟷
finite s ∧
(∀K∈s. K ⊆ i ∧ K ≠ {} ∧ (∃a b. K = cbox a b)) ∧
(∀K1∈s. ∀K2∈s. K1 ≠ K2 ⟶ interior(K1) ∩ interior(K2) = {}) ∧
(⋃s = i)"
lemma division_ofD[dest]:
assumes "s division_of i"
shows "finite s"
and "⋀K. K ∈ s ⟹ K ⊆ i"
and "⋀K. K ∈ s ⟹ K ≠ {}"
and "⋀K. K ∈ s ⟹ ∃a b. K = cbox a b"
and "⋀K1 K2. K1 ∈ s ⟹ K2 ∈ s ⟹ K1 ≠ K2 ⟹ interior(K1) ∩ interior(K2) = {}"
and "⋃s = i"
using assms unfolding division_of_def by auto
lemma division_ofI:
assumes "finite s"
and "⋀K. K ∈ s ⟹ K ⊆ i"
and "⋀K. K ∈ s ⟹ K ≠ {}"
and "⋀K. K ∈ s ⟹ ∃a b. K = cbox a b"
and "⋀K1 K2. K1 ∈ s ⟹ K2 ∈ s ⟹ K1 ≠ K2 ⟹ interior K1 ∩ interior K2 = {}"
and "⋃s = i"
shows "s division_of i"
using assms unfolding division_of_def by auto
lemma division_of_finite: "s division_of i ⟹ finite s"
by auto
lemma division_of_self[intro]: "cbox a b ≠ {} ⟹ {cbox a b} division_of (cbox a b)"
unfolding division_of_def by auto
lemma division_of_trivial[simp]: "s division_of {} ⟷ s = {}"
unfolding division_of_def by auto
lemma division_of_sing[simp]:
"s division_of cbox a (a::'a::euclidean_space) ⟷ s = {cbox a a}"
(is "?l = ?r")
proof
assume ?r
moreover
{ fix K
assume "s = {{a}}" "K∈s"
then have "∃x y. K = cbox x y"
apply (rule_tac x=a in exI)+
apply force
done
}
ultimately show ?l
unfolding division_of_def cbox_sing by auto
next
assume ?l
have "x = {a}" if "x ∈ s" for x
by (metis ‹s division_of cbox a a› cbox_sing division_ofD(2) division_ofD(3) subset_singletonD that)
moreover have "s ≠ {}"
using ‹s division_of cbox a a› 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 ⟹ ∀x∈i. ∃k∈s. x ∈ k"
unfolding division_of_def by auto
lemma forall_in_division:
"d division_of i ⟹ (∀x∈d. P x) ⟷ (∀a b. cbox a b ∈ d ⟶ P (cbox a b))"
unfolding division_of_def by fastforce
lemma cbox_division_memE:
assumes 𝒟: "K ∈ 𝒟" "𝒟 division_of S"
obtains a b where "K = cbox a b" "K ≠ {}" "K ⊆ S"
using assms unfolding division_of_def by metis
lemma division_of_subset:
assumes "p division_of (⋃p)"
and "q ⊆ p"
shows "q division_of (⋃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 ∈ q"
then have kp: "k ∈ p"
using assms(2) by auto
show "k ⊆ ⋃q"
using ‹k ∈ q› by auto
show "∃a b. k = cbox a b"
using *(4)[OF kp] by auto
show "k ≠ {}"
using *(3)[OF kp] by auto
}
fix k1 k2
assume "k1 ∈ q" "k2 ∈ q" "k1 ≠ k2"
then have **: "k1 ∈ p" "k2 ∈ p" "k1 ≠ k2"
using assms(2) by auto
show "interior k1 ∩ interior k2 = {}"
using *(5)[OF **] by auto
qed auto
lemma division_of_union_self[intro]: "p division_of s ⟹ p division_of (⋃p)"
unfolding division_of_def by auto
lemma division_inter:
fixes s1 s2 :: "'a::euclidean_space set"
assumes "p1 division_of s1"
and "p2 division_of s2"
shows "{k1 ∩ k2 | k1 k2. k1 ∈ p1 ∧ k2 ∈ p2 ∧ k1 ∩ k2 ≠ {}} division_of (s1 ∩ s2)"
(is "?A' division_of _")
proof -
let ?A = "{s. s ∈ (λ(k1,k2). k1 ∩ k2) ` (p1 × p2) ∧ s ≠ {}}"
have *: "?A' = ?A" by auto
show ?thesis
unfolding *
proof (rule division_ofI)
have "?A ⊆ (λ(x, y). x ∩ y) ` (p1 × p2)"
by auto
moreover have "finite (p1 × p2)"
using assms unfolding division_of_def by auto
ultimately show "finite ?A" by auto
have *: "⋀s. ⋃{x∈s. x ≠ {}} = ⋃s"
by auto
show "⋃?A = s1 ∩ s2"
unfolding *
using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
{
fix k
assume "k ∈ ?A"
then obtain k1 k2 where k: "k = k1 ∩ k2" "k1 ∈ p1" "k2 ∈ p2" "k ≠ {}"
by auto
then show "k ≠ {}"
by auto
show "k ⊆ s1 ∩ 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 "∃a b. k = cbox a b"
unfolding k k1 k2 unfolding Int_interval by auto
}
fix k1 k2
assume "k1 ∈ ?A"
then obtain x1 y1 where k1: "k1 = x1 ∩ y1" "x1 ∈ p1" "y1 ∈ p2" "k1 ≠ {}"
by auto
assume "k2 ∈ ?A"
then obtain x2 y2 where k2: "k2 = x2 ∩ y2" "x2 ∈ p1" "y2 ∈ p2" "k2 ≠ {}"
by auto
assume "k1 ≠ k2"
then have th: "x1 ≠ x2 ∨ y1 ≠ y2"
unfolding k1 k2 by auto
have *: "interior x1 ∩ interior x2 = {} ∨ interior y1 ∩ interior y2 = {} ⟹
interior (x1 ∩ y1) ⊆ interior x1 ⟹ interior (x1 ∩ y1) ⊆ interior y1 ⟹
interior (x2 ∩ y2) ⊆ interior x2 ⟹ interior (x2 ∩ y2) ⊆ interior y2 ⟹
interior (x1 ∩ y1) ∩ interior (x2 ∩ y2) = {}" by auto
show "interior k1 ∩ 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) ⊆ i"
shows "{cbox a b ∩ k | k. k ∈ d ∧ cbox a b ∩ k ≠ {}} 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 ∩ 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_Int:
fixes s t :: "'a::euclidean_space set"
assumes "p1 division_of s"
and "p2 division_of t"
shows "∃p. p division_of (s ∩ t)"
using assms division_inter by blast
lemma elementary_Inter:
assumes "finite f"
and "f ≠ {}"
and "∀s∈f. ∃p. p division_of (s::('a::euclidean_space) set)"
shows "∃p. p division_of (⋂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 ⋂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_Int Inter_insert)
qed
qed auto
lemma division_disjoint_union:
assumes "p1 division_of s1"
and "p2 division_of s2"
and "interior s1 ∩ interior s2 = {}"
shows "(p1 ∪ p2) division_of (s1 ∪ s2)"
proof (rule division_ofI)
note d1 = division_ofD[OF assms(1)]
note d2 = division_ofD[OF assms(2)]
show "finite (p1 ∪ p2)"
using d1(1) d2(1) by auto
show "⋃(p1 ∪ p2) = s1 ∪ s2"
using d1(6) d2(6) by auto
{
fix k1 k2
assume as: "k1 ∈ p1 ∪ p2" "k2 ∈ p1 ∪ p2" "k1 ≠ k2"
moreover
let ?g="interior k1 ∩ interior k2 = {}"
{
assume as: "k1∈p1" "k2∈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∈p2" "k2∈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 ∈ p1 ∪ p2"
show "k ⊆ s1 ∪ s2"
using k d1(2) d2(2) by auto
show "k ≠ {}"
using k d1(3) d2(3) by auto
show "∃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 ⊆ cbox a b"
and nonempty: "cbox c d ≠ {}"
obtains p where "p division_of (cbox a b)" "cbox c d ∈ p"
proof
let ?B = "λf::'a⇒'a × 'a.
cbox (∑i∈Basis. (fst (f i) ∙ i) *⇩R i) (∑i∈Basis. (snd (f i) ∙ i) *⇩R i)"
define p where "p = ?B ` (Basis →⇩E {(a, c), (c, d), (d, b)})"
show "cbox c d ∈ p"
unfolding p_def
by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="λ(i::'a)∈Basis. (c, d)"])
have ord: "a ∙ i ≤ c ∙ i" "c ∙ i ≤ d ∙ i" "d ∙ i ≤ b ∙ i" if "i ∈ Basis" for i
using incl nonempty that
unfolding box_eq_empty subset_box by (auto simp: not_le)
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 ∈ p"
then obtain f where f: "f ∈ Basis →⇩E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
by (auto simp: p_def)
then show "∃a b. k = cbox a b"
by auto
have "k ⊆ cbox a b ∧ k ≠ {}"
proof (simp add: k box_eq_empty subset_box not_less, safe)
fix i :: 'a
assume i: "i ∈ Basis"
with f have "f i = (a, c) ∨ f i = (c, d) ∨ f i = (d, b)"
by (auto simp: PiE_iff)
with i ord[of i]
show "a ∙ i ≤ fst (f i) ∙ i" "snd (f i) ∙ i ≤ b ∙ i" "fst (f i) ∙ i ≤ snd (f i) ∙ i"
by auto
qed
then show "k ≠ {}" "k ⊆ cbox a b"
by auto
{
fix l
assume "l ∈ p"
then obtain g where g: "g ∈ Basis →⇩E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
by (auto simp: p_def)
assume "l ≠ k"
have "∃i∈Basis. f i ≠ g i"
proof (rule ccontr)
assume "¬ ?thesis"
with f g have "f = g"
by (auto simp: PiE_iff extensional_def fun_eq_iff)
with ‹l ≠ k› show False
by (simp add: l k)
qed
then obtain i where *: "i ∈ Basis" "f i ≠ g i" ..
then have "f i = (a, c) ∨ f i = (c, d) ∨ f i = (d, b)"
"g i = (a, c) ∨ g i = (c, d) ∨ g i = (d, b)"
using f g by (auto simp: PiE_iff)
with * ord[of i] show "interior l ∩ interior k = {}"
by (auto simp add: l k disjoint_interval intro!: bexI[of _ i])
}
note ‹k ⊆ cbox a b›
}
moreover
{
fix x assume x: "x ∈ cbox a b"
have "∀i∈Basis. ∃l. x ∙ i ∈ {fst l ∙ i .. snd l ∙ i} ∧ l ∈ {(a, c), (c, d), (d, b)}"
proof
fix i :: 'a
assume "i ∈ Basis"
with x ord[of i]
have "(a ∙ i ≤ x ∙ i ∧ x ∙ i ≤ c ∙ i) ∨ (c ∙ i ≤ x ∙ i ∧ x ∙ i ≤ d ∙ i) ∨
(d ∙ i ≤ x ∙ i ∧ x ∙ i ≤ b ∙ i)"
by (auto simp: cbox_def)
then show "∃l. x ∙ i ∈ {fst l ∙ i .. snd l ∙ i} ∧ l ∈ {(a, c), (c, d), (d, b)}"
by auto
qed
then obtain f where
f: "∀i∈Basis. x ∙ i ∈ {fst (f i) ∙ i..snd (f i) ∙ i} ∧ f i ∈ {(a, c), (c, d), (d, b)}"
unfolding bchoice_iff ..
moreover from f have "restrict f Basis ∈ Basis →⇩E {(a, c), (c, d), (d, b)}"
by auto
moreover from f have "x ∈ ?B (restrict f Basis)"
by (auto simp: mem_box)
ultimately have "∃k∈p. x ∈ k"
unfolding p_def by blast
}
ultimately show "⋃p = cbox a b"
by auto
qed
qed
proposition partial_division_extend_interval:
assumes "p division_of (⋃p)" "(⋃p) ⊆ cbox a b"
obtains q where "p ⊆ 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: "∀k∈p. ∃q. q division_of cbox a b ∧ k ∈ q"
proof
fix k
assume kp: "k ∈ p"
obtain c d where k: "k = cbox c d"
using p(4)[OF kp] by blast
have *: "cbox c d ⊆ cbox a b" "cbox c d ≠ {}"
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 ∈ q"
by (rule partial_division_extend_1[OF *])
then show "∃q. q division_of cbox a b ∧ k ∈ q"
unfolding k by auto
qed
obtain q where q: "⋀x. x ∈ p ⟹ q x division_of cbox a b" "⋀x. x ∈ p ⟹ x ∈ q x"
using bchoice[OF div_cbox] by blast
have "q x division_of ⋃(q x)" if x: "x ∈ p" for x
apply (rule division_ofI)
using division_ofD[OF q(1)[OF x]] by auto
then have di: "⋀x. x ∈ p ⟹ ∃d. d division_of ⋃(q x - {x})"
by (meson Diff_subset division_of_subset)
have "∃d. d division_of ⋂((λi. ⋃(q i - {i})) ` p)"
apply (rule elementary_Inter [OF finite_imageI[OF p(1)]])
apply (auto dest: di simp: False elementary_Inter [OF finite_imageI[OF p(1)]])
done
then obtain d where d: "d division_of ⋂((λi. ⋃(q i - {i})) ` p)" ..
have "d ∪ p division_of cbox a b"
proof -
have te: "⋀S f T. S ≠ {} ⟹ ∀i∈S. f i ∪ i = T ⟹ T = ⋂(f ` S) ∪ ⋃S" by auto
have cbox_eq: "cbox a b = ⋂((λi. ⋃(q i - {i})) ` p) ∪ ⋃p"
proof (rule te[OF False], clarify)
fix i
assume i: "i ∈ p"
show "⋃(q i - {i}) ∪ 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 ∈ p"
note qk=division_ofD[OF q(1)[OF K]]
have *: "⋀u T S. T ∩ S = {} ⟹ u ⊆ S ⟹ u ∩ T = {}"
by auto
have "interior (⋂i∈p. ⋃(q i - {i})) ∩ interior K = {}"
proof (rule *[OF Int_interior_Union_intervals])
show "⋀T. T∈q K - {K} ⟹ interior K ∩ interior T = {}"
using qk(5) using q(2)[OF K] by auto
show "interior (⋂i∈p. ⋃(q i - {i})) ⊆ interior (⋃(q K - {K}))"
apply (rule interior_mono)+
using K by auto
qed (use qk in auto)} note [simp] = this
show "d ∪ p division_of (cbox a b)"
unfolding cbox_eq
apply (rule division_disjoint_union[OF d assms(1)])
apply (rule Int_interior_Union_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 ⟹ bounded S"
unfolding division_of_def by (metis bounded_Union bounded_cbox)
lemma elementary_subset_cbox:
"p division_of S ⟹ ∃a b. S ⊆ cbox a (b::'a::euclidean_space)"
by (meson bounded_subset_cbox_symmetric elementary_bounded)
proposition division_union_intervals_exists:
fixes a b :: "'a::euclidean_space"
assumes "cbox a b ≠ {}"
obtains p where "(insert (cbox a b) p) division_of (cbox a b ∪ cbox c d)"
proof (cases "cbox c d = {}")
case True
with assms that show ?thesis by force
next
case False
show ?thesis
proof (cases "cbox a b ∩ 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 ∩ cbox c d = cbox u v"
unfolding Int_interval by auto
have uv_sub: "cbox u v ⊆ cbox c d" using uv by auto
obtain p where pd: "p division_of cbox c d" and "cbox u v ∈ p"
by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
note p = this division_ofD[OF pd]
have "interior (cbox a b ∩ ⋃(p - {cbox u v})) = interior(cbox u v ∩ ⋃(p - {cbox u v}))"
apply (rule arg_cong[of _ _ interior])
using p(8) uv by auto
also have "… = {}"
unfolding interior_Int
apply (rule Int_interior_Union_intervals)
using p(6) p(7)[OF p(2)] ‹finite p›
apply auto
done
finally have [simp]: "interior (cbox a b) ∩ interior (⋃(p - {cbox u v})) = {}" by simp
have cbe: "cbox a b ∪ cbox c d = cbox a b ∪ ⋃(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 ∪ ⋃(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 ∪ ⋃(p - {cbox u v})"
by (metis (no_types) Diff_subset ‹interior (cbox a b) ∩ interior (⋃(p - {cbox u v})) = {}› 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_Union:
assumes "finite f"
and "⋀p. p ∈ f ⟹ p division_of (⋃p)"
and "⋀k1 k2. k1 ∈ ⋃f ⟹ k2 ∈ ⋃f ⟹ k1 ≠ k2 ⟹ interior k1 ∩ interior k2 = {}"
shows "⋃f division_of ⋃(⋃f)"
using assms by (auto intro!: division_ofI)
lemma elementary_union_interval:
fixes a b :: "'a::euclidean_space"
assumes "p division_of ⋃p"
obtains q where "q division_of (cbox a b ∪ ⋃p)"
proof (cases "p = {} ∨ cbox a b = {}")
case True
obtain p where "p division_of (cbox a b)"
by (rule elementary_interval)
then show thesis
using True assms that by auto
next
case False
then have "p ≠ {}" "cbox a b ≠ {}"
by auto
note pdiv = division_ofD[OF assms]
show ?thesis
proof (cases "interior (cbox a b) = {}")
case True
show ?thesis
apply (rule that [of "insert (cbox a b) p", OF division_ofI])
using pdiv(1-4) True False apply auto
apply (metis IntI equals0D pdiv(5))
by (metis disjoint_iff_not_equal pdiv(5))
next
case False
have "∀K∈p. ∃q. (insert (cbox a b) q) division_of (cbox a b ∪ K)"
proof
fix K
assume kp: "K ∈ p"
from pdiv(4)[OF kp] obtain c d where "K = cbox c d" by blast
then show "∃q. (insert (cbox a b) q) division_of (cbox a b ∪ K)"
by (meson ‹cbox a b ≠ {}› division_union_intervals_exists)
qed
from bchoice[OF this] obtain q where "∀x∈p. insert (cbox a b) (q x) division_of (cbox a b) ∪ x" ..
note q = division_ofD[OF this[rule_format]]
let ?D = "⋃{insert (cbox a b) (q K) | K. K ∈ p}"
show thesis
proof (rule that[OF division_ofI])
have *: "{insert (cbox a b) (q K) |K. K ∈ p} = (λK. insert (cbox a b) (q K)) ` p"
by auto
show "finite ?D"
using "*" pdiv(1) q(1) by auto
have "⋃?D = (⋃x∈p. ⋃(insert (cbox a b) (q x)))"
by auto
also have "... = ⋃{cbox a b ∪ t |t. t ∈ p}"
using q(6) by auto
also have "... = cbox a b ∪ ⋃p"
using ‹p ≠ {}› by auto
finally show "⋃?D = cbox a b ∪ ⋃p" .
show "K ⊆ cbox a b ∪ ⋃p" "K ≠ {}" if "K ∈ ?D" for K
using q that by blast+
show "∃a b. K = cbox a b" if "K ∈ ?D" for K
using q(4) that by auto
next
fix K' K
assume K: "K ∈ ?D" and K': "K' ∈ ?D" "K ≠ K'"
obtain x where x: "K ∈ insert (cbox a b) (q x)" "x∈p"
using K by auto
obtain x' where x': "K'∈insert (cbox a b) (q x')" "x'∈p"
using K' by auto
show "interior K ∩ interior K' = {}"
proof (cases "x = x' ∨ K = cbox a b ∨ K' = cbox a b")
case True
then show ?thesis
using True K' q(5) x' x by auto
next
case False
then have as': "K ≠ cbox a b" "K' ≠ cbox a b"
by auto
obtain c d where K: "K = cbox c d"
using q(4) x by blast
have "interior K ∩ interior (cbox a b) = {}"
using as' K'(2) q(5) x by blast
then have "interior K ⊆ interior x"
by (metis ‹interior (cbox a b) ≠ {}› 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' ∩ interior (cbox a b) = {}"
using as'(2) q(5) x' by blast
then have "interior K' ⊆ interior x'"
by (metis ‹interior (cbox a b) ≠ {}› c_d interior_subset_union_intervals q(2) x'(1) x'(2))
moreover have "interior x ∩ interior x' = {}"
by (meson False assms division_ofD(5) x'(2) x(2))
ultimately show ?thesis
using ‹interior K ⊆ interior x› ‹interior K' ⊆ interior x'› by auto
qed
qed
qed
qed
lemma elementary_unions_intervals:
assumes fin: "finite f"
and "⋀s. s ∈ f ⟹ ∃a b. s = cbox a (b::'a::euclidean_space)"
obtains p where "p division_of (⋃f)"
proof -
have "∃p. p division_of (⋃f)"
proof (induct_tac f rule:finite_subset_induct)
show "∃p. p division_of ⋃{}" using elementary_empty by auto
next
fix x F
assume as: "finite F" "x ∉ F" "∃p. p division_of ⋃F" "x∈f"
from this(3) obtain p where p: "p division_of ⋃F" ..
from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
have *: "⋃F = ⋃p"
using division_ofD[OF p] by auto
show "∃p. p division_of ⋃(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 ∪ T)"
proof -
have *: "S ∪ T = ⋃ps ∪ ⋃pt"
using assms unfolding division_of_def by auto
show ?thesis
apply (rule elementary_unions_intervals[of "ps ∪ 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 ⊆ T"
obtains r where "p ⊆ 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 ⊆ cbox a b"
using elementary_subset_cbox[OF assms(2)] by auto
obtain r1 where "p ⊆ 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 ⋃(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 (⋃(r1 - p)) ∩ (⋃q)"
by (metis assms(2) divq(6) elementary_Int)
{
fix x
assume x: "x ∈ T" "x ∉ S"
then obtain R where r: "R ∈ r1" "x ∈ R"
unfolding r1 using ab
by (meson division_contains r1(2) subsetCE)
moreover have "R ∉ p"
proof
assume "R ∈ p"
then have "x ∈ S" using divp(2) r by auto
then show False using x by auto
qed
ultimately have "x∈⋃(r1 - p)" by auto
}
then have Teq: "T = ⋃p ∪ (⋃(r1 - p) ∩ ⋃q)"
unfolding divp divq using assms(3) by auto
have "interior S ∩ interior (⋃(r1-p)) = {}"
proof (rule Int_interior_Union_intervals)
have *: "⋀S. (⋀x. x ∈ S ⟹ False) ⟹ S = {}"
by auto
show "interior S ∩ interior m = {}" if "m ∈ r1 - p" for m
proof -
have "interior m ∩ interior (⋃p) = {}"
proof (rule Int_interior_Union_intervals)
show "⋀T. T∈p ⟹ interior m ∩ interior T = {}"
by (metis DiffD1 DiffD2 that r1(1) r1(7) rev_subsetD)
qed (use divp in auto)
then show "interior S ∩ interior m = {}"
unfolding divp by auto
qed
qed (use r1 in auto)
then have "interior S ∩ interior (⋃(r1-p) ∩ (⋃q)) = {}"
using interior_subset by auto
then have div: "p ∪ r2 division_of ⋃p ∪ ⋃(r1 - p) ∩ ⋃q"
by (simp add: assms(1) division_disjoint_union divp(6) r2)
show ?thesis
apply (rule that[of "p ∪ r2"])
apply (auto simp: div Teq)
done
qed
lemma division_split:
fixes a :: "'a::euclidean_space"
assumes "p division_of (cbox a b)"
and k: "k∈Basis"
shows "{l ∩ {x. x∙k ≤ c} | l. l ∈ p ∧ l ∩ {x. x∙k ≤ c} ≠ {}} division_of(cbox a b ∩ {x. x∙k ≤ c})"
(is "?p1 division_of ?I1")
and "{l ∩ {x. x∙k ≥ c} | l. l ∈ p ∧ l ∩ {x. x∙k ≥ c} ≠ {}} division_of (cbox a b ∩ {x. x∙k ≥ c})"
(is "?p2 division_of ?I2")
proof (rule_tac[!] division_ofI)
note p = division_ofD[OF assms(1)]
show "finite ?p1" "finite ?p2"
using p(1) by auto
show "⋃?p1 = ?I1" "⋃?p2 = ?I2"
unfolding p(6)[symmetric] by auto
{
fix K
assume "K ∈ ?p1"
then obtain l where l: "K = l ∩ {x. x ∙ k ≤ c}" "l ∈ p" "l ∩ {x. x ∙ k ≤ c} ≠ {}"
by blast
obtain u v where uv: "l = cbox u v"
using assms(1) l(2) by blast
show "K ⊆ ?I1"
using l p(2) uv by force
show "K ≠ {}"
by (simp add: l)
show "∃a b. K = cbox a b"
apply (simp add: l uv p(2-3)[OF l(2)])
apply (subst interval_split[OF k])
apply (auto intro: order.trans)
done
fix K'
assume "K' ∈ ?p1"
then obtain l' where l': "K' = l' ∩ {x. x ∙ k ≤ c}" "l' ∈ p" "l' ∩ {x. x ∙ k ≤ c} ≠ {}"
by blast
assume "K ≠ K'"
then show "interior K ∩ interior K' = {}"
unfolding l l' using p(5)[OF l(2) l'(2)] by auto
}
{
fix K
assume "K ∈ ?p2"
then obtain l where l: "K = l ∩ {x. c ≤ x ∙ k}" "l ∈ p" "l ∩ {x. c ≤ x ∙ k} ≠ {}"
by blast
obtain u v where uv: "l = cbox u v"
using l(2) p(4) by blast
show "K ⊆ ?I2"
using l p(2) uv by force
show "K ≠ {}"
by (simp add: l)
show "∃a b. K = cbox a b"
apply (simp add: l uv p(2-3)[OF l(2)])
apply (subst interval_split[OF k])
apply (auto intro: order.trans)
done
fix K'
assume "K' ∈ ?p2"
then obtain l' where l': "K' = l' ∩ {x. c ≤ x ∙ k}" "l' ∈ p" "l' ∩ {x. c ≤ x ∙ k} ≠ {}"
by blast
assume "K ≠ K'"
then show "interior K ∩ interior K' = {}"
unfolding l l' using p(5)[OF l(2) l'(2)] by auto
}
qed
subsection ‹Tagged (partial) divisions›
definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
where "s tagged_partial_division_of i ⟷
finite s ∧
(∀x K. (x, K) ∈ s ⟶ x ∈ K ∧ K ⊆ i ∧ (∃a b. K = cbox a b)) ∧
(∀x1 K1 x2 K2. (x1, K1) ∈ s ∧ (x2, K2) ∈ s ∧ (x1, K1) ≠ (x2, K2) ⟶
interior K1 ∩ interior K2 = {})"
lemma tagged_partial_division_ofD:
assumes "s tagged_partial_division_of i"
shows "finite s"
and "⋀x K. (x,K) ∈ s ⟹ x ∈ K"
and "⋀x K. (x,K) ∈ s ⟹ K ⊆ i"
and "⋀x K. (x,K) ∈ s ⟹ ∃a b. K = cbox a b"
and "⋀x1 K1 x2 K2. (x1,K1) ∈ s ⟹
(x2, K2) ∈ s ⟹ (x1, K1) ≠ (x2, K2) ⟹ interior K1 ∩ 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 ⟷ s tagged_partial_division_of i ∧ (⋃{K. ∃x. (x,K) ∈ s} = i)"
lemma tagged_division_of_finite: "s tagged_division_of i ⟹ finite s"
unfolding tagged_division_of_def tagged_partial_division_of_def by auto
lemma tagged_division_of:
"s tagged_division_of i ⟷
finite s ∧
(∀x K. (x, K) ∈ s ⟶ x ∈ K ∧ K ⊆ i ∧ (∃a b. K = cbox a b)) ∧
(∀x1 K1 x2 K2. (x1, K1) ∈ s ∧ (x2, K2) ∈ s ∧ (x1, K1) ≠ (x2, K2) ⟶
interior K1 ∩ interior K2 = {}) ∧
(⋃{K. ∃x. (x,K) ∈ s} = i)"
unfolding tagged_division_of_def tagged_partial_division_of_def by auto
lemma tagged_division_ofI:
assumes "finite s"
and "⋀x K. (x,K) ∈ s ⟹ x ∈ K"
and "⋀x K. (x,K) ∈ s ⟹ K ⊆ i"
and "⋀x K. (x,K) ∈ s ⟹ ∃a b. K = cbox a b"
and "⋀x1 K1 x2 K2. (x1,K1) ∈ s ⟹ (x2, K2) ∈ s ⟹ (x1, K1) ≠ (x2, K2) ⟹
interior K1 ∩ interior K2 = {}"
and "(⋃{K. ∃x. (x,K) ∈ s} = i)"
shows "s tagged_division_of i"
unfolding tagged_division_of
using assms by fastforce
lemma tagged_division_ofD[dest]:
assumes "s tagged_division_of i"
shows "finite s"
and "⋀x K. (x,K) ∈ s ⟹ x ∈ K"
and "⋀x K. (x,K) ∈ s ⟹ K ⊆ i"
and "⋀x K. (x,K) ∈ s ⟹ ∃a b. K = cbox a b"
and "⋀x1 K1 x2 K2. (x1, K1) ∈ s ⟹ (x2, K2) ∈ s ⟹ (x1, K1) ≠ (x2, K2) ⟹
interior K1 ∩ interior K2 = {}"
and "(⋃{K. ∃x. (x,K) ∈ 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 "⋃(snd ` s) = i" "finite (snd ` s)"
using assm by auto
fix k
assume k: "k ∈ snd ` s"
then obtain xk where xk: "(xk, k) ∈ s"
by auto
then show "k ⊆ i" "k ≠ {}" "∃a b. k = cbox a b"
using assm by fastforce+
fix k'
assume k': "k' ∈ snd ` s" "k ≠ k'"
from this(1) obtain xk' where xk': "(xk', k') ∈ s"
by auto
then show "interior k ∩ 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 ⋃(snd ` s)"
proof (rule division_ofI)
note assm = tagged_partial_division_ofD[OF assms]
show "finite (snd ` s)" "⋃(snd ` s) = ⋃(snd ` s)"
using assm by auto
fix k
assume k: "k ∈ snd ` s"
then obtain xk where xk: "(xk, k) ∈ s"
by auto
then show "k ≠ {}" "∃a b. k = cbox a b" "k ⊆ ⋃(snd ` s)"
using assm by auto
fix k'
assume k': "k' ∈ snd ` s" "k ≠ k'"
from this(1) obtain xk' where xk': "(xk', k') ∈ s"
by auto
then show "interior k ∩ 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 ⊆ s"
shows "t tagged_partial_division_of i"
using assms finite_subset[OF assms(2)]
unfolding tagged_partial_division_of_def
by blast
lemma tag_in_interval: "p tagged_division_of i ⟹ (x, k) ∈ p ⟹ x ∈ 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 {} ⟷ p = {}"
unfolding tagged_partial_division_of_def by auto
lemma tagged_division_of_trivial[simp]: "p tagged_division_of {} ⟷ p = {}"
unfolding tagged_division_of by auto
lemma tagged_division_of_self: "x ∈ cbox a b ⟹ {(x,cbox a b)} tagged_division_of (cbox a b)"
by (rule tagged_division_ofI) auto
lemma tagged_division_of_self_real: "x ∈ {a .. b::real} ⟹ {(x,{a .. b})} tagged_division_of {a .. b}"
unfolding box_real[symmetric]
by (rule tagged_division_of_self)
lemma tagged_division_Un:
assumes "p1 tagged_division_of s1"
and "p2 tagged_division_of s2"
and "interior s1 ∩ interior s2 = {}"
shows "(p1 ∪ p2) tagged_division_of (s1 ∪ 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 ∪ p2)"
using p1(1) p2(1) by auto
show "⋃{k. ∃x. (x, k) ∈ p1 ∪ p2} = s1 ∪ s2"
using p1(6) p2(6) by blast
fix x k
assume xk: "(x, k) ∈ p1 ∪ p2"
show "x ∈ k" "∃a b. k = cbox a b"
using xk p1(2,4) p2(2,4) by auto
show "k ⊆ s1 ∪ s2"
using xk p1(3) p2(3) by blast
fix x' k'
assume xk': "(x', k') ∈ p1 ∪ p2" "(x, k) ≠ (x', k')"
have *: "⋀a b. a ⊆ s1 ⟹ b ⊆ s2 ⟹ interior a ∩ interior b = {}"
using assms(3) interior_mono by blast
show "interior k ∩ interior k' = {}"
apply (cases "(x, k) ∈ 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_Union:
assumes "finite I"
and tag: "⋀i. i∈I ⟹ pfn i tagged_division_of i"
and disj: "⋀i1 i2. ⟦i1 ∈ I; i2 ∈ I; i1 ≠ i2⟧ ⟹ interior(i1) ∩ interior(i2) = {}"
shows "⋃(pfn ` I) tagged_division_of (⋃I)"
proof (rule tagged_division_ofI)
note assm = tagged_division_ofD[OF tag]
show "finite (⋃(pfn ` I))"
using assms by auto
have "⋃{k. ∃x. (x, k) ∈ ⋃(pfn ` I)} = ⋃((λi. ⋃{k. ∃x. (x, k) ∈ pfn i}) ` I)"
by blast
also have "… = ⋃I"
using assm(6) by auto
finally show "⋃{k. ∃x. (x, k) ∈ ⋃(pfn ` I)} = ⋃I" .
fix x k
assume xk: "(x, k) ∈ ⋃(pfn ` I)"
then obtain i where i: "i ∈ I" "(x, k) ∈ pfn i"
by auto
show "x ∈ k" "∃a b. k = cbox a b" "k ⊆ ⋃I"
using assm(2-4)[OF i] using i(1) by auto
fix x' k'
assume xk': "(x', k') ∈ ⋃(pfn ` I)" "(x, k) ≠ (x', k')"
then obtain i' where i': "i' ∈ I" "(x', k') ∈ pfn i'"
by auto
have *: "⋀a b. i ≠ i' ⟹ a ⊆ i ⟹ b ⊆ i' ⟹ interior a ∩ interior b = {}"
using i(1) i'(1) disj interior_mono by blast
show "interior k ∩ interior k' = {}"
proof (cases "i = i'")
case True then show ?thesis
using assm(5) i' i xk'(2) by blast
next
case False then show ?thesis
using "*" assm(3) i' i by auto
qed
qed
lemma tagged_partial_division_of_Union_self:
assumes "p tagged_partial_division_of s"
shows "p tagged_division_of (⋃(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 (⋃(snd ` p))"
apply (rule tagged_division_ofI)
using tagged_division_ofD[OF assms]
apply auto
done
lemma tagged_division_Un_interval:
fixes a :: "'a::euclidean_space"
assumes "p1 tagged_division_of (cbox a b ∩ {x. x∙k ≤ (c::real)})"
and "p2 tagged_division_of (cbox a b ∩ {x. x∙k ≥ c})"
and k: "k ∈ Basis"
shows "(p1 ∪ p2) tagged_division_of (cbox a b)"
proof -
have *: "cbox a b = (cbox a b ∩ {x. x∙k ≤ c}) ∪ (cbox a b ∩ {x. x∙k ≥ c})"
by auto
show ?thesis
apply (subst *)
apply (rule tagged_division_Un[OF assms(1-2)])
unfolding interval_split[OF k] interior_cbox
using k
apply (auto simp add: box_def elim!: ballE[where x=k])
done
qed
lemma tagged_division_Un_interval_real:
fixes a :: real
assumes "p1 tagged_division_of ({a .. b} ∩ {x. x∙k ≤ (c::real)})"
and "p2 tagged_division_of ({a .. b} ∩ {x. x∙k ≥ c})"
and k: "k ∈ Basis"
shows "(p1 ∪ p2) tagged_division_of {a .. b}"
using assms
unfolding box_real[symmetric]
by (rule tagged_division_Un_interval)
lemma tagged_division_split_left_inj:
assumes d: "d tagged_division_of i"
and tags: "(x1, K1) ∈ d" "(x2, K2) ∈ d"
and "K1 ≠ K2"
and eq: "K1 ∩ {x. x ∙ k ≤ c} = K2 ∩ {x. x ∙ k ≤ c}"
shows "interior (K1 ∩ {x. x∙k ≤ c}) = {}"
proof -
have "interior (K1 ∩ K2) = {} ∨ (x2, K2) = (x1, K1)"
using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
then show ?thesis
using eq ‹K1 ≠ K2› by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
qed
lemma tagged_division_split_right_inj:
assumes d: "d tagged_division_of i"
and tags: "(x1, K1) ∈ d" "(x2, K2) ∈ d"
and "K1 ≠ K2"
and eq: "K1 ∩ {x. x∙k ≥ c} = K2 ∩ {x. x∙k ≥ c}"
shows "interior (K1 ∩ {x. x∙k ≥ c}) = {}"
proof -
have "interior (K1 ∩ K2) = {} ∨ (x2, K2) = (x1, K1)"
using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
then show ?thesis
using eq ‹K1 ≠ K2› by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
qed
lemma (in comm_monoid_set) over_tagged_division_lemma:
assumes "p tagged_division_of i"
and "⋀u v. box u v = {} ⟹ d (cbox u v) = ❙1"
shows "F (λ(_, k). d k) p = F d (snd ` p)"
proof -
have *: "(λ(_ ,k). d k) = d ∘ snd"
by (simp add: fun_eq_iff)
note assm = tagged_division_ofD[OF assms(1)]
show ?thesis
unfolding *
proof (rule reindex_nontrivial[symmetric])
show "finite p"
using assm by auto
fix x y
assume "x∈p" "y∈p" "x≠y" "snd x = snd y"
obtain a b where ab: "snd x = cbox a b"
using assm(4)[of "fst x" "snd x"] ‹x∈p› by auto
have "(fst x, snd y) ∈ p" "(fst x, snd y) ≠ y"
using ‹x ∈ p› ‹x ≠ y› ‹snd x = snd y› [symmetric] by auto
with ‹x∈p› ‹y∈p› have "interior (snd x) ∩ interior (snd y) = {}"
by (intro assm(5)[of "fst x" _ "fst y"]) auto
then have "box a b = {}"
unfolding ‹snd x = snd y›[symmetric] ab by auto
then have "d (cbox a b) = ❙1"
using assm(2)[of "fst x" "snd x"] ‹x∈p› ab[symmetric] by (intro assms(2)) auto
then show "d (snd x) = ❙1"
unfolding ab by auto
qed
qed
subsection ‹Functions closed on boxes: morphisms from boxes to monoids›
text ‹This auxiliary structure is used to sum up over the elements of a division. Main theorem is
‹operative_division›. Instances for the monoid are \<^typ>‹'a option›, \<^typ>‹real›, and
\<^typ>‹bool›.›
paragraph ‹Using additivity of lifted function to encode definedness.›
text ‹%whitespace›
definition lift_option :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a option ⇒ 'b option ⇒ 'c option"
where
"lift_option f a' b' = Option.bind a' (λa. Option.bind b' (λb. Some (f a b)))"
lemma lift_option_simps[simp]:
"lift_option f (Some a) (Some b) = Some (f a b)"
"lift_option f None b' = None"
"lift_option f a' None = None"
by (auto simp: lift_option_def)
lemma comm_monoid_lift_option:
assumes "comm_monoid f z"
shows "comm_monoid (lift_option f) (Some z)"
proof -
from assms interpret comm_monoid f z .
show ?thesis
by standard (auto simp: lift_option_def ac_simps split: bind_split)
qed
lemma comm_monoid_and: "comm_monoid HOL.conj True"
by standard auto
lemma comm_monoid_set_and: "comm_monoid_set HOL.conj True"
by (rule comm_monoid_set.intro) (fact comm_monoid_and)
paragraph ‹Misc›
lemma interval_real_split:
"{a .. b::real} ∩ {x. x ≤ c} = {a .. min b c}"
"{a .. b} ∩ {x. c ≤ x} = {max a c .. b}"
apply (metis Int_atLeastAtMostL1 atMost_def)
apply (metis Int_atLeastAtMostL2 atLeast_def)
done
lemma bgauge_existence_lemma: "(∀x∈s. ∃d::real. 0 < d ∧ q d x) ⟷ (∀x. ∃d>0. x∈s ⟶ q d x)"
by (meson zero_less_one)
paragraph ‹Division points›
text ‹%whitespace›
definition "division_points (k::('a::euclidean_space) set) d =
{(j,x). j ∈ Basis ∧ (interval_lowerbound k)∙j < x ∧ x < (interval_upperbound k)∙j ∧
(∃i∈d. (interval_lowerbound i)∙j = x ∨ (interval_upperbound i)∙j = x)}"
lemma division_points_finite:
fixes i :: "'a::euclidean_space set"
assumes "d division_of i"
shows "finite (division_points i d)"
proof -
note assm = division_ofD[OF assms]
let ?M = "λj. {(j,x)|x. (interval_lowerbound i)∙j < x ∧ x < (interval_upperbound i)∙j ∧
(∃i∈d. (interval_lowerbound i)∙j = x ∨ (interval_upperbound i)∙j = x)}"
have *: "division_points i d = ⋃(?M ` Basis)"
unfolding division_points_def by auto
show ?thesis
unfolding * using assm by auto
qed
lemma division_points_subset:
fixes a :: "'a::euclidean_space"
assumes "d division_of (cbox a b)"
and "∀i∈Basis. a∙i < b∙i" "a∙k < c" "c < b∙k"
and k: "k ∈ Basis"
shows "division_points (cbox a b ∩ {x. x∙k ≤ c}) {l ∩ {x. x∙k ≤ c} | l . l ∈ d ∧ l ∩ {x. x∙k ≤ c} ≠ {}} ⊆
division_points (cbox a b) d" (is ?t1)
and "division_points (cbox a b ∩ {x. x∙k ≥ c}) {l ∩ {x. x∙k ≥ c} | l . l ∈ d ∧ ¬(l ∩ {x. x∙k ≥ c} = {})} ⊆
division_points (cbox a b) d" (is ?t2)
proof -
note assm = division_ofD[OF assms(1)]
have *: "∀i∈Basis. a∙i ≤ b∙i"
"∀i∈Basis. a∙i ≤ (∑i∈Basis. (if i = k then min (b ∙ k) c else b ∙ i) *⇩R i) ∙ i"
"∀i∈Basis. (∑i∈Basis. (if i = k then max (a ∙ k) c else a ∙ i) *⇩R i) ∙ i ≤ b∙i"
"min (b ∙ k) c = c" "max (a ∙ k) c = c"
using assms using less_imp_le by auto
have "∃i∈d. interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
if "a ∙ x < y" "y < (if x = k then c else b ∙ x)"
"interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
"i = l ∩ {x. x ∙ k ≤ c}" "l ∈ d" "l ∩ {x. x ∙ k ≤ c} ≠ {}"
"x ∈ Basis" for i l x y
proof -
obtain u v where l: "l = cbox u v"
using ‹l ∈ d› assms(1) by blast
have *: "∀i∈Basis. u ∙ i ≤ (∑i∈Basis. (if i = k then min (v ∙ k) c else v ∙ i) *⇩R i) ∙ i"
using that(6) unfolding l interval_split[OF k] box_ne_empty that .
have **: "∀i∈Basis. u∙i ≤ v∙i"
using l using that(6) unfolding box_ne_empty[symmetric] by auto
show ?thesis
apply (rule bexI[OF _ ‹l ∈ d›])
using that(1-3,5) ‹x ∈ Basis›
unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] that
apply (auto split: if_split_asm)
done
qed
moreover have "⋀x y. ⟦y < (if x = k then c else b ∙ x)⟧ ⟹ y < b ∙ x"
using ‹c < b∙k› by (auto split: if_split_asm)
ultimately show ?t1
unfolding division_points_def interval_split[OF k, of a b]
unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
unfolding * by force
have "⋀x y i l. (if x = k then c else a ∙ x) < y ⟹ a ∙ x < y"
using ‹a∙k < c› by (auto split: if_split_asm)
moreover have "∃i∈d. interval_lowerbound i ∙ x = y ∨
interval_upperbound i ∙ x = y"
if "(if x = k then c else a ∙ x) < y" "y < b ∙ x"
"interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
"i = l ∩ {x. c ≤ x ∙ k}" "l ∈ d" "l ∩ {x. c ≤ x ∙ k} ≠ {}"
"x ∈ Basis" for x y i l
proof -
obtain u v where l: "l = cbox u v"
using ‹l ∈ d› assm(4) by blast
have *: "∀i∈Basis. (∑i∈Basis. (if i = k then max (u ∙ k) c else u ∙ i) *⇩R i) ∙ i ≤ v ∙ i"
using that(6) unfolding l interval_split[OF k] box_ne_empty that .
have **: "∀i∈Basis. u∙i ≤ v∙i"
using l using that(6) unfolding box_ne_empty[symmetric] by auto
show "∃i∈d. interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
apply (rule bexI[OF _ ‹l ∈ d›])
using that(1-3,5) ‹x ∈ Basis›
unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] that
apply (auto split: if_split_asm)
done
qed
ultimately show ?t2
unfolding division_points_def interval_split[OF k, of a b]
unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
unfolding *
by force
qed
lemma division_points_psubset:
fixes a :: "'a::euclidean_space"
assumes d: "d division_of (cbox a b)"
and altb: "∀i∈Basis. a∙i < b∙i" "a∙k < c" "c < b∙k"
and "l ∈ d"
and disj: "interval_lowerbound l∙k = c ∨ interval_upperbound l∙k = c"
and k: "k ∈ Basis"
shows "division_points (cbox a b ∩ {x. x∙k ≤ c}) {l ∩ {x. x∙k ≤ c} | l. l∈d ∧ l ∩ {x. x∙k ≤ c} ≠ {}} ⊂
division_points (cbox a b) d" (is "?D1 ⊂ ?D")
and "division_points (cbox a b ∩ {x. x∙k ≥ c}) {l ∩ {x. x∙k ≥ c} | l. l∈d ∧ l ∩ {x. x∙k ≥ c} ≠ {}} ⊂
division_points (cbox a b) d" (is "?D2 ⊂ ?D")
proof -
have ab: "∀i∈Basis. a∙i ≤ b∙i"
using altb by (auto intro!:less_imp_le)
obtain u v where l: "l = cbox u v"
using d ‹l ∈ d› by blast
have uv: "∀i∈Basis. u∙i ≤ v∙i" "∀i∈Basis. a∙i ≤ u∙i ∧ v∙i ≤ b∙i"
apply (metis assms(5) box_ne_empty(1) cbox_division_memE d l)
by (metis assms(5) box_ne_empty(1) cbox_division_memE d l subset_box(1))
have *: "interval_upperbound (cbox a b ∩ {x. x ∙ k ≤ interval_upperbound l ∙ k}) ∙ k = interval_upperbound l ∙ k"
"interval_upperbound (cbox a b ∩ {x. x ∙ k ≤ interval_lowerbound l ∙ k}) ∙ k = interval_lowerbound l ∙ k"
unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
using uv[rule_format, of k] ab k
by auto
have "∃x. x ∈ ?D - ?D1"
using assms(3-)
unfolding division_points_def interval_bounds[OF ab]
by (force simp add: *)
moreover have "?D1 ⊆ ?D"
by (auto simp add: assms division_points_subset)
ultimately show "?D1 ⊂ ?D"
by blast
have *: "interval_lowerbound (cbox a b ∩ {x. x ∙ k ≥ interval_lowerbound l ∙ k}) ∙ k = interval_lowerbound l ∙ k"
"interval_lowerbound (cbox a b ∩ {x. x ∙ k ≥ interval_upperbound l ∙ k}) ∙ k = interval_upperbound l ∙ k"
unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
using uv[rule_format, of k] ab k
by auto
have "∃x. x ∈ ?D - ?D2"
using assms(3-)
unfolding division_points_def interval_bounds[OF ab]
by (force simp add: *)
moreover have "?D2 ⊆ ?D"
by (auto simp add: assms division_points_subset)
ultimately show "?D2 ⊂ ?D"
by blast
qed
lemma division_split_left_inj:
fixes S :: "'a::euclidean_space set"
assumes div: "𝒟 division_of S"
and eq: "K1 ∩ {x::'a. x∙k ≤ c} = K2 ∩ {x. x∙k ≤ c}"
and "K1 ∈ 𝒟" "K2 ∈ 𝒟" "K1 ≠ K2"
shows "interior (K1 ∩ {x. x∙k ≤ c}) = {}"
proof -
have "interior K2 ∩ interior {a. a ∙ k ≤ c} = interior K1 ∩ interior {a. a ∙ k ≤ c}"
by (metis (no_types) eq interior_Int)
moreover have "⋀A. interior A ∩ interior K2 = {} ∨ A = K2 ∨ A ∉ 𝒟"
by (meson div ‹K2 ∈ 𝒟› division_of_def)
ultimately show ?thesis
using ‹K1 ∈ 𝒟› ‹K1 ≠ K2› by auto
qed
lemma division_split_right_inj:
fixes S :: "'a::euclidean_space set"
assumes div: "𝒟 division_of S"
and eq: "K1 ∩ {x::'a. x∙k ≥ c} = K2 ∩ {x. x∙k ≥ c}"
and "K1 ∈ 𝒟" "K2 ∈ 𝒟" "K1 ≠ K2"
shows "interior (K1 ∩ {x. x∙k ≥ c}) = {}"
proof -
have "interior K2 ∩ interior {a. a ∙ k ≥ c} = interior K1 ∩ interior {a. a ∙ k ≥ c}"
by (metis (no_types) eq interior_Int)
moreover have "⋀A. interior A ∩ interior K2 = {} ∨ A = K2 ∨ A ∉ 𝒟"
by (meson div ‹K2 ∈ 𝒟› division_of_def)
ultimately show ?thesis
using ‹K1 ∈ 𝒟› ‹K1 ≠ K2› by auto
qed
lemma interval_doublesplit:
fixes a :: "'a::euclidean_space"
assumes "k ∈ Basis"
shows "cbox a b ∩ {x . ¦x∙k - c¦ ≤ (e::real)} =
cbox (∑i∈Basis. (if i = k then max (a∙k) (c - e) else a∙i) *⇩R i)
(∑i∈Basis. (if i = k then min (b∙k) (c + e) else b∙i) *⇩R i)"
proof -
have *: "⋀x c e::real. ¦x - c¦ ≤ e ⟷ x ≥ c - e ∧ x ≤ c + e"
by auto
have **: "⋀s P Q. s ∩ {x. P x ∧ Q x} = (s ∩ {x. Q x}) ∩ {x. P x}"
by blast
show ?thesis
unfolding * ** interval_split[OF assms] by (rule refl)
qed
lemma division_doublesplit:
fixes a :: "'a::euclidean_space"
assumes "p division_of (cbox a b)"
and k: "k ∈ Basis"
shows "(λl. l ∩ {x. ¦x∙k - c¦ ≤ e}) ` {l∈p. l ∩ {x. ¦x∙k - c¦ ≤ e} ≠ {}}
division_of (cbox a b ∩ {x. ¦x∙k - c¦ ≤ e})"
proof -
have *: "⋀x c. ¦x - c¦ ≤ e ⟷ x ≥ c - e ∧ x ≤ c + e"
by auto
have **: "⋀p q p' q'. p division_of q ⟹ p = p' ⟹ q = q' ⟹ p' division_of q'"
by auto
note division_split(1)[OF assms, where c="c+e",unfolded interval_split[OF k]]
note division_split(2)[OF this, where c="c-e" and k=k,OF k]
then show ?thesis
apply (rule **)
subgoal
apply (simp add: abs_diff_le_iff field_simps Collect_conj_eq setcompr_eq_image [symmetric] cong: image_cong_simp)
apply (rule equalityI)
apply blast
apply clarsimp
apply (rule_tac x="xa ∩ {x. c + e ≥ x ∙ k}" in exI)
apply auto
done
by (simp add: interval_split k interval_doublesplit)
qed
paragraph ‹Operative›
locale operative = comm_monoid_set +
fixes g :: "'b::euclidean_space set ⇒ 'a"
assumes box_empty_imp: "⋀a b. box a b = {} ⟹ g (cbox a b) = ❙1"
and Basis_imp: "⋀a b c k. k ∈ Basis ⟹ g (cbox a b) = g (cbox a b ∩ {x. x∙k ≤ c}) ❙* g (cbox a b ∩ {x. x∙k ≥ c})"
begin
lemma empty [simp]:
"g {} = ❙1"
proof -
have *: "cbox One (-One) = ({}::'b set)"
by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
moreover have "box One (-One) = ({}::'b set)"
using box_subset_cbox[of One "-One"] by (auto simp: *)
ultimately show ?thesis
using box_empty_imp [of One "-One"] by simp
qed
lemma division:
"F g d = g (cbox a b)" if "d division_of (cbox a b)"
proof -
define C where [abs_def]: "C = card (division_points (cbox a b) d)"
then show ?thesis
using that proof (induction C arbitrary: a b d rule: less_induct)
case (less a b d)
show ?case
proof cases
assume "box a b = {}"
{ fix k assume "k∈d"
then obtain a' b' where k: "k = cbox a' b'"
using division_ofD(4)[OF less.prems] by blast
with ‹k∈d› division_ofD(2)[OF less.prems] have "cbox a' b' ⊆ cbox a b"
by auto
then have "box a' b' ⊆ box a b"
unfolding subset_box by auto
then have "g k = ❙1"
using box_empty_imp [of a' b'] k by (simp add: ‹box a b = {}›) }
then show "box a b = {} ⟹ F g d = g (cbox a b)"
by (auto intro!: neutral simp: box_empty_imp)
next
assume "box a b ≠ {}"
then have ab: "∀i∈Basis. a∙i < b∙i" and ab': "∀i∈Basis. a∙i ≤ b∙i"
by (auto simp: box_ne_empty)
show "F g d = g (cbox a b)"
proof (cases "division_points (cbox a b) d = {}")
case True
{ fix u v and j :: 'b
assume j: "j ∈ Basis" and as: "cbox u v ∈ d"
then have "cbox u v ≠ {}"
using less.prems by blast
then have uv: "∀i∈Basis. u∙i ≤ v∙i" "u∙j ≤ v∙j"
using j unfolding box_ne_empty by auto
have *: "⋀p r Q. ¬ j∈Basis ∨ p ∨ r ∨ (∀x∈d. Q x) ⟹ p ∨ r ∨ Q (cbox u v)"
using as j by auto
have "(j, u∙j) ∉ division_points (cbox a b) d"
"(j, v∙j) ∉ division_points (cbox a b) d" using True by auto
note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
moreover
have "a∙j ≤ u∙j" "v∙j ≤ b∙j"
using division_ofD(2,2,3)[OF ‹d division_of cbox a b› as]
apply (metis j subset_box(1) uv(1))
by (metis ‹cbox u v ⊆ cbox a b› j subset_box(1) uv(1))
ultimately have "u∙j = a∙j ∧ v∙j = a∙j ∨ u∙j = b∙j ∧ v∙j = b∙j ∨ u∙j = a∙j ∧ v∙j = b∙j"
unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
then have d': "∀i∈d. ∃u v. i = cbox u v ∧
(∀j∈Basis. u∙j = a∙j ∧ v∙j = a∙j ∨ u∙j = b∙j ∧ v∙j = b∙j ∨ u∙j = a∙j ∧ v∙j = b∙j)"
unfolding forall_in_division[OF less.prems] by blast
have "(1/2) *⇩R (a+b) ∈ cbox a b"
unfolding mem_box using ab by (auto simp: inner_simps)
note this[unfolded division_ofD(6)[OF ‹d division_of cbox a b›,symmetric] Union_iff]
then obtain i where i: "i ∈ d" "(1 / 2) *⇩R (a + b) ∈ i" ..
obtain u v where uv: "i = cbox u v"
"∀j∈Basis. u ∙ j = a ∙ j ∧ v ∙ j = a ∙ j ∨
u ∙ j = b ∙ j ∧ v ∙ j = b ∙ j ∨
u ∙ j = a ∙ j ∧ v ∙ j = b ∙ j"
using d' i(1) by auto
have "cbox a b ∈ d"
proof -
have "u = a" "v = b"
unfolding euclidean_eq_iff[where 'a='b]
proof safe
fix j :: 'b
assume j: "j ∈ Basis"
note i(2)[unfolded uv mem_box,rule_format,of j]
then show "u ∙ j = a ∙ j" and "v ∙ j = b ∙ j"
using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
qed
then have "i = cbox a b" using uv by auto
then show ?thesis using i by auto
qed
then have deq: "d = insert (cbox a b) (d - {cbox a b})"
by auto
have "F g (d - {cbox a b}) = ❙1"
proof (intro neutral ballI)
fix x
assume x: "x ∈ d - {cbox a b}"
then have "x∈d"
by auto note d'[rule_format,OF this]
then obtain u v where uv: "x = cbox u v"
"∀j∈Basis. u ∙ j = a ∙ j ∧ v ∙ j = a ∙ j ∨
u ∙ j = b ∙ j ∧ v ∙ j = b ∙ j ∨
u ∙ j = a ∙ j ∧ v ∙ j = b ∙ j"
by blast
have "u ≠ a ∨ v ≠ b"
using x[unfolded uv] by auto
then obtain j where "u∙j ≠ a∙j ∨ v∙j ≠ b∙j" and j: "j ∈ Basis"
unfolding euclidean_eq_iff[where 'a='b] by auto
then have "u∙j = v∙j"
using uv(2)[rule_format,OF j] by auto
then have "box u v = {}"
using j unfolding box_eq_empty by (auto intro!: bexI[of _ j])
then show "g x = ❙1"
unfolding uv(1) by (rule box_empty_imp)
qed
then show "F g d = g (cbox a b)"
using division_ofD[OF less.prems]
apply (subst deq)
apply (subst insert)
apply auto
done
next
case False
then have "∃x. x ∈ division_points (cbox a b) d"
by auto
then obtain k c
where "k ∈ Basis" "interval_lowerbound (cbox a b) ∙ k < c"
"c < interval_upperbound (cbox a b) ∙ k"
"∃i∈d. interval_lowerbound i ∙ k = c ∨ interval_upperbound i ∙ k = c"
unfolding division_points_def by auto
then obtain j where "a ∙ k < c" "c < b ∙ k"
and "j ∈ d" and j: "interval_lowerbound j ∙ k = c ∨ interval_upperbound j ∙ k = c"
by (metis division_of_trivial empty_iff interval_bounds' less.prems)
let ?lec = "{x. x∙k ≤ c}" let ?gec = "{x. x∙k ≥ c}"
define d1 where "d1 = {l ∩ ?lec | l. l ∈ d ∧ l ∩ ?lec ≠ {}}"
define d2 where "d2 = {l ∩ ?gec | l. l ∈ d ∧ l ∩ ?gec ≠ {}}"
define cb where "cb = (∑i∈Basis. (if i = k then c else b∙i) *⇩R i)"
define ca where "ca = (∑i∈Basis. (if i = k then c else a∙i) *⇩R i)"
have "division_points (cbox a b ∩ ?lec) {l ∩ ?lec |l. l ∈ d ∧ l ∩ ?lec ≠ {}}
⊂ division_points (cbox a b) d"
by (rule division_points_psubset[OF ‹d division_of cbox a b› ab ‹a ∙ k < c› ‹c < b ∙ k› ‹j ∈ d› j ‹k ∈ Basis›])
with division_points_finite[OF ‹d division_of cbox a b›]
have "card
(division_points (cbox a b ∩ ?lec) {l ∩ ?lec |l. l ∈ d ∧ l ∩ ?lec ≠ {}})
< card (division_points (cbox a b) d)"
by (rule psubset_card_mono)
moreover have "division_points (cbox a b ∩ {x. c ≤ x ∙ k}) {l ∩ {x. c ≤ x ∙ k} |l. l ∈ d ∧ l ∩ {x. c ≤ x ∙ k} ≠ {}}
⊂ division_points (cbox a b) d"
by (rule division_points_psubset[OF ‹d division_of cbox a b› ab ‹a ∙ k < c› ‹c < b ∙ k› ‹j ∈ d› j ‹k ∈ Basis›])
with division_points_finite[OF ‹d division_of cbox a b›]
have "card (division_points (cbox a b ∩ ?gec) {l ∩ ?gec |l. l ∈ d ∧ l ∩ ?gec ≠ {}})
< card (division_points (cbox a b) d)"
by (rule psubset_card_mono)
ultimately have *: "F g d1 = g (cbox a b ∩ ?lec)" "F g d2 = g (cbox a b ∩ ?gec)"
unfolding interval_split[OF ‹k ∈ Basis›]
apply (rule_tac[!] less.hyps)
using division_split[OF ‹d division_of cbox a b›, where k=k and c=c] ‹k ∈ Basis›
by (simp_all add: interval_split d1_def d2_def division_points_finite[OF ‹d division_of cbox a b›])
have fxk_le: "g (l ∩ ?lec) = ❙1"
if "l ∈ d" "y ∈ d" "l ∩ ?lec = y ∩ ?lec" "l ≠ y" for l y
proof -
obtain u v where leq: "l = cbox u v"
using ‹l ∈ d› less.prems by auto
have "interior (cbox u v ∩ ?lec) = {}"
using that division_split_left_inj leq less.prems by blast
then show ?thesis
unfolding leq interval_split [OF ‹k ∈ Basis›]
by (auto intro: box_empty_imp)
qed
have fxk_ge: "g (l ∩ {x. x ∙ k ≥ c}) = ❙1"
if "l ∈ d" "y ∈ d" "l ∩ ?gec = y ∩ ?gec" "l ≠ y" for l y
proof -
obtain u v where leq: "l = cbox u v"
using ‹l ∈ d› less.prems by auto
have "interior (cbox u v ∩ ?gec) = {}"
using that division_split_right_inj leq less.prems by blast
then show ?thesis
unfolding leq interval_split[OF ‹k ∈ Basis›]
by (auto intro: box_empty_imp)
qed
have d1_alt: "d1 = (λl. l ∩ ?lec) ` {l ∈ d. l ∩ ?lec ≠ {}}"
using d1_def by auto
have d2_alt: "d2 = (λl. l ∩ ?gec) ` {l ∈ d. l ∩ ?gec ≠ {}}"
using d2_def by auto
have "g (cbox a b) = F g d1 ❙* F g d2" (is "_ = ?prev")
unfolding * using ‹k ∈ Basis›
by (auto dest: Basis_imp)
also have "F g d1 = F (λl. g (l ∩ ?lec)) d"
unfolding d1_alt using division_of_finite[OF less.prems] fxk_le
by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
also have "F g d2 = F (λl. g (l ∩ ?gec)) d"
unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge
by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
also have *: "∀x∈d. g x = g (x ∩ ?lec) ❙* g (x ∩ ?gec)"
unfolding forall_in_division[OF ‹d division_of cbox a b›]
using ‹k ∈ Basis›
by (auto dest: Basis_imp)
have "F (λl. g (l ∩ ?lec)) d ❙* F (λl. g (l ∩ ?gec)) d = F g d"
using * by (simp add: distrib)
finally show ?thesis by auto
qed
qed
qed
qed
proposition tagged_division:
assumes "d tagged_division_of (cbox a b)"
shows "F (λ(_, l). g l) d = g (cbox a b)"
proof -
have "F (λ(_, k). g k) d = F g (snd ` d)"
using assms box_empty_imp by (rule over_tagged_division_lemma)
then show ?thesis
unfolding assms [THEN division_of_tagged_division, THEN division] .
qed
end
locale operative_real = comm_monoid_set +
fixes g :: "real set ⇒ 'a"
assumes neutral: "b ≤ a ⟹ g {a..b} = ❙1"
assumes coalesce_less: "a < c ⟹ c < b ⟹ g {a..c} ❙* g {c..b} = g {a..b}"
begin
sublocale operative where g = g
rewrites "box = (greaterThanLessThan :: real ⇒ _)"
and "cbox = (atLeastAtMost :: real ⇒ _)"
and "⋀x::real. x ∈ Basis ⟷ x = 1"
proof -
show "operative f z g"
proof
show "g (cbox a b) = ❙1" if "box a b = {}" for a b
using that by (simp add: neutral)
show "g (cbox a b) = g (cbox a b ∩ {x. x ∙ k ≤ c}) ❙* g (cbox a b ∩ {x. c ≤ x ∙ k})"
if "k ∈ Basis" for a b c k
proof -
from that have [simp]: "k = 1"
by simp
from neutral [of 0 1] neutral [of a a for a] coalesce_less
have [simp]: "g {} = ❙1" "⋀a. g {a} = ❙1"
"⋀a b c. a < c ⟹ c < b ⟹ g {a..c} ❙* g {c..b} = g {a..b}"
by auto
have "g {a..b} = g {a..min b c} ❙* g {max a c..b}"
by (auto simp: min_def max_def le_less)
then show "g (cbox a b) = g (cbox a b ∩ {x. x ∙ k ≤ c}) ❙* g (cbox a b ∩ {x. c ≤ x ∙ k})"
by (simp add: atMost_def [symmetric] atLeast_def [symmetric])
qed
qed
show "box = (greaterThanLessThan :: real ⇒ _)"
and "cbox = (atLeastAtMost :: real ⇒ _)"
and "⋀x::real. x ∈ Basis ⟷ x = 1"
by (simp_all add: fun_eq_iff)
qed
lemma coalesce_less_eq:
"g {a..c} ❙* g {c..b} = g {a..b}" if "a ≤ c" "c ≤ b"
proof (cases "c = a ∨ c = b")
case False
with that have "a < c" "c < b"
by auto
then show ?thesis
by (rule coalesce_less)
next
case True
with that box_empty_imp [of a a] box_empty_imp [of b b] show ?thesis
by safe simp_all
qed
end
lemma operative_realI:
"operative_real f z g" if "operative f z g"
proof -
interpret operative f z g
using that .
show ?thesis
proof
show "g {a..b} = z" if "b ≤ a" for a b
using that box_empty_imp by simp
show "f (g {a..c}) (g {c..b}) = g {a..b}" if "a < c" "c < b" for a b c
using that
using Basis_imp [of 1 a b c]
by (simp_all add: atMost_def [symmetric] atLeast_def [symmetric] max_def min_def)
qed
qed
subsection ‹Special case of additivity we need for the FTC›
lemma additive_tagged_division_1:
fixes f :: "real ⇒ 'a::real_normed_vector"
assumes "a ≤ b"
and "p tagged_division_of {a..b}"
shows "sum (λ(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
proof -
let ?f = "(λk::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
interpret operative_real plus 0 ?f
rewrites "comm_monoid_set.F (+) 0 = sum"
by standard[1] (auto simp add: sum_def)
have p_td: "p tagged_division_of cbox a b"
using assms(2) box_real(2) by presburger
have **: "cbox a b ≠ {}"
using assms(1) by auto
then have "f b - f a = (∑(x, l)∈p. if l = {} then 0 else f (interval_upperbound l) - f (interval_lowerbound l))"
proof -
have "(if cbox a b = {} then 0 else f (interval_upperbound (cbox a b)) - f (interval_lowerbound (cbox a b))) = f b - f a"
using assms by auto
then show ?thesis
using p_td assms by (simp add: tagged_division)
qed
then show ?thesis
using assms by (auto intro!: sum.cong)
qed
subsection ‹Fine-ness of a partition w.r.t. a gauge›
definition fine (infixr "fine" 46)
where "d fine s ⟷ (∀(x,k) ∈ s. k ⊆ d x)"
lemma fineI:
assumes "⋀x k. (x, k) ∈ s ⟹ k ⊆ d x"
shows "d fine s"
using assms unfolding fine_def by auto
lemma fineD[dest]:
assumes "d fine s"
shows "⋀x k. (x,k) ∈ s ⟹ k ⊆ d x"
using assms unfolding fine_def by auto
lemma fine_Int: "(λx. d1 x ∩ d2 x) fine p ⟷ d1 fine p ∧ d2 fine p"
unfolding fine_def by auto
lemma fine_Inter:
"(λx. ⋂{f d x | d. d ∈ s}) fine p ⟷ (∀d∈s. (f d) fine p)"
unfolding fine_def by blast
lemma fine_Un: "d fine p1 ⟹ d fine p2 ⟹ d fine (p1 ∪ p2)"
unfolding fine_def by blast
lemma fine_Union: "(⋀p. p ∈ ps ⟹ d fine p) ⟹ d fine (⋃ps)"
unfolding fine_def by auto
lemma fine_subset: "p ⊆ q ⟹ d fine q ⟹ d fine p"
unfolding fine_def by blast
subsection ‹Some basic combining lemmas›
lemma tagged_division_Union_exists:
assumes "finite I"
and "∀i∈I. ∃p. p tagged_division_of i ∧ d fine p"
and "∀i1∈I. ∀i2∈I. i1 ≠ i2 ⟶ interior i1 ∩ interior i2 = {}"
and "⋃I = i"
obtains p where "p tagged_division_of i" and "d fine p"
proof -
obtain pfn where pfn:
"⋀x. x ∈ I ⟹ pfn x tagged_division_of x"
"⋀x. x ∈ I ⟹ d fine pfn x"
using bchoice[OF assms(2)] by auto
show thesis
apply (rule_tac p="⋃(pfn ` I)" in that)
using assms(1) assms(3) assms(4) pfn(1) tagged_division_Union apply force
by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
qed
subsection ‹The set we're concerned with must be closed›
lemma division_of_closed:
fixes i :: "'n::euclidean_space set"
shows "s division_of i ⟹ closed i"
unfolding division_of_def by fastforce
subsection ‹General bisection principle for intervals; might be useful elsewhere›
lemma interval_bisection_step:
fixes type :: "'a::euclidean_space"
assumes emp: "P {}"
and Un: "⋀S T. ⟦P S; P T; interior(S) ∩ interior(T) = {}⟧ ⟹ P (S ∪ T)"
and non: "¬ P (cbox a (b::'a))"
obtains c d where "¬ P (cbox c d)"
and "⋀i. i ∈ Basis ⟹ a∙i ≤ c∙i ∧ c∙i ≤ d∙i ∧ d∙i ≤ b∙i ∧ 2 * (d∙i - c∙i) ≤ b∙i - a∙i"
proof -
have "cbox a b ≠ {}"
using emp non by metis
then have ab: "⋀i. i∈Basis ⟹ a ∙ i ≤ b ∙ i"
by (force simp: mem_box)
have UN_cases: "⟦finite ℱ;
⋀S. S∈ℱ ⟹ P S;
⋀S. S∈ℱ ⟹ ∃a b. S = cbox a b;
⋀S T. S∈ℱ ⟹ T∈ℱ ⟹ S ≠ T ⟹ interior S ∩ interior T = {}⟧ ⟹ P (⋃ℱ)" for ℱ
proof (induct ℱ rule: finite_induct)
case empty show ?case
using emp by auto
next
case (insert x f)
then show ?case
unfolding Union_insert by (metis Int_interior_Union_intervals Un insert_iff open_interior)
qed
let ?ab = "λi. (a∙i + b∙i) / 2"
let ?A = "{cbox c d | c d::'a. ∀i∈Basis. (c∙i = a∙i) ∧ (d∙i = ?ab i) ∨
(c∙i = ?ab i) ∧ (d∙i = b∙i)}"
have "P (⋃?A)"
if "⋀c d. ∀i∈Basis. a∙i ≤ c∙i ∧ c∙i ≤ d∙i ∧ d∙i ≤ b∙i ∧ 2 * (d∙i - c∙i) ≤ b∙i - a∙i ⟹ P (cbox c d)"
proof (rule UN_cases)
let ?B = "(λS. cbox (∑i∈Basis. (if i ∈ S then a∙i else ?ab i) *⇩R i::'a)
(∑i∈Basis. (if i ∈ S then ?ab i else b∙i) *⇩R i)) ` {s. s ⊆ Basis}"
have "?A ⊆ ?B"
proof
fix x
assume "x ∈ ?A"
then obtain c d
where x: "x = cbox c d"
"⋀i. i ∈ Basis ⟹
c ∙ i = a ∙ i ∧ d ∙ i = ?ab i ∨ c ∙ i = ?ab i ∧ d ∙ i = b ∙ i"
by blast
have "c = (∑i∈Basis. (if c ∙ i = a ∙ i then a ∙ i else ?ab i) *⇩R i)"
"d = (∑i∈Basis. (if c ∙ i = a ∙ i then ?ab i else b ∙ i) *⇩R i)"
using x(2) ab by (fastforce simp add: euclidean_eq_iff[where 'a='a])+
then show "x ∈ ?B"
unfolding x by (rule_tac x="{i. i∈Basis ∧ c∙i = a∙i}" in image_eqI) auto
qed
then show "finite ?A"
by (rule finite_subset) auto
next
fix S
assume "S ∈ ?A"
then obtain c d
where s: "S = cbox c d"
"⋀i. i ∈ Basis ⟹ c ∙ i = a ∙ i ∧ d ∙ i = ?ab i ∨ c ∙ i = ?ab i ∧ d ∙ i = b ∙ i"
by blast
show "P S"
unfolding s using ab s(2) by (fastforce intro!: that)
show "∃a b. S = cbox a b"
unfolding s by auto
fix T
assume "T ∈ ?A"
then obtain e f where t:
"T = cbox e f"
"⋀i. i ∈ Basis ⟹ e ∙ i = a ∙ i ∧ f ∙ i = ?ab i ∨ e ∙ i = ?ab i ∧ f ∙ i = b ∙ i"
by blast
assume "S ≠ T"
then have "¬ (c = e ∧ d = f)"
unfolding s t by auto
then obtain i where "c∙i ≠ e∙i ∨ d∙i ≠ f∙i" and i': "i ∈ Basis"
unfolding euclidean_eq_iff[where 'a='a] by auto
then have i: "c∙i ≠ e∙i" "d∙i ≠ f∙i"
using s(2) t(2) apply fastforce
using t(2)[OF i'] ‹c ∙ i ≠ e ∙ i ∨ d ∙ i ≠ f ∙ i› i' s(2) t(2) by fastforce
have *: "⋀s t. (⋀a. a ∈ s ⟹ a ∈ t ⟹ False) ⟹ s ∩ t = {}"
by auto
show "interior S ∩ interior T = {}"
unfolding s t interior_cbox
proof (rule *)
fix x
assume "x ∈ box c d" "x ∈ box e f"
then have x: "c∙i < d∙i" "e∙i < f∙i" "c∙i < f∙i" "e∙i < d∙i"
unfolding mem_box using i' by force+
show False using s(2)[OF i'] t(2)[OF i'] and i x
by auto
qed
qed
also have "⋃?A = cbox a b"
proof (rule set_eqI,rule)
fix x
assume "x ∈ ⋃?A"
then obtain c d where x:
"x ∈ cbox c d"
"⋀i. i ∈ Basis ⟹ c ∙ i = a ∙ i ∧ d ∙ i = ?ab i ∨ c ∙ i = ?ab i ∧ d ∙ i = b ∙ i"
by blast
then show "x∈cbox a b"
unfolding mem_box by force
next
fix x
assume x: "x ∈ cbox a b"
then have "∀i∈Basis. ∃c d. (c = a∙i ∧ d = ?ab i ∨ c = ?ab i ∧ d = b∙i) ∧ c≤x∙i ∧ x∙i ≤ d"
(is "∀i∈Basis. ∃c d. ?P i c d")
unfolding mem_box by (metis linear)
then obtain α β where "∀i∈Basis. (α ∙ i = a ∙ i ∧ β ∙ i = ?ab i ∨
α ∙ i = ?ab i ∧ β ∙ i = b ∙ i) ∧ α ∙ i ≤ x ∙ i ∧ x ∙ i ≤ β ∙ i"
by (auto simp: choice_Basis_iff)
then show "x∈⋃?A"
by (force simp add: mem_box)
qed
finally show thesis
by (metis (no_types, lifting) assms(3) that)
qed
lemma interval_bisection:
fixes type :: "'a::euclidean_space"
assumes "P {}"
and Un: "⋀S T. ⟦P S; P T; interior(S) ∩ interior(T) = {}⟧ ⟹ P (S ∪ T)"
and "¬ P (cbox a (b::'a))"
obtains x where "x ∈ cbox a b"
and "∀e>0. ∃c d. x ∈ cbox c d ∧ cbox c d ⊆ ball x e ∧ cbox c d ⊆ cbox a b ∧ ¬ P (cbox c d)"
proof -
have "∀x. ∃y. ¬ P (cbox (fst x) (snd x)) ⟶ (¬ P (cbox (fst y) (snd y)) ∧
(∀i∈Basis. fst x∙i ≤ fst y∙i ∧ fst y∙i ≤ snd y∙i ∧ snd y∙i ≤ snd x∙i ∧
2 * (snd y∙i - fst y∙i) ≤ snd x∙i - fst x∙i))" (is "∀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 False
obtain c d where "¬ P (cbox c d)"
"⋀i. i ∈ Basis ⟹
fst x ∙ i ≤ c ∙ i ∧
c ∙ i ≤ d ∙ i ∧
d ∙ i ≤ snd x ∙ i ∧
2 * (d ∙ i - c ∙ i) ≤ snd x ∙ i - fst x ∙ i"
by (blast intro: interval_bisection_step[of P, OF assms(1-2) False])
then show ?thesis
by (rule_tac x="(c,d)" in exI) auto
qed
qed
then obtain f where f:
"∀x.
¬ P (cbox (fst x) (snd x)) ⟶
¬ P (cbox (fst (f x)) (snd (f x))) ∧
(∀i∈Basis.
fst x ∙ i ≤ fst (f x) ∙ i ∧
fst (f x) ∙ i ≤ snd (f x) ∙ i ∧
snd (f x) ∙ i ≤ snd x ∙ i ∧
2 * (snd (f x) ∙ i - fst (f x) ∙ i) ≤ snd x ∙ i - fst x ∙ i)" by metis
define AB A B where ab_def: "AB n = (f ^^ n) (a,b)" "A n = fst(AB n)" "B n = snd(AB n)" for n
have [simp]: "A 0 = a" "B 0 = b" and ABRAW: "⋀n. ¬ P (cbox (A(Suc n)) (B(Suc n))) ∧
(∀i∈Basis. A(n)∙i ≤ A(Suc n)∙i ∧ A(Suc n)∙i ≤ B(Suc n)∙i ∧ B(Suc n)∙i ≤ B(n)∙i ∧
2 * (B(Suc n)∙i - A(Suc n)∙i) ≤ B(n)∙i - A(n)∙i)" (is "⋀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 using ‹¬ P (cbox a b)› f by auto
next
case (Suc n)
show ?case
unfolding S
apply (rule f[rule_format])
using Suc
unfolding S
apply auto
done
qed
qed
then have AB: "A(n)∙i ≤ A(Suc n)∙i" "A(Suc n)∙i ≤ B(Suc n)∙i"
"B(Suc n)∙i ≤ B(n)∙i" "2 * (B(Suc n)∙i - A(Suc n)∙i) ≤ B(n)∙i - A(n)∙i"
if "i∈Basis" for i n
using that by blast+
have notPAB: "¬ P (cbox (A(Suc n)) (B(Suc n)))" for n
using ABRAW by blast
have interv: "∃n. ∀x∈cbox (A n) (B n). ∀y∈cbox (A n) (B n). dist x y < e"
if e: "0 < e" for e
proof -
obtain n where n: "(∑i∈Basis. b ∙ i - a ∙ i) / e < 2 ^ n"
using real_arch_pow[of 2 "(sum (λi. b∙i - a∙i) Basis) / e"] by auto
show ?thesis
proof (rule exI [where x=n], clarify)
fix x y
assume xy: "x∈cbox (A n) (B n)" "y∈cbox (A n) (B n)"
have "dist x y ≤ sum (λi. ¦(x - y)∙i¦) Basis"
unfolding dist_norm by(rule norm_le_l1)
also have "… ≤ sum (λi. B n∙i - A n∙i) Basis"
proof (rule sum_mono)
fix i :: 'a
assume i: "i ∈ Basis"
show "¦(x - y) ∙ i¦ ≤ B n ∙ i - A n ∙ i"
using xy[unfolded mem_box,THEN bspec, OF i]
by (auto simp: inner_diff_left)
qed
also have "… ≤ sum (λi. b∙i - a∙i) Basis / 2^n"
unfolding sum_divide_distrib
proof (rule sum_mono)
show "B n ∙ i - A n ∙ i ≤ (b ∙ i - a ∙ i) / 2 ^ n" if i: "i ∈ Basis" for i
proof (induct n)
case 0
then show ?case
unfolding AB by auto
next
case (Suc n)
have "B (Suc n) ∙ i - A (Suc n) ∙ i ≤ (B n ∙ i - A n ∙ i) / 2"
using AB(3) that AB(4)[of i n] using i by auto
also have "… ≤ (b ∙ i - a ∙ i) / 2 ^ Suc n"
using Suc by (auto simp add: field_simps)
finally show ?case .
qed
qed
also have "… < e"
using n using e by (auto simp add: field_simps)
finally show "dist x y < e" .
qed
qed
{
fix n m :: nat
assume "m ≤ n" then have "cbox (A n) (B n) ⊆ cbox (A m) (B m)"
proof (induction rule: inc_induct)
case (step i)
show ?case
using AB by (intro order_trans[OF step.IH] subset_box_imp) auto
qed simp
} note ABsubset = this
have "⋀n. cbox (A n) (B n) ≠ {}"
by (meson AB dual_order.trans interval_not_empty)
then obtain x0 where x0: "⋀n. x0 ∈ cbox (A n) (B n)"
using decreasing_closed_nest [OF closed_cbox] ABsubset interv by blast
show thesis
proof (rule that[rule_format, of x0])
show "x0∈cbox a b"
using ‹A 0 = a› ‹B 0 = b› x0 by blast
fix e :: real
assume "e > 0"
from interv[OF this] obtain n
where n: "∀x∈cbox (A n) (B n). ∀y∈cbox (A n) (B n). dist x y < e" ..
have "¬ P (cbox (A n) (B n))"
proof (cases "0 < n")
case True then show ?thesis
by (metis Suc_pred' notPAB)
next
case False then show ?thesis
using ‹A 0 = a› ‹B 0 = b› ‹¬ P (cbox a b)› by blast
qed
moreover have "cbox (A n) (B n) ⊆ ball x0 e"
using n using x0[of n] by auto
moreover have "cbox (A n) (B n) ⊆ cbox a b"
using ABsubset ‹A 0 = a› ‹B 0 = b› by blast
ultimately show "∃c d. x0 ∈ cbox c d ∧ cbox c d ⊆ ball x0 e ∧ cbox c d ⊆ cbox a b ∧ ¬ P (cbox c d)"
apply (rule_tac x="A n" in exI)
apply (rule_tac x="B n" in exI)
apply (auto simp: x0)
done
qed
qed
subsection ‹Cousin's lemma›
lemma fine_division_exists:
fixes a b :: "'a::euclidean_space"
assumes "gauge g"
obtains p where "p tagged_division_of (cbox a b)" "g fine p"
proof (cases "∃p. p tagged_division_of (cbox a b) ∧ g fine p")
case True
then show ?thesis
using that by auto
next
case False
assume "¬ (∃p. p tagged_division_of (cbox a b) ∧ g fine p)"
obtain x where x:
"x ∈ (cbox a b)"
"⋀e. 0 < e ⟹
∃c d.
x ∈ cbox c d ∧
cbox c d ⊆ ball x e ∧
cbox c d ⊆ (cbox a b) ∧
¬ (∃p. p tagged_division_of cbox c d ∧ g fine p)"
apply (rule interval_bisection[of "λs. ∃p. p tagged_division_of s ∧ g fine p", OF _ _ False])
apply (simp add: fine_def)
apply (metis tagged_division_Un fine_Un)
apply auto
done
obtain e where e: "e > 0" "ball x e ⊆ g x"
using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
from x(2)[OF e(1)]
obtain c d where c_d: "x ∈ cbox c d"
"cbox c d ⊆ ball x e"
"cbox c d ⊆ cbox a b"
"¬ (∃p. p tagged_division_of cbox c d ∧ g fine p)"
by blast
have "g fine {(x, cbox c d)}"
unfolding fine_def using e using c_d(2) by auto
then show ?thesis
using tagged_division_of_self[OF c_d(1)] using c_d by auto
qed
lemma fine_division_exists_real:
fixes a b :: real
assumes "gauge g"
obtains p where "p tagged_division_of {a .. b}" "g fine p"
by (metis assms box_real(2) fine_division_exists)
subsection ‹A technical lemma about "refinement" of division›
lemma tagged_division_finer:
fixes p :: "('a::euclidean_space × ('a::euclidean_space set)) set"
assumes ptag: "p tagged_division_of (cbox a b)"
and "gauge d"
obtains q where "q tagged_division_of (cbox a b)"
and "d fine q"
and "∀(x,k) ∈ p. k ⊆ d(x) ⟶ (x,k) ∈ q"
proof -
have p: "finite p" "p tagged_partial_division_of (cbox a b)"
using ptag tagged_division_of_def by blast+
have "(∃q. q tagged_division_of (⋃{k. ∃x. (x,k) ∈ p}) ∧ d fine q ∧ (∀(x,k) ∈ p. k ⊆ d(x) ⟶ (x,k) ∈ q))"
if "finite p" "p tagged_partial_division_of (cbox a b)" "gauge d" for p
using that
proof (induct p)
case empty
show ?case
by (force simp add: fine_def)
next
case (insert xk p)
obtain x k where xk: "xk = (x, k)"
using surj_pair[of xk] by metis
obtain q1 where q1: "q1 tagged_division_of ⋃{k. ∃x. (x, k) ∈ p}"
and "d fine q1"
and q1I: "⋀x k. ⟦(x, k)∈p; k ⊆ d x⟧ ⟹ (x, k) ∈ q1"
using case_prodD tagged_partial_division_subset[OF insert(4) subset_insertI]
by (metis (mono_tags, lifting) insert.hyps(3) insert.prems(2))
have *: "⋃{l. ∃y. (y,l) ∈ insert xk p} = k ∪ ⋃{l. ∃y. (y,l) ∈ p}"
unfolding xk by auto
note p = tagged_partial_division_ofD[OF insert(4)]
obtain u v where uv: "k = cbox u v"
using p(4) xk by blast
have "finite {k. ∃x. (x, k) ∈ p}"
apply (rule finite_subset[of _ "snd ` p"])
using image_iff apply fastforce
using insert.hyps(1) by blast
then have int: "interior (cbox u v) ∩ interior (⋃{k. ∃x. (x, k) ∈ p}) = {}"
proof (rule Int_interior_Union_intervals)
show "open (interior (cbox u v))"
by auto
show "⋀T. T ∈ {k. ∃x. (x, k) ∈ p} ⟹ ∃a b. T = cbox a b"
using p(4) by auto
show "⋀T. T ∈ {k. ∃x. (x, k) ∈ p} ⟹ interior (cbox u v) ∩ interior T = {}"
by clarify (metis insert.hyps(2) insert_iff interior_cbox p(5) uv xk)
qed
show ?case
proof (cases "cbox u v ⊆ d x")
case True
have "{(x, cbox u v)} tagged_division_of cbox u v"
by (simp add: p(2) uv xk tagged_division_of_self)
then have "{(x, cbox u v)} ∪ q1 tagged_division_of ⋃{k. ∃x. (x, k) ∈ insert xk p}"
unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_Un)
with True show ?thesis
apply (rule_tac x="{(x,cbox u v)} ∪ q1" in exI)
using ‹d fine q1› fine_def q1I uv xk apply fastforce
done
next
case False
obtain q2 where q2: "q2 tagged_division_of cbox u v" "d fine q2"
using fine_division_exists[OF assms(2)] by blast
show ?thesis
apply (rule_tac x="q2 ∪ q1" in exI)
apply (intro conjI)
unfolding * uv
apply (rule tagged_division_Un q2 q1 int fine_Un)+
apply (auto intro: q1 q2 fine_Un ‹d fine q1› simp add: False q1I uv xk)
done
qed
qed
with p obtain q where q: "q tagged_division_of ⋃{k. ∃x. (x, k) ∈ p}" "d fine q" "∀(x, k)∈p. k ⊆ d x ⟶ (x, k) ∈ q"
by (meson ‹gauge d›)
with ptag that show ?thesis by auto
qed
subsubsection ‹Covering lemma›
text‹ Some technical lemmas used in the approximation results that follow. Proof of the covering
lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
"Introduction to Gauge Integrals". ›
proposition covering_lemma:
assumes "S ⊆ cbox a b" "box a b ≠ {}" "gauge g"
obtains 𝒟 where
"countable 𝒟" "⋃𝒟 ⊆ cbox a b"
"⋀K. K ∈ 𝒟 ⟹ interior K ≠ {} ∧ (∃c d. K = cbox c d)"
"pairwise (λA B. interior A ∩ interior B = {}) 𝒟"
"⋀K. K ∈ 𝒟 ⟹ ∃x ∈ S ∩ K. K ⊆ g x"
"⋀u v. cbox u v ∈ 𝒟 ⟹ ∃n. ∀i ∈ Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
"S ⊆ ⋃𝒟"
proof -
have aibi: "⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i" and normab: "0 < norm(b - a)"
using ‹box a b ≠ {}› box_eq_empty box_sing by fastforce+
let ?K0 = "λ(n, f::'a⇒nat).
cbox (∑i ∈ Basis. (a ∙ i + (f i / 2^n) * (b ∙ i - a ∙ i)) *⇩R i)
(∑i ∈ Basis. (a ∙ i + ((f i + 1) / 2^n) * (b ∙ i - a ∙ i)) *⇩R i)"
let ?D0 = "?K0 ` (SIGMA n:UNIV. Pi⇩E Basis (λi::'a. lessThan (2^n)))"
obtain 𝒟0 where count: "countable 𝒟0"
and sub: "⋃𝒟0 ⊆ cbox a b"
and int: "⋀K. K ∈ 𝒟0 ⟹ (interior K ≠ {}) ∧ (∃c d. K = cbox c d)"
and intdj: "⋀A B. ⟦A ∈ 𝒟0; B ∈ 𝒟0⟧ ⟹ A ⊆ B ∨ B ⊆ A ∨ interior A ∩ interior B = {}"
and SK: "⋀x. x ∈ S ⟹ ∃K ∈ 𝒟0. x ∈ K ∧ K ⊆ g x"
and cbox: "⋀u v. cbox u v ∈ 𝒟0 ⟹ ∃n. ∀i ∈ Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
and fin: "⋀K. K ∈ 𝒟0 ⟹ finite {L ∈ 𝒟0. K ⊆ L}"
proof
show "countable ?D0"
by (simp add: countable_PiE)
next
show "⋃?D0 ⊆ cbox a b"
apply (simp add: UN_subset_iff)
apply (intro conjI allI ballI subset_box_imp)
apply (simp add: field_simps)
apply (auto intro: mult_right_mono aibi)
apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem intro: mult_right_mono)
done
next
show "⋀K. K ∈ ?D0 ⟹ interior K ≠ {} ∧ (∃c d. K = cbox c d)"
using ‹box a b ≠ {}›
by (clarsimp simp: box_eq_empty) (fastforce simp add: field_split_simps dest: PiE_mem)
next
have realff: "(real w) * 2^m < (real v) * 2^n ⟷ w * 2^m < v * 2^n" for m n v w
using of_nat_less_iff less_imp_of_nat_less by fastforce
have *: "∀v w. ?K0(m,v) ⊆ ?K0(n,w) ∨ ?K0(n,w) ⊆ ?K0(m,v) ∨ interior(?K0(m,v)) ∩ interior(?K0(n,w)) = {}"
for m n
proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
fix v w m and n::nat
assume "m ≤ n"
have "?K0(n,w) ⊆ ?K0(m,v) ∨ interior(?K0(m,v)) ∩ interior(?K0(n,w)) = {}"
apply (simp add: subset_box disjoint_interval)
apply (rule ccontr)
apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le)
apply (drule_tac x=i in bspec, assumption)
using ‹m≤n› realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
apply (simp_all add: power_add)
apply (metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)
apply (metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)
done
then show "?K0(m,v) ⊆ ?K0(n,w) ∨ ?K0(n,w) ⊆ ?K0(m,v) ∨ interior(?K0(m,v)) ∩ interior(?K0(n,w)) = {}"
by meson
qed auto
show "⋀A B. ⟦A ∈ ?D0; B ∈ ?D0⟧ ⟹ A ⊆ B ∨ B ⊆ A ∨ interior A ∩ interior B = {}"
apply (erule imageE SigmaE)+
using * by simp
next
show "∃K ∈ ?D0. x ∈ K ∧ K ⊆ g x" if "x ∈ S" for x
proof (simp only: bex_simps split_paired_Bex_Sigma)
show "∃n. ∃f ∈ Basis →⇩E {..<2 ^ n}. x ∈ ?K0(n,f) ∧ ?K0(n,f) ⊆ g x"
proof -
obtain e where "0 < e"
and e: "⋀y. (⋀i. i ∈ Basis ⟹ ¦x ∙ i - y ∙ i¦ ≤ e) ⟹ y ∈ g x"
proof -
have "x ∈ g x" "open (g x)"
using ‹gauge g› by (auto simp: gauge_def)
then obtain ε where "0 < ε" and ε: "ball x ε ⊆ g x"
using openE by blast
have "norm (x - y) < ε"
if "(⋀i. i ∈ Basis ⟹ ¦x ∙ i - y ∙ i¦ ≤ ε / (2 * real DIM('a)))" for y
proof -
have "norm (x - y) ≤ (∑i∈Basis. ¦x ∙ i - y ∙ i¦)"
by (metis (no_types, lifting) inner_diff_left norm_le_l1 sum.cong)
also have "... ≤ DIM('a) * (ε / (2 * real DIM('a)))"
by (meson sum_bounded_above that)
also have "... = ε / 2"
by (simp add: field_split_simps)
also have "... < ε"
by (simp add: ‹0 < ε›)
finally show ?thesis .
qed
then show ?thesis
by (rule_tac e = "ε / 2 / DIM('a)" in that) (simp_all add: ‹0 < ε› dist_norm subsetD [OF ε])
qed
have xab: "x ∈ cbox a b"
using ‹x ∈ S› ‹S ⊆ cbox a b› by blast
obtain n where n: "norm (b - a) / 2^n < e"
using real_arch_pow_inv [of "e / norm(b - a)" "1/2"] normab ‹0 < e›
by (auto simp: field_split_simps)
then have "norm (b - a) < e * 2^n"
by (auto simp: field_split_simps)
then have bai: "b ∙ i - a ∙ i < e * 2 ^ n" if "i ∈ Basis" for i
proof -
have "b ∙ i - a ∙ i ≤ norm (b - a)"
by (metis abs_of_nonneg dual_order.trans inner_diff_left linear norm_ge_zero Basis_le_norm that)
also have "... < e * 2 ^ n"
using ‹norm (b - a) < e * 2 ^ n› by blast
finally show ?thesis .
qed
have D: "(a + n ≤ x ∧ x ≤ a + m) ⟹ (a + n ≤ y ∧ y ≤ a + m) ⟹ abs(x - y) ≤ m - n"
for a m n x and y::real
by auto
have "∀i∈Basis. ∃k<2 ^ n. (a ∙ i + real k * (b ∙ i - a ∙ i) / 2 ^ n ≤ x ∙ i ∧
x ∙ i ≤ a ∙ i + (real k + 1) * (b ∙ i - a ∙ i) / 2 ^ n)"
proof
fix i::'a assume "i ∈ Basis"
consider "x ∙ i = b ∙ i" | "x ∙ i < b ∙ i"
using ‹i ∈ Basis› mem_box(2) xab by force
then show "∃k<2 ^ n. (a ∙ i + real k * (b ∙ i - a ∙ i) / 2 ^ n ≤ x ∙ i ∧
x ∙ i ≤ a ∙ i + (real k + 1) * (b ∙ i - a ∙ i) / 2 ^ n)"
proof cases
case 1 then show ?thesis
by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps field_split_simps of_nat_diff ‹i ∈ Basis› aibi)
next
case 2
then have abi_less: "a ∙ i < b ∙ i"
using ‹i ∈ Basis› xab by (auto simp: mem_box)
let ?k = "nat ⌊2 ^ n * (x ∙ i - a ∙ i) / (b ∙ i - a ∙ i)⌋"
show ?thesis
proof (intro exI conjI)
show "?k < 2 ^ n"
using aibi xab ‹i ∈ Basis›
by (force simp: nat_less_iff floor_less_iff field_split_simps 2 mem_box)
next
have "a ∙ i + real ?k * (b ∙ i - a ∙ i) / 2 ^ n ≤
a ∙ i + (2 ^ n * (x ∙ i - a ∙ i) / (b ∙ i - a ∙ i)) * (b ∙ i - a ∙ i) / 2 ^ n"
apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
using aibi [OF ‹i ∈ Basis›] xab 2
apply (simp_all add: ‹i ∈ Basis› mem_box field_split_simps)
done
also have "... = x ∙ i"
using abi_less by (simp add: field_split_simps)
finally show "a ∙ i + real ?k * (b ∙ i - a ∙ i) / 2 ^ n ≤ x ∙ i" .
next
have "x ∙ i ≤ a ∙ i + (2 ^ n * (x ∙ i - a ∙ i) / (b ∙ i - a ∙ i)) * (b ∙ i - a ∙ i) / 2 ^ n"
using abi_less by (simp add: field_split_simps)
also have "... ≤ a ∙ i + (real ?k + 1) * (b ∙ i - a ∙ i) / 2 ^ n"
apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
using aibi [OF ‹i ∈ Basis›] xab
apply (auto simp: ‹i ∈ Basis› mem_box divide_simps)
done
finally show "x ∙ i ≤ a ∙ i + (real ?k + 1) * (b ∙ i - a ∙ i) / 2 ^ n" .
qed
qed
qed
then have "∃f∈Basis →⇩E {..<2 ^ n}. x ∈ ?K0(n,f)"
apply (simp add: mem_box Bex_def)
apply (clarify dest!: bchoice)
apply (rule_tac x="restrict f Basis" in exI, simp)
done
moreover have "⋀f. x ∈ ?K0(n,f) ⟹ ?K0(n,f) ⊆ g x"
apply (clarsimp simp add: mem_box)
apply (rule e)
apply (drule bspec D, assumption)+
apply (erule order_trans)
apply (simp add: divide_simps)
using bai apply (force simp add: algebra_simps)
done
ultimately show ?thesis by auto
qed
qed
next
show "⋀u v. cbox u v ∈ ?D0 ⟹ ∃n. ∀i ∈ Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
by (force simp: eq_cbox box_eq_empty field_simps dest!: aibi)
next
obtain j::'a where "j ∈ Basis"
using nonempty_Basis by blast
have "finite {L ∈ ?D0. ?K0(n,f) ⊆ L}" if "f ∈ Basis →⇩E {..<2 ^ n}" for n f
proof (rule finite_subset)
let ?B = "(λ(n, f::'a⇒nat). cbox (∑i∈Basis. (a ∙ i + (f i) / 2^n * (b ∙ i - a ∙ i)) *⇩R i)
(∑i∈Basis. (a ∙ i + ((f i) + 1) / 2^n * (b ∙ i - a ∙ i)) *⇩R i))
` (SIGMA m:atMost n. Pi⇩E Basis (λi::'a. lessThan (2^m)))"
have "?K0(m,g) ∈ ?B" if "g ∈ Basis →⇩E {..<2 ^ m}" "?K0(n,f) ⊆ ?K0(m,g)" for m g
proof -
have dd: "w / m ≤ v / n ∧ (v+1) / n ≤ (w+1) / m
⟹ inverse n ≤ inverse m" for w m v n::real
by (auto simp: field_split_simps)
have bjaj: "b ∙ j - a ∙ j > 0"
using ‹j ∈ Basis› ‹box a b ≠ {}› box_eq_empty(1) by fastforce
have "((g j) / 2 ^ m) * (b ∙ j - a ∙ j) ≤ ((f j) / 2 ^ n) * (b ∙ j - a ∙ j) ∧
(((f j) + 1) / 2 ^ n) * (b ∙ j - a ∙ j) ≤ (((g j) + 1) / 2 ^ m) * (b ∙ j - a ∙ j)"
using that ‹j ∈ Basis› by (simp add: subset_box field_split_simps aibi)
then have "((g j) / 2 ^ m) ≤ ((f j) / 2 ^ n) ∧
((real(f j) + 1) / 2 ^ n) ≤ ((real(g j) + 1) / 2 ^ m)"
by (metis bjaj mult.commute of_nat_1 of_nat_add mult_le_cancel_iff2)
then have "inverse (2^n) ≤ (inverse (2^m) :: real)"
by (rule dd)
then have "m ≤ n"
by auto
show ?thesis
by (rule imageI) (simp add: ‹m ≤ n› that)
qed
then show "{L ∈ ?D0. ?K0(n,f) ⊆ L} ⊆ ?B"
by auto
show "finite ?B"
by (intro finite_imageI finite_SigmaI finite_atMost finite_lessThan finite_PiE finite_Basis)
qed
then show "finite {L ∈ ?D0. K ⊆ L}" if "K ∈ ?D0" for K
using that by auto
qed
let ?D1 = "{K ∈ 𝒟0. ∃x ∈ S ∩ K. K ⊆ g x}"
obtain 𝒟 where count: "countable 𝒟"
and sub: "⋃𝒟 ⊆ cbox a b" "S ⊆ ⋃𝒟"
and int: "⋀K. K ∈ 𝒟 ⟹ (interior K ≠ {}) ∧ (∃c d. K = cbox c d)"
and intdj: "⋀A B. ⟦A ∈ 𝒟; B ∈ 𝒟⟧ ⟹ A ⊆ B ∨ B ⊆ A ∨ interior A ∩ interior B = {}"
and SK: "⋀K. K ∈ 𝒟 ⟹ ∃x. x ∈ S ∩ K ∧ K ⊆ g x"
and cbox: "⋀u v. cbox u v ∈ 𝒟 ⟹ ∃n. ∀i ∈ Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
and fin: "⋀K. K ∈ 𝒟 ⟹ finite {L. L ∈ 𝒟 ∧ K ⊆ L}"
proof
show "countable ?D1" using count countable_subset
by (simp add: count countable_subset)
show "⋃?D1 ⊆ cbox a b"
using sub by blast
show "S ⊆ ⋃?D1"
using SK by (force simp:)
show "⋀K. K ∈ ?D1 ⟹ (interior K ≠ {}) ∧ (∃c d. K = cbox c d)"
using int by blast
show "⋀A B. ⟦A ∈ ?D1; B ∈ ?D1⟧ ⟹ A ⊆ B ∨ B ⊆ A ∨ interior A ∩ interior B = {}"
using intdj by blast
show "⋀K. K ∈ ?D1 ⟹ ∃x. x ∈ S ∩ K ∧ K ⊆ g x"
by auto
show "⋀u v. cbox u v ∈ ?D1 ⟹ ∃n. ∀i ∈ Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
using cbox by blast
show "⋀K. K ∈ ?D1 ⟹ finite {L. L ∈ ?D1 ∧ K ⊆ L}"
using fin by simp (metis (mono_tags, lifting) Collect_mono rev_finite_subset)
qed
let ?𝒟 = "{K ∈ 𝒟. ∀K'. K' ∈ 𝒟 ∧ K ≠ K' ⟶ ¬(K ⊆ K')}"
show ?thesis
proof (rule that)
show "countable ?𝒟"
by (blast intro: countable_subset [OF _ count])
show "⋃?𝒟 ⊆ cbox a b"
using sub by blast
show "S ⊆ ⋃?𝒟"
proof clarsimp
fix x
assume "x ∈ S"
then obtain X where "x ∈ X" "X ∈ 𝒟" using ‹S ⊆ ⋃𝒟› by blast
let ?R = "{(K,L). K ∈ 𝒟 ∧ L ∈ 𝒟 ∧ L ⊂ K}"
have irrR: "irrefl ?R" by (force simp: irrefl_def)
have traR: "trans ?R" by (force simp: trans_def)
have finR: "⋀x. finite {y. (y, x) ∈ ?R}"
by simp (metis (mono_tags, lifting) fin ‹X ∈ 𝒟› finite_subset mem_Collect_eq psubset_imp_subset subsetI)
have "{X ∈ 𝒟. x ∈ X} ≠ {}"
using ‹X ∈ 𝒟› ‹x ∈ X› by blast
then obtain Y where "Y ∈ {X ∈ 𝒟. x ∈ X}" "⋀Y'. (Y', Y) ∈ ?R ⟹ Y' ∉ {X ∈ 𝒟. x ∈ X}"
by (rule wfE_min' [OF wf_finite_segments [OF irrR traR finR]]) blast
then show "∃Y. Y ∈ 𝒟 ∧ (∀K'. K' ∈ 𝒟 ∧ Y ≠ K' ⟶ ¬ Y ⊆ K') ∧ x ∈ Y"
by blast
qed
show "⋀K. K ∈ ?𝒟 ⟹ interior K ≠ {} ∧ (∃c d. K = cbox c d)"
by (blast intro: dest: int)
show "pairwise (λA B. interior A ∩ interior B = {}) ?𝒟"
using intdj by (simp add: pairwise_def) metis
show "⋀K. K ∈ ?𝒟 ⟹ ∃x ∈ S ∩ K. K ⊆ g x"
using SK by force
show "⋀u v. cbox u v ∈ ?𝒟 ⟹ ∃n. ∀i∈Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
using cbox by force
qed
qed
subsection ‹Division filter›
text ‹Divisions over all gauges towards finer divisions.›
definition division_filter :: "'a::euclidean_space set ⇒ ('a × 'a set) set filter"
where "division_filter s = (INF g∈{g. gauge g}. principal {p. p tagged_division_of s ∧ g fine p})"
proposition eventually_division_filter:
"(∀⇩F p in division_filter s. P p) ⟷
(∃g. gauge g ∧ (∀p. p tagged_division_of s ∧ g fine p ⟶ P p))"
unfolding division_filter_def
proof (subst eventually_INF_base; clarsimp)
fix g1 g2 :: "'a ⇒ 'a set" show "gauge g1 ⟹ gauge g2 ⟹ ∃x. gauge x ∧
{p. p tagged_division_of s ∧ x fine p} ⊆ {p. p tagged_division_of s ∧ g1 fine p} ∧
{p. p tagged_division_of s ∧ x fine p} ⊆ {p. p tagged_division_of s ∧ g2 fine p}"
by (intro exI[of _ "λx. g1 x ∩ g2 x"]) (auto simp: fine_Int)
qed (auto simp: eventually_principal)
lemma division_filter_not_empty: "division_filter (cbox a b) ≠ bot"
unfolding trivial_limit_def eventually_division_filter
by (auto elim: fine_division_exists)
lemma eventually_division_filter_tagged_division:
"eventually (λp. p tagged_division_of s) (division_filter s)"
unfolding eventually_division_filter by (intro exI[of _ "λx. ball x 1"]) auto
end