src/HOL/Analysis/Convex_Euclidean_Space.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 months ago) changeset 69981 3dced198b9ec parent 69922 4a9167f377b0 child 70097 4005298550a6 permissions -rw-r--r--
more strict AFP properties;
```     1 (* Title:      HOL/Analysis/Convex_Euclidean_Space.thy
```
```     2    Author:     L C Paulson, University of Cambridge
```
```     3    Author:     Robert Himmelmann, TU Muenchen
```
```     4    Author:     Bogdan Grechuk, University of Edinburgh
```
```     5    Author:     Armin Heller, TU Muenchen
```
```     6    Author:     Johannes Hoelzl, TU Muenchen
```
```     7 *)
```
```     8
```
```     9 section \<open>Convex Sets and Functions on (Normed) Euclidean Spaces\<close>
```
```    10
```
```    11 theory Convex_Euclidean_Space
```
```    12 imports
```
```    13   Convex
```
```    14   Topology_Euclidean_Space
```
```    15 begin
```
```    16
```
```    17 subsection%unimportant \<open>Topological Properties of Convex Sets and Functions\<close>
```
```    18
```
```    19 lemma convex_supp_sum:
```
```    20   assumes "convex S" and 1: "supp_sum u I = 1"
```
```    21       and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
```
```    22     shows "supp_sum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
```
```    23 proof -
```
```    24   have fin: "finite {i \<in> I. u i \<noteq> 0}"
```
```    25     using 1 sum.infinite by (force simp: supp_sum_def support_on_def)
```
```    26   then have eq: "supp_sum (\<lambda>i. u i *\<^sub>R f i) I = sum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
```
```    27     by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def)
```
```    28   show ?thesis
```
```    29     apply (simp add: eq)
```
```    30     apply (rule convex_sum [OF fin \<open>convex S\<close>])
```
```    31     using 1 assms apply (auto simp: supp_sum_def support_on_def)
```
```    32     done
```
```    33 qed
```
```    34
```
```    35 lemma closure_bounded_linear_image_subset:
```
```    36   assumes f: "bounded_linear f"
```
```    37   shows "f ` closure S \<subseteq> closure (f ` S)"
```
```    38   using linear_continuous_on [OF f] closed_closure closure_subset
```
```    39   by (rule image_closure_subset)
```
```    40
```
```    41 lemma closure_linear_image_subset:
```
```    42   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::real_normed_vector"
```
```    43   assumes "linear f"
```
```    44   shows "f ` (closure S) \<subseteq> closure (f ` S)"
```
```    45   using assms unfolding linear_conv_bounded_linear
```
```    46   by (rule closure_bounded_linear_image_subset)
```
```    47
```
```    48 lemma closed_injective_linear_image:
```
```    49     fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```    50     assumes S: "closed S" and f: "linear f" "inj f"
```
```    51     shows "closed (f ` S)"
```
```    52 proof -
```
```    53   obtain g where g: "linear g" "g \<circ> f = id"
```
```    54     using linear_injective_left_inverse [OF f] by blast
```
```    55   then have confg: "continuous_on (range f) g"
```
```    56     using linear_continuous_on linear_conv_bounded_linear by blast
```
```    57   have [simp]: "g ` f ` S = S"
```
```    58     using g by (simp add: image_comp)
```
```    59   have cgf: "closed (g ` f ` S)"
```
```    60     by (simp add: \<open>g \<circ> f = id\<close> S image_comp)
```
```    61   have [simp]: "(range f \<inter> g -` S) = f ` S"
```
```    62     using g unfolding o_def id_def image_def by auto metis+
```
```    63   show ?thesis
```
```    64   proof (rule closedin_closed_trans [of "range f"])
```
```    65     show "closedin (top_of_set (range f)) (f ` S)"
```
```    66       using continuous_closedin_preimage [OF confg cgf] by simp
```
```    67     show "closed (range f)"
```
```    68       apply (rule closed_injective_image_subspace)
```
```    69       using f apply (auto simp: linear_linear linear_injective_0)
```
```    70       done
```
```    71   qed
```
```    72 qed
```
```    73
```
```    74 lemma closed_injective_linear_image_eq:
```
```    75     fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```    76     assumes f: "linear f" "inj f"
```
```    77       shows "(closed(image f s) \<longleftrightarrow> closed s)"
```
```    78   by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff)
```
```    79
```
```    80 lemma closure_injective_linear_image:
```
```    81     fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```    82     shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
```
```    83   apply (rule subset_antisym)
```
```    84   apply (simp add: closure_linear_image_subset)
```
```    85   by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono)
```
```    86
```
```    87 lemma closure_bounded_linear_image:
```
```    88     fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
```
```    89     shows "\<lbrakk>linear f; bounded S\<rbrakk> \<Longrightarrow> f ` (closure S) = closure (f ` S)"
```
```    90   apply (rule subset_antisym, simp add: closure_linear_image_subset)
```
```    91   apply (rule closure_minimal, simp add: closure_subset image_mono)
```
```    92   by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear)
```
```    93
```
```    94 lemma closure_scaleR:
```
```    95   fixes S :: "'a::real_normed_vector set"
```
```    96   shows "((*\<^sub>R) c) ` (closure S) = closure (((*\<^sub>R) c) ` S)"
```
```    97 proof
```
```    98   show "((*\<^sub>R) c) ` (closure S) \<subseteq> closure (((*\<^sub>R) c) ` S)"
```
```    99     using bounded_linear_scaleR_right
```
```   100     by (rule closure_bounded_linear_image_subset)
```
```   101   show "closure (((*\<^sub>R) c) ` S) \<subseteq> ((*\<^sub>R) c) ` (closure S)"
```
```   102     by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
```
```   103 qed
```
```   104
```
```   105 lemma sphere_eq_empty [simp]:
```
```   106   fixes a :: "'a::{real_normed_vector, perfect_space}"
```
```   107   shows "sphere a r = {} \<longleftrightarrow> r < 0"
```
```   108 by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist)
```
```   109
```
```   110 lemma cone_closure:
```
```   111   fixes S :: "'a::real_normed_vector set"
```
```   112   assumes "cone S"
```
```   113   shows "cone (closure S)"
```
```   114 proof (cases "S = {}")
```
```   115   case True
```
```   116   then show ?thesis by auto
```
```   117 next
```
```   118   case False
```
```   119   then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` S = S)"
```
```   120     using cone_iff[of S] assms by auto
```
```   121   then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> (*\<^sub>R) c ` closure S = closure S)"
```
```   122     using closure_subset by (auto simp: closure_scaleR)
```
```   123   then show ?thesis
```
```   124     using False cone_iff[of "closure S"] by auto
```
```   125 qed
```
```   126
```
```   127 corollary component_complement_connected:
```
```   128   fixes S :: "'a::real_normed_vector set"
```
```   129   assumes "connected S" "C \<in> components (-S)"
```
```   130   shows "connected(-C)"
```
```   131   using component_diff_connected [of S UNIV] assms
```
```   132   by (auto simp: Compl_eq_Diff_UNIV)
```
```   133
```
```   134 proposition clopen:
```
```   135   fixes S :: "'a :: real_normed_vector set"
```
```   136   shows "closed S \<and> open S \<longleftrightarrow> S = {} \<or> S = UNIV"
```
```   137     by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format])
```
```   138
```
```   139 corollary compact_open:
```
```   140   fixes S :: "'a :: euclidean_space set"
```
```   141   shows "compact S \<and> open S \<longleftrightarrow> S = {}"
```
```   142   by (auto simp: compact_eq_bounded_closed clopen)
```
```   143
```
```   144 corollary finite_imp_not_open:
```
```   145     fixes S :: "'a::{real_normed_vector, perfect_space} set"
```
```   146     shows "\<lbrakk>finite S; open S\<rbrakk> \<Longrightarrow> S={}"
```
```   147   using clopen [of S] finite_imp_closed not_bounded_UNIV by blast
```
```   148
```
```   149 corollary empty_interior_finite:
```
```   150     fixes S :: "'a::{real_normed_vector, perfect_space} set"
```
```   151     shows "finite S \<Longrightarrow> interior S = {}"
```
```   152   by (metis interior_subset finite_subset open_interior [of S] finite_imp_not_open)
```
```   153
```
```   154 text \<open>Balls, being convex, are connected.\<close>
```
```   155
```
```   156 lemma convex_local_global_minimum:
```
```   157   fixes s :: "'a::real_normed_vector set"
```
```   158   assumes "e > 0"
```
```   159     and "convex_on s f"
```
```   160     and "ball x e \<subseteq> s"
```
```   161     and "\<forall>y\<in>ball x e. f x \<le> f y"
```
```   162   shows "\<forall>y\<in>s. f x \<le> f y"
```
```   163 proof (rule ccontr)
```
```   164   have "x \<in> s" using assms(1,3) by auto
```
```   165   assume "\<not> ?thesis"
```
```   166   then obtain y where "y\<in>s" and y: "f x > f y" by auto
```
```   167   then have xy: "0 < dist x y"  by auto
```
```   168   then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
```
```   169     using field_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
```
```   170   then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
```
```   171     using \<open>x\<in>s\<close> \<open>y\<in>s\<close>
```
```   172     using assms(2)[unfolded convex_on_def,
```
```   173       THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]]
```
```   174     by auto
```
```   175   moreover
```
```   176   have *: "x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)"
```
```   177     by (simp add: algebra_simps)
```
```   178   have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> ball x e"
```
```   179     unfolding mem_ball dist_norm
```
```   180     unfolding * and norm_scaleR and abs_of_pos[OF \<open>0<u\<close>]
```
```   181     unfolding dist_norm[symmetric]
```
```   182     using u
```
```   183     unfolding pos_less_divide_eq[OF xy]
```
```   184     by auto
```
```   185   then have "f x \<le> f ((1 - u) *\<^sub>R x + u *\<^sub>R y)"
```
```   186     using assms(4) by auto
```
```   187   ultimately show False
```
```   188     using mult_strict_left_mono[OF y \<open>u>0\<close>]
```
```   189     unfolding left_diff_distrib
```
```   190     by auto
```
```   191 qed
```
```   192
```
```   193 lemma convex_ball [iff]:
```
```   194   fixes x :: "'a::real_normed_vector"
```
```   195   shows "convex (ball x e)"
```
```   196 proof (auto simp: convex_def)
```
```   197   fix y z
```
```   198   assume yz: "dist x y < e" "dist x z < e"
```
```   199   fix u v :: real
```
```   200   assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
```
```   201   have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
```
```   202     using uv yz
```
```   203     using convex_on_dist [of "ball x e" x, unfolded convex_on_def,
```
```   204       THEN bspec[where x=y], THEN bspec[where x=z]]
```
```   205     by auto
```
```   206   then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e"
```
```   207     using convex_bound_lt[OF yz uv] by auto
```
```   208 qed
```
```   209
```
```   210 lemma convex_cball [iff]:
```
```   211   fixes x :: "'a::real_normed_vector"
```
```   212   shows "convex (cball x e)"
```
```   213 proof -
```
```   214   {
```
```   215     fix y z
```
```   216     assume yz: "dist x y \<le> e" "dist x z \<le> e"
```
```   217     fix u v :: real
```
```   218     assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
```
```   219     have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
```
```   220       using uv yz
```
```   221       using convex_on_dist [of "cball x e" x, unfolded convex_on_def,
```
```   222         THEN bspec[where x=y], THEN bspec[where x=z]]
```
```   223       by auto
```
```   224     then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e"
```
```   225       using convex_bound_le[OF yz uv] by auto
```
```   226   }
```
```   227   then show ?thesis by (auto simp: convex_def Ball_def)
```
```   228 qed
```
```   229
```
```   230 lemma connected_ball [iff]:
```
```   231   fixes x :: "'a::real_normed_vector"
```
```   232   shows "connected (ball x e)"
```
```   233   using convex_connected convex_ball by auto
```
```   234
```
```   235 lemma connected_cball [iff]:
```
```   236   fixes x :: "'a::real_normed_vector"
```
```   237   shows "connected (cball x e)"
```
```   238   using convex_connected convex_cball by auto
```
```   239
```
```   240
```
```   241 lemma bounded_convex_hull:
```
```   242   fixes s :: "'a::real_normed_vector set"
```
```   243   assumes "bounded s"
```
```   244   shows "bounded (convex hull s)"
```
```   245 proof -
```
```   246   from assms obtain B where B: "\<forall>x\<in>s. norm x \<le> B"
```
```   247     unfolding bounded_iff by auto
```
```   248   show ?thesis
```
```   249     apply (rule bounded_subset[OF bounded_cball, of _ 0 B])
```
```   250     unfolding subset_hull[of convex, OF convex_cball]
```
```   251     unfolding subset_eq mem_cball dist_norm using B
```
```   252     apply auto
```
```   253     done
```
```   254 qed
```
```   255
```
```   256 lemma finite_imp_bounded_convex_hull:
```
```   257   fixes s :: "'a::real_normed_vector set"
```
```   258   shows "finite s \<Longrightarrow> bounded (convex hull s)"
```
```   259   using bounded_convex_hull finite_imp_bounded
```
```   260   by auto
```
```   261
```
```   262 lemma aff_dim_cball:
```
```   263   fixes a :: "'n::euclidean_space"
```
```   264   assumes "e > 0"
```
```   265   shows "aff_dim (cball a e) = int (DIM('n))"
```
```   266 proof -
```
```   267   have "(\<lambda>x. a + x) ` (cball 0 e) \<subseteq> cball a e"
```
```   268     unfolding cball_def dist_norm by auto
```
```   269   then have "aff_dim (cball (0 :: 'n::euclidean_space) e) \<le> aff_dim (cball a e)"
```
```   270     using aff_dim_translation_eq[of a "cball 0 e"]
```
```   271           aff_dim_subset[of "(+) a ` cball 0 e" "cball a e"]
```
```   272     by auto
```
```   273   moreover have "aff_dim (cball (0 :: 'n::euclidean_space) e) = int (DIM('n))"
```
```   274     using hull_inc[of "(0 :: 'n::euclidean_space)" "cball 0 e"]
```
```   275       centre_in_cball[of "(0 :: 'n::euclidean_space)"] assms
```
```   276     by (simp add: dim_cball[of e] aff_dim_zero[of "cball 0 e"])
```
```   277   ultimately show ?thesis
```
```   278     using aff_dim_le_DIM[of "cball a e"] by auto
```
```   279 qed
```
```   280
```
```   281 lemma aff_dim_open:
```
```   282   fixes S :: "'n::euclidean_space set"
```
```   283   assumes "open S"
```
```   284     and "S \<noteq> {}"
```
```   285   shows "aff_dim S = int (DIM('n))"
```
```   286 proof -
```
```   287   obtain x where "x \<in> S"
```
```   288     using assms by auto
```
```   289   then obtain e where e: "e > 0" "cball x e \<subseteq> S"
```
```   290     using open_contains_cball[of S] assms by auto
```
```   291   then have "aff_dim (cball x e) \<le> aff_dim S"
```
```   292     using aff_dim_subset by auto
```
```   293   with e show ?thesis
```
```   294     using aff_dim_cball[of e x] aff_dim_le_DIM[of S] by auto
```
```   295 qed
```
```   296
```
```   297 lemma low_dim_interior:
```
```   298   fixes S :: "'n::euclidean_space set"
```
```   299   assumes "\<not> aff_dim S = int (DIM('n))"
```
```   300   shows "interior S = {}"
```
```   301 proof -
```
```   302   have "aff_dim(interior S) \<le> aff_dim S"
```
```   303     using interior_subset aff_dim_subset[of "interior S" S] by auto
```
```   304   then show ?thesis
```
```   305     using aff_dim_open[of "interior S"] aff_dim_le_DIM[of S] assms by auto
```
```   306 qed
```
```   307
```
```   308 corollary empty_interior_lowdim:
```
```   309   fixes S :: "'n::euclidean_space set"
```
```   310   shows "dim S < DIM ('n) \<Longrightarrow> interior S = {}"
```
```   311 by (metis low_dim_interior affine_hull_UNIV dim_affine_hull less_not_refl dim_UNIV)
```
```   312
```
```   313 corollary aff_dim_nonempty_interior:
```
```   314   fixes S :: "'a::euclidean_space set"
```
```   315   shows "interior S \<noteq> {} \<Longrightarrow> aff_dim S = DIM('a)"
```
```   316 by (metis low_dim_interior)
```
```   317
```
```   318
```
```   319 subsection \<open>Relative interior of a set\<close>
```
```   320
```
```   321 definition%important "rel_interior S =
```
```   322   {x. \<exists>T. openin (top_of_set (affine hull S)) T \<and> x \<in> T \<and> T \<subseteq> S}"
```
```   323
```
```   324 lemma rel_interior_mono:
```
```   325    "\<lbrakk>S \<subseteq> T; affine hull S = affine hull T\<rbrakk>
```
```   326    \<Longrightarrow> (rel_interior S) \<subseteq> (rel_interior T)"
```
```   327   by (auto simp: rel_interior_def)
```
```   328
```
```   329 lemma rel_interior_maximal:
```
```   330    "\<lbrakk>T \<subseteq> S; openin(top_of_set (affine hull S)) T\<rbrakk> \<Longrightarrow> T \<subseteq> (rel_interior S)"
```
```   331   by (auto simp: rel_interior_def)
```
```   332
```
```   333 lemma rel_interior:
```
```   334   "rel_interior S = {x \<in> S. \<exists>T. open T \<and> x \<in> T \<and> T \<inter> affine hull S \<subseteq> S}"
```
```   335   unfolding rel_interior_def[of S] openin_open[of "affine hull S"]
```
```   336   apply auto
```
```   337 proof -
```
```   338   fix x T
```
```   339   assume *: "x \<in> S" "open T" "x \<in> T" "T \<inter> affine hull S \<subseteq> S"
```
```   340   then have **: "x \<in> T \<inter> affine hull S"
```
```   341     using hull_inc by auto
```
```   342   show "\<exists>Tb. (\<exists>Ta. open Ta \<and> Tb = affine hull S \<inter> Ta) \<and> x \<in> Tb \<and> Tb \<subseteq> S"
```
```   343     apply (rule_tac x = "T \<inter> (affine hull S)" in exI)
```
```   344     using * **
```
```   345     apply auto
```
```   346     done
```
```   347 qed
```
```   348
```
```   349 lemma mem_rel_interior: "x \<in> rel_interior S \<longleftrightarrow> (\<exists>T. open T \<and> x \<in> T \<inter> S \<and> T \<inter> affine hull S \<subseteq> S)"
```
```   350   by (auto simp: rel_interior)
```
```   351
```
```   352 lemma mem_rel_interior_ball:
```
```   353   "x \<in> rel_interior S \<longleftrightarrow> x \<in> S \<and> (\<exists>e. e > 0 \<and> ball x e \<inter> affine hull S \<subseteq> S)"
```
```   354   apply (simp add: rel_interior, safe)
```
```   355   apply (force simp: open_contains_ball)
```
```   356   apply (rule_tac x = "ball x e" in exI, simp)
```
```   357   done
```
```   358
```
```   359 lemma rel_interior_ball:
```
```   360   "rel_interior S = {x \<in> S. \<exists>e. e > 0 \<and> ball x e \<inter> affine hull S \<subseteq> S}"
```
```   361   using mem_rel_interior_ball [of _ S] by auto
```
```   362
```
```   363 lemma mem_rel_interior_cball:
```
```   364   "x \<in> rel_interior S \<longleftrightarrow> x \<in> S \<and> (\<exists>e. e > 0 \<and> cball x e \<inter> affine hull S \<subseteq> S)"
```
```   365   apply (simp add: rel_interior, safe)
```
```   366   apply (force simp: open_contains_cball)
```
```   367   apply (rule_tac x = "ball x e" in exI)
```
```   368   apply (simp add: subset_trans [OF ball_subset_cball], auto)
```
```   369   done
```
```   370
```
```   371 lemma rel_interior_cball:
```
```   372   "rel_interior S = {x \<in> S. \<exists>e. e > 0 \<and> cball x e \<inter> affine hull S \<subseteq> S}"
```
```   373   using mem_rel_interior_cball [of _ S] by auto
```
```   374
```
```   375 lemma rel_interior_empty [simp]: "rel_interior {} = {}"
```
```   376    by (auto simp: rel_interior_def)
```
```   377
```
```   378 lemma affine_hull_sing [simp]: "affine hull {a :: 'n::euclidean_space} = {a}"
```
```   379   by (metis affine_hull_eq affine_sing)
```
```   380
```
```   381 lemma rel_interior_sing [simp]:
```
```   382     fixes a :: "'n::euclidean_space"  shows "rel_interior {a} = {a}"
```
```   383   apply (auto simp: rel_interior_ball)
```
```   384   apply (rule_tac x=1 in exI, force)
```
```   385   done
```
```   386
```
```   387 lemma subset_rel_interior:
```
```   388   fixes S T :: "'n::euclidean_space set"
```
```   389   assumes "S \<subseteq> T"
```
```   390     and "affine hull S = affine hull T"
```
```   391   shows "rel_interior S \<subseteq> rel_interior T"
```
```   392   using assms by (auto simp: rel_interior_def)
```
```   393
```
```   394 lemma rel_interior_subset: "rel_interior S \<subseteq> S"
```
```   395   by (auto simp: rel_interior_def)
```
```   396
```
```   397 lemma rel_interior_subset_closure: "rel_interior S \<subseteq> closure S"
```
```   398   using rel_interior_subset by (auto simp: closure_def)
```
```   399
```
```   400 lemma interior_subset_rel_interior: "interior S \<subseteq> rel_interior S"
```
```   401   by (auto simp: rel_interior interior_def)
```
```   402
```
```   403 lemma interior_rel_interior:
```
```   404   fixes S :: "'n::euclidean_space set"
```
```   405   assumes "aff_dim S = int(DIM('n))"
```
```   406   shows "rel_interior S = interior S"
```
```   407 proof -
```
```   408   have "affine hull S = UNIV"
```
```   409     using assms affine_hull_UNIV[of S] by auto
```
```   410   then show ?thesis
```
```   411     unfolding rel_interior interior_def by auto
```
```   412 qed
```
```   413
```
```   414 lemma rel_interior_interior:
```
```   415   fixes S :: "'n::euclidean_space set"
```
```   416   assumes "affine hull S = UNIV"
```
```   417   shows "rel_interior S = interior S"
```
```   418   using assms unfolding rel_interior interior_def by auto
```
```   419
```
```   420 lemma rel_interior_open:
```
```   421   fixes S :: "'n::euclidean_space set"
```
```   422   assumes "open S"
```
```   423   shows "rel_interior S = S"
```
```   424   by (metis assms interior_eq interior_subset_rel_interior rel_interior_subset set_eq_subset)
```
```   425
```
```   426 lemma interior_ball [simp]: "interior (ball x e) = ball x e"
```
```   427   by (simp add: interior_open)
```
```   428
```
```   429 lemma interior_rel_interior_gen:
```
```   430   fixes S :: "'n::euclidean_space set"
```
```   431   shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})"
```
```   432   by (metis interior_rel_interior low_dim_interior)
```
```   433
```
```   434 lemma rel_interior_nonempty_interior:
```
```   435   fixes S :: "'n::euclidean_space set"
```
```   436   shows "interior S \<noteq> {} \<Longrightarrow> rel_interior S = interior S"
```
```   437 by (metis interior_rel_interior_gen)
```
```   438
```
```   439 lemma affine_hull_nonempty_interior:
```
```   440   fixes S :: "'n::euclidean_space set"
```
```   441   shows "interior S \<noteq> {} \<Longrightarrow> affine hull S = UNIV"
```
```   442 by (metis affine_hull_UNIV interior_rel_interior_gen)
```
```   443
```
```   444 lemma rel_interior_affine_hull [simp]:
```
```   445   fixes S :: "'n::euclidean_space set"
```
```   446   shows "rel_interior (affine hull S) = affine hull S"
```
```   447 proof -
```
```   448   have *: "rel_interior (affine hull S) \<subseteq> affine hull S"
```
```   449     using rel_interior_subset by auto
```
```   450   {
```
```   451     fix x
```
```   452     assume x: "x \<in> affine hull S"
```
```   453     define e :: real where "e = 1"
```
```   454     then have "e > 0" "ball x e \<inter> affine hull (affine hull S) \<subseteq> affine hull S"
```
```   455       using hull_hull[of _ S] by auto
```
```   456     then have "x \<in> rel_interior (affine hull S)"
```
```   457       using x rel_interior_ball[of "affine hull S"] by auto
```
```   458   }
```
```   459   then show ?thesis using * by auto
```
```   460 qed
```
```   461
```
```   462 lemma rel_interior_UNIV [simp]: "rel_interior (UNIV :: ('n::euclidean_space) set) = UNIV"
```
```   463   by (metis open_UNIV rel_interior_open)
```
```   464
```
```   465 lemma rel_interior_convex_shrink:
```
```   466   fixes S :: "'a::euclidean_space set"
```
```   467   assumes "convex S"
```
```   468     and "c \<in> rel_interior S"
```
```   469     and "x \<in> S"
```
```   470     and "0 < e"
```
```   471     and "e \<le> 1"
```
```   472   shows "x - e *\<^sub>R (x - c) \<in> rel_interior S"
```
```   473 proof -
```
```   474   obtain d where "d > 0" and d: "ball c d \<inter> affine hull S \<subseteq> S"
```
```   475     using assms(2) unfolding  mem_rel_interior_ball by auto
```
```   476   {
```
```   477     fix y
```
```   478     assume as: "dist (x - e *\<^sub>R (x - c)) y < e * d" "y \<in> affine hull S"
```
```   479     have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x"
```
```   480       using \<open>e > 0\<close> by (auto simp: scaleR_left_diff_distrib scaleR_right_diff_distrib)
```
```   481     have "x \<in> affine hull S"
```
```   482       using assms hull_subset[of S] by auto
```
```   483     moreover have "1 / e + - ((1 - e) / e) = 1"
```
```   484       using \<open>e > 0\<close> left_diff_distrib[of "1" "(1-e)" "1/e"] by auto
```
```   485     ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x \<in> affine hull S"
```
```   486       using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"]
```
```   487       by (simp add: algebra_simps)
```
```   488     have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = \<bar>1/e\<bar> * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
```
```   489       unfolding dist_norm norm_scaleR[symmetric]
```
```   490       apply (rule arg_cong[where f=norm])
```
```   491       using \<open>e > 0\<close>
```
```   492       apply (auto simp: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
```
```   493       done
```
```   494     also have "\<dots> = \<bar>1/e\<bar> * norm (x - e *\<^sub>R (x - c) - y)"
```
```   495       by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
```
```   496     also have "\<dots> < d"
```
```   497       using as[unfolded dist_norm] and \<open>e > 0\<close>
```
```   498       by (auto simp:pos_divide_less_eq[OF \<open>e > 0\<close>] mult.commute)
```
```   499     finally have "y \<in> S"
```
```   500       apply (subst *)
```
```   501       apply (rule assms(1)[unfolded convex_alt,rule_format])
```
```   502       apply (rule d[THEN subsetD])
```
```   503       unfolding mem_ball
```
```   504       using assms(3-5) **
```
```   505       apply auto
```
```   506       done
```
```   507   }
```
```   508   then have "ball (x - e *\<^sub>R (x - c)) (e*d) \<inter> affine hull S \<subseteq> S"
```
```   509     by auto
```
```   510   moreover have "e * d > 0"
```
```   511     using \<open>e > 0\<close> \<open>d > 0\<close> by simp
```
```   512   moreover have c: "c \<in> S"
```
```   513     using assms rel_interior_subset by auto
```
```   514   moreover from c have "x - e *\<^sub>R (x - c) \<in> S"
```
```   515     using convexD_alt[of S x c e]
```
```   516     apply (simp add: algebra_simps)
```
```   517     using assms
```
```   518     apply auto
```
```   519     done
```
```   520   ultimately show ?thesis
```
```   521     using mem_rel_interior_ball[of "x - e *\<^sub>R (x - c)" S] \<open>e > 0\<close> by auto
```
```   522 qed
```
```   523
```
```   524 lemma interior_real_atLeast [simp]:
```
```   525   fixes a :: real
```
```   526   shows "interior {a..} = {a<..}"
```
```   527 proof -
```
```   528   {
```
```   529     fix y
```
```   530     assume "a < y"
```
```   531     then have "y \<in> interior {a..}"
```
```   532       apply (simp add: mem_interior)
```
```   533       apply (rule_tac x="(y-a)" in exI)
```
```   534       apply (auto simp: dist_norm)
```
```   535       done
```
```   536   }
```
```   537   moreover
```
```   538   {
```
```   539     fix y
```
```   540     assume "y \<in> interior {a..}"
```
```   541     then obtain e where e: "e > 0" "cball y e \<subseteq> {a..}"
```
```   542       using mem_interior_cball[of y "{a..}"] by auto
```
```   543     moreover from e have "y - e \<in> cball y e"
```
```   544       by (auto simp: cball_def dist_norm)
```
```   545     ultimately have "a \<le> y - e" by blast
```
```   546     then have "a < y" using e by auto
```
```   547   }
```
```   548   ultimately show ?thesis by auto
```
```   549 qed
```
```   550
```
```   551 lemma continuous_ge_on_Ioo:
```
```   552   assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
```
```   553   shows "g (x::real) \<ge> (a::real)"
```
```   554 proof-
```
```   555   from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_greaterThanLessThan[symmetric])
```
```   556   also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
```
```   557   hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
```
```   558   also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
```
```   559     by (auto simp: continuous_on_closed_vimage)
```
```   560   hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
```
```   561   finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto
```
```   562 qed
```
```   563
```
```   564 lemma interior_real_atMost [simp]:
```
```   565   fixes a :: real
```
```   566   shows "interior {..a} = {..<a}"
```
```   567 proof -
```
```   568   {
```
```   569     fix y
```
```   570     assume "a > y"
```
```   571     then have "y \<in> interior {..a}"
```
```   572       apply (simp add: mem_interior)
```
```   573       apply (rule_tac x="(a-y)" in exI)
```
```   574       apply (auto simp: dist_norm)
```
```   575       done
```
```   576   }
```
```   577   moreover
```
```   578   {
```
```   579     fix y
```
```   580     assume "y \<in> interior {..a}"
```
```   581     then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
```
```   582       using mem_interior_cball[of y "{..a}"] by auto
```
```   583     moreover from e have "y + e \<in> cball y e"
```
```   584       by (auto simp: cball_def dist_norm)
```
```   585     ultimately have "a \<ge> y + e" by auto
```
```   586     then have "a > y" using e by auto
```
```   587   }
```
```   588   ultimately show ?thesis by auto
```
```   589 qed
```
```   590
```
```   591 lemma interior_atLeastAtMost_real [simp]: "interior {a..b} = {a<..<b :: real}"
```
```   592 proof-
```
```   593   have "{a..b} = {a..} \<inter> {..b}" by auto
```
```   594   also have "interior \<dots> = {a<..} \<inter> {..<b}"
```
```   595     by (simp add: interior_real_atLeast interior_real_atMost)
```
```   596   also have "\<dots> = {a<..<b}" by auto
```
```   597   finally show ?thesis .
```
```   598 qed
```
```   599
```
```   600 lemma interior_atLeastLessThan [simp]:
```
```   601   fixes a::real shows "interior {a..<b} = {a<..<b}"
```
```   602   by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost_real interior_Int interior_interior interior_real_atLeast)
```
```   603
```
```   604 lemma interior_lessThanAtMost [simp]:
```
```   605   fixes a::real shows "interior {a<..b} = {a<..<b}"
```
```   606   by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost_real interior_Int
```
```   607             interior_interior interior_real_atLeast)
```
```   608
```
```   609 lemma interior_greaterThanLessThan_real [simp]: "interior {a<..<b} = {a<..<b :: real}"
```
```   610   by (metis interior_atLeastAtMost_real interior_interior)
```
```   611
```
```   612 lemma frontier_real_atMost [simp]:
```
```   613   fixes a :: real
```
```   614   shows "frontier {..a} = {a}"
```
```   615   unfolding frontier_def by (auto simp: interior_real_atMost)
```
```   616
```
```   617 lemma frontier_real_atLeast [simp]: "frontier {a..} = {a::real}"
```
```   618   by (auto simp: frontier_def)
```
```   619
```
```   620 lemma frontier_real_greaterThan [simp]: "frontier {a<..} = {a::real}"
```
```   621   by (auto simp: interior_open frontier_def)
```
```   622
```
```   623 lemma frontier_real_lessThan [simp]: "frontier {..<a} = {a::real}"
```
```   624   by (auto simp: interior_open frontier_def)
```
```   625
```
```   626 lemma rel_interior_real_box [simp]:
```
```   627   fixes a b :: real
```
```   628   assumes "a < b"
```
```   629   shows "rel_interior {a .. b} = {a <..< b}"
```
```   630 proof -
```
```   631   have "box a b \<noteq> {}"
```
```   632     using assms
```
```   633     unfolding set_eq_iff
```
```   634     by (auto intro!: exI[of _ "(a + b) / 2"] simp: box_def)
```
```   635   then show ?thesis
```
```   636     using interior_rel_interior_gen[of "cbox a b", symmetric]
```
```   637     by (simp split: if_split_asm del: box_real add: box_real[symmetric] interior_cbox)
```
```   638 qed
```
```   639
```
```   640 lemma rel_interior_real_semiline [simp]:
```
```   641   fixes a :: real
```
```   642   shows "rel_interior {a..} = {a<..}"
```
```   643 proof -
```
```   644   have *: "{a<..} \<noteq> {}"
```
```   645     unfolding set_eq_iff by (auto intro!: exI[of _ "a + 1"])
```
```   646   then show ?thesis using interior_real_atLeast interior_rel_interior_gen[of "{a..}"]
```
```   647     by (auto split: if_split_asm)
```
```   648 qed
```
```   649
```
```   650 subsubsection \<open>Relative open sets\<close>
```
```   651
```
```   652 definition%important "rel_open S \<longleftrightarrow> rel_interior S = S"
```
```   653
```
```   654 lemma rel_open: "rel_open S \<longleftrightarrow> openin (top_of_set (affine hull S)) S"
```
```   655   unfolding rel_open_def rel_interior_def
```
```   656   apply auto
```
```   657   using openin_subopen[of "top_of_set (affine hull S)" S]
```
```   658   apply auto
```
```   659   done
```
```   660
```
```   661 lemma openin_rel_interior: "openin (top_of_set (affine hull S)) (rel_interior S)"
```
```   662   apply (simp add: rel_interior_def)
```
```   663   apply (subst openin_subopen, blast)
```
```   664   done
```
```   665
```
```   666 lemma openin_set_rel_interior:
```
```   667    "openin (top_of_set S) (rel_interior S)"
```
```   668 by (rule openin_subset_trans [OF openin_rel_interior rel_interior_subset hull_subset])
```
```   669
```
```   670 lemma affine_rel_open:
```
```   671   fixes S :: "'n::euclidean_space set"
```
```   672   assumes "affine S"
```
```   673   shows "rel_open S"
```
```   674   unfolding rel_open_def
```
```   675   using assms rel_interior_affine_hull[of S] affine_hull_eq[of S]
```
```   676   by metis
```
```   677
```
```   678 lemma affine_closed:
```
```   679   fixes S :: "'n::euclidean_space set"
```
```   680   assumes "affine S"
```
```   681   shows "closed S"
```
```   682 proof -
```
```   683   {
```
```   684     assume "S \<noteq> {}"
```
```   685     then obtain L where L: "subspace L" "affine_parallel S L"
```
```   686       using assms affine_parallel_subspace[of S] by auto
```
```   687     then obtain a where a: "S = ((+) a ` L)"
```
```   688       using affine_parallel_def[of L S] affine_parallel_commut by auto
```
```   689     from L have "closed L" using closed_subspace by auto
```
```   690     then have "closed S"
```
```   691       using closed_translation a by auto
```
```   692   }
```
```   693   then show ?thesis by auto
```
```   694 qed
```
```   695
```
```   696 lemma closure_affine_hull:
```
```   697   fixes S :: "'n::euclidean_space set"
```
```   698   shows "closure S \<subseteq> affine hull S"
```
```   699   by (intro closure_minimal hull_subset affine_closed affine_affine_hull)
```
```   700
```
```   701 lemma closure_same_affine_hull [simp]:
```
```   702   fixes S :: "'n::euclidean_space set"
```
```   703   shows "affine hull (closure S) = affine hull S"
```
```   704 proof -
```
```   705   have "affine hull (closure S) \<subseteq> affine hull S"
```
```   706     using hull_mono[of "closure S" "affine hull S" "affine"]
```
```   707       closure_affine_hull[of S] hull_hull[of "affine" S]
```
```   708     by auto
```
```   709   moreover have "affine hull (closure S) \<supseteq> affine hull S"
```
```   710     using hull_mono[of "S" "closure S" "affine"] closure_subset by auto
```
```   711   ultimately show ?thesis by auto
```
```   712 qed
```
```   713
```
```   714 lemma closure_aff_dim [simp]:
```
```   715   fixes S :: "'n::euclidean_space set"
```
```   716   shows "aff_dim (closure S) = aff_dim S"
```
```   717 proof -
```
```   718   have "aff_dim S \<le> aff_dim (closure S)"
```
```   719     using aff_dim_subset closure_subset by auto
```
```   720   moreover have "aff_dim (closure S) \<le> aff_dim (affine hull S)"
```
```   721     using aff_dim_subset closure_affine_hull by blast
```
```   722   moreover have "aff_dim (affine hull S) = aff_dim S"
```
```   723     using aff_dim_affine_hull by auto
```
```   724   ultimately show ?thesis by auto
```
```   725 qed
```
```   726
```
```   727 lemma rel_interior_closure_convex_shrink:
```
```   728   fixes S :: "_::euclidean_space set"
```
```   729   assumes "convex S"
```
```   730     and "c \<in> rel_interior S"
```
```   731     and "x \<in> closure S"
```
```   732     and "e > 0"
```
```   733     and "e \<le> 1"
```
```   734   shows "x - e *\<^sub>R (x - c) \<in> rel_interior S"
```
```   735 proof -
```
```   736   obtain d where "d > 0" and d: "ball c d \<inter> affine hull S \<subseteq> S"
```
```   737     using assms(2) unfolding mem_rel_interior_ball by auto
```
```   738   have "\<exists>y \<in> S. norm (y - x) * (1 - e) < e * d"
```
```   739   proof (cases "x \<in> S")
```
```   740     case True
```
```   741     then show ?thesis using \<open>e > 0\<close> \<open>d > 0\<close>
```
```   742       apply (rule_tac bexI[where x=x], auto)
```
```   743       done
```
```   744   next
```
```   745     case False
```
```   746     then have x: "x islimpt S"
```
```   747       using assms(3)[unfolded closure_def] by auto
```
```   748     show ?thesis
```
```   749     proof (cases "e = 1")
```
```   750       case True
```
```   751       obtain y where "y \<in> S" "y \<noteq> x" "dist y x < 1"
```
```   752         using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto
```
```   753       then show ?thesis
```
```   754         apply (rule_tac x=y in bexI)
```
```   755         unfolding True
```
```   756         using \<open>d > 0\<close>
```
```   757         apply auto
```
```   758         done
```
```   759     next
```
```   760       case False
```
```   761       then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
```
```   762         using \<open>e \<le> 1\<close> \<open>e > 0\<close> \<open>d > 0\<close> by auto
```
```   763       then obtain y where "y \<in> S" "y \<noteq> x" "dist y x < e * d / (1 - e)"
```
```   764         using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
```
```   765       then show ?thesis
```
```   766         apply (rule_tac x=y in bexI)
```
```   767         unfolding dist_norm
```
```   768         using pos_less_divide_eq[OF *]
```
```   769         apply auto
```
```   770         done
```
```   771     qed
```
```   772   qed
```
```   773   then obtain y where "y \<in> S" and y: "norm (y - x) * (1 - e) < e * d"
```
```   774     by auto
```
```   775   define z where "z = c + ((1 - e) / e) *\<^sub>R (x - y)"
```
```   776   have *: "x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)"
```
```   777     unfolding z_def using \<open>e > 0\<close>
```
```   778     by (auto simp: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
```
```   779   have zball: "z \<in> ball c d"
```
```   780     using mem_ball z_def dist_norm[of c]
```
```   781     using y and assms(4,5)
```
```   782     by (auto simp:field_simps norm_minus_commute)
```
```   783   have "x \<in> affine hull S"
```
```   784     using closure_affine_hull assms by auto
```
```   785   moreover have "y \<in> affine hull S"
```
```   786     using \<open>y \<in> S\<close> hull_subset[of S] by auto
```
```   787   moreover have "c \<in> affine hull S"
```
```   788     using assms rel_interior_subset hull_subset[of S] by auto
```
```   789   ultimately have "z \<in> affine hull S"
```
```   790     using z_def affine_affine_hull[of S]
```
```   791       mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"]
```
```   792       assms
```
```   793     by (auto simp: field_simps)
```
```   794   then have "z \<in> S" using d zball by auto
```
```   795   obtain d1 where "d1 > 0" and d1: "ball z d1 \<le> ball c d"
```
```   796     using zball open_ball[of c d] openE[of "ball c d" z] by auto
```
```   797   then have "ball z d1 \<inter> affine hull S \<subseteq> ball c d \<inter> affine hull S"
```
```   798     by auto
```
```   799   then have "ball z d1 \<inter> affine hull S \<subseteq> S"
```
```   800     using d by auto
```
```   801   then have "z \<in> rel_interior S"
```
```   802     using mem_rel_interior_ball using \<open>d1 > 0\<close> \<open>z \<in> S\<close> by auto
```
```   803   then have "y - e *\<^sub>R (y - z) \<in> rel_interior S"
```
```   804     using rel_interior_convex_shrink[of S z y e] assms \<open>y \<in> S\<close> by auto
```
```   805   then show ?thesis using * by auto
```
```   806 qed
```
```   807
```
```   808 lemma rel_interior_eq:
```
```   809    "rel_interior s = s \<longleftrightarrow> openin(top_of_set (affine hull s)) s"
```
```   810 using rel_open rel_open_def by blast
```
```   811
```
```   812 lemma rel_interior_openin:
```
```   813    "openin(top_of_set (affine hull s)) s \<Longrightarrow> rel_interior s = s"
```
```   814 by (simp add: rel_interior_eq)
```
```   815
```
```   816 lemma rel_interior_affine:
```
```   817   fixes S :: "'n::euclidean_space set"
```
```   818   shows  "affine S \<Longrightarrow> rel_interior S = S"
```
```   819 using affine_rel_open rel_open_def by auto
```
```   820
```
```   821 lemma rel_interior_eq_closure:
```
```   822   fixes S :: "'n::euclidean_space set"
```
```   823   shows "rel_interior S = closure S \<longleftrightarrow> affine S"
```
```   824 proof (cases "S = {}")
```
```   825   case True
```
```   826  then show ?thesis
```
```   827     by auto
```
```   828 next
```
```   829   case False show ?thesis
```
```   830   proof
```
```   831     assume eq: "rel_interior S = closure S"
```
```   832     have "S = {} \<or> S = affine hull S"
```
```   833       apply (rule connected_clopen [THEN iffD1, rule_format])
```
```   834        apply (simp add: affine_imp_convex convex_connected)
```
```   835       apply (rule conjI)
```
```   836        apply (metis eq closure_subset openin_rel_interior rel_interior_subset subset_antisym)
```
```   837       apply (metis closed_subset closure_subset_eq eq hull_subset rel_interior_subset)
```
```   838       done
```
```   839     with False have "affine hull S = S"
```
```   840       by auto
```
```   841     then show "affine S"
```
```   842       by (metis affine_hull_eq)
```
```   843   next
```
```   844     assume "affine S"
```
```   845     then show "rel_interior S = closure S"
```
```   846       by (simp add: rel_interior_affine affine_closed)
```
```   847   qed
```
```   848 qed
```
```   849
```
```   850
```
```   851 subsubsection%unimportant\<open>Relative interior preserves under linear transformations\<close>
```
```   852
```
```   853 lemma rel_interior_translation_aux:
```
```   854   fixes a :: "'n::euclidean_space"
```
```   855   shows "((\<lambda>x. a + x) ` rel_interior S) \<subseteq> rel_interior ((\<lambda>x. a + x) ` S)"
```
```   856 proof -
```
```   857   {
```
```   858     fix x
```
```   859     assume x: "x \<in> rel_interior S"
```
```   860     then obtain T where "open T" "x \<in> T \<inter> S" "T \<inter> affine hull S \<subseteq> S"
```
```   861       using mem_rel_interior[of x S] by auto
```
```   862     then have "open ((\<lambda>x. a + x) ` T)"
```
```   863       and "a + x \<in> ((\<lambda>x. a + x) ` T) \<inter> ((\<lambda>x. a + x) ` S)"
```
```   864       and "((\<lambda>x. a + x) ` T) \<inter> affine hull ((\<lambda>x. a + x) ` S) \<subseteq> (\<lambda>x. a + x) ` S"
```
```   865       using affine_hull_translation[of a S] open_translation[of T a] x by auto
```
```   866     then have "a + x \<in> rel_interior ((\<lambda>x. a + x) ` S)"
```
```   867       using mem_rel_interior[of "a+x" "((\<lambda>x. a + x) ` S)"] by auto
```
```   868   }
```
```   869   then show ?thesis by auto
```
```   870 qed
```
```   871
```
```   872 lemma rel_interior_translation:
```
```   873   fixes a :: "'n::euclidean_space"
```
```   874   shows "rel_interior ((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` rel_interior S"
```
```   875 proof -
```
```   876   have "(\<lambda>x. (-a) + x) ` rel_interior ((\<lambda>x. a + x) ` S) \<subseteq> rel_interior S"
```
```   877     using rel_interior_translation_aux[of "-a" "(\<lambda>x. a + x) ` S"]
```
```   878       translation_assoc[of "-a" "a"]
```
```   879     by auto
```
```   880   then have "((\<lambda>x. a + x) ` rel_interior S) \<supseteq> rel_interior ((\<lambda>x. a + x) ` S)"
```
```   881     using translation_inverse_subset[of a "rel_interior ((+) a ` S)" "rel_interior S"]
```
```   882     by auto
```
```   883   then show ?thesis
```
```   884     using rel_interior_translation_aux[of a S] by auto
```
```   885 qed
```
```   886
```
```   887
```
```   888 lemma affine_hull_linear_image:
```
```   889   assumes "bounded_linear f"
```
```   890   shows "f ` (affine hull s) = affine hull f ` s"
```
```   891 proof -
```
```   892   interpret f: bounded_linear f by fact
```
```   893   have "affine {x. f x \<in> affine hull f ` s}"
```
```   894     unfolding affine_def
```
```   895     by (auto simp: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format])
```
```   896   moreover have "affine {x. x \<in> f ` (affine hull s)}"
```
```   897     using affine_affine_hull[unfolded affine_def, of s]
```
```   898     unfolding affine_def by (auto simp: f.scaleR [symmetric] f.add [symmetric])
```
```   899   ultimately show ?thesis
```
```   900     by (auto simp: hull_inc elim!: hull_induct)
```
```   901 qed
```
```   902
```
```   903
```
```   904 lemma rel_interior_injective_on_span_linear_image:
```
```   905   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
```
```   906     and S :: "'m::euclidean_space set"
```
```   907   assumes "bounded_linear f"
```
```   908     and "inj_on f (span S)"
```
```   909   shows "rel_interior (f ` S) = f ` (rel_interior S)"
```
```   910 proof -
```
```   911   {
```
```   912     fix z
```
```   913     assume z: "z \<in> rel_interior (f ` S)"
```
```   914     then have "z \<in> f ` S"
```
```   915       using rel_interior_subset[of "f ` S"] by auto
```
```   916     then obtain x where x: "x \<in> S" "f x = z" by auto
```
```   917     obtain e2 where e2: "e2 > 0" "cball z e2 \<inter> affine hull (f ` S) \<subseteq> (f ` S)"
```
```   918       using z rel_interior_cball[of "f ` S"] by auto
```
```   919     obtain K where K: "K > 0" "\<And>x. norm (f x) \<le> norm x * K"
```
```   920      using assms Real_Vector_Spaces.bounded_linear.pos_bounded[of f] by auto
```
```   921     define e1 where "e1 = 1 / K"
```
```   922     then have e1: "e1 > 0" "\<And>x. e1 * norm (f x) \<le> norm x"
```
```   923       using K pos_le_divide_eq[of e1] by auto
```
```   924     define e where "e = e1 * e2"
```
```   925     then have "e > 0" using e1 e2 by auto
```
```   926     {
```
```   927       fix y
```
```   928       assume y: "y \<in> cball x e \<inter> affine hull S"
```
```   929       then have h1: "f y \<in> affine hull (f ` S)"
```
```   930         using affine_hull_linear_image[of f S] assms by auto
```
```   931       from y have "norm (x-y) \<le> e1 * e2"
```
```   932         using cball_def[of x e] dist_norm[of x y] e_def by auto
```
```   933       moreover have "f x - f y = f (x - y)"
```
```   934         using assms linear_diff[of f x y] linear_conv_bounded_linear[of f] by auto
```
```   935       moreover have "e1 * norm (f (x-y)) \<le> norm (x - y)"
```
```   936         using e1 by auto
```
```   937       ultimately have "e1 * norm ((f x)-(f y)) \<le> e1 * e2"
```
```   938         by auto
```
```   939       then have "f y \<in> cball z e2"
```
```   940         using cball_def[of "f x" e2] dist_norm[of "f x" "f y"] e1 x by auto
```
```   941       then have "f y \<in> f ` S"
```
```   942         using y e2 h1 by auto
```
```   943       then have "y \<in> S"
```
```   944         using assms y hull_subset[of S] affine_hull_subset_span
```
```   945           inj_on_image_mem_iff [OF \<open>inj_on f (span S)\<close>]
```
```   946         by (metis Int_iff span_superset subsetCE)
```
```   947     }
```
```   948     then have "z \<in> f ` (rel_interior S)"
```
```   949       using mem_rel_interior_cball[of x S] \<open>e > 0\<close> x by auto
```
```   950   }
```
```   951   moreover
```
```   952   {
```
```   953     fix x
```
```   954     assume x: "x \<in> rel_interior S"
```
```   955     then obtain e2 where e2: "e2 > 0" "cball x e2 \<inter> affine hull S \<subseteq> S"
```
```   956       using rel_interior_cball[of S] by auto
```
```   957     have "x \<in> S" using x rel_interior_subset by auto
```
```   958     then have *: "f x \<in> f ` S" by auto
```
```   959     have "\<forall>x\<in>span S. f x = 0 \<longrightarrow> x = 0"
```
```   960       using assms subspace_span linear_conv_bounded_linear[of f]
```
```   961         linear_injective_on_subspace_0[of f "span S"]
```
```   962       by auto
```
```   963     then obtain e1 where e1: "e1 > 0" "\<forall>x \<in> span S. e1 * norm x \<le> norm (f x)"
```
```   964       using assms injective_imp_isometric[of "span S" f]
```
```   965         subspace_span[of S] closed_subspace[of "span S"]
```
```   966       by auto
```
```   967     define e where "e = e1 * e2"
```
```   968     hence "e > 0" using e1 e2 by auto
```
```   969     {
```
```   970       fix y
```
```   971       assume y: "y \<in> cball (f x) e \<inter> affine hull (f ` S)"
```
```   972       then have "y \<in> f ` (affine hull S)"
```
```   973         using affine_hull_linear_image[of f S] assms by auto
```
```   974       then obtain xy where xy: "xy \<in> affine hull S" "f xy = y" by auto
```
```   975       with y have "norm (f x - f xy) \<le> e1 * e2"
```
```   976         using cball_def[of "f x" e] dist_norm[of "f x" y] e_def by auto
```
```   977       moreover have "f x - f xy = f (x - xy)"
```
```   978         using assms linear_diff[of f x xy] linear_conv_bounded_linear[of f] by auto
```
```   979       moreover have *: "x - xy \<in> span S"
```
```   980         using subspace_diff[of "span S" x xy] subspace_span \<open>x \<in> S\<close> xy
```
```   981           affine_hull_subset_span[of S] span_superset
```
```   982         by auto
```
```   983       moreover from * have "e1 * norm (x - xy) \<le> norm (f (x - xy))"
```
```   984         using e1 by auto
```
```   985       ultimately have "e1 * norm (x - xy) \<le> e1 * e2"
```
```   986         by auto
```
```   987       then have "xy \<in> cball x e2"
```
```   988         using cball_def[of x e2] dist_norm[of x xy] e1 by auto
```
```   989       then have "y \<in> f ` S"
```
```   990         using xy e2 by auto
```
```   991     }
```
```   992     then have "f x \<in> rel_interior (f ` S)"
```
```   993       using mem_rel_interior_cball[of "(f x)" "(f ` S)"] * \<open>e > 0\<close> by auto
```
```   994   }
```
```   995   ultimately show ?thesis by auto
```
```   996 qed
```
```   997
```
```   998 lemma rel_interior_injective_linear_image:
```
```   999   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
```
```  1000   assumes "bounded_linear f"
```
```  1001     and "inj f"
```
```  1002   shows "rel_interior (f ` S) = f ` (rel_interior S)"
```
```  1003   using assms rel_interior_injective_on_span_linear_image[of f S]
```
```  1004     subset_inj_on[of f "UNIV" "span S"]
```
```  1005   by auto
```
```  1006
```
```  1007
```
```  1008 subsection%unimportant \<open>Openness and compactness are preserved by convex hull operation\<close>
```
```  1009
```
```  1010 lemma open_convex_hull[intro]:
```
```  1011   fixes S :: "'a::real_normed_vector set"
```
```  1012   assumes "open S"
```
```  1013   shows "open (convex hull S)"
```
```  1014 proof (clarsimp simp: open_contains_cball convex_hull_explicit)
```
```  1015   fix T and u :: "'a\<Rightarrow>real"
```
```  1016   assume obt: "finite T" "T\<subseteq>S" "\<forall>x\<in>T. 0 \<le> u x" "sum u T = 1"
```
```  1017
```
```  1018   from assms[unfolded open_contains_cball] obtain b
```
```  1019     where b: "\<And>x. x\<in>S \<Longrightarrow> 0 < b x \<and> cball x (b x) \<subseteq> S" by metis
```
```  1020   have "b ` T \<noteq> {}"
```
```  1021     using obt by auto
```
```  1022   define i where "i = b ` T"
```
```  1023   let ?\<Phi> = "\<lambda>y. \<exists>F. finite F \<and> F \<subseteq> S \<and> (\<exists>u. (\<forall>x\<in>F. 0 \<le> u x) \<and> sum u F = 1 \<and> (\<Sum>v\<in>F. u v *\<^sub>R v) = y)"
```
```  1024   let ?a = "\<Sum>v\<in>T. u v *\<^sub>R v"
```
```  1025   show "\<exists>e > 0. cball ?a e \<subseteq> {y. ?\<Phi> y}"
```
```  1026   proof (intro exI subsetI conjI)
```
```  1027     show "0 < Min i"
```
```  1028       unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] \<open>b ` T\<noteq>{}\<close>]
```
```  1029       using b \<open>T\<subseteq>S\<close> by auto
```
```  1030   next
```
```  1031     fix y
```
```  1032     assume "y \<in> cball ?a (Min i)"
```
```  1033     then have y: "norm (?a - y) \<le> Min i"
```
```  1034       unfolding dist_norm[symmetric] by auto
```
```  1035     { fix x
```
```  1036       assume "x \<in> T"
```
```  1037       then have "Min i \<le> b x"
```
```  1038         by (simp add: i_def obt(1))
```
```  1039       then have "x + (y - ?a) \<in> cball x (b x)"
```
```  1040         using y unfolding mem_cball dist_norm by auto
```
```  1041       moreover have "x \<in> S"
```
```  1042         using \<open>x\<in>T\<close> \<open>T\<subseteq>S\<close> by auto
```
```  1043       ultimately have "x + (y - ?a) \<in> S"
```
```  1044         using y b by blast
```
```  1045     }
```
```  1046     moreover
```
```  1047     have *: "inj_on (\<lambda>v. v + (y - ?a)) T"
```
```  1048       unfolding inj_on_def by auto
```
```  1049     have "(\<Sum>v\<in>(\<lambda>v. v + (y - ?a)) ` T. u (v - (y - ?a)) *\<^sub>R v) = y"
```
```  1050       unfolding sum.reindex[OF *] o_def using obt(4)
```
```  1051       by (simp add: sum.distrib sum_subtractf scaleR_left.sum[symmetric] scaleR_right_distrib)
```
```  1052     ultimately show "y \<in> {y. ?\<Phi> y}"
```
```  1053     proof (intro CollectI exI conjI)
```
```  1054       show "finite ((\<lambda>v. v + (y - ?a)) ` T)"
```
```  1055         by (simp add: obt(1))
```
```  1056       show "sum (\<lambda>v. u (v - (y - ?a))) ((\<lambda>v. v + (y - ?a)) ` T) = 1"
```
```  1057         unfolding sum.reindex[OF *] o_def using obt(4) by auto
```
```  1058     qed (use obt(1, 3) in auto)
```
```  1059   qed
```
```  1060 qed
```
```  1061
```
```  1062 lemma compact_convex_combinations:
```
```  1063   fixes S T :: "'a::real_normed_vector set"
```
```  1064   assumes "compact S" "compact T"
```
```  1065   shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> S \<and> y \<in> T}"
```
```  1066 proof -
```
```  1067   let ?X = "{0..1} \<times> S \<times> T"
```
```  1068   let ?h = "(\<lambda>z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))"
```
```  1069   have *: "{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> S \<and> y \<in> T} = ?h ` ?X"
```
```  1070     by force
```
```  1071   have "continuous_on ?X (\<lambda>z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))"
```
```  1072     unfolding continuous_on by (rule ballI) (intro tendsto_intros)
```
```  1073   with assms show ?thesis
```
```  1074     by (simp add: * compact_Times compact_continuous_image)
```
```  1075 qed
```
```  1076
```
```  1077 lemma finite_imp_compact_convex_hull:
```
```  1078   fixes S :: "'a::real_normed_vector set"
```
```  1079   assumes "finite S"
```
```  1080   shows "compact (convex hull S)"
```
```  1081 proof (cases "S = {}")
```
```  1082   case True
```
```  1083   then show ?thesis by simp
```
```  1084 next
```
```  1085   case False
```
```  1086   with assms show ?thesis
```
```  1087   proof (induct rule: finite_ne_induct)
```
```  1088     case (singleton x)
```
```  1089     show ?case by simp
```
```  1090   next
```
```  1091     case (insert x A)
```
```  1092     let ?f = "\<lambda>(u, y::'a). u *\<^sub>R x + (1 - u) *\<^sub>R y"
```
```  1093     let ?T = "{0..1::real} \<times> (convex hull A)"
```
```  1094     have "continuous_on ?T ?f"
```
```  1095       unfolding split_def continuous_on by (intro ballI tendsto_intros)
```
```  1096     moreover have "compact ?T"
```
```  1097       by (intro compact_Times compact_Icc insert)
```
```  1098     ultimately have "compact (?f ` ?T)"
```
```  1099       by (rule compact_continuous_image)
```
```  1100     also have "?f ` ?T = convex hull (insert x A)"
```
```  1101       unfolding convex_hull_insert [OF \<open>A \<noteq> {}\<close>]
```
```  1102       apply safe
```
```  1103       apply (rule_tac x=a in exI, simp)
```
```  1104       apply (rule_tac x="1 - a" in exI, simp, fast)
```
```  1105       apply (rule_tac x="(u, b)" in image_eqI, simp_all)
```
```  1106       done
```
```  1107     finally show "compact (convex hull (insert x A))" .
```
```  1108   qed
```
```  1109 qed
```
```  1110
```
```  1111 lemma compact_convex_hull:
```
```  1112   fixes S :: "'a::euclidean_space set"
```
```  1113   assumes "compact S"
```
```  1114   shows "compact (convex hull S)"
```
```  1115 proof (cases "S = {}")
```
```  1116   case True
```
```  1117   then show ?thesis using compact_empty by simp
```
```  1118 next
```
```  1119   case False
```
```  1120   then obtain w where "w \<in> S" by auto
```
```  1121   show ?thesis
```
```  1122     unfolding caratheodory[of S]
```
```  1123   proof (induct ("DIM('a) + 1"))
```
```  1124     case 0
```
```  1125     have *: "{x.\<exists>sa. finite sa \<and> sa \<subseteq> S \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}"
```
```  1126       using compact_empty by auto
```
```  1127     from 0 show ?case unfolding * by simp
```
```  1128   next
```
```  1129     case (Suc n)
```
```  1130     show ?case
```
```  1131     proof (cases "n = 0")
```
```  1132       case True
```
```  1133       have "{x. \<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T} = S"
```
```  1134         unfolding set_eq_iff and mem_Collect_eq
```
```  1135       proof (rule, rule)
```
```  1136         fix x
```
```  1137         assume "\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T"
```
```  1138         then obtain T where T: "finite T" "T \<subseteq> S" "card T \<le> Suc n" "x \<in> convex hull T"
```
```  1139           by auto
```
```  1140         show "x \<in> S"
```
```  1141         proof (cases "card T = 0")
```
```  1142           case True
```
```  1143           then show ?thesis
```
```  1144             using T(4) unfolding card_0_eq[OF T(1)] by simp
```
```  1145         next
```
```  1146           case False
```
```  1147           then have "card T = Suc 0" using T(3) \<open>n=0\<close> by auto
```
```  1148           then obtain a where "T = {a}" unfolding card_Suc_eq by auto
```
```  1149           then show ?thesis using T(2,4) by simp
```
```  1150         qed
```
```  1151       next
```
```  1152         fix x assume "x\<in>S"
```
```  1153         then show "\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T"
```
```  1154           apply (rule_tac x="{x}" in exI)
```
```  1155           unfolding convex_hull_singleton
```
```  1156           apply auto
```
```  1157           done
```
```  1158       qed
```
```  1159       then show ?thesis using assms by simp
```
```  1160     next
```
```  1161       case False
```
```  1162       have "{x. \<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T} =
```
```  1163         {(1 - u) *\<^sub>R x + u *\<^sub>R y | x y u.
```
```  1164           0 \<le> u \<and> u \<le> 1 \<and> x \<in> S \<and> y \<in> {x. \<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> n \<and> x \<in> convex hull T}}"
```
```  1165         unfolding set_eq_iff and mem_Collect_eq
```
```  1166       proof (rule, rule)
```
```  1167         fix x
```
```  1168         assume "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
```
```  1169           0 \<le> c \<and> c \<le> 1 \<and> u \<in> S \<and> (\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> n \<and> v \<in> convex hull T)"
```
```  1170         then obtain u v c T where obt: "x = (1 - c) *\<^sub>R u + c *\<^sub>R v"
```
```  1171           "0 \<le> c \<and> c \<le> 1" "u \<in> S" "finite T" "T \<subseteq> S" "card T \<le> n"  "v \<in> convex hull T"
```
```  1172           by auto
```
```  1173         moreover have "(1 - c) *\<^sub>R u + c *\<^sub>R v \<in> convex hull insert u T"
```
```  1174           apply (rule convexD_alt)
```
```  1175           using obt(2) and convex_convex_hull and hull_subset[of "insert u T" convex]
```
```  1176           using obt(7) and hull_mono[of T "insert u T"]
```
```  1177           apply auto
```
```  1178           done
```
```  1179         ultimately show "\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T"
```
```  1180           apply (rule_tac x="insert u T" in exI)
```
```  1181           apply (auto simp: card_insert_if)
```
```  1182           done
```
```  1183       next
```
```  1184         fix x
```
```  1185         assume "\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> Suc n \<and> x \<in> convex hull T"
```
```  1186         then obtain T where T: "finite T" "T \<subseteq> S" "card T \<le> Suc n" "x \<in> convex hull T"
```
```  1187           by auto
```
```  1188         show "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
```
```  1189           0 \<le> c \<and> c \<le> 1 \<and> u \<in> S \<and> (\<exists>T. finite T \<and> T \<subseteq> S \<and> card T \<le> n \<and> v \<in> convex hull T)"
```
```  1190         proof (cases "card T = Suc n")
```
```  1191           case False
```
```  1192           then have "card T \<le> n" using T(3) by auto
```
```  1193           then show ?thesis
```
```  1194             apply (rule_tac x=w in exI, rule_tac x=x in exI, rule_tac x=1 in exI)
```
```  1195             using \<open>w\<in>S\<close> and T
```
```  1196             apply (auto intro!: exI[where x=T])
```
```  1197             done
```
```  1198         next
```
```  1199           case True
```
```  1200           then obtain a u where au: "T = insert a u" "a\<notin>u"
```
```  1201             apply (drule_tac card_eq_SucD, auto)
```
```  1202             done
```
```  1203           show ?thesis
```
```  1204           proof (cases "u = {}")
```
```  1205             case True
```
```  1206             then have "x = a" using T(4)[unfolded au] by auto
```
```  1207             show ?thesis unfolding \<open>x = a\<close>
```
```  1208               apply (rule_tac x=a in exI)
```
```  1209               apply (rule_tac x=a in exI)
```
```  1210               apply (rule_tac x=1 in exI)
```
```  1211               using T and \<open>n \<noteq> 0\<close>
```
```  1212               unfolding au
```
```  1213               apply (auto intro!: exI[where x="{a}"])
```
```  1214               done
```
```  1215           next
```
```  1216             case False
```
```  1217             obtain ux vx b where obt: "ux\<ge>0" "vx\<ge>0" "ux + vx = 1"
```
```  1218               "b \<in> convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b"
```
```  1219               using T(4)[unfolded au convex_hull_insert[OF False]]
```
```  1220               by auto
```
```  1221             have *: "1 - vx = ux" using obt(3) by auto
```
```  1222             show ?thesis
```
```  1223               apply (rule_tac x=a in exI)
```
```  1224               apply (rule_tac x=b in exI)
```
```  1225               apply (rule_tac x=vx in exI)
```
```  1226               using obt and T(1-3)
```
```  1227               unfolding au and * using card_insert_disjoint[OF _ au(2)]
```
```  1228               apply (auto intro!: exI[where x=u])
```
```  1229               done
```
```  1230           qed
```
```  1231         qed
```
```  1232       qed
```
```  1233       then show ?thesis
```
```  1234         using compact_convex_combinations[OF assms Suc] by simp
```
```  1235     qed
```
```  1236   qed
```
```  1237 qed
```
```  1238
```
```  1239
```
```  1240 subsection%unimportant \<open>Extremal points of a simplex are some vertices\<close>
```
```  1241
```
```  1242 lemma dist_increases_online:
```
```  1243   fixes a b d :: "'a::real_inner"
```
```  1244   assumes "d \<noteq> 0"
```
```  1245   shows "dist a (b + d) > dist a b \<or> dist a (b - d) > dist a b"
```
```  1246 proof (cases "inner a d - inner b d > 0")
```
```  1247   case True
```
```  1248   then have "0 < inner d d + (inner a d * 2 - inner b d * 2)"
```
```  1249     apply (rule_tac add_pos_pos)
```
```  1250     using assms
```
```  1251     apply auto
```
```  1252     done
```
```  1253   then show ?thesis
```
```  1254     apply (rule_tac disjI2)
```
```  1255     unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
```
```  1256     apply  (simp add: algebra_simps inner_commute)
```
```  1257     done
```
```  1258 next
```
```  1259   case False
```
```  1260   then have "0 < inner d d + (inner b d * 2 - inner a d * 2)"
```
```  1261     apply (rule_tac add_pos_nonneg)
```
```  1262     using assms
```
```  1263     apply auto
```
```  1264     done
```
```  1265   then show ?thesis
```
```  1266     apply (rule_tac disjI1)
```
```  1267     unfolding dist_norm and norm_eq_sqrt_inner and real_sqrt_less_iff
```
```  1268     apply (simp add: algebra_simps inner_commute)
```
```  1269     done
```
```  1270 qed
```
```  1271
```
```  1272 lemma norm_increases_online:
```
```  1273   fixes d :: "'a::real_inner"
```
```  1274   shows "d \<noteq> 0 \<Longrightarrow> norm (a + d) > norm a \<or> norm(a - d) > norm a"
```
```  1275   using dist_increases_online[of d a 0] unfolding dist_norm by auto
```
```  1276
```
```  1277 lemma simplex_furthest_lt:
```
```  1278   fixes S :: "'a::real_inner set"
```
```  1279   assumes "finite S"
```
```  1280   shows "\<forall>x \<in> convex hull S.  x \<notin> S \<longrightarrow> (\<exists>y \<in> convex hull S. norm (x - a) < norm(y - a))"
```
```  1281   using assms
```
```  1282 proof induct
```
```  1283   fix x S
```
```  1284   assume as: "finite S" "x\<notin>S" "\<forall>x\<in>convex hull S. x \<notin> S \<longrightarrow> (\<exists>y\<in>convex hull S. norm (x - a) < norm (y - a))"
```
```  1285   show "\<forall>xa\<in>convex hull insert x S. xa \<notin> insert x S \<longrightarrow>
```
```  1286     (\<exists>y\<in>convex hull insert x S. norm (xa - a) < norm (y - a))"
```
```  1287   proof (intro impI ballI, cases "S = {}")
```
```  1288     case False
```
```  1289     fix y
```
```  1290     assume y: "y \<in> convex hull insert x S" "y \<notin> insert x S"
```
```  1291     obtain u v b where obt: "u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull S" "y = u *\<^sub>R x + v *\<^sub>R b"
```
```  1292       using y(1)[unfolded convex_hull_insert[OF False]] by auto
```
```  1293     show "\<exists>z\<in>convex hull insert x S. norm (y - a) < norm (z - a)"
```
```  1294     proof (cases "y \<in> convex hull S")
```
```  1295       case True
```
```  1296       then obtain z where "z \<in> convex hull S" "norm (y - a) < norm (z - a)"
```
```  1297         using as(3)[THEN bspec[where x=y]] and y(2) by auto
```
```  1298       then show ?thesis
```
```  1299         apply (rule_tac x=z in bexI)
```
```  1300         unfolding convex_hull_insert[OF False]
```
```  1301         apply auto
```
```  1302         done
```
```  1303     next
```
```  1304       case False
```
```  1305       show ?thesis
```
```  1306         using obt(3)
```
```  1307       proof (cases "u = 0", case_tac[!] "v = 0")
```
```  1308         assume "u = 0" "v \<noteq> 0"
```
```  1309         then have "y = b" using obt by auto
```
```  1310         then show ?thesis using False and obt(4) by auto
```
```  1311       next
```
```  1312         assume "u \<noteq> 0" "v = 0"
```
```  1313         then have "y = x" using obt by auto
```
```  1314         then show ?thesis using y(2) by auto
```
```  1315       next
```
```  1316         assume "u \<noteq> 0" "v \<noteq> 0"
```
```  1317         then obtain w where w: "w>0" "w<u" "w<v"
```
```  1318           using field_lbound_gt_zero[of u v] and obt(1,2) by auto
```
```  1319         have "x \<noteq> b"
```
```  1320         proof
```
```  1321           assume "x = b"
```
```  1322           then have "y = b" unfolding obt(5)
```
```  1323             using obt(3) by (auto simp: scaleR_left_distrib[symmetric])
```
```  1324           then show False using obt(4) and False by simp
```
```  1325         qed
```
```  1326         then have *: "w *\<^sub>R (x - b) \<noteq> 0" using w(1) by auto
```
```  1327         show ?thesis
```
```  1328           using dist_increases_online[OF *, of a y]
```
```  1329         proof (elim disjE)
```
```  1330           assume "dist a y < dist a (y + w *\<^sub>R (x - b))"
```
```  1331           then have "norm (y - a) < norm ((u + w) *\<^sub>R x + (v - w) *\<^sub>R b - a)"
```
```  1332             unfolding dist_commute[of a]
```
```  1333             unfolding dist_norm obt(5)
```
```  1334             by (simp add: algebra_simps)
```
```  1335           moreover have "(u + w) *\<^sub>R x + (v - w) *\<^sub>R b \<in> convex hull insert x S"
```
```  1336             unfolding convex_hull_insert[OF \<open>S\<noteq>{}\<close>]
```
```  1337           proof (intro CollectI conjI exI)
```
```  1338             show "u + w \<ge> 0" "v - w \<ge> 0"
```
```  1339               using obt(1) w by auto
```
```  1340           qed (use obt in auto)
```
```  1341           ultimately show ?thesis by auto
```
```  1342         next
```
```  1343           assume "dist a y < dist a (y - w *\<^sub>R (x - b))"
```
```  1344           then have "norm (y - a) < norm ((u - w) *\<^sub>R x + (v + w) *\<^sub>R b - a)"
```
```  1345             unfolding dist_commute[of a]
```
```  1346             unfolding dist_norm obt(5)
```
```  1347             by (simp add: algebra_simps)
```
```  1348           moreover have "(u - w) *\<^sub>R x + (v + w) *\<^sub>R b \<in> convex hull insert x S"
```
```  1349             unfolding convex_hull_insert[OF \<open>S\<noteq>{}\<close>]
```
```  1350           proof (intro CollectI conjI exI)
```
```  1351             show "u - w \<ge> 0" "v + w \<ge> 0"
```
```  1352               using obt(1) w by auto
```
```  1353           qed (use obt in auto)
```
```  1354           ultimately show ?thesis by auto
```
```  1355         qed
```
```  1356       qed auto
```
```  1357     qed
```
```  1358   qed auto
```
```  1359 qed (auto simp: assms)
```
```  1360
```
```  1361 lemma simplex_furthest_le:
```
```  1362   fixes S :: "'a::real_inner set"
```
```  1363   assumes "finite S"
```
```  1364     and "S \<noteq> {}"
```
```  1365   shows "\<exists>y\<in>S. \<forall>x\<in> convex hull S. norm (x - a) \<le> norm (y - a)"
```
```  1366 proof -
```
```  1367   have "convex hull S \<noteq> {}"
```
```  1368     using hull_subset[of S convex] and assms(2) by auto
```
```  1369   then obtain x where x: "x \<in> convex hull S" "\<forall>y\<in>convex hull S. norm (y - a) \<le> norm (x - a)"
```
```  1370     using distance_attains_sup[OF finite_imp_compact_convex_hull[OF \<open>finite S\<close>], of a]
```
```  1371     unfolding dist_commute[of a]
```
```  1372     unfolding dist_norm
```
```  1373     by auto
```
```  1374   show ?thesis
```
```  1375   proof (cases "x \<in> S")
```
```  1376     case False
```
```  1377     then obtain y where "y \<in> convex hull S" "norm (x - a) < norm (y - a)"
```
```  1378       using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1)
```
```  1379       by auto
```
```  1380     then show ?thesis
```
```  1381       using x(2)[THEN bspec[where x=y]] by auto
```
```  1382   next
```
```  1383     case True
```
```  1384     with x show ?thesis by auto
```
```  1385   qed
```
```  1386 qed
```
```  1387
```
```  1388 lemma simplex_furthest_le_exists:
```
```  1389   fixes S :: "('a::real_inner) set"
```
```  1390   shows "finite S \<Longrightarrow> \<forall>x\<in>(convex hull S). \<exists>y\<in>S. norm (x - a) \<le> norm (y - a)"
```
```  1391   using simplex_furthest_le[of S] by (cases "S = {}") auto
```
```  1392
```
```  1393 lemma simplex_extremal_le:
```
```  1394   fixes S :: "'a::real_inner set"
```
```  1395   assumes "finite S"
```
```  1396     and "S \<noteq> {}"
```
```  1397   shows "\<exists>u\<in>S. \<exists>v\<in>S. \<forall>x\<in>convex hull S. \<forall>y \<in> convex hull S. norm (x - y) \<le> norm (u - v)"
```
```  1398 proof -
```
```  1399   have "convex hull S \<noteq> {}"
```
```  1400     using hull_subset[of S convex] and assms(2) by auto
```
```  1401   then obtain u v where obt: "u \<in> convex hull S" "v \<in> convex hull S"
```
```  1402     "\<forall>x\<in>convex hull S. \<forall>y\<in>convex hull S. norm (x - y) \<le> norm (u - v)"
```
```  1403     using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]]
```
```  1404     by (auto simp: dist_norm)
```
```  1405   then show ?thesis
```
```  1406   proof (cases "u\<notin>S \<or> v\<notin>S", elim disjE)
```
```  1407     assume "u \<notin> S"
```
```  1408     then obtain y where "y \<in> convex hull S" "norm (u - v) < norm (y - v)"
```
```  1409       using simplex_furthest_lt[OF assms(1), THEN bspec[where x=u]] and obt(1)
```
```  1410       by auto
```
```  1411     then show ?thesis
```
```  1412       using obt(3)[THEN bspec[where x=y], THEN bspec[where x=v]] and obt(2)
```
```  1413       by auto
```
```  1414   next
```
```  1415     assume "v \<notin> S"
```
```  1416     then obtain y where "y \<in> convex hull S" "norm (v - u) < norm (y - u)"
```
```  1417       using simplex_furthest_lt[OF assms(1), THEN bspec[where x=v]] and obt(2)
```
```  1418       by auto
```
```  1419     then show ?thesis
```
```  1420       using obt(3)[THEN bspec[where x=u], THEN bspec[where x=y]] and obt(1)
```
```  1421       by (auto simp: norm_minus_commute)
```
```  1422   qed auto
```
```  1423 qed
```
```  1424
```
```  1425 lemma simplex_extremal_le_exists:
```
```  1426   fixes S :: "'a::real_inner set"
```
```  1427   shows "finite S \<Longrightarrow> x \<in> convex hull S \<Longrightarrow> y \<in> convex hull S \<Longrightarrow>
```
```  1428     \<exists>u\<in>S. \<exists>v\<in>S. norm (x - y) \<le> norm (u - v)"
```
```  1429   using convex_hull_empty simplex_extremal_le[of S]
```
```  1430   by(cases "S = {}") auto
```
```  1431
```
```  1432
```
```  1433 subsection \<open>Closest point of a convex set is unique, with a continuous projection\<close>
```
```  1434
```
```  1435 definition%important closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
```
```  1436   where "closest_point S a = (SOME x. x \<in> S \<and> (\<forall>y\<in>S. dist a x \<le> dist a y))"
```
```  1437
```
```  1438 lemma closest_point_exists:
```
```  1439   assumes "closed S"
```
```  1440     and "S \<noteq> {}"
```
```  1441   shows "closest_point S a \<in> S"
```
```  1442     and "\<forall>y\<in>S. dist a (closest_point S a) \<le> dist a y"
```
```  1443   unfolding closest_point_def
```
```  1444   apply(rule_tac[!] someI2_ex)
```
```  1445   apply (auto intro: distance_attains_inf[OF assms(1,2), of a])
```
```  1446   done
```
```  1447
```
```  1448 lemma closest_point_in_set: "closed S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> closest_point S a \<in> S"
```
```  1449   by (meson closest_point_exists)
```
```  1450
```
```  1451 lemma closest_point_le: "closed S \<Longrightarrow> x \<in> S \<Longrightarrow> dist a (closest_point S a) \<le> dist a x"
```
```  1452   using closest_point_exists[of S] by auto
```
```  1453
```
```  1454 lemma closest_point_self:
```
```  1455   assumes "x \<in> S"
```
```  1456   shows "closest_point S x = x"
```
```  1457   unfolding closest_point_def
```
```  1458   apply (rule some1_equality, rule ex1I[of _ x])
```
```  1459   using assms
```
```  1460   apply auto
```
```  1461   done
```
```  1462
```
```  1463 lemma closest_point_refl: "closed S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> closest_point S x = x \<longleftrightarrow> x \<in> S"
```
```  1464   using closest_point_in_set[of S x] closest_point_self[of x S]
```
```  1465   by auto
```
```  1466
```
```  1467 lemma closer_points_lemma:
```
```  1468   assumes "inner y z > 0"
```
```  1469   shows "\<exists>u>0. \<forall>v>0. v \<le> u \<longrightarrow> norm(v *\<^sub>R z - y) < norm y"
```
```  1470 proof -
```
```  1471   have z: "inner z z > 0"
```
```  1472     unfolding inner_gt_zero_iff using assms by auto
```
```  1473   have "norm (v *\<^sub>R z - y) < norm y"
```
```  1474     if "0 < v" and "v \<le> inner y z / inner z z" for v
```
```  1475     unfolding norm_lt using z assms that
```
```  1476     by (simp add: field_simps inner_diff inner_commute mult_strict_left_mono[OF _ \<open>0<v\<close>])
```
```  1477   then show ?thesis
```
```  1478     using assms z
```
```  1479     by (rule_tac x = "inner y z / inner z z" in exI) auto
```
```  1480 qed
```
```  1481
```
```  1482 lemma closer_point_lemma:
```
```  1483   assumes "inner (y - x) (z - x) > 0"
```
```  1484   shows "\<exists>u>0. u \<le> 1 \<and> dist (x + u *\<^sub>R (z - x)) y < dist x y"
```
```  1485 proof -
```
```  1486   obtain u where "u > 0"
```
```  1487     and u: "\<forall>v>0. v \<le> u \<longrightarrow> norm (v *\<^sub>R (z - x) - (y - x)) < norm (y - x)"
```
```  1488     using closer_points_lemma[OF assms] by auto
```
```  1489   show ?thesis
```
```  1490     apply (rule_tac x="min u 1" in exI)
```
```  1491     using u[THEN spec[where x="min u 1"]] and \<open>u > 0\<close>
```
```  1492     unfolding dist_norm by (auto simp: norm_minus_commute field_simps)
```
```  1493 qed
```
```  1494
```
```  1495 lemma any_closest_point_dot:
```
```  1496   assumes "convex S" "closed S" "x \<in> S" "y \<in> S" "\<forall>z\<in>S. dist a x \<le> dist a z"
```
```  1497   shows "inner (a - x) (y - x) \<le> 0"
```
```  1498 proof (rule ccontr)
```
```  1499   assume "\<not> ?thesis"
```
```  1500   then obtain u where u: "u>0" "u\<le>1" "dist (x + u *\<^sub>R (y - x)) a < dist x a"
```
```  1501     using closer_point_lemma[of a x y] by auto
```
```  1502   let ?z = "(1 - u) *\<^sub>R x + u *\<^sub>R y"
```
```  1503   have "?z \<in> S"
```
```  1504     using convexD_alt[OF assms(1,3,4), of u] using u by auto
```
```  1505   then show False
```
```  1506     using assms(5)[THEN bspec[where x="?z"]] and u(3)
```
```  1507     by (auto simp: dist_commute algebra_simps)
```
```  1508 qed
```
```  1509
```
```  1510 lemma any_closest_point_unique:
```
```  1511   fixes x :: "'a::real_inner"
```
```  1512   assumes "convex S" "closed S" "x \<in> S" "y \<in> S"
```
```  1513     "\<forall>z\<in>S. dist a x \<le> dist a z" "\<forall>z\<in>S. dist a y \<le> dist a z"
```
```  1514   shows "x = y"
```
```  1515   using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)]
```
```  1516   unfolding norm_pths(1) and norm_le_square
```
```  1517   by (auto simp: algebra_simps)
```
```  1518
```
```  1519 lemma closest_point_unique:
```
```  1520   assumes "convex S" "closed S" "x \<in> S" "\<forall>z\<in>S. dist a x \<le> dist a z"
```
```  1521   shows "x = closest_point S a"
```
```  1522   using any_closest_point_unique[OF assms(1-3) _ assms(4), of "closest_point S a"]
```
```  1523   using closest_point_exists[OF assms(2)] and assms(3) by auto
```
```  1524
```
```  1525 lemma closest_point_dot:
```
```  1526   assumes "convex S" "closed S" "x \<in> S"
```
```  1527   shows "inner (a - closest_point S a) (x - closest_point S a) \<le> 0"
```
```  1528   apply (rule any_closest_point_dot[OF assms(1,2) _ assms(3)])
```
```  1529   using closest_point_exists[OF assms(2)] and assms(3)
```
```  1530   apply auto
```
```  1531   done
```
```  1532
```
```  1533 lemma closest_point_lt:
```
```  1534   assumes "convex S" "closed S" "x \<in> S" "x \<noteq> closest_point S a"
```
```  1535   shows "dist a (closest_point S a) < dist a x"
```
```  1536   apply (rule ccontr)
```
```  1537   apply (rule_tac notE[OF assms(4)])
```
```  1538   apply (rule closest_point_unique[OF assms(1-3), of a])
```
```  1539   using closest_point_le[OF assms(2), of _ a]
```
```  1540   apply fastforce
```
```  1541   done
```
```  1542
```
```  1543 lemma setdist_closest_point:
```
```  1544     "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> setdist {a} S = dist a (closest_point S a)"
```
```  1545   apply (rule setdist_unique)
```
```  1546   using closest_point_le
```
```  1547   apply (auto simp: closest_point_in_set)
```
```  1548   done
```
```  1549
```
```  1550 lemma closest_point_lipschitz:
```
```  1551   assumes "convex S"
```
```  1552     and "closed S" "S \<noteq> {}"
```
```  1553   shows "dist (closest_point S x) (closest_point S y) \<le> dist x y"
```
```  1554 proof -
```
```  1555   have "inner (x - closest_point S x) (closest_point S y - closest_point S x) \<le> 0"
```
```  1556     and "inner (y - closest_point S y) (closest_point S x - closest_point S y) \<le> 0"
```
```  1557     apply (rule_tac[!] any_closest_point_dot[OF assms(1-2)])
```
```  1558     using closest_point_exists[OF assms(2-3)]
```
```  1559     apply auto
```
```  1560     done
```
```  1561   then show ?thesis unfolding dist_norm and norm_le
```
```  1562     using inner_ge_zero[of "(x - closest_point S x) - (y - closest_point S y)"]
```
```  1563     by (simp add: inner_add inner_diff inner_commute)
```
```  1564 qed
```
```  1565
```
```  1566 lemma continuous_at_closest_point:
```
```  1567   assumes "convex S"
```
```  1568     and "closed S"
```
```  1569     and "S \<noteq> {}"
```
```  1570   shows "continuous (at x) (closest_point S)"
```
```  1571   unfolding continuous_at_eps_delta
```
```  1572   using le_less_trans[OF closest_point_lipschitz[OF assms]] by auto
```
```  1573
```
```  1574 lemma continuous_on_closest_point:
```
```  1575   assumes "convex S"
```
```  1576     and "closed S"
```
```  1577     and "S \<noteq> {}"
```
```  1578   shows "continuous_on t (closest_point S)"
```
```  1579   by (metis continuous_at_imp_continuous_on continuous_at_closest_point[OF assms])
```
```  1580
```
```  1581 proposition closest_point_in_rel_interior:
```
```  1582   assumes "closed S" "S \<noteq> {}" and x: "x \<in> affine hull S"
```
```  1583     shows "closest_point S x \<in> rel_interior S \<longleftrightarrow> x \<in> rel_interior S"
```
```  1584 proof (cases "x \<in> S")
```
```  1585   case True
```
```  1586   then show ?thesis
```
```  1587     by (simp add: closest_point_self)
```
```  1588 next
```
```  1589   case False
```
```  1590   then have "False" if asm: "closest_point S x \<in> rel_interior S"
```
```  1591   proof -
```
```  1592     obtain e where "e > 0" and clox: "closest_point S x \<in> S"
```
```  1593                and e: "cball (closest_point S x) e \<inter> affine hull S \<subseteq> S"
```
```  1594       using asm mem_rel_interior_cball by blast
```
```  1595     then have clo_notx: "closest_point S x \<noteq> x"
```
```  1596       using \<open>x \<notin> S\<close> by auto
```
```  1597     define y where "y \<equiv> closest_point S x -
```
```  1598                         (min 1 (e / norm(closest_point S x - x))) *\<^sub>R (closest_point S x - x)"
```
```  1599     have "x - y = (1 - min 1 (e / norm (closest_point S x - x))) *\<^sub>R (x - closest_point S x)"
```
```  1600       by (simp add: y_def algebra_simps)
```
```  1601     then have "norm (x - y) = abs ((1 - min 1 (e / norm (closest_point S x - x)))) * norm(x - closest_point S x)"
```
```  1602       by simp
```
```  1603     also have "\<dots> < norm(x - closest_point S x)"
```
```  1604       using clo_notx \<open>e > 0\<close>
```
```  1605       by (auto simp: mult_less_cancel_right2 divide_simps)
```
```  1606     finally have no_less: "norm (x - y) < norm (x - closest_point S x)" .
```
```  1607     have "y \<in> affine hull S"
```
```  1608       unfolding y_def
```
```  1609       by (meson affine_affine_hull clox hull_subset mem_affine_3_minus2 subsetD x)
```
```  1610     moreover have "dist (closest_point S x) y \<le> e"
```
```  1611       using \<open>e > 0\<close> by (auto simp: y_def min_mult_distrib_right)
```
```  1612     ultimately have "y \<in> S"
```
```  1613       using subsetD [OF e] by simp
```
```  1614     then have "dist x (closest_point S x) \<le> dist x y"
```
```  1615       by (simp add: closest_point_le \<open>closed S\<close>)
```
```  1616     with no_less show False
```
```  1617       by (simp add: dist_norm)
```
```  1618   qed
```
```  1619   moreover have "x \<notin> rel_interior S"
```
```  1620     using rel_interior_subset False by blast
```
```  1621   ultimately show ?thesis by blast
```
```  1622 qed
```
```  1623
```
```  1624
```
```  1625 subsubsection%unimportant \<open>Various point-to-set separating/supporting hyperplane theorems\<close>
```
```  1626
```
```  1627 lemma supporting_hyperplane_closed_point:
```
```  1628   fixes z :: "'a::{real_inner,heine_borel}"
```
```  1629   assumes "convex S"
```
```  1630     and "closed S"
```
```  1631     and "S \<noteq> {}"
```
```  1632     and "z \<notin> S"
```
```  1633   shows "\<exists>a b. \<exists>y\<in>S. inner a z < b \<and> inner a y = b \<and> (\<forall>x\<in>S. inner a x \<ge> b)"
```
```  1634 proof -
```
```  1635   obtain y where "y \<in> S" and y: "\<forall>x\<in>S. dist z y \<le> dist z x"
```
```  1636     by (metis distance_attains_inf[OF assms(2-3)])
```
```  1637   show ?thesis
```
```  1638   proof (intro exI bexI conjI ballI)
```
```  1639     show "(y - z) \<bullet> z < (y - z) \<bullet> y"
```
```  1640       by (metis \<open>y \<in> S\<close> assms(4) diff_gt_0_iff_gt inner_commute inner_diff_left inner_gt_zero_iff right_minus_eq)
```
```  1641     show "(y - z) \<bullet> y \<le> (y - z) \<bullet> x" if "x \<in> S" for x
```
```  1642     proof (rule ccontr)
```
```  1643       have *: "\<And>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> dist z y \<le> dist z ((1 - u) *\<^sub>R y + u *\<^sub>R x)"
```
```  1644         using assms(1)[unfolded convex_alt] and y and \<open>x\<in>S\<close> and \<open>y\<in>S\<close> by auto
```
```  1645       assume "\<not> (y - z) \<bullet> y \<le> (y - z) \<bullet> x"
```
```  1646       then obtain v where "v > 0" "v \<le> 1" "dist (y + v *\<^sub>R (x - y)) z < dist y z"
```
```  1647         using closer_point_lemma[of z y x] by (auto simp: inner_diff)
```
```  1648       then show False
```
```  1649         using *[of v] by (auto simp: dist_commute algebra_simps)
```
```  1650     qed
```
```  1651   qed (use \<open>y \<in> S\<close> in auto)
```
```  1652 qed
```
```  1653
```
```  1654 lemma separating_hyperplane_closed_point:
```
```  1655   fixes z :: "'a::{real_inner,heine_borel}"
```
```  1656   assumes "convex S"
```
```  1657     and "closed S"
```
```  1658     and "z \<notin> S"
```
```  1659   shows "\<exists>a b. inner a z < b \<and> (\<forall>x\<in>S. inner a x > b)"
```
```  1660 proof (cases "S = {}")
```
```  1661   case True
```
```  1662   then show ?thesis
```
```  1663     by (simp add: gt_ex)
```
```  1664 next
```
```  1665   case False
```
```  1666   obtain y where "y \<in> S" and y: "\<And>x. x \<in> S \<Longrightarrow> dist z y \<le> dist z x"
```
```  1667     by (metis distance_attains_inf[OF assms(2) False])
```
```  1668   show ?thesis
```
```  1669   proof (intro exI conjI ballI)
```
```  1670     show "(y - z) \<bullet> z < inner (y - z) z + (norm (y - z))\<^sup>2 / 2"
```
```  1671       using \<open>y\<in>S\<close> \<open>z\<notin>S\<close> by auto
```
```  1672   next
```
```  1673     fix x
```
```  1674     assume "x \<in> S"
```
```  1675     have "False" if *: "0 < inner (z - y) (x - y)"
```
```  1676     proof -
```
```  1677       obtain u where "u > 0" "u \<le> 1" "dist (y + u *\<^sub>R (x - y)) z < dist y z"
```
```  1678         using * closer_point_lemma by blast
```
```  1679       then show False using y[of "y + u *\<^sub>R (x - y)"] convexD_alt [OF \<open>convex S\<close>]
```
```  1680         using \<open>x\<in>S\<close> \<open>y\<in>S\<close> by (auto simp: dist_commute algebra_simps)
```
```  1681     qed
```
```  1682     moreover have "0 < (norm (y - z))\<^sup>2"
```
```  1683       using \<open>y\<in>S\<close> \<open>z\<notin>S\<close> by auto
```
```  1684     then have "0 < inner (y - z) (y - z)"
```
```  1685       unfolding power2_norm_eq_inner by simp
```
```  1686     ultimately show "(y - z) \<bullet> z + (norm (y - z))\<^sup>2 / 2 < (y - z) \<bullet> x"
```
```  1687       by (force simp: field_simps power2_norm_eq_inner inner_commute inner_diff)
```
```  1688   qed
```
```  1689 qed
```
```  1690
```
```  1691 lemma separating_hyperplane_closed_0:
```
```  1692   assumes "convex (S::('a::euclidean_space) set)"
```
```  1693     and "closed S"
```
```  1694     and "0 \<notin> S"
```
```  1695   shows "\<exists>a b. a \<noteq> 0 \<and> 0 < b \<and> (\<forall>x\<in>S. inner a x > b)"
```
```  1696 proof (cases "S = {}")
```
```  1697   case True
```
```  1698   have "(SOME i. i\<in>Basis) \<noteq> (0::'a)"
```
```  1699     by (metis Basis_zero SOME_Basis)
```
```  1700   then show ?thesis
```
```  1701     using True zero_less_one by blast
```
```  1702 next
```
```  1703   case False
```
```  1704   then show ?thesis
```
```  1705     using False using separating_hyperplane_closed_point[OF assms]
```
```  1706     by (metis all_not_in_conv inner_zero_left inner_zero_right less_eq_real_def not_le)
```
```  1707 qed
```
```  1708
```
```  1709
```
```  1710 subsubsection%unimportant \<open>Now set-to-set for closed/compact sets\<close>
```
```  1711
```
```  1712 lemma separating_hyperplane_closed_compact:
```
```  1713   fixes S :: "'a::euclidean_space set"
```
```  1714   assumes "convex S"
```
```  1715     and "closed S"
```
```  1716     and "convex T"
```
```  1717     and "compact T"
```
```  1718     and "T \<noteq> {}"
```
```  1719     and "S \<inter> T = {}"
```
```  1720   shows "\<exists>a b. (\<forall>x\<in>S. inner a x < b) \<and> (\<forall>x\<in>T. inner a x > b)"
```
```  1721 proof (cases "S = {}")
```
```  1722   case True
```
```  1723   obtain b where b: "b > 0" "\<forall>x\<in>T. norm x \<le> b"
```
```  1724     using compact_imp_bounded[OF assms(4)] unfolding bounded_pos by auto
```
```  1725   obtain z :: 'a where z: "norm z = b + 1"
```
```  1726     using vector_choose_size[of "b + 1"] and b(1) by auto
```
```  1727   then have "z \<notin> T" using b(2)[THEN bspec[where x=z]] by auto
```
```  1728   then obtain a b where ab: "inner a z < b" "\<forall>x\<in>T. b < inner a x"
```
```  1729     using separating_hyperplane_closed_point[OF assms(3) compact_imp_closed[OF assms(4)], of z]
```
```  1730     by auto
```
```  1731   then show ?thesis
```
```  1732     using True by auto
```
```  1733 next
```
```  1734   case False
```
```  1735   then obtain y where "y \<in> S" by auto
```
```  1736   obtain a b where "0 < b" "\<forall>x \<in> (\<Union>x\<in> S. \<Union>y \<in> T. {x - y}). b < inner a x"
```
```  1737     using separating_hyperplane_closed_point[OF convex_differences[OF assms(1,3)], of 0]
```
```  1738     using closed_compact_differences[OF assms(2,4)]
```
```  1739     using assms(6) by auto
```
```  1740   then have ab: "\<forall>x\<in>S. \<forall>y\<in>T. b + inner a y < inner a x"
```
```  1741     apply -
```
```  1742     apply rule
```
```  1743     apply rule
```
```  1744     apply (erule_tac x="x - y" in ballE)
```
```  1745     apply (auto simp: inner_diff)
```
```  1746     done
```
```  1747   define k where "k = (SUP x\<in>T. a \<bullet> x)"
```
```  1748   show ?thesis
```
```  1749     apply (rule_tac x="-a" in exI)
```
```  1750     apply (rule_tac x="-(k + b / 2)" in exI)
```
```  1751     apply (intro conjI ballI)
```
```  1752     unfolding inner_minus_left and neg_less_iff_less
```
```  1753   proof -
```
```  1754     fix x assume "x \<in> T"
```
```  1755     then have "inner a x - b / 2 < k"
```
```  1756       unfolding k_def
```
```  1757     proof (subst less_cSUP_iff)
```
```  1758       show "T \<noteq> {}" by fact
```
```  1759       show "bdd_above ((\<bullet>) a ` T)"
```
```  1760         using ab[rule_format, of y] \<open>y \<in> S\<close>
```
```  1761         by (intro bdd_aboveI2[where M="inner a y - b"]) (auto simp: field_simps intro: less_imp_le)
```
```  1762     qed (auto intro!: bexI[of _ x] \<open>0<b\<close>)
```
```  1763     then show "inner a x < k + b / 2"
```
```  1764       by auto
```
```  1765   next
```
```  1766     fix x
```
```  1767     assume "x \<in> S"
```
```  1768     then have "k \<le> inner a x - b"
```
```  1769       unfolding k_def
```
```  1770       apply (rule_tac cSUP_least)
```
```  1771       using assms(5)
```
```  1772       using ab[THEN bspec[where x=x]]
```
```  1773       apply auto
```
```  1774       done
```
```  1775     then show "k + b / 2 < inner a x"
```
```  1776       using \<open>0 < b\<close> by auto
```
```  1777   qed
```
```  1778 qed
```
```  1779
```
```  1780 lemma separating_hyperplane_compact_closed:
```
```  1781   fixes S :: "'a::euclidean_space set"
```
```  1782   assumes "convex S"
```
```  1783     and "compact S"
```
```  1784     and "S \<noteq> {}"
```
```  1785     and "convex T"
```
```  1786     and "closed T"
```
```  1787     and "S \<inter> T = {}"
```
```  1788   shows "\<exists>a b. (\<forall>x\<in>S. inner a x < b) \<and> (\<forall>x\<in>T. inner a x > b)"
```
```  1789 proof -
```
```  1790   obtain a b where "(\<forall>x\<in>T. inner a x < b) \<and> (\<forall>x\<in>S. b < inner a x)"
```
```  1791     using separating_hyperplane_closed_compact[OF assms(4-5,1-2,3)] and assms(6)
```
```  1792     by auto
```
```  1793   then show ?thesis
```
```  1794     apply (rule_tac x="-a" in exI)
```
```  1795     apply (rule_tac x="-b" in exI, auto)
```
```  1796     done
```
```  1797 qed
```
```  1798
```
```  1799
```
```  1800 subsubsection%unimportant \<open>General case without assuming closure and getting non-strict separation\<close>
```
```  1801
```
```  1802 lemma separating_hyperplane_set_0:
```
```  1803   assumes "convex S" "(0::'a::euclidean_space) \<notin> S"
```
```  1804   shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>S. 0 \<le> inner a x)"
```
```  1805 proof -
```
```  1806   let ?k = "\<lambda>c. {x::'a. 0 \<le> inner c x}"
```
```  1807   have *: "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" if as: "f \<subseteq> ?k ` S" "finite f" for f
```
```  1808   proof -
```
```  1809     obtain c where c: "f = ?k ` c" "c \<subseteq> S" "finite c"
```
```  1810       using finite_subset_image[OF as(2,1)] by auto
```
```  1811     then obtain a b where ab: "a \<noteq> 0" "0 < b" "\<forall>x\<in>convex hull c. b < inner a x"
```
```  1812       using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
```
```  1813       using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2)
```
```  1814       using subset_hull[of convex, OF assms(1), symmetric, of c]
```
```  1815       by force
```
```  1816     then have "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> inner y x)"
```
```  1817       apply (rule_tac x = "inverse(norm a) *\<^sub>R a" in exI)
```
```  1818       using hull_subset[of c convex]
```
```  1819       unfolding subset_eq and inner_scaleR
```
```  1820       by (auto simp: inner_commute del: ballE elim!: ballE)
```
```  1821     then show "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}"
```
```  1822       unfolding c(1) frontier_cball sphere_def dist_norm by auto
```
```  1823   qed
```
```  1824   have "frontier (cball 0 1) \<inter> (\<Inter>(?k ` S)) \<noteq> {}"
```
```  1825     apply (rule compact_imp_fip)
```
```  1826     apply (rule compact_frontier[OF compact_cball])
```
```  1827     using * closed_halfspace_ge
```
```  1828     by auto
```
```  1829   then obtain x where "norm x = 1" "\<forall>y\<in>S. x\<in>?k y"
```
```  1830     unfolding frontier_cball dist_norm sphere_def by auto
```
```  1831   then show ?thesis
```
```  1832     by (metis inner_commute mem_Collect_eq norm_eq_zero zero_neq_one)
```
```  1833 qed
```
```  1834
```
```  1835 lemma separating_hyperplane_sets:
```
```  1836   fixes S T :: "'a::euclidean_space set"
```
```  1837   assumes "convex S"
```
```  1838     and "convex T"
```
```  1839     and "S \<noteq> {}"
```
```  1840     and "T \<noteq> {}"
```
```  1841     and "S \<inter> T = {}"
```
```  1842   shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>S. inner a x \<le> b) \<and> (\<forall>x\<in>T. inner a x \<ge> b)"
```
```  1843 proof -
```
```  1844   from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
```
```  1845   obtain a where "a \<noteq> 0" "\<forall>x\<in>{x - y |x y. x \<in> T \<and> y \<in> S}. 0 \<le> inner a x"
```
```  1846     using assms(3-5) by force
```
```  1847   then have *: "\<And>x y. x \<in> T \<Longrightarrow> y \<in> S \<Longrightarrow> inner a y \<le> inner a x"
```
```  1848     by (force simp: inner_diff)
```
```  1849   then have bdd: "bdd_above (((\<bullet>) a)`S)"
```
```  1850     using \<open>T \<noteq> {}\<close> by (auto intro: bdd_aboveI2[OF *])
```
```  1851   show ?thesis
```
```  1852     using \<open>a\<noteq>0\<close>
```
```  1853     by (intro exI[of _ a] exI[of _ "SUP x\<in>S. a \<bullet> x"])
```
```  1854        (auto intro!: cSUP_upper bdd cSUP_least \<open>a \<noteq> 0\<close> \<open>S \<noteq> {}\<close> *)
```
```  1855 qed
```
```  1856
```
```  1857
```
```  1858 subsection%unimportant \<open>More convexity generalities\<close>
```
```  1859
```
```  1860 lemma convex_closure [intro,simp]:
```
```  1861   fixes S :: "'a::real_normed_vector set"
```
```  1862   assumes "convex S"
```
```  1863   shows "convex (closure S)"
```
```  1864   apply (rule convexI)
```
```  1865   apply (unfold closure_sequential, elim exE)
```
```  1866   apply (rule_tac x="\<lambda>n. u *\<^sub>R xa n + v *\<^sub>R xb n" in exI)
```
```  1867   apply (rule,rule)
```
```  1868   apply (rule convexD [OF assms])
```
```  1869   apply (auto del: tendsto_const intro!: tendsto_intros)
```
```  1870   done
```
```  1871
```
```  1872 lemma convex_interior [intro,simp]:
```
```  1873   fixes S :: "'a::real_normed_vector set"
```
```  1874   assumes "convex S"
```
```  1875   shows "convex (interior S)"
```
```  1876   unfolding convex_alt Ball_def mem_interior
```
```  1877 proof clarify
```
```  1878   fix x y u
```
```  1879   assume u: "0 \<le> u" "u \<le> (1::real)"
```
```  1880   fix e d
```
```  1881   assume ed: "ball x e \<subseteq> S" "ball y d \<subseteq> S" "0<d" "0<e"
```
```  1882   show "\<exists>e>0. ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) e \<subseteq> S"
```
```  1883   proof (intro exI conjI subsetI)
```
```  1884     fix z
```
```  1885     assume "z \<in> ball ((1 - u) *\<^sub>R x + u *\<^sub>R y) (min d e)"
```
```  1886     then have "(1- u) *\<^sub>R (z - u *\<^sub>R (y - x)) + u *\<^sub>R (z + (1 - u) *\<^sub>R (y - x)) \<in> S"
```
```  1887       apply (rule_tac assms[unfolded convex_alt, rule_format])
```
```  1888       using ed(1,2) and u
```
```  1889       unfolding subset_eq mem_ball Ball_def dist_norm
```
```  1890       apply (auto simp: algebra_simps)
```
```  1891       done
```
```  1892     then show "z \<in> S"
```
```  1893       using u by (auto simp: algebra_simps)
```
```  1894   qed(insert u ed(3-4), auto)
```
```  1895 qed
```
```  1896
```
```  1897 lemma convex_hull_eq_empty[simp]: "convex hull S = {} \<longleftrightarrow> S = {}"
```
```  1898   using hull_subset[of S convex] convex_hull_empty by auto
```
```  1899
```
```  1900
```
```  1901 subsection%unimportant \<open>Convex set as intersection of halfspaces\<close>
```
```  1902
```
```  1903 lemma convex_halfspace_intersection:
```
```  1904   fixes s :: "('a::euclidean_space) set"
```
```  1905   assumes "closed s" "convex s"
```
```  1906   shows "s = \<Inter>{h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
```
```  1907   apply (rule set_eqI, rule)
```
```  1908   unfolding Inter_iff Ball_def mem_Collect_eq
```
```  1909   apply (rule,rule,erule conjE)
```
```  1910 proof -
```
```  1911   fix x
```
```  1912   assume "\<forall>xa. s \<subseteq> xa \<and> (\<exists>a b. xa = {x. inner a x \<le> b}) \<longrightarrow> x \<in> xa"
```
```  1913   then have "\<forall>a b. s \<subseteq> {x. inner a x \<le> b} \<longrightarrow> x \<in> {x. inner a x \<le> b}"
```
```  1914     by blast
```
```  1915   then show "x \<in> s"
```
```  1916     apply (rule_tac ccontr)
```
```  1917     apply (drule separating_hyperplane_closed_point[OF assms(2,1)])
```
```  1918     apply (erule exE)+
```
```  1919     apply (erule_tac x="-a" in allE)
```
```  1920     apply (erule_tac x="-b" in allE, auto)
```
```  1921     done
```
```  1922 qed auto
```
```  1923
```
```  1924
```
```  1925 subsection%unimportant \<open>Convexity of general and special intervals\<close>
```
```  1926
```
```  1927 lemma is_interval_convex:
```
```  1928   fixes S :: "'a::euclidean_space set"
```
```  1929   assumes "is_interval S"
```
```  1930   shows "convex S"
```
```  1931 proof (rule convexI)
```
```  1932   fix x y and u v :: real
```
```  1933   assume as: "x \<in> S" "y \<in> S" "0 \<le> u" "0 \<le> v" "u + v = 1"
```
```  1934   then have *: "u = 1 - v" "1 - v \<ge> 0" and **: "v = 1 - u" "1 - u \<ge> 0"
```
```  1935     by auto
```
```  1936   {
```
```  1937     fix a b
```
```  1938     assume "\<not> b \<le> u * a + v * b"
```
```  1939     then have "u * a < (1 - v) * b"
```
```  1940       unfolding not_le using as(4) by (auto simp: field_simps)
```
```  1941     then have "a < b"
```
```  1942       unfolding * using as(4) *(2)
```
```  1943       apply (rule_tac mult_left_less_imp_less[of "1 - v"])
```
```  1944       apply (auto simp: field_simps)
```
```  1945       done
```
```  1946     then have "a \<le> u * a + v * b"
```
```  1947       unfolding * using as(4)
```
```  1948       by (auto simp: field_simps intro!:mult_right_mono)
```
```  1949   }
```
```  1950   moreover
```
```  1951   {
```
```  1952     fix a b
```
```  1953     assume "\<not> u * a + v * b \<le> a"
```
```  1954     then have "v * b > (1 - u) * a"
```
```  1955       unfolding not_le using as(4) by (auto simp: field_simps)
```
```  1956     then have "a < b"
```
```  1957       unfolding * using as(4)
```
```  1958       apply (rule_tac mult_left_less_imp_less)
```
```  1959       apply (auto simp: field_simps)
```
```  1960       done
```
```  1961     then have "u * a + v * b \<le> b"
```
```  1962       unfolding **
```
```  1963       using **(2) as(3)
```
```  1964       by (auto simp: field_simps intro!:mult_right_mono)
```
```  1965   }
```
```  1966   ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> S"
```
```  1967     apply -
```
```  1968     apply (rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
```
```  1969     using as(3-) DIM_positive[where 'a='a]
```
```  1970     apply (auto simp: inner_simps)
```
```  1971     done
```
```  1972 qed
```
```  1973
```
```  1974 lemma is_interval_connected:
```
```  1975   fixes S :: "'a::euclidean_space set"
```
```  1976   shows "is_interval S \<Longrightarrow> connected S"
```
```  1977   using is_interval_convex convex_connected by auto
```
```  1978
```
```  1979 lemma convex_box [simp]: "convex (cbox a b)" "convex (box a (b::'a::euclidean_space))"
```
```  1980   apply (rule_tac[!] is_interval_convex)+
```
```  1981   using is_interval_box is_interval_cbox
```
```  1982   apply auto
```
```  1983   done
```
```  1984
```
```  1985 text\<open>A non-singleton connected set is perfect (i.e. has no isolated points). \<close>
```
```  1986 lemma connected_imp_perfect:
```
```  1987   fixes a :: "'a::metric_space"
```
```  1988   assumes "connected S" "a \<in> S" and S: "\<And>x. S \<noteq> {x}"
```
```  1989   shows "a islimpt S"
```
```  1990 proof -
```
```  1991   have False if "a \<in> T" "open T" "\<And>y. \<lbrakk>y \<in> S; y \<in> T\<rbrakk> \<Longrightarrow> y = a" for T
```
```  1992   proof -
```
```  1993     obtain e where "e > 0" and e: "cball a e \<subseteq> T"
```
```  1994       using \<open>open T\<close> \<open>a \<in> T\<close> by (auto simp: open_contains_cball)
```
```  1995     have "openin (top_of_set S) {a}"
```
```  1996       unfolding openin_open using that \<open>a \<in> S\<close> by blast
```
```  1997     moreover have "closedin (top_of_set S) {a}"
```
```  1998       by (simp add: assms)
```
```  1999     ultimately show "False"
```
```  2000       using \<open>connected S\<close> connected_clopen S by blast
```
```  2001   qed
```
```  2002   then show ?thesis
```
```  2003     unfolding islimpt_def by blast
```
```  2004 qed
```
```  2005
```
```  2006 lemma connected_imp_perfect_aff_dim:
```
```  2007      "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
```
```  2008   using aff_dim_sing connected_imp_perfect by blast
```
```  2009
```
```  2010 subsection%unimportant \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent\<close>
```
```  2011
```
```  2012 lemma mem_is_interval_1_I:
```
```  2013   fixes a b c::real
```
```  2014   assumes "is_interval S"
```
```  2015   assumes "a \<in> S" "c \<in> S"
```
```  2016   assumes "a \<le> b" "b \<le> c"
```
```  2017   shows "b \<in> S"
```
```  2018   using assms is_interval_1 by blast
```
```  2019
```
```  2020 lemma is_interval_connected_1:
```
```  2021   fixes s :: "real set"
```
```  2022   shows "is_interval s \<longleftrightarrow> connected s"
```
```  2023   apply rule
```
```  2024   apply (rule is_interval_connected, assumption)
```
```  2025   unfolding is_interval_1
```
```  2026   apply rule
```
```  2027   apply rule
```
```  2028   apply rule
```
```  2029   apply rule
```
```  2030   apply (erule conjE)
```
```  2031   apply (rule ccontr)
```
```  2032 proof -
```
```  2033   fix a b x
```
```  2034   assume as: "connected s" "a \<in> s" "b \<in> s" "a \<le> x" "x \<le> b" "x \<notin> s"
```
```  2035   then have *: "a < x" "x < b"
```
```  2036     unfolding not_le [symmetric] by auto
```
```  2037   let ?halfl = "{..<x} "
```
```  2038   let ?halfr = "{x<..}"
```
```  2039   {
```
```  2040     fix y
```
```  2041     assume "y \<in> s"
```
```  2042     with \<open>x \<notin> s\<close> have "x \<noteq> y" by auto
```
```  2043     then have "y \<in> ?halfr \<union> ?halfl" by auto
```
```  2044   }
```
```  2045   moreover have "a \<in> ?halfl" "b \<in> ?halfr" using * by auto
```
```  2046   then have "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}"
```
```  2047     using as(2-3) by auto
```
```  2048   ultimately show False
```
```  2049     apply (rule_tac notE[OF as(1)[unfolded connected_def]])
```
```  2050     apply (rule_tac x = ?halfl in exI)
```
```  2051     apply (rule_tac x = ?halfr in exI, rule)
```
```  2052     apply (rule open_lessThan, rule)
```
```  2053     apply (rule open_greaterThan, auto)
```
```  2054     done
```
```  2055 qed
```
```  2056
```
```  2057 lemma is_interval_convex_1:
```
```  2058   fixes s :: "real set"
```
```  2059   shows "is_interval s \<longleftrightarrow> convex s"
```
```  2060   by (metis is_interval_convex convex_connected is_interval_connected_1)
```
```  2061
```
```  2062 lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
```
```  2063   by (metis connected_ball is_interval_connected_1)
```
```  2064
```
```  2065 lemma connected_compact_interval_1:
```
```  2066      "connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})"
```
```  2067   by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
```
```  2068
```
```  2069 lemma connected_convex_1:
```
```  2070   fixes s :: "real set"
```
```  2071   shows "connected s \<longleftrightarrow> convex s"
```
```  2072   by (metis is_interval_convex convex_connected is_interval_connected_1)
```
```  2073
```
```  2074 lemma connected_convex_1_gen:
```
```  2075   fixes s :: "'a :: euclidean_space set"
```
```  2076   assumes "DIM('a) = 1"
```
```  2077   shows "connected s \<longleftrightarrow> convex s"
```
```  2078 proof -
```
```  2079   obtain f:: "'a \<Rightarrow> real" where linf: "linear f" and "inj f"
```
```  2080     using subspace_isomorphism[OF subspace_UNIV subspace_UNIV,
```
```  2081         where 'a='a and 'b=real]
```
```  2082     unfolding Euclidean_Space.dim_UNIV
```
```  2083     by (auto simp: assms)
```
```  2084   then have "f -` (f ` s) = s"
```
```  2085     by (simp add: inj_vimage_image_eq)
```
```  2086   then show ?thesis
```
```  2087     by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
```
```  2088 qed
```
```  2089
```
```  2090 lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
```
```  2091   by (simp add: is_interval_convex_1)
```
```  2092
```
```  2093
```
```  2094 subsection%unimportant \<open>Another intermediate value theorem formulation\<close>
```
```  2095
```
```  2096 lemma ivt_increasing_component_on_1:
```
```  2097   fixes f :: "real \<Rightarrow> 'a::euclidean_space"
```
```  2098   assumes "a \<le> b"
```
```  2099     and "continuous_on {a..b} f"
```
```  2100     and "(f a)\<bullet>k \<le> y" "y \<le> (f b)\<bullet>k"
```
```  2101   shows "\<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
```
```  2102 proof -
```
```  2103   have "f a \<in> f ` cbox a b" "f b \<in> f ` cbox a b"
```
```  2104     apply (rule_tac[!] imageI)
```
```  2105     using assms(1)
```
```  2106     apply auto
```
```  2107     done
```
```  2108   then show ?thesis
```
```  2109     using connected_ivt_component[of "f ` cbox a b" "f a" "f b" k y]
```
```  2110     by (simp add: connected_continuous_image assms)
```
```  2111 qed
```
```  2112
```
```  2113 lemma ivt_increasing_component_1:
```
```  2114   fixes f :: "real \<Rightarrow> 'a::euclidean_space"
```
```  2115   shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a..b}. continuous (at x) f \<Longrightarrow>
```
```  2116     f a\<bullet>k \<le> y \<Longrightarrow> y \<le> f b\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
```
```  2117   by (rule ivt_increasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
```
```  2118
```
```  2119 lemma ivt_decreasing_component_on_1:
```
```  2120   fixes f :: "real \<Rightarrow> 'a::euclidean_space"
```
```  2121   assumes "a \<le> b"
```
```  2122     and "continuous_on {a..b} f"
```
```  2123     and "(f b)\<bullet>k \<le> y"
```
```  2124     and "y \<le> (f a)\<bullet>k"
```
```  2125   shows "\<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
```
```  2126   apply (subst neg_equal_iff_equal[symmetric])
```
```  2127   using ivt_increasing_component_on_1[of a b "\<lambda>x. - f x" k "- y"]
```
```  2128   using assms using continuous_on_minus
```
```  2129   apply auto
```
```  2130   done
```
```  2131
```
```  2132 lemma ivt_decreasing_component_1:
```
```  2133   fixes f :: "real \<Rightarrow> 'a::euclidean_space"
```
```  2134   shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a..b}. continuous (at x) f \<Longrightarrow>
```
```  2135     f b\<bullet>k \<le> y \<Longrightarrow> y \<le> f a\<bullet>k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)\<bullet>k = y"
```
```  2136   by (rule ivt_decreasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
```
```  2137
```
```  2138
```
```  2139 subsection%unimportant \<open>A bound within an interval\<close>
```
```  2140
```
```  2141 lemma convex_hull_eq_real_cbox:
```
```  2142   fixes x y :: real assumes "x \<le> y"
```
```  2143   shows "convex hull {x, y} = cbox x y"
```
```  2144 proof (rule hull_unique)
```
```  2145   show "{x, y} \<subseteq> cbox x y" using \<open>x \<le> y\<close> by auto
```
```  2146   show "convex (cbox x y)"
```
```  2147     by (rule convex_box)
```
```  2148 next
```
```  2149   fix S assume "{x, y} \<subseteq> S" and "convex S"
```
```  2150   then show "cbox x y \<subseteq> S"
```
```  2151     unfolding is_interval_convex_1 [symmetric] is_interval_def Basis_real_def
```
```  2152     by - (clarify, simp (no_asm_use), fast)
```
```  2153 qed
```
```  2154
```
```  2155 lemma unit_interval_convex_hull:
```
```  2156   "cbox (0::'a::euclidean_space) One = convex hull {x. \<forall>i\<in>Basis. (x\<bullet>i = 0) \<or> (x\<bullet>i = 1)}"
```
```  2157   (is "?int = convex hull ?points")
```
```  2158 proof -
```
```  2159   have One[simp]: "\<And>i. i \<in> Basis \<Longrightarrow> One \<bullet> i = 1"
```
```  2160     by (simp add: inner_sum_left sum.If_cases inner_Basis)
```
```  2161   have "?int = {x. \<forall>i\<in>Basis. x \<bullet> i \<in> cbox 0 1}"
```
```  2162     by (auto simp: cbox_def)
```
```  2163   also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` cbox 0 1)"
```
```  2164     by (simp only: box_eq_set_sum_Basis)
```
```  2165   also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` (convex hull {0, 1}))"
```
```  2166     by (simp only: convex_hull_eq_real_cbox zero_le_one)
```
```  2167   also have "\<dots> = (\<Sum>i\<in>Basis. convex hull ((\<lambda>x. x *\<^sub>R i) ` {0, 1}))"
```
```  2168     by (simp add: convex_hull_linear_image)
```
```  2169   also have "\<dots> = convex hull (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` {0, 1})"
```
```  2170     by (simp only: convex_hull_set_sum)
```
```  2171   also have "\<dots> = convex hull {x. \<forall>i\<in>Basis. x\<bullet>i \<in> {0, 1}}"
```
```  2172     by (simp only: box_eq_set_sum_Basis)
```
```  2173   also have "convex hull {x. \<forall>i\<in>Basis. x\<bullet>i \<in> {0, 1}} = convex hull ?points"
```
```  2174     by simp
```
```  2175   finally show ?thesis .
```
```  2176 qed
```
```  2177
```
```  2178 text \<open>And this is a finite set of vertices.\<close>
```
```  2179
```
```  2180 lemma unit_cube_convex_hull:
```
```  2181   obtains S :: "'a::euclidean_space set"
```
```  2182   where "finite S" and "cbox 0 (\<Sum>Basis) = convex hull S"
```
```  2183 proof
```
```  2184   show "finite {x::'a. \<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1}"
```
```  2185   proof (rule finite_subset, clarify)
```
```  2186     show "finite ((\<lambda>S. \<Sum>i\<in>Basis. (if i \<in> S then 1 else 0) *\<^sub>R i) ` Pow Basis)"
```
```  2187       using finite_Basis by blast
```
```  2188     fix x :: 'a
```
```  2189     assume as: "\<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1"
```
```  2190     show "x \<in> (\<lambda>S. \<Sum>i\<in>Basis. (if i\<in>S then 1 else 0) *\<^sub>R i) ` Pow Basis"
```
```  2191       apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
```
```  2192       using as
```
```  2193        apply (subst euclidean_eq_iff, auto)
```
```  2194       done
```
```  2195   qed
```
```  2196   show "cbox 0 One = convex hull {x. \<forall>i\<in>Basis. x \<bullet> i = 0 \<or> x \<bullet> i = 1}"
```
```  2197     using unit_interval_convex_hull by blast
```
```  2198 qed
```
```  2199
```
```  2200 text \<open>Hence any cube (could do any nonempty interval).\<close>
```
```  2201
```
```  2202 lemma cube_convex_hull:
```
```  2203   assumes "d > 0"
```
```  2204   obtains S :: "'a::euclidean_space set" where
```
```  2205     "finite S" and "cbox (x - (\<Sum>i\<in>Basis. d*\<^sub>Ri)) (x + (\<Sum>i\<in>Basis. d*\<^sub>Ri)) = convex hull S"
```
```  2206 proof -
```
```  2207   let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
```
```  2208   have *: "cbox (x - ?d) (x + ?d) = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 (\<Sum>Basis)"
```
```  2209   proof (intro set_eqI iffI)
```
```  2210     fix y
```
```  2211     assume "y \<in> cbox (x - ?d) (x + ?d)"
```
```  2212     then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
```
```  2213       using assms by (simp add: mem_box field_simps inner_simps)
```
```  2214     with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum ((*\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
```
```  2215       by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"])
```
```  2216   next
```
```  2217     fix y
```
```  2218     assume "y \<in> (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` cbox 0 One"
```
```  2219     then obtain z where z: "z \<in> cbox 0 One" "y = x - ?d + (2*d) *\<^sub>R z"
```
```  2220       by auto
```
```  2221     then show "y \<in> cbox (x - ?d) (x + ?d)"
```
```  2222       using z assms by (auto simp: mem_box inner_simps)
```
```  2223   qed
```
```  2224   obtain S where "finite S" "cbox 0 (\<Sum>Basis::'a) = convex hull S"
```
```  2225     using unit_cube_convex_hull by auto
```
```  2226   then show ?thesis
```
```  2227     by (rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` S"]) (auto simp: convex_hull_affinity *)
```
```  2228 qed
```
```  2229
```
```  2230 subsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
```
```  2231
```
```  2232 lemma image_stretch_interval:
```
```  2233   "(\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) =
```
```  2234   (if (cbox a b) = {} then {} else
```
```  2235     cbox (\<Sum>k\<in>Basis. (min (m k * (a\<bullet>k)) (m k * (b\<bullet>k))) *\<^sub>R k::'a)
```
```  2236      (\<Sum>k\<in>Basis. (max (m k * (a\<bullet>k)) (m k * (b\<bullet>k))) *\<^sub>R k))"
```
```  2237 proof cases
```
```  2238   assume *: "cbox a b \<noteq> {}"
```
```  2239   show ?thesis
```
```  2240     unfolding box_ne_empty if_not_P[OF *]
```
```  2241     apply (simp add: cbox_def image_Collect set_eq_iff euclidean_eq_iff[where 'a='a] ball_conj_distrib[symmetric])
```
```  2242     apply (subst choice_Basis_iff[symmetric])
```
```  2243   proof (intro allI ball_cong refl)
```
```  2244     fix x i :: 'a assume "i \<in> Basis"
```
```  2245     with * have a_le_b: "a \<bullet> i \<le> b \<bullet> i"
```
```  2246       unfolding box_ne_empty by auto
```
```  2247     show "(\<exists>xa. x \<bullet> i = m i * xa \<and> a \<bullet> i \<le> xa \<and> xa \<le> b \<bullet> i) \<longleftrightarrow>
```
```  2248         min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) \<le> x \<bullet> i \<and> x \<bullet> i \<le> max (m i * (a \<bullet> i)) (m i * (b \<bullet> i))"
```
```  2249     proof (cases "m i = 0")
```
```  2250       case True
```
```  2251       with a_le_b show ?thesis by auto
```
```  2252     next
```
```  2253       case False
```
```  2254       then have *: "\<And>a b. a = m i * b \<longleftrightarrow> b = a / m i"
```
```  2255         by (auto simp: field_simps)
```
```  2256       from False have
```
```  2257           "min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (a \<bullet> i) else m i * (b \<bullet> i))"
```
```  2258           "max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (b \<bullet> i) else m i * (a \<bullet> i))"
```
```  2259         using a_le_b by (auto simp: min_def max_def mult_le_cancel_left)
```
```  2260       with False show ?thesis using a_le_b
```
```  2261         unfolding * by (auto simp: le_divide_eq divide_le_eq ac_simps)
```
```  2262     qed
```
```  2263   qed
```
```  2264 qed simp
```
```  2265
```
```  2266 lemma interval_image_stretch_interval:
```
```  2267   "\<exists>u v. (\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k) ` cbox a (b::'a::euclidean_space) = cbox u (v::'a::euclidean_space)"
```
```  2268   unfolding image_stretch_interval by auto
```
```  2269
```
```  2270 lemma cbox_translation: "cbox (c + a) (c + b) = image (\<lambda>x. c + x) (cbox a b)"
```
```  2271   using image_affinity_cbox [of 1 c a b]
```
```  2272   using box_ne_empty [of "a+c" "b+c"]  box_ne_empty [of a b]
```
```  2273   by (auto simp: inner_left_distrib add.commute)
```
```  2274
```
```  2275 lemma cbox_image_unit_interval:
```
```  2276   fixes a :: "'a::euclidean_space"
```
```  2277   assumes "cbox a b \<noteq> {}"
```
```  2278     shows "cbox a b =
```
```  2279            (+) a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` cbox 0 One"
```
```  2280 using assms
```
```  2281 apply (simp add: box_ne_empty image_stretch_interval cbox_translation [symmetric])
```
```  2282 apply (simp add: min_def max_def algebra_simps sum_subtractf euclidean_representation)
```
```  2283 done
```
```  2284
```
```  2285 lemma closed_interval_as_convex_hull:
```
```  2286   fixes a :: "'a::euclidean_space"
```
```  2287   obtains S where "finite S" "cbox a b = convex hull S"
```
```  2288 proof (cases "cbox a b = {}")
```
```  2289   case True with convex_hull_empty that show ?thesis
```
```  2290     by blast
```
```  2291 next
```
```  2292   case False
```
```  2293   obtain S::"'a set" where "finite S" and eq: "cbox 0 One = convex hull S"
```
```  2294     by (blast intro: unit_cube_convex_hull)
```
```  2295   have lin: "linear (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k)"
```
```  2296     by (rule linear_compose_sum) (auto simp: algebra_simps linearI)
```
```  2297   have "finite ((+) a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` S)"
```
```  2298     by (rule finite_imageI \<open>finite S\<close>)+
```
```  2299   then show ?thesis
```
```  2300     apply (rule that)
```
```  2301     apply (simp add: convex_hull_translation convex_hull_linear_image [OF lin, symmetric])
```
```  2302     apply (simp add: eq [symmetric] cbox_image_unit_interval [OF False])
```
```  2303     done
```
```  2304 qed
```
```  2305
```
```  2306
```
```  2307 subsection%unimportant \<open>Bounded convex function on open set is continuous\<close>
```
```  2308
```
```  2309 lemma convex_on_bounded_continuous:
```
```  2310   fixes S :: "('a::real_normed_vector) set"
```
```  2311   assumes "open S"
```
```  2312     and "convex_on S f"
```
```  2313     and "\<forall>x\<in>S. \<bar>f x\<bar> \<le> b"
```
```  2314   shows "continuous_on S f"
```
```  2315   apply (rule continuous_at_imp_continuous_on)
```
```  2316   unfolding continuous_at_real_range
```
```  2317 proof (rule,rule,rule)
```
```  2318   fix x and e :: real
```
```  2319   assume "x \<in> S" "e > 0"
```
```  2320   define B where "B = \<bar>b\<bar> + 1"
```
```  2321   then have B:  "0 < B""\<And>x. x\<in>S \<Longrightarrow> \<bar>f x\<bar> \<le> B"
```
```  2322     using assms(3) by auto
```
```  2323   obtain k where "k > 0" and k: "cball x k \<subseteq> S"
```
```  2324     using \<open>x \<in> S\<close> assms(1) open_contains_cball_eq by blast
```
```  2325   show "\<exists>d>0. \<forall>x'. norm (x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e"
```
```  2326   proof (intro exI conjI allI impI)
```
```  2327     fix y
```
```  2328     assume as: "norm (y - x) < min (k / 2) (e / (2 * B) * k)"
```
```  2329     show "\<bar>f y - f x\<bar> < e"
```
```  2330     proof (cases "y = x")
```
```  2331       case False
```
```  2332       define t where "t = k / norm (y - x)"
```
```  2333       have "2 < t" "0<t"
```
```  2334         unfolding t_def using as False and \<open>k>0\<close>
```
```  2335         by (auto simp:field_simps)
```
```  2336       have "y \<in> S"
```
```  2337         apply (rule k[THEN subsetD])
```
```  2338         unfolding mem_cball dist_norm
```
```  2339         apply (rule order_trans[of _ "2 * norm (x - y)"])
```
```  2340         using as
```
```  2341         by (auto simp: field_simps norm_minus_commute)
```
```  2342       {
```
```  2343         define w where "w = x + t *\<^sub>R (y - x)"
```
```  2344         have "w \<in> S"
```
```  2345           using \<open>k>0\<close> by (auto simp: dist_norm t_def w_def k[THEN subsetD])
```
```  2346         have "(1 / t) *\<^sub>R x + - x + ((t - 1) / t) *\<^sub>R x = (1 / t - 1 + (t - 1) / t) *\<^sub>R x"
```
```  2347           by (auto simp: algebra_simps)
```
```  2348         also have "\<dots> = 0"
```
```  2349           using \<open>t > 0\<close> by (auto simp:field_simps)
```
```  2350         finally have w: "(1 / t) *\<^sub>R w + ((t - 1) / t) *\<^sub>R x = y"
```
```  2351           unfolding w_def using False and \<open>t > 0\<close>
```
```  2352           by (auto simp: algebra_simps)
```
```  2353         have 2: "2 * B < e * t"
```
```  2354           unfolding t_def using \<open>0 < e\<close> \<open>0 < k\<close> \<open>B > 0\<close> and as and False
```
```  2355           by (auto simp:field_simps)
```
```  2356         have "f y - f x \<le> (f w - f x) / t"
```
```  2357           using assms(2)[unfolded convex_on_def,rule_format,of w x "1/t" "(t - 1)/t", unfolded w]
```
```  2358           using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>x \<in> S\<close> \<open>w \<in> S\<close>
```
```  2359           by (auto simp:field_simps)
```
```  2360         also have "... < e"
```
```  2361           using B(2)[OF \<open>w\<in>S\<close>] and B(2)[OF \<open>x\<in>S\<close>] 2 \<open>t > 0\<close> by (auto simp: field_simps)
```
```  2362         finally have th1: "f y - f x < e" .
```
```  2363       }
```
```  2364       moreover
```
```  2365       {
```
```  2366         define w where "w = x - t *\<^sub>R (y - x)"
```
```  2367         have "w \<in> S"
```
```  2368           using \<open>k > 0\<close> by (auto simp: dist_norm t_def w_def k[THEN subsetD])
```
```  2369         have "(1 / (1 + t)) *\<^sub>R x + (t / (1 + t)) *\<^sub>R x = (1 / (1 + t) + t / (1 + t)) *\<^sub>R x"
```
```  2370           by (auto simp: algebra_simps)
```
```  2371         also have "\<dots> = x"
```
```  2372           using \<open>t > 0\<close> by (auto simp:field_simps)
```
```  2373         finally have w: "(1 / (1+t)) *\<^sub>R w + (t / (1 + t)) *\<^sub>R y = x"
```
```  2374           unfolding w_def using False and \<open>t > 0\<close>
```
```  2375           by (auto simp: algebra_simps)
```
```  2376         have "2 * B < e * t"
```
```  2377           unfolding t_def
```
```  2378           using \<open>0 < e\<close> \<open>0 < k\<close> \<open>B > 0\<close> and as and False
```
```  2379           by (auto simp:field_simps)
```
```  2380         then have *: "(f w - f y) / t < e"
```
```  2381           using B(2)[OF \<open>w\<in>S\<close>] and B(2)[OF \<open>y\<in>S\<close>]
```
```  2382           using \<open>t > 0\<close>
```
```  2383           by (auto simp:field_simps)
```
```  2384         have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y"
```
```  2385           using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
```
```  2386           using \<open>0 < t\<close> \<open>2 < t\<close> and \<open>y \<in> S\<close> \<open>w \<in> S\<close>
```
```  2387           by (auto simp:field_simps)
```
```  2388         also have "\<dots> = (f w + t * f y) / (1 + t)"
```
```  2389           using \<open>t > 0\<close> by (auto simp: divide_simps)
```
```  2390         also have "\<dots> < e + f y"
```
```  2391           using \<open>t > 0\<close> * \<open>e > 0\<close> by (auto simp: field_simps)
```
```  2392         finally have "f x - f y < e" by auto
```
```  2393       }
```
```  2394       ultimately show ?thesis by auto
```
```  2395     qed (insert \<open>0<e\<close>, auto)
```
```  2396   qed (insert \<open>0<e\<close> \<open>0<k\<close> \<open>0<B\<close>, auto simp: field_simps)
```
```  2397 qed
```
```  2398
```
```  2399
```
```  2400 subsection%unimportant \<open>Upper bound on a ball implies upper and lower bounds\<close>
```
```  2401
```
```  2402 lemma convex_bounds_lemma:
```
```  2403   fixes x :: "'a::real_normed_vector"
```
```  2404   assumes "convex_on (cball x e) f"
```
```  2405     and "\<forall>y \<in> cball x e. f y \<le> b"
```
```  2406   shows "\<forall>y \<in> cball x e. \<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>"
```
```  2407   apply rule
```
```  2408 proof (cases "0 \<le> e")
```
```  2409   case True
```
```  2410   fix y
```
```  2411   assume y: "y \<in> cball x e"
```
```  2412   define z where "z = 2 *\<^sub>R x - y"
```
```  2413   have *: "x - (2 *\<^sub>R x - y) = y - x"
```
```  2414     by (simp add: scaleR_2)
```
```  2415   have z: "z \<in> cball x e"
```
```  2416     using y unfolding z_def mem_cball dist_norm * by (auto simp: norm_minus_commute)
```
```  2417   have "(1 / 2) *\<^sub>R y + (1 / 2) *\<^sub>R z = x"
```
```  2418     unfolding z_def by (auto simp: algebra_simps)
```
```  2419   then show "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>"
```
```  2420     using assms(1)[unfolded convex_on_def,rule_format, OF y z, of "1/2" "1/2"]
```
```  2421     using assms(2)[rule_format,OF y] assms(2)[rule_format,OF z]
```
```  2422     by (auto simp:field_simps)
```
```  2423 next
```
```  2424   case False
```
```  2425   fix y
```
```  2426   assume "y \<in> cball x e"
```
```  2427   then have "dist x y < 0"
```
```  2428     using False unfolding mem_cball not_le by (auto simp del: dist_not_less_zero)
```
```  2429   then show "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>"
```
```  2430     using zero_le_dist[of x y] by auto
```
```  2431 qed
```
```  2432
```
```  2433
```
```  2434 subsubsection%unimportant \<open>Hence a convex function on an open set is continuous\<close>
```
```  2435
```
```  2436 lemma real_of_nat_ge_one_iff: "1 \<le> real (n::nat) \<longleftrightarrow> 1 \<le> n"
```
```  2437   by auto
```
```  2438
```
```  2439 lemma convex_on_continuous:
```
```  2440   assumes "open (s::('a::euclidean_space) set)" "convex_on s f"
```
```  2441   shows "continuous_on s f"
```
```  2442   unfolding continuous_on_eq_continuous_at[OF assms(1)]
```
```  2443 proof
```
```  2444   note dimge1 = DIM_positive[where 'a='a]
```
```  2445   fix x
```
```  2446   assume "x \<in> s"
```
```  2447   then obtain e where e: "cball x e \<subseteq> s" "e > 0"
```
```  2448     using assms(1) unfolding open_contains_cball by auto
```
```  2449   define d where "d = e / real DIM('a)"
```
```  2450   have "0 < d"
```
```  2451     unfolding d_def using \<open>e > 0\<close> dimge1 by auto
```
```  2452   let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
```
```  2453   obtain c
```
```  2454     where c: "finite c"
```
```  2455     and c1: "convex hull c \<subseteq> cball x e"
```
```  2456     and c2: "cball x d \<subseteq> convex hull c"
```
```  2457   proof
```
```  2458     define c where "c = (\<Sum>i\<in>Basis. (\<lambda>a. a *\<^sub>R i) ` {x\<bullet>i - d, x\<bullet>i + d})"
```
```  2459     show "finite c"
```
```  2460       unfolding c_def by (simp add: finite_set_sum)
```
```  2461     have 1: "convex hull c = {a. \<forall>i\<in>Basis. a \<bullet> i \<in> cbox (x \<bullet> i - d) (x \<bullet> i + d)}"
```
```  2462       unfolding box_eq_set_sum_Basis
```
```  2463       unfolding c_def convex_hull_set_sum
```
```  2464       apply (subst convex_hull_linear_image [symmetric])
```
```  2465       apply (simp add: linear_iff scaleR_add_left)
```
```  2466       apply (rule sum.cong [OF refl])
```
```  2467       apply (rule image_cong [OF _ refl])
```
```  2468       apply (rule convex_hull_eq_real_cbox)
```
```  2469       apply (cut_tac \<open>0 < d\<close>, simp)
```
```  2470       done
```
```  2471     then have 2: "convex hull c = {a. \<forall>i\<in>Basis. a \<bullet> i \<in> cball (x \<bullet> i) d}"
```
```  2472       by (simp add: dist_norm abs_le_iff algebra_simps)
```
```  2473     show "cball x d \<subseteq> convex hull c"
```
```  2474       unfolding 2
```
```  2475       by (clarsimp simp: dist_norm) (metis inner_commute inner_diff_right norm_bound_Basis_le)
```
```  2476     have e': "e = (\<Sum>(i::'a)\<in>Basis. d)"
```
```  2477       by (simp add: d_def DIM_positive)
```
```  2478     show "convex hull c \<subseteq> cball x e"
```
```  2479       unfolding 2
```
```  2480       apply clarsimp
```
```  2481       apply (subst euclidean_dist_l2)
```
```  2482       apply (rule order_trans [OF L2_set_le_sum])
```
```  2483       apply (rule zero_le_dist)
```
```  2484       unfolding e'
```
```  2485       apply (rule sum_mono, simp)
```
```  2486       done
```
```  2487   qed
```
```  2488   define k where "k = Max (f ` c)"
```
```  2489   have "convex_on (convex hull c) f"
```
```  2490     apply(rule convex_on_subset[OF assms(2)])
```
```  2491     apply(rule subset_trans[OF c1 e(1)])
```
```  2492     done
```
```  2493   then have k: "\<forall>y\<in>convex hull c. f y \<le> k"
```
```  2494     apply (rule_tac convex_on_convex_hull_bound, assumption)
```
```  2495     by (simp add: k_def c)
```
```  2496   have "e \<le> e * real DIM('a)"
```
```  2497     using e(2) real_of_nat_ge_one_iff by auto
```
```  2498   then have "d \<le> e"
```
```  2499     by (simp add: d_def divide_simps)
```
```  2500   then have dsube: "cball x d \<subseteq> cball x e"
```
```  2501     by (rule subset_cball)
```
```  2502   have conv: "convex_on (cball x d) f"
```
```  2503     using \<open>convex_on (convex hull c) f\<close> c2 convex_on_subset by blast
```
```  2504   then have "\<forall>y\<in>cball x d. \<bar>f y\<bar> \<le> k + 2 * \<bar>f x\<bar>"
```
```  2505     by (rule convex_bounds_lemma) (use c2 k in blast)
```
```  2506   then have "continuous_on (ball x d) f"
```
```  2507     apply (rule_tac convex_on_bounded_continuous)
```
```  2508     apply (rule open_ball, rule convex_on_subset[OF conv])
```
```  2509     apply (rule ball_subset_cball, force)
```
```  2510     done
```
```  2511   then show "continuous (at x) f"
```
```  2512     unfolding continuous_on_eq_continuous_at[OF open_ball]
```
```  2513     using \<open>d > 0\<close> by auto
```
```  2514 qed
```
```  2515
```
```  2516 end
```