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
by induction (auto simp: sum.Sigma)
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 ‹Some useful lemmas about intervals›
lemma interior_subset_union_intervals:
fixes a b c d
defines "i ≡ cbox a b"
defines "j ≡ cbox c d"
assumes "interior j ≠ {}"
and "i ⊆ j ∪ S"
and "interior i ∩ interior j = {}"
shows "interior i ⊆ interior S"
by (smt (verit, del_insts) IntI Int_interval_mixed_eq_empty UnE assms empty_iff interior_cbox interior_maximal interior_subset open_interior subset_eq)
lemma interior_Union_subset_cbox:
assumes "finite ℱ"
assumes ℱ: "⋀S. S ∈ ℱ ⟹ ∃a b. S = cbox a b" "⋀S. S ∈ ℱ ⟹ interior S ⊆ T"
and T: "closed T"
shows "interior (⋃ℱ) ⊆ T"
proof -
have clo[simp]: "S ∈ ℱ ⟹ closed S" for S
using ℱ by auto
define E where "E = {s∈ℱ. interior s = {}}"
then have "finite E" "E ⊆ {s∈ℱ. interior s = {}}"
using ‹finite ℱ› by auto
then have "interior (⋃ℱ) = interior (⋃(ℱ - E))"
proof (induction E rule: finite_subset_induct')
case (insert s f')
have "interior (⋃(ℱ - insert s f') ∪ s) = interior (⋃(ℱ - insert s f'))"
using insert.hyps ‹finite ℱ› by (intro interior_closed_Un_empty_interior) auto
also have "⋃(ℱ - insert s f') ∪ s = ⋃(ℱ - f')"
using insert.hyps by auto
finally show ?case
by (simp add: insert.IH)
qed simp
also have "… ⊆ ⋃(ℱ - E)"
by (rule interior_subset)
also have "… ⊆ T"
proof (rule Union_least)
fix s assume "s ∈ ℱ - E"
with ℱ[of s] obtain a b where s: "s ∈ ℱ" "s = cbox a b" "box a b ≠ {}"
by (fastforce simp: E_def)
have "closure (interior s) ⊆ closure T"
by (intro closure_mono ℱ ‹s ∈ ℱ›)
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 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))"
by (metis (mono_tags, lifting) gauge_def imageI open_negations minus_minus)
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 *
by (simp add: assms gaugeD open_INT)
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 ?l
have "x = {a}" if "x ∈ s" for x
by (metis ‹s division_of cbox a a› cbox_idem 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_idem by auto
qed (use cbox_idem in blast)
lemma elementary_empty: obtains p where "p division_of {}"
by simp
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)
show "finite q"
using assms finite_subset by blast
next
fix k
assume "k ∈ q"
show "k ⊆ ⋃q"
using ‹k ∈ q› by auto
show "∃a b. k = cbox a b" "k ≠ {}"
using assms ‹k ∈ q› by blast+
next
fix k1 k2
assume "k1 ∈ q" "k2 ∈ q" "k1 ≠ k2"
then show "interior k1 ∩ interior k2 = {}"
using assms by blast
qed auto
lemma division_of_union_self[intro]: "p division_of s ⟹ p division_of (⋃p)"
by blast
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 UA: "⋃?A = s1 ∩ s2"
unfolding *
using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
{
fix k
assume kA: "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 UA kA by blast
show "∃a b. k = cbox a b"
using k by (metis (no_types, lifting) Int_interval assms division_ofD(4))
}
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 show "interior k1 ∩ interior k2 = {}"
unfolding k1 k2
using assms division_ofD(5) k1 k2 by auto
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 ℱ"
and "ℱ ≠ {}"
and "∀s∈ℱ. ∃p. p division_of (s::('a::euclidean_space) set)"
shows "∃p. p division_of (⋂ℱ)"
using assms
proof (induct ℱ rule: finite_induct)
case (insert x ℱ)
then show ?case
by (metis cInf_singleton complete_lattice_class.Inf_insert elementary_Int insert_iff)
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)]
fix k1 k2
assume "k1 ∈ p1 ∪ p2" "k2 ∈ p1 ∪ p2" "k1 ≠ k2"
with assms show "interior k1 ∩ interior k2 = {}"
by (smt (verit, best) IntE Un_iff disjoint_iff_not_equal division_ofD(2) division_ofD(5) inf.orderE interior_Int)
qed (use division_ofD assms in auto)
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
{
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"
using ‹l ≠ K› l k f g by auto
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])
}
have "a ∙ i ≤ fst (f i) ∙ i" "snd (f i) ∙ i ≤ b ∙ i" "fst (f i) ∙ i ≤ snd (f i) ∙ i"
if "i ∈ Basis" for i
proof -
have "f i = (a, c) ∨ f i = (c, d) ∨ f i = (d, b)"
using that f by (auto simp: PiE_iff)
with that 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 simp add: k box_eq_empty subset_box not_less)
}
moreover
have "∃k∈p. x ∈ k" if x: "x ∈ cbox a b" for x
proof -
have "∃l. x ∙ i ∈ {fst l ∙ i .. snd l ∙ i} ∧ l ∈ {(a, c), (c, d), (d, b)}" if "i ∈ Basis" for i
proof -
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)"
using that x ord[of 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)}"
by metis
moreover from f have "x ∈ ?B (restrict f Basis)" "restrict f Basis ∈ Basis →⇩E {(a,c), (c,d), (d,b)}"
by (auto simp: mem_box)
ultimately show ?thesis
unfolding p_def by blast
qed
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
then show ?thesis
using elementary_interval that by auto
next
case False
note p = division_ofD[OF assms(1)]
have "∀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
then obtain q where q: "⋀x. x ∈ p ⟹ q x division_of cbox a b" "⋀x. x ∈ p ⟹ x ∈ q x"
by metis
have "q x division_of ⋃(q x)" if x: "x ∈ p" for x
using q(1) x by blast
then have di: "⋀x. x ∈ p ⟹ ∃d. d division_of ⋃(q x - {x})"
by (meson Diff_subset division_of_subset)
have "∀s∈(λi. ⋃ (q i - {i})) ` p. ∃d. d division_of s"
using di by blast
then obtain d where d: "d division_of ⋂((λi. ⋃(q i - {i})) ` p)"
by (meson False elementary_Inter finite_imageI image_is_empty p(1))
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 ∈ p"
then show "⋃(q i - {i}) ∪ i = cbox a b"
by (metis Un_commute complete_lattice_class.Sup_insert division_ofD(6) insert_Diff q)
qed
have [simp]: "interior (⋂i∈p. ⋃(q i - {i})) ∩ interior K = {}" if K: "K ∈ p" for K
proof -
note qk = division_ofD[OF q(1)[OF K]]
have *: "⋀U T S. T ∩ S = {} ⟹ U ⊆ S ⟹ U ∩ T = {}"
by auto
show ?thesis
proof (rule *[OF Int_interior_Union_intervals])
show "⋀T. T∈q K - {K} ⟹ interior K ∩ interior T = {}"
using K q(2) qk(5) by auto
show "interior (⋂i∈p. ⋃(q i - {i})) ⊆ interior (⋃(q K - {K}))"
by (meson INF_lower K interior_mono)
qed (use qk in auto)
qed
show "d ∪ p division_of (cbox a b)"
by (simp add: Int_interior_Union_intervals assms(1) cbox_eq d division_disjoint_union p(1) p(4))
qed
then show ?thesis
by (meson Un_upper2 that)
qed
lemma elementary_bounded[dest]:
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"
by (meson bounded_subset_cbox_symmetric elementary_bounded)
proposition division_union_intervals_exists:
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) ∩ interior (⋃(p - {cbox u v}))"
by (metis Diff_subset Int_absorb1 Int_assoc Sup_subset_mono interior_Int p(8) uv)
also have "… = {}"
using p(6) p(7)[OF p(2)] ‹finite p›
by (intro Int_interior_Union_intervals) auto
finally have disj: "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})"
by (metis Diff_subset assms disj division_disjoint_union division_of_self division_of_subset insert_is_Un p(8) pd)
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
by (metis True assms division_disjoint_union elementary_interval inf_bot_left that)
next
case nonempty: False
have "∀K∈p. ∃q. (insert (cbox a b) q) division_of (cbox a b ∪ K)"
by (metis ‹cbox a b ≠ {}› division_union_intervals_exists pdiv(4))
then obtain q where "∀x∈p. insert (cbox a b) (q x) division_of (cbox a b) ∪ x"
by metis
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) x'(1) x'(2) by presburger
have "interior K' ∩ interior (cbox a b) = {}"
using as'(2) q(5) x' by blast
then have "interior K' ⊆ interior x'"
by (metis nonempty c_d interior_subset_union_intervals q(2) x')
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 ℱ"
and "⋀s. s ∈ ℱ ⟹ ∃a b. s = cbox a (b::'a::euclidean_space)"
obtains p where "p division_of (⋃ℱ)"
proof -
have "∃p. p division_of (⋃ℱ)"
proof (induct_tac ℱ 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∈ℱ"
then obtain a b where x: "x = cbox a b"
by (meson assms(2))
then show "∃p. p division_of ⋃(insert x F)"
using elementary_union_interval by (metis Union_insert as(3) division_ofD(6))
qed (use assms in auto)
then show ?thesis
using that by auto
qed
lemma elementary_union:
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
with elementary_unions_intervals[of "ps ∪ pt"] assms
show ?thesis
by (metis Un_iff Union_Un_distrib division_of_def finite_Un 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)"
by (metis Diff_subset division_of_subset r1(2) r1(8))
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"
using divp(6) r(2) x(2) by blast
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
by (metis Teq div sup_ge1 that)
qed
lemma division_split:
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)
have "∃a b. cbox u v ∩ {x. x ∙ k ≤ c} = cbox a b"
unfolding interval_split[OF k] by (auto intro: order.trans)
then show "∃a b. K = cbox a b"
by (simp add: l(1) uv)
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)
have "∃a b. cbox u v ∩ {x. c ≤ x ∙ k} = cbox a b"
unfolding interval_split[OF k] by (auto intro: order.trans)
then show "∃a b. K = cbox a b"
by (simp add: l(1) uv)
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 show "K ⊆ i" "K ≠ {}" "∃a b. K = cbox a b"
using assm by fastforce+
fix K'
assume k': "K' ∈ snd ` s" "K ≠ K'"
then show "interior K ∩ interior K' = {}"
by (metis (no_types, lifting) assms imageE k prod.collapse tagged_division_ofD(5))
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 show "K ≠ {}" "∃a b. K = cbox a b" "K ⊆ ⋃(snd ` s)"
using assm by fastforce+
fix K'
assume "K' ∈ snd ` s" "K ≠ K'"
then show "interior K ∩ interior K' = {}"
using assm(5) K by force
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}"
by (metis box_real(2) 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" "K ⊆ s1 ∪ s2"
using xK p1 p2 by auto
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
with assms show "interior K ∩ interior K' = {}"
by (metis Un_iff inf_commute p1(3) p2(3) tagged_division_ofD(5) xK xk')
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))"
using tagged_partial_division_ofD[OF assms]
by (intro tagged_division_ofI) auto
lemma tagged_division_of_union_self:
assumes "p tagged_division_of s"
shows "p tagged_division_of (⋃(snd ` p))"
using tagged_division_ofD[OF assms]
by (intro tagged_division_ofI) auto
lemma tagged_division_Un_interval:
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
have "interior (cbox a b ∩ {x. x ∙ k ≤ c}) ∩ interior (cbox a b ∩ {x. c ≤ x ∙ k}) = {}"
using k by (force simp: interval_split[OF k] box_def)
with assms show ?thesis
by (metis "*" tagged_division_Un)
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 by (metis box_real(2) 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}) = {}"
by (smt (verit) Int_Un_eq(1) Un_Int_distrib interior_Int prod.inject sup_bot.right_neutral tagged_division_ofD(5) assms)
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}) = {}"
by (smt (verit) Int_Un_eq(1) Un_Int_distrib interior_Int prod.inject sup_bot.right_neutral tagged_division_ofD(5) assms)
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 "box a b = {}"
by (metis ‹snd x = snd y› ab assm(5) inf.idem interior_cbox prod.collapse)
then show "d (snd x) = ❙1"
by (simp add: ab assms(2))
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_set_and: "comm_monoid_set HOL.conj True"
by (simp add: comm_monoid_set.intro conj.comm_monoid_axioms)
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}"
by auto
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 ≤ v∙i"
using l using that(6) unfolding box_ne_empty[symmetric] by auto
then show ?thesis
using that ‹x ∈ Basis› unfolding l interval_split[OF k]
by (force split: if_split_asm)
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. u∙i ≤ v∙i"
using l using that(6) unfolding box_ne_empty[symmetric] by auto
then show "∃i∈d. interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
using that ‹x ∈ Basis› unfolding l interval_split[OF k]
by (force split: if_split_asm)
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 **: "⋀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 (rename_tac S)
apply (rule_tac x="S ∩ {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"
by (metis box_empty_imp box_subset_cbox empty_as_interval subset_empty)
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 "box a b = {}")
case True
{ fix k assume "k∈d"
then obtain a' b' where k: "k = cbox a' b'"
using division_ofD(4)[OF less.prems] by blast
then have "cbox a' b' ⊆ cbox a b"
using ‹k ∈ d› less.prems by blast
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: True)
}
with True show "F g d = g (cbox a b)"
by (auto intro!: neutral simp: box_empty_imp)
next
case False
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"
by (meson as division_ofD(2) j less.prems 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"
using uv(2) 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]
then show "u ∙ j = a ∙ j" and "v ∙ j = b ∙ j"
by (smt (verit) False box_midpoint j mem_box(1) uv(2))+
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 show "g x = ❙1"
by (smt (verit) box_empty_imp box_eq_empty(1) j uv(1))
qed
then show "F g d = g (cbox a b)"
by (metis deq division_of_finite insert_Diff_single insert_remove less.prems right_neutral)
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)"
by (metis assms box_empty_imp division division_of_tagged_division over_tagged_division_lemma)
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"
by (metis coalesce_less commute left_neutral less_eq_real_def neutral that)
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 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))"
using assms(2) tagged_division by force
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 assms by metis
show thesis
proof
show "⋃ (pfn ` I) tagged_division_of i"
using assms pfn(1) tagged_division_Union by force
show "d fine ⋃ (pfn ` I)"
by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
qed
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"
by blast
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) 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 "c∙i < f∙i" "e∙i < d∙i"
unfolding mem_box using i' by force+
with i i' show False
using s(2) t(2) by fastforce
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)
then show ?case
unfolding S
by (force intro!: f[rule_format])
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 ∈ Basis"
with xy show "¦(x - y) ∙ i¦ ≤ B n ∙ i - A n ∙ i"
by (smt (verit, best) inner_diff_left mem_box(2))
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
have ABsubset: "cbox (A n) (B n) ⊆ cbox (A m) (B m)" if "m ≤ n" for m n
using that
proof (induction rule: inc_induct)
case (step i) show ?case
by (smt (verit, ccfv_SIG) ABRAW in_mono mem_box(2) step.IH subsetI)
qed simp
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 (intro that strip)
show "x0 ∈ cbox a b"
using ‹A 0 = a› ‹B 0 = b› x0 by blast
next
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)"
by (meson x0)
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)"
proof (rule interval_bisection[of "λs. ∃p. p tagged_division_of s ∧ _ p", OF _ _ False])
show "∃p. p tagged_division_of {} ∧ g fine p"
by (simp add: fine_def)
qed (meson tagged_division_Un fine_Un)+
obtain e where e: "e > 0" "ball x e ⊆ g x"
by (meson assms gauge_def openE)
then 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 (meson x(2))
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 simp
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 insert
by (metis (mono_tags, lifting) case_prodD subset_insertI tagged_partial_division_subset)
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 "{K. ∃x. (x, K) ∈ p} ⊆ snd ` p"
by force
then have "finite {K. ∃x. (x, K) ∈ p}"
using finite_surj 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 = {}"
using insert.hyps(2) p(5) uv xk by blast
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}"
by (smt (verit, best) "*" int q1 tagged_division_Un uv)
moreover have "d fine ({(x,cbox u v)} ∪ q1)"
using True ‹d fine q1› fine_def by fastforce
ultimately show ?thesis
by (metis (no_types, lifting) case_prodI2 insert_iff insert_is_Un q1I uv xk)
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
proof (intro exI conjI)
show "q2 ∪ q1 tagged_division_of ⋃ {k. ∃x. (x, k) ∈ insert xk p}"
by (smt (verit, best) "*" int q1 q2(1) tagged_division_Un uv)
show "d fine q2 ∪ q1"
by (simp add: ‹d fine q1› fine_Un q2(2))
qed (use False uv xk q1I in auto)
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_idem 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 aibi mult_right_mono)
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 (rule ccontr)
apply (simp add: subset_box disjoint_interval)
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 (metis (no_types, opaque_lifting) power_add 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 = {}"
using * by fastforce
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)
finally show ?thesis
using ‹0 < ε› by linarith
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
by (smt (verit, del_insts) Basis_le_norm diff_add_cancel inner_simps(1) that)
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"
using aibi [OF ‹i ∈ Basis›] xab 2
apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
apply (auto simp: ‹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"
using aibi [OF ‹i ∈ Basis›] xab
apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
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_left_pos)
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
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)"
using eventually_division_filter by auto
end