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