# HG changeset patch # User paulson # Date 1475240751 -3600 # Node ID 2aa42596edc3b3756d7f4fa922c55c2ae30a5aab # Parent 957ba35d1338092a043698cec697b92b959d1f2f new material on paths, etc. Also rationalisation diff -r 957ba35d1338 -r 2aa42596edc3 NEWS --- a/NEWS Fri Sep 30 10:00:49 2016 +0200 +++ b/NEWS Fri Sep 30 14:05:51 2016 +0100 @@ -267,14 +267,29 @@ clashes. INCOMPATIBILITY. -* Number_Theory: algebraic foundation for primes: Generalisation of +* In HOL-Probability the type of emeasure and nn_integral was changed +from ereal to ennreal: + emeasure :: 'a measure => 'a set => ennreal + nn_integral :: 'a measure => ('a => ennreal) => ennreal +INCOMPATIBILITY. + +* HOL-Analysis: more complex analysis including Cauchy's inequality, Liouville theorem, +open mapping theorem, maximum modulus principle, Residue theorem, Schwarz Lemma. + +* HOL-Analysis: Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman +Minkowski theorem. + +* HOL-Analysis: Numerous results ported from the HOL Light libraries: homeomorphisms, +continuous function extensions and other advanced topics in topology + +* Number_Theory: algebraic foundation for primes: Generalisation of predicate "prime" and introduction of predicates "prime_elem", -"irreducible", a "prime_factorization" function, and the "factorial_ring" -typeclass with instance proofs for nat, int, poly. Some theorems now have +"irreducible", a "prime_factorization" function, and the "factorial_ring" +typeclass with instance proofs for nat, int, poly. Some theorems now have different names, most notably "prime_def" is now "prime_nat_iff". INCOMPATIBILITY. -* Probability: Code generation and QuickCheck for Probability Mass +* Probability: Code generation and QuickCheck for Probability Mass Functions. * Theory Set_Interval.thy: substantial new theorems on indexed sums @@ -297,9 +312,9 @@ * Theory Library/Perm.thy: basic facts about almost everywhere fix bijections. -* Theory Library/Normalized_Fraction.thy: allows viewing an element -of a field of fractions as a normalized fraction (i.e. a pair of -numerator and denominator such that the two are coprime and the +* Theory Library/Normalized_Fraction.thy: allows viewing an element +of a field of fractions as a normalized fraction (i.e. a pair of +numerator and denominator such that the two are coprime and the denominator is normalized w.r.t. unit factors) * Locale bijection establishes convenient default simp rules @@ -330,8 +345,8 @@ a small guarantee that given constants specify a safe interface for the generated code. -* Probability/Random_Permutations.thy contains some theory about -choosing a permutation of a set uniformly at random and folding over a +* Probability/Random_Permutations.thy contains some theory about +choosing a permutation of a set uniformly at random and folding over a list in random order. * Probability/SPMF formalises discrete subprobability distributions. @@ -341,8 +356,8 @@ former Library/FinFun_Syntax.thy. INCOMPATIBILITY, e.g. use "unbundle finfun_syntax" to imitate import of "~~/src/HOL/Library/FinFun_Syntax". -* Library/Set_Permutations.thy (executably) defines the set of -permutations of a set, i.e. the set of all lists that contain every +* Library/Set_Permutations.thy (executably) defines the set of +permutations of a set, i.e. the set of all lists that contain every element of the carrier set exactly once. * Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on @@ -363,7 +378,7 @@ break existing proofs. INCOMPATIBILITY. * Sledgehammer: - - The MaSh relevance filter has been sped up. + - The MaSh relevance filter is now faster than before. - Produce syntactically correct Vampire 4.0 problem files. * The 'coinductive' command produces a proper coinduction rule for @@ -678,12 +693,6 @@ * Compound constants INFIMUM and SUPREMUM are mere abbreviations now. INCOMPATIBILITY. -* More complex analysis including Cauchy's inequality, Liouville theorem, -open mapping theorem, maximum modulus principle, Residue theorem, Schwarz Lemma. - -* Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman -Minkowski theorem. - * "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` A)". @@ -815,14 +824,8 @@ * Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis. -* In HOL-Probability the type of emeasure and nn_integral was changed -from ereal to ennreal: - emeasure :: 'a measure => 'a set => ennreal - nn_integral :: 'a measure => ('a => ennreal) => ennreal -INCOMPATIBILITY. - -* Renamed HOL/Quotient_Examples/FSet.thy to -HOL/Quotient_Examples/Quotient_FSet.thy +* Renamed HOL/Quotient_Examples/FSet.thy to +HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY. *** ML *** diff -r 957ba35d1338 -r 2aa42596edc3 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Sep 30 10:00:49 2016 +0200 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Sep 30 14:05:51 2016 +0100 @@ -8764,12 +8764,6 @@ qed qed -lemma rel_frontier_convex_Int_affine: - fixes S :: "'a::euclidean_space set" - assumes "convex S" "affine T" "interior S \ T \ {}" - shows "rel_frontier(S \ T) = frontier S \ T" -by (simp add: assms convex_affine_rel_frontier_Int) - lemma subset_rel_interior_convex: fixes S T :: "'n::euclidean_space set" assumes "convex S" diff -r 957ba35d1338 -r 2aa42596edc3 src/HOL/Analysis/Path_Connected.thy --- a/src/HOL/Analysis/Path_Connected.thy Fri Sep 30 10:00:49 2016 +0200 +++ b/src/HOL/Analysis/Path_Connected.thy Fri Sep 30 14:05:51 2016 +0100 @@ -5,7 +5,7 @@ section \Continuous paths and path-connected sets\ theory Path_Connected -imports Continuous_Extension +imports Continuous_Extension "~~/src/HOL/Library/Continuum_Not_Denumerable" begin subsection \Paths and Arcs\ @@ -6244,4 +6244,1422 @@ by blast qed +subsection\Some Uncountable Sets\ + +lemma uncountable_closed_segment: + fixes a :: "'a::real_normed_vector" + assumes "a \ b" shows "uncountable (closed_segment a b)" +unfolding path_image_linepath [symmetric] path_image_def + using inj_on_linepath [OF assms] uncountable_closed_interval [of 0 1] + countable_image_inj_on by auto + +lemma uncountable_open_segment: + fixes a :: "'a::real_normed_vector" + assumes "a \ b" shows "uncountable (open_segment a b)" + by (simp add: assms open_segment_def uncountable_closed_segment uncountable_minus_countable) + +lemma uncountable_convex: + fixes a :: "'a::real_normed_vector" + assumes "convex S" "a \ S" "b \ S" "a \ b" + shows "uncountable S" +proof - + have "uncountable (closed_segment a b)" + by (simp add: uncountable_closed_segment assms) + then show ?thesis + by (meson assms convex_contains_segment countable_subset) +qed + +lemma uncountable_ball: + fixes a :: "'a::euclidean_space" + assumes "r > 0" + shows "uncountable (ball a r)" +proof - + have "uncountable (open_segment a (a + r *\<^sub>R (SOME i. i \ Basis)))" + by (metis Basis_zero SOME_Basis add_cancel_right_right assms less_le real_vector.scale_eq_0_iff uncountable_open_segment) + moreover have "open_segment a (a + r *\<^sub>R (SOME i. i \ Basis)) \ ball a r" + using assms by (auto simp: in_segment algebra_simps dist_norm SOME_Basis) + ultimately show ?thesis + by (metis countable_subset) +qed + +lemma uncountable_cball: + fixes a :: "'a::euclidean_space" + assumes "r > 0" + shows "uncountable (cball a r)" + using assms countable_subset uncountable_ball by auto + +lemma pairwise_disjnt_countable: + fixes \ :: "nat set set" + assumes "pairwise disjnt \" + shows "countable \" +proof - + have "inj_on (\X. SOME n. n \ X) (\ - {{}})" + apply (clarsimp simp add: inj_on_def) + by (metis assms disjnt_insert2 insert_absorb pairwise_def subsetI subset_empty tfl_some) + then show ?thesis + by (metis countable_Diff_eq countable_def) +qed + +lemma pairwise_disjnt_countable_Union: + assumes "countable (\\)" and pwd: "pairwise disjnt \" + shows "countable \" +proof - + obtain f :: "_ \ nat" where f: "inj_on f (\\)" + using assms by blast + then have "pairwise disjnt (\ X \ \. {f ` X})" + using assms by (force simp: pairwise_def disjnt_inj_on_iff [OF f]) + then have "countable (\ X \ \. {f ` X})" + using pairwise_disjnt_countable by blast + then show ?thesis + by (meson pwd countable_image_inj_on disjoint_image f inj_on_image pairwise_disjnt_countable) +qed + + +subsection\ Some simple positive connection theorems\ + +proposition path_connected_convex_diff_countable: + fixes U :: "'a::euclidean_space set" + assumes "convex U" "~ collinear U" "countable S" + shows "path_connected(U - S)" +proof (clarsimp simp add: path_connected_def) + fix a b + assume "a \ U" "a \ S" "b \ U" "b \ S" + let ?m = "midpoint a b" + show "\g. path g \ path_image g \ U - S \ pathstart g = a \ pathfinish g = b" + proof (cases "a = b") + case True + then show ?thesis + by (metis DiffI \a \ U\ \a \ S\ path_component_def path_component_refl) + next + case False + then have "a \ ?m" "b \ ?m" + using midpoint_eq_endpoint by fastforce+ + have "?m \ U" + using \a \ U\ \b \ U\ \convex U\ convex_contains_segment by force + obtain c where "c \ U" and nc_abc: "\ collinear {a,b,c}" + by (metis False \a \ U\ \b \ U\ \~ collinear U\ collinear_triples insert_absorb) + have ncoll_mca: "\ collinear {?m,c,a}" + by (metis (full_types) \a \ ?m\ collinear_3_trans collinear_midpoint insert_commute nc_abc) + have ncoll_mcb: "\ collinear {?m,c,b}" + by (metis (full_types) \b \ ?m\ collinear_3_trans collinear_midpoint insert_commute nc_abc) + have "c \ ?m" + by (metis collinear_midpoint insert_commute nc_abc) + then have "closed_segment ?m c \ U" + by (simp add: \c \ U\ \?m \ U\ \convex U\ closed_segment_subset) + then obtain z where z: "z \ closed_segment ?m c" + and disjS: "(closed_segment a z \ closed_segment z b) \ S = {}" + proof - + have False if "closed_segment ?m c \ {z. (closed_segment a z \ closed_segment z b) \ S \ {}}" + proof - + have closb: "closed_segment ?m c \ + {z \ closed_segment ?m c. closed_segment a z \ S \ {}} \ {z \ closed_segment ?m c. closed_segment z b \ S \ {}}" + using that by blast + have *: "countable {z \ closed_segment ?m c. closed_segment z u \ S \ {}}" + if "u \ U" "u \ S" and ncoll: "\ collinear {?m, c, u}" for u + proof - + have **: False if x1: "x1 \ closed_segment ?m c" and x2: "x2 \ closed_segment ?m c" + and "x1 \ x2" "x1 \ u" + and w: "w \ closed_segment x1 u" "w \ closed_segment x2 u" + and "w \ S" for x1 x2 w + proof - + have "x1 \ affine hull {?m,c}" "x2 \ affine hull {?m,c}" + using segment_as_ball x1 x2 by auto + then have coll_x1: "collinear {x1, ?m, c}" and coll_x2: "collinear {?m, c, x2}" + by (simp_all add: affine_hull_3_imp_collinear) (metis affine_hull_3_imp_collinear insert_commute) + have "\ collinear {x1, u, x2}" + proof + assume "collinear {x1, u, x2}" + then have "collinear {?m, c, u}" + by (metis (full_types) \c \ ?m\ coll_x1 coll_x2 collinear_3_trans insert_commute ncoll \x1 \ x2\) + with ncoll show False .. + qed + then have "closed_segment x1 u \ closed_segment u x2 = {u}" + by (blast intro!: Int_closed_segment) + then have "w = u" + using closed_segment_commute w by auto + show ?thesis + using \u \ S\ \w = u\ that(7) by auto + qed + then have disj: "disjoint ((\z\closed_segment ?m c. {closed_segment z u \ S}))" + by (fastforce simp: pairwise_def disjnt_def) + have cou: "countable ((\z \ closed_segment ?m c. {closed_segment z u \ S}) - {{}})" + apply (rule pairwise_disjnt_countable_Union [OF _ pairwise_subset [OF disj]]) + apply (rule countable_subset [OF _ \countable S\], auto) + done + define f where "f \ \X. (THE z. z \ closed_segment ?m c \ X = closed_segment z u \ S)" + show ?thesis + proof (rule countable_subset [OF _ countable_image [OF cou, where f=f]], clarify) + fix x + assume x: "x \ closed_segment ?m c" "closed_segment x u \ S \ {}" + show "x \ f ` ((\z\closed_segment ?m c. {closed_segment z u \ S}) - {{}})" + proof (rule_tac x="closed_segment x u \ S" in image_eqI) + show "x = f (closed_segment x u \ S)" + unfolding f_def + apply (rule the_equality [symmetric]) + using x apply (auto simp: dest: **) + done + qed (use x in auto) + qed + qed + have "uncountable (closed_segment ?m c)" + by (metis \c \ ?m\ uncountable_closed_segment) + then show False + using closb * [OF \a \ U\ \a \ S\ ncoll_mca] * [OF \b \ U\ \b \ S\ ncoll_mcb] + apply (simp add: closed_segment_commute) + by (simp add: countable_subset) + qed + then show ?thesis + by (force intro: that) + qed + show ?thesis + proof (intro exI conjI) + have "path_image (linepath a z +++ linepath z b) \ U" + by (metis \a \ U\ \b \ U\ \closed_segment ?m c \ U\ z \convex U\ closed_segment_subset contra_subsetD path_image_linepath subset_path_image_join) + with disjS show "path_image (linepath a z +++ linepath z b) \ U - S" + by (force simp: path_image_join) + qed auto + qed +qed + + +corollary connected_convex_diff_countable: + fixes U :: "'a::euclidean_space set" + assumes "convex U" "~ collinear U" "countable S" + shows "connected(U - S)" + by (simp add: assms path_connected_convex_diff_countable path_connected_imp_connected) + +lemma path_connected_punctured_convex: + assumes "convex S" and aff: "aff_dim S \ 1" + shows "path_connected(S - {a})" +proof - + consider "aff_dim S = -1" | "aff_dim S = 0" | "aff_dim S \ 2" + using assms aff_dim_geq [of S] by linarith + then show ?thesis + proof cases + assume "aff_dim S = -1" + then show ?thesis + by (metis aff_dim_empty empty_Diff path_connected_empty) + next + assume "aff_dim S = 0" + then show ?thesis + by (metis aff_dim_eq_0 Diff_cancel Diff_empty Diff_insert0 convex_empty convex_imp_path_connected path_connected_singleton singletonD) + next + assume ge2: "aff_dim S \ 2" + then have "\ collinear S" + proof (clarsimp simp add: collinear_affine_hull) + fix u v + assume "S \ affine hull {u, v}" + then have "aff_dim S \ aff_dim {u, v}" + by (metis (no_types) aff_dim_affine_hull aff_dim_subset) + with ge2 show False + by (metis (no_types) aff_dim_2 antisym aff not_numeral_le_zero one_le_numeral order_trans) + qed + then show ?thesis + apply (rule path_connected_convex_diff_countable [OF \convex S\]) + by simp + qed +qed + +lemma connected_punctured_convex: + shows "\convex S; aff_dim S \ 1\ \ connected(S - {a})" + using path_connected_imp_connected path_connected_punctured_convex by blast + +lemma path_connected_complement_countable: + fixes S :: "'a::euclidean_space set" + assumes "2 \ DIM('a)" "countable S" + shows "path_connected(- S)" +proof - + have "path_connected(UNIV - S)" + apply (rule path_connected_convex_diff_countable) + using assms by (auto simp: collinear_aff_dim [of "UNIV :: 'a set"]) + then show ?thesis + by (simp add: Compl_eq_Diff_UNIV) +qed + +proposition path_connected_openin_diff_countable: + fixes S :: "'a::euclidean_space set" + assumes "connected S" and ope: "openin (subtopology euclidean (affine hull S)) S" + and "~ collinear S" "countable T" + shows "path_connected(S - T)" +proof (clarsimp simp add: path_connected_component) + fix x y + assume xy: "x \ S" "x \ T" "y \ S" "y \ T" + show "path_component (S - T) x y" + proof (rule connected_equivalence_relation_gen [OF \connected S\, where P = "\x. x \ T"]) + show "\z. z \ U \ z \ T" if opeU: "openin (subtopology euclidean S) U" and "x \ U" for U x + proof - + have "openin (subtopology euclidean (affine hull S)) U" + using opeU ope openin_trans by blast + with \x \ U\ obtain r where Usub: "U \ affine hull S" and "r > 0" + and subU: "ball x r \ affine hull S \ U" + by (auto simp: openin_contains_ball) + with \x \ U\ have x: "x \ ball x r \ affine hull S" + by auto + have "~ S \ {x}" + using \~ collinear S\ collinear_subset by blast + then obtain x' where "x' \ x" "x' \ S" + by blast + obtain y where y: "y \ x" "y \ ball x r \ affine hull S" + proof + show "x + (r / 2 / norm(x' - x)) *\<^sub>R (x' - x) \ x" + using \x' \ x\ \r > 0\ by auto + show "x + (r / 2 / norm (x' - x)) *\<^sub>R (x' - x) \ ball x r \ affine hull S" + using \x' \ x\ \r > 0\ \x' \ S\ x + by (simp add: dist_norm mem_affine_3_minus hull_inc) + qed + have "convex (ball x r \ affine hull S)" + by (simp add: affine_imp_convex convex_Int) + with x y subU have "uncountable U" + by (meson countable_subset uncountable_convex) + then have "\ U \ T" + using \countable T\ countable_subset by blast + then show ?thesis by blast + qed + show "\U. openin (subtopology euclidean S) U \ x \ U \ + (\x\U. \y\U. x \ T \ y \ T \ path_component (S - T) x y)" + if "x \ S" for x + proof - + obtain r where Ssub: "S \ affine hull S" and "r > 0" + and subS: "ball x r \ affine hull S \ S" + using ope \x \ S\ by (auto simp: openin_contains_ball) + then have conv: "convex (ball x r \ affine hull S)" + by (simp add: affine_imp_convex convex_Int) + have "\ aff_dim (affine hull S) \ 1" + using \\ collinear S\ collinear_aff_dim by auto + then have "\ collinear (ball x r \ affine hull S)" + apply (simp add: collinear_aff_dim) + by (metis (no_types, hide_lams) aff_dim_convex_Int_open IntI Topology_Euclidean_Space.open_ball \0 < r\ aff_dim_affine_hull affine_affine_hull affine_imp_convex centre_in_ball empty_iff hull_subset inf_commute subsetCE that) + then have *: "path_connected ((ball x r \ affine hull S) - T)" + by (rule path_connected_convex_diff_countable [OF conv _ \countable T\]) + have ST: "ball x r \ affine hull S - T \ S - T" + using subS by auto + show ?thesis + proof (intro exI conjI) + show "x \ ball x r \ affine hull S" + using \x \ S\ \r > 0\ by (simp add: hull_inc) + have "openin (subtopology euclidean (affine hull S)) (ball x r \ affine hull S)" + by (simp add: inf.commute openin_Int_open) + then show "openin (subtopology euclidean S) (ball x r \ affine hull S)" + by (rule openin_subset_trans [OF _ subS Ssub]) + qed (use * path_component_trans in \auto simp: path_connected_component path_component_of_subset [OF ST]\) + qed + qed (use xy path_component_trans in auto) +qed + +corollary connected_openin_diff_countable: + fixes S :: "'a::euclidean_space set" + assumes "connected S" and ope: "openin (subtopology euclidean (affine hull S)) S" + and "~ collinear S" "countable T" + shows "connected(S - T)" + by (metis path_connected_imp_connected path_connected_openin_diff_countable [OF assms]) + +corollary path_connected_open_diff_countable: + fixes S :: "'a::euclidean_space set" + assumes "2 \ DIM('a)" "open S" "connected S" "countable T" + shows "path_connected(S - T)" +proof (cases "S = {}") + case True + then show ?thesis + by (simp add: path_connected_empty) +next + case False + show ?thesis + proof (rule path_connected_openin_diff_countable) + show "openin (subtopology euclidean (affine hull S)) S" + by (simp add: assms hull_subset open_subset) + show "\ collinear S" + using assms False by (simp add: collinear_aff_dim aff_dim_open) + qed (simp_all add: assms) +qed + +corollary connected_open_diff_countable: + fixes S :: "'a::euclidean_space set" + assumes "2 \ DIM('a)" "open S" "connected S" "countable T" + shows "connected(S - T)" +by (simp add: assms path_connected_imp_connected path_connected_open_diff_countable) + + + +subsection\ Self-homeomorphisms shuffling points about in various ways.\ + +subsubsection\The theorem @{text homeomorphism_moving_points_exists}}\ + +lemma homeomorphism_moving_point_1: + fixes a :: "'a::euclidean_space" + assumes "affine T" "a \ T" and u: "u \ ball a r \ T" + obtains f g where "homeomorphism (cball a r \ T) (cball a r \ T) f g" + "f a = u" "\x. x \ sphere a r \ f x = x" +proof - + have nou: "norm (u - a) < r" and "u \ T" + using u by (auto simp: dist_norm norm_minus_commute) + then have "0 < r" + by (metis DiffD1 Diff_Diff_Int ball_eq_empty centre_in_ball not_le u) + define f where "f \ \x. (1 - norm(x - a) / r) *\<^sub>R (u - a) + x" + have *: "False" if eq: "x + (norm y / r) *\<^sub>R u = y + (norm x / r) *\<^sub>R u" + and nou: "norm u < r" and yx: "norm y < norm x" for x y and u::'a + proof - + have "x = y + (norm x / r - (norm y / r)) *\<^sub>R u" + using eq by (simp add: algebra_simps) + then have "norm x = norm (y + ((norm x - norm y) / r) *\<^sub>R u)" + by (metis diff_divide_distrib) + also have "... \ norm y + norm(((norm x - norm y) / r) *\<^sub>R u)" + using norm_triangle_ineq by blast + also have "... = norm y + (norm x - norm y) * (norm u / r)" + using yx \r > 0\ + by (simp add: divide_simps) + also have "... < norm y + (norm x - norm y) * 1" + apply (subst add_less_cancel_left) + apply (rule mult_strict_left_mono) + using nou \0 < r\ yx + apply (simp_all add: field_simps) + done + also have "... = norm x" + by simp + finally show False by simp + qed + have "inj f" + unfolding f_def + proof (clarsimp simp: inj_on_def) + fix x y + assume "(1 - norm (x - a) / r) *\<^sub>R (u - a) + x = + (1 - norm (y - a) / r) *\<^sub>R (u - a) + y" + then have eq: "(x - a) + (norm (y - a) / r) *\<^sub>R (u - a) = (y - a) + (norm (x - a) / r) *\<^sub>R (u - a)" + by (auto simp: algebra_simps) + show "x=y" + proof (cases "norm (x - a) = norm (y - a)") + case True + then show ?thesis + using eq by auto + next + case False + then consider "norm (x - a) < norm (y - a)" | "norm (x - a) > norm (y - a)" + by linarith + then have "False" + proof cases + case 1 show False + using * [OF _ nou 1] eq by simp + next + case 2 with * [OF eq nou] show False + by auto + qed + then show "x=y" .. + qed + qed + then have inj_onf: "inj_on f (cball a r \ T)" + using inj_on_Int by fastforce + have contf: "continuous_on (cball a r \ T) f" + unfolding f_def using \0 < r\ by (intro continuous_intros) blast + have fim: "f ` (cball a r \ T) = cball a r \ T" + proof + have *: "norm (y + (1 - norm y / r) *\<^sub>R u) \ r" if "norm y \ r" "norm u < r" for y u::'a + proof - + have "norm (y + (1 - norm y / r) *\<^sub>R u) \ norm y + norm((1 - norm y / r) *\<^sub>R u)" + using norm_triangle_ineq by blast + also have "... = norm y + abs(1 - norm y / r) * norm u" + by simp + also have "... \ r" + proof - + have "(r - norm u) * (r - norm y) \ 0" + using that by auto + then have "r * norm u + r * norm y \ r * r + norm u * norm y" + by (simp add: algebra_simps) + then show ?thesis + using that \0 < r\ by (simp add: abs_if field_simps) + qed + finally show ?thesis . + qed + have "f ` (cball a r) \ cball a r" + apply (clarsimp simp add: dist_norm norm_minus_commute f_def) + using * by (metis diff_add_eq diff_diff_add diff_diff_eq2 norm_minus_commute nou) + moreover have "f ` T \ T" + unfolding f_def using \affine T\ \a \ T\ \u \ T\ + by (force simp: add.commute mem_affine_3_minus) + ultimately show "f ` (cball a r \ T) \ cball a r \ T" + by blast + next + show "cball a r \ T \ f ` (cball a r \ T)" + proof (clarsimp simp add: dist_norm norm_minus_commute) + fix x + assume x: "norm (x - a) \ r" and "x \ T" + have "\v \ {0..1}. ((1 - v) * r - norm ((x - a) - v *\<^sub>R (u - a))) \ 1 = 0" + by (rule ivt_decreasing_component_on_1) (auto simp: x continuous_intros) + then obtain v where "0\v" "v\1" and v: "(1 - v) * r = norm ((x - a) - v *\<^sub>R (u - a))" + by auto + show "x \ f ` (cball a r \ T)" + proof (rule image_eqI) + show "x = f (x - v *\<^sub>R (u - a))" + using \r > 0\ v by (simp add: f_def field_simps) + have "x - v *\<^sub>R (u - a) \ cball a r" + using \r > 0\ v \0 \ v\ + apply (simp add: field_simps dist_norm norm_minus_commute) + by (metis le_add_same_cancel2 order.order_iff_strict zero_le_mult_iff) + moreover have "x - v *\<^sub>R (u - a) \ T" + by (simp add: f_def \affine T\ \u \ T\ \x \ T\ assms mem_affine_3_minus2) + ultimately show "x - v *\<^sub>R (u - a) \ cball a r \ T" + by blast + qed + qed + qed + have "\g. homeomorphism (cball a r \ T) (cball a r \ T) f g" + apply (rule homeomorphism_compact [OF _ contf fim inj_onf]) + apply (simp add: affine_closed compact_Int_closed \affine T\) + done + then show ?thesis + apply (rule exE) + apply (erule_tac f=f in that) + using \r > 0\ + apply (simp_all add: f_def dist_norm norm_minus_commute) + done +qed + +corollary homeomorphism_moving_point_2: + fixes a :: "'a::euclidean_space" + assumes "affine T" "a \ T" and u: "u \ ball a r \ T" and v: "v \ ball a r \ T" + obtains f g where "homeomorphism (cball a r \ T) (cball a r \ T) f g" + "f u = v" "\x. \x \ sphere a r; x \ T\ \ f x = x" +proof - + have "0 < r" + by (metis DiffD1 Diff_Diff_Int ball_eq_empty centre_in_ball not_le u) + obtain f1 g1 where hom1: "homeomorphism (cball a r \ T) (cball a r \ T) f1 g1" + and "f1 a = u" and f1: "\x. x \ sphere a r \ f1 x = x" + using homeomorphism_moving_point_1 [OF \affine T\ \a \ T\ u] by blast + obtain f2 g2 where hom2: "homeomorphism (cball a r \ T) (cball a r \ T) f2 g2" + and "f2 a = v" and f2: "\x. x \ sphere a r \ f2 x = x" + using homeomorphism_moving_point_1 [OF \affine T\ \a \ T\ v] by blast + show ?thesis + proof + show "homeomorphism (cball a r \ T) (cball a r \ T) (f2 \ g1) (f1 \ g2)" + by (metis homeomorphism_compose homeomorphism_symD hom1 hom2) + have "g1 u = a" + using \0 < r\ \f1 a = u\ assms hom1 homeomorphism_apply1 by fastforce + then show "(f2 \ g1) u = v" + by (simp add: \f2 a = v\) + show "\x. \x \ sphere a r; x \ T\ \ (f2 \ g1) x = x" + using f1 f2 hom1 homeomorphism_apply1 by fastforce + qed +qed + + +corollary homeomorphism_moving_point_3: + fixes a :: "'a::euclidean_space" + assumes "affine T" "a \ T" and ST: "ball a r \ T \ S" "S \ T" + and u: "u \ ball a r \ T" and v: "v \ ball a r \ T" + obtains f g where "homeomorphism S S f g" + "f u = v" "{x. ~ (f x = x \ g x = x)} \ ball a r \ T" +proof - + obtain f g where hom: "homeomorphism (cball a r \ T) (cball a r \ T) f g" + and "f u = v" and fid: "\x. \x \ sphere a r; x \ T\ \ f x = x" + using homeomorphism_moving_point_2 [OF \affine T\ \a \ T\ u v] by blast + have gid: "\x. \x \ sphere a r; x \ T\ \ g x = x" + using fid hom homeomorphism_apply1 by fastforce + define ff where "ff \ \x. if x \ ball a r \ T then f x else x" + define gg where "gg \ \x. if x \ ball a r \ T then g x else x" + show ?thesis + proof + show "homeomorphism S S ff gg" + proof (rule homeomorphismI) + have "continuous_on ((cball a r \ T) \ (T - ball a r)) ff" + apply (simp add: ff_def) + apply (rule continuous_on_cases) + using homeomorphism_cont1 [OF hom] + apply (auto simp: affine_closed \affine T\ continuous_on_id fid) + done + then show "continuous_on S ff" + apply (rule continuous_on_subset) + using ST by auto + have "continuous_on ((cball a r \ T) \ (T - ball a r)) gg" + apply (simp add: gg_def) + apply (rule continuous_on_cases) + using homeomorphism_cont2 [OF hom] + apply (auto simp: affine_closed \affine T\ continuous_on_id gid) + done + then show "continuous_on S gg" + apply (rule continuous_on_subset) + using ST by auto + show "ff ` S \ S" + proof (clarsimp simp add: ff_def) + fix x + assume "x \ S" and x: "dist a x < r" and "x \ T" + then have "f x \ cball a r \ T" + using homeomorphism_image1 [OF hom] by force + then show "f x \ S" + using ST(1) \x \ T\ gid hom homeomorphism_def x by fastforce + qed + show "gg ` S \ S" + proof (clarsimp simp add: gg_def) + fix x + assume "x \ S" and x: "dist a x < r" and "x \ T" + then have "g x \ cball a r \ T" + using homeomorphism_image2 [OF hom] by force + then have "g x \ ball a r" + using homeomorphism_apply2 [OF hom] + by (metis Diff_Diff_Int Diff_iff \x \ T\ cball_def fid le_less mem_Collect_eq mem_ball mem_sphere x) + then show "g x \ S" + using ST(1) \g x \ cball a r \ T\ by force + qed + show "\x. x \ S \ gg (ff x) = x" + apply (simp add: ff_def gg_def) + using homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] + apply auto + apply (metis Int_iff homeomorphism_apply1 [OF hom] fid image_eqI less_eq_real_def mem_cball mem_sphere) + done + show "\x. x \ S \ ff (gg x) = x" + apply (simp add: ff_def gg_def) + using homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] + apply auto + apply (metis Int_iff fid image_eqI less_eq_real_def mem_cball mem_sphere) + done + qed + show "ff u = v" + using u by (auto simp: ff_def \f u = v\) + show "{x. \ (ff x = x \ gg x = x)} \ ball a r \ T" + by (auto simp: ff_def gg_def) + qed +qed + + +proposition homeomorphism_moving_point: + fixes a :: "'a::euclidean_space" + assumes ope: "openin (subtopology euclidean (affine hull S)) S" + and "S \ T" + and TS: "T \ affine hull S" + and S: "connected S" "a \ S" "b \ S" + obtains f g where "homeomorphism T T f g" "f a = b" + "{x. ~ (f x = x \ g x = x)} \ S" + "bounded {x. ~ (f x = x \ g x = x)}" +proof - + have 1: "\h k. homeomorphism T T h k \ h (f d) = d \ + {x. ~ (h x = x \ k x = x)} \ S \ bounded {x. ~ (h x = x \ k x = x)}" + if "d \ S" "f d \ S" and homfg: "homeomorphism T T f g" + and S: "{x. ~ (f x = x \ g x = x)} \ S" + and bo: "bounded {x. ~ (f x = x \ g x = x)}" for d f g + proof (intro exI conjI) + show homgf: "homeomorphism T T g f" + by (metis homeomorphism_symD homfg) + then show "g (f d) = d" + by (meson \S \ T\ homeomorphism_def subsetD \d \ S\) + show "{x. \ (g x = x \ f x = x)} \ S" + using S by blast + show "bounded {x. \ (g x = x \ f x = x)}" + using bo by (simp add: conj_commute) + qed + have 2: "\f g. homeomorphism T T f g \ f x = f2 (f1 x) \ + {x. \ (f x = x \ g x = x)} \ S \ bounded {x. \ (f x = x \ g x = x)}" + if "x \ S" "f1 x \ S" "f2 (f1 x) \ S" + and hom: "homeomorphism T T f1 g1" "homeomorphism T T f2 g2" + and sub: "{x. \ (f1 x = x \ g1 x = x)} \ S" "{x. \ (f2 x = x \ g2 x = x)} \ S" + and bo: "bounded {x. \ (f1 x = x \ g1 x = x)}" "bounded {x. \ (f2 x = x \ g2 x = x)}" + for x f1 f2 g1 g2 + proof (intro exI conjI) + show homgf: "homeomorphism T T (f2 \ f1) (g1 \ g2)" + by (metis homeomorphism_compose hom) + then show "(f2 \ f1) x = f2 (f1 x)" + by force + show "{x. \ ((f2 \ f1) x = x \ (g1 \ g2) x = x)} \ S" + using sub by force + have "bounded ({x. ~(f1 x = x \ g1 x = x)} \ {x. ~(f2 x = x \ g2 x = x)})" + using bo by simp + then show "bounded {x. \ ((f2 \ f1) x = x \ (g1 \ g2) x = x)}" + by (rule bounded_subset) auto + qed + have 3: "\U. openin (subtopology euclidean S) U \ + d \ U \ + (\x\U. + \f g. homeomorphism T T f g \ f d = x \ + {x. \ (f x = x \ g x = x)} \ S \ + bounded {x. \ (f x = x \ g x = x)})" + if "d \ S" for d + proof - + obtain r where "r > 0" and r: "ball d r \ affine hull S \ S" + by (metis \d \ S\ ope openin_contains_ball) + have *: "\f g. homeomorphism T T f g \ f d = e \ + {x. \ (f x = x \ g x = x)} \ S \ + bounded {x. \ (f x = x \ g x = x)}" if "e \ S" "e \ ball d r" for e + apply (rule homeomorphism_moving_point_3 [of "affine hull S" d r T d e]) + using r \S \ T\ TS that + apply (auto simp: \d \ S\ \0 < r\ hull_inc) + using bounded_subset by blast + show ?thesis + apply (rule_tac x="S \ ball d r" in exI) + apply (intro conjI) + apply (simp add: openin_open_Int) + apply (simp add: \0 < r\ that) + apply (blast intro: *) + done + qed + have "\f g. homeomorphism T T f g \ f a = b \ + {x. ~ (f x = x \ g x = x)} \ S \ bounded {x. ~ (f x = x \ g x = x)}" + apply (rule connected_equivalence_relation [OF S], safe) + apply (blast intro: 1 2 3)+ + done + then show ?thesis + using that by auto +qed + + +lemma homeomorphism_moving_points_exists_gen: + assumes K: "finite K" "\i. i \ K \ x i \ S \ y i \ S" + "pairwise (\i j. (x i \ x j) \ (y i \ y j)) K" + and "2 \ aff_dim S" + and ope: "openin (subtopology euclidean (affine hull S)) S" + and "S \ T" "T \ affine hull S" "connected S" + shows "\f g. homeomorphism T T f g \ (\i \ K. f(x i) = y i) \ + {x. ~ (f x = x \ g x = x)} \ S \ bounded {x. ~ (f x = x \ g x = x)}" + using assms +proof (induction K) + case empty + then show ?case + by (force simp: homeomorphism_ident) +next + case (insert i K) + then have xney: "\j. \j \ K; j \ i\ \ x i \ x j \ y i \ y j" + and pw: "pairwise (\i j. x i \ x j \ y i \ y j) K" + and "x i \ S" "y i \ S" + and xyS: "\i. i \ K \ x i \ S \ y i \ S" + by (simp_all add: pairwise_insert) + obtain f g where homfg: "homeomorphism T T f g" and feq: "\i. i \ K \ f(x i) = y i" + and fg_sub: "{x. ~ (f x = x \ g x = x)} \ S" + and bo_fg: "bounded {x. ~ (f x = x \ g x = x)}" + using insert.IH [OF xyS pw] insert.prems by (blast intro: that) + then have "\f g. homeomorphism T T f g \ (\i \ K. f(x i) = y i) \ + {x. ~ (f x = x \ g x = x)} \ S \ bounded {x. ~ (f x = x \ g x = x)}" + using insert by blast + have aff_eq: "affine hull (S - y ` K) = affine hull S" + apply (rule affine_hull_Diff) + apply (auto simp: insert) + using \y i \ S\ insert.hyps(2) xney xyS by fastforce + have f_in_S: "f x \ S" if "x \ S" for x + using homfg fg_sub homeomorphism_apply1 \S \ T\ + proof - + have "(f (f x) \ f x \ g (f x) \ f x) \ f x \ S" + by (metis \S \ T\ homfg subsetD homeomorphism_apply1 that) + then show ?thesis + using fg_sub by force + qed + obtain h k where homhk: "homeomorphism T T h k" and heq: "h (f (x i)) = y i" + and hk_sub: "{x. \ (h x = x \ k x = x)} \ S - y ` K" + and bo_hk: "bounded {x. \ (h x = x \ k x = x)}" + proof (rule homeomorphism_moving_point [of "S - y`K" T "f(x i)" "y i"]) + show "openin (subtopology euclidean (affine hull (S - y ` K))) (S - y ` K)" + by (simp add: aff_eq openin_diff finite_imp_closedin image_subset_iff hull_inc insert xyS) + show "S - y ` K \ T" + using \S \ T\ by auto + show "T \ affine hull (S - y ` K)" + using insert by (simp add: aff_eq) + show "connected (S - y ` K)" + proof (rule connected_openin_diff_countable [OF \connected S\ ope]) + show "\ collinear S" + using collinear_aff_dim \2 \ aff_dim S\ by force + show "countable (y ` K)" + using countable_finite insert.hyps(1) by blast + qed + show "f (x i) \ S - y ` K" + apply (auto simp: f_in_S \x i \ S\) + by (metis feq homfg \x i \ S\ homeomorphism_def \S \ T\ \i \ K\ subsetCE xney xyS) + show "y i \ S - y ` K" + using insert.hyps xney by (auto simp: \y i \ S\) + qed blast + show ?case + proof (intro exI conjI) + show "homeomorphism T T (h \ f) (g \ k)" + using homfg homhk homeomorphism_compose by blast + show "\i \ insert i K. (h \ f) (x i) = y i" + using feq hk_sub by (auto simp: heq) + show "{x. \ ((h \ f) x = x \ (g \ k) x = x)} \ S" + using fg_sub hk_sub by force + have "bounded ({x. ~(f x = x \ g x = x)} \ {x. ~(h x = x \ k x = x)})" + using bo_fg bo_hk bounded_Un by blast + then show "bounded {x. \ ((h \ f) x = x \ (g \ k) x = x)}" + by (rule bounded_subset) auto + qed +qed + +proposition homeomorphism_moving_points_exists: + fixes S :: "'a::euclidean_space set" + assumes 2: "2 \ DIM('a)" "open S" "connected S" "S \ T" "finite K" + and KS: "\i. i \ K \ x i \ S \ y i \ S" + and pw: "pairwise (\i j. (x i \ x j) \ (y i \ y j)) K" + and S: "S \ T" "T \ affine hull S" "connected S" + obtains f g where "homeomorphism T T f g" "\i. i \ K \ f(x i) = y i" + "{x. ~ (f x = x \ g x = x)} \ S" "bounded {x. (~ (f x = x \ g x = x))}" +proof (cases "S = {}") + case True + then show ?thesis + using KS homeomorphism_ident that by fastforce +next + case False + then have affS: "affine hull S = UNIV" + by (simp add: affine_hull_open \open S\) + then have ope: "openin (subtopology euclidean (affine hull S)) S" + using \open S\ open_openin by auto + have "2 \ DIM('a)" by (rule 2) + also have "... = aff_dim (UNIV :: 'a set)" + by simp + also have "... \ aff_dim S" + by (metis aff_dim_UNIV aff_dim_affine_hull aff_dim_le_DIM affS) + finally have "2 \ aff_dim S" + by linarith + then show ?thesis + using homeomorphism_moving_points_exists_gen [OF \finite K\ KS pw _ ope S] that by fastforce +qed + + +subsubsection\The theorem @{text homeomorphism_grouping_points_exists}}\ + +lemma homeomorphism_grouping_point_1: + fixes a::real and c::real + assumes "a < b" "c < d" + obtains f g where "homeomorphism (cbox a b) (cbox c d) f g" "f a = c" "f b = d" +proof - + define f where "f \ \x. ((d - c) / (b - a)) * x + (c - a * ((d - c) / (b - a)))" + have "\g. homeomorphism (cbox a b) (cbox c d) f g" + proof (rule homeomorphism_compact) + show "continuous_on (cbox a b) f" + apply (simp add: f_def) + apply (intro continuous_intros) + using assms by auto + have "f ` {a..b} = {c..d}" + unfolding f_def image_affinity_atLeastAtMost + using assms sum_sqs_eq by (auto simp: divide_simps algebra_simps) + then show "f ` cbox a b = cbox c d" + by auto + show "inj_on f (cbox a b)" + unfolding f_def inj_on_def using assms by auto + qed auto + then obtain g where "homeomorphism (cbox a b) (cbox c d) f g" .. + then show ?thesis + proof + show "f a = c" + by (simp add: f_def) + show "f b = d" + using assms sum_sqs_eq [of a b] by (auto simp: f_def divide_simps algebra_simps) + qed +qed + +lemma homeomorphism_grouping_point_2: + fixes a::real and w::real + assumes hom_ab: "homeomorphism (cbox a b) (cbox u v) f1 g1" + and hom_bc: "homeomorphism (cbox b c) (cbox v w) f2 g2" + and "b \ cbox a c" "v \ cbox u w" + and eq: "f1 a = u" "f1 b = v" "f2 b = v" "f2 c = w" + obtains f g where "homeomorphism (cbox a c) (cbox u w) f g" "f a = u" "f c = w" + "\x. x \ cbox a b \ f x = f1 x" "\x. x \ cbox b c \ f x = f2 x" +proof - + have le: "a \ b" "b \ c" "u \ v" "v \ w" + using assms by simp_all + then have ac: "cbox a c = cbox a b \ cbox b c" and uw: "cbox u w = cbox u v \ cbox v w" + by auto + define f where "f \ \x. if x \ b then f1 x else f2 x" + have "\g. homeomorphism (cbox a c) (cbox u w) f g" + proof (rule homeomorphism_compact) + have cf1: "continuous_on (cbox a b) f1" + using hom_ab homeomorphism_cont1 by blast + have cf2: "continuous_on (cbox b c) f2" + using hom_bc homeomorphism_cont1 by blast + show "continuous_on (cbox a c) f" + apply (simp add: f_def) + apply (rule continuous_on_cases_le [OF continuous_on_subset [OF cf1] continuous_on_subset [OF cf2]]) + using le eq apply (force simp: continuous_on_id)+ + done + have "f ` cbox a b = f1 ` cbox a b" "f ` cbox b c = f2 ` cbox b c" + unfolding f_def using eq by force+ + then show "f ` cbox a c = cbox u w" + apply (simp only: ac uw image_Un) + by (metis hom_ab hom_bc homeomorphism_def) + have neq12: "f1 x \ f2 y" if x: "a \ x" "x \ b" and y: "b < y" "y \ c" for x y + proof - + have "f1 x \ cbox u v" + by (metis hom_ab homeomorphism_def image_eqI mem_box_real(2) x) + moreover have "f2 y \ cbox v w" + by (metis (full_types) hom_bc homeomorphism_def image_subset_iff mem_box_real(2) not_le not_less_iff_gr_or_eq order_refl y) + moreover have "f2 y \ f2 b" + by (metis cancel_comm_monoid_add_class.diff_cancel diff_gt_0_iff_gt hom_bc homeomorphism_def le(2) less_imp_le less_numeral_extra(3) mem_box_real(2) order_refl y) + ultimately show ?thesis + using le eq by simp + qed + have "inj_on f1 (cbox a b)" + by (metis (full_types) hom_ab homeomorphism_def inj_onI) + moreover have "inj_on f2 (cbox b c)" + by (metis (full_types) hom_bc homeomorphism_def inj_onI) + ultimately show "inj_on f (cbox a c)" + apply (simp (no_asm) add: inj_on_def) + apply (simp add: f_def inj_on_eq_iff) + using neq12 apply force + done + qed auto + then obtain g where "homeomorphism (cbox a c) (cbox u w) f g" .. + then show ?thesis + apply (rule that) + using eq le by (auto simp: f_def) +qed + +lemma homeomorphism_grouping_point_3: + fixes a::real + assumes cbox_sub: "cbox c d \ box a b" "cbox u v \ box a b" + and box_ne: "box c d \ {}" "box u v \ {}" + obtains f g where "homeomorphism (cbox a b) (cbox a b) f g" "f a = a" "f b = b" + "\x. x \ cbox c d \ f x \ cbox u v" +proof - + have less: "a < c" "a < u" "d < b" "v < b" "c < d" "u < v" "cbox c d \ {}" + using assms + by (simp_all add: cbox_sub subset_eq) + obtain f1 g1 where 1: "homeomorphism (cbox a c) (cbox a u) f1 g1" + and f1_eq: "f1 a = a" "f1 c = u" + using homeomorphism_grouping_point_1 [OF \a < c\ \a < u\] . + obtain f2 g2 where 2: "homeomorphism (cbox c d) (cbox u v) f2 g2" + and f2_eq: "f2 c = u" "f2 d = v" + using homeomorphism_grouping_point_1 [OF \c < d\ \u < v\] . + obtain f3 g3 where 3: "homeomorphism (cbox d b) (cbox v b) f3 g3" + and f3_eq: "f3 d = v" "f3 b = b" + using homeomorphism_grouping_point_1 [OF \d < b\ \v < b\] . + obtain f4 g4 where 4: "homeomorphism (cbox a d) (cbox a v) f4 g4" and "f4 a = a" "f4 d = v" + and f4_eq: "\x. x \ cbox a c \ f4 x = f1 x" "\x. x \ cbox c d \ f4 x = f2 x" + using homeomorphism_grouping_point_2 [OF 1 2] less by (auto simp: f1_eq f2_eq) + obtain f g where fg: "homeomorphism (cbox a b) (cbox a b) f g" "f a = a" "f b = b" + and f_eq: "\x. x \ cbox a d \ f x = f4 x" "\x. x \ cbox d b \ f x = f3 x" + using homeomorphism_grouping_point_2 [OF 4 3] less by (auto simp: f4_eq f3_eq f2_eq f1_eq) + show ?thesis + apply (rule that [OF fg]) + using f4_eq f_eq homeomorphism_image1 [OF 2] + apply simp + by (metis atLeastAtMost_iff box_real(1) box_real(2) cbox_sub(1) greaterThanLessThan_iff imageI less_eq_real_def subset_eq) +qed + + +lemma homeomorphism_grouping_point_4: + fixes T :: "real set" + assumes "open U" "open S" "connected S" "U \ {}" "finite K" "K \ S" "U \ S" "S \ T" + obtains f g where "homeomorphism T T f g" + "\x. x \ K \ f x \ U" "{x. (~ (f x = x \ g x = x))} \ S" + "bounded {x. (~ (f x = x \ g x = x))}" +proof - + obtain c d where "box c d \ {}" "cbox c d \ U" + proof - + obtain u where "u \ U" + using \U \ {}\ by blast + then obtain e where "e > 0" "cball u e \ U" + using \open U\ open_contains_cball by blast + then show ?thesis + by (rule_tac c=u and d="u+e" in that) (auto simp: dist_norm subset_iff) + qed + have "compact K" + by (simp add: \finite K\ finite_imp_compact) + obtain a b where "box a b \ {}" "K \ cbox a b" "cbox a b \ S" + proof (cases "K = {}") + case True then show ?thesis + using \box c d \ {}\ \cbox c d \ U\ \U \ S\ that by blast + next + case False + then obtain a b where "a \ K" "b \ K" + and a: "\x. x \ K \ a \ x" and b: "\x. x \ K \ x \ b" + using compact_attains_inf compact_attains_sup by (metis \compact K\)+ + obtain e where "e > 0" "cball b e \ S" + using \open S\ open_contains_cball + by (metis \b \ K\ \K \ S\ subsetD) + show ?thesis + proof + show "box a (b + e) \ {}" + using \0 < e\ \b \ K\ a by force + show "K \ cbox a (b + e)" + using \0 < e\ a b by fastforce + have "a \ S" + using \a \ K\ assms(6) by blast + have "b + e \ S" + using \0 < e\ \cball b e \ S\ by (force simp: dist_norm) + show "cbox a (b + e) \ S" + using \a \ S\ \b + e \ S\ \connected S\ connected_contains_Icc by auto + qed + qed + obtain w z where "cbox w z \ S" and sub_wz: "cbox a b \ cbox c d \ box w z" + proof - + have "a \ S" "b \ S" + using \box a b \ {}\ \cbox a b \ S\ by auto + moreover have "c \ S" "d \ S" + using \box c d \ {}\ \cbox c d \ U\ \U \ S\ by force+ + ultimately have "min a c \ S" "max b d \ S" + by linarith+ + then obtain e1 e2 where "e1 > 0" "cball (min a c) e1 \ S" "e2 > 0" "cball (max b d) e2 \ S" + using \open S\ open_contains_cball by metis + then have *: "min a c - e1 \ S" "max b d + e2 \ S" + by (auto simp: dist_norm) + show ?thesis + proof + show "cbox (min a c - e1) (max b d+ e2) \ S" + using * \connected S\ connected_contains_Icc by auto + show "cbox a b \ cbox c d \ box (min a c - e1) (max b d + e2)" + using \0 < e1\ \0 < e2\ by auto + qed + qed + then + obtain f g where hom: "homeomorphism (cbox w z) (cbox w z) f g" + and "f w = w" "f z = z" + and fin: "\x. x \ cbox a b \ f x \ cbox c d" + using homeomorphism_grouping_point_3 [of a b w z c d] + using \box a b \ {}\ \box c d \ {}\ by blast + have contfg: "continuous_on (cbox w z) f" "continuous_on (cbox w z) g" + using hom homeomorphism_def by blast+ + define f' where "f' \ \x. if x \ cbox w z then f x else x" + define g' where "g' \ \x. if x \ cbox w z then g x else x" + show ?thesis + proof + have T: "cbox w z \ (T - box w z) = T" + using \cbox w z \ S\ \S \ T\ by auto + show "homeomorphism T T f' g'" + proof + have clo: "closedin (subtopology euclidean (cbox w z \ (T - box w z))) (T - box w z)" + by (metis Diff_Diff_Int Diff_subset T closedin_def open_box openin_open_Int topspace_euclidean_subtopology) + have "continuous_on (cbox w z \ (T - box w z)) f'" "continuous_on (cbox w z \ (T - box w z)) g'" + unfolding f'_def g'_def + apply (safe intro!: continuous_on_cases_local contfg continuous_on_id clo) + apply (simp_all add: closed_subset) + using \f w = w\ \f z = z\ apply force + by (metis \f w = w\ \f z = z\ hom homeomorphism_def less_eq_real_def mem_box_real(2)) + then show "continuous_on T f'" "continuous_on T g'" + by (simp_all only: T) + show "f' ` T \ T" + unfolding f'_def + by clarsimp (metis \cbox w z \ S\ \S \ T\ subsetD hom homeomorphism_def imageI mem_box_real(2)) + show "g' ` T \ T" + unfolding g'_def + by clarsimp (metis \cbox w z \ S\ \S \ T\ subsetD hom homeomorphism_def imageI mem_box_real(2)) + show "\x. x \ T \ g' (f' x) = x" + unfolding f'_def g'_def + using homeomorphism_apply1 [OF hom] homeomorphism_image1 [OF hom] by fastforce + show "\y. y \ T \ f' (g' y) = y" + unfolding f'_def g'_def + using homeomorphism_apply2 [OF hom] homeomorphism_image2 [OF hom] by fastforce + qed + show "\x. x \ K \ f' x \ U" + using fin sub_wz \K \ cbox a b\ \cbox c d \ U\ by (force simp: f'_def) + show "{x. \ (f' x = x \ g' x = x)} \ S" + using \cbox w z \ S\ by (auto simp: f'_def g'_def) + show "bounded {x. \ (f' x = x \ g' x = x)}" + apply (rule bounded_subset [of "cbox w z"]) + using bounded_cbox apply blast + apply (auto simp: f'_def g'_def) + done + qed +qed + +proposition homeomorphism_grouping_points_exists: + fixes S :: "'a::euclidean_space set" + assumes "open U" "open S" "connected S" "U \ {}" "finite K" "K \ S" "U \ S" "S \ T" + obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \ g x = x))} \ S" + "bounded {x. (~ (f x = x \ g x = x))}" "\x. x \ K \ f x \ U" +proof (cases "2 \ DIM('a)") + case True + have TS: "T \ affine hull S" + using affine_hull_open assms by blast + have "infinite U" + using \open U\ \U \ {}\ finite_imp_not_open by blast + then obtain P where "P \ U" "finite P" "card K = card P" + using infinite_arbitrarily_large by metis + then obtain \ where \: "bij_betw \ K P" + using \finite K\ finite_same_card_bij by blast + obtain f g where "homeomorphism T T f g" "\i. i \ K \ f (id i) = \ i" "{x. \ (f x = x \ g x = x)} \ S" "bounded {x. \ (f x = x \ g x = x)}" + proof (rule homeomorphism_moving_points_exists [OF True \open S\ \connected S\ \S \ T\ \finite K\]) + show "\i. i \ K \ id i \ S \ \ i \ S" + using \P \ U\ \bij_betw \ K P\ \K \ S\ \U \ S\ bij_betwE by blast + show "pairwise (\i j. id i \ id j \ \ i \ \ j) K" + using \ by (auto simp: pairwise_def bij_betw_def inj_on_def) + qed (use affine_hull_open assms that in auto) + then show ?thesis + using \ \P \ U\ bij_betwE by (fastforce simp add: intro!: that) +next + case False + with DIM_positive have "DIM('a) = 1" + by (simp add: dual_order.antisym) + then obtain h::"'a \real" and j + where "linear h" "linear j" + and noh: "\x. norm(h x) = norm x" and noj: "\y. norm(j y) = norm y" + and hj: "\x. j(h x) = x" "\y. h(j y) = y" + and ranh: "surj h" + using isomorphisms_UNIV_UNIV + by (metis (mono_tags, hide_lams) DIM_real UNIV_eq_I range_eqI) + obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g" + and f: "\x. x \ h ` K \ f x \ h ` U" + and sub: "{x. \ (f x = x \ g x = x)} \ h ` S" + and bou: "bounded {x. \ (f x = x \ g x = x)}" + apply (rule homeomorphism_grouping_point_4 [of "h ` U" "h ` S" "h ` K" "h ` T"]) + by (simp_all add: assms image_mono \linear h\ open_surjective_linear_image connected_linear_image ranh) + have jf: "j (f (h x)) = x \ f (h x) = h x" for x + by (metis hj) + have jg: "j (g (h x)) = x \ g (h x) = h x" for x + by (metis hj) + have cont_hj: "continuous_on X h" "continuous_on Y j" for X Y + by (simp_all add: \linear h\ \linear j\ linear_linear linear_continuous_on) + show ?thesis + proof + show "homeomorphism T T (j \ f \ h) (j \ g \ h)" + proof + show "continuous_on T (j \ f \ h)" + apply (intro continuous_on_compose cont_hj) + using hom homeomorphism_def by blast + show "continuous_on T (j \ g \ h)" + apply (intro continuous_on_compose cont_hj) + using hom homeomorphism_def by blast + show "(j \ f \ h) ` T \ T" + by clarsimp (metis (mono_tags, hide_lams) hj(1) hom homeomorphism_def imageE imageI) + show "(j \ g \ h) ` T \ T" + by clarsimp (metis (mono_tags, hide_lams) hj(1) hom homeomorphism_def imageE imageI) + show "\x. x \ T \ (j \ g \ h) ((j \ f \ h) x) = x" + using hj hom homeomorphism_apply1 by fastforce + show "\y. y \ T \ (j \ f \ h) ((j \ g \ h) y) = y" + using hj hom homeomorphism_apply2 by fastforce + qed + show "{x. \ ((j \ f \ h) x = x \ (j \ g \ h) x = x)} \ S" + apply (clarsimp simp: jf jg hj) + using sub hj + apply (drule_tac c="h x" in subsetD, force) + by (metis imageE) + have "bounded (j ` {x. (~ (f x = x \ g x = x))})" + apply (rule bounded_linear_image [OF bou]) + using \linear j\ linear_conv_bounded_linear by auto + moreover + have *: "{x. ~((j \ f \ h) x = x \ (j \ g \ h) x = x)} = j ` {x. (~ (f x = x \ g x = x))}" + using hj apply (auto simp: jf jg image_iff, metis+) + done + ultimately show "bounded {x. \ ((j \ f \ h) x = x \ (j \ g \ h) x = x)}" + by metis + show "\x. x \ K \ (j \ f \ h) x \ U" + using f hj by fastforce + qed +qed + + +proposition homeomorphism_grouping_points_exists_gen: + fixes S :: "'a::euclidean_space set" + assumes opeU: "openin (subtopology euclidean S) U" + and opeS: "openin (subtopology euclidean (affine hull S)) S" + and "U \ {}" "finite K" "K \ S" and S: "S \ T" "T \ affine hull S" "connected S" + obtains f g where "homeomorphism T T f g" "{x. (~ (f x = x \ g x = x))} \ S" + "bounded {x. (~ (f x = x \ g x = x))}" "\x. x \ K \ f x \ U" +proof (cases "2 \ aff_dim S") + case True + have opeU': "openin (subtopology euclidean (affine hull S)) U" + using opeS opeU openin_trans by blast + obtain u where "u \ U" "u \ S" + using \U \ {}\ opeU openin_imp_subset by fastforce+ + have "infinite U" + apply (rule infinite_openin [OF opeU \u \ U\]) + apply (rule connected_imp_perfect_aff_dim [OF \connected S\ _ \u \ S\]) + using True apply simp + done + then obtain P where "P \ U" "finite P" "card K = card P" + using infinite_arbitrarily_large by metis + then obtain \ where \: "bij_betw \ K P" + using \finite K\ finite_same_card_bij by blast + have "\f g. homeomorphism T T f g \ (\i \ K. f(id i) = \ i) \ + {x. ~ (f x = x \ g x = x)} \ S \ bounded {x. ~ (f x = x \ g x = x)}" + proof (rule homeomorphism_moving_points_exists_gen [OF \finite K\ _ _ True opeS S]) + show "\i. i \ K \ id i \ S \ \ i \ S" + by (metis id_apply opeU openin_contains_cball subsetCE \P \ U\ \bij_betw \ K P\ \K \ S\ bij_betwE) + show "pairwise (\i j. id i \ id j \ \ i \ \ j) K" + using \ by (auto simp: pairwise_def bij_betw_def inj_on_def) + qed + then show ?thesis + using \ \P \ U\ bij_betwE by (fastforce simp add: intro!: that) +next + case False + with aff_dim_geq [of S] consider "aff_dim S = -1" | "aff_dim S = 0" | "aff_dim S = 1" by linarith + then show ?thesis + proof cases + assume "aff_dim S = -1" + then have "S = {}" + using aff_dim_empty by blast + then have "False" + using \U \ {}\ \K \ S\ openin_imp_subset [OF opeU] by blast + then show ?thesis .. + next + assume "aff_dim S = 0" + then obtain a where "S = {a}" + using aff_dim_eq_0 by blast + then have "K \ U" + using \U \ {}\ \K \ S\ openin_imp_subset [OF opeU] by blast + show ?thesis + apply (rule that [of id id]) + using \K \ U\ by (auto simp: continuous_on_id intro: homeomorphismI) + next + assume "aff_dim S = 1" + then have "affine hull S homeomorphic (UNIV :: real set)" + by (auto simp: homeomorphic_affine_sets) + then obtain h::"'a\real" and j where homhj: "homeomorphism (affine hull S) UNIV h j" + using homeomorphic_def by blast + then have h: "\x. x \ affine hull S \ j(h(x)) = x" and j: "\y. j y \ affine hull S \ h(j y) = y" + by (auto simp: homeomorphism_def) + have connh: "connected (h ` S)" + by (meson Topological_Spaces.connected_continuous_image \connected S\ homeomorphism_cont1 homeomorphism_of_subsets homhj hull_subset top_greatest) + have hUS: "h ` U \ h ` S" + by (meson homeomorphism_imp_open_map homeomorphism_of_subsets homhj hull_subset opeS opeU open_UNIV openin_open_eq) + have op: "openin (subtopology euclidean (affine hull S)) U \ open (h ` U)" for U + using homeomorphism_imp_open_map [OF homhj] by (simp add: open_openin) + have "open (h ` U)" "open (h ` S)" + by (auto intro: opeS opeU openin_trans op) + then obtain f g where hom: "homeomorphism (h ` T) (h ` T) f g" + and f: "\x. x \ h ` K \ f x \ h ` U" + and sub: "{x. \ (f x = x \ g x = x)} \ h ` S" + and bou: "bounded {x. \ (f x = x \ g x = x)}" + apply (rule homeomorphism_grouping_points_exists [of "h ` U" "h ` S" "h ` K" "h ` T"]) + using assms by (auto simp: connh hUS) + have jf: "\x. x \ affine hull S \ j (f (h x)) = x \ f (h x) = h x" + by (metis h j) + have jg: "\x. x \ affine hull S \ j (g (h x)) = x \ g (h x) = h x" + by (metis h j) + have cont_hj: "continuous_on T h" "continuous_on Y j" for Y + apply (rule continuous_on_subset [OF _ \T \ affine hull S\]) + using homeomorphism_def homhj apply blast + by (meson continuous_on_subset homeomorphism_def homhj top_greatest) + define f' where "f' \ \x. if x \ affine hull S then (j \ f \ h) x else x" + define g' where "g' \ \x. if x \ affine hull S then (j \ g \ h) x else x" + show ?thesis + proof + show "homeomorphism T T f' g'" + proof + have "continuous_on T (j \ f \ h)" + apply (intro continuous_on_compose cont_hj) + using hom homeomorphism_def by blast + then show "continuous_on T f'" + apply (rule continuous_on_eq) + using \T \ affine hull S\ f'_def by auto + have "continuous_on T (j \ g \ h)" + apply (intro continuous_on_compose cont_hj) + using hom homeomorphism_def by blast + then show "continuous_on T g'" + apply (rule continuous_on_eq) + using \T \ affine hull S\ g'_def by auto + show "f' ` T \ T" + proof (clarsimp simp: f'_def) + fix x assume "x \ T" + then have "f (h x) \ h ` T" + by (metis (no_types) hom homeomorphism_def image_subset_iff subset_refl) + then show "j (f (h x)) \ T" + using \T \ affine hull S\ h by auto + qed + show "g' ` T \ T" + proof (clarsimp simp: g'_def) + fix x assume "x \ T" + then have "g (h x) \ h ` T" + by (metis (no_types) hom homeomorphism_def image_subset_iff subset_refl) + then show "j (g (h x)) \ T" + using \T \ affine hull S\ h by auto + qed + show "\x. x \ T \ g' (f' x) = x" + using h j hom homeomorphism_apply1 by (fastforce simp add: f'_def g'_def) + show "\y. y \ T \ f' (g' y) = y" + using h j hom homeomorphism_apply2 by (fastforce simp add: f'_def g'_def) + qed + next + show "{x. \ (f' x = x \ g' x = x)} \ S" + apply (clarsimp simp: f'_def g'_def jf jg) + apply (rule imageE [OF subsetD [OF sub]], force) + by (metis h hull_inc) + next + have "bounded (j ` {x. (~ (f x = x \ g x = x))})" + apply (rule bounded_closure_image) + apply (rule compact_imp_bounded) + using bou by (auto simp: compact_continuous_image cont_hj) + moreover + have *: "{x \ affine hull S. j (f (h x)) \ x \ j (g (h x)) \ x} = j ` {x. (~ (f x = x \ g x = x))}" + using h j by (auto simp: image_iff; metis) + ultimately have "bounded {x \ affine hull S. j (f (h x)) \ x \ j (g (h x)) \ x}" + by metis + then show "bounded {x. \ (f' x = x \ g' x = x)}" + by (simp add: f'_def g'_def Collect_mono bounded_subset) + next + show "f' x \ U" if "x \ K" for x + proof - + have "U \ S" + using opeU openin_imp_subset by blast + then have "j (f (h x)) \ U" + using f h hull_subset that by fastforce + then show "f' x \ U" + using \K \ S\ S f'_def that by auto + qed + qed + qed +qed + +subsection\nullhomotopic mappings\ + +text\ A mapping out of a sphere is nullhomotopic iff it extends to the ball. +This even works out in the degenerate cases when the radius is \ 0, and +we also don't need to explicitly assume continuity since it's already implicit +in both sides of the equivalence.\ + +lemma nullhomotopic_from_lemma: + assumes contg: "continuous_on (cball a r - {a}) g" + and fa: "\e. 0 < e + \ \d. 0 < d \ (\x. x \ a \ norm(x - a) < d \ norm(g x - f a) < e)" + and r: "\x. x \ cball a r \ x \ a \ f x = g x" + shows "continuous_on (cball a r) f" +proof (clarsimp simp: continuous_on_eq_continuous_within Ball_def) + fix x + assume x: "dist a x \ r" + show "continuous (at x within cball a r) f" + proof (cases "x=a") + case True + then show ?thesis + by (metis continuous_within_eps_delta fa dist_norm dist_self r) + next + case False + show ?thesis + proof (rule continuous_transform_within [where f=g and d = "norm(x-a)"]) + have "\d>0. \x'\cball a r. + dist x' x < d \ dist (g x') (g x) < e" if "e>0" for e + proof - + obtain d where "d > 0" + and d: "\x'. \dist x' a \ r; x' \ a; dist x' x < d\ \ + dist (g x') (g x) < e" + using contg False x \e>0\ + unfolding continuous_on_iff by (fastforce simp add: dist_commute intro: that) + show ?thesis + using \d > 0\ \x \ a\ + by (rule_tac x="min d (norm(x - a))" in exI) + (auto simp: dist_commute dist_norm [symmetric] intro!: d) + qed + then show "continuous (at x within cball a r) g" + using contg False by (auto simp: continuous_within_eps_delta) + show "0 < norm (x - a)" + using False by force + show "x \ cball a r" + by (simp add: x) + show "\x'. \x' \ cball a r; dist x' x < norm (x - a)\ + \ g x' = f x'" + by (metis dist_commute dist_norm less_le r) + qed + qed +qed + +proposition nullhomotopic_from_sphere_extension: + fixes f :: "'M::euclidean_space \ 'a::real_normed_vector" + shows "(\c. homotopic_with (\x. True) (sphere a r) S f (\x. c)) \ + (\g. continuous_on (cball a r) g \ g ` (cball a r) \ S \ + (\x \ sphere a r. g x = f x))" + (is "?lhs = ?rhs") +proof (cases r "0::real" rule: linorder_cases) + case less + then show ?thesis by simp +next + case equal + with continuous_on_const show ?thesis + apply (auto simp: homotopic_with) + apply (rule_tac x="\x. h (0, a)" in exI) + apply (fastforce simp add:) + done +next + case greater + let ?P = "continuous_on {x. norm(x - a) = r} f \ f ` {x. norm(x - a) = r} \ S" + have ?P if ?lhs using that + proof + fix c + assume c: "homotopic_with (\x. True) (sphere a r) S f (\x. c)" + then have contf: "continuous_on (sphere a r) f" and fim: "f ` sphere a r \ S" + by (auto simp: homotopic_with_imp_subset1 homotopic_with_imp_continuous) + show ?P + using contf fim by (auto simp: sphere_def dist_norm norm_minus_commute) + qed + moreover have ?P if ?rhs using that + proof + fix g + assume g: "continuous_on (cball a r) g \ g ` cball a r \ S \ (\xa\sphere a r. g xa = f xa)" + then + show ?P + apply (safe elim!: continuous_on_eq [OF continuous_on_subset]) + apply (auto simp: dist_norm norm_minus_commute) + by (metis dist_norm image_subset_iff mem_sphere norm_minus_commute sphere_cball subsetCE) + qed + moreover have ?thesis if ?P + proof + assume ?lhs + then obtain c where "homotopic_with (\x. True) (sphere a r) S (\x. c) f" + using homotopic_with_sym by blast + then obtain h where conth: "continuous_on ({0..1::real} \ sphere a r) h" + and him: "h ` ({0..1} \ sphere a r) \ S" + and h: "\x. h(0, x) = c" "\x. h(1, x) = f x" + by (auto simp: homotopic_with_def) + obtain b1::'M where "b1 \ Basis" + using SOME_Basis by auto + have "c \ S" + apply (rule him [THEN subsetD]) + apply (rule_tac x = "(0, a + r *\<^sub>R b1)" in image_eqI) + using h greater \b1 \ Basis\ + apply (auto simp: dist_norm) + done + have uconth: "uniformly_continuous_on ({0..1::real} \ (sphere a r)) h" + by (force intro: compact_Times conth compact_uniformly_continuous) + let ?g = "\x. h (norm (x - a)/r, + a + (if x = a then r *\<^sub>R b1 else (r / norm(x - a)) *\<^sub>R (x - a)))" + let ?g' = "\x. h (norm (x - a)/r, a + (r / norm(x - a)) *\<^sub>R (x - a))" + show ?rhs + proof (intro exI conjI) + have "continuous_on (cball a r - {a}) ?g'" + apply (rule continuous_on_compose2 [OF conth]) + apply (intro continuous_intros) + using greater apply (auto simp: dist_norm norm_minus_commute) + done + then show "continuous_on (cball a r) ?g" + proof (rule nullhomotopic_from_lemma) + show "\d>0. \x. x \ a \ norm (x - a) < d \ norm (?g' x - ?g a) < e" if "0 < e" for e + proof - + obtain d where "0 < d" + and d: "\x x'. \x \ {0..1} \ sphere a r; x' \ {0..1} \ sphere a r; dist x' x < d\ + \ dist (h x') (h x) < e" + using uniformly_continuous_onE [OF uconth \0 < e\] by auto + have *: "norm (h (norm (x - a) / r, + a + (r / norm (x - a)) *\<^sub>R (x - a)) - h (0, a + r *\<^sub>R b1)) < e" + if "x \ a" "norm (x - a) < r" "norm (x - a) < d * r" for x + proof - + have "norm (h (norm (x - a) / r, a + (r / norm (x - a)) *\<^sub>R (x - a)) - h (0, a + r *\<^sub>R b1)) = + norm (h (norm (x - a) / r, a + (r / norm (x - a)) *\<^sub>R (x - a)) - h (0, a + (r / norm (x - a)) *\<^sub>R (x - a)))" + by (simp add: h) + also have "... < e" + apply (rule d [unfolded dist_norm]) + using greater \0 < d\ \b1 \ Basis\ that + by (auto simp: dist_norm divide_simps) + finally show ?thesis . + qed + show ?thesis + apply (rule_tac x = "min r (d * r)" in exI) + using greater \0 < d\ by (auto simp: *) + qed + show "\x. x \ cball a r \ x \ a \ ?g x = ?g' x" + by auto + qed + next + show "?g ` cball a r \ S" + using greater him \c \ S\ + by (force simp: h dist_norm norm_minus_commute) + next + show "\x\sphere a r. ?g x = f x" + using greater by (auto simp: h dist_norm norm_minus_commute) + qed + next + assume ?rhs + then obtain g where contg: "continuous_on (cball a r) g" + and gim: "g ` cball a r \ S" + and gf: "\x \ sphere a r. g x = f x" + by auto + let ?h = "\y. g (a + (fst y) *\<^sub>R (snd y - a))" + have "continuous_on ({0..1} \ sphere a r) ?h" + apply (rule continuous_on_compose2 [OF contg]) + apply (intro continuous_intros) + apply (auto simp: dist_norm norm_minus_commute mult_left_le_one_le) + done + moreover + have "?h ` ({0..1} \ sphere a r) \ S" + by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gim [THEN subsetD]) + moreover + have "\x\sphere a r. ?h (0, x) = g a" "\x\sphere a r. ?h (1, x) = f x" + by (auto simp: dist_norm norm_minus_commute mult_left_le_one_le gf) + ultimately + show ?lhs + apply (subst homotopic_with_sym) + apply (rule_tac x="g a" in exI) + apply (auto simp: homotopic_with) + done + qed + ultimately + show ?thesis by meson +qed + end diff -r 957ba35d1338 -r 2aa42596edc3 src/HOL/Analysis/Polytope.thy --- a/src/HOL/Analysis/Polytope.thy Fri Sep 30 10:00:49 2016 +0200 +++ b/src/HOL/Analysis/Polytope.thy Fri Sep 30 14:05:51 2016 +0100 @@ -2586,4 +2586,196 @@ using interior_subset by (force simp: frontier_of_triangle [OF assms, symmetric] frontier_def Diff_Diff_Int) +subsection\Subdividing a cell complex\ + +lemma subdivide_interval: + fixes x::real + assumes "a < \x - y\" "0 < a" + obtains n where "n \ \" "x < n * a \ n * a < y \ y < n * a \ n * a < x" +proof - + consider "a + x < y" | "a + y < x" + using assms by linarith + then show ?thesis + proof cases + case 1 + let ?n = "of_int (floor (x/a)) + 1" + have x: "x < ?n * a" + by (meson \0 < a\ divide_less_eq floor_unique_iff) + have "?n * a \ a + x" + apply (simp add: algebra_simps) + by (metis \0 < a\ floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right) + also have "... < y" + by (rule 1) + finally have "?n * a < y" . + with x show ?thesis + using Ints_1 Ints_add Ints_of_int that by blast + next + case 2 + let ?n = "of_int (floor (y/a)) + 1" + have y: "y < ?n * a" + by (meson \0 < a\ divide_less_eq floor_unique_iff) + have "?n * a \ a + y" + apply (simp add: algebra_simps) + by (metis \0 < a\ floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right) + also have "... < x" + by (rule 2) + finally have "?n * a < x" . + then show ?thesis + using Ints_1 Ints_add Ints_of_int that y by blast + qed +qed + + +lemma cell_subdivision_lemma: + assumes "finite \" + and "\X. X \ \ \ polytope X" + and "\X. X \ \ \ aff_dim X \ d" + and "\X Y. \X \ \; Y \ \\ \ (X \ Y) face_of X \ (X \ Y) face_of Y" + and "finite I" + shows "\\'. \\' = \\ \ + finite \' \ + (\X \ \'. polytope X) \ + (\X \ \'. aff_dim X \ d) \ + (\X \ \'. \Y \ \'. X \ Y face_of X \ X \ Y face_of Y) \ + (\X \ \'. \x \ X. \y \ X. \a b. + (a,b) \ I \ a \ x \ b \ a \ y \ b \ + a \ x \ b \ a \ y \ b)" + using \finite I\ +proof induction + case empty + then show ?case + by (rule_tac x="\" in exI) (simp add: assms) +next + case (insert ab I) + then obtain \' where eq: "\\' = \\" and "finite \'" + and poly: "\X. X \ \' \ polytope X" + and aff: "\X. X \ \' \ aff_dim X \ d" + and face: "\X Y. \X \ \'; Y \ \'\ \ X \ Y face_of X \ X \ Y face_of Y" + and I: "\X x y a b. \X \ \'; x \ X; y \ X; (a,b) \ I\ \ + a \ x \ b \ a \ y \ b \ a \ x \ b \ a \ y \ b" + by (auto simp: that) + obtain a b where "ab = (a,b)" + by fastforce + let ?\ = "(\X. X \ {x. a \ x \ b}) ` \' \ (\X. X \ {x. a \ x \ b}) ` \'" + have eqInt: "(S \ Collect P) \ (T \ Collect Q) = (S \ T) \ (Collect P \ Collect Q)" for S T::"'a set" and P Q + by blast + show ?case + proof (intro conjI exI) + show "\?\ = \\" + by (force simp: eq [symmetric]) + show "finite ?\" + using \finite \'\ by force + show "\X \ ?\. polytope X" + by (force simp: poly polytope_Int_polyhedron polyhedron_halfspace_le polyhedron_halfspace_ge) + show "\X \ ?\. aff_dim X \ d" + by (auto; metis order_trans aff aff_dim_subset inf_le1) + show "\X \ ?\. \x \ X. \y \ X. \a b. + (a,b) \ insert ab I \ a \ x \ b \ a \ y \ b \ + a \ x \ b \ a \ y \ b" + using \ab = (a, b)\ I by fastforce + show "\X \ ?\. \Y \ ?\. X \ Y face_of X \ X \ Y face_of Y" + by (auto simp: eqInt halfspace_Int_eq face_of_Int_Int face face_of_halfspace_le face_of_halfspace_ge) + qed +qed + + +proposition cell_complex_subdivision_exists: + fixes \ :: "'a::euclidean_space set set" + assumes "0 < e" "finite \" + and poly: "\X. X \ \ \ polytope X" + and aff: "\X. X \ \ \ aff_dim X \ d" + and face: "\X Y. \X \ \; Y \ \\ \ X \ Y face_of X \ X \ Y face_of Y" + obtains "\'" where "finite \'" "\\' = \\" "\X. X \ \' \ diameter X < e" + "\X. X \ \' \ polytope X" "\X. X \ \' \ aff_dim X \ d" + "\X Y. \X \ \'; Y \ \'\ \ X \ Y face_of X \ X \ Y face_of Y" +proof - + have "bounded(\\)" + by (simp add: \finite \\ poly bounded_Union polytope_imp_bounded) + then obtain B where "B > 0" and B: "\x. x \ \\ \ norm x < B" + by (meson bounded_pos_less) + define C where "C \ {z \ \. \z * e / 2 / real DIM('a)\ \ B}" + define I where "I \ \i \ Basis. \j \ C. { (i::'a, j * e / 2 / DIM('a)) }" + have "finite C" + using finite_int_segment [of "-B / (e / 2 / DIM('a))" "B / (e / 2 / DIM('a))"] + apply (simp add: C_def) + apply (erule rev_finite_subset) + using \0 < e\ + apply (auto simp: divide_simps) + done + then have "finite I" + by (simp add: I_def) + obtain \' where eq: "\\' = \\" and "finite \'" + and poly: "\X. X \ \' \ polytope X" + and aff: "\X. X \ \' \ aff_dim X \ d" + and face: "\X Y. \X \ \'; Y \ \'\ \ X \ Y face_of X \ X \ Y face_of Y" + and I: "\X x y a b. \X \ \'; x \ X; y \ X; (a,b) \ I\ \ + a \ x \ b \ a \ y \ b \ a \ x \ b \ a \ y \ b" + apply (rule exE [OF cell_subdivision_lemma]) + apply (rule assms \finite I\ | assumption)+ + apply (auto intro: that) + done + show ?thesis + proof (rule_tac \'="\'" in that) + show "diameter X < e" if "X \ \'" for X + proof - + have "diameter X \ e/2" + proof (rule diameter_le) + show "norm (x - y) \ e / 2" if "x \ X" "y \ X" for x y + proof - + have "norm x < B" "norm y < B" + using B \X \ \'\ eq that by fastforce+ + have "norm (x - y) \ (\b\Basis. \(x-y) \ b\)" + by (rule norm_le_l1) + also have "... \ of_nat (DIM('a)) * (e / 2 / DIM('a))" + proof (rule setsum_bounded_above) + fix i::'a + assume "i \ Basis" + then have I': "\z b. \z \ C; b = z * e / (2 * real DIM('a))\ \ i \ x \ b \ i \ y \ b \ i \ x \ b \ i \ y \ b" + using I \X \ \'\ that + by (fastforce simp: I_def) + show "\(x - y) \ i\ \ e / 2 / real DIM('a)" + proof (rule ccontr) + assume "\ \(x - y) \ i\ \ e / 2 / real DIM('a)" + then have xyi: "\i \ x - i \ y\ > e / 2 / real DIM('a)" + by (simp add: inner_commute inner_diff_right) + obtain n where "n \ \" and n: "i \ x < n * (e / 2 / real DIM('a)) \ n * (e / 2 / real DIM('a)) < i \ y \ i \ y < n * (e / 2 / real DIM('a)) \ n * (e / 2 / real DIM('a)) < i \ x" + using subdivide_interval [OF xyi] DIM_positive \0 < e\ + by (auto simp: zero_less_divide_iff) + have "\i \ x\ < B" + by (metis \i \ Basis\ \norm x < B\ inner_commute norm_bound_Basis_lt) + have "\i \ y\ < B" + by (metis \i \ Basis\ \norm y < B\ inner_commute norm_bound_Basis_lt) + have *: "\n * e\ \ B * (2 * real DIM('a))" + if "\ix\ < B" "\iy\ < B" + and ix: "ix * (2 * real DIM('a)) < n * e" + and iy: "n * e < iy * (2 * real DIM('a))" for ix iy + proof (rule abs_leI) + have "iy * (2 * real DIM('a)) \ B * (2 * real DIM('a))" + by (rule mult_right_mono) (use \\iy\ < B\ in linarith)+ + then show "n * e \ B * (2 * real DIM('a))" + using iy by linarith + next + have "- ix * (2 * real DIM('a)) \ B * (2 * real DIM('a))" + by (rule mult_right_mono) (use \\ix\ < B\ in linarith)+ + then show "- (n * e) \ B * (2 * real DIM('a))" + using ix by linarith + qed + have "n \ C" + using \n \ \\ n by (auto simp: C_def divide_simps intro: * \\i \ x\ < B\ \\i \ y\ < B\) + show False + using I' [OF \n \ C\ refl] n by auto + qed + qed + also have "... = e / 2" + by simp + finally show ?thesis . + qed + qed (use \0 < e\ in force) + also have "... < e" + by (simp add: \0 < e\) + finally show ?thesis . + qed + qed (auto simp: eq poly aff face \finite \'\) +qed + end diff -r 957ba35d1338 -r 2aa42596edc3 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Sep 30 10:00:49 2016 +0200 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Sep 30 14:05:51 2016 +0100 @@ -18,6 +18,11 @@ (* FIXME: move elsewhere *) +lemma halfspace_Int_eq: + "{x. a \ x \ b} \ {x. b \ a \ x} = {x. a \ x = b}" + "{x. b \ a \ x} \ {x. a \ x \ b} = {x. a \ x = b}" + by auto + definition (in monoid_add) support_on :: "'b set \ ('b \ 'a) \ 'b set" where "support_on s f = {x\s. f x \ 0}" @@ -8603,27 +8608,19 @@ (\f g. (\x\s. f(x) \ t \ (g(f(x)) = x)) \ (\y\t. g(y) \ s \ (f(g(y)) = y)) \ continuous_on s f \ continuous_on t g)" - unfolding homeomorphic_def homeomorphism_def - apply auto - apply (rule_tac x=f in exI) - apply (rule_tac x=g in exI) - apply auto - apply (rule_tac x=f in exI) - apply (rule_tac x=g in exI) - apply auto - unfolding image_iff - apply (erule_tac x="g x" in ballE) - apply (erule_tac x="x" in ballE) - apply auto - apply (rule_tac x="g x" in bexI) - apply auto - apply (erule_tac x="f x" in ballE) - apply (erule_tac x="x" in ballE) - apply auto - apply (rule_tac x="f x" in bexI) - apply auto - done - + (is "?lhs = ?rhs") +proof + assume ?lhs + then show ?rhs + by (fastforce simp: homeomorphic_def homeomorphism_def) +next + assume ?rhs + then show ?lhs + apply clarify + unfolding homeomorphic_def homeomorphism_def + by (metis equalityI image_subset_iff subsetI) + qed + lemma homeomorphicI [intro?]: "\f ` S = T; g ` T = S; continuous_on S f; continuous_on T g; @@ -8635,7 +8632,7 @@ "\homeomorphism S T f g; S' \ S; T'' \ T; f ` S' = T'\ \ homeomorphism S' T' f g" apply (auto simp: homeomorphism_def elim!: continuous_on_subset) -by (metis contra_subsetD imageI) +by (metis subsetD imageI) lemma homeomorphism_apply1: "\homeomorphism S T f g; x \ S\ \ g(f x) = x" by (simp add: homeomorphism_def) @@ -8655,6 +8652,39 @@ lemma homeomorphism_cont2: "homeomorphism S T f g \ continuous_on T g" by (simp add: homeomorphism_def) +lemma continuous_on_no_limpt: + "(\x. \ x islimpt S) \ continuous_on S f" + unfolding continuous_on_def + by (metis UNIV_I empty_iff eventually_at_topological islimptE open_UNIV tendsto_def trivial_limit_within) + +lemma continuous_on_finite: + fixes S :: "'a::t1_space set" + shows "finite S \ continuous_on S f" +by (metis continuous_on_no_limpt islimpt_finite) + +lemma homeomorphic_finite: + fixes S :: "'a::t1_space set" and T :: "'b::t1_space set" + assumes "finite T" + shows "S homeomorphic T \ finite S \ finite T \ card S = card T" (is "?lhs = ?rhs") +proof + assume "S homeomorphic T" + with assms show ?rhs + apply (auto simp: homeomorphic_def homeomorphism_def) + apply (metis finite_imageI) + by (metis card_image_le finite_imageI le_antisym) +next + assume R: ?rhs + with finite_same_card_bij obtain h where "bij_betw h S T" + by (auto simp: ) + with R show ?lhs + apply (auto simp: homeomorphic_def homeomorphism_def continuous_on_finite) + apply (rule_tac x="h" in exI) + apply (rule_tac x="inv_into S h" in exI) + apply (auto simp: bij_betw_inv_into_left bij_betw_inv_into_right bij_betw_imp_surj_on inv_into_into bij_betwE) + apply (metis bij_betw_def bij_betw_inv_into) + done +qed + text \Relatively weak hypotheses if a set is compact.\ lemma homeomorphism_compact: diff -r 957ba35d1338 -r 2aa42596edc3 src/HOL/Filter.thy --- a/src/HOL/Filter.thy Fri Sep 30 10:00:49 2016 +0200 +++ b/src/HOL/Filter.thy Fri Sep 30 14:05:51 2016 +0100 @@ -685,11 +685,11 @@ "eventually (\x. x < (c::_::unbounded_dense_linorder)) at_bot" unfolding eventually_at_bot_dense by auto -lemma trivial_limit_at_bot_linorder: "\ trivial_limit (at_bot ::('a::linorder) filter)" +lemma trivial_limit_at_bot_linorder [simp]: "\ trivial_limit (at_bot ::('a::linorder) filter)" unfolding trivial_limit_def by (metis eventually_at_bot_linorder order_refl) -lemma trivial_limit_at_top_linorder: "\ trivial_limit (at_top ::('a::linorder) filter)" +lemma trivial_limit_at_top_linorder [simp]: "\ trivial_limit (at_top ::('a::linorder) filter)" unfolding trivial_limit_def by (metis eventually_at_top_linorder order_refl) @@ -720,10 +720,10 @@ shows "eventually P sequentially" using assms by (auto simp: eventually_sequentially) -lemma eventually_sequentially_Suc: "eventually (\i. P (Suc i)) sequentially \ eventually P sequentially" +lemma eventually_sequentially_Suc [simp]: "eventually (\i. P (Suc i)) sequentially \ eventually P sequentially" unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq) -lemma eventually_sequentially_seg: "eventually (\n. P (n + k)) sequentially \ eventually P sequentially" +lemma eventually_sequentially_seg [simp]: "eventually (\n. P (n + k)) sequentially \ eventually P sequentially" using eventually_sequentially_Suc[of "\n. P (n + k)" for k] by (induction k) auto @@ -1103,7 +1103,7 @@ unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp lemma filterlim_Suc: "filterlim Suc sequentially sequentially" - by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq) + by (simp add: filterlim_iff eventually_sequentially) lemma filterlim_If: "LIM x inf F (principal {x. P x}). f x :> G \ diff -r 957ba35d1338 -r 2aa42596edc3 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Fri Sep 30 10:00:49 2016 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Fri Sep 30 14:05:51 2016 +0100 @@ -375,6 +375,21 @@ by (simp add: comp_def) qed +lemma fraction_scaleR_times [simp]: + fixes a :: "'a::real_algebra_1" + shows "(numeral u / numeral v) *\<^sub>R (numeral w * a) = (numeral u * numeral w / numeral v) *\<^sub>R a" +by (metis (no_types, lifting) of_real_numeral scaleR_conv_of_real scaleR_scaleR times_divide_eq_left) + +lemma inverse_scaleR_times [simp]: + fixes a :: "'a::real_algebra_1" + shows "(1 / numeral v) *\<^sub>R (numeral w * a) = (numeral w / numeral v) *\<^sub>R a" +by (metis divide_inverse_commute inverse_eq_divide of_real_numeral scaleR_conv_of_real scaleR_scaleR) + +lemma scaleR_times [simp]: + fixes a :: "'a::real_algebra_1" + shows "(numeral u) *\<^sub>R (numeral w * a) = (numeral u * numeral w) *\<^sub>R a" +by (simp add: scaleR_conv_of_real) + instance real_field < field_char_0 .. diff -r 957ba35d1338 -r 2aa42596edc3 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Fri Sep 30 10:00:49 2016 +0200 +++ b/src/HOL/Set_Interval.thy Fri Sep 30 14:05:51 2016 +0100 @@ -551,6 +551,18 @@ using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b] by (auto dest: finite_subset) +lemma infinite_Ioo_iff [simp]: "infinite {a<.. a < b" + using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioo) + +lemma infinite_Icc_iff [simp]: "infinite {a .. b} \ a < b" + using not_less_iff_gr_or_eq by (fastforce simp: infinite_Icc) + +lemma infinite_Ico_iff [simp]: "infinite {a.. a < b" + using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ico) + +lemma infinite_Ioc_iff [simp]: "infinite {a<..b} \ a < b" + using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioc) + end lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}"