src/HOL/Analysis/Starlike.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 69922 4a9167f377b0
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
lp15@66289
     1
(* Title:      HOL/Analysis/Starlike.thy
lp15@66289
     2
   Author:     L C Paulson, University of Cambridge
lp15@66289
     3
   Author:     Robert Himmelmann, TU Muenchen
lp15@66289
     4
   Author:     Bogdan Grechuk, University of Edinburgh
lp15@66289
     5
   Author:     Armin Heller, TU Muenchen
lp15@66289
     6
   Author:     Johannes Hoelzl, TU Muenchen
lp15@66289
     7
*)
immler@69676
     8
chapter \<open>Unsorted\<close>
lp15@66289
     9
lp15@66289
    10
theory Starlike
lp15@69922
    11
imports Convex_Euclidean_Space Abstract_Limits
lp15@66289
    12
begin
lp15@66289
    13
immler@69676
    14
section \<open>Line Segments\<close>
immler@69676
    15
immler@67685
    16
subsection \<open>Midpoint\<close>
immler@67685
    17
immler@67962
    18
definition%important midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
lp15@66289
    19
  where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
lp15@66289
    20
immler@67685
    21
lemma midpoint_idem [simp]: "midpoint x x = x"
lp15@68056
    22
  unfolding midpoint_def  by simp
immler@67685
    23
immler@67685
    24
lemma midpoint_sym: "midpoint a b = midpoint b a"
immler@67685
    25
  unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
immler@67685
    26
immler@67685
    27
lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
immler@67685
    28
proof -
immler@67685
    29
  have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
immler@67685
    30
    by simp
immler@67685
    31
  then show ?thesis
immler@67685
    32
    unfolding midpoint_def scaleR_2 [symmetric] by simp
immler@67685
    33
qed
immler@67685
    34
immler@67685
    35
lemma
immler@67685
    36
  fixes a::real
immler@67685
    37
  assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
immler@67685
    38
                    and le_midpoint_1: "midpoint a b \<le> b"
immler@67685
    39
  by (simp_all add: midpoint_def assms)
immler@67685
    40
immler@67685
    41
lemma dist_midpoint:
immler@67685
    42
  fixes a b :: "'a::real_normed_vector" shows
immler@67685
    43
  "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
immler@67685
    44
  "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
immler@67685
    45
  "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
immler@67685
    46
  "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
immler@67685
    47
proof -
immler@67685
    48
  have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
immler@67685
    49
    unfolding equation_minus_iff by auto
immler@67685
    50
  have **: "\<And>x y::'a. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2"
immler@67685
    51
    by auto
immler@67685
    52
  note scaleR_right_distrib [simp]
immler@67685
    53
  show ?t1
immler@67685
    54
    unfolding midpoint_def dist_norm
immler@67685
    55
    apply (rule **)
immler@67685
    56
    apply (simp add: scaleR_right_diff_distrib)
immler@67685
    57
    apply (simp add: scaleR_2)
immler@67685
    58
    done
immler@67685
    59
  show ?t2
immler@67685
    60
    unfolding midpoint_def dist_norm
immler@67685
    61
    apply (rule *)
immler@67685
    62
    apply (simp add: scaleR_right_diff_distrib)
immler@67685
    63
    apply (simp add: scaleR_2)
immler@67685
    64
    done
immler@67685
    65
  show ?t3
immler@67685
    66
    unfolding midpoint_def dist_norm
immler@67685
    67
    apply (rule *)
immler@67685
    68
    apply (simp add: scaleR_right_diff_distrib)
immler@67685
    69
    apply (simp add: scaleR_2)
immler@67685
    70
    done
immler@67685
    71
  show ?t4
immler@67685
    72
    unfolding midpoint_def dist_norm
immler@67685
    73
    apply (rule **)
immler@67685
    74
    apply (simp add: scaleR_right_diff_distrib)
immler@67685
    75
    apply (simp add: scaleR_2)
immler@67685
    76
    done
immler@67685
    77
qed
immler@67685
    78
immler@67685
    79
lemma midpoint_eq_endpoint [simp]:
immler@67685
    80
  "midpoint a b = a \<longleftrightarrow> a = b"
immler@67685
    81
  "midpoint a b = b \<longleftrightarrow> a = b"
immler@67685
    82
  unfolding midpoint_eq_iff by auto
immler@67685
    83
immler@67685
    84
lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
immler@67685
    85
  using midpoint_eq_iff by metis
immler@67685
    86
immler@67685
    87
lemma midpoint_linear_image:
immler@67685
    88
   "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
immler@67685
    89
by (simp add: linear_iff midpoint_def)
immler@67685
    90
immler@67685
    91
immler@67685
    92
subsection \<open>Line segments\<close>
immler@67685
    93
immler@67962
    94
definition%important closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
lp15@66289
    95
  where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
lp15@66289
    96
immler@67962
    97
definition%important open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
lp15@66289
    98
  "open_segment a b \<equiv> closed_segment a b - {a,b}"
lp15@66289
    99
lp15@66289
   100
lemmas segment = open_segment_def closed_segment_def
lp15@66289
   101
lp15@66289
   102
lemma in_segment:
lp15@66289
   103
    "x \<in> closed_segment a b \<longleftrightarrow> (\<exists>u. 0 \<le> u \<and> u \<le> 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
lp15@66289
   104
    "x \<in> open_segment a b \<longleftrightarrow> a \<noteq> b \<and> (\<exists>u. 0 < u \<and> u < 1 \<and> x = (1 - u) *\<^sub>R a + u *\<^sub>R b)"
lp15@66289
   105
  using less_eq_real_def by (auto simp: segment algebra_simps)
lp15@66289
   106
lp15@66289
   107
lemma closed_segment_linear_image:
immler@68072
   108
  "closed_segment (f a) (f b) = f ` (closed_segment a b)" if "linear f"
immler@68072
   109
proof -
immler@68072
   110
  interpret linear f by fact
immler@68072
   111
  show ?thesis
immler@68072
   112
    by (force simp add: in_segment add scale)
immler@68072
   113
qed
lp15@66289
   114
lp15@66289
   115
lemma open_segment_linear_image:
lp15@66289
   116
    "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)"
lp15@66289
   117
  by (force simp: open_segment_def closed_segment_linear_image inj_on_def)
lp15@66289
   118
lp15@66289
   119
lemma closed_segment_translation:
lp15@66289
   120
    "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)"
lp15@66289
   121
apply safe
lp15@66289
   122
apply (rule_tac x="x-c" in image_eqI)
lp15@66289
   123
apply (auto simp: in_segment algebra_simps)
lp15@66289
   124
done
lp15@66289
   125
lp15@66289
   126
lemma open_segment_translation:
lp15@66289
   127
    "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
lp15@66289
   128
by (simp add: open_segment_def closed_segment_translation translation_diff)
lp15@66289
   129
lp15@66289
   130
lemma closed_segment_of_real:
lp15@66289
   131
    "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y"
lp15@66289
   132
  apply (auto simp: image_iff in_segment scaleR_conv_of_real)
lp15@66289
   133
    apply (rule_tac x="(1-u)*x + u*y" in bexI)
lp15@66289
   134
  apply (auto simp: in_segment)
lp15@66289
   135
  done
lp15@66289
   136
lp15@66289
   137
lemma open_segment_of_real:
lp15@66289
   138
    "open_segment (of_real x) (of_real y) = of_real ` open_segment x y"
lp15@66289
   139
  apply (auto simp: image_iff in_segment scaleR_conv_of_real)
lp15@66289
   140
    apply (rule_tac x="(1-u)*x + u*y" in bexI)
lp15@66289
   141
  apply (auto simp: in_segment)
lp15@66289
   142
  done
lp15@66289
   143
lp15@66289
   144
lemma closed_segment_Reals:
lp15@66289
   145
    "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)"
lp15@66289
   146
  by (metis closed_segment_of_real of_real_Re)
lp15@66289
   147
lp15@66289
   148
lemma open_segment_Reals:
lp15@66289
   149
    "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)"
lp15@66289
   150
  by (metis open_segment_of_real of_real_Re)
lp15@66289
   151
lp15@66289
   152
lemma open_segment_PairD:
lp15@66289
   153
    "(x, x') \<in> open_segment (a, a') (b, b')
lp15@66289
   154
     \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"
lp15@66289
   155
  by (auto simp: in_segment)
lp15@66289
   156
lp15@66289
   157
lemma closed_segment_PairD:
lp15@66289
   158
  "(x, x') \<in> closed_segment (a, a') (b, b') \<Longrightarrow> x \<in> closed_segment a b \<and> x' \<in> closed_segment a' b'"
lp15@66289
   159
  by (auto simp: closed_segment_def)
lp15@66289
   160
lp15@66289
   161
lemma closed_segment_translation_eq [simp]:
lp15@66289
   162
    "d + x \<in> closed_segment (d + a) (d + b) \<longleftrightarrow> x \<in> closed_segment a b"
lp15@66289
   163
proof -
lp15@66289
   164
  have *: "\<And>d x a b. x \<in> closed_segment a b \<Longrightarrow> d + x \<in> closed_segment (d + a) (d + b)"
lp15@66289
   165
    apply (simp add: closed_segment_def)
lp15@66289
   166
    apply (erule ex_forward)
lp15@66289
   167
    apply (simp add: algebra_simps)
lp15@66289
   168
    done
lp15@66289
   169
  show ?thesis
lp15@66289
   170
  using * [where d = "-d"] *
lp15@66289
   171
  by (fastforce simp add:)
lp15@66289
   172
qed
lp15@66289
   173
lp15@66289
   174
lemma open_segment_translation_eq [simp]:
lp15@66289
   175
    "d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b"
lp15@66289
   176
  by (simp add: open_segment_def)
lp15@66289
   177
lp15@66289
   178
lemma of_real_closed_segment [simp]:
lp15@66289
   179
  "of_real x \<in> closed_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> closed_segment a b"
lp15@66289
   180
  apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward)
lp15@66289
   181
  using of_real_eq_iff by fastforce
lp15@66289
   182
lp15@66289
   183
lemma of_real_open_segment [simp]:
lp15@66289
   184
  "of_real x \<in> open_segment (of_real a) (of_real b) \<longleftrightarrow> x \<in> open_segment a b"
lp15@66289
   185
  apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
lp15@66289
   186
  using of_real_eq_iff by fastforce
lp15@66289
   187
lp15@66289
   188
lemma convex_contains_segment:
lp15@66289
   189
  "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
lp15@66289
   190
  unfolding convex_alt closed_segment_def by auto
lp15@66289
   191
lp15@68465
   192
lemma closed_segment_in_Reals:
lp15@68465
   193
   "\<lbrakk>x \<in> closed_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
lp15@68465
   194
  by (meson subsetD convex_Reals convex_contains_segment)
lp15@68465
   195
lp15@68465
   196
lemma open_segment_in_Reals:
lp15@68465
   197
   "\<lbrakk>x \<in> open_segment a b; a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
lp15@68465
   198
  by (metis Diff_iff closed_segment_in_Reals open_segment_def)
lp15@68465
   199
lp15@66289
   200
lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S"
lp15@66289
   201
  by (simp add: convex_contains_segment)
lp15@66289
   202
lp15@66289
   203
lemma closed_segment_subset_convex_hull:
lp15@66289
   204
    "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
lp15@66289
   205
  using convex_contains_segment by blast
lp15@66289
   206
lp15@66289
   207
lemma segment_convex_hull:
lp15@66289
   208
  "closed_segment a b = convex hull {a,b}"
lp15@66289
   209
proof -
lp15@66289
   210
  have *: "\<And>x. {x} \<noteq> {}" by auto
lp15@66289
   211
  show ?thesis
lp15@66289
   212
    unfolding segment convex_hull_insert[OF *] convex_hull_singleton
lp15@66289
   213
    by (safe; rule_tac x="1 - u" in exI; force)
lp15@66289
   214
qed
lp15@66289
   215
lp15@66289
   216
lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
lp15@66289
   217
  by (auto simp add: closed_segment_def open_segment_def)
lp15@66289
   218
lp15@66289
   219
lemma segment_open_subset_closed:
lp15@66289
   220
   "open_segment a b \<subseteq> closed_segment a b"
lp15@66289
   221
  by (auto simp: closed_segment_def open_segment_def)
lp15@66289
   222
lp15@66289
   223
lemma bounded_closed_segment:
lp15@66289
   224
    fixes a :: "'a::euclidean_space" shows "bounded (closed_segment a b)"
lp15@66289
   225
  by (simp add: segment_convex_hull compact_convex_hull compact_imp_bounded)
lp15@66289
   226
lp15@66289
   227
lemma bounded_open_segment:
lp15@66289
   228
    fixes a :: "'a::euclidean_space" shows "bounded (open_segment a b)"
lp15@66289
   229
  by (rule bounded_subset [OF bounded_closed_segment segment_open_subset_closed])
lp15@66289
   230
lp15@66289
   231
lemmas bounded_segment = bounded_closed_segment open_closed_segment
lp15@66289
   232
lp15@66289
   233
lemma ends_in_segment [iff]: "a \<in> closed_segment a b" "b \<in> closed_segment a b"
lp15@66289
   234
  unfolding segment_convex_hull
lp15@66289
   235
  by (auto intro!: hull_subset[unfolded subset_eq, rule_format])
lp15@66289
   236
lp15@66289
   237
lemma eventually_closed_segment:
lp15@66289
   238
  fixes x0::"'a::real_normed_vector"
lp15@66289
   239
  assumes "open X0" "x0 \<in> X0"
lp15@66289
   240
  shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0"
lp15@66289
   241
proof -
lp15@66289
   242
  from openE[OF assms]
lp15@66289
   243
  obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" .
lp15@66289
   244
  then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e"
lp15@66289
   245
    by (auto simp: dist_commute eventually_at)
lp15@66289
   246
  then show ?thesis
lp15@66289
   247
  proof eventually_elim
lp15@66289
   248
    case (elim x)
lp15@66289
   249
    have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp
lp15@66289
   250
    from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim]
lp15@66289
   251
    have "closed_segment x0 x \<subseteq> ball x0 e" .
lp15@66289
   252
    also note \<open>\<dots> \<subseteq> X0\<close>
lp15@66289
   253
    finally show ?case .
lp15@66289
   254
  qed
lp15@66289
   255
qed
lp15@66289
   256
lp15@66289
   257
lemma segment_furthest_le:
lp15@66289
   258
  fixes a b x y :: "'a::euclidean_space"
lp15@66289
   259
  assumes "x \<in> closed_segment a b"
lp15@66289
   260
  shows "norm (y - x) \<le> norm (y - a) \<or>  norm (y - x) \<le> norm (y - b)"
lp15@66289
   261
proof -
lp15@66289
   262
  obtain z where "z \<in> {a, b}" "norm (x - y) \<le> norm (z - y)"
lp15@66289
   263
    using simplex_furthest_le[of "{a, b}" y]
lp15@66289
   264
    using assms[unfolded segment_convex_hull]
lp15@66289
   265
    by auto
lp15@66289
   266
  then show ?thesis
lp15@66289
   267
    by (auto simp add:norm_minus_commute)
lp15@66289
   268
qed
lp15@66289
   269
lp15@66289
   270
lemma closed_segment_commute: "closed_segment a b = closed_segment b a"
lp15@66289
   271
proof -
lp15@66289
   272
  have "{a, b} = {b, a}" by auto
lp15@66289
   273
  thus ?thesis
lp15@66289
   274
    by (simp add: segment_convex_hull)
lp15@66289
   275
qed
lp15@66289
   276
lp15@66289
   277
lemma segment_bound1:
lp15@66289
   278
  assumes "x \<in> closed_segment a b"
lp15@66289
   279
  shows "norm (x - a) \<le> norm (b - a)"
lp15@66289
   280
proof -
lp15@66289
   281
  obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
lp15@66289
   282
    using assms by (auto simp add: closed_segment_def)
lp15@66289
   283
  then show "norm (x - a) \<le> norm (b - a)"
lp15@66289
   284
    apply clarify
lp15@66289
   285
    apply (auto simp: algebra_simps)
lp15@66289
   286
    apply (simp add: scaleR_diff_right [symmetric] mult_left_le_one_le)
lp15@66289
   287
    done
lp15@66289
   288
qed
lp15@66289
   289
lp15@66289
   290
lemma segment_bound:
lp15@66289
   291
  assumes "x \<in> closed_segment a b"
lp15@66289
   292
  shows "norm (x - a) \<le> norm (b - a)" "norm (x - b) \<le> norm (b - a)"
lp15@66289
   293
apply (simp add: assms segment_bound1)
lp15@66289
   294
by (metis assms closed_segment_commute dist_commute dist_norm segment_bound1)
lp15@66289
   295
lp15@66289
   296
lemma open_segment_commute: "open_segment a b = open_segment b a"
lp15@66289
   297
proof -
lp15@66289
   298
  have "{a, b} = {b, a}" by auto
lp15@66289
   299
  thus ?thesis
lp15@66289
   300
    by (simp add: closed_segment_commute open_segment_def)
lp15@66289
   301
qed
lp15@66289
   302
lp15@66289
   303
lemma closed_segment_idem [simp]: "closed_segment a a = {a}"
lp15@66289
   304
  unfolding segment by (auto simp add: algebra_simps)
lp15@66289
   305
lp15@66289
   306
lemma open_segment_idem [simp]: "open_segment a a = {}"
lp15@66289
   307
  by (simp add: open_segment_def)
lp15@66289
   308
lp15@66289
   309
lemma closed_segment_eq_open: "closed_segment a b = open_segment a b \<union> {a,b}"
lp15@66289
   310
  using open_segment_def by auto
lp15@66289
   311
lp15@66289
   312
lemma convex_contains_open_segment:
lp15@66289
   313
  "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. open_segment a b \<subseteq> s)"
lp15@66289
   314
  by (simp add: convex_contains_segment closed_segment_eq_open)
lp15@66289
   315
lp15@66289
   316
lemma closed_segment_eq_real_ivl:
lp15@66289
   317
  fixes a b::real
lp15@66289
   318
  shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
lp15@66289
   319
proof -
lp15@66289
   320
  have "b \<le> a \<Longrightarrow> closed_segment b a = {b .. a}"
lp15@66289
   321
    and "a \<le> b \<Longrightarrow> closed_segment a b = {a .. b}"
lp15@66289
   322
    by (auto simp: convex_hull_eq_real_cbox segment_convex_hull)
lp15@66289
   323
  thus ?thesis
lp15@66289
   324
    by (auto simp: closed_segment_commute)
lp15@66289
   325
qed
lp15@66289
   326
lp15@66289
   327
lemma open_segment_eq_real_ivl:
lp15@66289
   328
  fixes a b::real
lp15@66289
   329
  shows "open_segment a b = (if a \<le> b then {a<..<b} else {b<..<a})"
lp15@66289
   330
by (auto simp: closed_segment_eq_real_ivl open_segment_def split: if_split_asm)
lp15@66289
   331
lp15@66289
   332
lemma closed_segment_real_eq:
lp15@66289
   333
  fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"
lp15@66289
   334
  by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)
lp15@66289
   335
lp15@66289
   336
lemma dist_in_closed_segment:
lp15@66289
   337
  fixes a :: "'a :: euclidean_space"
lp15@66289
   338
  assumes "x \<in> closed_segment a b"
lp15@66289
   339
    shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b"
lp15@66289
   340
proof (intro conjI)
lp15@66289
   341
  obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
lp15@66289
   342
    using assms by (force simp: in_segment algebra_simps)
lp15@66289
   343
  have "dist x a = u * dist a b"
lp15@66289
   344
    apply (simp add: dist_norm algebra_simps x)
lp15@66289
   345
    by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib)
lp15@66289
   346
  also have "...  \<le> dist a b"
lp15@66289
   347
    by (simp add: mult_left_le_one_le u)
lp15@66289
   348
  finally show "dist x a \<le> dist a b" .
lp15@66289
   349
  have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
lp15@66289
   350
    by (simp add: dist_norm algebra_simps x)
lp15@66289
   351
  also have "... = (1-u) * dist a b"
lp15@66289
   352
  proof -
lp15@66289
   353
    have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
lp15@66289
   354
      using \<open>u \<le> 1\<close> by force
immler@67685
   355
    then show ?thesis
lp15@66289
   356
      by (simp add: dist_norm real_vector.scale_right_diff_distrib)
lp15@66289
   357
  qed
lp15@66289
   358
  also have "... \<le> dist a b"
lp15@66289
   359
    by (simp add: mult_left_le_one_le u)
lp15@66289
   360
  finally show "dist x b \<le> dist a b" .
lp15@66289
   361
qed
lp15@66289
   362
lp15@66289
   363
lemma dist_in_open_segment:
lp15@66289
   364
  fixes a :: "'a :: euclidean_space"
lp15@66289
   365
  assumes "x \<in> open_segment a b"
lp15@66289
   366
    shows "dist x a < dist a b \<and> dist x b < dist a b"
lp15@66289
   367
proof (intro conjI)
lp15@66289
   368
  obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
lp15@66289
   369
    using assms by (force simp: in_segment algebra_simps)
lp15@66289
   370
  have "dist x a = u * dist a b"
lp15@66289
   371
    apply (simp add: dist_norm algebra_simps x)
lp15@66289
   372
    by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>)
lp15@66289
   373
  also have *: "...  < dist a b"
lp15@66289
   374
    by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 \<open>u < 1\<close>)
lp15@66289
   375
  finally show "dist x a < dist a b" .
lp15@66289
   376
  have ab_ne0: "dist a b \<noteq> 0"
lp15@66289
   377
    using * by fastforce
lp15@66289
   378
  have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
lp15@66289
   379
    by (simp add: dist_norm algebra_simps x)
lp15@66289
   380
  also have "... = (1-u) * dist a b"
lp15@66289
   381
  proof -
lp15@66289
   382
    have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
lp15@66289
   383
      using \<open>u < 1\<close> by force
lp15@66289
   384
    then show ?thesis
lp15@66289
   385
      by (simp add: dist_norm real_vector.scale_right_diff_distrib)
lp15@66289
   386
  qed
lp15@66289
   387
  also have "... < dist a b"
lp15@66289
   388
    using ab_ne0 \<open>0 < u\<close> by simp
lp15@66289
   389
  finally show "dist x b < dist a b" .
lp15@66289
   390
qed
lp15@66289
   391
lp15@66289
   392
lemma dist_decreases_open_segment_0:
lp15@66289
   393
  fixes x :: "'a :: euclidean_space"
lp15@66289
   394
  assumes "x \<in> open_segment 0 b"
lp15@66289
   395
    shows "dist c x < dist c 0 \<or> dist c x < dist c b"
lp15@66289
   396
proof (rule ccontr, clarsimp simp: not_less)
lp15@66289
   397
  obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b"
lp15@66289
   398
    using assms by (auto simp: in_segment)
lp15@66289
   399
  have xb: "x \<bullet> b < b \<bullet> b"
lp15@66289
   400
    using u x by auto
lp15@66289
   401
  assume "norm c \<le> dist c x"
lp15@66289
   402
  then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)"
lp15@66289
   403
    by (simp add: dist_norm norm_le)
lp15@66289
   404
  moreover have "0 < x \<bullet> b"
lp15@66289
   405
    using u x by auto
lp15@66289
   406
  ultimately have less: "c \<bullet> b < x \<bullet> b"
lp15@66289
   407
    by (simp add: x algebra_simps inner_commute u)
lp15@66289
   408
  assume "dist c b \<le> dist c x"
lp15@66289
   409
  then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)"
lp15@66289
   410
    by (simp add: dist_norm norm_le)
lp15@66289
   411
  then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)"
lp15@66289
   412
    by (simp add: x algebra_simps inner_commute)
lp15@66289
   413
  then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)"
lp15@66289
   414
    by (simp add: algebra_simps)
lp15@66289
   415
  then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)"
lp15@66289
   416
    using \<open>u < 1\<close> by auto
lp15@66289
   417
  with xb have "c \<bullet> b \<ge> x \<bullet> b"
lp15@66289
   418
    by (auto simp: x algebra_simps inner_commute)
lp15@66289
   419
  with less show False by auto
lp15@66289
   420
qed
lp15@66289
   421
lp15@66289
   422
proposition dist_decreases_open_segment:
lp15@66289
   423
  fixes a :: "'a :: euclidean_space"
lp15@66289
   424
  assumes "x \<in> open_segment a b"
lp15@66289
   425
    shows "dist c x < dist c a \<or> dist c x < dist c b"
lp15@66289
   426
proof -
lp15@66289
   427
  have *: "x - a \<in> open_segment 0 (b - a)" using assms
lp15@66289
   428
    by (metis diff_self open_segment_translation_eq uminus_add_conv_diff)
lp15@66289
   429
  show ?thesis
lp15@66289
   430
    using dist_decreases_open_segment_0 [OF *, of "c-a"] assms
lp15@66289
   431
    by (simp add: dist_norm)
lp15@66289
   432
qed
lp15@66289
   433
lp15@66289
   434
corollary open_segment_furthest_le:
lp15@66289
   435
  fixes a b x y :: "'a::euclidean_space"
lp15@66289
   436
  assumes "x \<in> open_segment a b"
lp15@66289
   437
  shows "norm (y - x) < norm (y - a) \<or>  norm (y - x) < norm (y - b)"
lp15@66289
   438
  by (metis assms dist_decreases_open_segment dist_norm)
lp15@66289
   439
lp15@66289
   440
corollary dist_decreases_closed_segment:
lp15@66289
   441
  fixes a :: "'a :: euclidean_space"
lp15@66289
   442
  assumes "x \<in> closed_segment a b"
lp15@66289
   443
    shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b"
lp15@66289
   444
apply (cases "x \<in> open_segment a b")
lp15@66289
   445
 using dist_decreases_open_segment less_eq_real_def apply blast
lp15@66289
   446
by (metis DiffI assms empty_iff insertE open_segment_def order_refl)
lp15@66289
   447
lp15@66289
   448
lemma convex_intermediate_ball:
lp15@66289
   449
  fixes a :: "'a :: euclidean_space"
lp15@66289
   450
  shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T"
lp15@66289
   451
apply (simp add: convex_contains_open_segment, clarify)
lp15@66289
   452
by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
lp15@66289
   453
lp15@66289
   454
lemma csegment_midpoint_subset: "closed_segment (midpoint a b) b \<subseteq> closed_segment a b"
lp15@66289
   455
  apply (clarsimp simp: midpoint_def in_segment)
lp15@66289
   456
  apply (rule_tac x="(1 + u) / 2" in exI)
lp15@66289
   457
  apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib)
lp15@68527
   458
  by (metis field_sum_of_halves scaleR_left.add)
lp15@66289
   459
lp15@66289
   460
lemma notin_segment_midpoint:
lp15@66289
   461
  fixes a :: "'a :: euclidean_space"
lp15@66289
   462
  shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b"
lp15@66289
   463
by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
lp15@66289
   464
lp15@66289
   465
lemma segment_to_closest_point:
lp15@66289
   466
  fixes S :: "'a :: euclidean_space set"
lp15@66289
   467
  shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}"
lp15@66289
   468
  apply (subst disjoint_iff_not_equal)
lp15@66289
   469
  apply (clarify dest!: dist_in_open_segment)
lp15@66289
   470
  by (metis closest_point_le dist_commute le_less_trans less_irrefl)
lp15@66289
   471
lp15@66289
   472
lemma segment_to_point_exists:
lp15@66289
   473
  fixes S :: "'a :: euclidean_space set"
lp15@66289
   474
    assumes "closed S" "S \<noteq> {}"
lp15@66289
   475
    obtains b where "b \<in> S" "open_segment a b \<inter> S = {}"
lp15@66289
   476
  by (metis assms segment_to_closest_point closest_point_exists that)
lp15@66289
   477
lp15@66289
   478
subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
lp15@66289
   479
lp15@66289
   480
lemma segment_eq_compose:
lp15@66289
   481
  fixes a :: "'a :: real_vector"
lp15@66289
   482
  shows "(\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) = (\<lambda>x. a + x) o (\<lambda>u. u *\<^sub>R (b - a))"
lp15@66289
   483
    by (simp add: o_def algebra_simps)
lp15@66289
   484
lp15@66289
   485
lemma segment_degen_1:
lp15@66289
   486
  fixes a :: "'a :: real_vector"
lp15@66289
   487
  shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = b \<longleftrightarrow> a=b \<or> u=1"
lp15@66289
   488
proof -
lp15@66289
   489
  { assume "(1 - u) *\<^sub>R a + u *\<^sub>R b = b"
lp15@66289
   490
    then have "(1 - u) *\<^sub>R a = (1 - u) *\<^sub>R b"
lp15@66289
   491
      by (simp add: algebra_simps)
lp15@66289
   492
    then have "a=b \<or> u=1"
lp15@66289
   493
      by simp
lp15@66289
   494
  } then show ?thesis
lp15@66289
   495
      by (auto simp: algebra_simps)
lp15@66289
   496
qed
lp15@66289
   497
lp15@66289
   498
lemma segment_degen_0:
lp15@66289
   499
    fixes a :: "'a :: real_vector"
lp15@66289
   500
    shows "(1 - u) *\<^sub>R a + u *\<^sub>R b = a \<longleftrightarrow> a=b \<or> u=0"
lp15@66289
   501
  using segment_degen_1 [of "1-u" b a]
lp15@66289
   502
  by (auto simp: algebra_simps)
lp15@66289
   503
lp15@66289
   504
lemma add_scaleR_degen:
lp15@66289
   505
  fixes a b ::"'a::real_vector"
lp15@66289
   506
  assumes  "(u *\<^sub>R b + v *\<^sub>R a) = (u *\<^sub>R a + v *\<^sub>R b)"  "u \<noteq> v"
lp15@66289
   507
  shows "a=b"
lp15@66289
   508
  by (metis (no_types, hide_lams) add.commute add_diff_eq diff_add_cancel real_vector.scale_cancel_left real_vector.scale_left_diff_distrib assms)
lp15@66289
   509
  
lp15@66289
   510
lemma closed_segment_image_interval:
lp15@66289
   511
     "closed_segment a b = (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0..1}"
lp15@66289
   512
  by (auto simp: set_eq_iff image_iff closed_segment_def)
lp15@66289
   513
lp15@66289
   514
lemma open_segment_image_interval:
lp15@66289
   515
     "open_segment a b = (if a=b then {} else (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1})"
lp15@66289
   516
  by (auto simp:  open_segment_def closed_segment_def segment_degen_0 segment_degen_1)
lp15@66289
   517
lp15@66289
   518
lemmas segment_image_interval = closed_segment_image_interval open_segment_image_interval
lp15@66289
   519
lp15@66289
   520
lemma open_segment_bound1:
lp15@66289
   521
  assumes "x \<in> open_segment a b"
lp15@66289
   522
  shows "norm (x - a) < norm (b - a)"
lp15@66289
   523
proof -
lp15@66289
   524
  obtain u where "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 < u" "u < 1" "a \<noteq> b"
lp15@66289
   525
    using assms by (auto simp add: open_segment_image_interval split: if_split_asm)
lp15@66289
   526
  then show "norm (x - a) < norm (b - a)"
lp15@66289
   527
    apply clarify
lp15@66289
   528
    apply (auto simp: algebra_simps)
lp15@66289
   529
    apply (simp add: scaleR_diff_right [symmetric])
lp15@66289
   530
    done
lp15@66289
   531
qed
lp15@66289
   532
lp15@66289
   533
lemma compact_segment [simp]:
lp15@66289
   534
  fixes a :: "'a::real_normed_vector"
lp15@66289
   535
  shows "compact (closed_segment a b)"
lp15@66289
   536
  by (auto simp: segment_image_interval intro!: compact_continuous_image continuous_intros)
lp15@66289
   537
lp15@66289
   538
lemma closed_segment [simp]:
lp15@66289
   539
  fixes a :: "'a::real_normed_vector"
lp15@66289
   540
  shows "closed (closed_segment a b)"
lp15@66289
   541
  by (simp add: compact_imp_closed)
lp15@66289
   542
lp15@66289
   543
lemma closure_closed_segment [simp]:
lp15@66289
   544
  fixes a :: "'a::real_normed_vector"
lp15@66289
   545
  shows "closure(closed_segment a b) = closed_segment a b"
lp15@66289
   546
  by simp
lp15@66289
   547
lp15@66289
   548
lemma open_segment_bound:
lp15@66289
   549
  assumes "x \<in> open_segment a b"
lp15@66289
   550
  shows "norm (x - a) < norm (b - a)" "norm (x - b) < norm (b - a)"
lp15@66289
   551
apply (simp add: assms open_segment_bound1)
lp15@66289
   552
by (metis assms norm_minus_commute open_segment_bound1 open_segment_commute)
lp15@66289
   553
lp15@66289
   554
lemma closure_open_segment [simp]:
haftmann@69661
   555
  "closure (open_segment a b) = (if a = b then {} else closed_segment a b)"
haftmann@69661
   556
    for a :: "'a::euclidean_space"
haftmann@69661
   557
proof (cases "a = b")
haftmann@69661
   558
  case True
haftmann@69661
   559
  then show ?thesis
haftmann@69661
   560
    by simp
haftmann@69661
   561
next
haftmann@69661
   562
  case False
haftmann@69661
   563
  have "closure ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1}) = (\<lambda>u. u *\<^sub>R (b - a)) ` closure {0<..<1}"
lp15@66289
   564
    apply (rule closure_injective_linear_image [symmetric])
haftmann@69661
   565
     apply (use False in \<open>auto intro!: injI\<close>)
haftmann@69661
   566
    done
haftmann@69661
   567
  then have "closure
haftmann@69661
   568
     ((\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) ` {0<..<1}) =
haftmann@69661
   569
    (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b) ` closure {0<..<1}"
haftmann@69661
   570
    using closure_translation [of a "((\<lambda>x. x *\<^sub>R b - x *\<^sub>R a) ` {0<..<1})"]
haftmann@69661
   571
    by (simp add: segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right image_image)
lp15@66289
   572
  then show ?thesis
haftmann@69661
   573
    by (simp add: segment_image_interval closure_greaterThanLessThan [symmetric] del: closure_greaterThanLessThan)
lp15@66289
   574
qed
lp15@66289
   575
lp15@66289
   576
lemma closed_open_segment_iff [simp]:
lp15@66289
   577
    fixes a :: "'a::euclidean_space"  shows "closed(open_segment a b) \<longleftrightarrow> a = b"
lp15@66289
   578
  by (metis open_segment_def DiffE closure_eq closure_open_segment ends_in_segment(1) insert_iff segment_image_interval(2))
lp15@66289
   579
lp15@66289
   580
lemma compact_open_segment_iff [simp]:
lp15@66289
   581
    fixes a :: "'a::euclidean_space"  shows "compact(open_segment a b) \<longleftrightarrow> a = b"
lp15@66289
   582
  by (simp add: bounded_open_segment compact_eq_bounded_closed)
lp15@66289
   583
lp15@66289
   584
lemma convex_closed_segment [iff]: "convex (closed_segment a b)"
lp15@66289
   585
  unfolding segment_convex_hull by(rule convex_convex_hull)
lp15@66289
   586
haftmann@69661
   587
lemma convex_open_segment [iff]: "convex (open_segment a b)"
haftmann@69661
   588
proof -
haftmann@69661
   589
  have "convex ((\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})"
lp15@66289
   590
    by (rule convex_linear_image) auto
haftmann@69661
   591
  then have "convex ((+) a ` (\<lambda>u. u *\<^sub>R (b - a)) ` {0<..<1})"
haftmann@69661
   592
    by (rule convex_translation)
lp15@66289
   593
  then show ?thesis
haftmann@69661
   594
    by (simp add: image_image open_segment_image_interval segment_eq_compose field_simps scaleR_diff_left scaleR_diff_right)
lp15@66289
   595
qed
lp15@66289
   596
lp15@66289
   597
lemmas convex_segment = convex_closed_segment convex_open_segment
lp15@66289
   598
lp15@66289
   599
lemma connected_segment [iff]:
lp15@66289
   600
  fixes x :: "'a :: real_normed_vector"
lp15@66289
   601
  shows "connected (closed_segment x y)"
lp15@66289
   602
  by (simp add: convex_connected)
lp15@66289
   603
immler@67685
   604
lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real
immler@67685
   605
  by (auto simp: is_interval_convex_1)
immler@67685
   606
immler@67685
   607
lemma IVT'_closed_segment_real:
immler@67685
   608
  fixes f :: "real \<Rightarrow> real"
immler@67685
   609
  assumes "y \<in> closed_segment (f a) (f b)"
immler@67685
   610
  assumes "continuous_on (closed_segment a b) f"
immler@67685
   611
  shows "\<exists>x \<in> closed_segment a b. f x = y"
immler@67685
   612
  using IVT'[of f a y b]
immler@67685
   613
    IVT'[of "-f" a "-y" b]
immler@67685
   614
    IVT'[of f b y a]
immler@67685
   615
    IVT'[of "-f" b "-y" a] assms
immler@67685
   616
  by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)
immler@67685
   617
immler@67685
   618
immler@67685
   619
subsection\<open>Starlike sets\<close>
immler@67685
   620
immler@67962
   621
definition%important "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
immler@67685
   622
immler@67685
   623
lemma starlike_UNIV [simp]: "starlike UNIV"
immler@67685
   624
  by (simp add: starlike_def)
immler@67685
   625
immler@67685
   626
lemma convex_imp_starlike:
immler@67685
   627
  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
immler@67685
   628
  unfolding convex_contains_segment starlike_def by auto
immler@67685
   629
immler@67685
   630
lp15@66289
   631
lemma affine_hull_closed_segment [simp]:
lp15@66289
   632
     "affine hull (closed_segment a b) = affine hull {a,b}"
lp15@66289
   633
  by (simp add: segment_convex_hull)
lp15@66289
   634
lp15@66289
   635
lemma affine_hull_open_segment [simp]:
lp15@66289
   636
    fixes a :: "'a::euclidean_space"
lp15@66289
   637
    shows "affine hull (open_segment a b) = (if a = b then {} else affine hull {a,b})"
lp15@66289
   638
by (metis affine_hull_convex_hull affine_hull_empty closure_open_segment closure_same_affine_hull segment_convex_hull)
lp15@66289
   639
lp15@66289
   640
lemma rel_interior_closure_convex_segment:
lp15@66289
   641
  fixes S :: "_::euclidean_space set"
lp15@66289
   642
  assumes "convex S" "a \<in> rel_interior S" "b \<in> closure S"
lp15@66289
   643
    shows "open_segment a b \<subseteq> rel_interior S"
lp15@66289
   644
proof
lp15@66289
   645
  fix x
lp15@66289
   646
  have [simp]: "(1 - u) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>R (b - a)" for u
lp15@66289
   647
    by (simp add: algebra_simps)
lp15@66289
   648
  assume "x \<in> open_segment a b"
lp15@66289
   649
  then show "x \<in> rel_interior S"
lp15@66289
   650
    unfolding closed_segment_def open_segment_def  using assms
lp15@66289
   651
    by (auto intro: rel_interior_closure_convex_shrink)
lp15@66289
   652
qed
lp15@66289
   653
lp15@66289
   654
lemma convex_hull_insert_segments:
lp15@66289
   655
   "convex hull (insert a S) =
lp15@66289
   656
    (if S = {} then {a} else  \<Union>x \<in> convex hull S. closed_segment a x)"
lp15@66289
   657
  by (force simp add: convex_hull_insert_alt in_segment)
lp15@66289
   658
lp15@66289
   659
lemma Int_convex_hull_insert_rel_exterior:
lp15@66289
   660
  fixes z :: "'a::euclidean_space"
lp15@66289
   661
  assumes "convex C" "T \<subseteq> C" and z: "z \<in> rel_interior C" and dis: "disjnt S (rel_interior C)"
lp15@66289
   662
  shows "S \<inter> (convex hull (insert z T)) = S \<inter> (convex hull T)" (is "?lhs = ?rhs")
lp15@66289
   663
proof
lp15@66289
   664
  have "T = {} \<Longrightarrow> z \<notin> S"
lp15@66289
   665
    using dis z by (auto simp add: disjnt_def)
lp15@66289
   666
  then show "?lhs \<subseteq> ?rhs"
lp15@66289
   667
  proof (clarsimp simp add: convex_hull_insert_segments)
lp15@66289
   668
    fix x y
lp15@66289
   669
    assume "x \<in> S" and y: "y \<in> convex hull T" and "x \<in> closed_segment z y"
lp15@66289
   670
    have "y \<in> closure C"
lp15@66289
   671
      by (metis y \<open>convex C\<close> \<open>T \<subseteq> C\<close> closure_subset contra_subsetD convex_hull_eq hull_mono)
lp15@66289
   672
    moreover have "x \<notin> rel_interior C"
lp15@66289
   673
      by (meson \<open>x \<in> S\<close> dis disjnt_iff)
lp15@66289
   674
    moreover have "x \<in> open_segment z y \<union> {z, y}"
lp15@66289
   675
      using \<open>x \<in> closed_segment z y\<close> closed_segment_eq_open by blast
lp15@66289
   676
    ultimately show "x \<in> convex hull T"
lp15@66289
   677
      using rel_interior_closure_convex_segment [OF \<open>convex C\<close> z]
lp15@66289
   678
      using y z by blast
lp15@66289
   679
  qed
lp15@66289
   680
  show "?rhs \<subseteq> ?lhs"
lp15@66289
   681
    by (meson hull_mono inf_mono subset_insertI subset_refl)
lp15@66289
   682
qed
lp15@66289
   683
immler@67962
   684
subsection%unimportant\<open>More results about segments\<close>
lp15@66289
   685
lp15@66289
   686
lemma dist_half_times2:
lp15@66289
   687
  fixes a :: "'a :: real_normed_vector"
lp15@66289
   688
  shows "dist ((1 / 2) *\<^sub>R (a + b)) x * 2 = dist (a+b) (2 *\<^sub>R x)"
lp15@66289
   689
proof -
lp15@66289
   690
  have "norm ((1 / 2) *\<^sub>R (a + b) - x) * 2 = norm (2 *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x))"
lp15@66289
   691
    by simp
lp15@66289
   692
  also have "... = norm ((a + b) - 2 *\<^sub>R x)"
lp15@66289
   693
    by (simp add: real_vector.scale_right_diff_distrib)
lp15@66289
   694
  finally show ?thesis
lp15@66289
   695
    by (simp only: dist_norm)
lp15@66289
   696
qed
lp15@66289
   697
lp15@66289
   698
lemma closed_segment_as_ball:
lp15@66289
   699
    "closed_segment a b = affine hull {a,b} \<inter> cball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
lp15@66289
   700
proof (cases "b = a")
lp15@66289
   701
  case True then show ?thesis by (auto simp: hull_inc)
lp15@66289
   702
next
lp15@66289
   703
  case False
lp15@66289
   704
  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
lp15@66289
   705
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
lp15@66289
   706
                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)" for x
lp15@66289
   707
  proof -
lp15@66289
   708
    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
lp15@66289
   709
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a)) =
lp15@66289
   710
          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
lp15@66289
   711
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 \<le> norm (b - a))"
lp15@66289
   712
      unfolding eq_diff_eq [symmetric] by simp
lp15@66289
   713
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
lp15@66289
   714
                          norm ((a+b) - (2 *\<^sub>R x)) \<le> norm (b - a))"
lp15@66289
   715
      by (simp add: dist_half_times2) (simp add: dist_norm)
lp15@66289
   716
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
lp15@66289
   717
            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) \<le> norm (b - a))"
lp15@66289
   718
      by auto
lp15@66289
   719
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
lp15@66289
   720
                norm ((1 - u * 2) *\<^sub>R (b - a)) \<le> norm (b - a))"
lp15@66289
   721
      by (simp add: algebra_simps scaleR_2)
lp15@66289
   722
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
lp15@66289
   723
                          \<bar>1 - u * 2\<bar> * norm (b - a) \<le> norm (b - a))"
lp15@66289
   724
      by simp
lp15@66289
   725
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> \<le> 1)"
lp15@66289
   726
      by (simp add: mult_le_cancel_right2 False)
lp15@66289
   727
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1)"
lp15@66289
   728
      by auto
lp15@66289
   729
    finally show ?thesis .
lp15@66289
   730
  qed
lp15@66289
   731
  show ?thesis
lp15@66289
   732
    by (simp add: affine_hull_2 Set.set_eq_iff closed_segment_def *)
lp15@66289
   733
qed
lp15@66289
   734
lp15@66289
   735
lemma open_segment_as_ball:
lp15@66289
   736
    "open_segment a b =
lp15@66289
   737
     affine hull {a,b} \<inter> ball(inverse 2 *\<^sub>R (a + b))(norm(b - a) / 2)"
lp15@66289
   738
proof (cases "b = a")
lp15@66289
   739
  case True then show ?thesis by (auto simp: hull_inc)
lp15@66289
   740
next
lp15@66289
   741
  case False
lp15@66289
   742
  then have *: "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
lp15@66289
   743
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
lp15@66289
   744
                 (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)" for x
lp15@66289
   745
  proof -
lp15@66289
   746
    have "((\<exists>u v. x = u *\<^sub>R a + v *\<^sub>R b \<and> u + v = 1) \<and>
lp15@66289
   747
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a)) =
lp15@66289
   748
          ((\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b) \<and>
lp15@66289
   749
                  dist ((1 / 2) *\<^sub>R (a + b)) x * 2 < norm (b - a))"
lp15@66289
   750
      unfolding eq_diff_eq [symmetric] by simp
lp15@66289
   751
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
lp15@66289
   752
                          norm ((a+b) - (2 *\<^sub>R x)) < norm (b - a))"
lp15@66289
   753
      by (simp add: dist_half_times2) (simp add: dist_norm)
lp15@66289
   754
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
lp15@66289
   755
            norm ((a+b) - (2 *\<^sub>R ((1 - u) *\<^sub>R a + u *\<^sub>R b))) < norm (b - a))"
lp15@66289
   756
      by auto
lp15@66289
   757
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
lp15@66289
   758
                norm ((1 - u * 2) *\<^sub>R (b - a)) < norm (b - a))"
lp15@66289
   759
      by (simp add: algebra_simps scaleR_2)
lp15@66289
   760
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and>
lp15@66289
   761
                          \<bar>1 - u * 2\<bar> * norm (b - a) < norm (b - a))"
lp15@66289
   762
      by simp
lp15@66289
   763
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> \<bar>1 - u * 2\<bar> < 1)"
lp15@66289
   764
      by (simp add: mult_le_cancel_right2 False)
lp15@66289
   765
    also have "... = (\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 < u \<and> u < 1)"
lp15@66289
   766
      by auto
lp15@66289
   767
    finally show ?thesis .
lp15@66289
   768
  qed
lp15@66289
   769
  show ?thesis
lp15@66289
   770
    using False by (force simp: affine_hull_2 Set.set_eq_iff open_segment_image_interval *)
lp15@66289
   771
qed
lp15@66289
   772
lp15@66289
   773
lemmas segment_as_ball = closed_segment_as_ball open_segment_as_ball
lp15@66289
   774
lp15@66289
   775
lemma closed_segment_neq_empty [simp]: "closed_segment a b \<noteq> {}"
lp15@66289
   776
  by auto
lp15@66289
   777
lp15@66289
   778
lemma open_segment_eq_empty [simp]: "open_segment a b = {} \<longleftrightarrow> a = b"
lp15@66289
   779
proof -
lp15@66289
   780
  { assume a1: "open_segment a b = {}"
lp15@66289
   781
    have "{} \<noteq> {0::real<..<1}"
lp15@66289
   782
      by simp
lp15@66289
   783
    then have "a = b"
lp15@66289
   784
      using a1 open_segment_image_interval by fastforce
lp15@66289
   785
  } then show ?thesis by auto
lp15@66289
   786
qed
lp15@66289
   787
lp15@66289
   788
lemma open_segment_eq_empty' [simp]: "{} = open_segment a b \<longleftrightarrow> a = b"
lp15@66289
   789
  using open_segment_eq_empty by blast
lp15@66289
   790
lp15@66289
   791
lemmas segment_eq_empty = closed_segment_neq_empty open_segment_eq_empty
lp15@66289
   792
lp15@66289
   793
lemma inj_segment:
lp15@66289
   794
  fixes a :: "'a :: real_vector"
lp15@66289
   795
  assumes "a \<noteq> b"
lp15@66289
   796
    shows "inj_on (\<lambda>u. (1 - u) *\<^sub>R a + u *\<^sub>R b) I"
lp15@66289
   797
proof
lp15@66289
   798
  fix x y
lp15@66289
   799
  assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b"
lp15@66289
   800
  then have "x *\<^sub>R (b - a) = y *\<^sub>R (b - a)"
lp15@66289
   801
    by (simp add: algebra_simps)
lp15@66289
   802
  with assms show "x = y"
lp15@66289
   803
    by (simp add: real_vector.scale_right_imp_eq)
lp15@66289
   804
qed
lp15@66289
   805
lp15@66289
   806
lemma finite_closed_segment [simp]: "finite(closed_segment a b) \<longleftrightarrow> a = b"
lp15@66289
   807
  apply auto
lp15@66289
   808
  apply (rule ccontr)
lp15@66289
   809
  apply (simp add: segment_image_interval)
lp15@66289
   810
  using infinite_Icc [OF zero_less_one] finite_imageD [OF _ inj_segment] apply blast
lp15@66289
   811
  done
lp15@66289
   812
lp15@66289
   813
lemma finite_open_segment [simp]: "finite(open_segment a b) \<longleftrightarrow> a = b"
lp15@66289
   814
  by (auto simp: open_segment_def)
lp15@66289
   815
lp15@66289
   816
lemmas finite_segment = finite_closed_segment finite_open_segment
lp15@66289
   817
lp15@66289
   818
lemma closed_segment_eq_sing: "closed_segment a b = {c} \<longleftrightarrow> a = c \<and> b = c"
lp15@66289
   819
  by auto
lp15@66289
   820
lp15@66289
   821
lemma open_segment_eq_sing: "open_segment a b \<noteq> {c}"
lp15@66289
   822
  by (metis finite_insert finite_open_segment insert_not_empty open_segment_image_interval)
lp15@66289
   823
lp15@66289
   824
lemmas segment_eq_sing = closed_segment_eq_sing open_segment_eq_sing
lp15@66289
   825
lp15@66289
   826
lemma subset_closed_segment:
lp15@66289
   827
    "closed_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
lp15@66289
   828
     a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
lp15@66289
   829
  by auto (meson contra_subsetD convex_closed_segment convex_contains_segment)
lp15@66289
   830
lp15@66289
   831
lemma subset_co_segment:
lp15@66289
   832
    "closed_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
lp15@66289
   833
     a \<in> open_segment c d \<and> b \<in> open_segment c d"
lp15@66289
   834
using closed_segment_subset by blast
lp15@66289
   835
lp15@66289
   836
lemma subset_open_segment:
lp15@66289
   837
  fixes a :: "'a::euclidean_space"
lp15@66289
   838
  shows "open_segment a b \<subseteq> open_segment c d \<longleftrightarrow>
lp15@66289
   839
         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
lp15@66289
   840
        (is "?lhs = ?rhs")
lp15@66289
   841
proof (cases "a = b")
lp15@66289
   842
  case True then show ?thesis by simp
lp15@66289
   843
next
lp15@66289
   844
  case False show ?thesis
lp15@66289
   845
  proof
lp15@66289
   846
    assume rhs: ?rhs
lp15@66289
   847
    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
lp15@66289
   848
      using closed_segment_idem singleton_iff by auto
lp15@66289
   849
    have "\<exists>uc. (1 - u) *\<^sub>R ((1 - ua) *\<^sub>R c + ua *\<^sub>R d) + u *\<^sub>R ((1 - ub) *\<^sub>R c + ub *\<^sub>R d) =
lp15@66289
   850
               (1 - uc) *\<^sub>R c + uc *\<^sub>R d \<and> 0 < uc \<and> uc < 1"
lp15@66289
   851
        if neq: "(1 - ua) *\<^sub>R c + ua *\<^sub>R d \<noteq> (1 - ub) *\<^sub>R c + ub *\<^sub>R d" "c \<noteq> d"
lp15@66289
   852
           and "a = (1 - ua) *\<^sub>R c + ua *\<^sub>R d" "b = (1 - ub) *\<^sub>R c + ub *\<^sub>R d"
lp15@66289
   853
           and u: "0 < u" "u < 1" and uab: "0 \<le> ua" "ua \<le> 1" "0 \<le> ub" "ub \<le> 1"
lp15@66289
   854
        for u ua ub
lp15@66289
   855
    proof -
lp15@66289
   856
      have "ua \<noteq> ub"
lp15@66289
   857
        using neq by auto
lp15@66289
   858
      moreover have "(u - 1) * ua \<le> 0" using u uab
lp15@66289
   859
        by (simp add: mult_nonpos_nonneg)
lp15@66289
   860
      ultimately have lt: "(u - 1) * ua < u * ub" using u uab
lp15@66289
   861
        by (metis antisym_conv diff_ge_0_iff_ge le_less_trans mult_eq_0_iff mult_le_0_iff not_less)
lp15@66289
   862
      have "p * ua + q * ub < p+q" if p: "0 < p" and  q: "0 < q" for p q
lp15@66289
   863
      proof -
lp15@66289
   864
        have "\<not> p \<le> 0" "\<not> q \<le> 0"
lp15@66289
   865
          using p q not_less by blast+
lp15@66289
   866
        then show ?thesis
lp15@66289
   867
          by (metis \<open>ua \<noteq> ub\<close> add_less_cancel_left add_less_cancel_right add_mono_thms_linordered_field(5)
lp15@66289
   868
                    less_eq_real_def mult_cancel_left1 mult_less_cancel_left2 uab(2) uab(4))
lp15@66289
   869
      qed
lp15@66289
   870
      then have "(1 - u) * ua + u * ub < 1" using u \<open>ua \<noteq> ub\<close>
lp15@66289
   871
        by (metis diff_add_cancel diff_gt_0_iff_gt)
lp15@66289
   872
      with lt show ?thesis
lp15@66289
   873
        by (rule_tac x="ua + u*(ub-ua)" in exI) (simp add: algebra_simps)
lp15@66289
   874
    qed
lp15@66289
   875
    with rhs \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close> show ?lhs
lp15@66289
   876
      unfolding open_segment_image_interval closed_segment_def
lp15@66289
   877
      by (fastforce simp add:)
lp15@66289
   878
  next
lp15@66289
   879
    assume lhs: ?lhs
lp15@66289
   880
    with \<open>a \<noteq> b\<close> have "c \<noteq> d"
lp15@66289
   881
      by (meson finite_open_segment rev_finite_subset)
lp15@66289
   882
    have "closure (open_segment a b) \<subseteq> closure (open_segment c d)"
lp15@66289
   883
      using lhs closure_mono by blast
lp15@66289
   884
    then have "closed_segment a b \<subseteq> closed_segment c d"
lp15@66289
   885
      by (simp add: \<open>a \<noteq> b\<close> \<open>c \<noteq> d\<close>)
lp15@66289
   886
    then show ?rhs
lp15@66289
   887
      by (force simp: \<open>a \<noteq> b\<close>)
lp15@66289
   888
  qed
lp15@66289
   889
qed
lp15@66289
   890
lp15@66289
   891
lemma subset_oc_segment:
lp15@66289
   892
  fixes a :: "'a::euclidean_space"
lp15@66289
   893
  shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
lp15@66289
   894
         a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
lp15@66289
   895
apply (simp add: subset_open_segment [symmetric])
lp15@66289
   896
apply (rule iffI)
lp15@66289
   897
 apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
lp15@66289
   898
apply (meson dual_order.trans segment_open_subset_closed)
lp15@66289
   899
done
lp15@66289
   900
lp15@66289
   901
lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
lp15@66289
   902
lp15@66289
   903
lp15@66289
   904
subsection\<open>Betweenness\<close>
lp15@66289
   905
immler@67962
   906
definition%important "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
lp15@66289
   907
lp15@66289
   908
lemma betweenI:
lp15@66289
   909
  assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
lp15@66289
   910
  shows "between (a, b) x"
lp15@66289
   911
using assms unfolding between_def closed_segment_def by auto
lp15@66289
   912
lp15@66289
   913
lemma betweenE:
lp15@66289
   914
  assumes "between (a, b) x"
lp15@66289
   915
  obtains u where "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
lp15@66289
   916
using assms unfolding between_def closed_segment_def by auto
lp15@66289
   917
lp15@66289
   918
lemma between_implies_scaled_diff:
lp15@66289
   919
  assumes "between (S, T) X" "between (S, T) Y" "S \<noteq> Y"
lp15@66289
   920
  obtains c where "(X - Y) = c *\<^sub>R (S - Y)"
lp15@66289
   921
proof -
lp15@66289
   922
  from \<open>between (S, T) X\<close> obtain u\<^sub>X where X: "X = u\<^sub>X *\<^sub>R S + (1 - u\<^sub>X) *\<^sub>R T"
lp15@66289
   923
    by (metis add.commute betweenE eq_diff_eq)
lp15@66289
   924
  from \<open>between (S, T) Y\<close> obtain u\<^sub>Y where Y: "Y = u\<^sub>Y *\<^sub>R S + (1 - u\<^sub>Y) *\<^sub>R T"
lp15@66289
   925
    by (metis add.commute betweenE eq_diff_eq)
lp15@66289
   926
  have "X - Y = (u\<^sub>X - u\<^sub>Y) *\<^sub>R (S - T)"
lp15@66289
   927
  proof -
lp15@66289
   928
    from X Y have "X - Y =  u\<^sub>X *\<^sub>R S - u\<^sub>Y *\<^sub>R S + ((1 - u\<^sub>X) *\<^sub>R T - (1 - u\<^sub>Y) *\<^sub>R T)" by simp
lp15@66289
   929
    also have "\<dots> = (u\<^sub>X - u\<^sub>Y) *\<^sub>R S - (u\<^sub>X - u\<^sub>Y) *\<^sub>R T" by (simp add: scaleR_left.diff)
lp15@66289
   930
    finally show ?thesis by (simp add: real_vector.scale_right_diff_distrib)
lp15@66289
   931
  qed
lp15@66289
   932
  moreover from Y have "S - Y = (1 - u\<^sub>Y) *\<^sub>R (S - T)"
lp15@66289
   933
    by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
lp15@66289
   934
  moreover note \<open>S \<noteq> Y\<close>
lp15@66289
   935
  ultimately have "(X - Y) = ((u\<^sub>X - u\<^sub>Y) / (1 - u\<^sub>Y)) *\<^sub>R (S - Y)" by auto
lp15@66289
   936
  from this that show thesis by blast
lp15@66289
   937
qed
lp15@66289
   938
lp15@66289
   939
lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
lp15@66289
   940
  unfolding between_def by auto
lp15@66289
   941
lp15@66289
   942
lemma between: "between (a, b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
lp15@66289
   943
proof (cases "a = b")
lp15@66289
   944
  case True
lp15@66289
   945
  then show ?thesis
lp15@68056
   946
    by (auto simp add: between_def dist_commute)
lp15@66289
   947
next
lp15@66289
   948
  case False
lp15@66289
   949
  then have Fal: "norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0"
lp15@66289
   950
    by auto
lp15@66289
   951
  have *: "\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)"
lp15@66289
   952
    by (auto simp add: algebra_simps)
lp15@68056
   953
  have "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)" if "x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1" for u
lp15@66289
   954
  proof -
lp15@68056
   955
    have *: "a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
lp15@68056
   956
      unfolding that(1) by (auto simp add:algebra_simps)
lp15@66289
   957
    show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
lp15@68056
   958
      unfolding norm_minus_commute[of x a] * using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>
lp15@66289
   959
      by (auto simp add: field_simps)
lp15@66289
   960
  qed
lp15@68056
   961
  moreover have "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" if "dist a b = dist a x + dist x b" 
lp15@68056
   962
  proof -
lp15@68056
   963
    let ?\<beta> = "norm (a - x) / norm (a - b)"
lp15@68056
   964
    show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1"
lp15@68056
   965
    proof (intro exI conjI)
lp15@68056
   966
      show "?\<beta> \<le> 1"
lp15@68056
   967
        using Fal2 unfolding that[unfolded dist_norm] norm_ge_zero by auto
lp15@68056
   968
      show "x = (1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b"
lp15@68056
   969
      proof (subst euclidean_eq_iff; intro ballI)
lp15@68056
   970
        fix i :: 'a
lp15@68056
   971
        assume i: "i \<in> Basis"
lp15@68056
   972
        have "((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i 
lp15@68056
   973
              = ((norm (a - b) - norm (a - x)) * (a \<bullet> i) + norm (a - x) * (b \<bullet> i)) / norm (a - b)"
lp15@68056
   974
          using Fal by (auto simp add: field_simps inner_simps)
lp15@68056
   975
        also have "\<dots> = x\<bullet>i"
lp15@68056
   976
          apply (rule divide_eq_imp[OF Fal])
lp15@68056
   977
          unfolding that[unfolded dist_norm]
lp15@68056
   978
          using that[unfolded dist_triangle_eq] i
lp15@68056
   979
          apply (subst (asm) euclidean_eq_iff)
lp15@68056
   980
           apply (auto simp add: field_simps inner_simps)
lp15@68056
   981
          done
lp15@68056
   982
        finally show "x \<bullet> i = ((1 - ?\<beta>) *\<^sub>R a + (?\<beta>) *\<^sub>R b) \<bullet> i"
lp15@68056
   983
          by auto
lp15@68056
   984
      qed
lp15@68056
   985
    qed (use Fal2 in auto)
lp15@68056
   986
  qed
lp15@68056
   987
  ultimately show ?thesis
lp15@68056
   988
    by (force simp add: between_def closed_segment_def dist_triangle_eq)
lp15@66289
   989
qed
lp15@66289
   990
lp15@66289
   991
lemma between_midpoint:
lp15@66289
   992
  fixes a :: "'a::euclidean_space"
lp15@66289
   993
  shows "between (a,b) (midpoint a b)" (is ?t1)
lp15@66289
   994
    and "between (b,a) (midpoint a b)" (is ?t2)
lp15@66289
   995
proof -
lp15@66289
   996
  have *: "\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y"
lp15@66289
   997
    by auto
lp15@66289
   998
  show ?t1 ?t2
lp15@66289
   999
    unfolding between midpoint_def dist_norm
lp15@68056
  1000
    by (auto simp add: field_simps inner_simps euclidean_eq_iff[where 'a='a] intro!: *)
lp15@66289
  1001
qed
lp15@66289
  1002
lp15@66289
  1003
lemma between_mem_convex_hull:
lp15@66289
  1004
  "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
lp15@66289
  1005
  unfolding between_mem_segment segment_convex_hull ..
lp15@66289
  1006
lp15@66289
  1007
lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> a=b"
lp15@66289
  1008
  by (auto simp: between_def)
lp15@66289
  1009
lp15@66289
  1010
lemma between_triv1 [simp]: "between (a,b) a"
lp15@66289
  1011
  by (auto simp: between_def)
lp15@66289
  1012
lp15@66289
  1013
lemma between_triv2 [simp]: "between (a,b) b"
lp15@66289
  1014
  by (auto simp: between_def)
lp15@66289
  1015
lp15@66289
  1016
lemma between_commute:
lp15@66289
  1017
   "between (a,b) = between (b,a)"
lp15@66289
  1018
by (auto simp: between_def closed_segment_commute)
lp15@66289
  1019
lp15@66289
  1020
lemma between_antisym:
lp15@66289
  1021
  fixes a :: "'a :: euclidean_space"
lp15@66289
  1022
  shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b"
lp15@66289
  1023
by (auto simp: between dist_commute)
lp15@66289
  1024
lp15@66289
  1025
lemma between_trans:
lp15@66289
  1026
    fixes a :: "'a :: euclidean_space"
lp15@66289
  1027
    shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d"
lp15@66289
  1028
  using dist_triangle2 [of b c d] dist_triangle3 [of b d a]
lp15@66289
  1029
  by (auto simp: between dist_commute)
lp15@66289
  1030
lp15@66289
  1031
lemma between_norm:
lp15@66289
  1032
    fixes a :: "'a :: euclidean_space"
lp15@66289
  1033
    shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)"
lp15@66289
  1034
  by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps)
lp15@66289
  1035
lp15@66289
  1036
lemma between_swap:
lp15@66289
  1037
  fixes A B X Y :: "'a::euclidean_space"
lp15@66289
  1038
  assumes "between (A, B) X"
lp15@66289
  1039
  assumes "between (A, B) Y"
lp15@66289
  1040
  shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X"
lp15@66289
  1041
using assms by (auto simp add: between)
lp15@66289
  1042
lp15@66289
  1043
lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x"
lp15@66289
  1044
  by (auto simp: between_def)
lp15@66289
  1045
lp15@66289
  1046
lemma between_trans_2:
lp15@66289
  1047
  fixes a :: "'a :: euclidean_space"
lp15@66289
  1048
  shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> between (c,d) a"
lp15@66289
  1049
  by (metis between_commute between_swap between_trans)
lp15@66289
  1050
lp15@66289
  1051
lemma between_scaleR_lift [simp]:
lp15@66289
  1052
  fixes v :: "'a::euclidean_space"
lp15@66289
  1053
  shows "between (a *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>R v) \<longleftrightarrow> v = 0 \<or> between (a, b) c"
lp15@66289
  1054
  by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric])
lp15@66289
  1055
lp15@66289
  1056
lemma between_1:
lp15@66289
  1057
  fixes x::real
lp15@66289
  1058
  shows "between (a,b) x \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)"
lp15@66289
  1059
  by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
lp15@66289
  1060
lp15@66289
  1061
immler@67962
  1062
subsection%unimportant \<open>Shrinking towards the interior of a convex set\<close>
lp15@66289
  1063
lp15@66289
  1064
lemma mem_interior_convex_shrink:
lp15@68056
  1065
  fixes S :: "'a::euclidean_space set"
lp15@68056
  1066
  assumes "convex S"
lp15@68056
  1067
    and "c \<in> interior S"
lp15@68056
  1068
    and "x \<in> S"
lp15@66289
  1069
    and "0 < e"
lp15@66289
  1070
    and "e \<le> 1"
lp15@68056
  1071
  shows "x - e *\<^sub>R (x - c) \<in> interior S"
lp15@68056
  1072
proof -
lp15@68056
  1073
  obtain d where "d > 0" and d: "ball c d \<subseteq> S"
lp15@66289
  1074
    using assms(2) unfolding mem_interior by auto
lp15@66289
  1075
  show ?thesis
lp15@66289
  1076
    unfolding mem_interior
lp15@68056
  1077
  proof (intro exI subsetI conjI)
lp15@66289
  1078
    fix y
lp15@68056
  1079
    assume "y \<in> ball (x - e *\<^sub>R (x - c)) (e*d)"
lp15@68056
  1080
    then have as: "dist (x - e *\<^sub>R (x - c)) y < e * d"
lp15@68056
  1081
      by simp
lp15@66289
  1082
    have *: "y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x"
lp15@66289
  1083
      using \<open>e > 0\<close> by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
lp15@66289
  1084
    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)"
lp15@66289
  1085
      unfolding dist_norm
lp15@66289
  1086
      unfolding norm_scaleR[symmetric]
lp15@66289
  1087
      apply (rule arg_cong[where f=norm])
lp15@66289
  1088
      using \<open>e > 0\<close>
lp15@66289
  1089
      by (auto simp add: euclidean_eq_iff[where 'a='a] field_simps inner_simps)
lp15@66289
  1090
    also have "\<dots> = \<bar>1/e\<bar> * norm (x - e *\<^sub>R (x - c) - y)"
lp15@66289
  1091
      by (auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
lp15@66289
  1092
    also have "\<dots> < d"
lp15@66289
  1093
      using as[unfolded dist_norm] and \<open>e > 0\<close>
lp15@66289
  1094
      by (auto simp add:pos_divide_less_eq[OF \<open>e > 0\<close>] mult.commute)
lp15@68056
  1095
    finally show "y \<in> S"
lp15@66289
  1096
      apply (subst *)
lp15@66289
  1097
      apply (rule assms(1)[unfolded convex_alt,rule_format])
lp15@66289
  1098
      apply (rule d[unfolded subset_eq,rule_format])
lp15@66289
  1099
      unfolding mem_ball
lp15@66289
  1100
      using assms(3-5)
lp15@66289
  1101
      apply auto
lp15@66289
  1102
      done
lp15@66289
  1103
  qed (insert \<open>e>0\<close> \<open>d>0\<close>, auto)
lp15@66289
  1104
qed
lp15@66289
  1105
lp15@66289
  1106
lemma mem_interior_closure_convex_shrink:
lp15@68056
  1107
  fixes S :: "'a::euclidean_space set"
lp15@68056
  1108
  assumes "convex S"
lp15@68056
  1109
    and "c \<in> interior S"
lp15@68056
  1110
    and "x \<in> closure S"
lp15@66289
  1111
    and "0 < e"
lp15@66289
  1112
    and "e \<le> 1"
lp15@68056
  1113
  shows "x - e *\<^sub>R (x - c) \<in> interior S"
lp15@68056
  1114
proof -
lp15@68056
  1115
  obtain d where "d > 0" and d: "ball c d \<subseteq> S"
lp15@66289
  1116
    using assms(2) unfolding mem_interior by auto
lp15@68056
  1117
  have "\<exists>y\<in>S. norm (y - x) * (1 - e) < e * d"
lp15@68056
  1118
  proof (cases "x \<in> S")
lp15@66289
  1119
    case True
lp15@66289
  1120
    then show ?thesis
lp15@66289
  1121
      using \<open>e > 0\<close> \<open>d > 0\<close>
lp15@66289
  1122
      apply (rule_tac bexI[where x=x])
lp15@66289
  1123
      apply (auto)
lp15@66289
  1124
      done
lp15@66289
  1125
  next
lp15@66289
  1126
    case False
lp15@68056
  1127
    then have x: "x islimpt S"
lp15@66289
  1128
      using assms(3)[unfolded closure_def] by auto
lp15@66289
  1129
    show ?thesis
lp15@66289
  1130
    proof (cases "e = 1")
lp15@66289
  1131
      case True
lp15@68056
  1132
      obtain y where "y \<in> S" "y \<noteq> x" "dist y x < 1"
lp15@66289
  1133
        using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto
lp15@66289
  1134
      then show ?thesis
lp15@66289
  1135
        apply (rule_tac x=y in bexI)
lp15@66289
  1136
        unfolding True
lp15@66289
  1137
        using \<open>d > 0\<close>
lp15@66289
  1138
        apply auto
lp15@66289
  1139
        done
lp15@66289
  1140
    next
lp15@66289
  1141
      case False
lp15@66289
  1142
      then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
lp15@66289
  1143
        using \<open>e \<le> 1\<close> \<open>e > 0\<close> \<open>d > 0\<close> by auto
lp15@68056
  1144
      then obtain y where "y \<in> S" "y \<noteq> x" "dist y x < e * d / (1 - e)"
lp15@66289
  1145
        using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
lp15@66289
  1146
      then show ?thesis
lp15@66289
  1147
        apply (rule_tac x=y in bexI)
lp15@66289
  1148
        unfolding dist_norm
lp15@66289
  1149
        using pos_less_divide_eq[OF *]
lp15@66289
  1150
        apply auto
lp15@66289
  1151
        done
lp15@66289
  1152
    qed
lp15@66289
  1153
  qed
lp15@68056
  1154
  then obtain y where "y \<in> S" and y: "norm (y - x) * (1 - e) < e * d"
lp15@66289
  1155
    by auto
lp15@66289
  1156
  define z where "z = c + ((1 - e) / e) *\<^sub>R (x - y)"
lp15@66289
  1157
  have *: "x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)"
lp15@66289
  1158
    unfolding z_def using \<open>e > 0\<close>
lp15@66289
  1159
    by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
lp15@68056
  1160
  have "z \<in> interior S"
lp15@66289
  1161
    apply (rule interior_mono[OF d,unfolded subset_eq,rule_format])
lp15@66289
  1162
    unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
lp15@66289
  1163
    apply (auto simp add:field_simps norm_minus_commute)
lp15@66289
  1164
    done
lp15@66289
  1165
  then show ?thesis
lp15@66289
  1166
    unfolding *
lp15@68056
  1167
    using mem_interior_convex_shrink \<open>y \<in> S\<close> assms by blast
lp15@66289
  1168
qed
lp15@66289
  1169
lp15@66289
  1170
lemma in_interior_closure_convex_segment:
lp15@66289
  1171
  fixes S :: "'a::euclidean_space set"
lp15@66289
  1172
  assumes "convex S" and a: "a \<in> interior S" and b: "b \<in> closure S"
lp15@66289
  1173
    shows "open_segment a b \<subseteq> interior S"
lp15@66289
  1174
proof (clarsimp simp: in_segment)
lp15@66289
  1175
  fix u::real
lp15@66289
  1176
  assume u: "0 < u" "u < 1"
lp15@66289
  1177
  have "(1 - u) *\<^sub>R a + u *\<^sub>R b = b - (1 - u) *\<^sub>R (b - a)"
lp15@66289
  1178
    by (simp add: algebra_simps)
lp15@66289
  1179
  also have "... \<in> interior S" using mem_interior_closure_convex_shrink [OF assms] u
lp15@66289
  1180
    by simp
lp15@66289
  1181
  finally show "(1 - u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" .
lp15@66289
  1182
qed
lp15@66289
  1183
lp15@66289
  1184
lemma closure_open_Int_superset:
lp15@66289
  1185
  assumes "open S" "S \<subseteq> closure T"
lp15@66289
  1186
  shows "closure(S \<inter> T) = closure S"
lp15@66289
  1187
proof -
lp15@66289
  1188
  have "closure S \<subseteq> closure(S \<inter> T)"
lp15@66289
  1189
    by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
lp15@66289
  1190
  then show ?thesis
lp15@66289
  1191
    by (simp add: closure_mono dual_order.antisym)
lp15@66289
  1192
qed
lp15@66289
  1193
lp15@66289
  1194
lemma convex_closure_interior:
lp15@66289
  1195
  fixes S :: "'a::euclidean_space set"
lp15@66289
  1196
  assumes "convex S" and int: "interior S \<noteq> {}"
lp15@66289
  1197
  shows "closure(interior S) = closure S"
lp15@66289
  1198
proof -
lp15@66289
  1199
  obtain a where a: "a \<in> interior S"
lp15@66289
  1200
    using int by auto
lp15@66289
  1201
  have "closure S \<subseteq> closure(interior S)"
lp15@66289
  1202
  proof
lp15@66289
  1203
    fix x
lp15@66289
  1204
    assume x: "x \<in> closure S"
lp15@66289
  1205
    show "x \<in> closure (interior S)"
lp15@66289
  1206
    proof (cases "x=a")
lp15@66289
  1207
      case True
lp15@66289
  1208
      then show ?thesis
lp15@66289
  1209
        using \<open>a \<in> interior S\<close> closure_subset by blast
lp15@66289
  1210
    next
lp15@66289
  1211
      case False
lp15@66289
  1212
      show ?thesis
lp15@66289
  1213
      proof (clarsimp simp add: closure_def islimpt_approachable)
lp15@66289
  1214
        fix e::real
lp15@66289
  1215
        assume xnotS: "x \<notin> interior S" and "0 < e"
lp15@66289
  1216
        show "\<exists>x'\<in>interior S. x' \<noteq> x \<and> dist x' x < e"
lp15@66289
  1217
        proof (intro bexI conjI)
lp15@66289
  1218
          show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<noteq> x"
lp15@66289
  1219
            using False \<open>0 < e\<close> by (auto simp: algebra_simps min_def)
lp15@66289
  1220
          show "dist (x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a)) x < e"
lp15@66289
  1221
            using \<open>0 < e\<close> by (auto simp: dist_norm min_def)
lp15@66289
  1222
          show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<in> interior S"
lp15@66289
  1223
            apply (clarsimp simp add: min_def a)
lp15@66289
  1224
            apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x])
lp15@66289
  1225
            using \<open>0 < e\<close> False apply (auto simp: divide_simps)
lp15@66289
  1226
            done
lp15@66289
  1227
        qed
lp15@66289
  1228
      qed
lp15@66289
  1229
    qed
lp15@66289
  1230
  qed
lp15@66289
  1231
  then show ?thesis
lp15@66289
  1232
    by (simp add: closure_mono interior_subset subset_antisym)
lp15@66289
  1233
qed
lp15@66289
  1234
lp15@66289
  1235
lemma closure_convex_Int_superset:
lp15@66289
  1236
  fixes S :: "'a::euclidean_space set"
lp15@66289
  1237
  assumes "convex S" "interior S \<noteq> {}" "interior S \<subseteq> closure T"
lp15@66289
  1238
  shows "closure(S \<inter> T) = closure S"
lp15@66289
  1239
proof -
lp15@66289
  1240
  have "closure S \<subseteq> closure(interior S)"
lp15@66289
  1241
    by (simp add: convex_closure_interior assms)
lp15@66289
  1242
  also have "... \<subseteq> closure (S \<inter> T)"
lp15@66289
  1243
    using interior_subset [of S] assms
lp15@66289
  1244
    by (metis (no_types, lifting) Int_assoc Int_lower2 closure_mono closure_open_Int_superset inf.orderE open_interior)
lp15@66289
  1245
  finally show ?thesis
lp15@66289
  1246
    by (simp add: closure_mono dual_order.antisym)
lp15@66289
  1247
qed
lp15@66289
  1248
lp15@66289
  1249
immler@67962
  1250
subsection%unimportant \<open>Some obvious but surprisingly hard simplex lemmas\<close>
lp15@66289
  1251
lp15@66289
  1252
lemma simplex:
lp15@68056
  1253
  assumes "finite S"
lp15@68056
  1254
    and "0 \<notin> S"
lp15@68056
  1255
  shows "convex hull (insert 0 S) = {y. \<exists>u. (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S \<le> 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y}"
lp15@68056
  1256
proof (simp add: convex_hull_finite set_eq_iff assms, safe)
lp15@68056
  1257
  fix x and u :: "'a \<Rightarrow> real"
lp15@68056
  1258
  assume "0 \<le> u 0" "\<forall>x\<in>S. 0 \<le> u x" "u 0 + sum u S = 1"
lp15@68056
  1259
  then show "\<exists>v. (\<forall>x\<in>S. 0 \<le> v x) \<and> sum v S \<le> 1 \<and> (\<Sum>x\<in>S. v x *\<^sub>R x) = (\<Sum>x\<in>S. u x *\<^sub>R x)"
lp15@68056
  1260
    by force
lp15@68056
  1261
next
lp15@68056
  1262
  fix x and u :: "'a \<Rightarrow> real"
lp15@68056
  1263
  assume "\<forall>x\<in>S. 0 \<le> u x" "sum u S \<le> 1"
lp15@68056
  1264
  then show "\<exists>v. 0 \<le> v 0 \<and> (\<forall>x\<in>S. 0 \<le> v x) \<and> v 0 + sum v S = 1 \<and> (\<Sum>x\<in>S. v x *\<^sub>R x) = (\<Sum>x\<in>S. u x *\<^sub>R x)"
lp15@68056
  1265
    by (rule_tac x="\<lambda>x. if x = 0 then 1 - sum u S else u x" in exI) (auto simp: sum_delta_notmem assms if_smult)
lp15@68056
  1266
qed
lp15@66289
  1267
lp15@66289
  1268
lemma substd_simplex:
lp15@66289
  1269
  assumes d: "d \<subseteq> Basis"
lp15@66289
  1270
  shows "convex hull (insert 0 d) =
lp15@66289
  1271
    {x. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> (\<Sum>i\<in>d. x\<bullet>i) \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)}"
lp15@66289
  1272
  (is "convex hull (insert 0 ?p) = ?s")
lp15@66289
  1273
proof -
lp15@66289
  1274
  let ?D = d
lp15@66289
  1275
  have "0 \<notin> ?p"
lp15@66289
  1276
    using assms by (auto simp: image_def)
lp15@66289
  1277
  from d have "finite d"
lp15@66289
  1278
    by (blast intro: finite_subset finite_Basis)
lp15@66289
  1279
  show ?thesis
lp15@66289
  1280
    unfolding simplex[OF \<open>finite d\<close> \<open>0 \<notin> ?p\<close>]
lp15@68056
  1281
  proof (intro set_eqI; safe)
lp15@68056
  1282
    fix u :: "'a \<Rightarrow> real"
lp15@68056
  1283
    assume as: "\<forall>x\<in>?D. 0 \<le> u x" "sum u ?D \<le> 1" 
lp15@68056
  1284
    let ?x = "(\<Sum>x\<in>?D. u x *\<^sub>R x)"
lp15@68056
  1285
    have ind: "\<forall>i\<in>Basis. i \<in> d \<longrightarrow> u i = ?x \<bullet> i"
lp15@68056
  1286
      and notind: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> ?x \<bullet> i = 0)"
lp15@68056
  1287
      using substdbasis_expansion_unique[OF assms] by blast+
lp15@68056
  1288
    then have **: "sum u ?D = sum ((\<bullet>) ?x) ?D"
lp15@68056
  1289
      using assms by (auto intro!: sum.cong)
lp15@68056
  1290
    show "0 \<le> ?x \<bullet> i" if "i \<in> Basis" for i
lp15@68056
  1291
      using as(1) ind notind that by fastforce
lp15@68056
  1292
    show "sum ((\<bullet>) ?x) ?D \<le> 1"
lp15@68056
  1293
      using "**" as(2) by linarith
lp15@68056
  1294
    show "?x \<bullet> i = 0" if "i \<in> Basis" "i \<notin> d" for i
lp15@68056
  1295
      using notind that by blast
lp15@66289
  1296
  next
lp15@68056
  1297
    fix x 
lp15@68056
  1298
    assume "\<forall>i\<in>Basis. 0 \<le> x \<bullet> i" "sum ((\<bullet>) x) ?D \<le> 1" "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)"
lp15@68056
  1299
    with d show "\<exists>u. (\<forall>x\<in>?D. 0 \<le> u x) \<and> sum u ?D \<le> 1 \<and> (\<Sum>x\<in>?D. u x *\<^sub>R x) = x"
lp15@68056
  1300
      unfolding substdbasis_expansion_unique[OF assms] 
lp15@68056
  1301
      by (rule_tac x="inner x" in exI) auto
lp15@66289
  1302
  qed
lp15@66289
  1303
qed
lp15@66289
  1304
lp15@66289
  1305
lemma std_simplex:
lp15@66289
  1306
  "convex hull (insert 0 Basis) =
lp15@66289
  1307
    {x::'a::euclidean_space. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> sum (\<lambda>i. x\<bullet>i) Basis \<le> 1}"
lp15@66289
  1308
  using substd_simplex[of Basis] by auto
lp15@66289
  1309
lp15@66289
  1310
lemma interior_std_simplex:
lp15@66289
  1311
  "interior (convex hull (insert 0 Basis)) =
lp15@66289
  1312
    {x::'a::euclidean_space. (\<forall>i\<in>Basis. 0 < x\<bullet>i) \<and> sum (\<lambda>i. x\<bullet>i) Basis < 1}"
lp15@68056
  1313
  unfolding set_eq_iff mem_interior std_simplex
lp15@68056
  1314
proof (intro allI iffI CollectI; clarify)
lp15@66289
  1315
  fix x :: 'a
lp15@66289
  1316
  fix e
lp15@68056
  1317
  assume "e > 0" and as: "ball x e \<subseteq> {x. (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i) \<and> sum ((\<bullet>) x) Basis \<le> 1}"
lp15@68056
  1318
  show "(\<forall>i\<in>Basis. 0 < x \<bullet> i) \<and> sum ((\<bullet>) x) Basis < 1"
lp15@68056
  1319
  proof safe
lp15@66289
  1320
    fix i :: 'a
lp15@66289
  1321
    assume i: "i \<in> Basis"
lp15@66289
  1322
    then show "0 < x \<bullet> i"
lp15@68056
  1323
      using as[THEN subsetD[where c="x - (e / 2) *\<^sub>R i"]] and \<open>e > 0\<close> 
lp15@68056
  1324
      by (force simp add: inner_simps)
lp15@66289
  1325
  next
lp15@66289
  1326
    have **: "dist x (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis)) < e" using \<open>e > 0\<close>
lp15@66289
  1327
      unfolding dist_norm
lp15@66289
  1328
      by (auto intro!: mult_strict_left_mono simp: SOME_Basis)
lp15@66289
  1329
    have "\<And>i. i \<in> Basis \<Longrightarrow> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis)) \<bullet> i =
lp15@66289
  1330
      x\<bullet>i + (if i = (SOME i. i\<in>Basis) then e/2 else 0)"
lp15@66289
  1331
      by (auto simp: SOME_Basis inner_Basis inner_simps)
nipkow@67399
  1332
    then have *: "sum ((\<bullet>) (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis =
lp15@66289
  1333
      sum (\<lambda>i. x\<bullet>i + (if (SOME i. i\<in>Basis) = i then e/2 else 0)) Basis"
lp15@68056
  1334
      by (auto simp: intro!: sum.cong)
nipkow@67399
  1335
    have "sum ((\<bullet>) x) Basis < sum ((\<bullet>) (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis"
lp15@68056
  1336
      using \<open>e > 0\<close> DIM_positive by (auto simp: SOME_Basis sum.distrib *)
lp15@66289
  1337
    also have "\<dots> \<le> 1"
lp15@68056
  1338
      using ** as by force
nipkow@67399
  1339
    finally show "sum ((\<bullet>) x) Basis < 1" by auto
lp15@68056
  1340
  qed 
lp15@66289
  1341
next
lp15@66289
  1342
  fix x :: 'a
nipkow@67399
  1343
  assume as: "\<forall>i\<in>Basis. 0 < x \<bullet> i" "sum ((\<bullet>) x) Basis < 1"
lp15@66289
  1344
  obtain a :: 'b where "a \<in> UNIV" using UNIV_witness ..
nipkow@67399
  1345
  let ?d = "(1 - sum ((\<bullet>) x) Basis) / real (DIM('a))"
lp15@68056
  1346
  show "\<exists>e>0. ball x e \<subseteq> {x. (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i) \<and> sum ((\<bullet>) x) Basis \<le> 1}"
lp15@68056
  1347
  proof (rule_tac x="min (Min (((\<bullet>) x) ` Basis)) D" for D in exI, intro conjI subsetI CollectI)
lp15@66289
  1348
    fix y
lp15@68056
  1349
    assume y: "y \<in> ball x (min (Min ((\<bullet>) x ` Basis)) ?d)"
nipkow@67399
  1350
    have "sum ((\<bullet>) y) Basis \<le> sum (\<lambda>i. x\<bullet>i + ?d) Basis"
lp15@66289
  1351
    proof (rule sum_mono)
lp15@66289
  1352
      fix i :: 'a
lp15@66289
  1353
      assume i: "i \<in> Basis"
lp15@68056
  1354
      have "\<bar>y\<bullet>i - x\<bullet>i\<bar> \<le> norm (y - x)"
lp15@68056
  1355
        by (metis Basis_le_norm i inner_commute inner_diff_right)
lp15@68056
  1356
      also have "... < ?d"
lp15@68056
  1357
        using y by (simp add: dist_norm norm_minus_commute)
lp15@68056
  1358
      finally have "\<bar>y\<bullet>i - x\<bullet>i\<bar> < ?d" .
lp15@66289
  1359
      then show "y \<bullet> i \<le> x \<bullet> i + ?d" by auto
lp15@66289
  1360
    qed
lp15@66289
  1361
    also have "\<dots> \<le> 1"
lp15@66289
  1362
      unfolding sum.distrib sum_constant
lp15@66289
  1363
      by (auto simp add: Suc_le_eq)
nipkow@67399
  1364
    finally show "sum ((\<bullet>) y) Basis \<le> 1" .
lp15@66289
  1365
    show "(\<forall>i\<in>Basis. 0 \<le> y \<bullet> i)"
lp15@66289
  1366
    proof safe
lp15@66289
  1367
      fix i :: 'a
lp15@66289
  1368
      assume i: "i \<in> Basis"
haftmann@68796
  1369
      have "norm (x - y) < Min (((\<bullet>) x) ` Basis)"
lp15@68056
  1370
        using y by (auto simp: dist_norm less_eq_real_def)
lp15@68056
  1371
      also have "... \<le> x\<bullet>i"
lp15@68056
  1372
        using i by auto
lp15@68056
  1373
      finally have "norm (x - y) < x\<bullet>i" .
lp15@66289
  1374
      then show "0 \<le> y\<bullet>i"
lp15@66289
  1375
        using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i]
lp15@66289
  1376
        by (auto simp: inner_simps)
lp15@66289
  1377
    qed
lp15@66289
  1378
  next
nipkow@67399
  1379
    have "Min (((\<bullet>) x) ` Basis) > 0"
lp15@66289
  1380
      using as by simp
lp15@66289
  1381
    moreover have "?d > 0"
lp15@66289
  1382
      using as by (auto simp: Suc_le_eq)
nipkow@67399
  1383
    ultimately show "0 < min (Min ((\<bullet>) x ` Basis)) ((1 - sum ((\<bullet>) x) Basis) / real DIM('a))"
lp15@66289
  1384
      by linarith
lp15@66289
  1385
  qed 
lp15@66289
  1386
qed
lp15@66289
  1387
lp15@66289
  1388
lemma interior_std_simplex_nonempty:
lp15@66289
  1389
  obtains a :: "'a::euclidean_space" where
lp15@66289
  1390
    "a \<in> interior(convex hull (insert 0 Basis))"
lp15@66289
  1391
proof -
lp15@66289
  1392
  let ?D = "Basis :: 'a set"
lp15@66289
  1393
  let ?a = "sum (\<lambda>b::'a. inverse (2 * real DIM('a)) *\<^sub>R b) Basis"
lp15@66289
  1394
  {
lp15@66289
  1395
    fix i :: 'a
lp15@66289
  1396
    assume i: "i \<in> Basis"
lp15@66289
  1397
    have "?a \<bullet> i = inverse (2 * real DIM('a))"
lp15@66289
  1398
      by (rule trans[of _ "sum (\<lambda>j. if i = j then inverse (2 * real DIM('a)) else 0) ?D"])
lp15@66289
  1399
         (simp_all add: sum.If_cases i) }
lp15@66289
  1400
  note ** = this
lp15@66289
  1401
  show ?thesis
lp15@66289
  1402
    apply (rule that[of ?a])
lp15@66289
  1403
    unfolding interior_std_simplex mem_Collect_eq
lp15@66289
  1404
  proof safe
lp15@66289
  1405
    fix i :: 'a
lp15@66289
  1406
    assume i: "i \<in> Basis"
lp15@66289
  1407
    show "0 < ?a \<bullet> i"
lp15@66289
  1408
      unfolding **[OF i] by (auto simp add: Suc_le_eq DIM_positive)
lp15@66289
  1409
  next
nipkow@67399
  1410
    have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real DIM('a))) ?D"
lp15@66289
  1411
      apply (rule sum.cong)
lp15@66289
  1412
      apply rule
lp15@66289
  1413
      apply auto
lp15@66289
  1414
      done
lp15@66289
  1415
    also have "\<dots> < 1"
lp15@66289
  1416
      unfolding sum_constant divide_inverse[symmetric]
lp15@66289
  1417
      by (auto simp add: field_simps)
nipkow@67399
  1418
    finally show "sum ((\<bullet>) ?a) ?D < 1" by auto
lp15@66289
  1419
  qed
lp15@66289
  1420
qed
lp15@66289
  1421
lp15@66289
  1422
lemma rel_interior_substd_simplex:
lp15@68056
  1423
  assumes D: "D \<subseteq> Basis"
lp15@68056
  1424
  shows "rel_interior (convex hull (insert 0 D)) =
lp15@68056
  1425
    {x::'a::euclidean_space. (\<forall>i\<in>D. 0 < x\<bullet>i) \<and> (\<Sum>i\<in>D. x\<bullet>i) < 1 \<and> (\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> x\<bullet>i = 0)}"
lp15@66289
  1426
  (is "rel_interior (convex hull (insert 0 ?p)) = ?s")
lp15@66289
  1427
proof -
lp15@68056
  1428
  have "finite D"
lp15@68056
  1429
    using D finite_Basis finite_subset by blast
lp15@66289
  1430
  show ?thesis
lp15@68056
  1431
  proof (cases "D = {}")
lp15@66289
  1432
    case True
lp15@66289
  1433
    then show ?thesis
lp15@66289
  1434
      using rel_interior_sing using euclidean_eq_iff[of _ 0] by auto
lp15@66289
  1435
  next
lp15@66289
  1436
    case False
lp15@66289
  1437
    have h0: "affine hull (convex hull (insert 0 ?p)) =
lp15@68056
  1438
      {x::'a::euclidean_space. (\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> x\<bullet>i = 0)}"
lp15@66289
  1439
      using affine_hull_convex_hull affine_hull_substd_basis assms by auto
lp15@68056
  1440
    have aux: "\<And>x::'a. \<forall>i\<in>Basis. (\<forall>i\<in>D. 0 \<le> x\<bullet>i) \<and> (\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> x\<bullet>i = 0) \<longrightarrow> 0 \<le> x\<bullet>i"
lp15@66289
  1441
      by auto
lp15@66289
  1442
    {
lp15@66289
  1443
      fix x :: "'a::euclidean_space"
lp15@66289
  1444
      assume x: "x \<in> rel_interior (convex hull (insert 0 ?p))"
lp15@68056
  1445
      then obtain e where "e > 0" and
lp15@68056
  1446
        "ball x e \<inter> {xa. (\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> xa\<bullet>i = 0)} \<subseteq> convex hull (insert 0 ?p)"
lp15@66289
  1447
        using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto
lp15@68056
  1448
      then have as [rule_format]: "\<And>y. dist x y < e \<and> (\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> y\<bullet>i = 0) \<longrightarrow>
lp15@68056
  1449
        (\<forall>i\<in>D. 0 \<le> y \<bullet> i) \<and> sum ((\<bullet>) y) D \<le> 1"
lp15@66289
  1450
        unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto
lp15@68056
  1451
      have x0: "(\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> x\<bullet>i = 0)"
lp15@66289
  1452
        using x rel_interior_subset  substd_simplex[OF assms] by auto
lp15@68056
  1453
      have "(\<forall>i\<in>D. 0 < x \<bullet> i) \<and> sum ((\<bullet>) x) D < 1 \<and> (\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> x\<bullet>i = 0)"
lp15@68056
  1454
      proof (intro conjI ballI)
lp15@66289
  1455
        fix i :: 'a
lp15@68056
  1456
        assume "i \<in> D"
lp15@68056
  1457
        then have "\<forall>j\<in>D. 0 \<le> (x - (e / 2) *\<^sub>R i) \<bullet> j"
lp15@66289
  1458
          apply -
lp15@68056
  1459
          apply (rule as[THEN conjunct1])
lp15@68056
  1460
          using D \<open>e > 0\<close> x0
lp15@68056
  1461
          apply (auto simp: dist_norm inner_simps inner_Basis)
lp15@66289
  1462
          done
lp15@66289
  1463
        then show "0 < x \<bullet> i"
lp15@68056
  1464
          using \<open>e > 0\<close> \<open>i \<in> D\<close> D  by (force simp: inner_simps inner_Basis)
lp15@66289
  1465
      next
lp15@68056
  1466
        obtain a where a: "a \<in> D"
lp15@68056
  1467
          using \<open>D \<noteq> {}\<close> by auto
lp15@66289
  1468
        then have **: "dist x (x + (e / 2) *\<^sub>R a) < e"
lp15@68056
  1469
          using \<open>e > 0\<close> norm_Basis[of a] D
lp15@66289
  1470
          unfolding dist_norm
lp15@66289
  1471
          by auto
lp15@66289
  1472
        have "\<And>i. i \<in> Basis \<Longrightarrow> (x + (e / 2) *\<^sub>R a) \<bullet> i = x\<bullet>i + (if i = a then e/2 else 0)"
lp15@68056
  1473
          using a D by (auto simp: inner_simps inner_Basis)
lp15@68056
  1474
        then have *: "sum ((\<bullet>) (x + (e / 2) *\<^sub>R a)) D =
lp15@68056
  1475
          sum (\<lambda>i. x\<bullet>i + (if a = i then e/2 else 0)) D"
lp15@68056
  1476
          using D by (intro sum.cong) auto
lp15@66289
  1477
        have "a \<in> Basis"
lp15@68056
  1478
          using \<open>a \<in> D\<close> D by auto
lp15@68056
  1479
        then have h1: "(\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> (x + (e / 2) *\<^sub>R a) \<bullet> i = 0)"
lp15@68056
  1480
          using x0 D \<open>a\<in>D\<close> by (auto simp add: inner_add_left inner_Basis)
lp15@68056
  1481
        have "sum ((\<bullet>) x) D < sum ((\<bullet>) (x + (e / 2) *\<^sub>R a)) D"
lp15@68056
  1482
          using \<open>e > 0\<close> \<open>a \<in> D\<close> \<open>finite D\<close> by (auto simp add: * sum.distrib)
lp15@66289
  1483
        also have "\<dots> \<le> 1"
lp15@66289
  1484
          using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R a"]
lp15@66289
  1485
          by auto
lp15@68056
  1486
        finally show "sum ((\<bullet>) x) D < 1" "\<And>i. i\<in>Basis \<Longrightarrow> i \<notin> D \<longrightarrow> x\<bullet>i = 0"
lp15@66289
  1487
          using x0 by auto
lp15@66289
  1488
      qed
lp15@66289
  1489
    }
lp15@66289
  1490
    moreover
lp15@66289
  1491
    {
lp15@66289
  1492
      fix x :: "'a::euclidean_space"
lp15@66289
  1493
      assume as: "x \<in> ?s"
lp15@66289
  1494
      have "\<forall>i. 0 < x\<bullet>i \<or> 0 = x\<bullet>i \<longrightarrow> 0 \<le> x\<bullet>i"
lp15@66289
  1495
        by auto
lp15@68056
  1496
      moreover have "\<forall>i. i \<in> D \<or> i \<notin> D" by auto
lp15@66289
  1497
      ultimately
lp15@68056
  1498
      have "\<forall>i. (\<forall>i\<in>D. 0 < x\<bullet>i) \<and> (\<forall>i. i \<notin> D \<longrightarrow> x\<bullet>i = 0) \<longrightarrow> 0 \<le> x\<bullet>i"
lp15@66289
  1499
        by metis
lp15@66289
  1500
      then have h2: "x \<in> convex hull (insert 0 ?p)"
lp15@66289
  1501
        using as assms
lp15@66289
  1502
        unfolding substd_simplex[OF assms] by fastforce
lp15@68056
  1503
      obtain a where a: "a \<in> D"
lp15@68056
  1504
        using \<open>D \<noteq> {}\<close> by auto
lp15@68056
  1505
      let ?d = "(1 - sum ((\<bullet>) x) D) / real (card D)"
lp15@68056
  1506
      have "0 < card D" using \<open>D \<noteq> {}\<close> \<open>finite D\<close>
lp15@66289
  1507
        by (simp add: card_gt_0_iff)
lp15@68056
  1508
      have "Min (((\<bullet>) x) ` D) > 0"
lp15@68056
  1509
        using as \<open>D \<noteq> {}\<close> \<open>finite D\<close> by (simp add: Min_gr_iff)
lp15@68056
  1510
      moreover have "?d > 0" using as using \<open>0 < card D\<close> by auto
lp15@68056
  1511
      ultimately have h3: "min (Min (((\<bullet>) x) ` D)) ?d > 0"
lp15@66289
  1512
        by auto
lp15@66289
  1513
lp15@66289
  1514
      have "x \<in> rel_interior (convex hull (insert 0 ?p))"
lp15@66289
  1515
        unfolding rel_interior_ball mem_Collect_eq h0
lp15@66289
  1516
        apply (rule,rule h2)
lp15@66289
  1517
        unfolding substd_simplex[OF assms]
lp15@68056
  1518
        apply (rule_tac x="min (Min (((\<bullet>) x) ` D)) ?d" in exI)
lp15@66289
  1519
        apply (rule, rule h3)
lp15@66289
  1520
        apply safe
lp15@66289
  1521
        unfolding mem_ball
lp15@66289
  1522
      proof -
lp15@66289
  1523
        fix y :: 'a
lp15@68056
  1524
        assume y: "dist x y < min (Min ((\<bullet>) x ` D)) ?d"
lp15@68056
  1525
        assume y2: "\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> y\<bullet>i = 0"
lp15@68056
  1526
        have "sum ((\<bullet>) y) D \<le> sum (\<lambda>i. x\<bullet>i + ?d) D"
lp15@66289
  1527
        proof (rule sum_mono)
lp15@66289
  1528
          fix i
lp15@68056
  1529
          assume "i \<in> D"
lp15@68056
  1530
          with D have i: "i \<in> Basis"
lp15@66289
  1531
            by auto
lp15@68056
  1532
          have "\<bar>y\<bullet>i - x\<bullet>i\<bar> \<le> norm (y - x)"
lp15@68056
  1533
            by (metis i inner_commute inner_diff_right norm_bound_Basis_le order_refl)
lp15@68056
  1534
          also have "... < ?d"
lp15@68056
  1535
            by (metis dist_norm min_less_iff_conj norm_minus_commute y)
lp15@68056
  1536
          finally have "\<bar>y\<bullet>i - x\<bullet>i\<bar> < ?d" .
lp15@66289
  1537
          then show "y \<bullet> i \<le> x \<bullet> i + ?d" by auto
lp15@66289
  1538
        qed
lp15@66289
  1539
        also have "\<dots> \<le> 1"
lp15@68056
  1540
          unfolding sum.distrib sum_constant  using \<open>0 < card D\<close>
lp15@66289
  1541
          by auto
lp15@68056
  1542
        finally show "sum ((\<bullet>) y) D \<le> 1" .
lp15@66289
  1543
lp15@66289
  1544
        fix i :: 'a
lp15@66289
  1545
        assume i: "i \<in> Basis"
lp15@66289
  1546
        then show "0 \<le> y\<bullet>i"
lp15@68056
  1547
        proof (cases "i\<in>D")
lp15@66289
  1548
          case True
lp15@66289
  1549
          have "norm (x - y) < x\<bullet>i"
lp15@66289
  1550
            using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
lp15@68056
  1551
            using Min_gr_iff[of "(\<bullet>) x ` D" "norm (x - y)"] \<open>0 < card D\<close> \<open>i \<in> D\<close>
lp15@66289
  1552
            by (simp add: card_gt_0_iff)
lp15@66289
  1553
          then show "0 \<le> y\<bullet>i"
lp15@66289
  1554
            using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format]
lp15@66289
  1555
            by (auto simp: inner_simps)
lp15@66289
  1556
        qed (insert y2, auto)
lp15@66289
  1557
      qed
lp15@66289
  1558
    }
lp15@66289
  1559
    ultimately have
lp15@68056
  1560
      "\<And>x. x \<in> rel_interior (convex hull insert 0 D) \<longleftrightarrow>
lp15@68056
  1561
        x \<in> {x. (\<forall>i\<in>D. 0 < x \<bullet> i) \<and> sum ((\<bullet>) x) D < 1 \<and> (\<forall>i\<in>Basis. i \<notin> D \<longrightarrow> x \<bullet> i = 0)}"
lp15@66289
  1562
      by blast
lp15@66289
  1563
    then show ?thesis by (rule set_eqI)
lp15@66289
  1564
  qed
lp15@66289
  1565
qed
lp15@66289
  1566
lp15@66289
  1567
lemma rel_interior_substd_simplex_nonempty:
lp15@68056
  1568
  assumes "D \<noteq> {}"
lp15@68056
  1569
    and "D \<subseteq> Basis"
lp15@66289
  1570
  obtains a :: "'a::euclidean_space"
lp15@68056
  1571
    where "a \<in> rel_interior (convex hull (insert 0 D))"
lp15@68056
  1572
proof -
lp15@68056
  1573
  let ?D = D
lp15@68056
  1574
  let ?a = "sum (\<lambda>b::'a::euclidean_space. inverse (2 * real (card D)) *\<^sub>R b) ?D"
lp15@68056
  1575
  have "finite D"
lp15@66289
  1576
    apply (rule finite_subset)
lp15@66289
  1577
    using assms(2)
lp15@66289
  1578
    apply auto
lp15@66289
  1579
    done
lp15@68056
  1580
  then have d1: "0 < real (card D)"
lp15@68056
  1581
    using \<open>D \<noteq> {}\<close> by auto
lp15@66289
  1582
  {
lp15@66289
  1583
    fix i
lp15@68056
  1584
    assume "i \<in> D"
lp15@68056
  1585
    have "?a \<bullet> i = inverse (2 * real (card D))"
lp15@68056
  1586
      apply (rule trans[of _ "sum (\<lambda>j. if i = j then inverse (2 * real (card D)) else 0) ?D"])
lp15@66289
  1587
      unfolding inner_sum_left
lp15@66289
  1588
      apply (rule sum.cong)
lp15@68056
  1589
      using \<open>i \<in> D\<close> \<open>finite D\<close> sum.delta'[of D i "(\<lambda>k. inverse (2 * real (card D)))"]
lp15@66289
  1590
        d1 assms(2)
lp15@69712
  1591
      by (auto simp: inner_Basis rev_subsetD[OF _ assms(2)])
lp15@66289
  1592
  }
lp15@66289
  1593
  note ** = this
lp15@66289
  1594
  show ?thesis
lp15@66289
  1595
    apply (rule that[of ?a])
lp15@66289
  1596
    unfolding rel_interior_substd_simplex[OF assms(2)] mem_Collect_eq
lp15@66289
  1597
  proof safe
lp15@66289
  1598
    fix i
lp15@68056
  1599
    assume "i \<in> D"
lp15@68056
  1600
    have "0 < inverse (2 * real (card D))"
lp15@66289
  1601
      using d1 by auto
lp15@68056
  1602
    also have "\<dots> = ?a \<bullet> i" using **[of i] \<open>i \<in> D\<close>
lp15@66289
  1603
      by auto
lp15@66289
  1604
    finally show "0 < ?a \<bullet> i" by auto
lp15@66289
  1605
  next
lp15@68056
  1606
    have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real (card D))) ?D"
lp15@66289
  1607
      by (rule sum.cong) (rule refl, rule **)
lp15@66289
  1608
    also have "\<dots> < 1"
lp15@66289
  1609
      unfolding sum_constant divide_real_def[symmetric]
lp15@66289
  1610
      by (auto simp add: field_simps)
nipkow@67399
  1611
    finally show "sum ((\<bullet>) ?a) ?D < 1" by auto
lp15@66289
  1612
  next
lp15@66289
  1613
    fix i
lp15@68056
  1614
    assume "i \<in> Basis" and "i \<notin> D"
lp15@68056
  1615
    have "?a \<in> span D"
lp15@68056
  1616
    proof (rule span_sum[of D "(\<lambda>b. b /\<^sub>R (2 * real (card D)))" D])
lp15@66289
  1617
      {
lp15@66289
  1618
        fix x :: "'a::euclidean_space"
lp15@68056
  1619
        assume "x \<in> D"
lp15@68056
  1620
        then have "x \<in> span D"
immler@68074
  1621
          using span_base[of _ "D"] by auto
lp15@68056
  1622
        then have "x /\<^sub>R (2 * real (card D)) \<in> span D"
lp15@68056
  1623
          using span_mul[of x "D" "(inverse (real (card D)) / 2)"] by auto
lp15@66289
  1624
      }
lp15@68056
  1625
      then show "\<And>x. x\<in>D \<Longrightarrow> x /\<^sub>R (2 * real (card D)) \<in> span D"
lp15@66289
  1626
        by auto
lp15@66289
  1627
    qed
lp15@66289
  1628
    then show "?a \<bullet> i = 0 "
lp15@68056
  1629
      using \<open>i \<notin> D\<close> unfolding span_substd_basis[OF assms(2)] using \<open>i \<in> Basis\<close> by auto
lp15@66289
  1630
  qed
lp15@66289
  1631
qed
lp15@66289
  1632
lp15@66289
  1633
immler@67962
  1634
subsection%unimportant \<open>Relative interior of convex set\<close>
lp15@66289
  1635
lp15@66289
  1636
lemma rel_interior_convex_nonempty_aux:
lp15@66289
  1637
  fixes S :: "'n::euclidean_space set"
lp15@66289
  1638
  assumes "convex S"
lp15@66289
  1639
    and "0 \<in> S"
lp15@66289
  1640
  shows "rel_interior S \<noteq> {}"
lp15@66289
  1641
proof (cases "S = {0}")
lp15@66289
  1642
  case True
lp15@66289
  1643
  then show ?thesis using rel_interior_sing by auto
lp15@66289
  1644
next
lp15@66289
  1645
  case False
lp15@66289
  1646
  obtain B where B: "independent B \<and> B \<le> S \<and> S \<le> span B \<and> card B = dim S"
lp15@68069
  1647
    using basis_exists[of S] by metis
lp15@66289
  1648
  then have "B \<noteq> {}"
lp15@66289
  1649
    using B assms \<open>S \<noteq> {0}\<close> span_empty by auto
lp15@66289
  1650
  have "insert 0 B \<le> span B"
immler@68072
  1651
    using subspace_span[of B] subspace_0[of "span B"]
immler@68072
  1652
      span_superset by auto
lp15@66289
  1653
  then have "span (insert 0 B) \<le> span B"
lp15@66289
  1654
    using span_span[of B] span_mono[of "insert 0 B" "span B"] by blast
lp15@66289
  1655
  then have "convex hull insert 0 B \<le> span B"
lp15@66289
  1656
    using convex_hull_subset_span[of "insert 0 B"] by auto
lp15@66289
  1657
  then have "span (convex hull insert 0 B) \<le> span B"
immler@68072
  1658
    using span_span[of B]
immler@68072
  1659
      span_mono[of "convex hull insert 0 B" "span B"] by blast
lp15@66289
  1660
  then have *: "span (convex hull insert 0 B) = span B"
lp15@66289
  1661
    using span_mono[of B "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
lp15@66289
  1662
  then have "span (convex hull insert 0 B) = span S"
immler@68072
  1663
    using B span_mono[of B S] span_mono[of S "span B"]
immler@68072
  1664
      span_span[of B] by auto
lp15@66289
  1665
  moreover have "0 \<in> affine hull (convex hull insert 0 B)"
lp15@66289
  1666
    using hull_subset[of "convex hull insert 0 B"] hull_subset[of "insert 0 B"] by auto
lp15@66289
  1667
  ultimately have **: "affine hull (convex hull insert 0 B) = affine hull S"
lp15@66289
  1668
    using affine_hull_span_0[of "convex hull insert 0 B"] affine_hull_span_0[of "S"]
lp15@66289
  1669
      assms hull_subset[of S]
lp15@66289
  1670
    by auto
lp15@66289
  1671
  obtain d and f :: "'n \<Rightarrow> 'n" where
lp15@66289
  1672
    fd: "card d = card B" "linear f" "f ` B = d"
lp15@66289
  1673
      "f ` span B = {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = (0::real)} \<and> inj_on f (span B)"
lp15@66289
  1674
    and d: "d \<subseteq> Basis"
lp15@66289
  1675
    using basis_to_substdbasis_subspace_isomorphism[of B,OF _ ] B by auto
lp15@66289
  1676
  then have "bounded_linear f"
lp15@66289
  1677
    using linear_conv_bounded_linear by auto
lp15@66289
  1678
  have "d \<noteq> {}"
lp15@66289
  1679
    using fd B \<open>B \<noteq> {}\<close> by auto
lp15@66289
  1680
  have "insert 0 d = f ` (insert 0 B)"
lp15@66289
  1681
    using fd linear_0 by auto
lp15@66289
  1682
  then have "(convex hull (insert 0 d)) = f ` (convex hull (insert 0 B))"
lp15@66289
  1683
    using convex_hull_linear_image[of f "(insert 0 d)"]
lp15@66289
  1684
      convex_hull_linear_image[of f "(insert 0 B)"] \<open>linear f\<close>
lp15@66289
  1685
    by auto
lp15@66289
  1686
  moreover have "rel_interior (f ` (convex hull insert 0 B)) =
lp15@66289
  1687
    f ` rel_interior (convex hull insert 0 B)"
lp15@66289
  1688
    apply (rule  rel_interior_injective_on_span_linear_image[of f "(convex hull insert 0 B)"])
lp15@66289
  1689
    using \<open>bounded_linear f\<close> fd *
lp15@66289
  1690
    apply auto
lp15@66289
  1691
    done
lp15@66289
  1692
  ultimately have "rel_interior (convex hull insert 0 B) \<noteq> {}"
lp15@66289
  1693
    using rel_interior_substd_simplex_nonempty[OF \<open>d \<noteq> {}\<close> d]
lp15@66289
  1694
    apply auto
lp15@66289
  1695
    apply blast
lp15@66289
  1696
    done
lp15@66289
  1697
  moreover have "convex hull (insert 0 B) \<subseteq> S"
lp15@66289
  1698
    using B assms hull_mono[of "insert 0 B" "S" "convex"] convex_hull_eq
lp15@66289
  1699
    by auto
lp15@66289
  1700
  ultimately show ?thesis
lp15@66289
  1701
    using subset_rel_interior[of "convex hull insert 0 B" S] ** by auto
lp15@66289
  1702
qed
lp15@66289
  1703
lp15@66289
  1704
lemma rel_interior_eq_empty:
lp15@66289
  1705
  fixes S :: "'n::euclidean_space set"
lp15@66289
  1706
  assumes "convex S"
lp15@66289
  1707
  shows "rel_interior S = {} \<longleftrightarrow> S = {}"
lp15@66289
  1708
proof -
lp15@66289
  1709
  {
lp15@66289
  1710
    assume "S \<noteq> {}"
lp15@66289
  1711
    then obtain a where "a \<in> S" by auto
nipkow@67399
  1712
    then have "0 \<in> (+) (-a) ` S"
lp15@66289
  1713
      using assms exI[of "(\<lambda>x. x \<in> S \<and> - a + x = 0)" a] by auto
nipkow@67399
  1714
    then have "rel_interior ((+) (-a) ` S) \<noteq> {}"
nipkow@67399
  1715
      using rel_interior_convex_nonempty_aux[of "(+) (-a) ` S"]
lp15@66289
  1716
        convex_translation[of S "-a"] assms
lp15@66289
  1717
      by auto
lp15@66289
  1718
    then have "rel_interior S \<noteq> {}"
haftmann@69661
  1719
      using rel_interior_translation [of "- a"] by simp
lp15@66289
  1720
  }
lp15@66289
  1721
  then show ?thesis
lp15@66289
  1722
    using rel_interior_empty by auto
lp15@66289
  1723
qed
lp15@66289
  1724
lp15@66289
  1725
lemma interior_simplex_nonempty:
lp15@66289
  1726
  fixes S :: "'N :: euclidean_space set"
lp15@66289
  1727
  assumes "independent S" "finite S" "card S = DIM('N)"
lp15@66289
  1728
  obtains a where "a \<in> interior (convex hull (insert 0 S))"
lp15@66289
  1729
proof -
lp15@66289
  1730
  have "affine hull (insert 0 S) = UNIV"
immler@68072
  1731
    by (simp add: hull_inc affine_hull_span_0 dim_eq_full[symmetric]
immler@68072
  1732
         assms(1) assms(3) dim_eq_card_independent)
lp15@66289
  1733
  moreover have "rel_interior (convex hull insert 0 S) \<noteq> {}"
lp15@66289
  1734
    using rel_interior_eq_empty [of "convex hull (insert 0 S)"] by auto
lp15@66289
  1735
  ultimately have "interior (convex hull insert 0 S) \<noteq> {}"
lp15@66289
  1736
    by (simp add: rel_interior_interior)
lp15@66289
  1737
  with that show ?thesis
lp15@66289
  1738
    by auto
lp15@66289
  1739
qed
lp15@66289
  1740
lp15@66289
  1741
lemma convex_rel_interior:
lp15@66289
  1742
  fixes S :: "'n::euclidean_space set"
lp15@66289
  1743
  assumes "convex S"
lp15@66289
  1744
  shows "convex (rel_interior S)"
lp15@66289
  1745
proof -
lp15@66289
  1746
  {
lp15@66289
  1747
    fix x y and u :: real
lp15@66289
  1748
    assume assm: "x \<in> rel_interior S" "y \<in> rel_interior S" "0 \<le> u" "u \<le> 1"
lp15@66289
  1749
    then have "x \<in> S"
lp15@66289
  1750
      using rel_interior_subset by auto
lp15@66289
  1751
    have "x - u *\<^sub>R (x-y) \<in> rel_interior S"
lp15@66289
  1752
    proof (cases "0 = u")
lp15@66289
  1753
      case False
lp15@66289
  1754
      then have "0 < u" using assm by auto
lp15@66289
  1755
      then show ?thesis
lp15@66289
  1756
        using assm rel_interior_convex_shrink[of S y x u] assms \<open>x \<in> S\<close> by auto
lp15@66289
  1757
    next
lp15@66289
  1758
      case True
lp15@66289
  1759
      then show ?thesis using assm by auto
lp15@66289
  1760
    qed
lp15@66289
  1761
    then have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> rel_interior S"
lp15@66289
  1762
      by (simp add: algebra_simps)
lp15@66289
  1763
  }
lp15@66289
  1764
  then show ?thesis
lp15@66289
  1765
    unfolding convex_alt by auto
lp15@66289
  1766
qed
lp15@66289
  1767
lp15@66289
  1768
lemma convex_closure_rel_interior:
lp15@66289
  1769
  fixes S :: "'n::euclidean_space set"
lp15@66289
  1770
  assumes "convex S"
lp15@66289
  1771
  shows "closure (rel_interior S) = closure S"
lp15@66289
  1772
proof -
lp15@66289
  1773
  have h1: "closure (rel_interior S) \<le> closure S"
lp15@66289
  1774
    using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
lp15@66289
  1775
  show ?thesis
lp15@66289
  1776
  proof (cases "S = {}")
lp15@66289
  1777
    case False
lp15@66289
  1778
    then obtain a where a: "a \<in> rel_interior S"
lp15@66289
  1779
      using rel_interior_eq_empty assms by auto
lp15@66289
  1780
    { fix x
lp15@66289
  1781
      assume x: "x \<in> closure S"
lp15@66289
  1782
      {
lp15@66289
  1783
        assume "x = a"
lp15@66289
  1784
        then have "x \<in> closure (rel_interior S)"
lp15@66289
  1785
          using a unfolding closure_def by auto
lp15@66289
  1786
      }
lp15@66289
  1787
      moreover
lp15@66289
  1788
      {
lp15@66289
  1789
        assume "x \<noteq> a"
lp15@66289
  1790
         {
lp15@66289
  1791
           fix e :: real
lp15@66289
  1792
           assume "e > 0"
lp15@66289
  1793
           define e1 where "e1 = min 1 (e/norm (x - a))"
lp15@66289
  1794
           then have e1: "e1 > 0" "e1 \<le> 1" "e1 * norm (x - a) \<le> e"
lp15@66289
  1795
             using \<open>x \<noteq> a\<close> \<open>e > 0\<close> le_divide_eq[of e1 e "norm (x - a)"]
lp15@66289
  1796
             by simp_all
wenzelm@67613
  1797
           then have *: "x - e1 *\<^sub>R (x - a) \<in> rel_interior S"
lp15@66289
  1798
             using rel_interior_closure_convex_shrink[of S a x e1] assms x a e1_def
lp15@66289
  1799
             by auto
lp15@66289
  1800
           have "\<exists>y. y \<in> rel_interior S \<and> y \<noteq> x \<and> dist y x \<le> e"
lp15@66289
  1801
              apply (rule_tac x="x - e1 *\<^sub>R (x - a)" in exI)
lp15@66289
  1802
              using * e1 dist_norm[of "x - e1 *\<^sub>R (x - a)" x] \<open>x \<noteq> a\<close>
lp15@66289
  1803
              apply simp
lp15@66289
  1804
              done
lp15@66289
  1805
        }
lp15@66289
  1806
        then have "x islimpt rel_interior S"
lp15@66289
  1807
          unfolding islimpt_approachable_le by auto
lp15@66289
  1808
        then have "x \<in> closure(rel_interior S)"
lp15@66289
  1809
          unfolding closure_def by auto
lp15@66289
  1810
      }
lp15@66289
  1811
      ultimately have "x \<in> closure(rel_interior S)" by auto
lp15@66289
  1812
    }
lp15@66289
  1813
    then show ?thesis using h1 by auto
lp15@66289
  1814
  next
lp15@66289
  1815
    case True
lp15@66289
  1816
    then have "rel_interior S = {}"
lp15@66289
  1817
      using rel_interior_empty by auto
lp15@66289
  1818
    then have "closure (rel_interior S) = {}"
lp15@66289
  1819
      using closure_empty by auto
lp15@66289
  1820
    with True show ?thesis by auto
lp15@66289
  1821
  qed
lp15@66289
  1822
qed
lp15@66289
  1823
lp15@66289
  1824
lemma rel_interior_same_affine_hull:
lp15@66289
  1825
  fixes S :: "'n::euclidean_space set"
lp15@66289
  1826
  assumes "convex S"
lp15@66289
  1827
  shows "affine hull (rel_interior S) = affine hull S"
lp15@66289
  1828
  by (metis assms closure_same_affine_hull convex_closure_rel_interior)
lp15@66289
  1829
lp15@66289
  1830
lemma rel_interior_aff_dim:
lp15@66289
  1831
  fixes S :: "'n::euclidean_space set"
lp15@66289
  1832
  assumes "convex S"
lp15@66289
  1833
  shows "aff_dim (rel_interior S) = aff_dim S"
lp15@66289
  1834
  by (metis aff_dim_affine_hull2 assms rel_interior_same_affine_hull)
lp15@66289
  1835
lp15@66289
  1836
lemma rel_interior_rel_interior:
lp15@66289
  1837
  fixes S :: "'n::euclidean_space set"
lp15@66289
  1838
  assumes "convex S"
lp15@66289
  1839
  shows "rel_interior (rel_interior S) = rel_interior S"
lp15@66289
  1840
proof -
lp15@69922
  1841
  have "openin (top_of_set (affine hull (rel_interior S))) (rel_interior S)"
lp15@66289
  1842
    using openin_rel_interior[of S] rel_interior_same_affine_hull[of S] assms by auto
lp15@66289
  1843
  then show ?thesis
lp15@66289
  1844
    using rel_interior_def by auto
lp15@66289
  1845
qed
lp15@66289
  1846
lp15@66289
  1847
lemma rel_interior_rel_open:
lp15@66289
  1848
  fixes S :: "'n::euclidean_space set"
lp15@66289
  1849
  assumes "convex S"
lp15@66289
  1850
  shows "rel_open (rel_interior S)"
lp15@66289
  1851
  unfolding rel_open_def using rel_interior_rel_interior assms by auto
lp15@66289
  1852
lp15@66289
  1853
lemma convex_rel_interior_closure_aux:
lp15@66289
  1854
  fixes x y z :: "'n::euclidean_space"
lp15@66289
  1855
  assumes "0 < a" "0 < b" "(a + b) *\<^sub>R z = a *\<^sub>R x + b *\<^sub>R y"
lp15@66289
  1856
  obtains e where "0 < e" "e \<le> 1" "z = y - e *\<^sub>R (y - x)"
lp15@66289
  1857
proof -
lp15@66289
  1858
  define e where "e = a / (a + b)"
lp15@66289
  1859
  have "z = (1 / (a + b)) *\<^sub>R ((a + b) *\<^sub>R z)"
lp15@68056
  1860
    using assms  by (simp add: eq_vector_fraction_iff)
lp15@66289
  1861
  also have "\<dots> = (1 / (a + b)) *\<^sub>R (a *\<^sub>R x + b *\<^sub>R y)"
lp15@66289
  1862
    using assms scaleR_cancel_left[of "1/(a+b)" "(a + b) *\<^sub>R z" "a *\<^sub>R x + b *\<^sub>R y"]
lp15@66289
  1863
    by auto
lp15@66289
  1864
  also have "\<dots> = y - e *\<^sub>R (y-x)"
lp15@66289
  1865
    using e_def
lp15@66289
  1866
    apply (simp add: algebra_simps)
lp15@66289
  1867
    using scaleR_left_distrib[of "a/(a+b)" "b/(a+b)" y] assms add_divide_distrib[of a b "a+b"]
lp15@66289
  1868
    apply auto
lp15@66289
  1869
    done
lp15@66289
  1870
  finally have "z = y - e *\<^sub>R (y-x)"
lp15@66289
  1871
    by auto
lp15@66289
  1872
  moreover have "e > 0" using e_def assms by auto
lp15@66289
  1873
  moreover have "e \<le> 1" using e_def assms by auto
lp15@66289
  1874
  ultimately show ?thesis using that[of e] by auto
lp15@66289
  1875
qed
lp15@66289
  1876
lp15@66289
  1877
lemma convex_rel_interior_closure:
lp15@66289
  1878
  fixes S :: "'n::euclidean_space set"
lp15@66289
  1879
  assumes "convex S"
lp15@66289
  1880
  shows "rel_interior (closure S) = rel_interior S"
lp15@66289
  1881
proof (cases "S = {}")
lp15@66289
  1882
  case True
lp15@66289
  1883
  then show ?thesis
lp15@66289
  1884
    using assms rel_interior_eq_empty by auto
lp15@66289
  1885
next
lp15@66289
  1886
  case False
lp15@66289
  1887
  have "rel_interior (closure S) \<supseteq> rel_interior S"
lp15@66289
  1888
    using subset_rel_interior[of S "closure S"] closure_same_affine_hull closure_subset
lp15@66289
  1889
    by auto
lp15@66289
  1890
  moreover
lp15@66289
  1891
  {
lp15@66289
  1892
    fix z
lp15@66289
  1893
    assume z: "z \<in> rel_interior (closure S)"
lp15@66289
  1894
    obtain x where x: "x \<in> rel_interior S"
lp15@66289
  1895
      using \<open>S \<noteq> {}\<close> assms rel_interior_eq_empty by auto
lp15@66289
  1896
    have "z \<in> rel_interior S"
lp15@66289
  1897
    proof (cases "x = z")
lp15@66289
  1898
      case True
lp15@66289
  1899
      then show ?thesis using x by auto
lp15@66289
  1900
    next
lp15@66289
  1901
      case False
lp15@66289
  1902
      obtain e where e: "e > 0" "cball z e \<inter> affine hull closure S \<le> closure S"
lp15@66289
  1903
        using z rel_interior_cball[of "closure S"] by auto
lp15@66289
  1904
      hence *: "0 < e/norm(z-x)" using e False by auto
lp15@66289
  1905
      define y where "y = z + (e/norm(z-x)) *\<^sub>R (z-x)"
lp15@66289
  1906
      have yball: "y \<in> cball z e"
lp15@66289
  1907
        using mem_cball y_def dist_norm[of z y] e by auto
lp15@66289
  1908
      have "x \<in> affine hull closure S"
lp15@66289
  1909
        using x rel_interior_subset_closure hull_inc[of x "closure S"] by blast
lp15@66289
  1910
      moreover have "z \<in> affine hull closure S"
lp15@66289
  1911
        using z rel_interior_subset hull_subset[of "closure S"] by blast
lp15@66289
  1912
      ultimately have "y \<in> affine hull closure S"
lp15@66289
  1913
        using y_def affine_affine_hull[of "closure S"]
lp15@66289
  1914
          mem_affine_3_minus [of "affine hull closure S" z z x "e/norm(z-x)"] by auto
lp15@66289
  1915
      then have "y \<in> closure S" using e yball by auto
lp15@66289
  1916
      have "(1 + (e/norm(z-x))) *\<^sub>R z = (e/norm(z-x)) *\<^sub>R x + y"
lp15@66289
  1917
        using y_def by (simp add: algebra_simps)
lp15@66289
  1918
      then obtain e1 where "0 < e1" "e1 \<le> 1" "z = y - e1 *\<^sub>R (y - x)"
lp15@66289
  1919
        using * convex_rel_interior_closure_aux[of "e / norm (z - x)" 1 z x y]
lp15@66289
  1920
        by (auto simp add: algebra_simps)
lp15@66289
  1921
      then show ?thesis
lp15@66289
  1922
        using rel_interior_closure_convex_shrink assms x \<open>y \<in> closure S\<close>
lp15@66289
  1923
        by auto
lp15@66289
  1924
    qed
lp15@66289
  1925
  }
lp15@66289
  1926
  ultimately show ?thesis by auto
lp15@66289
  1927
qed
lp15@66289
  1928
lp15@66289
  1929
lemma convex_interior_closure:
lp15@66289
  1930
  fixes S :: "'n::euclidean_space set"
lp15@66289
  1931
  assumes "convex S"
lp15@66289
  1932
  shows "interior (closure S) = interior S"
lp15@66289
  1933
  using closure_aff_dim[of S] interior_rel_interior_gen[of S]
lp15@66289
  1934
    interior_rel_interior_gen[of "closure S"]
lp15@66289
  1935
    convex_rel_interior_closure[of S] assms
lp15@66289
  1936
  by auto
lp15@66289
  1937
lp15@66289
  1938
lemma closure_eq_rel_interior_eq:
lp15@66289
  1939
  fixes S1 S2 :: "'n::euclidean_space set"
lp15@66289
  1940
  assumes "convex S1"
lp15@66289
  1941
    and "convex S2"
lp15@66289
  1942
  shows "closure S1 = closure S2 \<longleftrightarrow> rel_interior S1 = rel_interior S2"
lp15@66289
  1943
  by (metis convex_rel_interior_closure convex_closure_rel_interior assms)
lp15@66289
  1944
lp15@66289
  1945
lemma closure_eq_between:
lp15@66289
  1946
  fixes S1 S2 :: "'n::euclidean_space set"
lp15@66289
  1947
  assumes "convex S1"
lp15@66289
  1948
    and "convex S2"
lp15@66289
  1949
  shows "closure S1 = closure S2 \<longleftrightarrow> rel_interior S1 \<le> S2 \<and> S2 \<subseteq> closure S1"
lp15@66289
  1950
  (is "?A \<longleftrightarrow> ?B")
lp15@66289
  1951
proof
lp15@66289
  1952
  assume ?A
lp15@66289
  1953
  then show ?B
lp15@66289
  1954
    by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
lp15@66289
  1955
next
lp15@66289
  1956
  assume ?B
lp15@66289
  1957
  then have "closure S1 \<subseteq> closure S2"
lp15@66289
  1958
    by (metis assms(1) convex_closure_rel_interior closure_mono)
lp15@66289
  1959
  moreover from \<open>?B\<close> have "closure S1 \<supseteq> closure S2"
lp15@66289
  1960
    by (metis closed_closure closure_minimal)
lp15@66289
  1961
  ultimately show ?A ..
lp15@66289
  1962
qed
lp15@66289
  1963
lp15@66289
  1964
lemma open_inter_closure_rel_interior:
lp15@66289
  1965
  fixes S A :: "'n::euclidean_space set"
lp15@66289
  1966
  assumes "convex S"
lp15@66289
  1967
    and "open A"
lp15@66289
  1968
  shows "A \<inter> closure S = {} \<longleftrightarrow> A \<inter> rel_interior S = {}"
lp15@66289
  1969
  by (metis assms convex_closure_rel_interior open_Int_closure_eq_empty)
lp15@66289
  1970
lp15@66289
  1971
lemma rel_interior_open_segment:
lp15@66289
  1972
  fixes a :: "'a :: euclidean_space"
lp15@66289
  1973
  shows "rel_interior(open_segment a b) = open_segment a b"
lp15@66289
  1974
proof (cases "a = b")
lp15@66289
  1975
  case True then show ?thesis by auto
lp15@66289
  1976
next
lp15@66289
  1977
  case False then show ?thesis
lp15@66289
  1978
    apply (simp add: rel_interior_eq openin_open)
lp15@66289
  1979
    apply (rule_tac x="ball (inverse 2 *\<^sub>R (a + b)) (norm(b - a) / 2)" in exI)
lp15@66289
  1980
    apply (simp add: open_segment_as_ball)
lp15@66289
  1981
    done
lp15@66289
  1982
qed
lp15@66289
  1983
lp15@66289
  1984
lemma rel_interior_closed_segment:
lp15@66289
  1985
  fixes a :: "'a :: euclidean_space"
lp15@66289
  1986
  shows "rel_interior(closed_segment a b) =
lp15@66289
  1987
         (if a = b then {a} else open_segment a b)"
lp15@66289
  1988
proof (cases "a = b")
lp15@66289
  1989
  case True then show ?thesis by auto
lp15@66289
  1990
next
lp15@66289
  1991
  case False then show ?thesis
lp15@66289
  1992
    by simp
lp15@66289
  1993
       (metis closure_open_segment convex_open_segment convex_rel_interior_closure
lp15@66289
  1994
              rel_interior_open_segment)
lp15@66289
  1995
qed
lp15@66289
  1996
lp15@66289
  1997
lemmas rel_interior_segment = rel_interior_closed_segment rel_interior_open_segment
lp15@66289
  1998
lp15@66289
  1999
lemma starlike_convex_tweak_boundary_points:
lp15@66289
  2000
  fixes S :: "'a::euclidean_space set"
lp15@66289
  2001
  assumes "convex S" "S \<noteq> {}" and ST: "rel_interior S \<subseteq> T" and TS: "T \<subseteq> closure S"
lp15@66289
  2002
  shows "starlike T"
lp15@66289
  2003
proof -
lp15@66289
  2004
  have "rel_interior S \<noteq> {}"
lp15@66289
  2005
    by (simp add: assms rel_interior_eq_empty)
lp15@66289
  2006
  then obtain a where a: "a \<in> rel_interior S"  by blast
lp15@66289
  2007
  with ST have "a \<in> T"  by blast
lp15@66289
  2008
  have *: "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
lp15@66289
  2009
    apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
lp15@66289
  2010
    using assms by blast
lp15@66289
  2011
  show ?thesis
lp15@66289
  2012
    unfolding starlike_def
lp15@66289
  2013
    apply (rule bexI [OF _ \<open>a \<in> T\<close>])
lp15@66289
  2014
    apply (simp add: closed_segment_eq_open)
lp15@66289
  2015
    apply (intro conjI ballI a \<open>a \<in> T\<close> rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
lp15@66289
  2016
    apply (simp add: order_trans [OF * ST])
lp15@66289
  2017
    done
lp15@66289
  2018
qed
lp15@66289
  2019
lp15@66289
  2020
subsection\<open>The relative frontier of a set\<close>
lp15@66289
  2021
immler@67962
  2022
definition%important "rel_frontier S = closure S - rel_interior S"
lp15@66289
  2023
lp15@66289
  2024
lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
lp15@66289
  2025
  by (simp add: rel_frontier_def)
lp15@66289
  2026
lp15@66289
  2027
lemma rel_frontier_eq_empty:
lp15@66289
  2028
    fixes S :: "'n::euclidean_space set"
lp15@66289
  2029
    shows "rel_frontier S = {} \<longleftrightarrow> affine S"
lp15@68056
  2030
  unfolding rel_frontier_def
lp15@68056
  2031
  using rel_interior_subset_closure  by (auto simp add: rel_interior_eq_closure [symmetric])
lp15@66289
  2032
lp15@66289
  2033
lemma rel_frontier_sing [simp]:
lp15@66289
  2034
    fixes a :: "'n::euclidean_space"
lp15@66289
  2035
    shows "rel_frontier {a} = {}"
lp15@66289
  2036
  by (simp add: rel_frontier_def)
lp15@66289
  2037
lp15@66289
  2038
lemma rel_frontier_affine_hull:
lp15@66289
  2039
  fixes S :: "'a::euclidean_space set"
lp15@66289
  2040
  shows "rel_frontier S \<subseteq> affine hull S"
lp15@66289
  2041
using closure_affine_hull rel_frontier_def by fastforce
lp15@66289
  2042
lp15@66289
  2043
lemma rel_frontier_cball [simp]:
lp15@66289
  2044
    fixes a :: "'n::euclidean_space"
lp15@66289
  2045
    shows "rel_frontier(cball a r) = (if r = 0 then {} else sphere a r)"
lp15@66289
  2046
proof (cases rule: linorder_cases [of r 0])
lp15@66289
  2047
  case less then show ?thesis
lp15@66289
  2048
    by (force simp: sphere_def)
lp15@66289
  2049
next
lp15@66289
  2050
  case equal then show ?thesis by simp
lp15@66289
  2051
next
lp15@66289
  2052
  case greater then show ?thesis
lp15@66289
  2053
    apply simp
lp15@66289
  2054
    by (metis centre_in_ball empty_iff frontier_cball frontier_def interior_cball interior_rel_interior_gen rel_frontier_def)
lp15@66289
  2055
qed
lp15@66289
  2056
lp15@66289
  2057
lemma rel_frontier_translation:
lp15@66289
  2058
  fixes a :: "'a::euclidean_space"
lp15@66289
  2059
  shows "rel_frontier((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (rel_frontier S)"
lp15@66289
  2060
by (simp add: rel_frontier_def translation_diff rel_interior_translation closure_translation)
lp15@66289
  2061
lp15@66289
  2062
lemma closed_affine_hull [iff]:
lp15@66289
  2063
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2064
  shows "closed (affine hull S)"
lp15@66289
  2065
  by (metis affine_affine_hull affine_closed)
lp15@66289
  2066
lp15@66289
  2067
lemma rel_frontier_nonempty_interior:
lp15@66289
  2068
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2069
  shows "interior S \<noteq> {} \<Longrightarrow> rel_frontier S = frontier S"
lp15@66289
  2070
by (metis frontier_def interior_rel_interior_gen rel_frontier_def)
lp15@66289
  2071
lp15@66289
  2072
lemma rel_frontier_frontier:
lp15@66289
  2073
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2074
  shows "affine hull S = UNIV \<Longrightarrow> rel_frontier S = frontier S"
lp15@66289
  2075
by (simp add: frontier_def rel_frontier_def rel_interior_interior)
lp15@66289
  2076
lp15@66289
  2077
lemma closest_point_in_rel_frontier:
lp15@66289
  2078
   "\<lbrakk>closed S; S \<noteq> {}; x \<in> affine hull S - rel_interior S\<rbrakk>
lp15@66289
  2079
   \<Longrightarrow> closest_point S x \<in> rel_frontier S"
lp15@66289
  2080
  by (simp add: closest_point_in_rel_interior closest_point_in_set rel_frontier_def)
lp15@66289
  2081
lp15@66289
  2082
lemma closed_rel_frontier [iff]:
lp15@66289
  2083
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2084
  shows "closed (rel_frontier S)"
lp15@66289
  2085
proof -
lp15@69922
  2086
  have *: "closedin (top_of_set (affine hull S)) (closure S - rel_interior S)"
lp15@66289
  2087
    by (simp add: closed_subset closedin_diff closure_affine_hull openin_rel_interior)
lp15@66289
  2088
  show ?thesis
lp15@66289
  2089
    apply (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"])
lp15@66289
  2090
    unfolding rel_frontier_def
lp15@66289
  2091
    using * closed_affine_hull
lp15@66289
  2092
    apply auto
lp15@66289
  2093
    done
lp15@66289
  2094
qed
lp15@66289
  2095
lp15@66289
  2096
lemma closed_rel_boundary:
lp15@66289
  2097
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2098
  shows "closed S \<Longrightarrow> closed(S - rel_interior S)"
lp15@66289
  2099
by (metis closed_rel_frontier closure_closed rel_frontier_def)
lp15@66289
  2100
lp15@66289
  2101
lemma compact_rel_boundary:
lp15@66289
  2102
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2103
  shows "compact S \<Longrightarrow> compact(S - rel_interior S)"
lp15@66289
  2104
by (metis bounded_diff closed_rel_boundary closure_eq compact_closure compact_imp_closed)
lp15@66289
  2105
lp15@66289
  2106
lemma bounded_rel_frontier:
lp15@66289
  2107
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2108
  shows "bounded S \<Longrightarrow> bounded(rel_frontier S)"
lp15@66289
  2109
by (simp add: bounded_closure bounded_diff rel_frontier_def)
lp15@66289
  2110
lp15@66289
  2111
lemma compact_rel_frontier_bounded:
lp15@66289
  2112
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2113
  shows "bounded S \<Longrightarrow> compact(rel_frontier S)"
lp15@66289
  2114
using bounded_rel_frontier closed_rel_frontier compact_eq_bounded_closed by blast
lp15@66289
  2115
lp15@66289
  2116
lemma compact_rel_frontier:
lp15@66289
  2117
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2118
  shows "compact S \<Longrightarrow> compact(rel_frontier S)"
lp15@66289
  2119
by (meson compact_eq_bounded_closed compact_rel_frontier_bounded)
lp15@66289
  2120
lp15@66289
  2121
lemma convex_same_rel_interior_closure:
lp15@66289
  2122
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2123
  shows "\<lbrakk>convex S; convex T\<rbrakk>
lp15@66289
  2124
         \<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow> closure S = closure T"
lp15@66289
  2125
by (simp add: closure_eq_rel_interior_eq)
lp15@66289
  2126
lp15@66289
  2127
lemma convex_same_rel_interior_closure_straddle:
lp15@66289
  2128
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2129
  shows "\<lbrakk>convex S; convex T\<rbrakk>
lp15@66289
  2130
         \<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow>
lp15@66289
  2131
             rel_interior S \<subseteq> T \<and> T \<subseteq> closure S"
lp15@66289
  2132
by (simp add: closure_eq_between convex_same_rel_interior_closure)
lp15@66289
  2133
lp15@66289
  2134
lemma convex_rel_frontier_aff_dim:
lp15@66289
  2135
  fixes S1 S2 :: "'n::euclidean_space set"
lp15@66289
  2136
  assumes "convex S1"
lp15@66289
  2137
    and "convex S2"
lp15@66289
  2138
    and "S2 \<noteq> {}"
lp15@66289
  2139
    and "S1 \<le> rel_frontier S2"
lp15@66289
  2140
  shows "aff_dim S1 < aff_dim S2"
lp15@66289
  2141
proof -
lp15@66289
  2142
  have "S1 \<subseteq> closure S2"
lp15@66289
  2143
    using assms unfolding rel_frontier_def by auto
lp15@66289
  2144
  then have *: "affine hull S1 \<subseteq> affine hull S2"
lp15@66289
  2145
    using hull_mono[of "S1" "closure S2"] closure_same_affine_hull[of S2] by blast
lp15@66289
  2146
  then have "aff_dim S1 \<le> aff_dim S2"
lp15@66289
  2147
    using * aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2]
lp15@66289
  2148
      aff_dim_subset[of "affine hull S1" "affine hull S2"]
lp15@66289
  2149
    by auto
lp15@66289
  2150
  moreover
lp15@66289
  2151
  {
lp15@66289
  2152
    assume eq: "aff_dim S1 = aff_dim S2"
lp15@66289
  2153
    then have "S1 \<noteq> {}"
lp15@66289
  2154
      using aff_dim_empty[of S1] aff_dim_empty[of S2] \<open>S2 \<noteq> {}\<close> by auto
lp15@66289
  2155
    have **: "affine hull S1 = affine hull S2"
lp15@66289
  2156
       apply (rule affine_dim_equal)
lp15@66289
  2157
       using * affine_affine_hull
lp15@66289
  2158
       apply auto
lp15@66289
  2159
       using \<open>S1 \<noteq> {}\<close> hull_subset[of S1]
lp15@66289
  2160
       apply auto
lp15@66289
  2161
       using eq aff_dim_affine_hull[of S1] aff_dim_affine_hull[of S2]
lp15@66289
  2162
       apply auto
lp15@66289
  2163
       done
lp15@66289
  2164
    obtain a where a: "a \<in> rel_interior S1"
lp15@66289
  2165
      using \<open>S1 \<noteq> {}\<close> rel_interior_eq_empty assms by auto
lp15@66289
  2166
    obtain T where T: "open T" "a \<in> T \<inter> S1" "T \<inter> affine hull S1 \<subseteq> S1"
lp15@66289
  2167
       using mem_rel_interior[of a S1] a by auto
lp15@66289
  2168
    then have "a \<in> T \<inter> closure S2"
lp15@66289
  2169
      using a assms unfolding rel_frontier_def by auto
lp15@66289
  2170
    then obtain b where b: "b \<in> T \<inter> rel_interior S2"
lp15@66289
  2171
      using open_inter_closure_rel_interior[of S2 T] assms T by auto
lp15@66289
  2172
    then have "b \<in> affine hull S1"
lp15@66289
  2173
      using rel_interior_subset hull_subset[of S2] ** by auto
lp15@66289
  2174
    then have "b \<in> S1"
lp15@66289
  2175
      using T b by auto
lp15@66289
  2176
    then have False
lp15@66289
  2177
      using b assms unfolding rel_frontier_def by auto
lp15@66289
  2178
  }
lp15@66289
  2179
  ultimately show ?thesis
lp15@66289
  2180
    using less_le by auto
lp15@66289
  2181
qed
lp15@66289
  2182
lp15@66289
  2183
lemma convex_rel_interior_if:
lp15@66289
  2184
  fixes S ::  "'n::euclidean_space set"
lp15@66289
  2185
  assumes "convex S"
lp15@66289
  2186
    and "z \<in> rel_interior S"
lp15@66289
  2187
  shows "\<forall>x\<in>affine hull S. \<exists>m. m > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> m \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)"
lp15@66289
  2188
proof -
lp15@66289
  2189
  obtain e1 where e1: "e1 > 0 \<and> cball z e1 \<inter> affine hull S \<subseteq> S"
lp15@66289
  2190
    using mem_rel_interior_cball[of z S] assms by auto
lp15@66289
  2191
  {
lp15@66289
  2192
    fix x
lp15@66289
  2193
    assume x: "x \<in> affine hull S"
lp15@66289
  2194
    {
lp15@66289
  2195
      assume "x \<noteq> z"
lp15@66289
  2196
      define m where "m = 1 + e1/norm(x-z)"
lp15@66289
  2197
      hence "m > 1" using e1 \<open>x \<noteq> z\<close> by auto
lp15@66289
  2198
      {
lp15@66289
  2199
        fix e
lp15@66289
  2200
        assume e: "e > 1 \<and> e \<le> m"
lp15@66289
  2201
        have "z \<in> affine hull S"
lp15@66289
  2202
          using assms rel_interior_subset hull_subset[of S] by auto
lp15@66289
  2203
        then have *: "(1 - e)*\<^sub>R x + e *\<^sub>R z \<in> affine hull S"
lp15@66289
  2204
          using mem_affine[of "affine hull S" x z "(1-e)" e] affine_affine_hull[of S] x
lp15@66289
  2205
          by auto
lp15@66289
  2206
        have "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) = norm ((e - 1) *\<^sub>R (x - z))"
lp15@66289
  2207
          by (simp add: algebra_simps)
lp15@66289
  2208
        also have "\<dots> = (e - 1) * norm (x-z)"
lp15@66289
  2209
          using norm_scaleR e by auto
lp15@66289
  2210
        also have "\<dots> \<le> (m - 1) * norm (x - z)"
lp15@66289
  2211
          using e mult_right_mono[of _ _ "norm(x-z)"] by auto
lp15@66289
  2212
        also have "\<dots> = (e1 / norm (x - z)) * norm (x - z)"
lp15@66289
  2213
          using m_def by auto
lp15@66289
  2214
        also have "\<dots> = e1"
lp15@66289
  2215
          using \<open>x \<noteq> z\<close> e1 by simp
lp15@66289
  2216
        finally have **: "norm (z + e *\<^sub>R x - (x + e *\<^sub>R z)) \<le> e1"
lp15@66289
  2217
          by auto
lp15@66289
  2218
        have "(1 - e)*\<^sub>R x+ e *\<^sub>R z \<in> cball z e1"
lp15@66289
  2219
          using m_def **
lp15@66289
  2220
          unfolding cball_def dist_norm
lp15@66289
  2221
          by (auto simp add: algebra_simps)
lp15@66289
  2222
        then have "(1 - e) *\<^sub>R x+ e *\<^sub>R z \<in> S"
lp15@66289
  2223
          using e * e1 by auto
lp15@66289
  2224
      }
lp15@66289
  2225
      then have "\<exists>m. m > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> m \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S )"
lp15@66289
  2226
        using \<open>m> 1 \<close> by auto
lp15@66289
  2227
    }
lp15@66289
  2228
    moreover
lp15@66289
  2229
    {
lp15@66289
  2230
      assume "x = z"
lp15@66289
  2231
      define m where "m = 1 + e1"
lp15@66289
  2232
      then have "m > 1"
lp15@66289
  2233
        using e1 by auto
lp15@66289
  2234
      {
lp15@66289
  2235
        fix e
lp15@66289
  2236
        assume e: "e > 1 \<and> e \<le> m"
lp15@66289
  2237
        then have "(1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S"
lp15@66289
  2238
          using e1 x \<open>x = z\<close> by (auto simp add: algebra_simps)
lp15@66289
  2239
        then have "(1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S"
lp15@66289
  2240
          using e by auto
lp15@66289
  2241
      }
lp15@66289
  2242
      then have "\<exists>m. m > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> m \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)"
lp15@66289
  2243
        using \<open>m > 1\<close> by auto
lp15@66289
  2244
    }
lp15@66289
  2245
    ultimately have "\<exists>m. m > 1 \<and> (\<forall>e. e > 1 \<and> e \<le> m \<longrightarrow> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S )"
lp15@66289
  2246
      by blast
lp15@66289
  2247
  }
lp15@66289
  2248
  then show ?thesis by auto
lp15@66289
  2249
qed
lp15@66289
  2250
lp15@66289
  2251
lemma convex_rel_interior_if2:
lp15@66289
  2252
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2253
  assumes "convex S"
lp15@66289
  2254
  assumes "z \<in> rel_interior S"
lp15@66289
  2255
  shows "\<forall>x\<in>affine hull S. \<exists>e. e > 1 \<and> (1 - e)*\<^sub>R x + e *\<^sub>R z \<in> S"
lp15@66289
  2256
  using convex_rel_interior_if[of S z] assms by auto
lp15@66289
  2257
lp15@66289
  2258
lemma convex_rel_interior_only_if:
lp15@66289
  2259
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2260
  assumes "convex S"
lp15@66289
  2261
    and "S \<noteq> {}"
lp15@66289
  2262
  assumes "\<forall>x\<in>S. \<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S"
lp15@66289
  2263
  shows "z \<in> rel_interior S"
lp15@66289
  2264
proof -
lp15@66289
  2265
  obtain x where x: "x \<in> rel_interior S"
lp15@66289
  2266
    using rel_interior_eq_empty assms by auto
lp15@66289
  2267
  then have "x \<in> S"
lp15@66289
  2268
    using rel_interior_subset by auto
lp15@66289
  2269
  then obtain e where e: "e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S"
lp15@66289
  2270
    using assms by auto
lp15@66289
  2271
  define y where [abs_def]: "y = (1 - e) *\<^sub>R x + e *\<^sub>R z"
lp15@66289
  2272
  then have "y \<in> S" using e by auto
lp15@66289
  2273
  define e1 where "e1 = 1/e"
lp15@66289
  2274
  then have "0 < e1 \<and> e1 < 1" using e by auto
lp15@66289
  2275
  then have "z  =y - (1 - e1) *\<^sub>R (y - x)"
lp15@66289
  2276
    using e1_def y_def by (auto simp add: algebra_simps)
lp15@66289
  2277
  then show ?thesis
lp15@66289
  2278
    using rel_interior_convex_shrink[of S x y "1-e1"] \<open>0 < e1 \<and> e1 < 1\<close> \<open>y \<in> S\<close> x assms
lp15@66289
  2279
    by auto
lp15@66289
  2280
qed
lp15@66289
  2281
lp15@66289
  2282
lemma convex_rel_interior_iff:
lp15@66289
  2283
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2284
  assumes "convex S"
lp15@66289
  2285
    and "S \<noteq> {}"
lp15@66289
  2286
  shows "z \<in> rel_interior S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)"
lp15@66289
  2287
  using assms hull_subset[of S "affine"]
lp15@66289
  2288
    convex_rel_interior_if[of S z] convex_rel_interior_only_if[of S z]
lp15@66289
  2289
  by auto
lp15@66289
  2290
lp15@66289
  2291
lemma convex_rel_interior_iff2:
lp15@66289
  2292
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2293
  assumes "convex S"
lp15@66289
  2294
    and "S \<noteq> {}"
lp15@66289
  2295
  shows "z \<in> rel_interior S \<longleftrightarrow> (\<forall>x\<in>affine hull S. \<exists>e. e > 1 \<and> (1 - e) *\<^sub>R x + e *\<^sub>R z \<in> S)"
lp15@66289
  2296
  using assms hull_subset[of S] convex_rel_interior_if2[of S z] convex_rel_interior_only_if[of S z]
lp15@66289
  2297
  by auto
lp15@66289
  2298
lp15@66289
  2299
lemma convex_interior_iff:
lp15@66289
  2300
  fixes S :: "'n::euclidean_space set"
lp15@66289
  2301
  assumes "convex S"
lp15@66289
  2302
  shows "z \<in> interior S \<longleftrightarrow> (\<forall>x. \<exists>e. e > 0 \<and> z + e *\<^sub>R x \<in> S)"
lp15@66289
  2303
proof (cases "aff_dim S = int DIM('n)")
lp15@66289
  2304
  case False
lp15@68056
  2305
  { assume "z \<in> interior S"
lp15@66289
  2306
    then have False
lp15@68056
  2307
      using False interior_rel_interior_gen[of S] by auto }
lp15@66289
  2308
  moreover
lp15@68056
  2309
  { assume r: "\<forall>x. \<exists>e. e > 0 \<and> z + e *\<^sub>R x \<in> S"
lp15@68056
  2310
    { fix x
lp15@66289
  2311
      obtain e1 where e1: "e1 > 0 \<and> z + e1 *\<^sub>R (x - z) \<in> S"
lp15@66289
  2312
        using r by auto
lp15@66289
  2313
      obtain e2 where e2: "e2 > 0 \<and> z + e2 *\<^sub>R (z - x) \<in> S"
lp15@66289
  2314
        using r by auto
lp15@66289
  2315
      define x1 where [abs_def]: "x1 = z + e1 *\<^sub>R (x - z)"
lp15@66289
  2316
      then have x1: "x1 \<in> affine hull S"
lp15@66289
  2317
        using e1 hull_subset[of S] by auto
lp15@66289
  2318
      define x2 where [abs_def]: "x2 = z + e2 *\<^sub>R (z - x)"
lp15@66289
  2319
      then have x2: "x2 \<in> affine hull S"
lp15@66289
  2320
        using e2 hull_subset[of S] by auto
lp15@66289
  2321
      have *: "e1/(e1+e2) + e2/(e1+e2) = 1"
lp15@66289
  2322
        using add_divide_distrib[of e1 e2 "e1+e2"] e1 e2 by simp
lp15@66289
  2323
      then have "z = (e2/(e1+e2)) *\<^sub>R x1 + (e1/(e1+e2)) *\<^sub>R x2"
lp15@66289
  2324
        using x1_def x2_def
lp15@66289
  2325
        apply (auto simp add: algebra_simps)
lp15@66289
  2326
        using scaleR_left_distrib[of "e1/(e1+e2)" "e2/(e1+e2)" z]
lp15@66289
  2327
        apply auto
lp15@66289
  2328
        done
lp15@66289
  2329
      then have z: "z \<in> affine hull S"
lp15@66289
  2330
        using mem_affine[of "affine hull S" x1 x2 "e2/(e1+e2)" "e1/(e1+e2)"]
lp15@66289
  2331
          x1 x2 affine_affine_hull[of S] *
lp15@66289
  2332
        by auto
lp15@66289
  2333
      have "x1 - x2 = (e1 + e2) *\<^sub>R (x - z)"
lp15@66289
  2334
        using x1_def x2_def by (auto simp add: algebra_simps)
lp15@66289
  2335
      then have "x = z+(1/(e1+e2)) *\<^sub>R (x1-x2)"
lp15@66289
  2336
        using e1 e2 by simp
lp15@66289
  2337
      then have "x \<in> affine hull S"
lp15@66289
  2338
        using mem_affine_3_minus[of "affine hull S" z x1 x2 "1/(e1+e2)"]
lp15@66289
  2339
          x1 x2 z affine_affine_hull[of S]
lp15@66289
  2340
        by auto
lp15@66289
  2341
    }
lp15@66289
  2342
    then have "affine hull S = UNIV"
lp15@66289
  2343
      by auto
lp15@66289
  2344
    then have "aff_dim S = int DIM('n)"
lp15@66289
  2345
      using aff_dim_affine_hull[of S] by (simp add: aff_dim_UNIV)
lp15@66289
  2346
    then have False
lp15@66289
  2347
      using False by auto
lp15@66289
  2348
  }
lp15@66289
  2349
  ultimately show ?thesis by auto
lp15@66289
  2350
next
lp15@66289
  2351
  case True
lp15@66289
  2352
  then have "S \<noteq> {}"
lp15@66289
  2353
    using aff_dim_empty[of S] by auto
lp15@66289
  2354
  have *: "affine hull S = UNIV"