(* Title: HOL/Analysis/Convex_Euclidean_Space.thy Author: L C Paulson, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Bogdan Grechuk, University of Edinburgh Author: Armin Heller, TU Muenchen Author: Johannes Hoelzl, TU Muenchen *) section \Convex Sets and Functions on (Normed) Euclidean Spaces\ theory Convex_Euclidean_Space imports Convex Topology_Euclidean_Space begin subsection\<^marker>\tag unimportant\ \Topological Properties of Convex Sets and Functions\ lemma convex_supp_sum: assumes "convex S" and 1: "supp_sum u I = 1" and "\i. i \ I \ 0 \ u i \ (u i = 0 \ f i \ S)" shows "supp_sum (\i. u i *\<^sub>R f i) I \ S" proof - have fin: "finite {i \ I. u i \ 0}" using 1 sum.infinite by (force simp: supp_sum_def support_on_def) then have eq: "supp_sum (\i. u i *\<^sub>R f i) I = sum (\i. u i *\<^sub>R f i) {i \ I. u i \ 0}" by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def) show ?thesis apply (simp add: eq) apply (rule convex_sum [OF fin \convex S\]) using 1 assms apply (auto simp: supp_sum_def support_on_def) done qed lemma closure_bounded_linear_image_subset: assumes f: "bounded_linear f" shows "f ` closure S \ closure (f ` S)" using linear_continuous_on [OF f] closed_closure closure_subset by (rule image_closure_subset) lemma closure_linear_image_subset: fixes f :: "'m::euclidean_space \ 'n::real_normed_vector" assumes "linear f" shows "f ` (closure S) \ closure (f ` S)" using assms unfolding linear_conv_bounded_linear by (rule closure_bounded_linear_image_subset) lemma closed_injective_linear_image: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes S: "closed S" and f: "linear f" "inj f" shows "closed (f ` S)" proof - obtain g where g: "linear g" "g \ f = id" using linear_injective_left_inverse [OF f] by blast then have confg: "continuous_on (range f) g" using linear_continuous_on linear_conv_bounded_linear by blast have [simp]: "g ` f ` S = S" using g by (simp add: image_comp) have cgf: "closed (g ` f ` S)" by (simp add: \g \ f = id\ S image_comp) have [simp]: "(range f \ g -` S) = f ` S" using g unfolding o_def id_def image_def by auto metis+ show ?thesis proof (rule closedin_closed_trans [of "range f"]) show "closedin (top_of_set (range f)) (f ` S)" using continuous_closedin_preimage [OF confg cgf] by simp show "closed (range f)" apply (rule closed_injective_image_subspace) using f apply (auto simp: linear_linear linear_injective_0) done qed qed lemma closed_injective_linear_image_eq: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" assumes f: "linear f" "inj f" shows "(closed(image f s) \ closed s)" by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff) lemma closure_injective_linear_image: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" shows "\linear f; inj f\ \ f ` (closure S) = closure (f ` S)" apply (rule subset_antisym) apply (simp add: closure_linear_image_subset) by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono) lemma closure_bounded_linear_image: fixes f :: "'a::euclidean_space \ 'b::euclidean_space" shows "\linear f; bounded S\ \ f ` (closure S) = closure (f ` S)" apply (rule subset_antisym, simp add: closure_linear_image_subset) apply (rule closure_minimal, simp add: closure_subset image_mono) by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear) lemma closure_scaleR: fixes S :: "'a::real_normed_vector set" shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)" proof show "((*\<^sub>R) c) ` (closure S) \ closure (((*\<^sub>R) c) ` S)" using bounded_linear_scaleR_right by (rule closure_bounded_linear_image_subset) show "closure (((*\<^sub>R) c) ` S) \ ((*\<^sub>R) c) ` (closure S)" by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure) qed lemma sphere_eq_empty [simp]: fixes a :: "'a::{real_normed_vector, perfect_space}" shows "sphere a r = {} \ r < 0" by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist) lemma cone_closure: fixes S :: "'a::real_normed_vector set" assumes "cone S" shows "cone (closure S)" proof (cases "S = {}") case True then show ?thesis by auto next case False then have "0 \ S \ (\c. c > 0 \ (*\<^sub>R) c ` S = S)" using cone_iff[of S] assms by auto then have "0 \ closure S \ (\c. c > 0 \ (*\<^sub>R) c ` closure S = closure S)" using closure_subset by (auto simp: closure_scaleR) then show ?thesis using False cone_iff[of "closure S"] by auto qed corollary component_complement_connected: fixes S :: "'a::real_normed_vector set" assumes "connected S" "C \ components (-S)" shows "connected(-C)" using component_diff_connected [of S UNIV] assms by (auto simp: Compl_eq_Diff_UNIV) proposition clopen: fixes S :: "'a :: real_normed_vector set" shows "closed S \ open S \ S = {} \ S = UNIV" by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format]) corollary compact_open: fixes S :: "'a :: euclidean_space set" shows "compact S \ open S \ S = {}" by (auto simp: compact_eq_bounded_closed clopen) corollary finite_imp_not_open: fixes S :: "'a::{real_normed_vector, perfect_space} set" shows "\finite S; open S\ \ S={}" using clopen [of S] finite_imp_closed not_bounded_UNIV by blast corollary empty_interior_finite: fixes S :: "'a::{real_normed_vector, perfect_space} set" shows "finite S \ interior S = {}" by (metis interior_subset finite_subset open_interior [of S] finite_imp_not_open) text \Balls, being convex, are connected.\ lemma convex_local_global_minimum: fixes s :: "'a::real_normed_vector set" assumes "e > 0" and "convex_on s f" and "ball x e \ s" and "\y\ball x e. f x \ f y" shows "\y\s. f x \ f y" proof (rule ccontr) have "x \ s" using assms(1,3) by auto assume "\ ?thesis" then obtain y where "y\s" and y: "f x > f y" by auto then have xy: "0 < dist x y" by auto then obtain u where "0 < u" "u \ 1" and u: "u < e / dist x y" using field_lbound_gt_zero[of 1 "e / dist x y"] xy \e>0\ by auto then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \ (1-u) * f x + u * f y" using \x\s\ \y\s\ using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto moreover have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" by (simp add: algebra_simps) have "(1 - u) *\<^sub>R x + u *\<^sub>R y \ ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF \0] unfolding dist_norm[symmetric] using u unfolding pos_less_divide_eq[OF xy] by auto then have "f x \ f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto ultimately show False using mult_strict_left_mono[OF y \u>0\] unfolding left_diff_distrib by auto qed lemma convex_ball [iff]: fixes x :: "'a::real_normed_vector" shows "convex (ball x e)" proof (auto simp: convex_def) fix y z assume yz: "dist x y < e" "dist x z < e" fix u v :: real assume uv: "0 \ u" "0 \ v" "u + v = 1" have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" using uv yz using convex_on_dist [of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using convex_bound_lt[OF yz uv] by auto qed lemma convex_cball [iff]: fixes x :: "'a::real_normed_vector" shows "convex (cball x e)" proof - { fix y z assume yz: "dist x y \ e" "dist x z \ e" fix u v :: real assume uv: "0 \ u" "0 \ v" "u + v = 1" have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" using uv yz using convex_on_dist [of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ e" using convex_bound_le[OF yz uv] by auto } then show ?thesis by (auto simp: convex_def Ball_def) qed lemma connected_ball [iff]: fixes x :: "'a::real_normed_vector" shows "connected (ball x e)" using convex_connected convex_ball by auto lemma connected_cball [iff]: fixes x :: "'a::real_normed_vector" shows "connected (cball x e)" using convex_connected convex_cball by auto lemma bounded_convex_hull: fixes s :: "'a::real_normed_vector set" assumes "bounded s" shows "bounded (convex hull s)" proof - from assms obtain B where B: "\x\s. norm x \ B" unfolding bounded_iff by auto show ?thesis apply (rule bounded_subset[OF bounded_cball, of _ 0 B]) unfolding subset_hull[of convex, OF convex_cball] unfolding subset_eq mem_cball dist_norm using B apply auto done qed lemma finite_imp_bounded_convex_hull: fixes s :: "'a::real_normed_vector set" shows "finite s \ bounded (convex hull s)" using bounded_convex_hull finite_imp_bounded by auto lemma aff_dim_cball: fixes a :: "'n::euclidean_space" assumes "e > 0" shows "aff_dim (cball a e) = int (DIM('n))" proof - have "(\x. a + x) ` (cball 0 e) \ cball a e" unfolding cball_def dist_norm by auto then have "aff_dim (cball (0 :: 'n::euclidean_space) e) \ aff_dim (cball a e)" using aff_dim_translation_eq[of a "cball 0 e"] aff_dim_subset[of "(+) a ` cball 0 e" "cball a e"] by auto moreover have "aff_dim (cball (0 :: 'n::euclidean_space) e) = int (DIM('n))" using hull_inc[of "(0 :: 'n::euclidean_space)" "cball 0 e"] centre_in_cball[of "(0 :: 'n::euclidean_space)"] assms by (simp add: dim_cball[of e] aff_dim_zero[of "cball 0 e"]) ultimately show ?thesis using aff_dim_le_DIM[of "cball a e"] by auto qed lemma aff_dim_open: fixes S :: "'n::euclidean_space set" assumes "open S" and "S \ {}" shows "aff_dim S = int (DIM('n))" proof - obtain x where "x \ S" using assms by auto then obtain e where e: "e > 0" "cball x e \ S" using open_contains_cball[of S] assms by auto then have "aff_dim (cball x e) \ aff_dim S" using aff_dim_subset by auto with e show ?thesis using aff_dim_cball[of e x] aff_dim_le_DIM[of S] by auto qed lemma low_dim_interior: fixes S :: "'n::euclidean_space set" assumes "\ aff_dim S = int (DIM('n))" shows "interior S = {}" proof - have "aff_dim(interior S) \ aff_dim S" using interior_subset aff_dim_subset[of "interior S" S] by auto then show ?thesis using aff_dim_open[of "interior S"] aff_dim_le_DIM[of S] assms by auto qed corollary empty_interior_lowdim: fixes S :: "'n::euclidean_space set" shows "dim S < DIM ('n) \ interior S = {}" by (metis low_dim_interior affine_hull_UNIV dim_affine_hull less_not_refl dim_UNIV) corollary aff_dim_nonempty_interior: fixes S :: "'a::euclidean_space set" shows "interior S \ {} \ aff_dim S = DIM('a)" by (metis low_dim_interior) subsection \Relative interior of a set\ definition\<^marker>\tag important\ "rel_interior S = {x. \T. openin (top_of_set (affine hull S)) T \ x \ T \ T \ S}" lemma rel_interior_mono: "\S \ T; affine hull S = affine hull T\ \ (rel_interior S) \ (rel_interior T)" by (auto simp: rel_interior_def) lemma rel_interior_maximal: "\T \ S; openin(top_of_set (affine hull S)) T\ \ T \ (rel_interior S)" by (auto simp: rel_interior_def) lemma rel_interior: "rel_interior S = {x \ S. \T. open T \ x \ T \ T \ affine hull S \ S}" unfolding rel_interior_def[of S] openin_open[of "affine hull S"] apply auto proof - fix x T assume *: "x \ S" "open T" "x \ T" "T \ affine hull S \ S" then have **: "x \ T \ affine hull S" using hull_inc by auto show "\Tb. (\Ta. open Ta \ Tb = affine hull S \ Ta) \ x \ Tb \ Tb \ S" apply (rule_tac x = "T \ (affine hull S)" in exI) using * ** apply auto done qed lemma mem_rel_interior: "x \ rel_interior S \ (\T. open T \ x \ T \ S \ T \ affine hull S \ S)" by (auto simp: rel_interior) lemma mem_rel_interior_ball: "x \ rel_interior S \ x \ S \ (\e. e > 0 \ ball x e \ affine hull S \ S)" apply (simp add: rel_interior, safe) apply (force simp: open_contains_ball) apply (rule_tac x = "ball x e" in exI, simp) done lemma rel_interior_ball: "rel_interior S = {x \ S. \e. e > 0 \ ball x e \ affine hull S \ S}" using mem_rel_interior_ball [of _ S] by auto lemma mem_rel_interior_cball: "x \ rel_interior S \ x \ S \ (\e. e > 0 \ cball x e \ affine hull S \ S)" apply (simp add: rel_interior, safe) apply (force simp: open_contains_cball) apply (rule_tac x = "ball x e" in exI) apply (simp add: subset_trans [OF ball_subset_cball], auto) done lemma rel_interior_cball: "rel_interior S = {x \ S. \e. e > 0 \ cball x e \ affine hull S \ S}" using mem_rel_interior_cball [of _ S] by auto lemma rel_interior_empty [simp]: "rel_interior {} = {}" by (auto simp: rel_interior_def) lemma affine_hull_sing [simp]: "affine hull {a :: 'n::euclidean_space} = {a}" by (metis affine_hull_eq affine_sing) lemma rel_interior_sing [simp]: fixes a :: "'n::euclidean_space" shows "rel_interior {a} = {a}" apply (auto simp: rel_interior_ball) apply (rule_tac x=1 in exI, force) done lemma subset_rel_interior: fixes S T :: "'n::euclidean_space set" assumes "S \ T" and "affine hull S = affine hull T" shows "rel_interior S \ rel_interior T" using assms by (auto simp: rel_interior_def) lemma rel_interior_subset: "rel_interior S \ S" by (auto simp: rel_interior_def) lemma rel_interior_subset_closure: "rel_interior S \ closure S" using rel_interior_subset by (auto simp: closure_def) lemma interior_subset_rel_interior: "interior S \ rel_interior S" by (auto simp: rel_interior interior_def) lemma interior_rel_interior: fixes S :: "'n::euclidean_space set" assumes "aff_dim S = int(DIM('n))" shows "rel_interior S = interior S" proof - have "affine hull S = UNIV" using assms affine_hull_UNIV[of S] by auto then show ?thesis unfolding rel_interior interior_def by auto qed lemma rel_interior_interior: fixes S :: "'n::euclidean_space set" assumes "affine hull S = UNIV" shows "rel_interior S = interior S" using assms unfolding rel_interior interior_def by auto lemma rel_interior_open: fixes S :: "'n::euclidean_space set" assumes "open S" shows "rel_interior S = S" by (metis assms interior_eq interior_subset_rel_interior rel_interior_subset set_eq_subset) lemma interior_ball [simp]: "interior (ball x e) = ball x e" by (simp add: interior_open) lemma interior_rel_interior_gen: fixes S :: "'n::euclidean_space set" shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})" by (metis interior_rel_interior low_dim_interior) lemma rel_interior_nonempty_interior: fixes S :: "'n::euclidean_space set" shows "interior S \ {} \ rel_interior S = interior S" by (metis interior_rel_interior_gen) lemma affine_hull_nonempty_interior: fixes S :: "'n::euclidean_space set" shows "interior S \ {} \ affine hull S = UNIV" by (metis affine_hull_UNIV interior_rel_interior_gen) lemma rel_interior_affine_hull [simp]: fixes S :: "'n::euclidean_space set" shows "rel_interior (affine hull S) = affine hull S" proof - have *: "rel_interior (affine hull S) \ affine hull S" using rel_interior_subset by auto { fix x assume x: "x \ affine hull S" define e :: real where "e = 1" then have "e > 0" "ball x e \ affine hull (affine hull S) \ affine hull S" using hull_hull[of _ S] by auto then have "x \ rel_interior (affine hull S)" using x rel_interior_ball[of "affine hull S"] by auto } then show ?thesis using * by auto qed lemma rel_interior_UNIV [simp]: "rel_interior (UNIV :: ('n::euclidean_space) set) = UNIV" by (metis open_UNIV rel_interior_open) lemma rel_interior_convex_shrink: fixes S :: "'a::euclidean_space set" assumes "convex S" and "c \ rel_interior S" and "x \ S" and "0 < e" and "e \ 1" shows "x - e *\<^sub>R (x - c) \ rel_interior S" proof - obtain d where "d > 0" and d: "ball c d \ affine hull S \ S" using assms(2) unfolding mem_rel_interior_ball by auto { fix y assume as: "dist (x - e *\<^sub>R (x - c)) y < e * d" "y \ affine hull S" have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using \e > 0\ by (auto simp: scaleR_left_diff_distrib scaleR_right_diff_distrib) have "x \ affine hull S" using assms hull_subset[of S] by auto moreover have "1 / e + - ((1 - e) / e) = 1" using \e > 0\ left_diff_distrib[of "1" "(1-e)" "1/e"] by auto ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x \ affine hull S" using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"] by (simp add: algebra_simps) have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \1/e\ * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)" unfolding dist_norm norm_scaleR[symmetric] apply (rule arg_cong[where f=norm]) using \e > 0\ apply (auto simp: euclidean_eq_iff[where 'a='a] field_simps inner_simps) done also have "\ = \1/e\ * norm (x - e *\<^sub>R (x - c) - y)" by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps) also have "\ < d" using as[unfolded dist_norm] and \e > 0\ by (auto simp:pos_divide_less_eq[OF \e > 0\] mult.commute) finally have "y \ S" apply (subst *) apply (rule assms(1)[unfolded convex_alt,rule_format]) apply (rule d[THEN subsetD]) unfolding mem_ball using assms(3-5) ** apply auto done } then have "ball (x - e *\<^sub>R (x - c)) (e*d) \ affine hull S \ S" by auto moreover have "e * d > 0" using \e > 0\ \d > 0\ by simp moreover have c: "c \ S" using assms rel_interior_subset by auto moreover from c have "x - e *\<^sub>R (x - c) \ S" using convexD_alt[of S x c e] apply (simp add: algebra_simps) using assms apply auto done ultimately show ?thesis using mem_rel_interior_ball[of "x - e *\<^sub>R (x - c)" S] \e > 0\ by auto qed lemma interior_real_atLeast [simp]: fixes a :: real shows "interior {a..} = {a<..}" proof - { fix y assume "a < y" then have "y \ interior {a..}" apply (simp add: mem_interior) apply (rule_tac x="(y-a)" in exI) apply (auto simp: dist_norm) done } moreover { fix y assume "y \ interior {a..}" then obtain e where e: "e > 0" "cball y e \ {a..}" using mem_interior_cball[of y "{a..}"] by auto moreover from e have "y - e \ cball y e" by (auto simp: cball_def dist_norm) ultimately have "a \ y - e" by blast then have "a < y" using e by auto } ultimately show ?thesis by auto qed lemma continuous_ge_on_Ioo: assumes "continuous_on {c..d} g" "\x. x \ {c<.. g x \ a" "c < d" "x \ {c..d}" shows "g (x::real) \ (a::real)" proof- from assms(3) have "{c..d} = closure {c<.. (g -` {a..} \ {c..d})" by auto hence "closure {c<.. closure (g -` {a..} \ {c..d})" by (rule closure_mono) also from assms(1) have "closed (g -` {a..} \ {c..d})" by (auto simp: continuous_on_closed_vimage) hence "closure (g -` {a..} \ {c..d}) = g -` {a..} \ {c..d}" by simp finally show ?thesis using \x \ {c..d}\ by auto qed lemma interior_real_atMost [simp]: fixes a :: real shows "interior {..a} = {.. y" then have "y \ interior {..a}" apply (simp add: mem_interior) apply (rule_tac x="(a-y)" in exI) apply (auto simp: dist_norm) done } moreover { fix y assume "y \ interior {..a}" then obtain e where e: "e > 0" "cball y e \ {..a}" using mem_interior_cball[of y "{..a}"] by auto moreover from e have "y + e \ cball y e" by (auto simp: cball_def dist_norm) ultimately have "a \ y + e" by auto then have "a > y" using e by auto } ultimately show ?thesis by auto qed lemma interior_atLeastAtMost_real [simp]: "interior {a..b} = {a<.. {..b}" by auto also have "interior \ = {a<..} \ {.. = {a<.. {}" using assms unfolding set_eq_iff by (auto intro!: exI[of _ "(a + b) / 2"] simp: box_def) then show ?thesis using interior_rel_interior_gen[of "cbox a b", symmetric] by (simp split: if_split_asm del: box_real add: box_real[symmetric] interior_cbox) qed lemma rel_interior_real_semiline [simp]: fixes a :: real shows "rel_interior {a..} = {a<..}" proof - have *: "{a<..} \ {}" unfolding set_eq_iff by (auto intro!: exI[of _ "a + 1"]) then show ?thesis using interior_real_atLeast interior_rel_interior_gen[of "{a..}"] by (auto split: if_split_asm) qed subsubsection \Relative open sets\ definition\<^marker>\tag important\ "rel_open S \ rel_interior S = S" lemma rel_open: "rel_open S \ openin (top_of_set (affine hull S)) S" unfolding rel_open_def rel_interior_def apply auto using openin_subopen[of "top_of_set (affine hull S)" S] apply auto done lemma openin_rel_interior: "openin (top_of_set (affine hull S)) (rel_interior S)" apply (simp add: rel_interior_def) apply (subst openin_subopen, blast) done lemma openin_set_rel_interior: "openin (top_of_set S) (rel_interior S)" by (rule openin_subset_trans [OF openin_rel_interior rel_interior_subset hull_subset]) lemma affine_rel_open: fixes S :: "'n::euclidean_space set" assumes "affine S" shows "rel_open S" unfolding rel_open_def using assms rel_interior_affine_hull[of S] affine_hull_eq[of S] by metis lemma affine_closed: fixes S :: "'n::euclidean_space set" assumes "affine S" shows "closed S" proof - { assume "S \ {}" then obtain L where L: "subspace L" "affine_parallel S L" using assms affine_parallel_subspace[of S] by auto then obtain a where a: "S = ((+) a ` L)" using affine_parallel_def[of L S] affine_parallel_commut by auto from L have "closed L" using closed_subspace by auto then have "closed S" using closed_translation a by auto } then show ?thesis by auto qed lemma closure_affine_hull: fixes S :: "'n::euclidean_space set" shows "closure S \ affine hull S" by (intro closure_minimal hull_subset affine_closed affine_affine_hull) lemma closure_same_affine_hull [simp]: fixes S :: "'n::euclidean_space set" shows "affine hull (closure S) = affine hull S" proof - have "affine hull (closure S) \ affine hull S" using hull_mono[of "closure S" "affine hull S" "affine"] closure_affine_hull[of S] hull_hull[of "affine" S] by auto moreover have "affine hull (closure S) \ affine hull S" using hull_mono[of "S" "closure S" "affine"] closure_subset by auto ultimately show ?thesis by auto qed lemma closure_aff_dim [simp]: fixes S :: "'n::euclidean_space set" shows "aff_dim (closure S) = aff_dim S" proof - have "aff_dim S \ aff_dim (closure S)" using aff_dim_subset closure_subset by auto moreover have "aff_dim (closure S) \ aff_dim (affine hull S)" using aff_dim_subset closure_affine_hull by blast moreover have "aff_dim (affine hull S) = aff_dim S" using aff_dim_affine_hull by auto ultimately show ?thesis by auto qed lemma rel_interior_closure_convex_shrink: fixes S :: "_::euclidean_space set" assumes "convex S" and "c \ rel_interior S" and "x \ closure S" and "e > 0" and "e \ 1" shows "x - e *\<^sub>R (x - c) \ rel_interior S" proof - obtain d where "d > 0" and d: "ball c d \ affine hull S \ S" using assms(2) unfolding mem_rel_interior_ball by auto have "\y \ S. norm (y - x) * (1 - e) < e * d" proof (cases "x \ S") case True then show ?thesis using \e > 0\ \d > 0\ apply (rule_tac bexI[where x=x], auto) done next case False then have x: "x islimpt S" using assms(3)[unfolded closure_def] by auto show ?thesis proof (cases "e = 1") case True obtain y where "y \ S" "y \ x" "dist y x < 1" using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto then show ?thesis apply (rule_tac x=y in bexI) unfolding True using \d > 0\ apply auto done next case False then have "0 < e * d / (1 - e)" and *: "1 - e > 0" using \e \ 1\ \e > 0\ \d > 0\ by auto then obtain y where "y \ S" "y \ x" "dist y x < e * d / (1 - e)" using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto then show ?thesis apply (rule_tac x=y in bexI) unfolding dist_norm using pos_less_divide_eq[OF *] apply auto done qed qed then obtain y where "y \ S" and y: "norm (y - x) * (1 - e) < e * d" by auto define z where "z = c + ((1 - e) / e) *\<^sub>R (x - y)" have *: "x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using \e > 0\ by (auto simp: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib) have zball: "z \ ball c d" using mem_ball z_def dist_norm[of c] using y and assms(4,5) by (simp add: norm_minus_commute) (simp add: field_simps) have "x \ affine hull S" using closure_affine_hull assms by auto moreover have "y \ affine hull S" using \y \ S\ hull_subset[of S] by auto moreover have "c \ affine hull S" using assms rel_interior_subset hull_subset[of S] by auto ultimately have "z \ affine hull S" using z_def affine_affine_hull[of S] mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"] assms by simp then have "z \ S" using d zball by auto obtain d1 where "d1 > 0" and d1: "ball z d1 \ ball c d" using zball open_ball[of c d] openE[of "ball c d" z] by auto then have "ball z d1 \ affine hull S \ ball c d \ affine hull S" by auto then have "ball z d1 \ affine hull S \ S" using d by auto then have "z \ rel_interior S" using mem_rel_interior_ball using \d1 > 0\ \z \ S\ by auto then have "y - e *\<^sub>R (y - z) \ rel_interior S" using rel_interior_convex_shrink[of S z y e] assms \y \ S\ by auto then show ?thesis using * by auto qed lemma rel_interior_eq: "rel_interior s = s \ openin(top_of_set (affine hull s)) s" using rel_open rel_open_def by blast lemma rel_interior_openin: "openin(top_of_set (affine hull s)) s \ rel_interior s = s" by (simp add: rel_interior_eq) lemma rel_interior_affine: fixes S :: "'n::euclidean_space set" shows "affine S \ rel_interior S = S" using affine_rel_open rel_open_def by auto lemma rel_interior_eq_closure: fixes S :: "'n::euclidean_space set" shows "rel_interior S = closure S \ affine S" proof (cases "S = {}") case True then show ?thesis by auto next case False show ?thesis proof assume eq: "rel_interior S = closure S" have "S = {} \ S = affine hull S" apply (rule connected_clopen [THEN iffD1, rule_format]) apply (simp add: affine_imp_convex convex_connected) apply (rule conjI) apply (metis eq closure_subset openin_rel_interior rel_interior_subset subset_antisym) apply (metis closed_subset closure_subset_eq eq hull_subset rel_interior_subset) done with False have "affine hull S = S" by auto then show "affine S" by (metis affine_hull_eq) next assume "affine S" then show "rel_interior S = closure S" by (simp add: rel_interior_affine affine_closed) qed qed subsubsection\<^marker>\tag unimportant\\Relative interior preserves under linear transformations\ lemma rel_interior_translation_aux: fixes a :: "'n::euclidean_space" shows "((\x. a + x) ` rel_interior S) \ rel_interior ((\x. a + x) ` S)" proof - { fix x assume x: "x \ rel_interior S" then obtain T where "open T" "x \ T \ S" "T \ affine hull S \ S" using mem_rel_interior[of x S] by auto then have "open ((\x. a + x) ` T)" and "a + x \ ((\x. a + x) ` T) \ ((\x. a + x) ` S)" and "((\x. a + x) ` T) \ affine hull ((\x. a + x) ` S) \ (\x. a + x) ` S" using affine_hull_translation[of a S] open_translation[of T a] x by auto then have "a + x \ rel_interior ((\x. a + x) ` S)" using mem_rel_interior[of "a+x" "((\x. a + x) ` S)"] by auto } then show ?thesis by auto qed lemma rel_interior_translation: fixes a :: "'n::euclidean_space" shows "rel_interior ((\x. a + x) ` S) = (\x. a + x) ` rel_interior S" proof - have "(\x. (-a) + x) ` rel_interior ((\x. a + x) ` S) \ rel_interior S" using rel_interior_translation_aux[of "-a" "(\x. a + x) ` S"] translation_assoc[of "-a" "a"] by auto then have "((\x. a + x) ` rel_interior S) \ rel_interior ((\x. a + x) ` S)" using translation_inverse_subset[of a "rel_interior ((+) a ` S)" "rel_interior S"] by auto then show ?thesis using rel_interior_translation_aux[of a S] by auto qed lemma affine_hull_linear_image: assumes "bounded_linear f" shows "f ` (affine hull s) = affine hull f ` s" proof - interpret f: bounded_linear f by fact have "affine {x. f x \ affine hull f ` s}" unfolding affine_def by (auto simp: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format]) moreover have "affine {x. x \ f ` (affine hull s)}" using affine_affine_hull[unfolded affine_def, of s] unfolding affine_def by (auto simp: f.scaleR [symmetric] f.add [symmetric]) ultimately show ?thesis by (auto simp: hull_inc elim!: hull_induct) qed lemma rel_interior_injective_on_span_linear_image: fixes f :: "'m::euclidean_space \ 'n::euclidean_space" and S :: "'m::euclidean_space set" assumes "bounded_linear f" and "inj_on f (span S)" shows "rel_interior (f ` S) = f ` (rel_interior S)" proof - { fix z assume z: "z \ rel_interior (f ` S)" then have "z \ f ` S" using rel_interior_subset[of "f ` S"] by auto then obtain x where x: "x \ S" "f x = z" by auto obtain e2 where e2: "e2 > 0" "cball z e2 \ affine hull (f ` S) \ (f ` S)" using z rel_interior_cball[of "f ` S"] by auto obtain K where K: "K > 0" "\x. norm (f x) \ norm x * K" using assms Real_Vector_Spaces.bounded_linear.pos_bounded[of f] by auto define e1 where "e1 = 1 / K" then have e1: "e1 > 0" "\x. e1 * norm (f x) \ norm x" using K pos_le_divide_eq[of e1] by auto define e where "e = e1 * e2" then have "e > 0" using e1 e2 by auto { fix y assume y: "y \ cball x e \ affine hull S" then have h1: "f y \ affine hull (f ` S)" using affine_hull_linear_image[of f S] assms by auto from y have "norm (x-y) \ e1 * e2" using cball_def[of x e] dist_norm[of x y] e_def by auto moreover have "f x - f y = f (x - y)" using assms linear_diff[of f x y] linear_conv_bounded_linear[of f] by auto moreover have "e1 * norm (f (x-y)) \ norm (x - y)" using e1 by auto ultimately have "e1 * norm ((f x)-(f y)) \ e1 * e2" by auto then have "f y \ cball z e2" using cball_def[of "f x" e2] dist_norm[of "f x" "f y"] e1 x by auto then have "f y \ f ` S" using y e2 h1 by auto then have "y \ S" using assms y hull_subset[of S] affine_hull_subset_span inj_on_image_mem_iff [OF \inj_on f (span S)\] by (metis Int_iff span_superset subsetCE) } then have "z \ f ` (rel_interior S)" using mem_rel_interior_cball[of x S] \e > 0\ x by auto } moreover { fix x assume x: "x \ rel_interior S" then obtain e2 where e2: "e2 > 0" "cball x e2 \ affine hull S \ S" using rel_interior_cball[of S] by auto have "x \ S" using x rel_interior_subset by auto then have *: "f x \ f ` S" by auto have "\x\span S. f x = 0 \ x = 0" using assms subspace_span linear_conv_bounded_linear[of f] linear_injective_on_subspace_0[of f "span S"] by auto then obtain e1 where e1: "e1 > 0" "\x \ span S. e1 * norm x \ norm (f x)" using assms injective_imp_isometric[of "span S" f] subspace_span[of S] closed_subspace[of "span S"] by auto define e where "e = e1 * e2" hence "e > 0" using e1 e2 by auto { fix y assume y: "y \ cball (f x) e \ affine hull (f ` S)" then have "y \ f ` (affine hull S)" using affine_hull_linear_image[of f S] assms by auto then obtain xy where xy: "xy \ affine hull S" "f xy = y" by auto with y have "norm (f x - f xy) \ e1 * e2" using cball_def[of "f x" e] dist_norm[of "f x" y] e_def by auto moreover have "f x - f xy = f (x - xy)" using assms linear_diff[of f x xy] linear_conv_bounded_linear[of f] by auto moreover have *: "x - xy \ span S" using subspace_diff[of "span S" x xy] subspace_span \x \ S\ xy affine_hull_subset_span[of S] span_superset by auto moreover from * have "e1 * norm (x - xy) \ norm (f (x - xy))" using e1 by auto ultimately have "e1 * norm (x - xy) \ e1 * e2" by auto then have "xy \ cball x e2" using cball_def[of x e2] dist_norm[of x xy] e1 by auto then have "y \ f ` S" using xy e2 by auto } then have "f x \ rel_interior (f ` S)" using mem_rel_interior_cball[of "(f x)" "(f ` S)"] * \e > 0\ by auto } ultimately show ?thesis by auto qed lemma rel_interior_injective_linear_image: fixes f :: "'m::euclidean_space \ 'n::euclidean_space" assumes "bounded_linear f" and "inj f" shows "rel_interior (f ` S) = f ` (rel_interior S)" using assms rel_interior_injective_on_span_linear_image[of f S] subset_inj_on[of f "UNIV" "span S"] by auto subsection\<^marker>\tag unimportant\ \Openness and compactness are preserved by convex hull operation\ lemma open_convex_hull[intro]: fixes S :: "'a::real_normed_vector set" assumes "open S" shows "open (convex hull S)" proof (clarsimp simp: open_contains_cball convex_hull_explicit) fix T and u :: "'a\real" assume obt: "finite T" "T\S" "\x\T. 0 \ u x" "sum u T = 1" from assms[unfolded open_contains_cball] obtain b where b: "\x. x\S \ 0 < b x \ cball x (b x) \ S" by metis have "b ` T \ {}" using obt by auto define i where "i = b ` T" let ?\ = "\y. \F. finite F \ F \ S \ (\u. (\x\F. 0 \ u x) \ sum u F = 1 \ (\v\F. u v *\<^sub>R v) = y)" let ?a = "\v\T. u v *\<^sub>R v" show "\e > 0. cball ?a e \ {y. ?\ y}" proof (intro exI subsetI conjI) show "0 < Min i" unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] \b ` T\{}\] using b \T\S\ by auto next fix y assume "y \ cball ?a (Min i)" then have y: "norm (?a - y) \ Min i" unfolding dist_norm[symmetric] by auto { fix x assume "x \ T" then have "Min i \ b x" by (simp add: i_def obt(1)) then have "x + (y - ?a) \ cball x (b x)" using y unfolding mem_cball dist_norm by auto moreover have "x \ S" using \x\T\ \T\S\ by auto ultimately have "x + (y - ?a) \ S" using y b by blast } moreover have *: "inj_on (\v. v + (y - ?a)) T" unfolding inj_on_def by auto have "(\v\(\v. v + (y - ?a)) ` T. u (v - (y - ?a)) *\<^sub>R v) = y" unfolding sum.reindex[OF *] o_def using obt(4) by (simp add: sum.distrib sum_subtractf scaleR_left.sum[symmetric] scaleR_right_distrib) ultimately show "y \ {y. ?\ y}" proof (intro CollectI exI conjI) show "finite ((\v. v + (y - ?a)) ` T)" by (simp add: obt(1)) show "sum (\v. u (v - (y - ?a))) ((\v. v + (y - ?a)) ` T) = 1" unfolding sum.reindex[OF *] o_def using obt(4) by auto qed (use obt(1, 3) in auto) qed qed lemma compact_convex_combinations: fixes S T :: "'a::real_normed_vector set" assumes "compact S" "compact T" shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ S \ y \ T}" proof - let ?X = "{0..1} \ S \ T" let ?h = "(\z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))" have *: "{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ S \ y \ T} = ?h ` ?X" by force have "continuous_on ?X (\z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))" unfolding continuous_on by (rule ballI) (intro tendsto_intros) with assms show ?thesis by (simp add: * compact_Times compact_continuous_image) qed lemma finite_imp_compact_convex_hull: fixes S :: "'a::real_normed_vector set" assumes "finite S" shows "compact (convex hull S)" proof (cases "S = {}") case True then show ?thesis by simp next case False with assms show ?thesis proof (induct rule: finite_ne_induct) case (singleton x) show ?case by simp next case (insert x A) let ?f = "\(u, y::'a). u *\<^sub>R x + (1 - u) *\<^sub>R y" let ?T = "{0..1::real} \ (convex hull A)" have "continuous_on ?T ?f" unfolding split_def continuous_on by (intro ballI tendsto_intros) moreover have "compact ?T" by (intro compact_Times compact_Icc insert) ultimately have "compact (?f ` ?T)" by (rule compact_continuous_image) also have "?f ` ?T = convex hull (insert x A)" unfolding convex_hull_insert [OF \A \ {}\] apply safe apply (rule_tac x=a in exI, simp) apply (rule_tac x="1 - a" in exI, simp, fast) apply (rule_tac x="(u, b)" in image_eqI, simp_all) done finally show "compact (convex hull (insert x A))" . qed qed lemma compact_convex_hull: fixes S :: "'a::euclidean_space set" assumes "compact S" shows "compact (convex hull S)" proof (cases "S = {}") case True then show ?thesis using compact_empty by simp next case False then obtain w where "w \ S" by auto show ?thesis unfolding caratheodory[of S] proof (induct ("DIM('a) + 1")) case 0 have *: "{x.\sa. finite sa \ sa \ S \ card sa \ 0 \ x \ convex hull sa} = {}" using compact_empty by auto from 0 show ?case unfolding * by simp next case (Suc n) show ?case proof (cases "n = 0") case True have "{x. \T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T} = S" unfolding set_eq_iff and mem_Collect_eq proof (rule, rule) fix x assume "\T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T" then obtain T where T: "finite T" "T \ S" "card T \ Suc n" "x \ convex hull T" by auto show "x \ S" proof (cases "card T = 0") case True then show ?thesis using T(4) unfolding card_0_eq[OF T(1)] by simp next case False then have "card T = Suc 0" using T(3) \n=0\ by auto then obtain a where "T = {a}" unfolding card_Suc_eq by auto then show ?thesis using T(2,4) by simp qed next fix x assume "x\S" then show "\T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T" apply (rule_tac x="{x}" in exI) unfolding convex_hull_singleton apply auto done qed then show ?thesis using assms by simp next case False have "{x. \T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T} = {(1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ S \ y \ {x. \T. finite T \ T \ S \ card T \ n \ x \ convex hull T}}" unfolding set_eq_iff and mem_Collect_eq proof (rule, rule) fix x assume "\u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \ 0 \ c \ c \ 1 \ u \ S \ (\T. finite T \ T \ S \ card T \ n \ v \ convex hull T)" then obtain u v c T where obt: "x = (1 - c) *\<^sub>R u + c *\<^sub>R v" "0 \ c \ c \ 1" "u \ S" "finite T" "T \ S" "card T \ n" "v \ convex hull T" by auto moreover have "(1 - c) *\<^sub>R u + c *\<^sub>R v \ convex hull insert u T" apply (rule convexD_alt) using obt(2) and convex_convex_hull and hull_subset[of "insert u T" convex] using obt(7) and hull_mono[of T "insert u T"] apply auto done ultimately show "\T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T" apply (rule_tac x="insert u T" in exI) apply (auto simp: card_insert_if) done next fix x assume "\T. finite T \ T \ S \ card T \ Suc n \ x \ convex hull T" then obtain T where T: "finite T" "T \ S" "card T \ Suc n" "x \ convex hull T" by auto show "\u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \ 0 \ c \ c \ 1 \ u \ S \ (\T. finite T \ T \ S \ card T \ n \ v \ convex hull T)" proof (cases "card T = Suc n") case False then have "card T \ n" using T(3) by auto then show ?thesis apply (rule_tac x=w in exI, rule_tac x=x in exI, rule_tac x=1 in exI) using \w\S\ and T apply (auto intro!: exI[where x=T]) done next case True then obtain a u where au: "T = insert a u" "a\u" apply (drule_tac card_eq_SucD, auto) done show ?thesis proof (cases "u = {}") case True then have "x = a" using T(4)[unfolded au] by auto show ?thesis unfolding \x = a\ apply (rule_tac x=a in exI) apply (rule_tac x=a in exI) apply (rule_tac x=1 in exI) using T and \n \ 0\ unfolding au apply (auto intro!: exI[where x="{a}"]) done next case False obtain ux vx b where obt: "ux\0" "vx\0" "ux + vx = 1" "b \ convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b" using T(4)[unfolded au convex_hull_insert[OF False]] by auto have *: "1 - vx = ux" using obt(3) by auto show ?thesis apply (rule_tac x=a in exI) apply (rule_tac x=b in exI) apply (rule_tac x=vx in exI) using obt and T(1-3) unfolding au and * using card_insert_disjoint[OF _ au(2)] apply (auto intro!: exI[where x=u]) done qed qed qed then show ?thesis using compact_convex_combinations[OF assms Suc] by simp qed qed qed subsection\<^marker>\tag unimportant\ \Extremal points of a simplex are some vertices\ lemma dist_increases_online: fixes a b d :: "'a::real_inner" assumes "d \ 0" shows "dist a (b + d) > dist a b \ dist a (b - d) > dist a b" proof (cases "inner a d - inner b d > 0") case True then have "0 < inner d d + (inner a d * 2 - inner b d * 2)" apply (rule_tac add_pos_pos) using assms apply auto done then show ?thesis apply (rule_tac disjI2) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff apply (simp add: algebra_simps inner_commute) done next case False then have "0 < inner d d + (inner b d * 2 - inner a d * 2)" apply (rule_tac add_pos_nonneg) using assms apply auto done then show ?thesis apply (rule_tac disjI1) unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff apply (simp add: algebra_simps inner_commute) done qed lemma norm_increases_online: fixes d :: "'a::real_inner" shows "d \ 0 \ norm (a + d) > norm a \ norm(a - d) > norm a" using dist_increases_online[of d a 0] unfolding dist_norm by auto lemma simplex_furthest_lt: fixes S :: "'a::real_inner set" assumes "finite S" shows "\x \ convex hull S. x \ S \ (\y \ convex hull S. norm (x - a) < norm(y - a))" using assms proof induct fix x S assume as: "finite S" "x\S" "\x\convex hull S. x \ S \ (\y\convex hull S. norm (x - a) < norm (y - a))" show "\xa\convex hull insert x S. xa \ insert x S \ (\y\convex hull insert x S. norm (xa - a) < norm (y - a))" proof (intro impI ballI, cases "S = {}") case False fix y assume y: "y \ convex hull insert x S" "y \ insert x S" obtain u v b where obt: "u\0" "v\0" "u + v = 1" "b \ convex hull S" "y = u *\<^sub>R x + v *\<^sub>R b" using y(1)[unfolded convex_hull_insert[OF False]] by auto show "\z\convex hull insert x S. norm (y - a) < norm (z - a)" proof (cases "y \ convex hull S") case True then obtain z where "z \ convex hull S" "norm (y - a) < norm (z - a)" using as(3)[THEN bspec[where x=y]] and y(2) by auto then show ?thesis apply (rule_tac x=z in bexI) unfolding convex_hull_insert[OF False] apply auto done next case False show ?thesis using obt(3) proof (cases "u = 0", case_tac[!] "v = 0") assume "u = 0" "v \ 0" then have "y = b" using obt by auto then show ?thesis using False and obt(4) by auto next assume "u \ 0" "v = 0" then have "y = x" using obt by auto then show ?thesis using y(2) by auto next assume "u \ 0" "v \ 0" then obtain w where w: "w>0" "w b" proof assume "x = b" then have "y = b" unfolding obt(5) using obt(3) by (auto simp: scaleR_left_distrib[symmetric]) then show False using obt(4) and False by simp qed then have *: "w *\<^sub>R (x - b) \ 0" using w(1) by auto show ?thesis using dist_increases_online[OF *, of a y] proof (elim disjE) assume "dist a y < dist a (y + w *\<^sub>R (x - b))" then have "norm (y - a) < norm ((u + w) *\<^sub>R x + (v - w) *\<^sub>R b - a)" unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps) moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \ convex hull insert x S" unfolding convex_hull_insert[OF \S\{}\] proof (intro CollectI conjI exI) show "u + w \ 0" "v - w \ 0" using obt(1) w by auto qed (use obt in auto) ultimately show ?thesis by auto next assume "dist a y < dist a (y - w *\<^sub>R (x - b))" then have "norm (y - a) < norm ((u - w) *\<^sub>R x + (v + w) *\<^sub>R b - a)" unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: algebra_simps) moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \ convex hull insert x S" unfolding convex_hull_insert[OF \S\{}\] proof (intro CollectI conjI exI) show "u - w \ 0" "v + w \ 0" using obt(1) w by auto qed (use obt in auto) ultimately show ?thesis by auto qed qed auto qed qed auto qed (auto simp: assms) lemma simplex_furthest_le: fixes S :: "'a::real_inner set" assumes "finite S" and "S \ {}" shows "\y\S. \x\ convex hull S. norm (x - a) \ norm (y - a)" proof - have "convex hull S \ {}" using hull_subset[of S convex] and assms(2) by auto then obtain x where x: "x \ convex hull S" "\y\convex hull S. norm (y - a) \ norm (x - a)" using distance_attains_sup[OF finite_imp_compact_convex_hull[OF \finite S\], of a] unfolding dist_commute[of a] unfolding dist_norm by auto show ?thesis proof (cases "x \ S") case False then obtain y where "y \ convex hull S" "norm (x - a) < norm (y - a)" using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1) by auto then show ?thesis using x(2)[THEN bspec[where x=y]] by auto next case True with x show ?thesis by auto qed qed lemma simplex_furthest_le_exists: fixes S :: "('a::real_inner) set" shows "finite S \ \x\(convex hull S). \y\S. norm (x - a) \ norm (y - a)" using simplex_furthest_le[of S] by (cases "S = {}") auto lemma simplex_extremal_le: fixes S :: "'a::real_inner set" assumes "finite S" and "S \ {}" shows "\u\S. \v\S. \x\convex hull S. \y \ convex hull S. norm (x - y) \ norm (u - v)" proof - have "convex hull S \ {}" using hull_subset[of S convex] and assms(2) by auto then obtain u v where obt: "u \ convex hull S" "v \ convex hull S" "\x\convex hull S. \y\convex hull S. norm (x - y) \ norm (u - v)" using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]] by (auto simp: dist_norm) then show ?thesis proof (cases "u\S \ v\S", elim disjE) assume "u \ S" then obtain y where "y \ convex hull S" "norm (u - v) < norm (y - v)" using simplex_furthest_lt[OF assms(1), THEN bspec[where x=u]] and obt(1) by auto then show ?thesis using obt(3)[THEN bspec[where x=y], THEN bspec[where x=v]] and obt(2) by auto next assume "v \ S" then obtain y where "y \ convex hull S" "norm (v - u) < norm (y - u)" using simplex_furthest_lt[OF assms(1), THEN bspec[where x=v]] and obt(2) by auto then show ?thesis using obt(3)[THEN bspec[where x=u], THEN bspec[where x=y]] and obt(1) by (auto simp: norm_minus_commute) qed auto qed lemma simplex_extremal_le_exists: fixes S :: "'a::real_inner set" shows "finite S \ x \ convex hull S \ y \ convex hull S \ \u\S. \v\S. norm (x - y) \ norm (u - v)" using convex_hull_empty simplex_extremal_le[of S] by(cases "S = {}") auto subsection \Closest point of a convex set is unique, with a continuous projection\ definition\<^marker>\tag important\ closest_point :: "'a::{real_inner,heine_borel} set \ 'a \ 'a" where "closest_point S a = (SOME x. x \ S \ (\y\S. dist a x \ dist a y))" lemma closest_point_exists: assumes "closed S" and "S \ {}" shows "closest_point S a \ S" and "\y\S. dist a (closest_point S a) \ dist a y" unfolding closest_point_def apply(rule_tac[!] someI2_ex) apply (auto intro: distance_attains_inf[OF assms(1,2), of a]) done lemma closest_point_in_set: "closed S \ S \ {} \ closest_point S a \ S" by (meson closest_point_exists) lemma closest_point_le: "closed S \ x \ S \ dist a (closest_point S a) \ dist a x" using closest_point_exists[of S] by auto lemma closest_point_self: assumes "x \ S" shows "closest_point S x = x" unfolding closest_point_def apply (rule some1_equality, rule ex1I[of _ x]) using assms apply auto done lemma closest_point_refl: "closed S \ S \ {} \ closest_point S x = x \ x \ S" using closest_point_in_set[of S x] closest_point_self[of x S] by auto lemma closer_points_lemma: assumes "inner y z > 0" shows "\u>0. \v>0. v \ u \ norm(v *\<^sub>R z - y) < norm y" proof - have z: "inner z z > 0" unfolding inner_gt_zero_iff using assms by auto have "norm (v *\<^sub>R z - y) < norm y" if "0 < v" and "v \ inner y z / inner z z" for v unfolding norm_lt using z assms that by (simp add: field_simps inner_diff inner_commute mult_strict_left_mono[OF _ \0]) then show ?thesis using assms z by (rule_tac x = "inner y z / inner z z" in exI) auto qed lemma closer_point_lemma: assumes "inner (y - x) (z - x) > 0" shows "\u>0. u \ 1 \ dist (x + u *\<^sub>R (z - x)) y < dist x y" proof - obtain u where "u > 0" and u: "\v>0. v \ u \ norm (v *\<^sub>R (z - x) - (y - x)) < norm (y - x)" using closer_points_lemma[OF assms] by auto show ?thesis apply (rule_tac x="min u 1" in exI) using u[THEN spec[where x="min u 1"]] and \u > 0\ unfolding dist_norm by (auto simp: norm_minus_commute field_simps) qed lemma any_closest_point_dot: assumes "convex S" "closed S" "x \ S" "y \ S" "\z\S. dist a x \ dist a z" shows "inner (a - x) (y - x) \ 0" proof (rule ccontr) assume "\ ?thesis" then obtain u where u: "u>0" "u\1" "dist (x + u *\<^sub>R (y - x)) a < dist x a" using closer_point_lemma[of a x y] by auto let ?z = "(1 - u) *\<^sub>R x + u *\<^sub>R y" have "?z \ S" using convexD_alt[OF assms(1,3,4), of u] using u by auto then show False using assms(5)[THEN bspec[where x="?z"]] and u(3) by (auto simp: dist_commute algebra_simps) qed lemma any_closest_point_unique: fixes x :: "'a::real_inner" assumes "convex S" "closed S" "x \ S" "y \ S" "\z\S. dist a x \ dist a z" "\z\S. dist a y \ dist a z" shows "x = y" using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)] unfolding norm_pths(1) and norm_le_square by (auto simp: algebra_simps) lemma closest_point_unique: assumes "convex S" "closed S" "x \ S" "\z\S. dist a x \ dist a z" shows "x = closest_point S a" using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point S a"] using closest_point_exists[OF assms(2)] and assms(3) by auto lemma closest_point_dot: assumes "convex S" "closed S" "x \ S" shows "inner (a - closest_point S a) (x - closest_point S a) \ 0" apply (rule any_closest_point_dot[OF assms(1,2) _ assms(3)]) using closest_point_exists[OF assms(2)] and assms(3) apply auto done lemma closest_point_lt: assumes "convex S" "closed S" "x \ S" "x \ closest_point S a" shows "dist a (closest_point S a) < dist a x" apply (rule ccontr) apply (rule_tac notE[OF assms(4)]) apply (rule closest_point_unique[OF assms(1-3), of a]) using closest_point_le[OF assms(2), of _ a] apply fastforce done lemma setdist_closest_point: "\closed S; S \ {}\ \ setdist {a} S = dist a (closest_point S a)" apply (rule setdist_unique) using closest_point_le apply (auto simp: closest_point_in_set) done lemma closest_point_lipschitz: assumes "convex S" and "closed S" "S \ {}" shows "dist (closest_point S x) (closest_point S y) \ dist x y" proof - have "inner (x - closest_point S x) (closest_point S y - closest_point S x) \ 0" and "inner (y - closest_point S y) (closest_point S x - closest_point S y) \ 0" apply (rule_tac[!] any_closest_point_dot[OF assms(1-2)]) using closest_point_exists[OF assms(2-3)] apply auto done then show ?thesis unfolding dist_norm and norm_le using inner_ge_zero[of "(x - closest_point S x) - (y - closest_point S y)"] by (simp add: inner_add inner_diff inner_commute) qed lemma continuous_at_closest_point: assumes "convex S" and "closed S" and "S \ {}" shows "continuous (at x) (closest_point S)" unfolding continuous_at_eps_delta using le_less_trans[OF closest_point_lipschitz[OF assms]] by auto lemma continuous_on_closest_point: assumes "convex S" and "closed S" and "S \ {}" shows "continuous_on t (closest_point S)" by (metis continuous_at_imp_continuous_on continuous_at_closest_point[OF assms]) proposition closest_point_in_rel_interior: assumes "closed S" "S \ {}" and x: "x \ affine hull S" shows "closest_point S x \ rel_interior S \ x \ rel_interior S" proof (cases "x \ S") case True then show ?thesis by (simp add: closest_point_self) next case False then have "False" if asm: "closest_point S x \ rel_interior S" proof - obtain e where "e > 0" and clox: "closest_point S x \ S" and e: "cball (closest_point S x) e \ affine hull S \ S" using asm mem_rel_interior_cball by blast then have clo_notx: "closest_point S x \ x" using \x \ S\ by auto define y where "y \ closest_point S x - (min 1 (e / norm(closest_point S x - x))) *\<^sub>R (closest_point S x - x)" have "x - y = (1 - min 1 (e / norm (closest_point S x - x))) *\<^sub>R (x - closest_point S x)" by (simp add: y_def algebra_simps) then have "norm (x - y) = abs ((1 - min 1 (e / norm (closest_point S x - x)))) * norm(x - closest_point S x)" by simp also have "\ < norm(x - closest_point S x)" using clo_notx \e > 0\ by (auto simp: mult_less_cancel_right2 field_split_simps) finally have no_less: "norm (x - y) < norm (x - closest_point S x)" . have "y \ affine hull S" unfolding y_def by (meson affine_affine_hull clox hull_subset mem_affine_3_minus2 subsetD x) moreover have "dist (closest_point S x) y \ e" using \e > 0\ by (auto simp: y_def min_mult_distrib_right) ultimately have "y \ S" using subsetD [OF e] by simp then have "dist x (closest_point S x) \ dist x y" by (simp add: closest_point_le \closed S\) with no_less show False by (simp add: dist_norm) qed moreover have "x \ rel_interior S" using rel_interior_subset False by blast ultimately show ?thesis by blast qed subsubsection\<^marker>\tag unimportant\ \Various point-to-set separating/supporting hyperplane theorems\ lemma supporting_hyperplane_closed_point: fixes z :: "'a::{real_inner,heine_borel}" assumes "convex S" and "closed S" and "S \ {}" and "z \ S" shows "\a b. \y\S. inner a z < b \ inner a y = b \ (\x\S. inner a x \ b)" proof - obtain y where "y \ S" and y: "\x\S. dist z y \ dist z x" by (metis distance_attains_inf[OF assms(2-3)]) show ?thesis proof (intro exI bexI conjI ballI) show "(y - z) \ z < (y - z) \ y" by (metis \y \ S\ assms(4) diff_gt_0_iff_gt inner_commute inner_diff_left inner_gt_zero_iff right_minus_eq) show "(y - z) \ y \ (y - z) \ x" if "x \ S" for x proof (rule ccontr) have *: "\u. 0 \ u \ u \ 1 \ dist z y \ dist z ((1 - u) *\<^sub>R y + u *\<^sub>R x)" using assms(1)[unfolded convex_alt] and y and \x\S\ and \y\S\ by auto assume "\ (y - z) \ y \ (y - z) \ x" then obtain v where "v > 0" "v \ 1" "dist (y + v *\<^sub>R (x - y)) z < dist y z" using closer_point_lemma[of z y x] by (auto simp: inner_diff) then show False using *[of v] by (auto simp: dist_commute algebra_simps) qed qed (use \y \ S\ in auto) qed lemma separating_hyperplane_closed_point: fixes z :: "'a::{real_inner,heine_borel}" assumes "convex S" and "closed S" and "z \ S" shows "\a b. inner a z < b \ (\x\S. inner a x > b)" proof (cases "S = {}") case True then show ?thesis by (simp add: gt_ex) next case False obtain y where "y \ S" and y: "\x. x \ S \ dist z y \ dist z x" by (metis distance_attains_inf[OF assms(2) False]) show ?thesis proof (intro exI conjI ballI) show "(y - z) \ z < inner (y - z) z + (norm (y - z))\<^sup>2 / 2" using \y\S\ \z\S\ by auto next fix x assume "x \ S" have "False" if *: "0 < inner (z - y) (x - y)" proof - obtain u where "u > 0" "u \ 1" "dist (y + u *\<^sub>R (x - y)) z < dist y z" using * closer_point_lemma by blast then show False using y[of "y + u *\<^sub>R (x - y)"] convexD_alt [OF \convex S\] using \x\S\ \y\S\ by (auto simp: dist_commute algebra_simps) qed moreover have "0 < (norm (y - z))\<^sup>2" using \y\S\ \z\S\ by auto then have "0 < inner (y - z) (y - z)" unfolding power2_norm_eq_inner by simp ultimately show "(y - z) \ z + (norm (y - z))\<^sup>2 / 2 < (y - z) \ x" by (force simp: field_simps power2_norm_eq_inner inner_commute inner_diff) qed qed lemma separating_hyperplane_closed_0: assumes "convex (S::('a::euclidean_space) set)" and "closed S" and "0 \ S" shows "\a b. a \ 0 \ 0 < b \ (\x\S. inner a x > b)" proof (cases "S = {}") case True have "(SOME i. i\Basis) \ (0::'a)" by (metis Basis_zero SOME_Basis) then show ?thesis using True zero_less_one by blast next case False then show ?thesis using False using separating_hyperplane_closed_point[OF assms] by (metis all_not_in_conv inner_zero_left inner_zero_right less_eq_real_def not_le) qed subsubsection\<^marker>\tag unimportant\ \Now set-to-set for closed/compact sets\ lemma separating_hyperplane_closed_compact: fixes S :: "'a::euclidean_space set" assumes "convex S" and "closed S" and "convex T" and "compact T" and "T \ {}" and "S \ T = {}" shows "\a b. (\x\S. inner a x < b) \ (\x\T. inner a x > b)" proof (cases "S = {}") case True obtain b where b: "b > 0" "\x\T. norm x \ b" using compact_imp_bounded[OF assms(4)] unfolding bounded_pos by auto obtain z :: 'a where z: "norm z = b + 1" using vector_choose_size[of "b + 1"] and b(1) by auto then have "z \ T" using b(2)[THEN bspec[where x=z]] by auto then obtain a b where ab: "inner a z < b" "\x\T. b < inner a x" using separating_hyperplane_closed_point[OF assms(3) compact_imp_closed[OF assms(4)], of z] by auto then show ?thesis using True by auto next case False then obtain y where "y \ S" by auto obtain a b where "0 < b" "\x \ (\x\ S. \y \ T. {x - y}). b < inner a x" using separating_hyperplane_closed_point[OF convex_differences[OF assms(1,3)], of 0] using closed_compact_differences[OF assms(2,4)] using assms(6) by auto then have ab: "\x\S. \y\T. b + inner a y < inner a x" apply - apply rule apply rule apply (erule_tac x="x - y" in ballE) apply (auto simp: inner_diff) done define k where "k = (SUP x\T. a \ x)" show ?thesis apply (rule_tac x="-a" in exI) apply (rule_tac x="-(k + b / 2)" in exI) apply (intro conjI ballI) unfolding inner_minus_left and neg_less_iff_less proof - fix x assume "x \ T" then have "inner a x - b / 2 < k" unfolding k_def proof (subst less_cSUP_iff) show "T \ {}" by fact show "bdd_above ((\) a ` T)" using ab[rule_format, of y] \y \ S\ by (intro bdd_aboveI2[where M="inner a y - b"]) (auto simp: field_simps intro: less_imp_le) qed (auto intro!: bexI[of _ x] \0) then show "inner a x < k + b / 2" by auto next fix x assume "x \ S" then have "k \ inner a x - b" unfolding k_def apply (rule_tac cSUP_least) using assms(5) using ab[THEN bspec[where x=x]] apply auto done then show "k + b / 2 < inner a x" using \0 < b\ by auto qed qed lemma separating_hyperplane_compact_closed: fixes S :: "'a::euclidean_space set" assumes "convex S" and "compact S" and "S \ {}" and "convex T" and "closed T" and "S \ T = {}" shows "\a b. (\x\S. inner a x < b) \ (\x\T. inner a x > b)" proof - obtain a b where "(\x\T. inner a x < b) \ (\x\S. b < inner a x)" using separating_hyperplane_closed_compact[OF assms(4-5,1-2,3)] and assms(6) by auto then show ?thesis apply (rule_tac x="-a" in exI) apply (rule_tac x="-b" in exI, auto) done qed subsubsection\<^marker>\tag unimportant\ \General case without assuming closure and getting non-strict separation\ lemma separating_hyperplane_set_0: assumes "convex S" "(0::'a::euclidean_space) \ S" shows "\a. a \ 0 \ (\x\S. 0 \ inner a x)" proof - let ?k = "\c. {x::'a. 0 \ inner c x}" have *: "frontier (cball 0 1) \ \f \ {}" if as: "f \ ?k ` S" "finite f" for f proof - obtain c where c: "f = ?k ` c" "c \ S" "finite c" using finite_subset_image[OF as(2,1)] by auto then obtain a b where ab: "a \ 0" "0 < b" "\x\convex hull c. b < inner a x" using separating_hyperplane_closed_0[OF convex_convex_hull, of c] using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2) using subset_hull[of convex, OF assms(1), symmetric, of c] by force then have "\x. norm x = 1 \ (\y\c. 0 \ inner y x)" apply (rule_tac x = "inverse(norm a) *\<^sub>R a" in exI) using hull_subset[of c convex] unfolding subset_eq and inner_scaleR by (auto simp: inner_commute del: ballE elim!: ballE) then show "frontier (cball 0 1) \ \f \ {}" unfolding c(1) frontier_cball sphere_def dist_norm by auto qed have "frontier (cball 0 1) \ (\(?k ` S)) \ {}" apply (rule compact_imp_fip) apply (rule compact_frontier[OF compact_cball]) using * closed_halfspace_ge by auto then obtain x where "norm x = 1" "\y\S. x\?k y" unfolding frontier_cball dist_norm sphere_def by auto then show ?thesis by (metis inner_commute mem_Collect_eq norm_eq_zero zero_neq_one) qed lemma separating_hyperplane_sets: fixes S T :: "'a::euclidean_space set" assumes "convex S" and "convex T" and "S \ {}" and "T \ {}" and "S \ T = {}" shows "\a b. a \ 0 \ (\x\S. inner a x \ b) \ (\x\T. inner a x \ b)" proof - from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]] obtain a where "a \ 0" "\x\{x - y |x y. x \ T \ y \ S}. 0 \ inner a x" using assms(3-5) by force then have *: "\x y. x \ T \ y \ S \ inner a y \ inner a x" by (force simp: inner_diff) then have bdd: "bdd_above (((\) a)`S)" using \T \ {}\ by (auto intro: bdd_aboveI2[OF *]) show ?thesis using \a\0\ by (intro exI[of _ a] exI[of _ "SUP x\S. a \ x"]) (auto intro!: cSUP_upper bdd cSUP_least \a \ 0\ \S \ {}\ *) qed subsection\<^marker>\tag unimportant\ \More convexity generalities\ lemma convex_closure [intro,simp]: fixes S :: "'a::real_normed_vector set" assumes "convex S" shows "convex (closure S)" apply (rule convexI) apply (unfold closure_sequential, elim exE) apply (rule_tac x="\n. u *\<^sub>R xa n + v *\<^sub>R xb n" in exI) apply (rule,rule) apply (rule convexD [OF assms]) apply (auto del: tendsto_const intro!: tendsto_intros) done lemma convex_interior [intro,simp]: fixes S :: "'a::real_normed_vector set" assumes "convex S" shows "convex (interior S)" unfolding convex_alt Ball_def mem_interior proof clarify fix x y u assume u: "0 \ u" "u \ (1::real)" fix e d assume ed: "ball x e \ S" "ball y d \ S" "0e>0. ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) e \ S" proof (intro exI conjI subsetI) fix z assume "z \ ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) (min d e)" then have "(1- u) *\<^sub>R (z - u *\<^sub>R (y - x)) + u *\<^sub>R (z + (1 - u) *\<^sub>R (y - x)) \ S" apply (rule_tac assms[unfolded convex_alt, rule_format]) using ed(1,2) and u unfolding subset_eq mem_ball Ball_def dist_norm apply (auto simp: algebra_simps) done then show "z \ S" using u by (auto simp: algebra_simps) qed(insert u ed(3-4), auto) qed lemma convex_hull_eq_empty[simp]: "convex hull S = {} \ S = {}" using hull_subset[of S convex] convex_hull_empty by auto subsection\<^marker>\tag unimportant\ \Convex set as intersection of halfspaces\ lemma convex_halfspace_intersection: fixes s :: "('a::euclidean_space) set" assumes "closed s" "convex s" shows "s = \{h. s \ h \ (\a b. h = {x. inner a x \ b})}" apply (rule set_eqI, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply (rule,rule,erule conjE) proof - fix x assume "\xa. s \ xa \ (\a b. xa = {x. inner a x \ b}) \ x \ xa" then have "\a b. s \ {x. inner a x \ b} \ x \ {x. inner a x \ b}" by blast then show "x \ s" apply (rule_tac ccontr) apply (drule separating_hyperplane_closed_point[OF assms(2,1)]) apply (erule exE)+ apply (erule_tac x="-a" in allE) apply (erule_tac x="-b" in allE, auto) done qed auto subsection\<^marker>\tag unimportant\ \Convexity of general and special intervals\ lemma is_interval_convex: fixes S :: "'a::euclidean_space set" assumes "is_interval S" shows "convex S" proof (rule convexI) fix x y and u v :: real assume as: "x \ S" "y \ S" "0 \ u" "0 \ v" "u + v = 1" then have *: "u = 1 - v" "1 - v \ 0" and **: "v = 1 - u" "1 - u \ 0" by auto { fix a b assume "\ b \ u * a + v * b" then have "u * a < (1 - v) * b" unfolding not_le using as(4) by (auto simp: field_simps) then have "a < b" unfolding * using as(4) *(2) apply (rule_tac mult_left_less_imp_less[of "1 - v"]) apply (auto simp: field_simps) done then have "a \ u * a + v * b" unfolding * using as(4) by (auto simp: field_simps intro!:mult_right_mono) } moreover { fix a b assume "\ u * a + v * b \ a" then have "v * b > (1 - u) * a" unfolding not_le using as(4) by (auto simp: field_simps) then have "a < b" unfolding * using as(4) apply (rule_tac mult_left_less_imp_less) apply (auto simp: field_simps) done then have "u * a + v * b \ b" unfolding ** using **(2) as(3) by (auto simp: field_simps intro!:mult_right_mono) } ultimately show "u *\<^sub>R x + v *\<^sub>R y \ S" apply - apply (rule assms[unfolded is_interval_def, rule_format, OF as(1,2)]) using as(3-) DIM_positive[where 'a='a] apply (auto simp: inner_simps) done qed lemma is_interval_connected: fixes S :: "'a::euclidean_space set" shows "is_interval S \ connected S" using is_interval_convex convex_connected by auto lemma convex_box [simp]: "convex (cbox a b)" "convex (box a (b::'a::euclidean_space))" apply (rule_tac[!] is_interval_convex)+ using is_interval_box is_interval_cbox apply auto done text\A non-singleton connected set is perfect (i.e. has no isolated points). \ lemma connected_imp_perfect: fixes a :: "'a::metric_space" assumes "connected S" "a \ S" and S: "\x. S \ {x}" shows "a islimpt S" proof - have False if "a \ T" "open T" "\y. \y \ S; y \ T\ \ y = a" for T proof - obtain e where "e > 0" and e: "cball a e \ T" using \open T\ \a \ T\ by (auto simp: open_contains_cball) have "openin (top_of_set S) {a}" unfolding openin_open using that \a \ S\ by blast moreover have "closedin (top_of_set S) {a}" by (simp add: assms) ultimately show "False" using \connected S\ connected_clopen S by blast qed then show ?thesis unfolding islimpt_def by blast qed lemma connected_imp_perfect_aff_dim: "\connected S; aff_dim S \ 0; a \ S\ \ a islimpt S" using aff_dim_sing connected_imp_perfect by blast subsection\<^marker>\tag unimportant\ \On \real\, \is_interval\, \convex\ and \connected\ are all equivalent\ lemma mem_is_interval_1_I: fixes a b c::real assumes "is_interval S" assumes "a \ S" "c \ S" assumes "a \ b" "b \ c" shows "b \ S" using assms is_interval_1 by blast lemma is_interval_connected_1: fixes s :: "real set" shows "is_interval s \ connected s" apply rule apply (rule is_interval_connected, assumption) unfolding is_interval_1 apply rule apply rule apply rule apply rule apply (erule conjE) apply (rule ccontr) proof - fix a b x assume as: "connected s" "a \ s" "b \ s" "a \ x" "x \ b" "x \ s" then have *: "a < x" "x < b" unfolding not_le [symmetric] by auto let ?halfl = "{.. s" with \x \ s\ have "x \ y" by auto then have "y \ ?halfr \ ?halfl" by auto } moreover have "a \ ?halfl" "b \ ?halfr" using * by auto then have "?halfl \ s \ {}" "?halfr \ s \ {}" using as(2-3) by auto ultimately show False apply (rule_tac notE[OF as(1)[unfolded connected_def]]) apply (rule_tac x = ?halfl in exI) apply (rule_tac x = ?halfr in exI, rule) apply (rule open_lessThan, rule) apply (rule open_greaterThan, auto) done qed lemma is_interval_convex_1: fixes s :: "real set" shows "is_interval s \ convex s" by (metis is_interval_convex convex_connected is_interval_connected_1) lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real by (metis connected_ball is_interval_connected_1) lemma connected_compact_interval_1: "connected S \ compact S \ (\a b. S = {a..b::real})" by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact) lemma connected_convex_1: fixes s :: "real set" shows "connected s \ convex s" by (metis is_interval_convex convex_connected is_interval_connected_1) lemma connected_convex_1_gen: fixes s :: "'a :: euclidean_space set" assumes "DIM('a) = 1" shows "connected s \ convex s" proof - obtain f:: "'a \ real" where linf: "linear f" and "inj f" using subspace_isomorphism[OF subspace_UNIV subspace_UNIV, where 'a='a and 'b=real] unfolding Euclidean_Space.dim_UNIV by (auto simp: assms) then have "f -` (f ` s) = s" by (simp add: inj_vimage_image_eq) then show ?thesis by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image) qed lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real by (simp add: is_interval_convex_1) lemma [simp]: fixes r s::real shows is_interval_io: "is_interval {..\tag unimportant\ \Another intermediate value theorem formulation\ lemma ivt_increasing_component_on_1: fixes f :: "real \ 'a::euclidean_space" assumes "a \ b" and "continuous_on {a..b} f" and "(f a)\k \ y" "y \ (f b)\k" shows "\x\{a..b}. (f x)\k = y" proof - have "f a \ f ` cbox a b" "f b \ f ` cbox a b" apply (rule_tac[!] imageI) using assms(1) apply auto done then show ?thesis using connected_ivt_component[of "f ` cbox a b" "f a" "f b" k y] by (simp add: connected_continuous_image assms) qed lemma ivt_increasing_component_1: fixes f :: "real \ 'a::euclidean_space" shows "a \ b \ \x\{a..b}. continuous (at x) f \ f a\k \ y \ y \ f b\k \ \x\{a..b}. (f x)\k = y" by (rule ivt_increasing_component_on_1) (auto simp: continuous_at_imp_continuous_on) lemma ivt_decreasing_component_on_1: fixes f :: "real \ 'a::euclidean_space" assumes "a \ b" and "continuous_on {a..b} f" and "(f b)\k \ y" and "y \ (f a)\k" shows "\x\{a..b}. (f x)\k = y" apply (subst neg_equal_iff_equal[symmetric]) using ivt_increasing_component_on_1[of a b "\x. - f x" k "- y"] using assms using continuous_on_minus apply auto done lemma ivt_decreasing_component_1: fixes f :: "real \ 'a::euclidean_space" shows "a \ b \ \x\{a..b}. continuous (at x) f \ f b\k \ y \ y \ f a\k \ \x\{a..b}. (f x)\k = y" by (rule ivt_decreasing_component_on_1) (auto simp: continuous_at_imp_continuous_on) subsection\<^marker>\tag unimportant\ \A bound within an interval\ lemma convex_hull_eq_real_cbox: fixes x y :: real assumes "x \ y" shows "convex hull {x, y} = cbox x y" proof (rule hull_unique) show "{x, y} \ cbox x y" using \x \ y\ by auto show "convex (cbox x y)" by (rule convex_box) next fix S assume "{x, y} \ S" and "convex S" then show "cbox x y \ S" unfolding is_interval_convex_1 [symmetric] is_interval_def Basis_real_def by - (clarify, simp (no_asm_use), fast) qed lemma unit_interval_convex_hull: "cbox (0::'a::euclidean_space) One = convex hull {x. \i\Basis. (x\i = 0) \ (x\i = 1)}" (is "?int = convex hull ?points") proof - have One[simp]: "\i. i \ Basis \ One \ i = 1" by (simp add: inner_sum_left sum.If_cases inner_Basis) have "?int = {x. \i\Basis. x \ i \ cbox 0 1}" by (auto simp: cbox_def) also have "\ = (\i\Basis. (\x. x *\<^sub>R i) ` cbox 0 1)" by (simp only: box_eq_set_sum_Basis) also have "\ = (\i\Basis. (\x. x *\<^sub>R i) ` (convex hull {0, 1}))" by (simp only: convex_hull_eq_real_cbox zero_le_one) also have "\ = (\i\Basis. convex hull ((\x. x *\<^sub>R i) ` {0, 1}))" by (simp add: convex_hull_linear_image) also have "\ = convex hull (\i\Basis. (\x. x *\<^sub>R i) ` {0, 1})" by (simp only: convex_hull_set_sum) also have "\ = convex hull {x. \i\Basis. x\i \ {0, 1}}" by (simp only: box_eq_set_sum_Basis) also have "convex hull {x. \i\Basis. x\i \ {0, 1}} = convex hull ?points" by simp finally show ?thesis . qed text \And this is a finite set of vertices.\ lemma unit_cube_convex_hull: obtains S :: "'a::euclidean_space set" where "finite S" and "cbox 0 (\Basis) = convex hull S" proof show "finite {x::'a. \i\Basis. x \ i = 0 \ x \ i = 1}" proof (rule finite_subset, clarify) show "finite ((\S. \i\Basis. (if i \ S then 1 else 0) *\<^sub>R i) ` Pow Basis)" using finite_Basis by blast fix x :: 'a assume as: "\i\Basis. x \ i = 0 \ x \ i = 1" show "x \ (\S. \i\Basis. (if i\S then 1 else 0) *\<^sub>R i) ` Pow Basis" apply (rule image_eqI[where x="{i. i\Basis \ x\i = 1}"]) using as apply (subst euclidean_eq_iff, auto) done qed show "cbox 0 One = convex hull {x. \i\Basis. x \ i = 0 \ x \ i = 1}" using unit_interval_convex_hull by blast qed text \Hence any cube (could do any nonempty interval).\ lemma cube_convex_hull: assumes "d > 0" obtains S :: "'a::euclidean_space set" where "finite S" and "cbox (x - (\i\Basis. d*\<^sub>Ri)) (x + (\i\Basis. d*\<^sub>Ri)) = convex hull S" proof - let ?d = "(\i\Basis. d *\<^sub>R i)::'a" have *: "cbox (x - ?d) (x + ?d) = (\y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 (\Basis)" proof (intro set_eqI iffI) fix y assume "y \ cbox (x - ?d) (x + ?d)" then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \ cbox 0 (\Basis)" using assms by (simp add: mem_box inner_simps) (simp add: field_simps) with \0 < d\ show "y \ (\y. x - sum ((*\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One" by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) next fix y assume "y \ (\y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 One" then obtain z where z: "z \ cbox 0 One" "y = x - ?d + (2*d) *\<^sub>R z" by auto then show "y \ cbox (x - ?d) (x + ?d)" using z assms by (auto simp: mem_box inner_simps) qed obtain S where "finite S" "cbox 0 (\Basis::'a) = convex hull S" using unit_cube_convex_hull by auto then show ?thesis by (rule_tac that[of "(\y. x - ?d + (2 * d) *\<^sub>R y)` S"]) (auto simp: convex_hull_affinity *) qed subsection\<^marker>\tag unimportant\\Representation of any interval as a finite convex hull\ lemma image_stretch_interval: "(\x. \k\Basis. (m k * (x\k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) = (if (cbox a b) = {} then {} else cbox (\k\Basis. (min (m k * (a\k)) (m k * (b\k))) *\<^sub>R k::'a) (\k\Basis. (max (m k * (a\k)) (m k * (b\k))) *\<^sub>R k))" proof cases assume *: "cbox a b \ {}" show ?thesis unfolding box_ne_empty if_not_P[OF *] apply (simp add: cbox_def image_Collect set_eq_iff euclidean_eq_iff[where 'a='a] ball_conj_distrib[symmetric]) apply (subst choice_Basis_iff[symmetric]) proof (intro allI ball_cong refl) fix x i :: 'a assume "i \ Basis" with * have a_le_b: "a \ i \ b \ i" unfolding box_ne_empty by auto show "(\xa. x \ i = m i * xa \ a \ i \ xa \ xa \ b \ i) \ min (m i * (a \ i)) (m i * (b \ i)) \ x \ i \ x \ i \ max (m i * (a \ i)) (m i * (b \ i))" proof (cases "m i = 0") case True with a_le_b show ?thesis by auto next case False then have *: "\a b. a = m i * b \ b = a / m i" by (auto simp: field_simps) from False have "min (m i * (a \ i)) (m i * (b \ i)) = (if 0 < m i then m i * (a \ i) else m i * (b \ i))" "max (m i * (a \ i)) (m i * (b \ i)) = (if 0 < m i then m i * (b \ i) else m i * (a \ i))" using a_le_b by (auto simp: min_def max_def mult_le_cancel_left) with False show ?thesis using a_le_b unfolding * by (auto simp: le_divide_eq divide_le_eq ac_simps) qed qed qed simp lemma interval_image_stretch_interval: "\u v. (\x. \k\Basis. (m k * (x\k))*\<^sub>R k) ` cbox a (b::'a::euclidean_space) = cbox u (v::'a::euclidean_space)" unfolding image_stretch_interval by auto lemma cbox_translation: "cbox (c + a) (c + b) = image (\x. c + x) (cbox a b)" using image_affinity_cbox [of 1 c a b] using box_ne_empty [of "a+c" "b+c"] box_ne_empty [of a b] by (auto simp: inner_left_distrib add.commute) lemma cbox_image_unit_interval: fixes a :: "'a::euclidean_space" assumes "cbox a b \ {}" shows "cbox a b = (+) a ` (\x. \k\Basis. ((b \ k - a \ k) * (x \ k)) *\<^sub>R k) ` cbox 0 One" using assms apply (simp add: box_ne_empty image_stretch_interval cbox_translation [symmetric]) apply (simp add: min_def max_def algebra_simps sum_subtractf euclidean_representation) done lemma closed_interval_as_convex_hull: fixes a :: "'a::euclidean_space" obtains S where "finite S" "cbox a b = convex hull S" proof (cases "cbox a b = {}") case True with convex_hull_empty that show ?thesis by blast next case False obtain S::"'a set" where "finite S" and eq: "cbox 0 One = convex hull S" by (blast intro: unit_cube_convex_hull) have lin: "linear (\x. \k\Basis. ((b \ k - a \ k) * (x \ k)) *\<^sub>R k)" by (rule linear_compose_sum) (auto simp: algebra_simps linearI) have "finite ((+) a ` (\x. \k\Basis. ((b \ k - a \ k) * (x \ k)) *\<^sub>R k) ` S)" by (rule finite_imageI \finite S\)+ then show ?thesis apply (rule that) apply (simp add: convex_hull_translation convex_hull_linear_image [OF lin, symmetric]) apply (simp add: eq [symmetric] cbox_image_unit_interval [OF False]) done qed subsection\<^marker>\tag unimportant\ \Bounded convex function on open set is continuous\ lemma convex_on_bounded_continuous: fixes S :: "('a::real_normed_vector) set" assumes "open S" and "convex_on S f" and "\x\S. \f x\ \ b" shows "continuous_on S f" apply (rule continuous_at_imp_continuous_on) unfolding continuous_at_real_range proof (rule,rule,rule) fix x and e :: real assume "x \ S" "e > 0" define B where "B = \b\ + 1" then have B: "0 < B""\x. x\S \ \f x\ \ B" using assms(3) by auto obtain k where "k > 0" and k: "cball x k \ S" using \x \ S\ assms(1) open_contains_cball_eq by blast show "\d>0. \x'. norm (x' - x) < d \ \f x' - f x\ < e" proof (intro exI conjI allI impI) fix y assume as: "norm (y - x) < min (k / 2) (e / (2 * B) * k)" show "\f y - f x\ < e" proof (cases "y = x") case False define t where "t = k / norm (y - x)" have "2 < t" "0k>0\ by (auto simp:field_simps) have "y \ S" apply (rule k[THEN subsetD]) unfolding mem_cball dist_norm apply (rule order_trans[of _ "2 * norm (x - y)"]) using as by (auto simp: field_simps norm_minus_commute) { define w where "w = x + t *\<^sub>R (y - x)" have "w \ S" using \k>0\ by (auto simp: dist_norm t_def w_def k[THEN subsetD]) have "(1 / t) *\<^sub>R x + - x + ((t - 1) / t) *\<^sub>R x = (1 / t - 1 + (t - 1) / t) *\<^sub>R x" by (auto simp: algebra_simps) also have "\ = 0" using \t > 0\ by (auto simp:field_simps) finally have w: "(1 / t) *\<^sub>R w + ((t - 1) / t) *\<^sub>R x = y" unfolding w_def using False and \t > 0\ by (auto simp: algebra_simps) have 2: "2 * B < e * t" unfolding t_def using \0 < e\ \0 < k\ \B > 0\ and as and False by (auto simp:field_simps) have "f y - f x \ (f w - f x) / t" using assms(2)[unfolded convex_on_def,rule_format,of w x "1/t" "(t - 1)/t", unfolded w] using \0 < t\ \2 < t\ and \x \ S\ \w \ S\ by (auto simp:field_simps) also have "... < e" using B(2)[OF \w\S\] and B(2)[OF \x\S\] 2 \t > 0\ by (auto simp: field_simps) finally have th1: "f y - f x < e" . } moreover { define w where "w = x - t *\<^sub>R (y - x)" have "w \ S" using \k > 0\ by (auto simp: dist_norm t_def w_def k[THEN subsetD]) have "(1 / (1 + t)) *\<^sub>R x + (t / (1 + t)) *\<^sub>R x = (1 / (1 + t) + t / (1 + t)) *\<^sub>R x" by (auto simp: algebra_simps) also have "\ = x" using \t > 0\ by (auto simp:field_simps) finally have w: "(1 / (1+t)) *\<^sub>R w + (t / (1 + t)) *\<^sub>R y = x" unfolding w_def using False and \t > 0\ by (auto simp: algebra_simps) have "2 * B < e * t" unfolding t_def using \0 < e\ \0 < k\ \B > 0\ and as and False by (auto simp:field_simps) then have *: "(f w - f y) / t < e" using B(2)[OF \w\S\] and B(2)[OF \y\S\] using \t > 0\ by (auto simp:field_simps) have "f x \ 1 / (1 + t) * f w + (t / (1 + t)) * f y" using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w] using \0 < t\ \2 < t\ and \y \ S\ \w \ S\ by (auto simp:field_simps) also have "\ = (f w + t * f y) / (1 + t)" using \t > 0\ by (simp add: add_divide_distrib) also have "\ < e + f y" using \t > 0\ * \e > 0\ by (auto simp: field_simps) finally have "f x - f y < e" by auto } ultimately show ?thesis by auto qed (insert \0, auto) qed (insert \0 \0 \0, auto simp: field_simps) qed subsection\<^marker>\tag unimportant\ \Upper bound on a ball implies upper and lower bounds\ lemma convex_bounds_lemma: fixes x :: "'a::real_normed_vector" assumes "convex_on (cball x e) f" and "\y \ cball x e. f y \ b" shows "\y \ cball x e. \f y\ \ b + 2 * \f x\" apply rule proof (cases "0 \ e") case True fix y assume y: "y \ cball x e" define z where "z = 2 *\<^sub>R x - y" have *: "x - (2 *\<^sub>R x - y) = y - x" by (simp add: scaleR_2) have z: "z \ cball x e" using y unfolding z_def mem_cball dist_norm * by (auto simp: norm_minus_commute) have "(1 / 2) *\<^sub>R y + (1 / 2) *\<^sub>R z = x" unfolding z_def by (auto simp: algebra_simps) then show "\f y\ \ b + 2 * \f x\" using assms(1)[unfolded convex_on_def,rule_format, OF y z, of "1/2" "1/2"] using assms(2)[rule_format,OF y] assms(2)[rule_format,OF z] by (auto simp:field_simps) next case False fix y assume "y \ cball x e" then have "dist x y < 0" using False unfolding mem_cball not_le by (auto simp del: dist_not_less_zero) then show "\f y\ \ b + 2 * \f x\" using zero_le_dist[of x y] by auto qed subsubsection\<^marker>\tag unimportant\ \Hence a convex function on an open set is continuous\ lemma real_of_nat_ge_one_iff: "1 \ real (n::nat) \ 1 \ n" by auto lemma convex_on_continuous: assumes "open (s::('a::euclidean_space) set)" "convex_on s f" shows "continuous_on s f" unfolding continuous_on_eq_continuous_at[OF assms(1)] proof note dimge1 = DIM_positive[where 'a='a] fix x assume "x \ s" then obtain e where e: "cball x e \ s" "e > 0" using assms(1) unfolding open_contains_cball by auto define d where "d = e / real DIM('a)" have "0 < d" unfolding d_def using \e > 0\ dimge1 by auto let ?d = "(\i\Basis. d *\<^sub>R i)::'a" obtain c where c: "finite c" and c1: "convex hull c \ cball x e" and c2: "cball x d \ convex hull c" proof define c where "c = (\i\Basis. (\a. a *\<^sub>R i) ` {x\i - d, x\i + d})" show "finite c" unfolding c_def by (simp add: finite_set_sum) have 1: "convex hull c = {a. \i\Basis. a \ i \ cbox (x \ i - d) (x \ i + d)}" unfolding box_eq_set_sum_Basis unfolding c_def convex_hull_set_sum apply (subst convex_hull_linear_image [symmetric]) apply (simp add: linear_iff scaleR_add_left) apply (rule sum.cong [OF refl]) apply (rule image_cong [OF _ refl]) apply (rule convex_hull_eq_real_cbox) apply (cut_tac \0 < d\, simp) done then have 2: "convex hull c = {a. \i\Basis. a \ i \ cball (x \ i) d}" by (simp add: dist_norm abs_le_iff algebra_simps) show "cball x d \ convex hull c" unfolding 2 by (clarsimp simp: dist_norm) (metis inner_commute inner_diff_right norm_bound_Basis_le) have e': "e = (\(i::'a)\Basis. d)" by (simp add: d_def DIM_positive) show "convex hull c \ cball x e" unfolding 2 apply clarsimp apply (subst euclidean_dist_l2) apply (rule order_trans [OF L2_set_le_sum]) apply (rule zero_le_dist) unfolding e' apply (rule sum_mono, simp) done qed define k where "k = Max (f ` c)" have "convex_on (convex hull c) f" apply(rule convex_on_subset[OF assms(2)]) apply(rule subset_trans[OF c1 e(1)]) done then have k: "\y\convex hull c. f y \ k" apply (rule_tac convex_on_convex_hull_bound, assumption) by (simp add: k_def c) have "e \ e * real DIM('a)" using e(2) real_of_nat_ge_one_iff by auto then have "d \ e" by (simp add: d_def field_split_simps) then have dsube: "cball x d \ cball x e" by (rule subset_cball) have conv: "convex_on (cball x d) f" using \convex_on (convex hull c) f\ c2 convex_on_subset by blast then have "\y\cball x d. \f y\ \ k + 2 * \f x\" by (rule convex_bounds_lemma) (use c2 k in blast) then have "continuous_on (ball x d) f" apply (rule_tac convex_on_bounded_continuous) apply (rule open_ball, rule convex_on_subset[OF conv]) apply (rule ball_subset_cball, force) done then show "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] using \d > 0\ by auto qed section \Line Segments\ subsection \Midpoint\ definition\<^marker>\tag important\ midpoint :: "'a::real_vector \ 'a \ 'a" where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" lemma midpoint_idem [simp]: "midpoint x x = x" unfolding midpoint_def by simp lemma midpoint_sym: "midpoint a b = midpoint b a" unfolding midpoint_def by (auto simp add: scaleR_right_distrib) lemma midpoint_eq_iff: "midpoint a b = c \ a + b = c + c" proof - have "midpoint a b = c \ scaleR 2 (midpoint a b) = scaleR 2 c" by simp then show ?thesis unfolding midpoint_def scaleR_2 [symmetric] by simp qed lemma fixes a::real assumes "a \ b" shows ge_midpoint_1: "a \ midpoint a b" and le_midpoint_1: "midpoint a b \ b" by (simp_all add: midpoint_def assms) lemma dist_midpoint: fixes a b :: "'a::real_normed_vector" shows "dist a (midpoint a b) = (dist a b) / 2" (is ?t1) "dist b (midpoint a b) = (dist a b) / 2" (is ?t2) "dist (midpoint a b) a = (dist a b) / 2" (is ?t3) "dist (midpoint a b) b = (dist a b) / 2" (is ?t4) proof - have *: "\x y::'a. 2 *\<^sub>R x = - y \ norm x = (norm y) / 2" unfolding equation_minus_iff by auto have **: "\x y::'a. 2 *\<^sub>R x = y \ norm x = (norm y) / 2" by auto note scaleR_right_distrib [simp] show ?t1 unfolding midpoint_def dist_norm apply (rule **) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done show ?t2 unfolding midpoint_def dist_norm apply (rule *) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done show ?t3 unfolding midpoint_def dist_norm apply (rule *) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done show ?t4 unfolding midpoint_def dist_norm apply (rule **) apply (simp add: scaleR_right_diff_distrib) apply (simp add: scaleR_2) done qed lemma midpoint_eq_endpoint [simp]: "midpoint a b = a \ a = b" "midpoint a b = b \ a = b" unfolding midpoint_eq_iff by auto lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b" using midpoint_eq_iff by metis lemma midpoint_linear_image: "linear f \ midpoint(f a)(f b) = f(midpoint a b)" by (simp add: linear_iff midpoint_def) subsection \Line segments\ definition\<^marker>\tag important\ closed_segment :: "'a::real_vector \ 'a \ 'a set" where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \ u \ u \ 1}" definition\<^marker>\tag important\ open_segment :: "'a::real_vector \ 'a \ 'a set" where "open_segment a b \ closed_segment a b - {a,b}" lemmas segment = open_segment_def closed_segment_def lemma in_segment: "x \ closed_segment a b \ (\u. 0 \ u \ u \ 1 \ x = (1 - u) *\<^sub>R a + u *\<^sub>R b)" "x \ open_segment a b \ a \ b \ (\u. 0 < u \ u < 1 \ x = (1 - u) *\<^sub>R a + u *\<^sub>R b)" using less_eq_real_def by (auto simp: segment algebra_simps) lemma closed_segmentI: "u \ {0..1} \ z = (1 - u) *\<^sub>R a + u *\<^sub>R b \ z \ closed_segment a b" by (auto simp: closed_segment_def) lemma closed_segment_linear_image: "closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f" proof - interpret linear f by fact show ?thesis by (force simp add: in_segment add scale) qed lemma open_segment_linear_image: "\linear f; inj f\ \ open_segment (f a) (f b) = f ` (open_segment a b)" by (force simp: open_segment_def closed_segment_linear_image inj_on_def) lemma closed_segment_translation: "closed_segment (c + a) (c + b) = image (\x. c + x) (closed_segment a b)" apply safe apply (rule_tac x="x-c" in image_eqI) apply (auto simp: in_segment algebra_simps) done lemma open_segment_translation: "open_segment (c + a) (c + b) = image (\x. c + x) (open_segment a b)" by (simp add: open_segment_def closed_segment_translation translation_diff) lemma closed_segment_of_real: "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y" apply (auto simp: image_iff in_segment scaleR_conv_of_real) apply (rule_tac x="(1-u)*x + u*y" in bexI) apply (auto simp: in_segment) done lemma open_segment_of_real: "open_segment (of_real x) (of_real y) = of_real ` open_segment x y" apply (auto simp: image_iff in_segment scaleR_conv_of_real) apply (rule_tac x="(1-u)*x + u*y" in bexI) apply (auto simp: in_segment) done lemma closed_segment_Reals: "\x \ Reals; y \ Reals\ \ closed_segment x y = of_real ` closed_segment (Re x) (Re y)" by (metis closed_segment_of_real of_real_Re) lemma open_segment_Reals: "\x \ Reals; y \ Reals\ \ open_segment x y = of_real ` open_segment (Re x) (Re y)" by (metis open_segment_of_real of_real_Re) lemma open_segment_PairD: "(x, x') \ open_segment (a, a') (b, b') \ (x \ open_segment a b \ a = b) \ (x' \ open_segment a' b' \ a' = b')" by (auto simp: in_segment) lemma closed_segment_PairD: "(x, x') \ closed_segment (a, a') (b, b') \ x \ closed_segment a b \ x' \ closed_segment a' b'" by (auto simp: closed_segment_def) lemma closed_segment_translation_eq [simp]: "d + x \ closed_segment (d + a) (d + b) \ x \ closed_segment a b" proof - have *: "\d x a b. x \ closed_segment a b \ d + x \ closed_segment (d + a) (d + b)" apply (simp add: closed_segment_def) apply (erule ex_forward) apply (simp add: algebra_simps) done show ?thesis using * [where d = "-d"] * by (fastforce simp add:) qed lemma open_segment_translation_eq [simp]: "d + x \ open_segment (d + a) (d + b) \ x \ open_segment a b" by (simp add: open_segment_def) lemma of_real_closed_segment [simp]: "of_real x \ closed_segment (of_real a) (of_real b) \ x \ closed_segment a b" apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward) using of_real_eq_iff by fastforce lemma of_real_open_segment [simp]: "of_real x \ open_segment (of_real a) (of_real b) \ x \ open_segment a b" apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE) using of_real_eq_iff by fastforce lemma convex_contains_segment: "convex S \ (\a\S. \b\S. closed_segment a b \ S)" unfolding convex_alt closed_segment_def by auto lemma closed_segment_in_Reals: "\x \ closed_segment a b; a \ Reals; b \ Reals\ \ x \ Reals" by (meson subsetD convex_Reals convex_contains_segment) lemma open_segment_in_Reals: "\x \ open_segment a b; a \ Reals; b \ Reals\ \ x \ Reals" by (metis Diff_iff closed_segment_in_Reals open_segment_def) lemma closed_segment_subset: "\x \ S; y \ S; convex S\ \ closed_segment x y \ S" by (simp add: convex_contains_segment) lemma closed_segment_subset_convex_hull: "\x \ convex hull S; y \ convex hull S\ \ closed_segment x y \ convex hull S" using convex_contains_segment by blast lemma segment_convex_hull: "closed_segment a b = convex hull {a,b}" proof - have *: "\x. {x} \ {}" by auto show ?thesis unfolding segment convex_hull_insert[OF *] convex_hull_singleton by (safe; rule_tac x="1 - u" in exI; force) qed lemma open_closed_segment: "u \ open_segment w z \ u \ closed_segment w z" by (auto simp add: closed_segment_def open_segment_def) lemma segment_open_subset_closed: "open_segment a b \ closed_segment a b" by (auto simp: closed_segment_def open_segment_def) lemma bounded_closed_segment: fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)" by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded) lemma bounded_open_segment: fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)" by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed]) lemmas bounded_segment = bounded_closed_segment open_closed_segment lemma ends_in_segment [iff]: "a \ closed_segment a b" "b \ closed_segment a b" 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" shows "norm (y - x) \ norm (y - a) \ norm (y - x) \ norm (y - b)" proof - obtain z where "z \ {a, b}" "norm (x - y) \ norm (z - y)" using simplex_furthest_le[of "{a, b}" y] using assms[unfolded segment_convex_hull] by auto then show ?thesis by (auto simp add:norm_minus_commute) qed lemma closed_segment_commute: "closed_segment a b = closed_segment b a" proof - have "{a, b} = {b, a}" by auto thus ?thesis by (simp add: segment_convex_hull) qed lemma segment_bound1: assumes "x \ closed_segment a b" shows "norm (x - a) \ norm (b - a)" proof - obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \ u" "u \ 1" using assms by (auto simp add: closed_segment_def) then show "norm (x - a) \ norm (b - a)" apply clarify apply (auto simp: algebra_simps) apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le) done qed lemma segment_bound: assumes "x \ closed_segment a b" shows "norm (x - a) \ norm (b - a)" "norm (x - b) \ norm (b - a)" apply (simp add: assms segment_bound1) by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1) lemma open_segment_commute: "open_segment a b = open_segment b a" proof - have "{a, b} = {b, a}" by auto thus ?thesis by (simp add: closed_segment_commute open_segment_def) qed lemma closed_segment_idem [simp]: "closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps) lemma open_segment_idem [simp]: "open_segment a a = {}" by (simp add: open_segment_def) lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \ {a,b}" using open_segment_def by auto lemma convex_contains_open_segment: "convex s \ (\a\s. \b\s. open_segment a b \ s)" by (simp add: convex_contains_segment closed_segment_eq_open) lemma closed_segment_eq_real_ivl: fixes a b::real shows "closed_segment a b = (if a \ b then {a .. b} else {b .. a})" proof - have "b \ a \ closed_segment b a = {b .. a}" and "a \ b \ closed_segment a b = {a .. b}" by (auto simp: convex_hull_eq_real_cbox segment_convex_hull) thus ?thesis by (auto simp: closed_segment_commute) qed lemma open_segment_eq_real_ivl: fixes a b::real shows "open_segment a b = (if a \ b then {a<..x. (v - u) * x + u) ` {0..1}" by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl) lemma dist_in_closed_segment: fixes a :: "'a :: euclidean_space" assumes "x \ closed_segment a b" shows "dist x a \ dist a b \ dist x b \ dist a b" proof (intro conjI) obtain u where u: "0 \ u" "u \ 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" using assms by (force simp: in_segment algebra_simps) have "dist x a = u * dist a b" apply (simp add: dist_norm algebra_simps x) by (metis \0 \ u\ abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib) also have "... \ dist a b" by (simp add: mult_left_le_one_le u) finally show "dist x a \ dist a b" . have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)" by (simp add: dist_norm algebra_simps x) also have "... = (1-u) * dist a b" proof - have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)" using \u \ 1\ by force then show ?thesis by (simp add: dist_norm real_vector.scale_right_diff_distrib) qed also have "... \ dist a b" by (simp add: mult_left_le_one_le u) finally show "dist x b \ dist a b" . qed lemma dist_in_open_segment: fixes a :: "'a :: euclidean_space" assumes "x \ open_segment a b" shows "dist x a < dist a b \ dist x b < dist a b" proof (intro conjI) obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" using assms by (force simp: in_segment algebra_simps) have "dist x a = u * dist a b" apply (simp add: dist_norm algebra_simps x) by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \0 < u\) also have *: "... < dist a b" by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 \u < 1\) finally show "dist x a < dist a b" . have ab_ne0: "dist a b \ 0" using * by fastforce have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)" by (simp add: dist_norm algebra_simps x) also have "... = (1-u) * dist a b" proof - have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)" using \u < 1\ by force then show ?thesis by (simp add: dist_norm real_vector.scale_right_diff_distrib) qed also have "... < dist a b" using ab_ne0 \0 < u\ by simp finally show "dist x b < dist a b" . qed lemma dist_decreases_open_segment_0: fixes x :: "'a :: euclidean_space" assumes "x \ open_segment 0 b" shows "dist c x < dist c 0 \ dist c x < dist c b" proof (rule ccontr, clarsimp simp: not_less) obtain u where u: "0 \ b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b" using assms by (auto simp: in_segment) have xb: "x \ b < b \ b" using u x by auto assume "norm c \ dist c x" then have "c \ c \ (c - x) \ (c - x)" by (simp add: dist_norm norm_le) moreover have "0 < x \ b" using u x by auto ultimately have less: "c \ b < x \ b" by (simp add: x algebra_simps inner_commute u) assume "dist c b \ dist c x" then have "(c - b) \ (c - b) \ (c - x) \ (c - x)" by (simp add: dist_norm norm_le) then have "(b \ b) * (1 - u*u) \ 2 * (b \ c) * (1-u)" by (simp add: x algebra_simps inner_commute) then have "(1+u) * (b \ b) * (1-u) \ 2 * (b \ c) * (1-u)" by (simp add: algebra_simps) then have "(1+u) * (b \ b) \ 2 * (b \ c)" using \u < 1\ by auto with xb have "c \ b \ x \ b" by (auto simp: x algebra_simps inner_commute) with less show False by auto qed proposition dist_decreases_open_segment: fixes a :: "'a :: euclidean_space" assumes "x \ open_segment a b" shows "dist c x < dist c a \ dist c x < dist c b" proof - have *: "x - a \ open_segment 0 (b - a)" using assms by (metis diff_self open_segment_translation_eq uminus_add_conv_diff) show ?thesis using dist_decreases_open_segment_0 [OF *, of "c-a"] assms by (simp add: dist_norm) qed corollary open_segment_furthest_le: fixes a b x y :: "'a::euclidean_space" assumes "x \ open_segment a b" shows "norm (y - x) < norm (y - a) \ norm (y - x) < norm (y - b)" by (metis assms dist_decreases_open_segment dist_norm) corollary dist_decreases_closed_segment: fixes a :: "'a :: euclidean_space" assumes "x \ closed_segment a b" shows "dist c x \ dist c a \ dist c x \ dist c b" apply (cases "x \ open_segment a b") using dist_decreases_open_segment less_eq_real_def apply blast by (metis DiffI assms empty_iff insertE open_segment_def order_refl) lemma convex_intermediate_ball: fixes a :: "'a :: euclidean_space" shows "\ball a r \ T; T \ cball a r\ \ convex T" apply (simp add: convex_contains_open_segment, clarify) by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment) lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \ closed_segment a b" apply (clarsimp simp: midpoint_def in_segment) apply (rule_tac x="(1 + u) / 2" in exI) apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib) by (metis field_sum_of_halves scaleR_left.add) lemma notin_segment_midpoint: fixes a :: "'a :: euclidean_space" shows "a \ b \ a \ closed_segment (midpoint a b) b" by (auto simp: dist_midpoint dest!: dist_in_closed_segment) lemma segment_to_closest_point: fixes S :: "'a :: euclidean_space set" shows "\closed S; S \ {}\ \ open_segment a (closest_point S a) \ S = {}" apply (subst disjoint_iff_not_equal) apply (clarify dest!: dist_in_open_segment) by (metis closest_point_le dist_commute le_less_trans less_irrefl) lemma segment_to_point_exists: fixes S :: "'a :: euclidean_space set" assumes "closed S" "S \ {}" obtains b where "b \ S" "open_segment a b \ S = {}" by (metis assms segment_to_closest_point closest_point_exists that) subsubsection\More lemmas, especially for working with the underlying formula\ lemma segment_eq_compose: fixes a :: "'a :: real_vector" shows "(\u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\x. a + x) o (\u. u *\<^sub>R (b - a))" by (simp add: o_def algebra_simps) lemma segment_degen_1: fixes a :: "'a :: real_vector" shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \ a=b \ u=1" proof - { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b" then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b" by (simp add: algebra_simps) then have "a=b \ u=1" by simp } then show ?thesis by (auto simp: algebra_simps) qed lemma segment_degen_0: fixes a :: "'a :: real_vector" shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \ a=b \ u=0" using segment_degen_1 [of "1-u" b a] by (auto simp: algebra_simps) lemma add_scaleR_degen: fixes a b ::"'a::real_vector" assumes "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)" "u \ v" shows "a=b" by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms) lemma closed_segment_image_interval: "closed_segment a b = (\u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}" by (auto simp: set_eq_iff image_iff closed_segment_def) lemma open_segment_image_interval: "open_segment a b = (if a=b then {} else (\u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})" by (auto simp: open_segment_def closed_segment_def segment_degen_0 segment_degen_1) lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval lemma open_segment_bound1: assumes "x \ open_segment a b" shows "norm (x - a) < norm (b - a)" proof - obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \ b" using assms by (auto simp add: open_segment_image_interval split: if_split_asm) then show "norm (x - a) < norm (b - a)" apply clarify apply (auto simp: algebra_simps) apply (simp add: scaleR_diff_right [symmetric]) done qed lemma compact_segment [simp]: fixes a :: "'a::real_normed_vector" shows "compact (closed_segment a b)" by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros) lemma closed_segment [simp]: fixes a :: "'a::real_normed_vector" shows "closed (closed_segment a b)" by (simp add: compact_imp_closed) lemma closure_closed_segment [simp]: fixes a :: "'a::real_normed_vector" shows "closure(closed_segment a b) = closed_segment a b" by simp lemma open_segment_bound: assumes "x \ open_segment a b" shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)" apply (simp add: assms open_segment_bound1) by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute) lemma closure_open_segment [simp]: "closure (open_segment a b) = (if a = b then {} else closed_segment a b)" for a :: "'a::euclidean_space" proof (cases "a = b") case True then show ?thesis by simp next case False have "closure ((\u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\u. u *\<^sub>R (b - a)) ` closure {0<..<1}" apply (rule closure_injective_linear_image [symmetric]) apply (use False in \auto intro!: injI\) done then have "closure ((\u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) = (\x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}" using closure_translation [of a "((\x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"] by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image) then show ?thesis by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan) qed lemma closed_open_segment_iff [simp]: fixes a :: "'a::euclidean_space" shows "closed(open_segment a b) \ a = b" by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2)) lemma compact_open_segment_iff [simp]: fixes a :: "'a::euclidean_space" shows "compact(open_segment a b) \ a = b" by (simp add: bounded_open_segment compact_eq_bounded_closed) lemma convex_closed_segment [iff]: "convex (closed_segment a b)" unfolding segment_convex_hull by(rule convex_convex_hull) lemma convex_open_segment [iff]: "convex (open_segment a b)" proof - have "convex ((\u. u *\<^sub>R (b - a)) ` {0<..<1})" by (rule convex_linear_image) auto then have "convex ((+) a ` (\u. u *\<^sub>R (b - a)) ` {0<..<1})" by (rule convex_translation) then show ?thesis by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right) qed lemmas convex_segment = convex_closed_segment convex_open_segment lemma connected_segment [iff]: fixes x :: "'a :: real_normed_vector" shows "connected (closed_segment x y)" by (simp add: convex_connected) lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real by (auto simp: is_interval_convex_1) lemma IVT'_closed_segment_real: fixes f :: "real \ real" assumes "y \ closed_segment (f a) (f b)" assumes "continuous_on (closed_segment a b) f" shows "\x \ closed_segment a b. f x = y" using IVT'[of f a y b] IVT'[of "-f" a "-y" b] IVT'[of f b y a] IVT'[of "-f" b "-y" a] assms by (cases "a \ b"; cases "f b \ f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus) end