# HG changeset patch # User hoelzl # Date 1475146963 -7200 # Node ID c3da799b1b456d7b07983130082270726143e3e5 # Parent b235e845c8e8de31d9bd93544f9f7d9fbaf6f8a3 HOL-Analysis: move gauges and (tagged) divisions to its own theory file diff -r b235e845c8e8 -r c3da799b1b45 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Sep 28 16:15:51 2016 +0200 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Sep 29 13:02:43 2016 +0200 @@ -6417,6 +6417,26 @@ unfolding segment_convex_hull by (auto intro!: hull_subset[unfolded subset_eq, rule_format]) +lemma eventually_closed_segment: + fixes x0::"'a::real_normed_vector" + assumes "open X0" "x0 \ X0" + shows "\\<^sub>F x in at x0 within U. closed_segment x0 x \ X0" +proof - + from openE[OF assms] + obtain e where e: "0 < e" "ball x0 e \ X0" . + then have "\\<^sub>F x in at x0 within U. x \ ball x0 e" + by (auto simp: dist_commute eventually_at) + then show ?thesis + proof eventually_elim + case (elim x) + have "x0 \ ball x0 e" using \e > 0\ by simp + from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim] + have "closed_segment x0 x \ ball x0 e" . + also note \\ \ X0\ + finally show ?case . + qed +qed + lemma segment_furthest_le: fixes a b x y :: "'a::euclidean_space" assumes "x \ closed_segment a b" @@ -10500,7 +10520,7 @@ lemma collinear_3_expand: "collinear{a,b,c} \ a = c \ (\u. b = u *\<^sub>R a + (1 - u) *\<^sub>R c)" -proof - +proof - have "collinear{a,b,c} = collinear{a,c,b}" by (simp add: insert_commute) also have "... = collinear {0, a - c, b - c}" diff -r b235e845c8e8 -r c3da799b1b45 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Sep 28 16:15:51 2016 +0200 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Sep 29 13:02:43 2016 +0200 @@ -1209,8 +1209,8 @@ have sum_p': "(\(x, k)\p'. norm (integral k f)) = (\k\snd ` p'. norm (integral k f))" apply (subst setsum.over_tagged_division_lemma[OF p'',of "\k. norm (integral k f)"]) unfolding norm_eq_zero - apply (rule integral_null) - apply assumption + apply (rule integral_null) + apply (simp add: content_eq_0_interior) apply rule done note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]] @@ -1657,7 +1657,7 @@ show "(\(x, k)\p. norm (integral k f)) \ ?S" using partial_division_of_tagged_division[of p "cbox a b"] p(1) apply (subst setsum.over_tagged_division_lemma[OF p(1)]) - apply (simp add: integral_null) + apply (simp add: content_eq_0_interior) apply (intro cSUP_upper2[OF D(2), of "snd ` p"]) apply (auto simp: tagged_partial_division_of_def) done diff -r b235e845c8e8 -r c3da799b1b45 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Sep 28 16:15:51 2016 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 29 13:02:43 2016 +0200 @@ -6,201 +6,49 @@ theory Henstock_Kurzweil_Integration imports - Lebesgue_Measure + Lebesgue_Measure Tagged_Division begin -lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib - scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff - scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one - - -subsection \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" +(* BEGIN MOVE *) +lemma swap_continuous: + assumes "continuous_on (cbox (a,c) (b,d)) (\(x,y). f x y)" + shows "continuous_on (cbox (c,a) (d,b)) (\(x, y). f y x)" 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\) + have "(\(x, y). f y x) = (\(x, y). f x y) \ prod.swap" + by auto then show ?thesis - by (simp add: field_simps) + apply (rule ssubst) + apply (rule continuous_on_compose) + apply (simp add: split_def) + apply (rule continuous_intros | simp add: assms)+ + done qed -lemma conjunctD2: assumes "a \ b" shows a b using assms by auto -lemma conjunctD3: assumes "a \ b \ c" shows a b c using assms by auto -lemma conjunctD4: assumes "a \ b \ c \ d" shows a b c d using assms by auto - -lemma cond_cases: "(P \ Q x) \ (\ P \ Q y) \ Q (if P then x else y)" + +lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)" + by (simp add: norm_minus_eqI) + +lemma norm_diff2: "\y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \ e1; norm(y2 - x2) \ e2\ + \ norm(y - x) \ e" + using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"] + by (simp add: add_diff_add) + +lemma setcomp_dot1: "{z. P (z \ (i,0))} = {(x,y). P(x \ i)}" by auto -declare norm_triangle_ineq4[intro] - -lemma transitive_stepwise_le: - assumes "\x. R x x" "\x y z. R x y \ R y z \ R x z" and "\n. R n (Suc n)" - shows "\n\m. R m n" -proof (intro allI impI) - show "m \ n \ R m n" for n - by (induction rule: dec_induct) - (use assms in blast)+ -qed - -subsection \Some useful lemmas about intervals.\ +lemma setcomp_dot2: "{z. P (z \ (0,i))} = {(x,y). P(y \ i)}" + by auto + +lemma Sigma_Int_Paircomp1: "(Sigma A B) \ {(x, y). P x} = Sigma (A \ {x. P x}) B" + by blast + +lemma Sigma_Int_Paircomp2: "(Sigma A B) \ {(x, y). P y} = Sigma A (\z. B z \ {y. P y})" + by blast lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)" using nonempty_Basis by (fastforce simp add: set_eq_iff mem_box) - -lemma interior_subset_union_intervals: - assumes "i = cbox a b" - and "j = cbox c d" - and "interior j \ {}" - and "i \ j \ s" - and "interior i \ interior j = {}" - shows "interior i \ interior s" -proof - - have "box a b \ cbox c d = {}" - using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5) - unfolding assms(1,2) interior_cbox by auto - moreover - have "box a b \ cbox c d \ s" - apply (rule order_trans,rule box_subset_cbox) - using assms(4) unfolding assms(1,2) - apply auto - done - ultimately - show ?thesis - unfolding assms interior_cbox - by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI) -qed - -lemma 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 add: closure_box) - qed - finally show ?thesis . -qed - -lemma inter_interior_unions_intervals: - "finite f \ open s \ \t\f. \a b. t = cbox a b \ \t\f. s \ (interior t) = {} \ s \ interior (\f) = {}" - using interior_Union_subset_cbox[of f "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) *\<^sub>R i)" - "cbox a b \ {x. x\k \ c} = cbox (\i\Basis. (if i = k then max (a\k) c else a\i) *\<^sub>R i) b" - apply (rule_tac[!] set_eqI) - unfolding Int_iff mem_box mem_Collect_eq - using assms - apply auto - done - -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) *\<^sub>R i)" - -definition interval_lowerbound :: "('a::euclidean_space) set \ 'a" - where "interval_lowerbound s = (\i\Basis. (INF x:s. x\i) *\<^sub>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_setsum 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_setsum cbox_def - by (safe intro!: cInf_eq) auto - -lemmas interval_bounds = interval_upperbound interval_lowerbound - -lemma - fixes X::"real set" - shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X" - and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X" - by (auto simp: interval_upperbound_def interval_lowerbound_def) - -lemma interval_bounds'[simp]: - assumes "cbox a b \ {}" - 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)) *\<^sub>R i) = (\i\Basis. (SUP x:A. x \ i) *\<^sub>R i)" - by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0) - moreover from assms have snd_image_times': "B = snd ` (A \ B)" by simp - have "(\i\Basis. (SUP x:A \ B. x \ (0, i)) *\<^sub>R i) = (\i\Basis. (SUP x:B. x \ i) *\<^sub>R i)" - by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0) - ultimately show ?thesis unfolding interval_upperbound_def - by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod) -qed - -lemma interval_lowerbound_Times: - assumes "A \ {}" 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)) *\<^sub>R i) = (\i\Basis. (INF x:A. x \ i) *\<^sub>R i)" - by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0) - moreover from assms have snd_image_times': "B = snd ` (A \ B)" by simp - have "(\i\Basis. (INF x:A \ B. x \ (0, i)) *\<^sub>R i) = (\i\Basis. (INF x:B. x \ i) *\<^sub>R i)" - by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0) - ultimately show ?thesis unfolding interval_lowerbound_def - by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod) -qed +(* END MOVE *) subsection \Content (length, area, volume...) of an interval.\ @@ -322,1508 +170,34 @@ by (auto simp: not_le) qed -subsection \The notion of a gauge --- simply an open set containing the point.\ - -definition "gauge d \ (\x. x \ d x \ open (d x))" - -lemma gaugeI: - assumes "\x. x \ g x" - and "\x. open (g x)" - shows "gauge g" - using assms unfolding gauge_def by auto - -lemma gaugeD[dest]: - assumes "gauge d" - shows "x \ d x" - and "open (d 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_inter[intro]: "gauge d1 \ gauge d2 \ gauge (\x. d1 x \ d2 x)" - unfolding gauge_def by auto - -lemma gauge_inters: - assumes "finite s" - and "\d\s. gauge (f d)" - shows "gauge (\x. \{f d x | d. d \ s})" -proof - - have *: "\x. {f d x |d. d \ s} = (\d. f d x) ` s" - by auto - show ?thesis - unfolding gauge_def unfolding * - using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto -qed - -lemma gauge_existence_lemma: - "(\x. \d :: real. p x \ 0 < d \ q d x) \ (\x. \d>0. p x \ q d x)" - by (metis zero_less_one) - - -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" - unfolding division_of_def 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 simp: cbox_sing) - done - } - ultimately show ?l - unfolding division_of_def cbox_sing by auto -next - assume ?l - note * = conjunctD4[OF this[unfolded division_of_def cbox_sing]] - { - fix x - assume x: "x \ s" have "x = {a}" - using *(2)[rule_format,OF x] by auto - } - moreover have "s \ {}" - using *(4) by auto - ultimately show ?r - unfolding cbox_sing by auto -qed - -lemma elementary_empty: obtains p where "p division_of {}" - unfolding division_of_trivial by auto - -lemma elementary_interval: obtains p where "p division_of (cbox a b)" - by (metis division_of_trivial division_of_self) - -lemma division_contains: "s division_of i \ \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 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_of_content_0: assumes "content (cbox a b) = 0" "d division_of (cbox a b)" shows "\k\d. content k = 0" unfolding forall_in_division[OF assms(2)] by (metis antisym_conv assms content_pos_le content_subset division_ofD(2)) -lemma division_inter: - fixes s1 s2 :: "'a::euclidean_space set" - assumes "p1 division_of s1" - and "p2 division_of s2" - shows "{k1 \ 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" - apply (rule set_eqI) - unfolding * and UN_iff - using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] - apply auto - done - { - fix k - assume "k \ ?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_inter: - 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_inters: - 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_inter 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) *\<^sub>R i) (\i\Basis. (snd (f i) \ i) *\<^sub>R i)" - define p where "p = ?B ` (Basis \\<^sub>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)"]) - { - fix i :: 'a - assume "i \ Basis" - with incl nonempty have "a \ i \ c \ i" "c \ i \ d \ i" "d \ i \ b \ i" - unfolding box_eq_empty subset_box by (auto simp: not_le) - } - note ord = this - - show "p division_of (cbox a b)" - proof (rule division_ofI) - show "finite p" - unfolding p_def by (auto intro!: finite_PiE) - { - fix k - assume "k \ p" - then obtain f where f: "f \ Basis \\<^sub>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 \\<^sub>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 intro!: ext) - 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 interior_cbox 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 \\<^sub>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 - -lemma 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 - { fix x - assume x: "x \ p" - have "q x division_of \q x" - apply (rule division_ofI) - using division_ofD[OF q(1)[OF x]] - apply auto - done } - then have "\x. x \ p \ \d. d division_of \(q x - {x})" - by (meson Diff_subset division_of_subset) - then have "\d. d division_of \((\i. \(q i - {i})) ` p)" - apply - - apply (rule elementary_inters [OF finite_imageI[OF p(1)]]) - apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]]) - done - then obtain d where d: "d division_of \((\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" - have *: "\u t s. t \ s = {} \ u \ s \ u \ t = {}" - by auto - have "interior (\i\p. \(q i - {i})) \ interior k = {}" - proof (rule *[OF inter_interior_unions_intervals]) - note qk=division_ofD[OF q(1)[OF k]] - show "finite (q k - {k})" "open (interior k)" "\t\q k - {k}. \a b. t = cbox a b" - using qk by auto - show "\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 - apply auto - done - qed } 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 inter_interior_unions_intervals) - apply (rule p open_interior ballI)+ - apply simp_all - done - qed - then show ?thesis - by (meson Un_upper2 that) -qed - -lemma elementary_bounded[dest]: - fixes s :: "'a::euclidean_space set" - shows "p division_of s \ 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 elementary_bounded bounded_subset_cbox) - -lemma 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 - show ?thesis - apply (rule that[of "{}"]) - unfolding True - using assms - apply auto - done -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 "p division_of cbox c d" "cbox u v \ p" - by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]]) - note p = this division_ofD[OF this(1)] - have "interior (cbox a b \ \(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 inter_interior_unions_intervals) - using p(6) p(7)[OF p(2)] p(3) - 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_unions: - 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 - - note assm = division_ofD[OF assms] - have lem1: "\f s. \\(f ` s) = \((\x. \(f x)) ` s)" - by auto - have lem2: "\f s. f \ {} \ \{s \ t |t. t \ f} = s \ \f" +lemma setsum_content_null: + assumes "content (cbox a b) = 0" + and "p tagged_division_of (cbox a b)" + shows "setsum (\(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)" +proof (rule setsum.neutral, rule) + fix y + assume y: "y \ p" + obtain x k where xk: "y = (x, k)" + using surj_pair[of y] by blast + note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]] + from this(2) obtain c d where k: "k = cbox c d" by blast + have "(\(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x" + unfolding xk by auto + also have "\ = 0" + using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d] + unfolding assms(1) k by auto - { - presume "p = {} \ thesis" - "cbox a b = {} \ thesis" - "cbox a b \ {} \ interior (cbox a b) = {} \ thesis" - "p \ {} \ interior (cbox a b)\{} \ cbox a b \ {} \ thesis" - then show thesis by auto - next - assume as: "p = {}" - obtain p where "p division_of (cbox a b)" - by (rule elementary_interval) - then show thesis - using as that by auto - next - assume as: "cbox a b = {}" - show thesis - using as assms that by auto - next - assume as: "interior (cbox a b) = {}" "cbox a b \ {}" - show thesis - apply (rule that[of "insert (cbox a b) p"],rule division_ofI) - unfolding finite_insert - apply (rule assm(1)) unfolding Union_insert - using assm(2-4) as - apply - - apply (fast dest: assm(5))+ - done - next - assume as: "p \ {}" "interior (cbox a b) \ {}" "cbox a b \ {}" - have "\k\p. \q. (insert (cbox a b) q) division_of (cbox a b \ k)" - proof - fix k - assume kp: "k \ p" - from assm(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 as(3) 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 "*" assm(1) q(1) by auto - show "\?D = cbox a b \ \p" - unfolding * lem1 - unfolding lem2[OF as(1), of "cbox a b", symmetric] - using q(6) - by auto - fix k - assume k: "k \ ?D" - then show "k \ cbox a b \ \p" - using q(2) by auto - show "k \ {}" - using q(3) k by auto - show "\a b. k = cbox a b" - using q(4) k by auto - fix k' - assume 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'") - case True - show ?thesis - using True k' q(5) x' x by auto - next - case False - { - presume "k = cbox a b \ ?thesis" - and "k' = cbox a b \ ?thesis" - and "k \ cbox a b \ k' \ cbox a b \ ?thesis" - then show ?thesis by linarith - next - assume as': "k = cbox a b" - show ?thesis - using as' k' q(5) x' by blast - next - assume as': "k' = cbox a b" - show ?thesis - using as' k'(2) q(5) x by blast - } - assume as': "k \ cbox a b" "k' \ cbox a b" - obtain c d where k: "k = cbox c d" - using q(4)[OF x(2,1)] by blast - have "interior k \ interior (cbox a b) = {}" - using as' k'(2) q(5) x by blast - then have "interior k \ interior x" - using interior_subset_union_intervals - by (metis as(2) k q(2) x interior_subset_union_intervals) - moreover - obtain c d where c_d: "k' = cbox c d" - using q(4)[OF x'(2,1)] by blast - have "interior k' \ interior (cbox a b) = {}" - using as'(2) q(5) x' by blast - then have "interior k' \ interior x'" - by (metis as(2) c_d interior_subset_union_intervals q(2) x'(1) x'(2)) - ultimately show ?thesis - using assm(5)[OF x(2) x'(2) False] by auto - qed - qed - } -qed - -lemma elementary_unions_intervals: - assumes fin: "finite f" - and "\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_inter) - { - fix x - assume x: "x \ t" "x \ s" - then have "x\\r1" - unfolding r1 using ab by auto - then obtain r where r: "r \ r1" "x \ r" - unfolding Union_iff .. - 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 *: "t = \p \ (\(r1 - p) \ \q)" - unfolding divp divq using assms(3) by auto - show ?thesis - apply (rule that[of "p \ r2"]) - unfolding * - defer - apply (rule division_disjoint_union) - unfolding divp(6) - apply(rule assms r2)+ - proof - - have "interior s \ interior (\(r1-p)) = {}" - proof (rule inter_interior_unions_intervals) - show "finite (r1 - p)" and "open (interior s)" and "\t\r1-p. \a b. t = cbox a b" - using r1 by auto - have *: "\s. (\x. x \ s \ False) \ s = {}" - by auto - show "\t\r1-p. interior s \ interior t = {}" - proof - fix m x - assume as: "m \ r1 - p" - have "interior m \ interior (\p) = {}" - proof (rule inter_interior_unions_intervals) - show "finite p" and "open (interior m)" and "\t\p. \a b. t = cbox a b" - using divp by auto - show "\t\p. interior m \ interior t = {}" - by (metis DiffD1 DiffD2 as r1(1) r1(7) set_rev_mp) - qed - then show "interior s \ interior m = {}" - unfolding divp by auto - qed - qed - then show "interior s \ interior (\(r1-p) \ (\q)) = {}" - using interior_subset by auto - qed auto -qed - -lemma division_split_left_inj: - fixes type :: "'a::euclidean_space" - assumes "d division_of i" - and "k1 \ d" - and "k2 \ d" - and "k1 \ k2" - and "k1 \ {x::'a. x\k \ c} = k2 \ {x. x\k \ c}" - and k: "k\Basis" - shows "content(k1 \ {x. x\k \ c}) = 0" -proof - - note d=division_ofD[OF assms(1)] - have *: "\(a::'a) b c. content (cbox a b \ {x. x\k \ c}) = 0 \ - interior(cbox a b \ {x. x\k \ c}) = {}" - unfolding interval_split[OF k] content_eq_0_interior by auto - guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this - guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this - have **: "\s t u. s \ t = {} \ u \ s \ u \ t \ u = {}" - by auto - show ?thesis - unfolding uv1 uv2 * - apply (rule **[OF d(5)[OF assms(2-4)]]) - apply (simp add: uv1) - using assms(5) uv1 by auto -qed - -lemma division_split_right_inj: - fixes type :: "'a::euclidean_space" - assumes "d division_of i" - and "k1 \ d" - and "k2 \ d" - and "k1 \ k2" - and "k1 \ {x::'a. x\k \ c} = k2 \ {x. x\k \ c}" - and k: "k \ Basis" - shows "content (k1 \ {x. x\k \ c}) = 0" -proof - - note d=division_ofD[OF assms(1)] - have *: "\a b::'a. \c. content(cbox a b \ {x. x\k \ c}) = 0 \ - interior(cbox a b \ {x. x\k \ c}) = {}" - unfolding interval_split[OF k] content_eq_0_interior by auto - guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this - guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this - have **: "\s t u. s \ t = {} \ u \ s \ u \ t \ u = {}" - by auto - show ?thesis - unfolding uv1 uv2 * - apply (rule **[OF d(5)[OF assms(2-4)]]) - apply (simp add: uv1) - using assms(5) uv1 by auto + finally show "(\(x, k). content k *\<^sub>R f x) y = 0" . 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 guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this - guess u v using p(4)[OF l(2)] by (elim exE) note uv=this - 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 guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this - 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 guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this - guess u v using p(4)[OF l(2)] by (elim exE) note uv=this - 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 guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this - 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[dest]: - 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 - apply auto - apply fastforce+ - done - -lemma tagged_division_ofD[dest]: (*FIXME USE A LOCALE*) - 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 - unfolding tagged_partial_division_of_def - using finite_subset[OF assms(2)] - by blast - -lemma (in comm_monoid_set) over_tagged_division_lemma: - assumes "p tagged_division_of i" - and "\u v. cbox u v \ {} \ content (cbox u v) = 0 \ d (cbox u v) = \<^bold>1" - shows "F (\(x,k). d k) p = F d (snd ` p)" -proof - - have *: "(\(x,k). d k) = d \ snd" - unfolding o_def by (rule ext) auto - 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" - by (metis prod.collapse \x\p\ \snd x = snd y\ \x \ y\)+ - with \x\p\ \y\p\ have "interior (snd x) \ interior (snd y) = {}" - by (intro assm(5)[of "fst x" _ "fst y"]) auto - then have "content (cbox a b) = 0" - unfolding \snd x = snd y\[symmetric] ab content_eq_0_interior by auto - then have "d (cbox a b) = \<^bold>1" - using assm(2)[of "fst x" "snd x"] \x\p\ ab[symmetric] by (intro assms(2)) auto - then show "d (snd x) = \<^bold>1" - unfolding ab by auto - qed -qed - -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_union: - 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_unions: - assumes "finite iset" - and "\i\iset. pfn i tagged_division_of i" - and "\i1\iset. \i2\iset. i1 \ i2 \ interior(i1) \ interior(i2) = {}" - shows "\(pfn ` iset) tagged_division_of (\iset)" -proof (rule tagged_division_ofI) - note assm = tagged_division_ofD[OF assms(2)[rule_format]] - show "finite (\(pfn ` iset))" - using assms by auto - have "\{k. \x. (x, k) \ \(pfn ` iset)} = \((\i. \{k. \x. (x, k) \ pfn i}) ` iset)" - by blast - also have "\ = \iset" - using assm(6) by auto - finally show "\{k. \x. (x, k) \ \(pfn ` iset)} = \iset" . - fix x k - assume xk: "(x, k) \ \(pfn ` iset)" - then obtain i where i: "i \ iset" "(x, k) \ pfn i" - by auto - show "x \ k" "\a b. k = cbox a b" "k \ \iset" - using assm(2-4)[OF i] using i(1) by auto - fix x' k' - assume xk': "(x', k') \ \(pfn ` iset)" "(x, k) \ (x', k')" - then obtain i' where i': "i' \ iset" "(x', k') \ pfn i'" - by auto - have *: "\a b. i \ i' \ a \ i \ b \ i' \ interior a \ interior b = {}" - using i(1) i'(1) - using assms(3)[rule_format] interior_mono - by blast - show "interior k \ interior k' = {}" - apply (cases "i = i'") - using assm(5) i' i(2) xk'(2) apply blast - using "*" assm(3) i' i by auto -qed - -lemma tagged_partial_division_of_union_self: - assumes "p tagged_partial_division_of s" - shows "p tagged_division_of (\(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 - -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 - @{text operative_division}. Instances for the monoid are @{typ "'a option"}, @{typ real}, and - @{typ bool}.\ - -lemma property_empty_interval: "\a b. content (cbox a b) = 0 \ P (cbox a b) \ P {}" - using content_empty unfolding empty_as_interval by auto - -paragraph \Using additivity of lifted function to encode definedness.\ - -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 \Operative\ - -definition (in comm_monoid) operative :: "('b::euclidean_space set \ 'a) \ bool" - where "operative g \ - (\a b. content (cbox a b) = 0 \ g (cbox a b) = \<^bold>1) \ - (\a b c. \k\Basis. g (cbox a b) = g (cbox a b \ {x. x\k \ c}) \<^bold>* g (cbox a b \ {x. x\k \ c}))" - -lemma (in comm_monoid) operativeD[dest]: - assumes "operative g" - shows "\a b. content (cbox a b) = 0 \ g (cbox a b) = \<^bold>1" - and "\a b c k. k \ Basis \ g (cbox a b) = g (cbox a b \ {x. x\k \ c}) \<^bold>* g (cbox a b \ {x. x\k \ c})" - using assms unfolding operative_def by auto - -lemma (in comm_monoid) operative_empty: "operative g \ g {} = \<^bold>1" - unfolding operative_def by (rule property_empty_interval) auto - lemma operative_content[intro]: "add.operative content" - by (force simp add: add.operative_def content_split[symmetric]) - -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) *\<^sub>R i) \ i" - "\i\Basis. (\i\Basis. (if i = k then max (a \ k) c else a \ i) *\<^sub>R i) \ i \ b\i" - "min (b \ k) c = c" "max (a \ k) c = c" - using assms using less_imp_le by auto - show ?t1 (*FIXME a horrible mess*) - 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 * - apply (rule subsetI) - unfolding mem_Collect_eq split_beta - apply (erule bexE conjE)+ - apply (simp add: ) - apply (erule exE conjE)+ - proof - fix i l x - assume as: - "a \ fst x < snd x" "snd x < (if fst x = k then c else b \ fst x)" - "interval_lowerbound i \ fst x = snd x \ interval_upperbound i \ fst x = snd x" - "i = l \ {x. x \ k \ c}" "l \ d" "l \ {x. x \ k \ c} \ {}" - and fstx: "fst x \ Basis" - from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this - have *: "\i\Basis. u \ i \ (\i\Basis. (if i = k then min (v \ k) c else v \ i) *\<^sub>R i) \ i" - using as(6) unfolding l interval_split[OF k] box_ne_empty as . - have **: "\i\Basis. u\i \ v\i" - using l using as(6) unfolding box_ne_empty[symmetric] by auto - show "\i\d. interval_lowerbound i \ fst x = snd x \ interval_upperbound i \ fst x = snd x" - apply (rule bexI[OF _ \l \ d\]) - using as(1-3,5) fstx - unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as - apply (auto split: if_split_asm) - done - show "snd x < b \ fst x" - using as(2) \c < b\k\ by (auto split: if_split_asm) - qed - 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 * - unfolding subset_eq - apply rule - unfolding mem_Collect_eq split_beta - apply (erule bexE conjE)+ - apply (simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms) - apply (erule exE conjE)+ - proof - fix i l x - assume as: - "(if fst x = k then c else a \ fst x) < snd x" "snd x < b \ fst x" - "interval_lowerbound i \ fst x = snd x \ interval_upperbound i \ fst x = snd x" - "i = l \ {x. c \ x \ k}" "l \ d" "l \ {x. c \ x \ k} \ {}" - and fstx: "fst x \ Basis" - from assm(4)[OF this(5)] guess u v by (elim exE) note l=this - have *: "\i\Basis. (\i\Basis. (if i = k then max (u \ k) c else u \ i) *\<^sub>R i) \ i \ v \ i" - using as(6) unfolding l interval_split[OF k] box_ne_empty as . - have **: "\i\Basis. u\i \ v\i" - using l using as(6) unfolding box_ne_empty[symmetric] by auto - show "\i\d. interval_lowerbound i \ fst x = snd x \ interval_upperbound i \ fst x = snd x" - apply (rule bexI[OF _ \l \ d\]) - using as(1-3,5) fstx - unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as - apply (auto split: if_split_asm) - done - show "a \ fst x < snd x" - using as(1) \a\k < c\ by (auto split: if_split_asm) - qed -qed - -lemma division_points_psubset: - 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 "l \ d" - and "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 assms(2) by (auto intro!:less_imp_le) - guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this - have uv: "\i\Basis. u\i \ v\i" "\i\Basis. a\i \ u\i \ v\i \ b\i" - using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty - using subset_box(1) - apply auto - apply blast+ - done - 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] - apply - - apply (erule disjE) - apply (rule_tac x="(k,(interval_lowerbound l)\k)" in exI, force simp add: *) - apply (rule_tac x="(k,(interval_upperbound l)\k)" in exI, force simp add: *) - done - 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] - apply - - apply (erule disjE) - apply (rule_tac x="(k,(interval_lowerbound l)\k)" in exI, force simp add: *) - apply (rule_tac x="(k,(interval_upperbound l)\k)" in exI, force simp add: *) - done - moreover have "?D2 \ ?D" - by (auto simp add: assms division_points_subset) - ultimately show "?D2 \ ?D" - by blast -qed - -lemma (in comm_monoid_set) operative_division: - fixes g :: "'b::euclidean_space set \ 'a" - assumes g: "operative g" and d: "d division_of (cbox a b)" shows "F g d = g (cbox a b)" -proof - - define C where [abs_def]: "C = card (division_points (cbox a b) d)" - then show ?thesis - using d - proof (induction C arbitrary: a b d rule: less_induct) - case (less a b d) - show ?case - proof cases - show "content (cbox a b) = 0 \ F g d = g (cbox a b)" - using division_of_content_0[OF _ less.prems] operativeD(1)[OF g] division_ofD(4)[OF less.prems] - by (fastforce intro!: neutral) - next - assume "content (cbox a b) \ 0" - note ab = this[unfolded content_lt_nz[symmetric] content_pos_lt_eq] - then have ab': "\i\Basis. a\i \ b\i" - by (auto intro!: less_imp_le) - 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) *\<^sub>R (a+b) \ cbox a b" - unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps) - note this[unfolded division_ofD(6)[OF \d division_of cbox a b\,symmetric] Union_iff] - then guess i .. note i=this - guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this - 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}) = \<^bold>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 guess u v by (elim exE conjE) note uv=this - 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 "content (cbox u v) = 0" - unfolding content_eq_0 using j - by force - then show "g x = \<^bold>1" - unfolding uv(1) by (rule operativeD(1)[OF g]) - 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 guess k c - unfolding split_paired_Ex division_points_def mem_Collect_eq split_conv - apply (elim exE conjE) - done - note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']] - from this(3) guess j .. note j=this - define d1 where "d1 = {l \ {x. x\k \ c} | l. l \ d \ l \ {x. x\k \ c} \ {}}" - define d2 where "d2 = {l \ {x. x\k \ c} | l. l \ d \ l \ {x. x\k \ c} \ {}}" - define cb where "cb = (\i\Basis. (if i = k then c else b\i) *\<^sub>R i)" - define ca where "ca = (\i\Basis. (if i = k then c else a\i) *\<^sub>R i)" - note division_points_psubset[OF \d division_of cbox a b\ ab kc(1-2) j] - note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)] - then have *: "F g d1 = g (cbox a b \ {x. x\k \ c})" "F g d2 = g (cbox a b \ {x. x\k \ c})" - unfolding interval_split[OF kc(4)] - apply (rule_tac[!] "less.hyps"[rule_format]) - using division_split[OF \d division_of cbox a b\, where k=k and c=c] - apply (simp_all add: interval_split kc d1_def d2_def division_points_finite[OF \d division_of cbox a b\]) - done - { fix l y - assume as: "l \ d" "y \ d" "l \ {x. x \ k \ c} = y \ {x. x \ k \ c}" "l \ y" - from division_ofD(4)[OF \d division_of cbox a b\ this(1)] guess u v by (elim exE) note leq=this - have "g (l \ {x. x \ k \ c}) = \<^bold>1" - unfolding leq interval_split[OF kc(4)] - apply (rule operativeD[OF g]) - unfolding interval_split[symmetric, OF kc(4)] - using division_split_left_inj less as kc leq by blast - } note fxk_le = this - { fix l y - assume as: "l \ d" "y \ d" "l \ {x. c \ x \ k} = y \ {x. c \ x \ k}" "l \ y" - from division_ofD(4)[OF \d division_of cbox a b\ this(1)] guess u v by (elim exE) note leq=this - have "g (l \ {x. x \ k \ c}) = \<^bold>1" - unfolding leq interval_split[OF kc(4)] - apply (rule operativeD(1)[OF g]) - unfolding interval_split[symmetric,OF kc(4)] - using division_split_right_inj less leq as kc by blast - } note fxk_ge = this - have d1_alt: "d1 = (\l. l \ {x. x\k \ c}) ` {l \ d. l \ {x. x\k \ c} \ {}}" - using d1_def by auto - have d2_alt: "d2 = (\l. l \ {x. x\k \ c}) ` {l \ d. l \ {x. x\k \ c} \ {}}" - using d2_def by auto - have "g (cbox a b) = F g d1 \<^bold>* F g d2" (is "_ = ?prev") - unfolding * using g kc(4) by blast - also have "F g d1 = F (\l. g (l \ {x. x\k \ c})) d" - unfolding d1_alt using division_of_finite[OF less.prems] fxk_le - by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g]) - also have "F g d2 = F (\l. g (l \ {x. x\k \ c})) d" - unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge - by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g]) - also have *: "\x\d. g x = g (x \ {x. x \ k \ c}) \<^bold>* g (x \ {x. c \ x \ k})" - unfolding forall_in_division[OF \d division_of cbox a b\] - using g kc(4) by blast - have "F (\l. g (l \ {x. x\k \ c})) d \<^bold>* F (\l. g (l \ {x. x\k \ c})) d = F g d" - using * by (simp add: distrib) - finally show ?thesis by auto - qed - qed - qed -qed - -lemma (in comm_monoid_set) operative_tagged_division: - assumes f: "operative g" and d: "d tagged_division_of (cbox a b)" - shows "F (\(x, l). g l) d = g (cbox a b)" - unfolding d[THEN division_of_tagged_division, THEN operative_division[OF f], symmetric] - by (simp add: f[THEN operativeD(1)] over_tagged_division_lemma[OF d]) + by (force simp add: add.operative_def content_split[symmetric] content_eq_0_interior) lemma additive_content_division: "d division_of (cbox a b) \ setsum content d = content (cbox a b)" by (metis operative_content setsum.operative_division) @@ -1835,537 +209,8 @@ lemma content_real_eq_0: "content {a .. b::real} = 0 \ a \ b" by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0) -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 (in comm_monoid) operative_1_lt: - "operative (g :: real set \ 'a) \ - ((\a b. b \ a \ g {a .. b} = \<^bold>1) \ (\a b c. a < c \ c < b \ g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))" - apply (simp add: operative_def content_real_eq_0 atMost_def[symmetric] atLeast_def[symmetric] - del: content_real_if) -proof safe - fix a b c :: real - assume *: "\a b c. g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}" - assume "a < c" "c < b" - with *[rule_format, of a b c] show "g {a..c} \<^bold>* g {c..b} = g {a..b}" - by (simp add: less_imp_le min.absorb2 max.absorb2) -next - fix a b c :: real - assume as: "\a b. b \ a \ g {a..b} = \<^bold>1" - "\a b c. a < c \ c < b \ g {a..c} \<^bold>* g {c..b} = g {a..b}" - from as(1)[rule_format, of 0 1] as(1)[rule_format, of a a for a] as(2) - have [simp]: "g {} = \<^bold>1" "\a. g {a} = \<^bold>1" - "\a b c. a < c \ c < b \ g {a..c} \<^bold>* g {c..b} = g {a..b}" - by auto - show "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}" - by (auto simp: min_def max_def le_less) -qed - -lemma (in comm_monoid) operative_1_le: - "operative (g :: real set \ 'a) \ - ((\a b. b \ a \ g {a..b} = \<^bold>1) \ (\a b c. a \ c \ c \ b \ g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))" - unfolding operative_1_lt -proof safe - fix a b c :: real - assume as: "\a b c. a \ c \ c \ b \ g {a..c} \<^bold>* g {c..b} = g {a..b}" "a < c" "c < b" - show "g {a..c} \<^bold>* g {c..b} = g {a..b}" - apply (rule as(1)[rule_format]) - using as(2-) - apply auto - done -next - fix a b c :: real - assume "\a b. b \ a \ g {a .. b} = \<^bold>1" - and "\a b c. a < c \ c < b \ g {a..c} \<^bold>* g {c..b} = g {a..b}" - and "a \ c" - and "c \ b" - note as = this[rule_format] - show "g {a..c} \<^bold>* g {c..b} = g {a..b}" - proof (cases "c = a \ c = b") - case False - then show ?thesis - apply - - apply (subst as(2)) - using as(3-) - apply auto - done - next - case True - then show ?thesis - proof - assume *: "c = a" - then have "g {a .. c} = \<^bold>1" - apply - - apply (rule as(1)[rule_format]) - apply auto - done - then show ?thesis - unfolding * by auto - next - assume *: "c = b" - then have "g {c .. b} = \<^bold>1" - apply - - apply (rule as(1)[rule_format]) - apply auto - done - then show ?thesis - unfolding * by auto - qed - qed -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_inter: "(\x. d1 x \ d2 x) fine p \ d1 fine p \ d2 fine p" - unfolding fine_def by auto - -lemma fine_inters: - "(\x. \{f d x | d. d \ s}) fine p \ (\d\s. (f d) fine p)" - unfolding fine_def by blast - -lemma fine_union: "d fine p1 \ d fine p2 \ d fine (p1 \ p2)" - unfolding fine_def by blast - -lemma fine_unions: "(\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_unions_exists: - assumes "finite iset" - and "\i\iset. \p. p tagged_division_of i \ d fine p" - and "\i1\iset. \i2\iset. i1 \ i2 \ interior i1 \ interior i2 = {}" - and "\iset = i" - obtains p where "p tagged_division_of i" and "d fine p" -proof - - obtain pfn where pfn: - "\x. x \ iset \ pfn x tagged_division_of x" - "\x. x \ iset \ d fine pfn x" - using bchoice[OF assms(2)] by auto - show thesis - apply (rule_tac p="\(pfn ` iset)" in that) - using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force - by (metis (mono_tags, lifting) fine_unions imageE pfn(2)) -qed - - -subsection \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 "P {}" - and "\s t. P s \ P t \ interior(s) \ interior(t) = {} \ P (s \ t)" - and "\ P (cbox a (b::'a))" - obtains c d where "\ P (cbox c d)" - and "\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 assms(1,3) by metis - then have ab: "\i. i\Basis \ a \ i \ b \ i" - by (force simp: mem_box) - { fix f - have "\finite f; - \s. s\f \ P s; - \s. s\f \ \a b. s = cbox a b; - \s t. s\f \ t\f \ s \ t \ interior s \ interior t = {}\ \ P (\f)" - proof (induct f rule: finite_induct) - case empty - show ?case - using assms(1) by auto - next - case (insert x f) - show ?case - unfolding Union_insert - apply (rule assms(2)[rule_format]) - using inter_interior_unions_intervals [of f "interior x"] - apply (auto simp: insert) - by (metis IntI empty_iff insert.hyps(2) insert.prems(3) insert_iff) - qed - } note UN_cases = this - let ?A = "{cbox c d | c d::'a. \i\Basis. (c\i = a\i) \ (d\i = (a\i + b\i) / 2) \ - (c\i = (a\i + b\i) / 2) \ (d\i = b\i)}" - let ?PP = "\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" - { - presume "\c d. ?PP c d \ P (cbox c d) \ False" - then show thesis - unfolding atomize_not not_all - by (blast intro: that) - } - assume as: "\c d. ?PP c d \ P (cbox c d)" - have "P (\?A)" - proof (rule UN_cases) - let ?B = "(\s. cbox (\i\Basis. (if i \ s then a\i else (a\i + b\i) / 2) *\<^sub>R i::'a) - (\i\Basis. (if i \ s then (a\i + b\i) / 2 else b\i) *\<^sub>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 = (a \ i + b \ i) / 2 \ - c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" by blast - show "x \ ?B" - unfolding image_iff x - apply (rule_tac x="{i. i\Basis \ c\i = a\i}" in bexI) - apply (rule arg_cong2 [where f = cbox]) - using x(2) ab - apply (auto simp add: euclidean_eq_iff[where 'a='a]) - by fastforce - qed - then show "finite ?A" - by (rule finite_subset) auto - next - fix s - assume "s \ ?A" - then obtain c d - where s: "s = cbox c d" - "\i. i \ Basis \ - c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ - c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" - by blast - show "P s" - unfolding s - apply (rule as[rule_format]) - using ab s(2) by force - 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 = (a \ i + b \ i) / 2 \ - e \ i = (a \ i + b \ i) / 2 \ 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'] - proof safe - assume as: "c \ i = a \ i" "d \ i = (a \ i + b \ i) / 2" - show False - using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps) - next - assume as: "c \ i = (a \ i + b \ i) / 2" "d \ i = b \ i" - show False - using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps) - qed - 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 = (a \ i + b \ i) / 2 \ - c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" - by blast - show "x\cbox a b" - unfolding mem_box - proof safe - fix i :: 'a - assume i: "i \ Basis" - then show "a \ i \ x \ i" "x \ i \ b \ i" - using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto - qed - next - fix x - assume x: "x \ cbox a b" - have "\i\Basis. - \c d. (c = a\i \ d = (a\i + b\i) / 2 \ c = (a\i + b\i) / 2 \ d = b\i) \ c\x\i \ x\i \ d" - (is "\i\Basis. \c d. ?P i c d") - unfolding mem_box - proof - fix i :: 'a - assume i: "i \ Basis" - have "?P i (a\i) ((a \ i + b \ i) / 2) \ ?P i ((a \ i + b \ i) / 2) (b\i)" - using x[unfolded mem_box,THEN bspec, OF i] by auto - then show "\c d. ?P i c d" - by blast - qed - then show "x\\?A" - unfolding Union_iff Bex_def mem_Collect_eq choice_Basis_iff - apply auto - apply (rule_tac x="cbox xa xaa" in exI) - unfolding mem_box - apply auto - done - qed - finally show False - using assms by auto -qed - -lemma interval_bisection: - fixes type :: "'a::euclidean_space" - assumes "P {}" - and "(\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 as: False - obtain c d where "\ P (cbox c d)" - "\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 (rule interval_bisection_step[of P, OF assms(1-2) as]) - then show ?thesis - apply - - apply (rule_tac x="(c,d)" in exI) - apply auto - done - qed - qed - then obtain f where f: - "\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)" - apply - - apply (drule choice) - apply blast - done - 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 "A 0 = a" "B 0 = b" "\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 - apply (rule f[rule_format]) using assms(3) - apply auto - done - next - case (Suc n) - show ?case - unfolding S - apply (rule f[rule_format]) - using Suc - unfolding S - apply auto - done - qed - qed - note AB = this(1-2) conjunctD2[OF this(3),rule_format] - - 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 "(setsum (\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 \ setsum (\i. \(x - y)\i\) Basis" - unfolding dist_norm by(rule norm_le_l1) - also have "\ \ setsum (\i. B n\i - A n\i) Basis" - proof (rule setsum_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 "\ \ setsum (\i. b\i - a\i) Basis / 2^n" - unfolding setsum_divide_distrib - proof (rule setsum_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(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(4) by (intro order_trans[OF step.IH] subset_box_imp) auto - qed simp - } note ABsubset = this - have "\a. \n. a\ cbox (A n) (B n)" - by (rule decreasing_closed_nest[rule_format,OF closed_cbox _ ABsubset interv]) - (metis nat.exhaust AB(1-3) assms(1,3)) - then obtain x0 where x0: "\n. x0 \ cbox (A n) (B n)" - by blast - show thesis - proof (rule that[rule_format, of x0]) - show "x0\cbox a b" - using x0[of 0] unfolding AB . - 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))" - apply (cases "0 < n") - using AB(3)[of "n - 1"] assms(3) AB(1-2) - apply auto - done - 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" - unfolding AB(1-2)[symmetric] by (rule ABsubset) auto - 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 - - presume "\ (\p. p tagged_division_of (cbox a b) \ g fine p) \ False" - then obtain p where "p tagged_division_of (cbox a b)" "g fine p" - by blast - then show thesis .. -next - assume as: "\ (\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 _ _ as]) - apply (simp add: fine_def) - apply (metis tagged_division_union fine_union) - apply (auto simp: ) - 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 False - 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 \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})" - -lemma eventually_division_filter: - "(\\<^sub>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_inter) -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 +lemma property_empty_interval: "\a b. content (cbox a b) = 0 \ P (cbox a b) \ P {}" + using content_empty unfolding empty_as_interval by auto subsection \Gauge integral\ @@ -2443,26 +288,6 @@ lemma has_integral_integral: "f integrable_on s \ (f has_integral (integral s f)) s" by auto -lemma setsum_content_null: - assumes "content (cbox a b) = 0" - and "p tagged_division_of (cbox a b)" - shows "setsum (\(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)" -proof (rule setsum.neutral, rule) - fix y - assume y: "y \ p" - obtain x k where xk: "y = (x, k)" - using surj_pair[of y] by blast - note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]] - from this(2) obtain c d where k: "k = cbox c d" by blast - have "(\(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x" - unfolding xk by auto - also have "\ = 0" - using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d] - unfolding assms(1) k - by auto - finally show "(\(x, k). content k *\<^sub>R f x) y = 0" . -qed - subsection \Basic theorems about integrals.\ lemma has_integral_unique: @@ -3175,38 +1000,32 @@ subsection \Additivity of integral on abutting intervals.\ -lemma tagged_division_split_left_inj: - fixes x1 :: "'a::euclidean_space" +lemma tagged_division_split_left_inj_content: assumes d: "d tagged_division_of i" - and k12: "(x1, k1) \ d" - "(x2, k2) \ d" - "k1 \ k2" - "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" - "k \ Basis" + and "(x1, k1) \ d" "(x2, k2) \ d" "k1 \ k2" "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" "k \ Basis" shows "content (k1 \ {x. x\k \ c}) = 0" proof - - have *: "\a b c. (a,b) \ c \ b \ snd ` c" - by force + from tagged_division_ofD(4)[OF d \(x1, k1) \ d\] obtain a b where k1: "k1 = cbox a b" + by auto show ?thesis - using k12 - by (fastforce intro!: division_split_left_inj[OF division_of_tagged_division[OF d]] *) + unfolding k1 interval_split[OF \k \ Basis\] + unfolding content_eq_0_interior + unfolding interval_split[OF \k \ Basis\, symmetric] k1[symmetric] + by (rule tagged_division_split_left_inj[OF assms]) qed -lemma tagged_division_split_right_inj: - fixes x1 :: "'a::euclidean_space" +lemma tagged_division_split_right_inj_content: assumes d: "d tagged_division_of i" - and k12: "(x1, k1) \ d" - "(x2, k2) \ d" - "k1 \ k2" - "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" - "k \ Basis" + and "(x1, k1) \ d" "(x2, k2) \ d" "k1 \ k2" "k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c}" "k \ Basis" shows "content (k1 \ {x. x\k \ c}) = 0" proof - - have *: "\a b c. (a,b) \ c \ b \ snd ` c" - by force + from tagged_division_ofD(4)[OF d \(x1, k1) \ d\] obtain a b where k1: "k1 = cbox a b" + by auto show ?thesis - using k12 - by (fastforce intro!: division_split_right_inj[OF division_of_tagged_division[OF d]] *) + unfolding k1 interval_split[OF \k \ Basis\] + unfolding content_eq_0_interior + unfolding interval_split[OF \k \ Basis\, symmetric] k1[symmetric] + by (rule tagged_division_split_right_inj[OF assms]) qed lemma has_integral_split: @@ -3284,7 +1103,8 @@ have lem1: "\f P Q. (\x k. (x, k) \ {(x, f k) | x k. P x k} \ Q x k) \ (\x k. P x k \ Q x (f k))" by auto - have fin_finite: "finite {(x,f k) | x k. (x,k) \ s \ P x k}" if "finite s" for f s P + have fin_finite: "finite {(x,f k) | x k. (x,k) \ s \ P x k}" + if "finite s" for s and f :: "'a set \ 'a set" and P :: "'a \ 'a set \ bool" proof - from that have "finite ((\(x, k). (x, f k)) ` s)" by auto @@ -3398,8 +1218,9 @@ also have "\ = (\(x, ka)\p. content (ka \ {x. x \ k \ c}) *\<^sub>R f x) + (\(x, ka)\p. content (ka \ {x. c \ x \ k}) *\<^sub>R f x) - (i + j)" unfolding lem3[OF p(3)] - by (subst setsum.reindex_nontrivial[OF p(3)], auto intro!: k eq0 tagged_division_split_left_inj[OF p(1)] tagged_division_split_right_inj[OF p(1)] - simp: cont_eq)+ + by (subst (1 2) setsum.reindex_nontrivial[OF p(3)]) + (auto intro!: k eq0 tagged_division_split_left_inj_content[OF p(1)] tagged_division_split_right_inj_content[OF p(1)] + simp: cont_eq)+ also note setsum.distrib[symmetric] also have "\x. x \ p \ (\(x,ka). content (ka \ {x. x \ k \ c}) *\<^sub>R f x) x + @@ -3429,34 +1250,6 @@ subsection \A sort of converse, integrability on subintervals.\ -lemma tagged_division_union_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_union[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_union_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_union_interval) - lemma has_integral_separate_sides: fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" assumes "(f has_integral i) (cbox a b)" @@ -3621,10 +1414,10 @@ qed next fix a b :: 'a - assume "content (cbox a b) = 0" + assume "box a b = {}" then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0" using has_integral_null_eq - by (auto simp: integrable_on_null) + by (auto simp: integrable_on_null content_eq_0_interior) qed qed @@ -4069,47 +1862,6 @@ subsection \Negligibility of hyperplane.\ -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) *\<^sub>R i) - (\i\Basis. (if i = k then min (b\k) (c + e) else b\i) *\<^sub>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]) - apply (rule equalityI) - apply blast - apply clarsimp - apply (rule_tac x="l \ {x. c + e \ x \ k}" in exI) - apply auto - done - by (simp add: interval_split k interval_doublesplit) -qed - lemma content_doublesplit: fixes a :: "'a::euclidean_space" assumes "0 < e" @@ -4262,6 +2014,8 @@ also have "\ < e" proof (subst setsum.over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases) case prems: (1 u v) + then have *: "content (cbox u v) = 0" + unfolding content_eq_0_interior by simp have "content (cbox u v \ {x. \x \ k - c\ \ d}) \ content (cbox u v)" unfolding interval_doublesplit[OF k] apply (rule content_subset) @@ -4269,7 +2023,7 @@ apply auto done then show ?case - unfolding prems interval_doublesplit[OF k] + unfolding * interval_doublesplit[OF k] by (blast intro: antisym) next have "(\l\snd ` p. content (l \ {x. \x \ k - c\ \ d})) = @@ -4303,188 +2057,9 @@ qed -subsection \A technical lemma about "refinement" of division.\ - -lemma tagged_division_finer: - fixes p :: "('a::euclidean_space \ ('a::euclidean_space set)) set" - assumes "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 - - let ?P = "\p. p tagged_partial_division_of (cbox a b) \ gauge d \ - (\q. q tagged_division_of (\{k. \x. (x,k) \ p}) \ d fine q \ - (\(x,k) \ p. k \ d(x) \ (x,k) \ q))" - { - have *: "finite p" "p tagged_partial_division_of (cbox a b)" - using assms(1) - unfolding tagged_division_of_def - by auto - presume "\p. finite p \ ?P p" - from this[rule_format,OF * assms(2)] guess q .. note q=this - then show ?thesis - apply - - apply (rule that[of q]) - unfolding tagged_division_ofD[OF assms(1)] - apply auto - done - } - fix p :: "('a::euclidean_space \ ('a::euclidean_space set)) set" - assume as: "finite p" - show "?P p" - apply rule - apply rule - using as - proof (induct p) - case empty - show ?case - apply (rule_tac x="{}" in exI) - unfolding fine_def - apply auto - done - next - case (insert xk p) - guess x k using surj_pair[of xk] by (elim exE) note xk=this - note tagged_partial_division_subset[OF insert(4) subset_insertI] - from insert(3)[OF this insert(5)] guess q1 .. note q1 = conjunctD3[OF this] - 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)] - from p(4)[unfolded xk, OF insertI1] guess u v by (elim exE) note uv=this - - have "finite {k. \x. (x, k) \ p}" - apply (rule finite_subset[of _ "snd ` p"]) - using p - apply safe - apply (metis image_iff snd_conv) - apply auto - done - then have int: "interior (cbox u v) \ interior (\{k. \x. (x, k) \ p}) = {}" - apply (rule inter_interior_unions_intervals) - apply (rule open_interior) - apply (rule_tac[!] ballI) - unfolding mem_Collect_eq - apply (erule_tac[!] exE) - apply (drule p(4)[OF insertI2]) - apply assumption - apply (rule p(5)) - unfolding uv xk - apply (rule insertI1) - apply (rule insertI2) - apply assumption - using insert(2) - unfolding uv xk - apply auto - done - show ?case - proof (cases "cbox u v \ d x") - case True - then show ?thesis - apply (rule_tac x="{(x,cbox u v)} \ q1" in exI) - apply rule - unfolding * uv - apply (rule tagged_division_union) - apply (rule tagged_division_of_self) - apply (rule p[unfolded xk uv] insertI1)+ - apply (rule q1) - apply (rule int) - apply rule - apply (rule fine_union) - apply (subst fine_def) - defer - apply (rule q1) - unfolding Ball_def split_paired_All split_conv - apply rule - apply rule - apply rule - apply rule - apply (erule insertE) - apply (simp add: uv xk) - apply (rule UnI2) - apply (drule q1(3)[rule_format]) - unfolding xk uv - apply auto - done - next - case False - from fine_division_exists[OF assms(2), of u v] guess q2 . note q2=this - show ?thesis - apply (rule_tac x="q2 \ q1" in exI) - apply rule - unfolding * uv - apply (rule tagged_division_union q2 q1 int fine_union)+ - unfolding Ball_def split_paired_All split_conv - apply rule - apply (rule fine_union) - apply (rule q1 q2)+ - apply rule - apply rule - apply rule - apply rule - apply (erule insertE) - apply (rule UnI2) - apply (simp add: False uv xk) - apply (drule q1(3)[rule_format]) - using False - unfolding xk uv - apply auto - done - qed - qed -qed - subsection \Hence the main theorem about negligible sets.\ -lemma finite_product_dependent: - assumes "finite s" - and "\x. x \ s \ finite (t x)" - shows "finite {(i, j) |i j. i \ s \ j \ t i}" - using assms -proof induct - case (insert x s) - have *: "{(i, j) |i j. i \ insert x s \ j \ t i} = - (\y. (x,y)) ` (t x) \ {(i, j) |i j. i \ s \ j \ t i}" by auto - show ?case - unfolding * - apply (rule finite_UnI) - using insert - apply auto - done -qed auto - -lemma sum_sum_product: - assumes "finite s" - and "\i\s. finite (t i)" - shows "setsum (\i. setsum (x i) (t i)::real) s = - setsum (\(i,j). x i j) {(i,j) | i j. i \ s \ j \ t i}" - using assms -proof induct - case (insert a s) - have *: "{(i, j) |i j. i \ insert a s \ j \ t i} = - (\y. (a,y)) ` (t a) \ {(i, j) |i j. i \ s \ j \ t i}" by auto - show ?case - unfolding * - apply (subst setsum.union_disjoint) - unfolding setsum.insert[OF insert(1-2)] - prefer 4 - apply (subst insert(3)) - unfolding add_right_cancel - proof - - show "setsum (x a) (t a) = (\(xa, y)\ Pair a ` t a. x xa y)" - apply (subst setsum.reindex) - unfolding inj_on_def - apply auto - done - show "finite {(i, j) |i j. i \ s \ j \ t i}" - apply (rule finite_product_dependent) - using insert - apply auto - done - qed (insert insert, auto) -qed auto - lemma has_integral_negligible: fixes f :: "'b::euclidean_space \ 'a::real_normed_vector" assumes "negligible s" @@ -4937,10 +2512,10 @@ proof safe fix a b :: 'b show "\g. (\x\cbox a b. norm (f x - g x) \ e) \ g integrable_on cbox a b" - if "content (cbox a b) = 0" + if "box a b = {}" apply (rule_tac x=f in exI) using assms that - apply (auto intro!: integrable_on_null) + apply (auto simp: content_eq_0_interior) done { fix c g @@ -5059,33 +2634,6 @@ subsection \Specialization of additivity to one dimension.\ -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 "setsum (\(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))" - have ***: "\i\Basis. a \ i \ b \ i" - using assms by auto - have *: "add.operative ?f" - unfolding add.operative_1_lt box_eq_empty - by auto - have **: "cbox a b \ {}" - using assms(1) by auto - note setsum.operative_tagged_division[OF * assms(2)[simplified box_real[symmetric]]] - note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric] - show ?thesis - unfolding * - apply (rule setsum.cong) - unfolding split_paired_all split_conv - using assms(2) - apply auto - done -qed - subsection \A useful lemma allowing us to factor out the content size.\ @@ -5373,20 +2921,6 @@ qed -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 - apply safe - defer - apply (erule_tac x="f x" in allE) - apply (erule_tac x="d (f x)" in allE) - apply auto - done - subsection \Only need trivial subintervals if the interval itself is trivial.\ @@ -5524,10 +3058,12 @@ shows "comm_monoid.operative op \ True (\i. f integrable_on i)" unfolding comm_monoid.operative_def[OF comm_monoid_and] apply safe - apply (subst integrable_on_def) - unfolding has_integral_null_eq - apply (rule, rule refl) - apply (rule, assumption, assumption)+ + apply (subst integrable_on_def) + apply rule + apply (rule has_integral_null_eq[where i=0, THEN iffD2]) + apply (simp add: content_eq_0_interior) + apply rule + apply (rule, assumption, assumption)+ unfolding integrable_on_def by (auto intro!: has_integral_split) @@ -6121,18 +3657,6 @@ subsection \Stronger form of FCT; quite a tedious proof.\ -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) - -lemma additive_tagged_division_1': - fixes f :: "real \ 'a::real_normed_vector" - assumes "a \ b" - and "p tagged_division_of {a..b}" - shows "setsum (\(x,k). f (Sup k) - f(Inf k)) p = f b - f a" - using additive_tagged_division_1[OF _ assms(2), of f] - using assms(1) - by auto - lemma split_minus[simp]: "(\(x, k). f x k) x - (\(x, k). g x k) x = (\(x, k). f x k - g x k) x" by (simp add: split_def) @@ -7717,39 +5241,6 @@ shows "f integrable_on s \ f integrable_on t" by (blast intro: integrable_spike_set assms negligible_subset) -(*lemma integral_spike_set: - "\f:real^M->real^N g s t. - negligible(s DIFF t \ t DIFF s) - \ integral s f = integral t f" -qed REPEAT STRIP_TAC THEN REWRITE_TAC[integral] THEN - AP_TERM_TAC THEN ABS_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN - ASM_MESON_TAC[]);; - -lemma has_integral_interior: - "\f:real^M->real^N y s. - negligible(frontier s) - \ ((f has_integral y) (interior s) \ (f has_integral y) s)" -qed REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN - FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] - NEGLIGIBLE_SUBSET)) THEN - REWRITE_TAC[frontier] THEN - MP_TAC(ISPEC `s:real^M->bool` INTERIOR_SUBSET) THEN - MP_TAC(ISPEC `s:real^M->bool` CLOSURE_SUBSET) THEN - SET_TAC[]);; - -lemma has_integral_closure: - "\f:real^M->real^N y s. - negligible(frontier s) - \ ((f has_integral y) (closure s) \ (f has_integral y) s)" -qed REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN - FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] - NEGLIGIBLE_SUBSET)) THEN - REWRITE_TAC[frontier] THEN - MP_TAC(ISPEC `s:real^M->bool` INTERIOR_SUBSET) THEN - MP_TAC(ISPEC `s:real^M->bool` CLOSURE_SUBSET) THEN - SET_TAC[]);;*) - - subsection \More lemmas that are useful later\ lemma has_integral_subset_component_le: @@ -8434,34 +5925,26 @@ subsection \Also tagged divisions\ +lemma has_integral_iff: "(f has_integral i) s \ (f integrable_on s \ integral s f = i)" + by blast + lemma has_integral_combine_tagged_division: fixes f :: "'n::euclidean_space \ 'a::banach" assumes "p tagged_division_of s" and "\(x,k) \ p. (f has_integral (i k)) k" - shows "(f has_integral (setsum (\(x,k). i k) p)) s" + shows "(f has_integral (\(x,k)\p. i k)) s" proof - - have *: "(f has_integral (setsum (\k. integral k f) (snd ` p))) s" - apply (rule has_integral_combine_division) - apply (rule division_of_tagged_division[OF assms(1)]) + have *: "(f has_integral (\k\snd`p. integral k f)) s" using assms(2) - unfolding has_integral_integral[symmetric] - apply safe + apply (intro has_integral_combine_division) + apply (auto simp: has_integral_integral[symmetric] intro: division_of_tagged_division[OF assms(1)]) apply auto done - then show ?thesis - apply - - apply (rule subst[where P="\i. (f has_integral i) s"]) - defer - apply assumption - apply (rule trans[of _ "setsum (\(x,k). integral k f) p"]) - apply (subst eq_commute) - apply (rule setsum.over_tagged_division_lemma[OF assms(1)]) - apply (rule integral_null) - apply assumption - apply (rule setsum.cong) - using assms(2) - apply auto - done + also have "(\k\snd`p. integral k f) = (\(x, k)\p. integral k f)" + by (intro setsum.over_tagged_division_lemma[OF assms(1), symmetric] integral_null) + (simp add: content_eq_0_interior) + finally show ?thesis + using assms by (auto simp add: has_integral_iff intro!: setsum.cong) qed lemma integral_combine_tagged_division_bottomup: @@ -9616,84 +7099,6 @@ subsection \differentiation under the integral sign\ -lemma tube_lemma: - assumes "compact K" - assumes "open W" - assumes "{x0} \ K \ W" - shows "\X0. x0 \ X0 \ open X0 \ X0 \ K \ W" -proof - - { - fix y assume "y \ K" - then have "(x0, y) \ W" using assms by auto - with \open W\ - have "\X0 Y. open X0 \ open Y \ x0 \ X0 \ y \ Y \ X0 \ Y \ W" - by (rule open_prod_elim) blast - } - then obtain X0 Y where - *: "\y \ K. open (X0 y) \ open (Y y) \ x0 \ X0 y \ y \ Y y \ X0 y \ Y y \ W" - by metis - from * have "\t\Y ` K. open t" "K \ \(Y ` K)" by auto - with \compact K\ obtain CC where CC: "CC \ Y ` K" "finite CC" "K \ \CC" - by (rule compactE) - then obtain c where c: "\C. C \ CC \ c C \ K \ C = Y (c C)" - by (force intro!: choice) - with * CC show ?thesis - by (force intro!: exI[where x="\C\CC. X0 (c C)"]) (* SLOW *) -qed - -lemma continuous_on_prod_compactE: - fixes fx::"'a::topological_space \ 'b::topological_space \ 'c::metric_space" - and e::real - assumes cont_fx: "continuous_on (U \ C) fx" - assumes "compact C" - assumes [intro]: "x0 \ U" - notes [continuous_intros] = continuous_on_compose2[OF cont_fx] - assumes "e > 0" - obtains X0 where "x0 \ X0" "open X0" - "\x\X0 \ U. \t \ C. dist (fx (x, t)) (fx (x0, t)) \ e" -proof - - define psi where "psi = (\(x, t). dist (fx (x, t)) (fx (x0, t)))" - define W0 where "W0 = {(x, t) \ U \ C. psi (x, t) < e}" - have W0_eq: "W0 = psi -` {.. U \ C" - by (auto simp: vimage_def W0_def) - have "open {.. C) psi" - by (auto intro!: continuous_intros simp: psi_def split_beta') - from this[unfolded continuous_on_open_invariant, rule_format, OF \open {..] - obtain W where W: "open W" "W \ U \ C = W0 \ U \ C" - unfolding W0_eq by blast - have "{x0} \ C \ W \ U \ C" - unfolding W - by (auto simp: W0_def psi_def \0 < e\) - then have "{x0} \ C \ W" by blast - from tube_lemma[OF \compact C\ \open W\ this] - obtain X0 where X0: "x0 \ X0" "open X0" "X0 \ C \ W" - by blast - - have "\x\X0 \ U. \t \ C. dist (fx (x, t)) (fx (x0, t)) \ e" - proof safe - fix x assume x: "x \ X0" "x \ U" - fix t assume t: "t \ C" - have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)" - by (auto simp: psi_def) - also - { - have "(x, t) \ X0 \ C" - using t x - by auto - also note \\ \ W\ - finally have "(x, t) \ W" . - with t x have "(x, t) \ W \ U \ C" - by blast - also note \W \ U \ C = W0 \ U \ C\ - finally have "psi (x, t) < e" - by (auto simp: W0_def) - } - finally show "dist (fx (x, t)) (fx (x0, t)) \ e" by simp - qed - from X0(1,2) this show ?thesis .. -qed - lemma integral_continuous_on_param: fixes f::"'a::topological_space \ 'b::euclidean_space \ 'c::banach" assumes cont_fx: "continuous_on (U \ cbox a b) (\(x, t). f x t)" @@ -9743,26 +7148,6 @@ qed qed (auto intro!: continuous_on_const) -lemma eventually_closed_segment: - fixes x0::"'a::real_normed_vector" - assumes "open X0" "x0 \ X0" - shows "\\<^sub>F x in at x0 within U. closed_segment x0 x \ X0" -proof - - from openE[OF assms] - obtain e where e: "0 < e" "ball x0 e \ X0" . - then have "\\<^sub>F x in at x0 within U. x \ ball x0 e" - by (auto simp: dist_commute eventually_at) - then show ?thesis - proof eventually_elim - case (elim x) - have "x0 \ ball x0 e" using \e > 0\ by simp - from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim] - have "closed_segment x0 x \ ball x0 e" . - also note \\ \ X0\ - finally show ?case . - qed -qed - lemma leibniz_rule: fixes f::"'a::banach \ 'b::euclidean_space \ 'c::banach" assumes fx: "\x t. x \ U \ t \ cbox a b \ @@ -9856,8 +7241,7 @@ qed (rule blinfun.bounded_linear_right) qed (auto intro!: derivative_eq_intros simp: blinfun.bilinear_simps) -lemma - has_vector_derivative_eq_has_derivative_blinfun: +lemma has_vector_derivative_eq_has_derivative_blinfun: "(f has_vector_derivative f') (at x within U) \ (f has_derivative blinfun_scaleR_left f') (at x within U)" by (simp add: has_vector_derivative_def) @@ -9889,8 +7273,7 @@ done qed -lemma - has_field_derivative_eq_has_derivative_blinfun: +lemma has_field_derivative_eq_has_derivative_blinfun: "(f has_field_derivative f') (at x within U) \ (f has_derivative blinfun_mult_right f') (at x within U)" by (simp add: has_field_derivative_def) @@ -9922,8 +7305,7 @@ subsection \Exchange uniform limit and integral\ -lemma - uniform_limit_integral: +lemma uniform_limit_integral: fixes f::"'a \ 'b::euclidean_space \ 'c::banach" assumes u: "uniform_limit (cbox a b) f g F" assumes c: "\n. continuous_on (cbox a b) (f n)" @@ -10117,18 +7499,6 @@ subsection \Compute a double integral using iterated integrals and switching the order of integration\ -lemma setcomp_dot1: "{z. P (z \ (i,0))} = {(x,y). P(x \ i)}" - by auto - -lemma setcomp_dot2: "{z. P (z \ (0,i))} = {(x,y). P(y \ i)}" - by auto - -lemma Sigma_Int_Paircomp1: "(Sigma A B) \ {(x, y). P x} = Sigma (A \ {x. P x}) B" - by blast - -lemma Sigma_Int_Paircomp2: "(Sigma A B) \ {(x, y). P y} = Sigma A (\z. B z \ {y. P y})" - by blast - lemma continuous_on_imp_integrable_on_Pair1: fixes f :: "_ \ 'b::banach" assumes con: "continuous_on (cbox (a,c) (b,d)) f" and x: "x \ cbox a b" @@ -10180,11 +7550,6 @@ done qed -lemma norm_diff2: "\y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \ e1; norm(y2 - x2) \ e2\ - \ norm(y - x) \ e" -using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"] - by (simp add: add_diff_add) - lemma integral_split: fixes f :: "'a::euclidean_space \ 'b::{real_normed_vector,complete_space}" assumes f: "f integrable_on (cbox a b)" @@ -10208,9 +7573,11 @@ \ e * content (cbox (a,c) (b,d)))" proof (auto simp: comm_monoid.operative_def[OF comm_monoid_and]) fix a::'a and c::'b and b::'a and d::'b and u::'a and v::'a and w::'b and z::'b - assume c0: "content (cbox (a, c) (b, d)) = 0" + assume *: "box (a, c) (b, d) = {}" and cb1: "cbox (u, w) (v, z) \ cbox (a, c) (b, d)" and cb2: "cbox (u, w) (v, z) \ s" + then have c0: "content (cbox (a, c) (b, d)) = 0" + using * unfolding content_eq_0_interior by simp have c0': "content (cbox (u, w) (v, z)) = 0" by (fact content_0_subset [OF c0 cb1]) show "norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\x. integral (cbox w z) (\y. f (x, y)))) @@ -10296,9 +7663,6 @@ integral (cbox a b) (\x. integral (cbox c d) (\y. k))" by (simp add: content_Pair) -lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)" - by (simp add: norm_minus_eqI) - lemma integral_prod_continuous: fixes f :: "('a::euclidean_space * 'b::euclidean_space) \ 'c::banach" assumes "continuous_on (cbox (a,c) (b,d)) f" (is "continuous_on ?CBOX f") @@ -10414,20 +7778,6 @@ by simp qed -lemma swap_continuous: - assumes "continuous_on (cbox (a,c) (b,d)) (\(x,y). f x y)" - shows "continuous_on (cbox (c,a) (d,b)) (\(x, y). f y x)" -proof - - have "(\(x, y). f y x) = (\(x, y). f x y) \ prod.swap" - by auto - then show ?thesis - apply (rule ssubst) - apply (rule continuous_on_compose) - apply (simp add: split_def) - apply (rule continuous_intros | simp add: assms)+ - done -qed - lemma integral_swap_2dim: fixes f :: "['a::euclidean_space, 'b::euclidean_space] \ 'c::banach" assumes "continuous_on (cbox (a,c) (b,d)) (\(x,y). f x y)" @@ -10731,277 +8081,6 @@ (insert assms, simp_all add: powr_minus powr_realpow divide_simps) 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)) *\<^sub>R i) - (\i \ Basis. (a \ i + ((f i + 1) / 2^n) * (b \ i - a \ i)) *\<^sub>R i)" - let ?D0 = "?K0 ` (SIGMA n:UNIV. PiE 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: divide_simps zero_le_mult_iff aibi) - apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem) - 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: divide_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 --\The symmetry argument requires a single HOL formula\ - proof (rule linorder_wlog [where a=m and b=n], intro allI impI) - fix v w m and n::nat - assume "m \ n" --\WLOG we can assume @{term"m \ n"}, when the first disjunct becomes impossible\ - 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 add: power_add, 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 \\<^sub>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 setsum.cong) - also have "... \ DIM('a) * (\ / (2 * real DIM('a)))" - by (meson setsum_bounded_above that) - also have "... = \ / 2" - by (simp add: divide_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: divide_simps) - then have "norm (b - a) < e * 2^n" - by (auto simp: divide_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 divide_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 divide_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 divide_simps) - done - also have "... = x \ i" - using abi_less by (simp add: divide_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: divide_simps algebra_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 \\<^sub>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 by (force simp: algebra_simps) - 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 \\<^sub>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)) *\<^sub>R i) - (\i\Basis. (a \ i + ((f i) + 1) / 2^n * (b \ i - a \ i)) *\<^sub>R i)) - ` (SIGMA m:atMost n. PiE Basis (\i::'a. lessThan (2^m)))" - have "?K0(m,g) \ ?B" if "g \ Basis \\<^sub>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: divide_simps algebra_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 algebra_simps divide_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 real_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 - subsubsection \Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\ lemma integral_component_eq_cart[simp]: diff -r b235e845c8e8 -r c3da799b1b45 src/HOL/Analysis/Tagged_Division.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Tagged_Division.thy Thu Sep 29 13:02:43 2016 +0200 @@ -0,0 +1,2817 @@ +(* Title: HOL/Analysis/Tagged_Division.thy + Author: John Harrison + Author: Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP +*) + +section \Tagged divisions used for the Henstock-Kurzweil gauge integration\ + +theory Tagged_Division +imports + Topology_Euclidean_Space +begin + +lemma finite_product_dependent: + assumes "finite s" + and "\x. x \ s \ finite (t x)" + shows "finite {(i, j) |i j. i \ s \ j \ t i}" + using assms +proof induct + case (insert x s) + have *: "{(i, j) |i j. i \ insert x s \ j \ t i} = + (\y. (x,y)) ` (t x) \ {(i, j) |i j. i \ s \ j \ t i}" by auto + show ?case + unfolding * + apply (rule finite_UnI) + using insert + apply auto + done +qed auto + +lemma sum_sum_product: + assumes "finite s" + and "\i\s. finite (t i)" + shows "setsum (\i. setsum (x i) (t i)::real) s = + setsum (\(i,j). x i j) {(i,j) | i j. i \ s \ j \ t i}" + using assms +proof induct + case (insert a s) + have *: "{(i, j) |i j. i \ insert a s \ j \ t i} = + (\y. (a,y)) ` (t a) \ {(i, j) |i j. i \ s \ j \ t i}" by auto + show ?case + unfolding * + apply (subst setsum.union_disjoint) + unfolding setsum.insert[OF insert(1-2)] + prefer 4 + apply (subst insert(3)) + unfolding add_right_cancel + proof - + show "setsum (x a) (t a) = (\(xa, y)\ Pair a ` t a. x xa y)" + apply (subst setsum.reindex) + unfolding inj_on_def + apply auto + done + show "finite {(i, j) |i j. i \ s \ j \ t i}" + apply (rule finite_product_dependent) + using insert + apply auto + done + qed (insert insert, auto) +qed auto + +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 + +lemma conjunctD2: assumes "a \ b" shows a b using assms by auto +lemma conjunctD3: assumes "a \ b \ c" shows a b c using assms by auto +lemma conjunctD4: assumes "a \ b \ c \ d" shows a b c d using assms by auto + +lemma cond_cases: "(P \ Q x) \ (\ P \ Q y) \ Q (if P then x else y)" + by auto + +declare norm_triangle_ineq4[intro] + +lemma transitive_stepwise_le: + assumes "\x. R x x" "\x y z. R x y \ R y z \ R x z" and "\n. R n (Suc n)" + shows "\n\m. R m n" +proof (intro allI impI) + show "m \ n \ R m n" for n + by (induction rule: dec_induct) + (use assms in blast)+ +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 inter_interval_mixed_eq_empty[of c d a b] and assms(3,5) + unfolding assms(1,2) interior_cbox by auto + moreover + have "box a b \ cbox c d \ s" + apply (rule order_trans,rule box_subset_cbox) + using assms(4) unfolding assms(1,2) + apply auto + done + ultimately + show ?thesis + unfolding assms interior_cbox + by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI) +qed + +lemma 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 inter_interior_unions_intervals: + "finite f \ open s \ \t\f. \a b. t = cbox a b \ \t\f. s \ (interior t) = {} \ s \ interior (\f) = {}" + using interior_Union_subset_cbox[of f "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) *\<^sub>R i)" + "cbox a b \ {x. x\k \ c} = cbox (\i\Basis. (if i = k then max (a\k) c else a\i) *\<^sub>R i) b" + apply (rule_tac[!] set_eqI) + unfolding Int_iff mem_box mem_Collect_eq + using assms + apply auto + done + +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) *\<^sub>R i)" + +definition interval_lowerbound :: "('a::euclidean_space) set \ 'a" + where "interval_lowerbound s = (\i\Basis. (INF x:s. x\i) *\<^sub>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_setsum 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_setsum cbox_def + by (safe intro!: cInf_eq) auto + +lemmas interval_bounds = interval_upperbound interval_lowerbound + +lemma + fixes X::"real set" + shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X" + and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X" + by (auto simp: interval_upperbound_def interval_lowerbound_def) + +lemma interval_bounds'[simp]: + assumes "cbox a b \ {}" + 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)) *\<^sub>R i) = (\i\Basis. (SUP x:A. x \ i) *\<^sub>R i)" + by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0) + moreover from assms have snd_image_times': "B = snd ` (A \ B)" by simp + have "(\i\Basis. (SUP x:A \ B. x \ (0, i)) *\<^sub>R i) = (\i\Basis. (SUP x:B. x \ i) *\<^sub>R i)" + by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0) + ultimately show ?thesis unfolding interval_upperbound_def + by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod) +qed + +lemma interval_lowerbound_Times: + assumes "A \ {}" 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)) *\<^sub>R i) = (\i\Basis. (INF x:A. x \ i) *\<^sub>R i)" + by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0) + moreover from assms have snd_image_times': "B = snd ` (A \ B)" by simp + have "(\i\Basis. (INF x:A \ B. x \ (0, i)) *\<^sub>R i) = (\i\Basis. (INF x:B. x \ i) *\<^sub>R i)" + by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0) + ultimately show ?thesis unfolding interval_lowerbound_def + by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod) +qed + +subsection \The notion of a gauge --- simply an open set containing the point.\ + +definition "gauge d \ (\x. x \ d x \ open (d x))" + +lemma gaugeI: + assumes "\x. x \ g x" + and "\x. open (g x)" + shows "gauge g" + using assms unfolding gauge_def by auto + +lemma gaugeD[dest]: + assumes "gauge d" + shows "x \ d x" + and "open (d 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_inter[intro]: "gauge d1 \ gauge d2 \ gauge (\x. d1 x \ d2 x)" + unfolding gauge_def by auto + +lemma gauge_inters: + assumes "finite s" + and "\d\s. gauge (f d)" + shows "gauge (\x. \{f d x | d. d \ s})" +proof - + have *: "\x. {f d x |d. d \ s} = (\d. f d x) ` s" + by auto + show ?thesis + unfolding gauge_def unfolding * + using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto +qed + +lemma gauge_existence_lemma: + "(\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 + apply safe + defer + apply (erule_tac x="f x" in allE) + apply (erule_tac x="d (f x)" in allE) + apply auto + done + +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" + unfolding division_of_def 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 simp: cbox_sing) + done + } + ultimately show ?l + unfolding division_of_def cbox_sing by auto +next + assume ?l + note * = conjunctD4[OF this[unfolded division_of_def cbox_sing]] + { + fix x + assume x: "x \ s" have "x = {a}" + using *(2)[rule_format,OF x] by auto + } + moreover have "s \ {}" + using *(4) by auto + ultimately show ?r + unfolding cbox_sing by auto +qed + +lemma elementary_empty: obtains p where "p division_of {}" + unfolding division_of_trivial by auto + +lemma elementary_interval: obtains p where "p division_of (cbox a b)" + by (metis division_of_trivial division_of_self) + +lemma division_contains: "s division_of i \ \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 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" + apply (rule set_eqI) + unfolding * and UN_iff + using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] + apply auto + done + { + fix k + assume "k \ ?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_inter: + 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_inters: + 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_inter 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) *\<^sub>R i) (\i\Basis. (snd (f i) \ i) *\<^sub>R i)" + define p where "p = ?B ` (Basis \\<^sub>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)"]) + { + fix i :: 'a + assume "i \ Basis" + with incl nonempty have "a \ i \ c \ i" "c \ i \ d \ i" "d \ i \ b \ i" + unfolding box_eq_empty subset_box by (auto simp: not_le) + } + note ord = this + + show "p division_of (cbox a b)" + proof (rule division_ofI) + show "finite p" + unfolding p_def by (auto intro!: finite_PiE) + { + fix k + assume "k \ p" + then obtain f where f: "f \ Basis \\<^sub>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 \\<^sub>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 interior_cbox 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 \\<^sub>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 + +lemma 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 + { fix x + assume x: "x \ p" + have "q x division_of \q x" + apply (rule division_ofI) + using division_ofD[OF q(1)[OF x]] + apply auto + done } + then have "\x. x \ p \ \d. d division_of \(q x - {x})" + by (meson Diff_subset division_of_subset) + then have "\d. d division_of \((\i. \(q i - {i})) ` p)" + apply - + apply (rule elementary_inters [OF finite_imageI[OF p(1)]]) + apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]]) + done + then obtain d where d: "d division_of \((\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" + have *: "\u t s. t \ s = {} \ u \ s \ u \ t = {}" + by auto + have "interior (\i\p. \(q i - {i})) \ interior k = {}" + proof (rule *[OF inter_interior_unions_intervals]) + note qk=division_ofD[OF q(1)[OF k]] + show "finite (q k - {k})" "open (interior k)" "\t\q k - {k}. \a b. t = cbox a b" + using qk by auto + show "\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 + apply auto + done + qed } 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 inter_interior_unions_intervals) + apply (rule p open_interior ballI)+ + apply simp_all + done + qed + then show ?thesis + by (meson Un_upper2 that) +qed + +lemma elementary_bounded[dest]: + fixes s :: "'a::euclidean_space set" + shows "p division_of s \ 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 elementary_bounded bounded_subset_cbox) + +lemma 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 + show ?thesis + apply (rule that[of "{}"]) + unfolding True + using assms + apply auto + done +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 "p division_of cbox c d" "cbox u v \ p" + by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]]) + note p = this division_ofD[OF this(1)] + have "interior (cbox a b \ \(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 inter_interior_unions_intervals) + using p(6) p(7)[OF p(2)] p(3) + 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_unions: + 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 - + note assm = division_ofD[OF assms] + have lem1: "\f s. \\(f ` s) = \((\x. \(f x)) ` s)" + by auto + have lem2: "\f s. f \ {} \ \{s \ t |t. t \ f} = s \ \f" + by auto + { + presume "p = {} \ thesis" + "cbox a b = {} \ thesis" + "cbox a b \ {} \ interior (cbox a b) = {} \ thesis" + "p \ {} \ interior (cbox a b)\{} \ cbox a b \ {} \ thesis" + then show thesis by auto + next + assume as: "p = {}" + obtain p where "p division_of (cbox a b)" + by (rule elementary_interval) + then show thesis + using as that by auto + next + assume as: "cbox a b = {}" + show thesis + using as assms that by auto + next + assume as: "interior (cbox a b) = {}" "cbox a b \ {}" + show thesis + apply (rule that[of "insert (cbox a b) p"],rule division_ofI) + unfolding finite_insert + apply (rule assm(1)) unfolding Union_insert + using assm(2-4) as + apply - + apply (fast dest: assm(5))+ + done + next + assume as: "p \ {}" "interior (cbox a b) \ {}" "cbox a b \ {}" + have "\k\p. \q. (insert (cbox a b) q) division_of (cbox a b \ k)" + proof + fix k + assume kp: "k \ p" + from assm(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 as(3) 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 "*" assm(1) q(1) by auto + show "\?D = cbox a b \ \p" + unfolding * lem1 + unfolding lem2[OF as(1), of "cbox a b", symmetric] + using q(6) + by auto + fix k + assume k: "k \ ?D" + then show "k \ cbox a b \ \p" + using q(2) by auto + show "k \ {}" + using q(3) k by auto + show "\a b. k = cbox a b" + using q(4) k by auto + fix k' + assume 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'") + case True + show ?thesis + using True k' q(5) x' x by auto + next + case False + { + presume "k = cbox a b \ ?thesis" + and "k' = cbox a b \ ?thesis" + and "k \ cbox a b \ k' \ cbox a b \ ?thesis" + then show ?thesis by linarith + next + assume as': "k = cbox a b" + show ?thesis + using as' k' q(5) x' by blast + next + assume as': "k' = cbox a b" + show ?thesis + using as' k'(2) q(5) x by blast + } + assume as': "k \ cbox a b" "k' \ cbox a b" + obtain c d where k: "k = cbox c d" + using q(4)[OF x(2,1)] by blast + have "interior k \ interior (cbox a b) = {}" + using as' k'(2) q(5) x by blast + then have "interior k \ interior x" + using interior_subset_union_intervals + by (metis as(2) k q(2) x interior_subset_union_intervals) + moreover + obtain c d where c_d: "k' = cbox c d" + using q(4)[OF x'(2,1)] by blast + have "interior k' \ interior (cbox a b) = {}" + using as'(2) q(5) x' by blast + then have "interior k' \ interior x'" + by (metis as(2) c_d interior_subset_union_intervals q(2) x'(1) x'(2)) + ultimately show ?thesis + using assm(5)[OF x(2) x'(2) False] by auto + qed + qed + } +qed + +lemma elementary_unions_intervals: + assumes fin: "finite f" + and "\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_inter) + { + fix x + assume x: "x \ t" "x \ s" + then have "x\\r1" + unfolding r1 using ab by auto + then obtain r where r: "r \ r1" "x \ r" + unfolding Union_iff .. + 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 *: "t = \p \ (\(r1 - p) \ \q)" + unfolding divp divq using assms(3) by auto + show ?thesis + apply (rule that[of "p \ r2"]) + unfolding * + defer + apply (rule division_disjoint_union) + unfolding divp(6) + apply(rule assms r2)+ + proof - + have "interior s \ interior (\(r1-p)) = {}" + proof (rule inter_interior_unions_intervals) + show "finite (r1 - p)" and "open (interior s)" and "\t\r1-p. \a b. t = cbox a b" + using r1 by auto + have *: "\s. (\x. x \ s \ False) \ s = {}" + by auto + show "\t\r1-p. interior s \ interior t = {}" + proof + fix m x + assume as: "m \ r1 - p" + have "interior m \ interior (\p) = {}" + proof (rule inter_interior_unions_intervals) + show "finite p" and "open (interior m)" and "\t\p. \a b. t = cbox a b" + using divp by auto + show "\t\p. interior m \ interior t = {}" + by (metis DiffD1 DiffD2 as r1(1) r1(7) set_rev_mp) + qed + then show "interior s \ interior m = {}" + unfolding divp by auto + qed + qed + then show "interior s \ interior (\(r1-p) \ (\q)) = {}" + using interior_subset by auto + qed auto +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 guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this + guess u v using p(4)[OF l(2)] by (elim exE) note uv=this + 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 guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this + 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 guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this + guess u v using p(4)[OF l(2)] by (elim exE) note uv=this + 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 guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this + 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[dest]: + 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 + apply auto + apply fastforce+ + done + +lemma tagged_division_ofD[dest]: (*FIXME USE A LOCALE*) + 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 + unfolding tagged_partial_division_of_def + using finite_subset[OF assms(2)] + 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_union: + 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_unions: + assumes "finite iset" + and "\i\iset. pfn i tagged_division_of i" + and "\i1\iset. \i2\iset. i1 \ i2 \ interior(i1) \ interior(i2) = {}" + shows "\(pfn ` iset) tagged_division_of (\iset)" +proof (rule tagged_division_ofI) + note assm = tagged_division_ofD[OF assms(2)[rule_format]] + show "finite (\(pfn ` iset))" + using assms by auto + have "\{k. \x. (x, k) \ \(pfn ` iset)} = \((\i. \{k. \x. (x, k) \ pfn i}) ` iset)" + by blast + also have "\ = \iset" + using assm(6) by auto + finally show "\{k. \x. (x, k) \ \(pfn ` iset)} = \iset" . + fix x k + assume xk: "(x, k) \ \(pfn ` iset)" + then obtain i where i: "i \ iset" "(x, k) \ pfn i" + by auto + show "x \ k" "\a b. k = cbox a b" "k \ \iset" + using assm(2-4)[OF i] using i(1) by auto + fix x' k' + assume xk': "(x', k') \ \(pfn ` iset)" "(x, k) \ (x', k')" + then obtain i' where i': "i' \ iset" "(x', k') \ pfn i'" + by auto + have *: "\a b. i \ i' \ a \ i \ b \ i' \ interior a \ interior b = {}" + using i(1) i'(1) + using assms(3)[rule_format] interior_mono + by blast + show "interior k \ interior k' = {}" + apply (cases "i = i'") + using assm(5) i' i(2) xk'(2) apply blast + using "*" assm(3) i' i by auto +qed + +lemma tagged_partial_division_of_union_self: + assumes "p tagged_partial_division_of s" + shows "p tagged_division_of (\(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 + +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 + @{text operative_division}. Instances for the monoid are @{typ "'a option"}, @{typ real}, and + @{typ bool}.\ + +paragraph \Using additivity of lifted function to encode definedness.\ + +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 \Operative\ + +definition (in comm_monoid) operative :: "('b::euclidean_space set \ 'a) \ bool" + where "operative g \ + (\a b. box a b = {} \ g (cbox a b) = \<^bold>1) \ + (\a b c. \k\Basis. g (cbox a b) = g (cbox a b \ {x. x\k \ c}) \<^bold>* g (cbox a b \ {x. x\k \ c}))" + +lemma (in comm_monoid) operativeD[dest]: + assumes "operative g" + shows "\a b. box a b = {} \ g (cbox a b) = \<^bold>1" + and "\a b c k. k \ Basis \ g (cbox a b) = g (cbox a b \ {x. x\k \ c}) \<^bold>* g (cbox a b \ {x. x\k \ c})" + using assms unfolding operative_def by auto + +lemma (in comm_monoid) operative_empty: + assumes g: "operative g" shows "g {} = \<^bold>1" +proof - + have *: "cbox One (-One) = ({}::'b set)" + by (auto simp: box_eq_empty inner_setsum_left inner_Basis setsum.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 operativeD(1)[OF g, of One "-One"] by simp +qed + +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) *\<^sub>R i) \ i" + "\i\Basis. (\i\Basis. (if i = k then max (a \ k) c else a \ i) *\<^sub>R i) \ i \ b\i" + "min (b \ k) c = c" "max (a \ k) c = c" + using assms using less_imp_le by auto + show ?t1 (*FIXME a horrible mess*) + 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 * + apply (rule subsetI) + unfolding mem_Collect_eq split_beta + apply (erule bexE conjE)+ + apply (simp add: ) + apply (erule exE conjE)+ + proof + fix i l x + assume as: + "a \ fst x < snd x" "snd x < (if fst x = k then c else b \ fst x)" + "interval_lowerbound i \ fst x = snd x \ interval_upperbound i \ fst x = snd x" + "i = l \ {x. x \ k \ c}" "l \ d" "l \ {x. x \ k \ c} \ {}" + and fstx: "fst x \ Basis" + from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this + have *: "\i\Basis. u \ i \ (\i\Basis. (if i = k then min (v \ k) c else v \ i) *\<^sub>R i) \ i" + using as(6) unfolding l interval_split[OF k] box_ne_empty as . + have **: "\i\Basis. u\i \ v\i" + using l using as(6) unfolding box_ne_empty[symmetric] by auto + show "\i\d. interval_lowerbound i \ fst x = snd x \ interval_upperbound i \ fst x = snd x" + apply (rule bexI[OF _ \l \ d\]) + using as(1-3,5) fstx + unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as + apply (auto split: if_split_asm) + done + show "snd x < b \ fst x" + using as(2) \c < b\k\ by (auto split: if_split_asm) + qed + 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 * + unfolding subset_eq + apply rule + unfolding mem_Collect_eq split_beta + apply (erule bexE conjE)+ + apply (simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms) + apply (erule exE conjE)+ + proof + fix i l x + assume as: + "(if fst x = k then c else a \ fst x) < snd x" "snd x < b \ fst x" + "interval_lowerbound i \ fst x = snd x \ interval_upperbound i \ fst x = snd x" + "i = l \ {x. c \ x \ k}" "l \ d" "l \ {x. c \ x \ k} \ {}" + and fstx: "fst x \ Basis" + from assm(4)[OF this(5)] guess u v by (elim exE) note l=this + have *: "\i\Basis. (\i\Basis. (if i = k then max (u \ k) c else u \ i) *\<^sub>R i) \ i \ v \ i" + using as(6) unfolding l interval_split[OF k] box_ne_empty as . + have **: "\i\Basis. u\i \ v\i" + using l using as(6) unfolding box_ne_empty[symmetric] by auto + show "\i\d. interval_lowerbound i \ fst x = snd x \ interval_upperbound i \ fst x = snd x" + apply (rule bexI[OF _ \l \ d\]) + using as(1-3,5) fstx + unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as + apply (auto split: if_split_asm) + done + show "a \ fst x < snd x" + using as(1) \a\k < c\ by (auto split: if_split_asm) + qed +qed + +lemma division_points_psubset: + 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 "l \ d" + and "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 assms(2) by (auto intro!:less_imp_le) + guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this + have uv: "\i\Basis. u\i \ v\i" "\i\Basis. a\i \ u\i \ v\i \ b\i" + using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty + using subset_box(1) + apply auto + apply blast+ + done + 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] + apply - + apply (erule disjE) + apply (rule_tac x="(k,(interval_lowerbound l)\k)" in exI, force simp add: *) + apply (rule_tac x="(k,(interval_upperbound l)\k)" in exI, force simp add: *) + done + 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] + apply - + apply (erule disjE) + apply (rule_tac x="(k,(interval_lowerbound l)\k)" in exI, force simp add: *) + apply (rule_tac x="(k,(interval_upperbound l)\k)" in exI, force simp add: *) + done + 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 type :: "'a::euclidean_space" + assumes "d division_of i" + and "k1 \ d" + and "k2 \ d" + and "k1 \ k2" + and "k1 \ {x::'a. x\k \ c} = k2 \ {x. x\k \ c}" + and k: "k\Basis" + shows "interior (k1 \ {x. x\k \ c}) = {}" +proof - + note d=division_ofD[OF assms(1)] + guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this + guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this + have **: "\s t u. s \ t = {} \ u \ s \ u \ t \ u = {}" + by auto + show ?thesis + unfolding uv1 uv2 + apply (rule **[OF d(5)[OF assms(2-4)]]) + apply (simp add: uv1) + using assms(5) uv1 by auto +qed + +lemma division_split_right_inj: + fixes type :: "'a::euclidean_space" + assumes "d division_of i" + and "k1 \ d" + and "k2 \ d" + and "k1 \ k2" + and "k1 \ {x::'a. x\k \ c} = k2 \ {x. x\k \ c}" + and k: "k \ Basis" + shows "interior (k1 \ {x. x\k \ c}) = {}" +proof - + note d=division_ofD[OF assms(1)] + guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this + guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this + have **: "\s t u. s \ t = {} \ u \ s \ u \ t \ u = {}" + by auto + show ?thesis + unfolding uv1 uv2 + apply (rule **[OF d(5)[OF assms(2-4)]]) + apply (simp add: uv1) + using assms(5) uv1 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) *\<^sub>R i) + (\i\Basis. (if i = k then min (b\k) (c + e) else b\i) *\<^sub>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]) + apply (rule equalityI) + apply blast + apply clarsimp + apply (rule_tac x="l \ {x. c + e \ x \ k}" in exI) + apply auto + done + by (simp add: interval_split k interval_doublesplit) +qed + +lemma (in comm_monoid_set) operative_division: + fixes g :: "'b::euclidean_space set \ 'a" + assumes g: "operative g" and d: "d division_of (cbox a b)" shows "F g d = g (cbox a b)" +proof - + define C where [abs_def]: "C = card (division_points (cbox a b) d)" + then show ?thesis + using d + 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 = \<^bold>1" + using operativeD(1)[OF g, 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: operativeD(1)[OF g]) + 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) *\<^sub>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 guess i .. note i=this + guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this + 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}) = \<^bold>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 guess u v by (elim exE conjE) note uv=this + 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 = \<^bold>1" + unfolding uv(1) by (rule operativeD(1)[OF g]) + 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 guess k c + unfolding split_paired_Ex division_points_def mem_Collect_eq split_conv + apply (elim exE conjE) + done + note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']] + from this(3) guess j .. note j=this + define d1 where "d1 = {l \ {x. x\k \ c} | l. l \ d \ l \ {x. x\k \ c} \ {}}" + define d2 where "d2 = {l \ {x. x\k \ c} | l. l \ d \ l \ {x. x\k \ c} \ {}}" + define cb where "cb = (\i\Basis. (if i = k then c else b\i) *\<^sub>R i)" + define ca where "ca = (\i\Basis. (if i = k then c else a\i) *\<^sub>R i)" + note division_points_psubset[OF \d division_of cbox a b\ ab kc(1-2) j] + note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)] + then have *: "F g d1 = g (cbox a b \ {x. x\k \ c})" "F g d2 = g (cbox a b \ {x. x\k \ c})" + unfolding interval_split[OF kc(4)] + apply (rule_tac[!] "less.hyps"[rule_format]) + using division_split[OF \d division_of cbox a b\, where k=k and c=c] + apply (simp_all add: interval_split kc d1_def d2_def division_points_finite[OF \d division_of cbox a b\]) + done + { fix l y + assume as: "l \ d" "y \ d" "l \ {x. x \ k \ c} = y \ {x. x \ k \ c}" "l \ y" + from division_ofD(4)[OF \d division_of cbox a b\ this(1)] guess u v by (elim exE) note leq=this + have "g (l \ {x. x \ k \ c}) = \<^bold>1" + unfolding leq interval_split[OF kc(4)] + apply (rule operativeD[OF g]) + unfolding interior_cbox[symmetric] interval_split[symmetric, OF kc(4)] + using division_split_left_inj less as kc leq by blast + } note fxk_le = this + { fix l y + assume as: "l \ d" "y \ d" "l \ {x. c \ x \ k} = y \ {x. c \ x \ k}" "l \ y" + from division_ofD(4)[OF \d division_of cbox a b\ this(1)] guess u v by (elim exE) note leq=this + have "g (l \ {x. x \ k \ c}) = \<^bold>1" + unfolding leq interval_split[OF kc(4)] + apply (rule operativeD(1)[OF g]) + unfolding interior_cbox[symmetric] interval_split[symmetric,OF kc(4)] + using division_split_right_inj less leq as kc by blast + } note fxk_ge = this + have d1_alt: "d1 = (\l. l \ {x. x\k \ c}) ` {l \ d. l \ {x. x\k \ c} \ {}}" + using d1_def by auto + have d2_alt: "d2 = (\l. l \ {x. x\k \ c}) ` {l \ d. l \ {x. x\k \ c} \ {}}" + using d2_def by auto + have "g (cbox a b) = F g d1 \<^bold>* F g d2" (is "_ = ?prev") + unfolding * using g kc(4) by blast + also have "F g d1 = F (\l. g (l \ {x. x\k \ c})) d" + unfolding d1_alt using division_of_finite[OF less.prems] fxk_le + by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g]) + also have "F g d2 = F (\l. g (l \ {x. x\k \ c})) d" + unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge + by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g]) + also have *: "\x\d. g x = g (x \ {x. x \ k \ c}) \<^bold>* g (x \ {x. c \ x \ k})" + unfolding forall_in_division[OF \d division_of cbox a b\] + using g kc(4) by blast + have "F (\l. g (l \ {x. x\k \ c})) d \<^bold>* F (\l. g (l \ {x. x\k \ c})) d = F g d" + using * by (simp add: distrib) + finally show ?thesis by auto + qed + qed + qed +qed + +lemma (in comm_monoid_set) over_tagged_division_lemma: + assumes "p tagged_division_of i" + and "\u v. cbox u v \ {} \ box u v = {} \ d (cbox u v) = \<^bold>1" + shows "F (\(x,k). d k) p = F d (snd ` p)" +proof - + have *: "(\(x,k). d k) = d \ snd" + unfolding o_def by (rule ext) auto + 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" + by (metis prod.collapse \x\p\ \snd x = snd y\ \x \ y\)+ + 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) = \<^bold>1" + using assm(2)[of "fst x" "snd x"] \x\p\ ab[symmetric] by (intro assms(2)) auto + then show "d (snd x) = \<^bold>1" + unfolding ab by auto + qed +qed + +lemma (in comm_monoid_set) operative_tagged_division: + assumes f: "operative g" and d: "d tagged_division_of (cbox a b)" + shows "F (\(x, l). g l) d = g (cbox a b)" + unfolding d[THEN division_of_tagged_division, THEN operative_division[OF f], symmetric] + by (simp add: f[THEN operativeD(1)] over_tagged_division_lemma[OF d]) + +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 (in comm_monoid) operative_1_lt: + "operative (g :: real set \ 'a) \ + ((\a b. b \ a \ g {a .. b} = \<^bold>1) \ (\a b c. a < c \ c < b \ g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))" + apply (simp add: operative_def atMost_def[symmetric] atLeast_def[symmetric]) +proof safe + fix a b c :: real + assume *: "\a b c. g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}" + assume "a < c" "c < b" + with *[rule_format, of a b c] show "g {a..c} \<^bold>* g {c..b} = g {a..b}" + by (simp add: less_imp_le min.absorb2 max.absorb2) +next + fix a b c :: real + assume as: "\a b. b \ a \ g {a..b} = \<^bold>1" + "\a b c. a < c \ c < b \ g {a..c} \<^bold>* g {c..b} = g {a..b}" + from as(1)[rule_format, of 0 1] as(1)[rule_format, of a a for a] as(2) + have [simp]: "g {} = \<^bold>1" "\a. g {a} = \<^bold>1" + "\a b c. a < c \ c < b \ g {a..c} \<^bold>* g {c..b} = g {a..b}" + by auto + show "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}" + by (auto simp: min_def max_def le_less) +qed + +lemma (in comm_monoid) operative_1_le: + "operative (g :: real set \ 'a) \ + ((\a b. b \ a \ g {a..b} = \<^bold>1) \ (\a b c. a \ c \ c \ b \ g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))" + unfolding operative_1_lt +proof safe + fix a b c :: real + assume as: "\a b c. a \ c \ c \ b \ g {a..c} \<^bold>* g {c..b} = g {a..b}" "a < c" "c < b" + show "g {a..c} \<^bold>* g {c..b} = g {a..b}" + apply (rule as(1)[rule_format]) + using as(2-) + apply auto + done +next + fix a b c :: real + assume "\a b. b \ a \ g {a .. b} = \<^bold>1" + and "\a b c. a < c \ c < b \ g {a..c} \<^bold>* g {c..b} = g {a..b}" + and "a \ c" + and "c \ b" + note as = this[rule_format] + show "g {a..c} \<^bold>* g {c..b} = g {a..b}" + proof (cases "c = a \ c = b") + case False + then show ?thesis + apply - + apply (subst as(2)) + using as(3-) + apply auto + done + next + case True + then show ?thesis + proof + assume *: "c = a" + then have "g {a .. c} = \<^bold>1" + apply - + apply (rule as(1)[rule_format]) + apply auto + done + then show ?thesis + unfolding * by auto + next + assume *: "c = b" + then have "g {c .. b} = \<^bold>1" + apply - + apply (rule as(1)[rule_format]) + apply auto + done + then show ?thesis + unfolding * by auto + qed + qed +qed + +lemma tagged_division_union_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_union[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_union_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_union_interval) + +lemma tagged_division_split_left_inj: + "d tagged_division_of i \ (x1, k1) \ d \ (x2, k2) \ d \ k1 \ k2 \ + k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c} \ k \ Basis \ + interior (k1 \ {x. x\k \ c}) = {}" + by (intro division_split_left_inj[of "snd`d" i k1 k2, OF division_of_tagged_division]) + (auto simp add: snd_def[abs_def] image_iff split: prod.split ) + +lemma tagged_division_split_right_inj: + "d tagged_division_of i \ (x1, k1) \ d \ (x2, k2) \ d \ k1 \ k2 \ + k1 \ {x. x\k \ c} = k2 \ {x. x\k \ c} \ k \ Basis \ + interior (k1 \ {x. x\k \ c}) = {}" + by (intro division_split_right_inj[of "snd`d" i k1 k2, OF division_of_tagged_division]) + (auto simp add: snd_def[abs_def] image_iff split: prod.split ) + +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 "setsum (\(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))" + have ***: "\i\Basis. a \ i \ b \ i" + using assms by auto + have *: "add.operative ?f" + unfolding add.operative_1_lt box_eq_empty + by auto + have **: "cbox a b \ {}" + using assms(1) by auto + note setsum.operative_tagged_division[OF * assms(2)[simplified box_real[symmetric]]] + note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric] + show ?thesis + unfolding * + apply (rule setsum.cong) + unfolding split_paired_all split_conv + using assms(2) + apply auto + done +qed + +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) + +lemma additive_tagged_division_1': + fixes f :: "real \ 'a::real_normed_vector" + assumes "a \ b" + and "p tagged_division_of {a..b}" + shows "setsum (\(x,k). f (Sup k) - f(Inf k)) p = f b - f a" + using additive_tagged_division_1[OF _ assms(2), of f] + using assms(1) + by auto + +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_inter: "(\x. d1 x \ d2 x) fine p \ d1 fine p \ d2 fine p" + unfolding fine_def by auto + +lemma fine_inters: + "(\x. \{f d x | d. d \ s}) fine p \ (\d\s. (f d) fine p)" + unfolding fine_def by blast + +lemma fine_union: "d fine p1 \ d fine p2 \ d fine (p1 \ p2)" + unfolding fine_def by blast + +lemma fine_unions: "(\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_unions_exists: + assumes "finite iset" + and "\i\iset. \p. p tagged_division_of i \ d fine p" + and "\i1\iset. \i2\iset. i1 \ i2 \ interior i1 \ interior i2 = {}" + and "\iset = i" + obtains p where "p tagged_division_of i" and "d fine p" +proof - + obtain pfn where pfn: + "\x. x \ iset \ pfn x tagged_division_of x" + "\x. x \ iset \ d fine pfn x" + using bchoice[OF assms(2)] by auto + show thesis + apply (rule_tac p="\(pfn ` iset)" in that) + using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force + by (metis (mono_tags, lifting) fine_unions imageE pfn(2)) +qed + + +subsection \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 "P {}" + and "\s t. P s \ P t \ interior(s) \ interior(t) = {} \ P (s \ t)" + and "\ P (cbox a (b::'a))" + obtains c d where "\ P (cbox c d)" + and "\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 assms(1,3) by metis + then have ab: "\i. i\Basis \ a \ i \ b \ i" + by (force simp: mem_box) + { fix f + have "\finite f; + \s. s\f \ P s; + \s. s\f \ \a b. s = cbox a b; + \s t. s\f \ t\f \ s \ t \ interior s \ interior t = {}\ \ P (\f)" + proof (induct f rule: finite_induct) + case empty + show ?case + using assms(1) by auto + next + case (insert x f) + show ?case + unfolding Union_insert + apply (rule assms(2)[rule_format]) + using inter_interior_unions_intervals [of f "interior x"] + apply (auto simp: insert) + by (metis IntI empty_iff insert.hyps(2) insert.prems(3) insert_iff) + qed + } note UN_cases = this + let ?A = "{cbox c d | c d::'a. \i\Basis. (c\i = a\i) \ (d\i = (a\i + b\i) / 2) \ + (c\i = (a\i + b\i) / 2) \ (d\i = b\i)}" + let ?PP = "\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" + { + presume "\c d. ?PP c d \ P (cbox c d) \ False" + then show thesis + unfolding atomize_not not_all + by (blast intro: that) + } + assume as: "\c d. ?PP c d \ P (cbox c d)" + have "P (\?A)" + proof (rule UN_cases) + let ?B = "(\s. cbox (\i\Basis. (if i \ s then a\i else (a\i + b\i) / 2) *\<^sub>R i::'a) + (\i\Basis. (if i \ s then (a\i + b\i) / 2 else b\i) *\<^sub>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 = (a \ i + b \ i) / 2 \ + c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" by blast + show "x \ ?B" + unfolding image_iff x + apply (rule_tac x="{i. i\Basis \ c\i = a\i}" in bexI) + apply (rule arg_cong2 [where f = cbox]) + using x(2) ab + apply (auto simp add: euclidean_eq_iff[where 'a='a]) + by fastforce + qed + then show "finite ?A" + by (rule finite_subset) auto + next + fix s + assume "s \ ?A" + then obtain c d + where s: "s = cbox c d" + "\i. i \ Basis \ + c \ i = a \ i \ d \ i = (a \ i + b \ i) / 2 \ + c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" + by blast + show "P s" + unfolding s + apply (rule as[rule_format]) + using ab s(2) by force + 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 = (a \ i + b \ i) / 2 \ + e \ i = (a \ i + b \ i) / 2 \ 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'] + proof safe + assume as: "c \ i = a \ i" "d \ i = (a \ i + b \ i) / 2" + show False + using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps) + next + assume as: "c \ i = (a \ i + b \ i) / 2" "d \ i = b \ i" + show False + using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps) + qed + 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 = (a \ i + b \ i) / 2 \ + c \ i = (a \ i + b \ i) / 2 \ d \ i = b \ i" + by blast + show "x\cbox a b" + unfolding mem_box + proof safe + fix i :: 'a + assume i: "i \ Basis" + then show "a \ i \ x \ i" "x \ i \ b \ i" + using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto + qed + next + fix x + assume x: "x \ cbox a b" + have "\i\Basis. + \c d. (c = a\i \ d = (a\i + b\i) / 2 \ c = (a\i + b\i) / 2 \ d = b\i) \ c\x\i \ x\i \ d" + (is "\i\Basis. \c d. ?P i c d") + unfolding mem_box + proof + fix i :: 'a + assume i: "i \ Basis" + have "?P i (a\i) ((a \ i + b \ i) / 2) \ ?P i ((a \ i + b \ i) / 2) (b\i)" + using x[unfolded mem_box,THEN bspec, OF i] by auto + then show "\c d. ?P i c d" + by blast + qed + then show "x\\?A" + unfolding Union_iff Bex_def mem_Collect_eq choice_Basis_iff + apply auto + apply (rule_tac x="cbox xa xaa" in exI) + unfolding mem_box + apply auto + done + qed + finally show False + using assms by auto +qed + +lemma interval_bisection: + fixes type :: "'a::euclidean_space" + assumes "P {}" + and "(\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 as: False + obtain c d where "\ P (cbox c d)" + "\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 (rule interval_bisection_step[of P, OF assms(1-2) as]) + then show ?thesis + apply - + apply (rule_tac x="(c,d)" in exI) + apply auto + done + qed + qed + then obtain f where f: + "\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)" + apply - + apply (drule choice) + apply blast + done + 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 "A 0 = a" "B 0 = b" "\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 + apply (rule f[rule_format]) using assms(3) + apply auto + done + next + case (Suc n) + show ?case + unfolding S + apply (rule f[rule_format]) + using Suc + unfolding S + apply auto + done + qed + qed + note AB = this(1-2) conjunctD2[OF this(3),rule_format] + + 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 "(setsum (\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 \ setsum (\i. \(x - y)\i\) Basis" + unfolding dist_norm by(rule norm_le_l1) + also have "\ \ setsum (\i. B n\i - A n\i) Basis" + proof (rule setsum_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 "\ \ setsum (\i. b\i - a\i) Basis / 2^n" + unfolding setsum_divide_distrib + proof (rule setsum_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(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(4) by (intro order_trans[OF step.IH] subset_box_imp) auto + qed simp + } note ABsubset = this + have "\a. \n. a\ cbox (A n) (B n)" + by (rule decreasing_closed_nest[rule_format,OF closed_cbox _ ABsubset interv]) + (metis nat.exhaust AB(1-3) assms(1,3)) + then obtain x0 where x0: "\n. x0 \ cbox (A n) (B n)" + by blast + show thesis + proof (rule that[rule_format, of x0]) + show "x0\cbox a b" + using x0[of 0] unfolding AB . + 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))" + apply (cases "0 < n") + using AB(3)[of "n - 1"] assms(3) AB(1-2) + apply auto + done + 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" + unfolding AB(1-2)[symmetric] by (rule ABsubset) auto + 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 - + presume "\ (\p. p tagged_division_of (cbox a b) \ g fine p) \ False" + then obtain p where "p tagged_division_of (cbox a b)" "g fine p" + by blast + then show thesis .. +next + assume as: "\ (\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 _ _ as]) + apply (simp add: fine_def) + apply (metis tagged_division_union fine_union) + apply (auto simp: ) + 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 False + 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 "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 - + let ?P = "\p. p tagged_partial_division_of (cbox a b) \ gauge d \ + (\q. q tagged_division_of (\{k. \x. (x,k) \ p}) \ d fine q \ + (\(x,k) \ p. k \ d(x) \ (x,k) \ q))" + { + have *: "finite p" "p tagged_partial_division_of (cbox a b)" + using assms(1) + unfolding tagged_division_of_def + by auto + presume "\p. finite p \ ?P p" + from this[rule_format,OF * assms(2)] guess q .. note q=this + then show ?thesis + apply - + apply (rule that[of q]) + unfolding tagged_division_ofD[OF assms(1)] + apply auto + done + } + fix p :: "('a::euclidean_space \ ('a::euclidean_space set)) set" + assume as: "finite p" + show "?P p" + apply rule + apply rule + using as + proof (induct p) + case empty + show ?case + apply (rule_tac x="{}" in exI) + unfolding fine_def + apply auto + done + next + case (insert xk p) + guess x k using surj_pair[of xk] by (elim exE) note xk=this + note tagged_partial_division_subset[OF insert(4) subset_insertI] + from insert(3)[OF this insert(5)] guess q1 .. note q1 = conjunctD3[OF this] + 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)] + from p(4)[unfolded xk, OF insertI1] guess u v by (elim exE) note uv=this + + have "finite {k. \x. (x, k) \ p}" + apply (rule finite_subset[of _ "snd ` p"]) + using p + apply safe + apply (metis image_iff snd_conv) + apply auto + done + then have int: "interior (cbox u v) \ interior (\{k. \x. (x, k) \ p}) = {}" + apply (rule inter_interior_unions_intervals) + apply (rule open_interior) + apply (rule_tac[!] ballI) + unfolding mem_Collect_eq + apply (erule_tac[!] exE) + apply (drule p(4)[OF insertI2]) + apply assumption + apply (rule p(5)) + unfolding uv xk + apply (rule insertI1) + apply (rule insertI2) + apply assumption + using insert(2) + unfolding uv xk + apply auto + done + show ?case + proof (cases "cbox u v \ d x") + case True + then show ?thesis + apply (rule_tac x="{(x,cbox u v)} \ q1" in exI) + apply rule + unfolding * uv + apply (rule tagged_division_union) + apply (rule tagged_division_of_self) + apply (rule p[unfolded xk uv] insertI1)+ + apply (rule q1) + apply (rule int) + apply rule + apply (rule fine_union) + apply (subst fine_def) + defer + apply (rule q1) + unfolding Ball_def split_paired_All split_conv + apply rule + apply rule + apply rule + apply rule + apply (erule insertE) + apply (simp add: uv xk) + apply (rule UnI2) + apply (drule q1(3)[rule_format]) + unfolding xk uv + apply auto + done + next + case False + from fine_division_exists[OF assms(2), of u v] guess q2 . note q2=this + show ?thesis + apply (rule_tac x="q2 \ q1" in exI) + apply rule + unfolding * uv + apply (rule tagged_division_union q2 q1 int fine_union)+ + unfolding Ball_def split_paired_All split_conv + apply rule + apply (rule fine_union) + apply (rule q1 q2)+ + apply rule + apply rule + apply rule + apply rule + apply (erule insertE) + apply (rule UnI2) + apply (simp add: False uv xk) + apply (drule q1(3)[rule_format]) + using False + unfolding xk uv + apply auto + done + qed + qed +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)) *\<^sub>R i) + (\i \ Basis. (a \ i + ((f i + 1) / 2^n) * (b \ i - a \ i)) *\<^sub>R i)" + let ?D0 = "?K0 ` (SIGMA n:UNIV. PiE 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: divide_simps zero_le_mult_iff aibi) + apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem) + 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: divide_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 --\The symmetry argument requires a single HOL formula\ + proof (rule linorder_wlog [where a=m and b=n], intro allI impI) + fix v w m and n::nat + assume "m \ n" --\WLOG we can assume @{term"m \ n"}, when the first disjunct becomes impossible\ + 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 add: power_add, 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 \\<^sub>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 setsum.cong) + also have "... \ DIM('a) * (\ / (2 * real DIM('a)))" + by (meson setsum_bounded_above that) + also have "... = \ / 2" + by (simp add: divide_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: divide_simps) + then have "norm (b - a) < e * 2^n" + by (auto simp: divide_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 divide_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 divide_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 divide_simps) + done + also have "... = x \ i" + using abi_less by (simp add: divide_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: divide_simps algebra_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 \\<^sub>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 by (force simp: algebra_simps) + 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 \\<^sub>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)) *\<^sub>R i) + (\i\Basis. (a \ i + ((f i) + 1) / 2^n * (b \ i - a \ i)) *\<^sub>R i)) + ` (SIGMA m:atMost n. PiE Basis (\i::'a. lessThan (2^m)))" + have "?K0(m,g) \ ?B" if "g \ Basis \\<^sub>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: divide_simps algebra_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 algebra_simps divide_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 real_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})" + +lemma eventually_division_filter: + "(\\<^sub>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_inter) +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 \ No newline at end of file diff -r b235e845c8e8 -r c3da799b1b45 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Sep 28 16:15:51 2016 +0200 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Sep 29 13:02:43 2016 +0200 @@ -1414,7 +1414,7 @@ then have "cbox a b \ box c d" "box c d \cbox a b" by auto then show ?rhs - apply (simp add: subset_box) + apply (simp add: subset_box) using \cbox a b = box c d\ box_ne_empty box_sing apply (fastforce simp add:) done @@ -1435,7 +1435,7 @@ by auto then show ?rhs apply (simp add: subset_box) - using box_ne_empty(2) \box a b = box c d\ + using box_ne_empty(2) \box a b = box c d\ apply auto apply (meson euclidean_eqI less_eq_real_def not_less)+ done @@ -10009,6 +10009,83 @@ by (metis (no_types, lifting) IntD2 IntI f someI_ex) qed +lemma tube_lemma: + assumes "compact K" + assumes "open W" + assumes "{x0} \ K \ W" + shows "\X0. x0 \ X0 \ open X0 \ X0 \ K \ W" +proof - + { + fix y assume "y \ K" + then have "(x0, y) \ W" using assms by auto + with \open W\ + have "\X0 Y. open X0 \ open Y \ x0 \ X0 \ y \ Y \ X0 \ Y \ W" + by (rule open_prod_elim) blast + } + then obtain X0 Y where + *: "\y \ K. open (X0 y) \ open (Y y) \ x0 \ X0 y \ y \ Y y \ X0 y \ Y y \ W" + by metis + from * have "\t\Y ` K. open t" "K \ \(Y ` K)" by auto + with \compact K\ obtain CC where CC: "CC \ Y ` K" "finite CC" "K \ \CC" + by (rule compactE) + then obtain c where c: "\C. C \ CC \ c C \ K \ C = Y (c C)" + by (force intro!: choice) + with * CC show ?thesis + by (force intro!: exI[where x="\C\CC. X0 (c C)"]) (* SLOW *) +qed + +lemma continuous_on_prod_compactE: + fixes fx::"'a::topological_space \ 'b::topological_space \ 'c::metric_space" + and e::real + assumes cont_fx: "continuous_on (U \ C) fx" + assumes "compact C" + assumes [intro]: "x0 \ U" + notes [continuous_intros] = continuous_on_compose2[OF cont_fx] + assumes "e > 0" + obtains X0 where "x0 \ X0" "open X0" + "\x\X0 \ U. \t \ C. dist (fx (x, t)) (fx (x0, t)) \ e" +proof - + define psi where "psi = (\(x, t). dist (fx (x, t)) (fx (x0, t)))" + define W0 where "W0 = {(x, t) \ U \ C. psi (x, t) < e}" + have W0_eq: "W0 = psi -` {.. U \ C" + by (auto simp: vimage_def W0_def) + have "open {.. C) psi" + by (auto intro!: continuous_intros simp: psi_def split_beta') + from this[unfolded continuous_on_open_invariant, rule_format, OF \open {..] + obtain W where W: "open W" "W \ U \ C = W0 \ U \ C" + unfolding W0_eq by blast + have "{x0} \ C \ W \ U \ C" + unfolding W + by (auto simp: W0_def psi_def \0 < e\) + then have "{x0} \ C \ W" by blast + from tube_lemma[OF \compact C\ \open W\ this] + obtain X0 where X0: "x0 \ X0" "open X0" "X0 \ C \ W" + by blast + + have "\x\X0 \ U. \t \ C. dist (fx (x, t)) (fx (x0, t)) \ e" + proof safe + fix x assume x: "x \ X0" "x \ U" + fix t assume t: "t \ C" + have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)" + by (auto simp: psi_def) + also + { + have "(x, t) \ X0 \ C" + using t x + by auto + also note \\ \ W\ + finally have "(x, t) \ W" . + with t x have "(x, t) \ W \ U \ C" + by blast + also note \W \ U \ C = W0 \ U \ C\ + finally have "psi (x, t) < e" + by (auto simp: W0_def) + } + finally show "dist (fx (x, t)) (fx (x0, t)) \ e" by simp + qed + from X0(1,2) this show ?thesis .. +qed no_notation eucl_less (infix "