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