src/HOL/Analysis/Convex.thy
author immler
Mon Jan 07 14:06:54 2019 +0100 (4 months ago)
changeset 69619 3f7d8e05e0f2
child 69661 a03a63b81f44
permissions -rw-r--r--
split off Convex.thy: material that does not require Topology_Euclidean_Space
immler@69619
     1
(* Title:      HOL/Analysis/Convex_Euclidean_Space.thy
immler@69619
     2
   Author:     L C Paulson, University of Cambridge
immler@69619
     3
   Author:     Robert Himmelmann, TU Muenchen
immler@69619
     4
   Author:     Bogdan Grechuk, University of Edinburgh
immler@69619
     5
   Author:     Armin Heller, TU Muenchen
immler@69619
     6
   Author:     Johannes Hoelzl, TU Muenchen
immler@69619
     7
*)
immler@69619
     8
immler@69619
     9
section \<open>Convex Sets and Functions\<close>
immler@69619
    10
immler@69619
    11
theory Convex
immler@69619
    12
imports
immler@69619
    13
  Linear_Algebra
immler@69619
    14
  "HOL-Library.Set_Algebras"
immler@69619
    15
begin
immler@69619
    16
immler@69619
    17
lemma substdbasis_expansion_unique:
immler@69619
    18
  assumes d: "d \<subseteq> Basis"
immler@69619
    19
  shows "(\<Sum>i\<in>d. f i *\<^sub>R i) = (x::'a::euclidean_space) \<longleftrightarrow>
immler@69619
    20
    (\<forall>i\<in>Basis. (i \<in> d \<longrightarrow> f i = x \<bullet> i) \<and> (i \<notin> d \<longrightarrow> x \<bullet> i = 0))"
immler@69619
    21
proof -
immler@69619
    22
  have *: "\<And>x a b P. x * (if P then a else b) = (if P then x * a else x * b)"
immler@69619
    23
    by auto
immler@69619
    24
  have **: "finite d"
immler@69619
    25
    by (auto intro: finite_subset[OF assms])
immler@69619
    26
  have ***: "\<And>i. i \<in> Basis \<Longrightarrow> (\<Sum>i\<in>d. f i *\<^sub>R i) \<bullet> i = (\<Sum>x\<in>d. if x = i then f x else 0)"
immler@69619
    27
    using d
immler@69619
    28
    by (auto intro!: sum.cong simp: inner_Basis inner_sum_left)
immler@69619
    29
  show ?thesis
immler@69619
    30
    unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***)
immler@69619
    31
qed
immler@69619
    32
immler@69619
    33
lemma independent_substdbasis: "d \<subseteq> Basis \<Longrightarrow> independent d"
immler@69619
    34
  by (rule independent_mono[OF independent_Basis])
immler@69619
    35
immler@69619
    36
lemma sum_not_0: "sum f A \<noteq> 0 \<Longrightarrow> \<exists>a \<in> A. f a \<noteq> 0"
immler@69619
    37
  by (rule ccontr) auto
immler@69619
    38
immler@69619
    39
lemma subset_translation_eq [simp]:
immler@69619
    40
    fixes a :: "'a::real_vector" shows "(+) a ` s \<subseteq> (+) a ` t \<longleftrightarrow> s \<subseteq> t"
immler@69619
    41
  by auto
immler@69619
    42
immler@69619
    43
lemma translate_inj_on:
immler@69619
    44
  fixes A :: "'a::ab_group_add set"
immler@69619
    45
  shows "inj_on (\<lambda>x. a + x) A"
immler@69619
    46
  unfolding inj_on_def by auto
immler@69619
    47
immler@69619
    48
lemma translation_assoc:
immler@69619
    49
  fixes a b :: "'a::ab_group_add"
immler@69619
    50
  shows "(\<lambda>x. b + x) ` ((\<lambda>x. a + x) ` S) = (\<lambda>x. (a + b) + x) ` S"
immler@69619
    51
  by auto
immler@69619
    52
immler@69619
    53
lemma translation_invert:
immler@69619
    54
  fixes a :: "'a::ab_group_add"
immler@69619
    55
  assumes "(\<lambda>x. a + x) ` A = (\<lambda>x. a + x) ` B"
immler@69619
    56
  shows "A = B"
immler@69619
    57
proof -
immler@69619
    58
  have "(\<lambda>x. -a + x) ` ((\<lambda>x. a + x) ` A) = (\<lambda>x. - a + x) ` ((\<lambda>x. a + x) ` B)"
immler@69619
    59
    using assms by auto
immler@69619
    60
  then show ?thesis
immler@69619
    61
    using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto
immler@69619
    62
qed
immler@69619
    63
immler@69619
    64
lemma translation_galois:
immler@69619
    65
  fixes a :: "'a::ab_group_add"
immler@69619
    66
  shows "T = ((\<lambda>x. a + x) ` S) \<longleftrightarrow> S = ((\<lambda>x. (- a) + x) ` T)"
immler@69619
    67
  using translation_assoc[of "-a" a S]
immler@69619
    68
  apply auto
immler@69619
    69
  using translation_assoc[of a "-a" T]
immler@69619
    70
  apply auto
immler@69619
    71
  done
immler@69619
    72
immler@69619
    73
lemma translation_inverse_subset:
immler@69619
    74
  assumes "((\<lambda>x. - a + x) ` V) \<le> (S :: 'n::ab_group_add set)"
immler@69619
    75
  shows "V \<le> ((\<lambda>x. a + x) ` S)"
immler@69619
    76
proof -
immler@69619
    77
  {
immler@69619
    78
    fix x
immler@69619
    79
    assume "x \<in> V"
immler@69619
    80
    then have "x-a \<in> S" using assms by auto
immler@69619
    81
    then have "x \<in> {a + v |v. v \<in> S}"
immler@69619
    82
      apply auto
immler@69619
    83
      apply (rule exI[of _ "x-a"], simp)
immler@69619
    84
      done
immler@69619
    85
    then have "x \<in> ((\<lambda>x. a+x) ` S)" by auto
immler@69619
    86
  }
immler@69619
    87
  then show ?thesis by auto
immler@69619
    88
qed
immler@69619
    89
immler@69619
    90
subsection \<open>Convexity\<close>
immler@69619
    91
immler@69619
    92
definition%important convex :: "'a::real_vector set \<Rightarrow> bool"
immler@69619
    93
  where "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
immler@69619
    94
immler@69619
    95
lemma convexI:
immler@69619
    96
  assumes "\<And>x y u v. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 \<le> u \<Longrightarrow> 0 \<le> v \<Longrightarrow> u + v = 1 \<Longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s"
immler@69619
    97
  shows "convex s"
immler@69619
    98
  using assms unfolding convex_def by fast
immler@69619
    99
immler@69619
   100
lemma convexD:
immler@69619
   101
  assumes "convex s" and "x \<in> s" and "y \<in> s" and "0 \<le> u" and "0 \<le> v" and "u + v = 1"
immler@69619
   102
  shows "u *\<^sub>R x + v *\<^sub>R y \<in> s"
immler@69619
   103
  using assms unfolding convex_def by fast
immler@69619
   104
immler@69619
   105
lemma convex_alt: "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> ((1 - u) *\<^sub>R x + u *\<^sub>R y) \<in> s)"
immler@69619
   106
  (is "_ \<longleftrightarrow> ?alt")
immler@69619
   107
proof
immler@69619
   108
  show "convex s" if alt: ?alt
immler@69619
   109
  proof -
immler@69619
   110
    {
immler@69619
   111
      fix x y and u v :: real
immler@69619
   112
      assume mem: "x \<in> s" "y \<in> s"
immler@69619
   113
      assume "0 \<le> u" "0 \<le> v"
immler@69619
   114
      moreover
immler@69619
   115
      assume "u + v = 1"
immler@69619
   116
      then have "u = 1 - v" by auto
immler@69619
   117
      ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> s"
immler@69619
   118
        using alt [rule_format, OF mem] by auto
immler@69619
   119
    }
immler@69619
   120
    then show ?thesis
immler@69619
   121
      unfolding convex_def by auto
immler@69619
   122
  qed
immler@69619
   123
  show ?alt if "convex s"
immler@69619
   124
    using that by (auto simp: convex_def)
immler@69619
   125
qed
immler@69619
   126
immler@69619
   127
lemma convexD_alt:
immler@69619
   128
  assumes "convex s" "a \<in> s" "b \<in> s" "0 \<le> u" "u \<le> 1"
immler@69619
   129
  shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
immler@69619
   130
  using assms unfolding convex_alt by auto
immler@69619
   131
immler@69619
   132
lemma mem_convex_alt:
immler@69619
   133
  assumes "convex S" "x \<in> S" "y \<in> S" "u \<ge> 0" "v \<ge> 0" "u + v > 0"
immler@69619
   134
  shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) \<in> S"
immler@69619
   135
  apply (rule convexD)
immler@69619
   136
  using assms
immler@69619
   137
       apply (simp_all add: zero_le_divide_iff add_divide_distrib [symmetric])
immler@69619
   138
  done
immler@69619
   139
immler@69619
   140
lemma convex_empty[intro,simp]: "convex {}"
immler@69619
   141
  unfolding convex_def by simp
immler@69619
   142
immler@69619
   143
lemma convex_singleton[intro,simp]: "convex {a}"
immler@69619
   144
  unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric])
immler@69619
   145
immler@69619
   146
lemma convex_UNIV[intro,simp]: "convex UNIV"
immler@69619
   147
  unfolding convex_def by auto
immler@69619
   148
immler@69619
   149
lemma convex_Inter: "(\<And>s. s\<in>f \<Longrightarrow> convex s) \<Longrightarrow> convex(\<Inter>f)"
immler@69619
   150
  unfolding convex_def by auto
immler@69619
   151
immler@69619
   152
lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
immler@69619
   153
  unfolding convex_def by auto
immler@69619
   154
immler@69619
   155
lemma convex_INT: "(\<And>i. i \<in> A \<Longrightarrow> convex (B i)) \<Longrightarrow> convex (\<Inter>i\<in>A. B i)"
immler@69619
   156
  unfolding convex_def by auto
immler@69619
   157
immler@69619
   158
lemma convex_Times: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<times> t)"
immler@69619
   159
  unfolding convex_def by auto
immler@69619
   160
immler@69619
   161
lemma convex_halfspace_le: "convex {x. inner a x \<le> b}"
immler@69619
   162
  unfolding convex_def
immler@69619
   163
  by (auto simp: inner_add intro!: convex_bound_le)
immler@69619
   164
immler@69619
   165
lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}"
immler@69619
   166
proof -
immler@69619
   167
  have *: "{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}"
immler@69619
   168
    by auto
immler@69619
   169
  show ?thesis
immler@69619
   170
    unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
immler@69619
   171
qed
immler@69619
   172
immler@69619
   173
lemma convex_halfspace_abs_le: "convex {x. \<bar>inner a x\<bar> \<le> b}"
immler@69619
   174
proof -
immler@69619
   175
  have *: "{x. \<bar>inner a x\<bar> \<le> b} = {x. inner a x \<le> b} \<inter> {x. -b \<le> inner a x}"
immler@69619
   176
    by auto
immler@69619
   177
  show ?thesis
immler@69619
   178
    unfolding * by (simp add: convex_Int convex_halfspace_ge convex_halfspace_le)
immler@69619
   179
qed
immler@69619
   180
immler@69619
   181
lemma convex_hyperplane: "convex {x. inner a x = b}"
immler@69619
   182
proof -
immler@69619
   183
  have *: "{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}"
immler@69619
   184
    by auto
immler@69619
   185
  show ?thesis using convex_halfspace_le convex_halfspace_ge
immler@69619
   186
    by (auto intro!: convex_Int simp: *)
immler@69619
   187
qed
immler@69619
   188
immler@69619
   189
lemma convex_halfspace_lt: "convex {x. inner a x < b}"
immler@69619
   190
  unfolding convex_def
immler@69619
   191
  by (auto simp: convex_bound_lt inner_add)
immler@69619
   192
immler@69619
   193
lemma convex_halfspace_gt: "convex {x. inner a x > b}"
immler@69619
   194
  using convex_halfspace_lt[of "-a" "-b"] by auto
immler@69619
   195
immler@69619
   196
lemma convex_halfspace_Re_ge: "convex {x. Re x \<ge> b}"
immler@69619
   197
  using convex_halfspace_ge[of b "1::complex"] by simp
immler@69619
   198
immler@69619
   199
lemma convex_halfspace_Re_le: "convex {x. Re x \<le> b}"
immler@69619
   200
  using convex_halfspace_le[of "1::complex" b] by simp
immler@69619
   201
immler@69619
   202
lemma convex_halfspace_Im_ge: "convex {x. Im x \<ge> b}"
immler@69619
   203
  using convex_halfspace_ge[of b \<i>] by simp
immler@69619
   204
immler@69619
   205
lemma convex_halfspace_Im_le: "convex {x. Im x \<le> b}"
immler@69619
   206
  using convex_halfspace_le[of \<i> b] by simp
immler@69619
   207
immler@69619
   208
lemma convex_halfspace_Re_gt: "convex {x. Re x > b}"
immler@69619
   209
  using convex_halfspace_gt[of b "1::complex"] by simp
immler@69619
   210
immler@69619
   211
lemma convex_halfspace_Re_lt: "convex {x. Re x < b}"
immler@69619
   212
  using convex_halfspace_lt[of "1::complex" b] by simp
immler@69619
   213
immler@69619
   214
lemma convex_halfspace_Im_gt: "convex {x. Im x > b}"
immler@69619
   215
  using convex_halfspace_gt[of b \<i>] by simp
immler@69619
   216
immler@69619
   217
lemma convex_halfspace_Im_lt: "convex {x. Im x < b}"
immler@69619
   218
  using convex_halfspace_lt[of \<i> b] by simp
immler@69619
   219
immler@69619
   220
lemma convex_real_interval [iff]:
immler@69619
   221
  fixes a b :: "real"
immler@69619
   222
  shows "convex {a..}" and "convex {..b}"
immler@69619
   223
    and "convex {a<..}" and "convex {..<b}"
immler@69619
   224
    and "convex {a..b}" and "convex {a<..b}"
immler@69619
   225
    and "convex {a..<b}" and "convex {a<..<b}"
immler@69619
   226
proof -
immler@69619
   227
  have "{a..} = {x. a \<le> inner 1 x}"
immler@69619
   228
    by auto
immler@69619
   229
  then show 1: "convex {a..}"
immler@69619
   230
    by (simp only: convex_halfspace_ge)
immler@69619
   231
  have "{..b} = {x. inner 1 x \<le> b}"
immler@69619
   232
    by auto
immler@69619
   233
  then show 2: "convex {..b}"
immler@69619
   234
    by (simp only: convex_halfspace_le)
immler@69619
   235
  have "{a<..} = {x. a < inner 1 x}"
immler@69619
   236
    by auto
immler@69619
   237
  then show 3: "convex {a<..}"
immler@69619
   238
    by (simp only: convex_halfspace_gt)
immler@69619
   239
  have "{..<b} = {x. inner 1 x < b}"
immler@69619
   240
    by auto
immler@69619
   241
  then show 4: "convex {..<b}"
immler@69619
   242
    by (simp only: convex_halfspace_lt)
immler@69619
   243
  have "{a..b} = {a..} \<inter> {..b}"
immler@69619
   244
    by auto
immler@69619
   245
  then show "convex {a..b}"
immler@69619
   246
    by (simp only: convex_Int 1 2)
immler@69619
   247
  have "{a<..b} = {a<..} \<inter> {..b}"
immler@69619
   248
    by auto
immler@69619
   249
  then show "convex {a<..b}"
immler@69619
   250
    by (simp only: convex_Int 3 2)
immler@69619
   251
  have "{a..<b} = {a..} \<inter> {..<b}"
immler@69619
   252
    by auto
immler@69619
   253
  then show "convex {a..<b}"
immler@69619
   254
    by (simp only: convex_Int 1 4)
immler@69619
   255
  have "{a<..<b} = {a<..} \<inter> {..<b}"
immler@69619
   256
    by auto
immler@69619
   257
  then show "convex {a<..<b}"
immler@69619
   258
    by (simp only: convex_Int 3 4)
immler@69619
   259
qed
immler@69619
   260
immler@69619
   261
lemma convex_Reals: "convex \<real>"
immler@69619
   262
  by (simp add: convex_def scaleR_conv_of_real)
immler@69619
   263
immler@69619
   264
immler@69619
   265
subsection%unimportant \<open>Explicit expressions for convexity in terms of arbitrary sums\<close>
immler@69619
   266
immler@69619
   267
lemma convex_sum:
immler@69619
   268
  fixes C :: "'a::real_vector set"
immler@69619
   269
  assumes "finite s"
immler@69619
   270
    and "convex C"
immler@69619
   271
    and "(\<Sum> i \<in> s. a i) = 1"
immler@69619
   272
  assumes "\<And>i. i \<in> s \<Longrightarrow> a i \<ge> 0"
immler@69619
   273
    and "\<And>i. i \<in> s \<Longrightarrow> y i \<in> C"
immler@69619
   274
  shows "(\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C"
immler@69619
   275
  using assms(1,3,4,5)
immler@69619
   276
proof (induct arbitrary: a set: finite)
immler@69619
   277
  case empty
immler@69619
   278
  then show ?case by simp
immler@69619
   279
next
immler@69619
   280
  case (insert i s) note IH = this(3)
immler@69619
   281
  have "a i + sum a s = 1"
immler@69619
   282
    and "0 \<le> a i"
immler@69619
   283
    and "\<forall>j\<in>s. 0 \<le> a j"
immler@69619
   284
    and "y i \<in> C"
immler@69619
   285
    and "\<forall>j\<in>s. y j \<in> C"
immler@69619
   286
    using insert.hyps(1,2) insert.prems by simp_all
immler@69619
   287
  then have "0 \<le> sum a s"
immler@69619
   288
    by (simp add: sum_nonneg)
immler@69619
   289
  have "a i *\<^sub>R y i + (\<Sum>j\<in>s. a j *\<^sub>R y j) \<in> C"
immler@69619
   290
  proof (cases "sum a s = 0")
immler@69619
   291
    case True
immler@69619
   292
    with \<open>a i + sum a s = 1\<close> have "a i = 1"
immler@69619
   293
      by simp
immler@69619
   294
    from sum_nonneg_0 [OF \<open>finite s\<close> _ True] \<open>\<forall>j\<in>s. 0 \<le> a j\<close> have "\<forall>j\<in>s. a j = 0"
immler@69619
   295
      by simp
immler@69619
   296
    show ?thesis using \<open>a i = 1\<close> and \<open>\<forall>j\<in>s. a j = 0\<close> and \<open>y i \<in> C\<close>
immler@69619
   297
      by simp
immler@69619
   298
  next
immler@69619
   299
    case False
immler@69619
   300
    with \<open>0 \<le> sum a s\<close> have "0 < sum a s"
immler@69619
   301
      by simp
immler@69619
   302
    then have "(\<Sum>j\<in>s. (a j / sum a s) *\<^sub>R y j) \<in> C"
immler@69619
   303
      using \<open>\<forall>j\<in>s. 0 \<le> a j\<close> and \<open>\<forall>j\<in>s. y j \<in> C\<close>
immler@69619
   304
      by (simp add: IH sum_divide_distrib [symmetric])
immler@69619
   305
    from \<open>convex C\<close> and \<open>y i \<in> C\<close> and this and \<open>0 \<le> a i\<close>
immler@69619
   306
      and \<open>0 \<le> sum a s\<close> and \<open>a i + sum a s = 1\<close>
immler@69619
   307
    have "a i *\<^sub>R y i + sum a s *\<^sub>R (\<Sum>j\<in>s. (a j / sum a s) *\<^sub>R y j) \<in> C"
immler@69619
   308
      by (rule convexD)
immler@69619
   309
    then show ?thesis
immler@69619
   310
      by (simp add: scaleR_sum_right False)
immler@69619
   311
  qed
immler@69619
   312
  then show ?case using \<open>finite s\<close> and \<open>i \<notin> s\<close>
immler@69619
   313
    by simp
immler@69619
   314
qed
immler@69619
   315
immler@69619
   316
lemma convex:
immler@69619
   317
  "convex s \<longleftrightarrow> (\<forall>(k::nat) u x. (\<forall>i. 1\<le>i \<and> i\<le>k \<longrightarrow> 0 \<le> u i \<and> x i \<in>s) \<and> (sum u {1..k} = 1)
immler@69619
   318
      \<longrightarrow> sum (\<lambda>i. u i *\<^sub>R x i) {1..k} \<in> s)"
immler@69619
   319
proof safe
immler@69619
   320
  fix k :: nat
immler@69619
   321
  fix u :: "nat \<Rightarrow> real"
immler@69619
   322
  fix x
immler@69619
   323
  assume "convex s"
immler@69619
   324
    "\<forall>i. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s"
immler@69619
   325
    "sum u {1..k} = 1"
immler@69619
   326
  with convex_sum[of "{1 .. k}" s] show "(\<Sum>j\<in>{1 .. k}. u j *\<^sub>R x j) \<in> s"
immler@69619
   327
    by auto
immler@69619
   328
next
immler@69619
   329
  assume *: "\<forall>k u x. (\<forall> i :: nat. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s) \<and> sum u {1..k} = 1
immler@69619
   330
    \<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R (x i :: 'a)) \<in> s"
immler@69619
   331
  {
immler@69619
   332
    fix \<mu> :: real
immler@69619
   333
    fix x y :: 'a
immler@69619
   334
    assume xy: "x \<in> s" "y \<in> s"
immler@69619
   335
    assume mu: "\<mu> \<ge> 0" "\<mu> \<le> 1"
immler@69619
   336
    let ?u = "\<lambda>i. if (i :: nat) = 1 then \<mu> else 1 - \<mu>"
immler@69619
   337
    let ?x = "\<lambda>i. if (i :: nat) = 1 then x else y"
immler@69619
   338
    have "{1 :: nat .. 2} \<inter> - {x. x = 1} = {2}"
immler@69619
   339
      by auto
immler@69619
   340
    then have card: "card ({1 :: nat .. 2} \<inter> - {x. x = 1}) = 1"
immler@69619
   341
      by simp
immler@69619
   342
    then have "sum ?u {1 .. 2} = 1"
immler@69619
   343
      using sum.If_cases[of "{(1 :: nat) .. 2}" "\<lambda> x. x = 1" "\<lambda> x. \<mu>" "\<lambda> x. 1 - \<mu>"]
immler@69619
   344
      by auto
immler@69619
   345
    with *[rule_format, of "2" ?u ?x] have s: "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) \<in> s"
immler@69619
   346
      using mu xy by auto
immler@69619
   347
    have grarr: "(\<Sum>j \<in> {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \<mu>) *\<^sub>R y"
immler@69619
   348
      using sum_head_Suc[of "Suc (Suc 0)" 2 "\<lambda> j. (1 - \<mu>) *\<^sub>R y"] by auto
immler@69619
   349
    from sum_head_Suc[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this]
immler@69619
   350
    have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
immler@69619
   351
      by auto
immler@69619
   352
    then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s"
immler@69619
   353
      using s by (auto simp: add.commute)
immler@69619
   354
  }
immler@69619
   355
  then show "convex s"
immler@69619
   356
    unfolding convex_alt by auto
immler@69619
   357
qed
immler@69619
   358
immler@69619
   359
immler@69619
   360
lemma convex_explicit:
immler@69619
   361
  fixes s :: "'a::real_vector set"
immler@69619
   362
  shows "convex s \<longleftrightarrow>
immler@69619
   363
    (\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> sum u t = 1 \<longrightarrow> sum (\<lambda>x. u x *\<^sub>R x) t \<in> s)"
immler@69619
   364
proof safe
immler@69619
   365
  fix t
immler@69619
   366
  fix u :: "'a \<Rightarrow> real"
immler@69619
   367
  assume "convex s"
immler@69619
   368
    and "finite t"
immler@69619
   369
    and "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "sum u t = 1"
immler@69619
   370
  then show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
immler@69619
   371
    using convex_sum[of t s u "\<lambda> x. x"] by auto
immler@69619
   372
next
immler@69619
   373
  assume *: "\<forall>t. \<forall> u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and>
immler@69619
   374
    sum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
immler@69619
   375
  show "convex s"
immler@69619
   376
    unfolding convex_alt
immler@69619
   377
  proof safe
immler@69619
   378
    fix x y
immler@69619
   379
    fix \<mu> :: real
immler@69619
   380
    assume **: "x \<in> s" "y \<in> s" "0 \<le> \<mu>" "\<mu> \<le> 1"
immler@69619
   381
    show "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s"
immler@69619
   382
    proof (cases "x = y")
immler@69619
   383
      case False
immler@69619
   384
      then show ?thesis
immler@69619
   385
        using *[rule_format, of "{x, y}" "\<lambda> z. if z = x then 1 - \<mu> else \<mu>"] **
immler@69619
   386
        by auto
immler@69619
   387
    next
immler@69619
   388
      case True
immler@69619
   389
      then show ?thesis
immler@69619
   390
        using *[rule_format, of "{x, y}" "\<lambda> z. 1"] **
immler@69619
   391
        by (auto simp: field_simps real_vector.scale_left_diff_distrib)
immler@69619
   392
    qed
immler@69619
   393
  qed
immler@69619
   394
qed
immler@69619
   395
immler@69619
   396
lemma convex_finite:
immler@69619
   397
  assumes "finite s"
immler@69619
   398
  shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> sum u s = 1 \<longrightarrow> sum (\<lambda>x. u x *\<^sub>R x) s \<in> s)"
immler@69619
   399
  unfolding convex_explicit
immler@69619
   400
  apply safe
immler@69619
   401
  subgoal for u by (erule allE [where x=s], erule allE [where x=u]) auto
immler@69619
   402
  subgoal for t u
immler@69619
   403
  proof -
immler@69619
   404
    have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)"
immler@69619
   405
      by simp
immler@69619
   406
    assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> sum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s"
immler@69619
   407
    assume *: "\<forall>x\<in>t. 0 \<le> u x" "sum u t = 1"
immler@69619
   408
    assume "t \<subseteq> s"
immler@69619
   409
    then have "s \<inter> t = t" by auto
immler@69619
   410
    with sum[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]] * show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
immler@69619
   411
      by (auto simp: assms sum.If_cases if_distrib if_distrib_arg)
immler@69619
   412
  qed
immler@69619
   413
  done
immler@69619
   414
immler@69619
   415
immler@69619
   416
subsection \<open>Functions that are convex on a set\<close>
immler@69619
   417
immler@69619
   418
definition%important convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
immler@69619
   419
  where "convex_on s f \<longleftrightarrow>
immler@69619
   420
    (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
immler@69619
   421
immler@69619
   422
lemma convex_onI [intro?]:
immler@69619
   423
  assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
immler@69619
   424
    f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
immler@69619
   425
  shows "convex_on A f"
immler@69619
   426
  unfolding convex_on_def
immler@69619
   427
proof clarify
immler@69619
   428
  fix x y
immler@69619
   429
  fix u v :: real
immler@69619
   430
  assume A: "x \<in> A" "y \<in> A" "u \<ge> 0" "v \<ge> 0" "u + v = 1"
immler@69619
   431
  from A(5) have [simp]: "v = 1 - u"
immler@69619
   432
    by (simp add: algebra_simps)
immler@69619
   433
  from A(1-4) show "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y"
immler@69619
   434
    using assms[of u y x]
immler@69619
   435
    by (cases "u = 0 \<or> u = 1") (auto simp: algebra_simps)
immler@69619
   436
qed
immler@69619
   437
immler@69619
   438
lemma convex_on_linorderI [intro?]:
immler@69619
   439
  fixes A :: "('a::{linorder,real_vector}) set"
immler@69619
   440
  assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x < y \<Longrightarrow>
immler@69619
   441
    f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
immler@69619
   442
  shows "convex_on A f"
immler@69619
   443
proof
immler@69619
   444
  fix x y
immler@69619
   445
  fix t :: real
immler@69619
   446
  assume A: "x \<in> A" "y \<in> A" "t > 0" "t < 1"
immler@69619
   447
  with assms [of t x y] assms [of "1 - t" y x]
immler@69619
   448
  show "f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
immler@69619
   449
    by (cases x y rule: linorder_cases) (auto simp: algebra_simps)
immler@69619
   450
qed
immler@69619
   451
immler@69619
   452
lemma convex_onD:
immler@69619
   453
  assumes "convex_on A f"
immler@69619
   454
  shows "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
immler@69619
   455
    f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
immler@69619
   456
  using assms by (auto simp: convex_on_def)
immler@69619
   457
immler@69619
   458
lemma convex_onD_Icc:
immler@69619
   459
  assumes "convex_on {x..y} f" "x \<le> (y :: _ :: {real_vector,preorder})"
immler@69619
   460
  shows "\<And>t. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow>
immler@69619
   461
    f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
immler@69619
   462
  using assms(2) by (intro convex_onD [OF assms(1)]) simp_all
immler@69619
   463
immler@69619
   464
lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
immler@69619
   465
  unfolding convex_on_def by auto
immler@69619
   466
immler@69619
   467
lemma convex_on_add [intro]:
immler@69619
   468
  assumes "convex_on s f"
immler@69619
   469
    and "convex_on s g"
immler@69619
   470
  shows "convex_on s (\<lambda>x. f x + g x)"
immler@69619
   471
proof -
immler@69619
   472
  {
immler@69619
   473
    fix x y
immler@69619
   474
    assume "x \<in> s" "y \<in> s"
immler@69619
   475
    moreover
immler@69619
   476
    fix u v :: real
immler@69619
   477
    assume "0 \<le> u" "0 \<le> v" "u + v = 1"
immler@69619
   478
    ultimately
immler@69619
   479
    have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> (u * f x + v * f y) + (u * g x + v * g y)"
immler@69619
   480
      using assms unfolding convex_on_def by (auto simp: add_mono)
immler@69619
   481
    then have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \<le> u * (f x + g x) + v * (f y + g y)"
immler@69619
   482
      by (simp add: field_simps)
immler@69619
   483
  }
immler@69619
   484
  then show ?thesis
immler@69619
   485
    unfolding convex_on_def by auto
immler@69619
   486
qed
immler@69619
   487
immler@69619
   488
lemma convex_on_cmul [intro]:
immler@69619
   489
  fixes c :: real
immler@69619
   490
  assumes "0 \<le> c"
immler@69619
   491
    and "convex_on s f"
immler@69619
   492
  shows "convex_on s (\<lambda>x. c * f x)"
immler@69619
   493
proof -
immler@69619
   494
  have *: "u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)"
immler@69619
   495
    for u c fx v fy :: real
immler@69619
   496
    by (simp add: field_simps)
immler@69619
   497
  show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)]
immler@69619
   498
    unfolding convex_on_def and * by auto
immler@69619
   499
qed
immler@69619
   500
immler@69619
   501
lemma convex_lower:
immler@69619
   502
  assumes "convex_on s f"
immler@69619
   503
    and "x \<in> s"
immler@69619
   504
    and "y \<in> s"
immler@69619
   505
    and "0 \<le> u"
immler@69619
   506
    and "0 \<le> v"
immler@69619
   507
    and "u + v = 1"
immler@69619
   508
  shows "f (u *\<^sub>R x + v *\<^sub>R y) \<le> max (f x) (f y)"
immler@69619
   509
proof -
immler@69619
   510
  let ?m = "max (f x) (f y)"
immler@69619
   511
  have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
immler@69619
   512
    using assms(4,5) by (auto simp: mult_left_mono add_mono)
immler@69619
   513
  also have "\<dots> = max (f x) (f y)"
immler@69619
   514
    using assms(6) by (simp add: distrib_right [symmetric])
immler@69619
   515
  finally show ?thesis
immler@69619
   516
    using assms unfolding convex_on_def by fastforce
immler@69619
   517
qed
immler@69619
   518
immler@69619
   519
lemma convex_on_dist [intro]:
immler@69619
   520
  fixes s :: "'a::real_normed_vector set"
immler@69619
   521
  shows "convex_on s (\<lambda>x. dist a x)"
immler@69619
   522
proof (auto simp: convex_on_def dist_norm)
immler@69619
   523
  fix x y
immler@69619
   524
  assume "x \<in> s" "y \<in> s"
immler@69619
   525
  fix u v :: real
immler@69619
   526
  assume "0 \<le> u"
immler@69619
   527
  assume "0 \<le> v"
immler@69619
   528
  assume "u + v = 1"
immler@69619
   529
  have "a = u *\<^sub>R a + v *\<^sub>R a"
immler@69619
   530
    unfolding scaleR_left_distrib[symmetric] and \<open>u + v = 1\<close> by simp
immler@69619
   531
  then have *: "a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))"
immler@69619
   532
    by (auto simp: algebra_simps)
immler@69619
   533
  show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)"
immler@69619
   534
    unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"]
immler@69619
   535
    using \<open>0 \<le> u\<close> \<open>0 \<le> v\<close> by auto
immler@69619
   536
qed
immler@69619
   537
immler@69619
   538
immler@69619
   539
subsection%unimportant \<open>Arithmetic operations on sets preserve convexity\<close>
immler@69619
   540
immler@69619
   541
lemma convex_linear_image:
immler@69619
   542
  assumes "linear f"
immler@69619
   543
    and "convex s"
immler@69619
   544
  shows "convex (f ` s)"
immler@69619
   545
proof -
immler@69619
   546
  interpret f: linear f by fact
immler@69619
   547
  from \<open>convex s\<close> show "convex (f ` s)"
immler@69619
   548
    by (simp add: convex_def f.scaleR [symmetric] f.add [symmetric])
immler@69619
   549
qed
immler@69619
   550
immler@69619
   551
lemma convex_linear_vimage:
immler@69619
   552
  assumes "linear f"
immler@69619
   553
    and "convex s"
immler@69619
   554
  shows "convex (f -` s)"
immler@69619
   555
proof -
immler@69619
   556
  interpret f: linear f by fact
immler@69619
   557
  from \<open>convex s\<close> show "convex (f -` s)"
immler@69619
   558
    by (simp add: convex_def f.add f.scaleR)
immler@69619
   559
qed
immler@69619
   560
immler@69619
   561
lemma convex_scaling:
immler@69619
   562
  assumes "convex s"
immler@69619
   563
  shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)"
immler@69619
   564
proof -
immler@69619
   565
  have "linear (\<lambda>x. c *\<^sub>R x)"
immler@69619
   566
    by (simp add: linearI scaleR_add_right)
immler@69619
   567
  then show ?thesis
immler@69619
   568
    using \<open>convex s\<close> by (rule convex_linear_image)
immler@69619
   569
qed
immler@69619
   570
immler@69619
   571
lemma convex_scaled:
immler@69619
   572
  assumes "convex S"
immler@69619
   573
  shows "convex ((\<lambda>x. x *\<^sub>R c) ` S)"
immler@69619
   574
proof -
immler@69619
   575
  have "linear (\<lambda>x. x *\<^sub>R c)"
immler@69619
   576
    by (simp add: linearI scaleR_add_left)
immler@69619
   577
  then show ?thesis
immler@69619
   578
    using \<open>convex S\<close> by (rule convex_linear_image)
immler@69619
   579
qed
immler@69619
   580
immler@69619
   581
lemma convex_negations:
immler@69619
   582
  assumes "convex S"
immler@69619
   583
  shows "convex ((\<lambda>x. - x) ` S)"
immler@69619
   584
proof -
immler@69619
   585
  have "linear (\<lambda>x. - x)"
immler@69619
   586
    by (simp add: linearI)
immler@69619
   587
  then show ?thesis
immler@69619
   588
    using \<open>convex S\<close> by (rule convex_linear_image)
immler@69619
   589
qed
immler@69619
   590
immler@69619
   591
lemma convex_sums:
immler@69619
   592
  assumes "convex S"
immler@69619
   593
    and "convex T"
immler@69619
   594
  shows "convex (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
immler@69619
   595
proof -
immler@69619
   596
  have "linear (\<lambda>(x, y). x + y)"
immler@69619
   597
    by (auto intro: linearI simp: scaleR_add_right)
immler@69619
   598
  with assms have "convex ((\<lambda>(x, y). x + y) ` (S \<times> T))"
immler@69619
   599
    by (intro convex_linear_image convex_Times)
immler@69619
   600
  also have "((\<lambda>(x, y). x + y) ` (S \<times> T)) = (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
immler@69619
   601
    by auto
immler@69619
   602
  finally show ?thesis .
immler@69619
   603
qed
immler@69619
   604
immler@69619
   605
lemma convex_differences:
immler@69619
   606
  assumes "convex S" "convex T"
immler@69619
   607
  shows "convex (\<Union>x\<in> S. \<Union>y \<in> T. {x - y})"
immler@69619
   608
proof -
immler@69619
   609
  have "{x - y| x y. x \<in> S \<and> y \<in> T} = {x + y |x y. x \<in> S \<and> y \<in> uminus ` T}"
immler@69619
   610
    by (auto simp: diff_conv_add_uminus simp del: add_uminus_conv_diff)
immler@69619
   611
  then show ?thesis
immler@69619
   612
    using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto
immler@69619
   613
qed
immler@69619
   614
immler@69619
   615
lemma convex_translation:
immler@69619
   616
  assumes "convex S"
immler@69619
   617
  shows "convex ((\<lambda>x. a + x) ` S)"
immler@69619
   618
proof -
immler@69619
   619
  have "(\<Union> x\<in> {a}. \<Union>y \<in> S. {x + y}) = (\<lambda>x. a + x) ` S"
immler@69619
   620
    by auto
immler@69619
   621
  then show ?thesis
immler@69619
   622
    using convex_sums[OF convex_singleton[of a] assms] by auto
immler@69619
   623
qed
immler@69619
   624
immler@69619
   625
lemma convex_affinity:
immler@69619
   626
  assumes "convex S"
immler@69619
   627
  shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` S)"
immler@69619
   628
proof -
immler@69619
   629
  have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` (*\<^sub>R) c ` S"
immler@69619
   630
    by auto
immler@69619
   631
  then show ?thesis
immler@69619
   632
    using convex_translation[OF convex_scaling[OF assms], of a c] by auto
immler@69619
   633
qed
immler@69619
   634
immler@69619
   635
lemma pos_is_convex: "convex {0 :: real <..}"
immler@69619
   636
  unfolding convex_alt
immler@69619
   637
proof safe
immler@69619
   638
  fix y x \<mu> :: real
immler@69619
   639
  assume *: "y > 0" "x > 0" "\<mu> \<ge> 0" "\<mu> \<le> 1"
immler@69619
   640
  {
immler@69619
   641
    assume "\<mu> = 0"
immler@69619
   642
    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y = y"
immler@69619
   643
      by simp
immler@69619
   644
    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
immler@69619
   645
      using * by simp
immler@69619
   646
  }
immler@69619
   647
  moreover
immler@69619
   648
  {
immler@69619
   649
    assume "\<mu> = 1"
immler@69619
   650
    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
immler@69619
   651
      using * by simp
immler@69619
   652
  }
immler@69619
   653
  moreover
immler@69619
   654
  {
immler@69619
   655
    assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
immler@69619
   656
    then have "\<mu> > 0" "(1 - \<mu>) > 0"
immler@69619
   657
      using * by auto
immler@69619
   658
    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
immler@69619
   659
      using * by (auto simp: add_pos_pos)
immler@69619
   660
  }
immler@69619
   661
  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0"
immler@69619
   662
    by fastforce
immler@69619
   663
qed
immler@69619
   664
immler@69619
   665
lemma convex_on_sum:
immler@69619
   666
  fixes a :: "'a \<Rightarrow> real"
immler@69619
   667
    and y :: "'a \<Rightarrow> 'b::real_vector"
immler@69619
   668
    and f :: "'b \<Rightarrow> real"
immler@69619
   669
  assumes "finite s" "s \<noteq> {}"
immler@69619
   670
    and "convex_on C f"
immler@69619
   671
    and "convex C"
immler@69619
   672
    and "(\<Sum> i \<in> s. a i) = 1"
immler@69619
   673
    and "\<And>i. i \<in> s \<Longrightarrow> a i \<ge> 0"
immler@69619
   674
    and "\<And>i. i \<in> s \<Longrightarrow> y i \<in> C"
immler@69619
   675
  shows "f (\<Sum> i \<in> s. a i *\<^sub>R y i) \<le> (\<Sum> i \<in> s. a i * f (y i))"
immler@69619
   676
  using assms
immler@69619
   677
proof (induct s arbitrary: a rule: finite_ne_induct)
immler@69619
   678
  case (singleton i)
immler@69619
   679
  then have ai: "a i = 1"
immler@69619
   680
    by auto
immler@69619
   681
  then show ?case
immler@69619
   682
    by auto
immler@69619
   683
next
immler@69619
   684
  case (insert i s)
immler@69619
   685
  then have "convex_on C f"
immler@69619
   686
    by simp
immler@69619
   687
  from this[unfolded convex_on_def, rule_format]
immler@69619
   688
  have conv: "\<And>x y \<mu>. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> 0 \<le> \<mu> \<Longrightarrow> \<mu> \<le> 1 \<Longrightarrow>
immler@69619
   689
      f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
immler@69619
   690
    by simp
immler@69619
   691
  show ?case
immler@69619
   692
  proof (cases "a i = 1")
immler@69619
   693
    case True
immler@69619
   694
    then have "(\<Sum> j \<in> s. a j) = 0"
immler@69619
   695
      using insert by auto
immler@69619
   696
    then have "\<And>j. j \<in> s \<Longrightarrow> a j = 0"
immler@69619
   697
      using insert by (fastforce simp: sum_nonneg_eq_0_iff)
immler@69619
   698
    then show ?thesis
immler@69619
   699
      using insert by auto
immler@69619
   700
  next
immler@69619
   701
    case False
immler@69619
   702
    from insert have yai: "y i \<in> C" "a i \<ge> 0"
immler@69619
   703
      by auto
immler@69619
   704
    have fis: "finite (insert i s)"
immler@69619
   705
      using insert by auto
immler@69619
   706
    then have ai1: "a i \<le> 1"
immler@69619
   707
      using sum_nonneg_leq_bound[of "insert i s" a] insert by simp
immler@69619
   708
    then have "a i < 1"
immler@69619
   709
      using False by auto
immler@69619
   710
    then have i0: "1 - a i > 0"
immler@69619
   711
      by auto
immler@69619
   712
    let ?a = "\<lambda>j. a j / (1 - a i)"
immler@69619
   713
    have a_nonneg: "?a j \<ge> 0" if "j \<in> s" for j
immler@69619
   714
      using i0 insert that by fastforce
immler@69619
   715
    have "(\<Sum> j \<in> insert i s. a j) = 1"
immler@69619
   716
      using insert by auto
immler@69619
   717
    then have "(\<Sum> j \<in> s. a j) = 1 - a i"
immler@69619
   718
      using sum.insert insert by fastforce
immler@69619
   719
    then have "(\<Sum> j \<in> s. a j) / (1 - a i) = 1"
immler@69619
   720
      using i0 by auto
immler@69619
   721
    then have a1: "(\<Sum> j \<in> s. ?a j) = 1"
immler@69619
   722
      unfolding sum_divide_distrib by simp
immler@69619
   723
    have "convex C" using insert by auto
immler@69619
   724
    then have asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
immler@69619
   725
      using insert convex_sum [OF \<open>finite s\<close> \<open>convex C\<close> a1 a_nonneg] by auto
immler@69619
   726
    have asum_le: "f (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<le> (\<Sum> j \<in> s. ?a j * f (y j))"
immler@69619
   727
      using a_nonneg a1 insert by blast
immler@69619
   728
    have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) = f ((\<Sum> j \<in> s. a j *\<^sub>R y j) + a i *\<^sub>R y i)"
immler@69619
   729
      using sum.insert[of s i "\<lambda> j. a j *\<^sub>R y j", OF \<open>finite s\<close> \<open>i \<notin> s\<close>] insert
immler@69619
   730
      by (auto simp only: add.commute)
immler@69619
   731
    also have "\<dots> = f (((1 - a i) * inverse (1 - a i)) *\<^sub>R (\<Sum> j \<in> s. a j *\<^sub>R y j) + a i *\<^sub>R y i)"
immler@69619
   732
      using i0 by auto
immler@69619
   733
    also have "\<dots> = f ((1 - a i) *\<^sub>R (\<Sum> j \<in> s. (a j * inverse (1 - a i)) *\<^sub>R y j) + a i *\<^sub>R y i)"
immler@69619
   734
      using scaleR_right.sum[of "inverse (1 - a i)" "\<lambda> j. a j *\<^sub>R y j" s, symmetric]
immler@69619
   735
      by (auto simp: algebra_simps)
immler@69619
   736
    also have "\<dots> = f ((1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) + a i *\<^sub>R y i)"
immler@69619
   737
      by (auto simp: divide_inverse)
immler@69619
   738
    also have "\<dots> \<le> (1 - a i) *\<^sub>R f ((\<Sum> j \<in> s. ?a j *\<^sub>R y j)) + a i * f (y i)"
immler@69619
   739
      using conv[of "y i" "(\<Sum> j \<in> s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1]
immler@69619
   740
      by (auto simp: add.commute)
immler@69619
   741
    also have "\<dots> \<le> (1 - a i) * (\<Sum> j \<in> s. ?a j * f (y j)) + a i * f (y i)"
immler@69619
   742
      using add_right_mono [OF mult_left_mono [of _ _ "1 - a i",
immler@69619
   743
            OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"]
immler@69619
   744
      by simp
immler@69619
   745
    also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
immler@69619
   746
      unfolding sum_distrib_left[of "1 - a i" "\<lambda> j. ?a j * f (y j)"]
immler@69619
   747
      using i0 by auto
immler@69619
   748
    also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)"
immler@69619
   749
      using i0 by auto
immler@69619
   750
    also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))"
immler@69619
   751
      using insert by auto
immler@69619
   752
    finally show ?thesis
immler@69619
   753
      by simp
immler@69619
   754
  qed
immler@69619
   755
qed
immler@69619
   756
immler@69619
   757
lemma convex_on_alt:
immler@69619
   758
  fixes C :: "'a::real_vector set"
immler@69619
   759
  assumes "convex C"
immler@69619
   760
  shows "convex_on C f \<longleftrightarrow>
immler@69619
   761
    (\<forall>x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1 \<longrightarrow>
immler@69619
   762
      f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
immler@69619
   763
proof safe
immler@69619
   764
  fix x y
immler@69619
   765
  fix \<mu> :: real
immler@69619
   766
  assume *: "convex_on C f" "x \<in> C" "y \<in> C" "0 \<le> \<mu>" "\<mu> \<le> 1"
immler@69619
   767
  from this[unfolded convex_on_def, rule_format]
immler@69619
   768
  have "0 \<le> u \<Longrightarrow> 0 \<le> v \<Longrightarrow> u + v = 1 \<Longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" for u v
immler@69619
   769
    by auto
immler@69619
   770
  from this [of "\<mu>" "1 - \<mu>", simplified] *
immler@69619
   771
  show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
immler@69619
   772
    by auto
immler@69619
   773
next
immler@69619
   774
  assume *: "\<forall>x\<in>C. \<forall>y\<in>C. \<forall>\<mu>. 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow>
immler@69619
   775
    f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
immler@69619
   776
  {
immler@69619
   777
    fix x y
immler@69619
   778
    fix u v :: real
immler@69619
   779
    assume **: "x \<in> C" "y \<in> C" "u \<ge> 0" "v \<ge> 0" "u + v = 1"
immler@69619
   780
    then have[simp]: "1 - u = v" by auto
immler@69619
   781
    from *[rule_format, of x y u]
immler@69619
   782
    have "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y"
immler@69619
   783
      using ** by auto
immler@69619
   784
  }
immler@69619
   785
  then show "convex_on C f"
immler@69619
   786
    unfolding convex_on_def by auto
immler@69619
   787
qed
immler@69619
   788
immler@69619
   789
lemma convex_on_diff:
immler@69619
   790
  fixes f :: "real \<Rightarrow> real"
immler@69619
   791
  assumes f: "convex_on I f"
immler@69619
   792
    and I: "x \<in> I" "y \<in> I"
immler@69619
   793
    and t: "x < t" "t < y"
immler@69619
   794
  shows "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
immler@69619
   795
    and "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
immler@69619
   796
proof -
immler@69619
   797
  define a where "a \<equiv> (t - y) / (x - y)"
immler@69619
   798
  with t have "0 \<le> a" "0 \<le> 1 - a"
immler@69619
   799
    by (auto simp: field_simps)
immler@69619
   800
  with f \<open>x \<in> I\<close> \<open>y \<in> I\<close> have cvx: "f (a * x + (1 - a) * y) \<le> a * f x + (1 - a) * f y"
immler@69619
   801
    by (auto simp: convex_on_def)
immler@69619
   802
  have "a * x + (1 - a) * y = a * (x - y) + y"
immler@69619
   803
    by (simp add: field_simps)
immler@69619
   804
  also have "\<dots> = t"
immler@69619
   805
    unfolding a_def using \<open>x < t\<close> \<open>t < y\<close> by simp
immler@69619
   806
  finally have "f t \<le> a * f x + (1 - a) * f y"
immler@69619
   807
    using cvx by simp
immler@69619
   808
  also have "\<dots> = a * (f x - f y) + f y"
immler@69619
   809
    by (simp add: field_simps)
immler@69619
   810
  finally have "f t - f y \<le> a * (f x - f y)"
immler@69619
   811
    by simp
immler@69619
   812
  with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
immler@69619
   813
    by (simp add: le_divide_eq divide_le_eq field_simps a_def)
immler@69619
   814
  with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
immler@69619
   815
    by (simp add: le_divide_eq divide_le_eq field_simps)
immler@69619
   816
qed
immler@69619
   817
immler@69619
   818
lemma pos_convex_function:
immler@69619
   819
  fixes f :: "real \<Rightarrow> real"
immler@69619
   820
  assumes "convex C"
immler@69619
   821
    and leq: "\<And>x y. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
immler@69619
   822
  shows "convex_on C f"
immler@69619
   823
  unfolding convex_on_alt[OF assms(1)]
immler@69619
   824
  using assms
immler@69619
   825
proof safe
immler@69619
   826
  fix x y \<mu> :: real
immler@69619
   827
  let ?x = "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
immler@69619
   828
  assume *: "convex C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
immler@69619
   829
  then have "1 - \<mu> \<ge> 0" by auto
immler@69619
   830
  then have xpos: "?x \<in> C"
immler@69619
   831
    using * unfolding convex_alt by fastforce
immler@69619
   832
  have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x) \<ge>
immler@69619
   833
      \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
immler@69619
   834
    using add_mono [OF mult_left_mono [OF leq [OF xpos *(2)] \<open>\<mu> \<ge> 0\<close>]
immler@69619
   835
        mult_left_mono [OF leq [OF xpos *(3)] \<open>1 - \<mu> \<ge> 0\<close>]]
immler@69619
   836
    by auto
immler@69619
   837
  then have "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
immler@69619
   838
    by (auto simp: field_simps)
immler@69619
   839
  then show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
immler@69619
   840
    using convex_on_alt by auto
immler@69619
   841
qed
immler@69619
   842
immler@69619
   843
lemma atMostAtLeast_subset_convex:
immler@69619
   844
  fixes C :: "real set"
immler@69619
   845
  assumes "convex C"
immler@69619
   846
    and "x \<in> C" "y \<in> C" "x < y"
immler@69619
   847
  shows "{x .. y} \<subseteq> C"
immler@69619
   848
proof safe
immler@69619
   849
  fix z assume z: "z \<in> {x .. y}"
immler@69619
   850
  have less: "z \<in> C" if *: "x < z" "z < y"
immler@69619
   851
  proof -
immler@69619
   852
    let ?\<mu> = "(y - z) / (y - x)"
immler@69619
   853
    have "0 \<le> ?\<mu>" "?\<mu> \<le> 1"
immler@69619
   854
      using assms * by (auto simp: field_simps)
immler@69619
   855
    then have comb: "?\<mu> * x + (1 - ?\<mu>) * y \<in> C"
immler@69619
   856
      using assms iffD1[OF convex_alt, rule_format, of C y x ?\<mu>]
immler@69619
   857
      by (simp add: algebra_simps)
immler@69619
   858
    have "?\<mu> * x + (1 - ?\<mu>) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"
immler@69619
   859
      by (auto simp: field_simps)
immler@69619
   860
    also have "\<dots> = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"
immler@69619
   861
      using assms by (simp only: add_divide_distrib) (auto simp: field_simps)
immler@69619
   862
    also have "\<dots> = z"
immler@69619
   863
      using assms by (auto simp: field_simps)
immler@69619
   864
    finally show ?thesis
immler@69619
   865
      using comb by auto
immler@69619
   866
  qed
immler@69619
   867
  show "z \<in> C"
immler@69619
   868
    using z less assms by (auto simp: le_less)
immler@69619
   869
qed
immler@69619
   870
immler@69619
   871
lemma f''_imp_f':
immler@69619
   872
  fixes f :: "real \<Rightarrow> real"
immler@69619
   873
  assumes "convex C"
immler@69619
   874
    and f': "\<And>x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
immler@69619
   875
    and f'': "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
immler@69619
   876
    and pos: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
immler@69619
   877
    and x: "x \<in> C"
immler@69619
   878
    and y: "y \<in> C"
immler@69619
   879
  shows "f' x * (y - x) \<le> f y - f x"
immler@69619
   880
  using assms
immler@69619
   881
proof -
immler@69619
   882
  have less_imp: "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
immler@69619
   883
    if *: "x \<in> C" "y \<in> C" "y > x" for x y :: real
immler@69619
   884
  proof -
immler@69619
   885
    from * have ge: "y - x > 0" "y - x \<ge> 0"
immler@69619
   886
      by auto
immler@69619
   887
    from * have le: "x - y < 0" "x - y \<le> 0"
immler@69619
   888
      by auto
immler@69619
   889
    then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1"
immler@69619
   890
      using subsetD[OF atMostAtLeast_subset_convex[OF \<open>convex C\<close> \<open>x \<in> C\<close> \<open>y \<in> C\<close> \<open>x < y\<close>],
immler@69619
   891
          THEN f', THEN MVT2[OF \<open>x < y\<close>, rule_format, unfolded atLeastAtMost_iff[symmetric]]]
immler@69619
   892
      by auto
immler@69619
   893
    then have "z1 \<in> C"
immler@69619
   894
      using atMostAtLeast_subset_convex \<open>convex C\<close> \<open>x \<in> C\<close> \<open>y \<in> C\<close> \<open>x < y\<close>
immler@69619
   895
      by fastforce
immler@69619
   896
    from z1 have z1': "f x - f y = (x - y) * f' z1"
immler@69619
   897
      by (simp add: field_simps)
immler@69619
   898
    obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2"
immler@69619
   899
      using subsetD[OF atMostAtLeast_subset_convex[OF \<open>convex C\<close> \<open>x \<in> C\<close> \<open>z1 \<in> C\<close> \<open>x < z1\<close>],
immler@69619
   900
          THEN f'', THEN MVT2[OF \<open>x < z1\<close>, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
immler@69619
   901
      by auto
immler@69619
   902
    obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3"
immler@69619
   903
      using subsetD[OF atMostAtLeast_subset_convex[OF \<open>convex C\<close> \<open>z1 \<in> C\<close> \<open>y \<in> C\<close> \<open>z1 < y\<close>],
immler@69619
   904
          THEN f'', THEN MVT2[OF \<open>z1 < y\<close>, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
immler@69619
   905
      by auto
immler@69619
   906
    have "f' y - (f x - f y) / (x - y) = f' y - f' z1"
immler@69619
   907
      using * z1' by auto
immler@69619
   908
    also have "\<dots> = (y - z1) * f'' z3"
immler@69619
   909
      using z3 by auto
immler@69619
   910
    finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3"
immler@69619
   911
      by simp
immler@69619
   912
    have A': "y - z1 \<ge> 0"
immler@69619
   913
      using z1 by auto
immler@69619
   914
    have "z3 \<in> C"
immler@69619
   915
      using z3 * atMostAtLeast_subset_convex \<open>convex C\<close> \<open>x \<in> C\<close> \<open>z1 \<in> C\<close> \<open>x < z1\<close>
immler@69619
   916
      by fastforce
immler@69619
   917
    then have B': "f'' z3 \<ge> 0"
immler@69619
   918
      using assms by auto
immler@69619
   919
    from A' B' have "(y - z1) * f'' z3 \<ge> 0"
immler@69619
   920
      by auto
immler@69619
   921
    from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0"
immler@69619
   922
      by auto
immler@69619
   923
    from mult_right_mono_neg[OF this le(2)]
immler@69619
   924
    have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
immler@69619
   925
      by (simp add: algebra_simps)
immler@69619
   926
    then have "f' y * (x - y) - (f x - f y) \<le> 0"
immler@69619
   927
      using le by auto
immler@69619
   928
    then have res: "f' y * (x - y) \<le> f x - f y"
immler@69619
   929
      by auto
immler@69619
   930
    have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
immler@69619
   931
      using * z1 by auto
immler@69619
   932
    also have "\<dots> = (z1 - x) * f'' z2"
immler@69619
   933
      using z2 by auto
immler@69619
   934
    finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2"
immler@69619
   935
      by simp
immler@69619
   936
    have A: "z1 - x \<ge> 0"
immler@69619
   937
      using z1 by auto
immler@69619
   938
    have "z2 \<in> C"
immler@69619
   939
      using z2 z1 * atMostAtLeast_subset_convex \<open>convex C\<close> \<open>z1 \<in> C\<close> \<open>y \<in> C\<close> \<open>z1 < y\<close>
immler@69619
   940
      by fastforce
immler@69619
   941
    then have B: "f'' z2 \<ge> 0"
immler@69619
   942
      using assms by auto
immler@69619
   943
    from A B have "(z1 - x) * f'' z2 \<ge> 0"
immler@69619
   944
      by auto
immler@69619
   945
    with cool have "(f y - f x) / (y - x) - f' x \<ge> 0"
immler@69619
   946
      by auto
immler@69619
   947
    from mult_right_mono[OF this ge(2)]
immler@69619
   948
    have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
immler@69619
   949
      by (simp add: algebra_simps)
immler@69619
   950
    then have "f y - f x - f' x * (y - x) \<ge> 0"
immler@69619
   951
      using ge by auto
immler@69619
   952
    then show "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
immler@69619
   953
      using res by auto
immler@69619
   954
  qed
immler@69619
   955
  show ?thesis
immler@69619
   956
  proof (cases "x = y")
immler@69619
   957
    case True
immler@69619
   958
    with x y show ?thesis by auto
immler@69619
   959
  next
immler@69619
   960
    case False
immler@69619
   961
    with less_imp x y show ?thesis
immler@69619
   962
      by (auto simp: neq_iff)
immler@69619
   963
  qed
immler@69619
   964
qed
immler@69619
   965
immler@69619
   966
lemma f''_ge0_imp_convex:
immler@69619
   967
  fixes f :: "real \<Rightarrow> real"
immler@69619
   968
  assumes conv: "convex C"
immler@69619
   969
    and f': "\<And>x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
immler@69619
   970
    and f'': "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
immler@69619
   971
    and pos: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
immler@69619
   972
  shows "convex_on C f"
immler@69619
   973
  using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function
immler@69619
   974
  by fastforce
immler@69619
   975
immler@69619
   976
lemma minus_log_convex:
immler@69619
   977
  fixes b :: real
immler@69619
   978
  assumes "b > 1"
immler@69619
   979
  shows "convex_on {0 <..} (\<lambda> x. - log b x)"
immler@69619
   980
proof -
immler@69619
   981
  have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)"
immler@69619
   982
    using DERIV_log by auto
immler@69619
   983
  then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
immler@69619
   984
    by (auto simp: DERIV_minus)
immler@69619
   985
  have "\<And>z::real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
immler@69619
   986
    using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
immler@69619
   987
  from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
immler@69619
   988
  have "\<And>z::real. z > 0 \<Longrightarrow>
immler@69619
   989
    DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
immler@69619
   990
    by auto
immler@69619
   991
  then have f''0: "\<And>z::real. z > 0 \<Longrightarrow>
immler@69619
   992
    DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
immler@69619
   993
    unfolding inverse_eq_divide by (auto simp: mult.assoc)
immler@69619
   994
  have f''_ge0: "\<And>z::real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
immler@69619
   995
    using \<open>b > 1\<close> by (auto intro!: less_imp_le)
immler@69619
   996
  from f''_ge0_imp_convex[OF pos_is_convex, unfolded greaterThan_iff, OF f' f''0 f''_ge0]
immler@69619
   997
  show ?thesis
immler@69619
   998
    by auto
immler@69619
   999
qed
immler@69619
  1000
immler@69619
  1001
immler@69619
  1002
subsection%unimportant \<open>Convexity of real functions\<close>
immler@69619
  1003
immler@69619
  1004
lemma convex_on_realI:
immler@69619
  1005
  assumes "connected A"
immler@69619
  1006
    and "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
immler@69619
  1007
    and "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f' x \<le> f' y"
immler@69619
  1008
  shows "convex_on A f"
immler@69619
  1009
proof (rule convex_on_linorderI)
immler@69619
  1010
  fix t x y :: real
immler@69619
  1011
  assume t: "t > 0" "t < 1"
immler@69619
  1012
  assume xy: "x \<in> A" "y \<in> A" "x < y"
immler@69619
  1013
  define z where "z = (1 - t) * x + t * y"
immler@69619
  1014
  with \<open>connected A\<close> and xy have ivl: "{x..y} \<subseteq> A"
immler@69619
  1015
    using connected_contains_Icc by blast
immler@69619
  1016
immler@69619
  1017
  from xy t have xz: "z > x"
immler@69619
  1018
    by (simp add: z_def algebra_simps)
immler@69619
  1019
  have "y - z = (1 - t) * (y - x)"
immler@69619
  1020
    by (simp add: z_def algebra_simps)
immler@69619
  1021
  also from xy t have "\<dots> > 0"
immler@69619
  1022
    by (intro mult_pos_pos) simp_all
immler@69619
  1023
  finally have yz: "z < y"
immler@69619
  1024
    by simp
immler@69619
  1025
immler@69619
  1026
  from assms xz yz ivl t have "\<exists>\<xi>. \<xi> > x \<and> \<xi> < z \<and> f z - f x = (z - x) * f' \<xi>"
immler@69619
  1027
    by (intro MVT2) (auto intro!: assms(2))
immler@69619
  1028
  then obtain \<xi> where \<xi>: "\<xi> > x" "\<xi> < z" "f' \<xi> = (f z - f x) / (z - x)"
immler@69619
  1029
    by auto
immler@69619
  1030
  from assms xz yz ivl t have "\<exists>\<eta>. \<eta> > z \<and> \<eta> < y \<and> f y - f z = (y - z) * f' \<eta>"
immler@69619
  1031
    by (intro MVT2) (auto intro!: assms(2))
immler@69619
  1032
  then obtain \<eta> where \<eta>: "\<eta> > z" "\<eta> < y" "f' \<eta> = (f y - f z) / (y - z)"
immler@69619
  1033
    by auto
immler@69619
  1034
immler@69619
  1035
  from \<eta>(3) have "(f y - f z) / (y - z) = f' \<eta>" ..
immler@69619
  1036
  also from \<xi> \<eta> ivl have "\<xi> \<in> A" "\<eta> \<in> A"
immler@69619
  1037
    by auto
immler@69619
  1038
  with \<xi> \<eta> have "f' \<eta> \<ge> f' \<xi>"
immler@69619
  1039
    by (intro assms(3)) auto
immler@69619
  1040
  also from \<xi>(3) have "f' \<xi> = (f z - f x) / (z - x)" .
immler@69619
  1041
  finally have "(f y - f z) * (z - x) \<ge> (f z - f x) * (y - z)"
immler@69619
  1042
    using xz yz by (simp add: field_simps)
immler@69619
  1043
  also have "z - x = t * (y - x)"
immler@69619
  1044
    by (simp add: z_def algebra_simps)
immler@69619
  1045
  also have "y - z = (1 - t) * (y - x)"
immler@69619
  1046
    by (simp add: z_def algebra_simps)
immler@69619
  1047
  finally have "(f y - f z) * t \<ge> (f z - f x) * (1 - t)"
immler@69619
  1048
    using xy by simp
immler@69619
  1049
  then show "(1 - t) * f x + t * f y \<ge> f ((1 - t) *\<^sub>R x + t *\<^sub>R y)"
immler@69619
  1050
    by (simp add: z_def algebra_simps)
immler@69619
  1051
qed
immler@69619
  1052
immler@69619
  1053
lemma convex_on_inverse:
immler@69619
  1054
  assumes "A \<subseteq> {0<..}"
immler@69619
  1055
  shows "convex_on A (inverse :: real \<Rightarrow> real)"
immler@69619
  1056
proof (rule convex_on_subset[OF _ assms], intro convex_on_realI[of _ _ "\<lambda>x. -inverse (x^2)"])
immler@69619
  1057
  fix u v :: real
immler@69619
  1058
  assume "u \<in> {0<..}" "v \<in> {0<..}" "u \<le> v"
immler@69619
  1059
  with assms show "-inverse (u^2) \<le> -inverse (v^2)"
immler@69619
  1060
    by (intro le_imp_neg_le le_imp_inverse_le power_mono) (simp_all)
immler@69619
  1061
qed (insert assms, auto intro!: derivative_eq_intros simp: divide_simps power2_eq_square)
immler@69619
  1062
immler@69619
  1063
lemma convex_onD_Icc':
immler@69619
  1064
  assumes "convex_on {x..y} f" "c \<in> {x..y}"
immler@69619
  1065
  defines "d \<equiv> y - x"
immler@69619
  1066
  shows "f c \<le> (f y - f x) / d * (c - x) + f x"
immler@69619
  1067
proof (cases x y rule: linorder_cases)
immler@69619
  1068
  case less
immler@69619
  1069
  then have d: "d > 0"
immler@69619
  1070
    by (simp add: d_def)
immler@69619
  1071
  from assms(2) less have A: "0 \<le> (c - x) / d" "(c - x) / d \<le> 1"
immler@69619
  1072
    by (simp_all add: d_def divide_simps)
immler@69619
  1073
  have "f c = f (x + (c - x) * 1)"
immler@69619
  1074
    by simp
immler@69619
  1075
  also from less have "1 = ((y - x) / d)"
immler@69619
  1076
    by (simp add: d_def)
immler@69619
  1077
  also from d have "x + (c - x) * \<dots> = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y"
immler@69619
  1078
    by (simp add: field_simps)
immler@69619
  1079
  also have "f \<dots> \<le> (1 - (c - x) / d) * f x + (c - x) / d * f y"
immler@69619
  1080
    using assms less by (intro convex_onD_Icc) simp_all
immler@69619
  1081
  also from d have "\<dots> = (f y - f x) / d * (c - x) + f x"
immler@69619
  1082
    by (simp add: field_simps)
immler@69619
  1083
  finally show ?thesis .
immler@69619
  1084
qed (insert assms(2), simp_all)
immler@69619
  1085
immler@69619
  1086
lemma convex_onD_Icc'':
immler@69619
  1087
  assumes "convex_on {x..y} f" "c \<in> {x..y}"
immler@69619
  1088
  defines "d \<equiv> y - x"
immler@69619
  1089
  shows "f c \<le> (f x - f y) / d * (y - c) + f y"
immler@69619
  1090
proof (cases x y rule: linorder_cases)
immler@69619
  1091
  case less
immler@69619
  1092
  then have d: "d > 0"
immler@69619
  1093
    by (simp add: d_def)
immler@69619
  1094
  from assms(2) less have A: "0 \<le> (y - c) / d" "(y - c) / d \<le> 1"
immler@69619
  1095
    by (simp_all add: d_def divide_simps)
immler@69619
  1096
  have "f c = f (y - (y - c) * 1)"
immler@69619
  1097
    by simp
immler@69619
  1098
  also from less have "1 = ((y - x) / d)"
immler@69619
  1099
    by (simp add: d_def)
immler@69619
  1100
  also from d have "y - (y - c) * \<dots> = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y"
immler@69619
  1101
    by (simp add: field_simps)
immler@69619
  1102
  also have "f \<dots> \<le> (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y"
immler@69619
  1103
    using assms less by (intro convex_onD_Icc) (simp_all add: field_simps)
immler@69619
  1104
  also from d have "\<dots> = (f x - f y) / d * (y - c) + f y"
immler@69619
  1105
    by (simp add: field_simps)
immler@69619
  1106
  finally show ?thesis .
immler@69619
  1107
qed (insert assms(2), simp_all)
immler@69619
  1108
immler@69619
  1109
lemma convex_translation_eq [simp]: "convex ((\<lambda>x. a + x) ` s) \<longleftrightarrow> convex s"
immler@69619
  1110
  by (metis convex_translation translation_galois)
immler@69619
  1111
immler@69619
  1112
lemma convex_linear_image_eq [simp]:
immler@69619
  1113
    fixes f :: "'a::real_vector \<Rightarrow> 'b::real_vector"
immler@69619
  1114
    shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> convex (f ` s) \<longleftrightarrow> convex s"
immler@69619
  1115
    by (metis (no_types) convex_linear_image convex_linear_vimage inj_vimage_image_eq)
immler@69619
  1116
immler@69619
  1117
lemma fst_linear: "linear fst"
immler@69619
  1118
  unfolding linear_iff by (simp add: algebra_simps)
immler@69619
  1119
immler@69619
  1120
lemma snd_linear: "linear snd"
immler@69619
  1121
  unfolding linear_iff by (simp add: algebra_simps)
immler@69619
  1122
immler@69619
  1123
lemma fst_snd_linear: "linear (\<lambda>(x,y). x + y)"
immler@69619
  1124
  unfolding linear_iff by (simp add: algebra_simps)
immler@69619
  1125
immler@69619
  1126
lemma vector_choose_size:
immler@69619
  1127
  assumes "0 \<le> c"
immler@69619
  1128
  obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c"
immler@69619
  1129
proof -
immler@69619
  1130
  obtain a::'a where "a \<noteq> 0"
immler@69619
  1131
    using UNIV_not_singleton UNIV_eq_I set_zero singletonI by fastforce
immler@69619
  1132
  then show ?thesis
immler@69619
  1133
    by (rule_tac x="scaleR (c / norm a) a" in that) (simp add: assms)
immler@69619
  1134
qed
immler@69619
  1135
immler@69619
  1136
lemma vector_choose_dist:
immler@69619
  1137
  assumes "0 \<le> c"
immler@69619
  1138
  obtains y :: "'a::{real_normed_vector, perfect_space}" where "dist x y = c"
immler@69619
  1139
by (metis add_diff_cancel_left' assms dist_commute dist_norm vector_choose_size)
immler@69619
  1140
immler@69619
  1141
lemma sum_delta_notmem:
immler@69619
  1142
  assumes "x \<notin> s"
immler@69619
  1143
  shows "sum (\<lambda>y. if (y = x) then P x else Q y) s = sum Q s"
immler@69619
  1144
    and "sum (\<lambda>y. if (x = y) then P x else Q y) s = sum Q s"
immler@69619
  1145
    and "sum (\<lambda>y. if (y = x) then P y else Q y) s = sum Q s"
immler@69619
  1146
    and "sum (\<lambda>y. if (x = y) then P y else Q y) s = sum Q s"
immler@69619
  1147
  apply (rule_tac [!] sum.cong)
immler@69619
  1148
  using assms
immler@69619
  1149
  apply auto
immler@69619
  1150
  done
immler@69619
  1151
immler@69619
  1152
lemma sum_delta'':
immler@69619
  1153
  fixes s::"'a::real_vector set"
immler@69619
  1154
  assumes "finite s"
immler@69619
  1155
  shows "(\<Sum>x\<in>s. (if y = x then f x else 0) *\<^sub>R x) = (if y\<in>s then (f y) *\<^sub>R y else 0)"
immler@69619
  1156
proof -
immler@69619
  1157
  have *: "\<And>x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)"
immler@69619
  1158
    by auto
immler@69619
  1159
  show ?thesis
immler@69619
  1160
    unfolding * using sum.delta[OF assms, of y "\<lambda>x. f x *\<^sub>R x"] by auto
immler@69619
  1161
qed
immler@69619
  1162
immler@69619
  1163
lemma if_smult: "(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)"
immler@69619
  1164
  by (fact if_distrib)
immler@69619
  1165
immler@69619
  1166
lemma dist_triangle_eq:
immler@69619
  1167
  fixes x y z :: "'a::real_inner"
immler@69619
  1168
  shows "dist x z = dist x y + dist y z \<longleftrightarrow>
immler@69619
  1169
    norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
immler@69619
  1170
proof -
immler@69619
  1171
  have *: "x - y + (y - z) = x - z" by auto
immler@69619
  1172
  show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
immler@69619
  1173
    by (auto simp:norm_minus_commute)
immler@69619
  1174
qed
immler@69619
  1175
immler@69619
  1176
immler@69619
  1177
subsection \<open>Affine set and affine hull\<close>
immler@69619
  1178
immler@69619
  1179
definition%important affine :: "'a::real_vector set \<Rightarrow> bool"
immler@69619
  1180
  where "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
immler@69619
  1181
immler@69619
  1182
lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
immler@69619
  1183
  unfolding affine_def by (metis eq_diff_eq')
immler@69619
  1184
immler@69619
  1185
lemma affine_empty [iff]: "affine {}"
immler@69619
  1186
  unfolding affine_def by auto
immler@69619
  1187
immler@69619
  1188
lemma affine_sing [iff]: "affine {x}"
immler@69619
  1189
  unfolding affine_alt by (auto simp: scaleR_left_distrib [symmetric])
immler@69619
  1190
immler@69619
  1191
lemma affine_UNIV [iff]: "affine UNIV"
immler@69619
  1192
  unfolding affine_def by auto
immler@69619
  1193
immler@69619
  1194
lemma affine_Inter [intro]: "(\<And>s. s\<in>f \<Longrightarrow> affine s) \<Longrightarrow> affine (\<Inter>f)"
immler@69619
  1195
  unfolding affine_def by auto
immler@69619
  1196
immler@69619
  1197
lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
immler@69619
  1198
  unfolding affine_def by auto
immler@69619
  1199
immler@69619
  1200
lemma affine_scaling: "affine s \<Longrightarrow> affine (image (\<lambda>x. c *\<^sub>R x) s)"
immler@69619
  1201
  apply (clarsimp simp add: affine_def)
immler@69619
  1202
  apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI)
immler@69619
  1203
  apply (auto simp: algebra_simps)
immler@69619
  1204
  done
immler@69619
  1205
immler@69619
  1206
lemma affine_affine_hull [simp]: "affine(affine hull s)"
immler@69619
  1207
  unfolding hull_def
immler@69619
  1208
  using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] by auto
immler@69619
  1209
immler@69619
  1210
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
immler@69619
  1211
  by (metis affine_affine_hull hull_same)
immler@69619
  1212
immler@69619
  1213
lemma affine_hyperplane: "affine {x. a \<bullet> x = b}"
immler@69619
  1214
  by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)
immler@69619
  1215
immler@69619
  1216
immler@69619
  1217
subsubsection%unimportant \<open>Some explicit formulations\<close>
immler@69619
  1218
immler@69619
  1219
text "Formalized by Lars Schewe."
immler@69619
  1220
immler@69619
  1221
lemma affine:
immler@69619
  1222
  fixes V::"'a::real_vector set"
immler@69619
  1223
  shows "affine V \<longleftrightarrow>
immler@69619
  1224
         (\<forall>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> V \<and> sum u S = 1 \<longrightarrow> (\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V)"
immler@69619
  1225
proof -
immler@69619
  1226
  have "u *\<^sub>R x + v *\<^sub>R y \<in> V" if "x \<in> V" "y \<in> V" "u + v = (1::real)"
immler@69619
  1227
    and *: "\<And>S u. \<lbrakk>finite S; S \<noteq> {}; S \<subseteq> V; sum u S = 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V" for x y u v
immler@69619
  1228
  proof (cases "x = y")
immler@69619
  1229
    case True
immler@69619
  1230
    then show ?thesis
immler@69619
  1231
      using that by (metis scaleR_add_left scaleR_one)
immler@69619
  1232
  next
immler@69619
  1233
    case False
immler@69619
  1234
    then show ?thesis
immler@69619
  1235
      using that *[of "{x,y}" "\<lambda>w. if w = x then u else v"] by auto
immler@69619
  1236
  qed
immler@69619
  1237
  moreover have "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V"
immler@69619
  1238
                if *: "\<And>x y u v. \<lbrakk>x\<in>V; y\<in>V; u + v = 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
immler@69619
  1239
                  and "finite S" "S \<noteq> {}" "S \<subseteq> V" "sum u S = 1" for S u
immler@69619
  1240
  proof -
immler@69619
  1241
    define n where "n = card S"
immler@69619
  1242
    consider "card S = 0" | "card S = 1" | "card S = 2" | "card S > 2" by linarith
immler@69619
  1243
    then show "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V"
immler@69619
  1244
    proof cases
immler@69619
  1245
      assume "card S = 1"
immler@69619
  1246
      then obtain a where "S={a}"
immler@69619
  1247
        by (auto simp: card_Suc_eq)
immler@69619
  1248
      then show ?thesis
immler@69619
  1249
        using that by simp
immler@69619
  1250
    next
immler@69619
  1251
      assume "card S = 2"
immler@69619
  1252
      then obtain a b where "S = {a, b}"
immler@69619
  1253
        by (metis Suc_1 card_1_singletonE card_Suc_eq)
immler@69619
  1254
      then show ?thesis
immler@69619
  1255
        using *[of a b] that
immler@69619
  1256
        by (auto simp: sum_clauses(2))
immler@69619
  1257
    next
immler@69619
  1258
      assume "card S > 2"
immler@69619
  1259
      then show ?thesis using that n_def
immler@69619
  1260
      proof (induct n arbitrary: u S)
immler@69619
  1261
        case 0
immler@69619
  1262
        then show ?case by auto
immler@69619
  1263
      next
immler@69619
  1264
        case (Suc n u S)
immler@69619
  1265
        have "sum u S = card S" if "\<not> (\<exists>x\<in>S. u x \<noteq> 1)"
immler@69619
  1266
          using that unfolding card_eq_sum by auto
immler@69619
  1267
        with Suc.prems obtain x where "x \<in> S" and x: "u x \<noteq> 1" by force
immler@69619
  1268
        have c: "card (S - {x}) = card S - 1"
immler@69619
  1269
          by (simp add: Suc.prems(3) \<open>x \<in> S\<close>)
immler@69619
  1270
        have "sum u (S - {x}) = 1 - u x"
immler@69619
  1271
          by (simp add: Suc.prems sum_diff1_ring \<open>x \<in> S\<close>)
immler@69619
  1272
        with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1"
immler@69619
  1273
          by auto
immler@69619
  1274
        have inV: "(\<Sum>y\<in>S - {x}. (inverse (1 - u x) * u y) *\<^sub>R y) \<in> V"
immler@69619
  1275
        proof (cases "card (S - {x}) > 2")
immler@69619
  1276
          case True
immler@69619
  1277
          then have S: "S - {x} \<noteq> {}" "card (S - {x}) = n"
immler@69619
  1278
            using Suc.prems c by force+
immler@69619
  1279
          show ?thesis
immler@69619
  1280
          proof (rule Suc.hyps)
immler@69619
  1281
            show "(\<Sum>a\<in>S - {x}. inverse (1 - u x) * u a) = 1"
immler@69619
  1282
              by (auto simp: eq1 sum_distrib_left[symmetric])
immler@69619
  1283
          qed (use S Suc.prems True in auto)
immler@69619
  1284
        next
immler@69619
  1285
          case False
immler@69619
  1286
          then have "card (S - {x}) = Suc (Suc 0)"
immler@69619
  1287
            using Suc.prems c by auto
immler@69619
  1288
          then obtain a b where ab: "(S - {x}) = {a, b}" "a\<noteq>b"
immler@69619
  1289
            unfolding card_Suc_eq by auto
immler@69619
  1290
          then show ?thesis
immler@69619
  1291
            using eq1 \<open>S \<subseteq> V\<close>
immler@69619
  1292
            by (auto simp: sum_distrib_left distrib_left intro!: Suc.prems(2)[of a b])
immler@69619
  1293
        qed
immler@69619
  1294
        have "u x + (1 - u x) = 1 \<Longrightarrow>
immler@69619
  1295
          u x *\<^sub>R x + (1 - u x) *\<^sub>R ((\<Sum>y\<in>S - {x}. u y *\<^sub>R y) /\<^sub>R (1 - u x)) \<in> V"
immler@69619
  1296
          by (rule Suc.prems) (use \<open>x \<in> S\<close> Suc.prems inV in \<open>auto simp: scaleR_right.sum\<close>)
immler@69619
  1297
        moreover have "(\<Sum>a\<in>S. u a *\<^sub>R a) = u x *\<^sub>R x + (\<Sum>a\<in>S - {x}. u a *\<^sub>R a)"
immler@69619
  1298
          by (meson Suc.prems(3) sum.remove \<open>x \<in> S\<close>)
immler@69619
  1299
        ultimately show "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V"
immler@69619
  1300
          by (simp add: x)
immler@69619
  1301
      qed
immler@69619
  1302
    qed (use \<open>S\<noteq>{}\<close> \<open>finite S\<close> in auto)
immler@69619
  1303
  qed
immler@69619
  1304
  ultimately show ?thesis
immler@69619
  1305
    unfolding affine_def by meson
immler@69619
  1306
qed
immler@69619
  1307
immler@69619
  1308
immler@69619
  1309
lemma affine_hull_explicit:
immler@69619
  1310
  "affine hull p = {y. \<exists>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p \<and> sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
immler@69619
  1311
  (is "_ = ?rhs")
immler@69619
  1312
proof (rule hull_unique)
immler@69619
  1313
  show "p \<subseteq> ?rhs"
immler@69619
  1314
  proof (intro subsetI CollectI exI conjI)
immler@69619
  1315
    show "\<And>x. sum (\<lambda>z. 1) {x} = 1"
immler@69619
  1316
      by auto
immler@69619
  1317
  qed auto
immler@69619
  1318
  show "?rhs \<subseteq> T" if "p \<subseteq> T" "affine T" for T
immler@69619
  1319
    using that unfolding affine by blast
immler@69619
  1320
  show "affine ?rhs"
immler@69619
  1321
    unfolding affine_def
immler@69619
  1322
  proof clarify
immler@69619
  1323
    fix u v :: real and sx ux sy uy
immler@69619
  1324
    assume uv: "u + v = 1"
immler@69619
  1325
      and x: "finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "sum ux sx = (1::real)"
immler@69619
  1326
      and y: "finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "sum uy sy = (1::real)" 
immler@69619
  1327
    have **: "(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy"
immler@69619
  1328
      by auto
immler@69619
  1329
    show "\<exists>S w. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p \<and>
immler@69619
  1330
        sum w S = 1 \<and> (\<Sum>v\<in>S. w v *\<^sub>R v) = u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)"
immler@69619
  1331
    proof (intro exI conjI)
immler@69619
  1332
      show "finite (sx \<union> sy)"
immler@69619
  1333
        using x y by auto
immler@69619
  1334
      show "sum (\<lambda>i. (if i\<in>sx then u * ux i else 0) + (if i\<in>sy then v * uy i else 0)) (sx \<union> sy) = 1"
immler@69619
  1335
        using x y uv
immler@69619
  1336
        by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] sum_distrib_left [symmetric] **)
immler@69619
  1337
      have "(\<Sum>i\<in>sx \<union> sy. ((if i \<in> sx then u * ux i else 0) + (if i \<in> sy then v * uy i else 0)) *\<^sub>R i)
immler@69619
  1338
          = (\<Sum>i\<in>sx. (u * ux i) *\<^sub>R i) + (\<Sum>i\<in>sy. (v * uy i) *\<^sub>R i)"
immler@69619
  1339
        using x y
immler@69619
  1340
        unfolding scaleR_left_distrib scaleR_zero_left if_smult
immler@69619
  1341
        by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric]  **)
immler@69619
  1342
      also have "\<dots> = u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)"
immler@69619
  1343
        unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by blast
immler@69619
  1344
      finally show "(\<Sum>i\<in>sx \<union> sy. ((if i \<in> sx then u * ux i else 0) + (if i \<in> sy then v * uy i else 0)) *\<^sub>R i) 
immler@69619
  1345
                  = u *\<^sub>R (\<Sum>v\<in>sx. ux v *\<^sub>R v) + v *\<^sub>R (\<Sum>v\<in>sy. uy v *\<^sub>R v)" .
immler@69619
  1346
    qed (use x y in auto)
immler@69619
  1347
  qed
immler@69619
  1348
qed
immler@69619
  1349
immler@69619
  1350
lemma affine_hull_finite:
immler@69619
  1351
  assumes "finite S"
immler@69619
  1352
  shows "affine hull S = {y. \<exists>u. sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
immler@69619
  1353
proof -
immler@69619
  1354
  have *: "\<exists>h. sum h S = 1 \<and> (\<Sum>v\<in>S. h v *\<^sub>R v) = x" 
immler@69619
  1355
    if "F \<subseteq> S" "finite F" "F \<noteq> {}" and sum: "sum u F = 1" and x: "(\<Sum>v\<in>F. u v *\<^sub>R v) = x" for x F u
immler@69619
  1356
  proof -
immler@69619
  1357
    have "S \<inter> F = F"
immler@69619
  1358
      using that by auto
immler@69619
  1359
    show ?thesis
immler@69619
  1360
    proof (intro exI conjI)
immler@69619
  1361
      show "(\<Sum>x\<in>S. if x \<in> F then u x else 0) = 1"
immler@69619
  1362
        by (metis (mono_tags, lifting) \<open>S \<inter> F = F\<close> assms sum.inter_restrict sum)
immler@69619
  1363
      show "(\<Sum>v\<in>S. (if v \<in> F then u v else 0) *\<^sub>R v) = x"
immler@69619
  1364
        by (simp add: if_smult cong: if_cong) (metis (no_types) \<open>S \<inter> F = F\<close> assms sum.inter_restrict x)
immler@69619
  1365
    qed
immler@69619
  1366
  qed
immler@69619
  1367
  show ?thesis
immler@69619
  1368
    unfolding affine_hull_explicit using assms
immler@69619
  1369
    by (fastforce dest: *)
immler@69619
  1370
qed
immler@69619
  1371
immler@69619
  1372
immler@69619
  1373
subsubsection%unimportant \<open>Stepping theorems and hence small special cases\<close>
immler@69619
  1374
immler@69619
  1375
lemma affine_hull_empty[simp]: "affine hull {} = {}"
immler@69619
  1376
  by simp
immler@69619
  1377
immler@69619
  1378
lemma affine_hull_finite_step:
immler@69619
  1379
  fixes y :: "'a::real_vector"
immler@69619
  1380
  shows "finite S \<Longrightarrow>
immler@69619
  1381
      (\<exists>u. sum u (insert a S) = w \<and> sum (\<lambda>x. u x *\<^sub>R x) (insert a S) = y) \<longleftrightarrow>
immler@69619
  1382
      (\<exists>v u. sum u S = w - v \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y - v *\<^sub>R a)" (is "_ \<Longrightarrow> ?lhs = ?rhs")
immler@69619
  1383
proof -
immler@69619
  1384
  assume fin: "finite S"
immler@69619
  1385
  show "?lhs = ?rhs"
immler@69619
  1386
  proof
immler@69619
  1387
    assume ?lhs
immler@69619
  1388
    then obtain u where u: "sum u (insert a S) = w \<and> (\<Sum>x\<in>insert a S. u x *\<^sub>R x) = y"
immler@69619
  1389
      by auto
immler@69619
  1390
    show ?rhs
immler@69619
  1391
    proof (cases "a \<in> S")
immler@69619
  1392
      case True
immler@69619
  1393
      then show ?thesis
immler@69619
  1394
        using u by (simp add: insert_absorb) (metis diff_zero real_vector.scale_zero_left)
immler@69619
  1395
    next
immler@69619
  1396
      case False
immler@69619
  1397
      show ?thesis
immler@69619
  1398
        by (rule exI [where x="u a"]) (use u fin False in auto)
immler@69619
  1399
    qed
immler@69619
  1400
  next
immler@69619
  1401
    assume ?rhs
immler@69619
  1402
    then obtain v u where vu: "sum u S = w - v"  "(\<Sum>x\<in>S. u x *\<^sub>R x) = y - v *\<^sub>R a"
immler@69619
  1403
      by auto
immler@69619
  1404
    have *: "\<And>x M. (if x = a then v else M) *\<^sub>R x = (if x = a then v *\<^sub>R x else M *\<^sub>R x)"
immler@69619
  1405
      by auto
immler@69619
  1406
    show ?lhs
immler@69619
  1407
    proof (cases "a \<in> S")
immler@69619
  1408
      case True
immler@69619
  1409
      show ?thesis
immler@69619
  1410
        by (rule exI [where x="\<lambda>x. (if x=a then v else 0) + u x"])
immler@69619
  1411
           (simp add: True scaleR_left_distrib sum.distrib sum_clauses fin vu * cong: if_cong)
immler@69619
  1412
    next
immler@69619
  1413
      case False
immler@69619
  1414
      then show ?thesis
immler@69619
  1415
        apply (rule_tac x="\<lambda>x. if x=a then v else u x" in exI) 
immler@69619
  1416
        apply (simp add: vu sum_clauses(2)[OF fin] *)
immler@69619
  1417
        by (simp add: sum_delta_notmem(3) vu)
immler@69619
  1418
    qed
immler@69619
  1419
  qed
immler@69619
  1420
qed
immler@69619
  1421
immler@69619
  1422
lemma affine_hull_2:
immler@69619
  1423
  fixes a b :: "'a::real_vector"
immler@69619
  1424
  shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}"
immler@69619
  1425
  (is "?lhs = ?rhs")
immler@69619
  1426
proof -
immler@69619
  1427
  have *:
immler@69619
  1428
    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
immler@69619
  1429
    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
immler@69619
  1430
  have "?lhs = {y. \<exists>u. sum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}"
immler@69619
  1431
    using affine_hull_finite[of "{a,b}"] by auto
immler@69619
  1432
  also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}"
immler@69619
  1433
    by (simp add: affine_hull_finite_step[of "{b}" a])
immler@69619
  1434
  also have "\<dots> = ?rhs" unfolding * by auto
immler@69619
  1435
  finally show ?thesis by auto
immler@69619
  1436
qed
immler@69619
  1437
immler@69619
  1438
lemma affine_hull_3:
immler@69619
  1439
  fixes a b c :: "'a::real_vector"
immler@69619
  1440
  shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}"
immler@69619
  1441
proof -
immler@69619
  1442
  have *:
immler@69619
  1443
    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
immler@69619
  1444
    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
immler@69619
  1445
  show ?thesis
immler@69619
  1446
    apply (simp add: affine_hull_finite affine_hull_finite_step)
immler@69619
  1447
    unfolding *
immler@69619
  1448
    apply safe
immler@69619
  1449
     apply (metis add.assoc)
immler@69619
  1450
    apply (rule_tac x=u in exI, force)
immler@69619
  1451
    done
immler@69619
  1452
qed
immler@69619
  1453
immler@69619
  1454
lemma mem_affine:
immler@69619
  1455
  assumes "affine S" "x \<in> S" "y \<in> S" "u + v = 1"
immler@69619
  1456
  shows "u *\<^sub>R x + v *\<^sub>R y \<in> S"
immler@69619
  1457
  using assms affine_def[of S] by auto
immler@69619
  1458
immler@69619
  1459
lemma mem_affine_3:
immler@69619
  1460
  assumes "affine S" "x \<in> S" "y \<in> S" "z \<in> S" "u + v + w = 1"
immler@69619
  1461
  shows "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \<in> S"
immler@69619
  1462
proof -
immler@69619
  1463
  have "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \<in> affine hull {x, y, z}"
immler@69619
  1464
    using affine_hull_3[of x y z] assms by auto
immler@69619
  1465
  moreover
immler@69619
  1466
  have "affine hull {x, y, z} \<subseteq> affine hull S"
immler@69619
  1467
    using hull_mono[of "{x, y, z}" "S"] assms by auto
immler@69619
  1468
  moreover
immler@69619
  1469
  have "affine hull S = S"
immler@69619
  1470
    using assms affine_hull_eq[of S] by auto
immler@69619
  1471
  ultimately show ?thesis by auto
immler@69619
  1472
qed
immler@69619
  1473
immler@69619
  1474
lemma mem_affine_3_minus:
immler@69619
  1475
  assumes "affine S" "x \<in> S" "y \<in> S" "z \<in> S"
immler@69619
  1476
  shows "x + v *\<^sub>R (y-z) \<in> S"
immler@69619
  1477
  using mem_affine_3[of S x y z 1 v "-v"] assms
immler@69619
  1478
  by (simp add: algebra_simps)
immler@69619
  1479
immler@69619
  1480
corollary mem_affine_3_minus2:
immler@69619
  1481
    "\<lbrakk>affine S; x \<in> S; y \<in> S; z \<in> S\<rbrakk> \<Longrightarrow> x - v *\<^sub>R (y-z) \<in> S"
immler@69619
  1482
  by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left)
immler@69619
  1483
immler@69619
  1484
immler@69619
  1485
subsubsection%unimportant \<open>Some relations between affine hull and subspaces\<close>
immler@69619
  1486
immler@69619
  1487
lemma affine_hull_insert_subset_span:
immler@69619
  1488
  "affine hull (insert a S) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> S}}"
immler@69619
  1489
proof -
immler@69619
  1490
  have "\<exists>v T u. x = a + v \<and> (finite T \<and> T \<subseteq> {x - a |x. x \<in> S} \<and> (\<Sum>v\<in>T. u v *\<^sub>R v) = v)"
immler@69619
  1491
    if "finite F" "F \<noteq> {}" "F \<subseteq> insert a S" "sum u F = 1" "(\<Sum>v\<in>F. u v *\<^sub>R v) = x"
immler@69619
  1492
    for x F u
immler@69619
  1493
  proof -
immler@69619
  1494
    have *: "(\<lambda>x. x - a) ` (F - {a}) \<subseteq> {x - a |x. x \<in> S}"
immler@69619
  1495
      using that by auto
immler@69619
  1496
    show ?thesis
immler@69619
  1497
    proof (intro exI conjI)
immler@69619
  1498
      show "finite ((\<lambda>x. x - a) ` (F - {a}))"
immler@69619
  1499
        by (simp add: that(1))
immler@69619
  1500
      show "(\<Sum>v\<in>(\<lambda>x. x - a) ` (F - {a}). u(v+a) *\<^sub>R v) = x-a"
immler@69619
  1501
        by (simp add: sum.reindex[unfolded inj_on_def] algebra_simps
immler@69619
  1502
            sum_subtractf scaleR_left.sum[symmetric] sum_diff1 that)
immler@69619
  1503
    qed (use \<open>F \<subseteq> insert a S\<close> in auto)
immler@69619
  1504
  qed
immler@69619
  1505
  then show ?thesis
immler@69619
  1506
    unfolding affine_hull_explicit span_explicit by blast
immler@69619
  1507
qed
immler@69619
  1508
immler@69619
  1509
lemma affine_hull_insert_span:
immler@69619
  1510
  assumes "a \<notin> S"
immler@69619
  1511
  shows "affine hull (insert a S) = {a + v | v . v \<in> span {x - a | x.  x \<in> S}}"
immler@69619
  1512
proof -
immler@69619
  1513
  have *: "\<exists>G u. finite G \<and> G \<noteq> {} \<and> G \<subseteq> insert a S \<and> sum u G = 1 \<and> (\<Sum>v\<in>G. u v *\<^sub>R v) = y"
immler@69619
  1514
    if "v \<in> span {x - a |x. x \<in> S}" "y = a + v" for y v
immler@69619
  1515
  proof -
immler@69619
  1516
    from that
immler@69619
  1517
    obtain T u where u: "finite T" "T \<subseteq> {x - a |x. x \<in> S}" "a + (\<Sum>v\<in>T. u v *\<^sub>R v) = y"
immler@69619
  1518
      unfolding span_explicit by auto
immler@69619
  1519
    define F where "F = (\<lambda>x. x + a) ` T"
immler@69619
  1520
    have F: "finite F" "F \<subseteq> S" "(\<Sum>v\<in>F. u (v - a) *\<^sub>R (v - a)) = y - a"
immler@69619
  1521
      unfolding F_def using u by (auto simp: sum.reindex[unfolded inj_on_def])
immler@69619
  1522
    have *: "F \<inter> {a} = {}" "F \<inter> - {a} = F"
immler@69619
  1523
      using F assms by auto
immler@69619
  1524
    show "\<exists>G u. finite G \<and> G \<noteq> {} \<and> G \<subseteq> insert a S \<and> sum u G = 1 \<and> (\<Sum>v\<in>G. u v *\<^sub>R v) = y"
immler@69619
  1525
      apply (rule_tac x = "insert a F" in exI)
immler@69619
  1526
      apply (rule_tac x = "\<lambda>x. if x=a then 1 - sum (\<lambda>x. u (x - a)) F else u (x - a)" in exI)
immler@69619
  1527
      using assms F
immler@69619
  1528
      apply (auto simp:  sum_clauses sum.If_cases if_smult sum_subtractf scaleR_left.sum algebra_simps *)
immler@69619
  1529
      done
immler@69619
  1530
  qed
immler@69619
  1531
  show ?thesis
immler@69619
  1532
    by (intro subset_antisym affine_hull_insert_subset_span) (auto simp: affine_hull_explicit dest!: *)
immler@69619
  1533
qed
immler@69619
  1534
immler@69619
  1535
lemma affine_hull_span:
immler@69619
  1536
  assumes "a \<in> S"
immler@69619
  1537
  shows "affine hull S = {a + v | v. v \<in> span {x - a | x. x \<in> S - {a}}}"
immler@69619
  1538
  using affine_hull_insert_span[of a "S - {a}", unfolded insert_Diff[OF assms]] by auto
immler@69619
  1539
immler@69619
  1540
immler@69619
  1541
subsubsection%unimportant \<open>Parallel affine sets\<close>
immler@69619
  1542
immler@69619
  1543
definition affine_parallel :: "'a::real_vector set \<Rightarrow> 'a::real_vector set \<Rightarrow> bool"
immler@69619
  1544
  where "affine_parallel S T \<longleftrightarrow> (\<exists>a. T = (\<lambda>x. a + x) ` S)"
immler@69619
  1545
immler@69619
  1546
lemma affine_parallel_expl_aux:
immler@69619
  1547
  fixes S T :: "'a::real_vector set"
immler@69619
  1548
  assumes "\<And>x. x \<in> S \<longleftrightarrow> a + x \<in> T"
immler@69619
  1549
  shows "T = (\<lambda>x. a + x) ` S"
immler@69619
  1550
proof -
immler@69619
  1551
  have "x \<in> ((\<lambda>x. a + x) ` S)" if "x \<in> T" for x
immler@69619
  1552
    using that
immler@69619
  1553
    by (simp add: image_iff) (metis add.commute diff_add_cancel assms)
immler@69619
  1554
  moreover have "T \<ge> (\<lambda>x. a + x) ` S"
immler@69619
  1555
    using assms by auto
immler@69619
  1556
  ultimately show ?thesis by auto
immler@69619
  1557
qed
immler@69619
  1558
immler@69619
  1559
lemma affine_parallel_expl: "affine_parallel S T \<longleftrightarrow> (\<exists>a. \<forall>x. x \<in> S \<longleftrightarrow> a + x \<in> T)"
immler@69619
  1560
  unfolding affine_parallel_def
immler@69619
  1561
  using affine_parallel_expl_aux[of S _ T] by auto
immler@69619
  1562
immler@69619
  1563
lemma affine_parallel_reflex: "affine_parallel S S"
immler@69619
  1564
  unfolding affine_parallel_def
immler@69619
  1565
  using image_add_0 by blast
immler@69619
  1566
immler@69619
  1567
lemma affine_parallel_commut:
immler@69619
  1568
  assumes "affine_parallel A B"
immler@69619
  1569
  shows "affine_parallel B A"
immler@69619
  1570
proof -
immler@69619
  1571
  from assms obtain a where B: "B = (\<lambda>x. a + x) ` A"
immler@69619
  1572
    unfolding affine_parallel_def by auto
immler@69619
  1573
  have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
immler@69619
  1574
  from B show ?thesis
immler@69619
  1575
    using translation_galois [of B a A]
immler@69619
  1576
    unfolding affine_parallel_def by auto
immler@69619
  1577
qed
immler@69619
  1578
immler@69619
  1579
lemma affine_parallel_assoc:
immler@69619
  1580
  assumes "affine_parallel A B"
immler@69619
  1581
    and "affine_parallel B C"
immler@69619
  1582
  shows "affine_parallel A C"
immler@69619
  1583
proof -
immler@69619
  1584
  from assms obtain ab where "B = (\<lambda>x. ab + x) ` A"
immler@69619
  1585
    unfolding affine_parallel_def by auto
immler@69619
  1586
  moreover
immler@69619
  1587
  from assms obtain bc where "C = (\<lambda>x. bc + x) ` B"
immler@69619
  1588
    unfolding affine_parallel_def by auto
immler@69619
  1589
  ultimately show ?thesis
immler@69619
  1590
    using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto
immler@69619
  1591
qed
immler@69619
  1592
immler@69619
  1593
lemma affine_translation_aux:
immler@69619
  1594
  fixes a :: "'a::real_vector"
immler@69619
  1595
  assumes "affine ((\<lambda>x. a + x) ` S)"
immler@69619
  1596
  shows "affine S"
immler@69619
  1597
proof -
immler@69619
  1598
  {
immler@69619
  1599
    fix x y u v
immler@69619
  1600
    assume xy: "x \<in> S" "y \<in> S" "(u :: real) + v = 1"
immler@69619
  1601
    then have "(a + x) \<in> ((\<lambda>x. a + x) ` S)" "(a + y) \<in> ((\<lambda>x. a + x) ` S)"
immler@69619
  1602
      by auto
immler@69619
  1603
    then have h1: "u *\<^sub>R  (a + x) + v *\<^sub>R (a + y) \<in> (\<lambda>x. a + x) ` S"
immler@69619
  1604
      using xy assms unfolding affine_def by auto
immler@69619
  1605
    have "u *\<^sub>R (a + x) + v *\<^sub>R (a + y) = (u + v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)"
immler@69619
  1606
      by (simp add: algebra_simps)
immler@69619
  1607
    also have "\<dots> = a + (u *\<^sub>R x + v *\<^sub>R y)"
immler@69619
  1608
      using \<open>u + v = 1\<close> by auto
immler@69619
  1609
    ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) \<in> (\<lambda>x. a + x) ` S"
immler@69619
  1610
      using h1 by auto
immler@69619
  1611
    then have "u *\<^sub>R x + v *\<^sub>R y \<in> S" by auto
immler@69619
  1612
  }
immler@69619
  1613
  then show ?thesis unfolding affine_def by auto
immler@69619
  1614
qed
immler@69619
  1615
immler@69619
  1616
lemma affine_translation:
immler@69619
  1617
  fixes a :: "'a::real_vector"
immler@69619
  1618
  shows "affine S \<longleftrightarrow> affine ((\<lambda>x. a + x) ` S)"
immler@69619
  1619
proof -
immler@69619
  1620
  have "affine S \<Longrightarrow> affine ((\<lambda>x. a + x) ` S)"
immler@69619
  1621
    using affine_translation_aux[of "-a" "((\<lambda>x. a + x) ` S)"]
immler@69619
  1622
    using translation_assoc[of "-a" a S] by auto
immler@69619
  1623
  then show ?thesis using affine_translation_aux by auto
immler@69619
  1624
qed
immler@69619
  1625
immler@69619
  1626
lemma parallel_is_affine:
immler@69619
  1627
  fixes S T :: "'a::real_vector set"
immler@69619
  1628
  assumes "affine S" "affine_parallel S T"
immler@69619
  1629
  shows "affine T"
immler@69619
  1630
proof -
immler@69619
  1631
  from assms obtain a where "T = (\<lambda>x. a + x) ` S"
immler@69619
  1632
    unfolding affine_parallel_def by auto
immler@69619
  1633
  then show ?thesis
immler@69619
  1634
    using affine_translation assms by auto
immler@69619
  1635
qed
immler@69619
  1636
immler@69619
  1637
lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
immler@69619
  1638
  unfolding subspace_def affine_def by auto
immler@69619
  1639
immler@69619
  1640
immler@69619
  1641
subsubsection%unimportant \<open>Subspace parallel to an affine set\<close>
immler@69619
  1642
immler@69619
  1643
lemma subspace_affine: "subspace S \<longleftrightarrow> affine S \<and> 0 \<in> S"
immler@69619
  1644
proof -
immler@69619
  1645
  have h0: "subspace S \<Longrightarrow> affine S \<and> 0 \<in> S"
immler@69619
  1646
    using subspace_imp_affine[of S] subspace_0 by auto
immler@69619
  1647
  {
immler@69619
  1648
    assume assm: "affine S \<and> 0 \<in> S"
immler@69619
  1649
    {
immler@69619
  1650
      fix c :: real
immler@69619
  1651
      fix x
immler@69619
  1652
      assume x: "x \<in> S"
immler@69619
  1653
      have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto
immler@69619
  1654
      moreover
immler@69619
  1655
      have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \<in> S"
immler@69619
  1656
        using affine_alt[of S] assm x by auto
immler@69619
  1657
      ultimately have "c *\<^sub>R x \<in> S" by auto
immler@69619
  1658
    }
immler@69619
  1659
    then have h1: "\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S" by auto
immler@69619
  1660
immler@69619
  1661
    {
immler@69619
  1662
      fix x y
immler@69619
  1663
      assume xy: "x \<in> S" "y \<in> S"
immler@69619
  1664
      define u where "u = (1 :: real)/2"
immler@69619
  1665
      have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)"
immler@69619
  1666
        by auto
immler@69619
  1667
      moreover
immler@69619
  1668
      have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y"
immler@69619
  1669
        by (simp add: algebra_simps)
immler@69619
  1670
      moreover
immler@69619
  1671
      have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> S"
immler@69619
  1672
        using affine_alt[of S] assm xy by auto
immler@69619
  1673
      ultimately
immler@69619
  1674
      have "(1/2) *\<^sub>R (x+y) \<in> S"
immler@69619
  1675
        using u_def by auto
immler@69619
  1676
      moreover
immler@69619
  1677
      have "x + y = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))"
immler@69619
  1678
        by auto
immler@69619
  1679
      ultimately
immler@69619
  1680
      have "x + y \<in> S"
immler@69619
  1681
        using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
immler@69619
  1682
    }
immler@69619
  1683
    then have "\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S"
immler@69619
  1684
      by auto
immler@69619
  1685
    then have "subspace S"
immler@69619
  1686
      using h1 assm unfolding subspace_def by auto
immler@69619
  1687
  }
immler@69619
  1688
  then show ?thesis using h0 by metis
immler@69619
  1689
qed
immler@69619
  1690
immler@69619
  1691
lemma affine_diffs_subspace:
immler@69619
  1692
  assumes "affine S" "a \<in> S"
immler@69619
  1693
  shows "subspace ((\<lambda>x. (-a)+x) ` S)"
immler@69619
  1694
proof -
immler@69619
  1695
  have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
immler@69619
  1696
  have "affine ((\<lambda>x. (-a)+x) ` S)"
immler@69619
  1697
    using  affine_translation assms by auto
immler@69619
  1698
  moreover have "0 \<in> ((\<lambda>x. (-a)+x) ` S)"
immler@69619
  1699
    using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto
immler@69619
  1700
  ultimately show ?thesis using subspace_affine by auto
immler@69619
  1701
qed
immler@69619
  1702
immler@69619
  1703
lemma parallel_subspace_explicit:
immler@69619
  1704
  assumes "affine S"
immler@69619
  1705
    and "a \<in> S"
immler@69619
  1706
  assumes "L \<equiv> {y. \<exists>x \<in> S. (-a) + x = y}"
immler@69619
  1707
  shows "subspace L \<and> affine_parallel S L"
immler@69619
  1708
proof -
immler@69619
  1709
  from assms have "L = plus (- a) ` S" by auto
immler@69619
  1710
  then have par: "affine_parallel S L"
immler@69619
  1711
    unfolding affine_parallel_def ..
immler@69619
  1712
  then have "affine L" using assms parallel_is_affine by auto
immler@69619
  1713
  moreover have "0 \<in> L"
immler@69619
  1714
    using assms by auto
immler@69619
  1715
  ultimately show ?thesis
immler@69619
  1716
    using subspace_affine par by auto
immler@69619
  1717
qed
immler@69619
  1718
immler@69619
  1719
lemma parallel_subspace_aux:
immler@69619
  1720
  assumes "subspace A"
immler@69619
  1721
    and "subspace B"
immler@69619
  1722
    and "affine_parallel A B"
immler@69619
  1723
  shows "A \<supseteq> B"
immler@69619
  1724
proof -
immler@69619
  1725
  from assms obtain a where a: "\<forall>x. x \<in> A \<longleftrightarrow> a + x \<in> B"
immler@69619
  1726
    using affine_parallel_expl[of A B] by auto
immler@69619
  1727
  then have "-a \<in> A"
immler@69619
  1728
    using assms subspace_0[of B] by auto
immler@69619
  1729
  then have "a \<in> A"
immler@69619
  1730
    using assms subspace_neg[of A "-a"] by auto
immler@69619
  1731
  then show ?thesis
immler@69619
  1732
    using assms a unfolding subspace_def by auto
immler@69619
  1733
qed
immler@69619
  1734
immler@69619
  1735
lemma parallel_subspace:
immler@69619
  1736
  assumes "subspace A"
immler@69619
  1737
    and "subspace B"
immler@69619
  1738
    and "affine_parallel A B"
immler@69619
  1739
  shows "A = B"
immler@69619
  1740
proof
immler@69619
  1741
  show "A \<supseteq> B"
immler@69619
  1742
    using assms parallel_subspace_aux by auto
immler@69619
  1743
  show "A \<subseteq> B"
immler@69619
  1744
    using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto
immler@69619
  1745
qed
immler@69619
  1746
immler@69619
  1747
lemma affine_parallel_subspace:
immler@69619
  1748
  assumes "affine S" "S \<noteq> {}"
immler@69619
  1749
  shows "\<exists>!L. subspace L \<and> affine_parallel S L"
immler@69619
  1750
proof -
immler@69619
  1751
  have ex: "\<exists>L. subspace L \<and> affine_parallel S L"
immler@69619
  1752
    using assms parallel_subspace_explicit by auto
immler@69619
  1753
  {
immler@69619
  1754
    fix L1 L2
immler@69619
  1755
    assume ass: "subspace L1 \<and> affine_parallel S L1" "subspace L2 \<and> affine_parallel S L2"
immler@69619
  1756
    then have "affine_parallel L1 L2"
immler@69619
  1757
      using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto
immler@69619
  1758
    then have "L1 = L2"
immler@69619
  1759
      using ass parallel_subspace by auto
immler@69619
  1760
  }
immler@69619
  1761
  then show ?thesis using ex by auto
immler@69619
  1762
qed
immler@69619
  1763
immler@69619
  1764
immler@69619
  1765
subsection \<open>Cones\<close>
immler@69619
  1766
immler@69619
  1767
definition%important cone :: "'a::real_vector set \<Rightarrow> bool"
immler@69619
  1768
  where "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. c *\<^sub>R x \<in> s)"
immler@69619
  1769
immler@69619
  1770
lemma cone_empty[intro, simp]: "cone {}"
immler@69619
  1771
  unfolding cone_def by auto
immler@69619
  1772
immler@69619
  1773
lemma cone_univ[intro, simp]: "cone UNIV"
immler@69619
  1774
  unfolding cone_def by auto
immler@69619
  1775
immler@69619
  1776
lemma cone_Inter[intro]: "\<forall>s\<in>f. cone s \<Longrightarrow> cone (\<Inter>f)"
immler@69619
  1777
  unfolding cone_def by auto
immler@69619
  1778
immler@69619
  1779
lemma subspace_imp_cone: "subspace S \<Longrightarrow> cone S"
immler@69619
  1780
  by (simp add: cone_def subspace_scale)
immler@69619
  1781
immler@69619
  1782
immler@69619
  1783
subsubsection \<open>Conic hull\<close>
immler@69619
  1784
immler@69619
  1785
lemma cone_cone_hull: "cone (cone hull s)"
immler@69619
  1786
  unfolding hull_def by auto
immler@69619
  1787
immler@69619
  1788
lemma cone_hull_eq: "cone hull s = s \<longleftrightarrow> cone s"
immler@69619
  1789
  apply (rule hull_eq)
immler@69619
  1790
  using cone_Inter
immler@69619
  1791
  unfolding subset_eq
immler@69619
  1792
  apply auto
immler@69619
  1793
  done
immler@69619
  1794
immler@69619
  1795
lemma mem_cone:
immler@69619
  1796
  assumes "cone S" "x \<in> S" "c \<ge> 0"
immler@69619
  1797
  shows "c *\<^sub>R x \<in> S"
immler@69619
  1798
  using assms cone_def[of S] by auto
immler@69619
  1799
immler@69619
  1800
lemma cone_contains_0:
immler@69619
  1801
  assumes "cone S"
immler@69619
  1802
  shows "S \<noteq> {} \<longleftrightarrow> 0 \<in> S"
immler@69619
  1803
proof -
immler@69619
  1804
  {
immler@69619
  1805
    assume "S \<noteq> {}"
immler@69619
  1806
    then obtain a where "a \<in> S" by auto
immler@69619
  1807
    then have "0 \<in> S"
immler@69619
  1808
      using assms mem_cone[of S a 0] by auto
immler@69619
  1809
  }
immler@69619
  1810
  then show ?thesis by auto
immler@69619
  1811
qed
immler@69619
  1812
immler@69619
  1813
lemma cone_0: "cone {0}"
immler@69619
  1814
  unfolding cone_def by auto
immler@69619
  1815
immler@69619
  1816
lemma cone_Union[intro]: "(\<forall>s\<in>f. cone s) \<longrightarrow> cone (\<Union>f)"
immler@69619
  1817
  unfolding cone_def by blast
immler@69619
  1818
immler@69619
  1819
lemma cone_iff:
immler@69619
  1820
  assumes "S \<noteq> {}"
immler@69619
  1821
  shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
immler@69619
  1822
proof -
immler@69619
  1823
  {
immler@69619
  1824
    assume "cone S"
immler@69619
  1825
    {
immler@69619
  1826
      fix c :: real
immler@69619
  1827
      assume "c > 0"
immler@69619
  1828
      {
immler@69619
  1829
        fix x
immler@69619
  1830
        assume "x \<in> S"
immler@69619
  1831
        then have "x \<in> ((*\<^sub>R) c) ` S"
immler@69619
  1832
          unfolding image_def
immler@69619
  1833
          using \<open>cone S\<close> \<open>c>0\<close> mem_cone[of S x "1/c"]
immler@69619
  1834
            exI[of "(\<lambda>t. t \<in> S \<and> x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"]
immler@69619
  1835
          by auto
immler@69619
  1836
      }
immler@69619
  1837
      moreover
immler@69619
  1838
      {
immler@69619
  1839
        fix x
immler@69619
  1840
        assume "x \<in> ((*\<^sub>R) c) ` S"
immler@69619
  1841
        then have "x \<in> S"
immler@69619
  1842
          using \<open>cone S\<close> \<open>c > 0\<close>
immler@69619
  1843
          unfolding cone_def image_def \<open>c > 0\<close> by auto
immler@69619
  1844
      }
immler@69619
  1845
      ultimately have "((*\<^sub>R) c) ` S = S" by auto
immler@69619
  1846
    }
immler@69619
  1847
    then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
immler@69619
  1848
      using \<open>cone S\<close> cone_contains_0[of S] assms by auto
immler@69619
  1849
  }
immler@69619
  1850
  moreover
immler@69619
  1851
  {
immler@69619
  1852
    assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
immler@69619
  1853
    {
immler@69619
  1854
      fix x
immler@69619
  1855
      assume "x \<in> S"
immler@69619
  1856
      fix c1 :: real
immler@69619
  1857
      assume "c1 \<ge> 0"
immler@69619
  1858
      then have "c1 = 0 \<or> c1 > 0" by auto
immler@69619
  1859
      then have "c1 *\<^sub>R x \<in> S" using a \<open>x \<in> S\<close> by auto
immler@69619
  1860
    }
immler@69619
  1861
    then have "cone S" unfolding cone_def by auto
immler@69619
  1862
  }
immler@69619
  1863
  ultimately show ?thesis by blast
immler@69619
  1864
qed
immler@69619
  1865
immler@69619
  1866
lemma cone_hull_empty: "cone hull {} = {}"
immler@69619
  1867
  by (metis cone_empty cone_hull_eq)
immler@69619
  1868
immler@69619
  1869
lemma cone_hull_empty_iff: "S = {} \<longleftrightarrow> cone hull S = {}"
immler@69619
  1870
  by (metis bot_least cone_hull_empty hull_subset xtrans(5))
immler@69619
  1871
immler@69619
  1872
lemma cone_hull_contains_0: "S \<noteq> {} \<longleftrightarrow> 0 \<in> cone hull S"
immler@69619
  1873
  using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S]
immler@69619
  1874
  by auto
immler@69619
  1875
immler@69619
  1876
lemma mem_cone_hull:
immler@69619
  1877
  assumes "x \<in> S" "c \<ge> 0"
immler@69619
  1878
  shows "c *\<^sub>R x \<in> cone hull S"
immler@69619
  1879
  by (metis assms cone_cone_hull hull_inc mem_cone)
immler@69619
  1880
immler@69619
  1881
proposition cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
immler@69619
  1882
  (is "?lhs = ?rhs")
immler@69619
  1883
proof -
immler@69619
  1884
  {
immler@69619
  1885
    fix x
immler@69619
  1886
    assume "x \<in> ?rhs"
immler@69619
  1887
    then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S"
immler@69619
  1888
      by auto
immler@69619
  1889
    fix c :: real
immler@69619
  1890
    assume c: "c \<ge> 0"
immler@69619
  1891
    then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx"
immler@69619
  1892
      using x by (simp add: algebra_simps)
immler@69619
  1893
    moreover
immler@69619
  1894
    have "c * cx \<ge> 0" using c x by auto
immler@69619
  1895
    ultimately
immler@69619
  1896
    have "c *\<^sub>R x \<in> ?rhs" using x by auto
immler@69619
  1897
  }
immler@69619
  1898
  then have "cone ?rhs"
immler@69619
  1899
    unfolding cone_def by auto
immler@69619
  1900
  then have "?rhs \<in> Collect cone"
immler@69619
  1901
    unfolding mem_Collect_eq by auto
immler@69619
  1902
  {
immler@69619
  1903
    fix x
immler@69619
  1904
    assume "x \<in> S"
immler@69619
  1905
    then have "1 *\<^sub>R x \<in> ?rhs"
immler@69619
  1906
      apply auto
immler@69619
  1907
      apply (rule_tac x = 1 in exI, auto)
immler@69619
  1908
      done
immler@69619
  1909
    then have "x \<in> ?rhs" by auto
immler@69619
  1910
  }
immler@69619
  1911
  then have "S \<subseteq> ?rhs" by auto
immler@69619
  1912
  then have "?lhs \<subseteq> ?rhs"
immler@69619
  1913
    using \<open>?rhs \<in> Collect cone\<close> hull_minimal[of S "?rhs" "cone"] by auto
immler@69619
  1914
  moreover
immler@69619
  1915
  {
immler@69619
  1916
    fix x
immler@69619
  1917
    assume "x \<in> ?rhs"
immler@69619
  1918
    then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S"
immler@69619
  1919
      by auto
immler@69619
  1920
    then have "xx \<in> cone hull S"
immler@69619
  1921
      using hull_subset[of S] by auto
immler@69619
  1922
    then have "x \<in> ?lhs"
immler@69619
  1923
      using x cone_cone_hull[of S] cone_def[of "cone hull S"] by auto
immler@69619
  1924
  }
immler@69619
  1925
  ultimately show ?thesis by auto
immler@69619
  1926
qed
immler@69619
  1927
immler@69619
  1928
immler@69619
  1929
subsection \<open>Affine dependence and consequential theorems\<close>
immler@69619
  1930
immler@69619
  1931
text "Formalized by Lars Schewe."
immler@69619
  1932
immler@69619
  1933
definition%important affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
immler@69619
  1934
  where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
immler@69619
  1935
immler@69619
  1936
lemma affine_dependent_subset:
immler@69619
  1937
   "\<lbrakk>affine_dependent s; s \<subseteq> t\<rbrakk> \<Longrightarrow> affine_dependent t"
immler@69619
  1938
apply (simp add: affine_dependent_def Bex_def)
immler@69619
  1939
apply (blast dest: hull_mono [OF Diff_mono [OF _ subset_refl]])
immler@69619
  1940
done
immler@69619
  1941
immler@69619
  1942
lemma affine_independent_subset:
immler@69619
  1943
  shows "\<lbrakk>\<not> affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> \<not> affine_dependent s"
immler@69619
  1944
by (metis affine_dependent_subset)
immler@69619
  1945
immler@69619
  1946
lemma affine_independent_Diff:
immler@69619
  1947
   "\<not> affine_dependent s \<Longrightarrow> \<not> affine_dependent(s - t)"
immler@69619
  1948
by (meson Diff_subset affine_dependent_subset)
immler@69619
  1949
immler@69619
  1950
proposition affine_dependent_explicit:
immler@69619
  1951
  "affine_dependent p \<longleftrightarrow>
immler@69619
  1952
    (\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
immler@69619
  1953
proof -
immler@69619
  1954
  have "\<exists>S u. finite S \<and> S \<subseteq> p \<and> sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> (\<Sum>w\<in>S. u w *\<^sub>R w) = 0"
immler@69619
  1955
    if "(\<Sum>w\<in>S. u w *\<^sub>R w) = x" "x \<in> p" "finite S" "S \<noteq> {}" "S \<subseteq> p - {x}" "sum u S = 1" for x S u
immler@69619
  1956
  proof (intro exI conjI)
immler@69619
  1957
    have "x \<notin> S" 
immler@69619
  1958
      using that by auto
immler@69619
  1959
    then show "(\<Sum>v \<in> insert x S. if v = x then - 1 else u v) = 0"
immler@69619
  1960
      using that by (simp add: sum_delta_notmem)
immler@69619
  1961
    show "(\<Sum>w \<in> insert x S. (if w = x then - 1 else u w) *\<^sub>R w) = 0"
immler@69619
  1962
      using that \<open>x \<notin> S\<close> by (simp add: if_smult sum_delta_notmem cong: if_cong)
immler@69619
  1963
  qed (use that in auto)
immler@69619
  1964
  moreover have "\<exists>x\<in>p. \<exists>S u. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p - {x} \<and> sum u S = 1 \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = x"
immler@69619
  1965
    if "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0" "finite S" "S \<subseteq> p" "sum u S = 0" "v \<in> S" "u v \<noteq> 0" for S u v
immler@69619
  1966
  proof (intro bexI exI conjI)
immler@69619
  1967
    have "S \<noteq> {v}"
immler@69619
  1968
      using that by auto
immler@69619
  1969
    then show "S - {v} \<noteq> {}"
immler@69619
  1970
      using that by auto
immler@69619
  1971
    show "(\<Sum>x \<in> S - {v}. - (1 / u v) * u x) = 1"
immler@69619
  1972
      unfolding sum_distrib_left[symmetric] sum_diff1[OF \<open>finite S\<close>] by (simp add: that)
immler@69619
  1973
    show "(\<Sum>x\<in>S - {v}. (- (1 / u v) * u x) *\<^sub>R x) = v"
immler@69619
  1974
      unfolding sum_distrib_left [symmetric] scaleR_scaleR[symmetric]
immler@69619
  1975
                scaleR_right.sum [symmetric] sum_diff1[OF \<open>finite S\<close>] 
immler@69619
  1976
      using that by auto
immler@69619
  1977
    show "S - {v} \<subseteq> p - {v}"
immler@69619
  1978
      using that by auto
immler@69619
  1979
  qed (use that in auto)
immler@69619
  1980
  ultimately show ?thesis
immler@69619
  1981
    unfolding affine_dependent_def affine_hull_explicit by auto
immler@69619
  1982
qed
immler@69619
  1983
immler@69619
  1984
lemma affine_dependent_explicit_finite:
immler@69619
  1985
  fixes S :: "'a::real_vector set"
immler@69619
  1986
  assumes "finite S"
immler@69619
  1987
  shows "affine_dependent S \<longleftrightarrow>
immler@69619
  1988
    (\<exists>u. sum u S = 0 \<and> (\<exists>v\<in>S. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) S = 0)"
immler@69619
  1989
  (is "?lhs = ?rhs")
immler@69619
  1990
proof
immler@69619
  1991
  have *: "\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else 0::'a)"
immler@69619
  1992
    by auto
immler@69619
  1993
  assume ?lhs
immler@69619
  1994
  then obtain t u v where
immler@69619
  1995
    "finite t" "t \<subseteq> S" "sum u t = 0" "v\<in>t" "u v \<noteq> 0"  "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0"
immler@69619
  1996
    unfolding affine_dependent_explicit by auto
immler@69619
  1997
  then show ?rhs
immler@69619
  1998
    apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
immler@69619
  1999
    apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \<open>t\<subseteq>S\<close>])
immler@69619
  2000
    done
immler@69619
  2001
next
immler@69619
  2002
  assume ?rhs
immler@69619
  2003
  then obtain u v where "sum u S = 0"  "v\<in>S" "u v \<noteq> 0" "(\<Sum>v\<in>S. u v *\<^sub>R v) = 0"
immler@69619
  2004
    by auto
immler@69619
  2005
  then show ?lhs unfolding affine_dependent_explicit
immler@69619
  2006
    using assms by auto
immler@69619
  2007
qed
immler@69619
  2008
immler@69619
  2009
immler@69619
  2010
subsection%unimportant \<open>Connectedness of convex sets\<close>
immler@69619
  2011
immler@69619
  2012
lemma connectedD:
immler@69619
  2013
  "connected S \<Longrightarrow> open A \<Longrightarrow> open B \<Longrightarrow> S \<subseteq> A \<union> B \<Longrightarrow> A \<inter> B \<inter> S = {} \<Longrightarrow> A \<inter> S = {} \<or> B \<inter> S = {}"
immler@69619
  2014
  by (rule Topological_Spaces.topological_space_class.connectedD)
immler@69619
  2015
immler@69619
  2016
lemma convex_connected:
immler@69619
  2017
  fixes S :: "'a::real_normed_vector set"
immler@69619
  2018
  assumes "convex S"
immler@69619
  2019
  shows "connected S"
immler@69619
  2020
proof (rule connectedI)
immler@69619
  2021
  fix A B
immler@69619
  2022
  assume "open A" "open B" "A \<inter> B \<inter> S = {}" "S \<subseteq> A \<union> B"
immler@69619
  2023
  moreover
immler@69619
  2024
  assume "A \<inter> S \<noteq> {}" "B \<inter> S \<noteq> {}"
immler@69619
  2025
  then obtain a b where a: "a \<in> A" "a \<in> S" and b: "b \<in> B" "b \<in> S" by auto
immler@69619
  2026
  define f where [abs_def]: "f u = u *\<^sub>R a + (1 - u) *\<^sub>R b" for u
immler@69619
  2027
  then have "continuous_on {0 .. 1} f"
immler@69619
  2028
    by (auto intro!: continuous_intros)
immler@69619
  2029
  then have "connected (f ` {0 .. 1})"
immler@69619
  2030
    by (auto intro!: connected_continuous_image)
immler@69619
  2031
  note connectedD[OF this, of A B]
immler@69619
  2032
  moreover have "a \<in> A \<inter> f ` {0 .. 1}"
immler@69619
  2033
    using a by (auto intro!: image_eqI[of _ _ 1] simp: f_def)
immler@69619
  2034
  moreover have "b \<in> B \<inter> f ` {0 .. 1}"
immler@69619
  2035
    using b by (auto intro!: image_eqI[of _ _ 0] simp: f_def)
immler@69619
  2036
  moreover have "f ` {0 .. 1} \<subseteq> S"
immler@69619
  2037
    using \<open>convex S\<close> a b unfolding convex_def f_def by auto
immler@69619
  2038
  ultimately show False by auto
immler@69619
  2039
qed
immler@69619
  2040
immler@69619
  2041
corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
immler@69619
  2042
  by (simp add: convex_connected)
immler@69619
  2043
immler@69619
  2044
lemma convex_prod:
immler@69619
  2045
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> convex {x. P i x}"
immler@69619
  2046
  shows "convex {x. \<forall>i\<in>Basis. P i (x\<bullet>i)}"
immler@69619
  2047
  using assms unfolding convex_def
immler@69619
  2048
  by (auto simp: inner_add_left)
immler@69619
  2049
immler@69619
  2050
lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i)}"
immler@69619
  2051
  by (rule convex_prod) (simp add: atLeast_def[symmetric] convex_real_interval)
immler@69619
  2052
immler@69619
  2053
subsection \<open>Convex hull\<close>
immler@69619
  2054
immler@69619
  2055
lemma convex_convex_hull [iff]: "convex (convex hull s)"
immler@69619
  2056
  unfolding hull_def
immler@69619
  2057
  using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"]
immler@69619
  2058
  by auto
immler@69619
  2059
immler@69619
  2060
lemma convex_hull_subset:
immler@69619
  2061
    "s \<subseteq> convex hull t \<Longrightarrow> convex hull s \<subseteq> convex hull t"
immler@69619
  2062
  by (simp add: convex_convex_hull subset_hull)
immler@69619
  2063
immler@69619
  2064
lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
immler@69619
  2065
  by (metis convex_convex_hull hull_same)
immler@69619
  2066
immler@69619
  2067
subsubsection%unimportant \<open>Convex hull is "preserved" by a linear function\<close>
immler@69619
  2068
immler@69619
  2069
lemma convex_hull_linear_image:
immler@69619
  2070
  assumes f: "linear f"
immler@69619
  2071
  shows "f ` (convex hull s) = convex hull (f ` s)"
immler@69619
  2072
proof
immler@69619
  2073
  show "convex hull (f ` s) \<subseteq> f ` (convex hull s)"
immler@69619
  2074
    by (intro hull_minimal image_mono hull_subset convex_linear_image assms convex_convex_hull)
immler@69619
  2075
  show "f ` (convex hull s) \<subseteq> convex hull (f ` s)"
immler@69619
  2076
  proof (unfold image_subset_iff_subset_vimage, rule hull_minimal)
immler@69619
  2077
    show "s \<subseteq> f -` (convex hull (f ` s))"
immler@69619
  2078
      by (fast intro: hull_inc)
immler@69619
  2079
    show "convex (f -` (convex hull (f ` s)))"
immler@69619
  2080
      by (intro convex_linear_vimage [OF f] convex_convex_hull)
immler@69619
  2081
  qed
immler@69619
  2082
qed
immler@69619
  2083
immler@69619
  2084
lemma in_convex_hull_linear_image:
immler@69619
  2085
  assumes "linear f"
immler@69619
  2086
    and "x \<in> convex hull s"
immler@69619
  2087
  shows "f x \<in> convex hull (f ` s)"
immler@69619
  2088
  using convex_hull_linear_image[OF assms(1)] assms(2) by auto
immler@69619
  2089
immler@69619
  2090
lemma convex_hull_Times:
immler@69619
  2091
  "convex hull (s \<times> t) = (convex hull s) \<times> (convex hull t)"
immler@69619
  2092
proof
immler@69619
  2093
  show "convex hull (s \<times> t) \<subseteq> (convex hull s) \<times> (convex hull t)"
immler@69619
  2094
    by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull)
immler@69619
  2095
  have "(x, y) \<in> convex hull (s \<times> t)" if x: "x \<in> convex hull s" and y: "y \<in> convex hull t" for x y
immler@69619
  2096
  proof (rule hull_induct [OF x], rule hull_induct [OF y])
immler@69619
  2097
    fix x y assume "x \<in> s" and "y \<in> t"
immler@69619
  2098
    then show "(x, y) \<in> convex hull (s \<times> t)"
immler@69619
  2099
      by (simp add: hull_inc)
immler@69619
  2100
  next
immler@69619
  2101
    fix x let ?S = "((\<lambda>y. (0, y)) -` (\<lambda>p. (- x, 0) + p) ` (convex hull s \<times> t))"
immler@69619
  2102
    have "convex ?S"
immler@69619
  2103
      by (intro convex_linear_vimage convex_translation convex_convex_hull,
immler@69619
  2104
        simp add: linear_iff)
immler@69619
  2105
    also have "?S = {y. (x, y) \<in> convex hull (s \<times> t)}"
immler@69619
  2106
      by (auto simp: image_def Bex_def)
immler@69619
  2107
    finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
immler@69619
  2108
  next
immler@69619
  2109
    show "convex {x. (x, y) \<in> convex hull s \<times> t}"
immler@69619
  2110
    proof -
immler@69619
  2111
      fix y let ?S = "((\<lambda>x. (x, 0)) -` (\<lambda>p. (0, - y) + p) ` (convex hull s \<times> t))"
immler@69619
  2112
      have "convex ?S"
immler@69619
  2113
      by (intro convex_linear_vimage convex_translation convex_convex_hull,
immler@69619
  2114
        simp add: linear_iff)
immler@69619
  2115
      also have "?S = {x. (x, y) \<in> convex hull (s \<times> t)}"
immler@69619
  2116
        by (auto simp: image_def Bex_def)
immler@69619
  2117
      finally show "convex {x. (x, y) \<in> convex hull (s \<times> t)}" .
immler@69619
  2118
    qed
immler@69619
  2119
  qed
immler@69619
  2120
  then show "(convex hull s) \<times> (convex hull t) \<subseteq> convex hull (s \<times> t)"
immler@69619
  2121
    unfolding subset_eq split_paired_Ball_Sigma by blast
immler@69619
  2122
qed
immler@69619
  2123
immler@69619
  2124
immler@69619
  2125
subsubsection%unimportant \<open>Stepping theorems for convex hulls of finite sets\<close>
immler@69619
  2126
immler@69619
  2127
lemma convex_hull_empty[simp]: "convex hull {} = {}"
immler@69619
  2128
  by (rule hull_unique) auto
immler@69619
  2129
immler@69619
  2130
lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
immler@69619
  2131
  by (rule hull_unique) auto
immler@69619
  2132
immler@69619
  2133
lemma convex_hull_insert:
immler@69619
  2134
  fixes S :: "'a::real_vector set"
immler@69619
  2135
  assumes "S \<noteq> {}"
immler@69619
  2136
  shows "convex hull (insert a S) =
immler@69619
  2137
         {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and> b \<in> (convex hull S) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}"
immler@69619
  2138
  (is "_ = ?hull")
immler@69619
  2139
proof (intro equalityI hull_minimal subsetI)
immler@69619
  2140
  fix x
immler@69619
  2141
  assume "x \<in> insert a S"
immler@69619
  2142
  then have "\<exists>u\<ge>0. \<exists>v\<ge>0. u + v = 1 \<and> (\<exists>b. b \<in> convex hull S \<and> x = u *\<^sub>R a + v *\<^sub>R b)"
immler@69619
  2143
  unfolding insert_iff
immler@69619
  2144
  proof
immler@69619
  2145
    assume "x = a"
immler@69619
  2146
    then show ?thesis
immler@69619
  2147
      by (rule_tac x=1 in exI) (use assms hull_subset in fastforce)
immler@69619
  2148
  next
immler@69619
  2149
    assume "x \<in> S"
immler@69619
  2150
    with hull_subset[of S convex] show ?thesis
immler@69619
  2151
      by force
immler@69619
  2152
  qed
immler@69619
  2153
  then show "x \<in> ?hull"
immler@69619
  2154
    by simp
immler@69619
  2155
next
immler@69619
  2156
  fix x
immler@69619
  2157
  assume "x \<in> ?hull"
immler@69619
  2158
  then obtain u v b where obt: "u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull S" "x = u *\<^sub>R a + v *\<^sub>R b"
immler@69619
  2159
    by auto
immler@69619
  2160
  have "a \<in> convex hull insert a S" "b \<in> convex hull insert a S"
immler@69619
  2161
    using hull_mono[of S "insert a S" convex] hull_mono[of "{a}" "insert a S" convex] and obt(4)
immler@69619
  2162
    by auto
immler@69619
  2163
  then show "x \<in> convex hull insert a S"
immler@69619
  2164
    unfolding obt(5) using obt(1-3)
immler@69619
  2165
    by (rule convexD [OF convex_convex_hull])
immler@69619
  2166
next
immler@69619
  2167
  show "convex ?hull"
immler@69619
  2168
  proof (rule convexI)
immler@69619
  2169
    fix x y u v
immler@69619
  2170
    assume as: "(0::real) \<le> u" "0 \<le> v" "u + v = 1" and x: "x \<in> ?hull" and y: "y \<in> ?hull"
immler@69619
  2171
    from x obtain u1 v1 b1 where
immler@69619
  2172
      obt1: "u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull S" and xeq: "x = u1 *\<^sub>R a + v1 *\<^sub>R b1"
immler@69619
  2173
      by auto
immler@69619
  2174
    from y obtain u2 v2 b2 where
immler@69619
  2175
      obt2: "u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull S" and yeq: "y = u2 *\<^sub>R a + v2 *\<^sub>R b2"
immler@69619
  2176
      by auto
immler@69619
  2177
    have *: "\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
immler@69619
  2178
      by (auto simp: algebra_simps)
immler@69619
  2179
    have "\<exists>b \<in> convex hull S. u *\<^sub>R x + v *\<^sub>R y =
immler@69619
  2180
      (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"
immler@69619
  2181
    proof (cases "u * v1 + v * v2 = 0")
immler@69619
  2182
      case True
immler@69619
  2183
      have *: "\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
immler@69619
  2184
        by (auto simp: algebra_simps)
immler@69619
  2185
      have eq0: "u * v1 = 0" "v * v2 = 0"
immler@69619
  2186
        using True mult_nonneg_nonneg[OF \<open>u\<ge>0\<close> \<open>v1\<ge>0\<close>] mult_nonneg_nonneg[OF \<open>v\<ge>0\<close> \<open>v2\<ge>0\<close>]
immler@69619
  2187
        by arith+
immler@69619
  2188
      then have "u * u1 + v * u2 = 1"
immler@69619
  2189
        using as(3) obt1(3) obt2(3) by auto
immler@69619
  2190
      then show ?thesis
immler@69619
  2191
        using "*" eq0 as obt1(4) xeq yeq by auto
immler@69619
  2192
    next
immler@69619
  2193
      case False
immler@69619
  2194
      have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)"
immler@69619
  2195
        using as(3) obt1(3) obt2(3) by (auto simp: field_simps)
immler@69619
  2196
      also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)"
immler@69619
  2197
        using as(3) obt1(3) obt2(3) by (auto simp: field_simps)
immler@69619
  2198
      also have "\<dots> = u * v1 + v * v2"
immler@69619
  2199
        by simp
immler@69619
  2200
      finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
immler@69619
  2201
      let ?b = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2"
immler@69619
  2202
      have zeroes: "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2"
immler@69619
  2203
        using as(1,2) obt1(1,2) obt2(1,2) by auto
immler@69619
  2204
      show ?thesis
immler@69619
  2205
      proof
immler@69619
  2206
        show "u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (?b - (u * u1) *\<^sub>R ?b - (v * u2) *\<^sub>R ?b)"
immler@69619
  2207
          unfolding xeq yeq * **
immler@69619
  2208
          using False by (auto simp: scaleR_left_distrib scaleR_right_distrib)
immler@69619
  2209
        show "?b \<in> convex hull S"
immler@69619
  2210
          using False zeroes obt1(4) obt2(4)
immler@69619
  2211
          by (auto simp: convexD [OF convex_convex_hull] scaleR_left_distrib scaleR_right_distrib  add_divide_distrib[symmetric]  zero_le_divide_iff)
immler@69619
  2212
      qed
immler@69619
  2213
    qed
immler@69619
  2214
    then obtain b where b: "b \<in> convex hull S" 
immler@69619
  2215
       "u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" ..
immler@69619
  2216
immler@69619
  2217
    have u1: "u1 \<le> 1"
immler@69619
  2218
      unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto
immler@69619
  2219
    have u2: "u2 \<le> 1"
immler@69619
  2220
      unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
immler@69619
  2221
    have "u1 * u + u2 * v \<le> max u1 u2 * u + max u1 u2 * v"
immler@69619
  2222
    proof (rule add_mono)
immler@69619
  2223
      show "u1 * u \<le> max u1 u2 * u" "u2 * v \<le> max u1 u2 * v"
immler@69619
  2224
        by (simp_all add: as mult_right_mono)
immler@69619
  2225
    qed
immler@69619
  2226
    also have "\<dots> \<le> 1"
immler@69619
  2227
      unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
immler@69619
  2228
    finally have le1: "u1 * u + u2 * v \<le> 1" .    
immler@69619
  2229
    show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull"
immler@69619
  2230
    proof (intro CollectI exI conjI)
immler@69619
  2231
      show "0 \<le> u * u1 + v * u2"
immler@69619
  2232
        by (simp add: as(1) as(2) obt1(1) obt2(1))
immler@69619
  2233
      show "0 \<le> 1 - u * u1 - v * u2"
immler@69619
  2234
        by (simp add: le1 diff_diff_add mult.commute)
immler@69619
  2235
    qed (use b in \<open>auto simp: algebra_simps\<close>)
immler@69619
  2236
  qed
immler@69619
  2237
qed
immler@69619
  2238
immler@69619
  2239
lemma convex_hull_insert_alt:
immler@69619
  2240
   "convex hull (insert a S) =
immler@69619
  2241
     (if S = {} then {a}
immler@69619
  2242
      else {(1 - u) *\<^sub>R a + u *\<^sub>R x |x u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> convex hull S})"
immler@69619
  2243
  apply (auto simp: convex_hull_insert)
immler@69619
  2244
  using diff_eq_eq apply fastforce
immler@69619
  2245
  by (metis add.group_left_neutral add_le_imp_le_diff diff_add_cancel)
immler@69619
  2246
immler@69619
  2247
subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
immler@69619
  2248
immler@69619
  2249
proposition convex_hull_indexed:
immler@69619
  2250
  fixes S :: "'a::real_vector set"
immler@69619
  2251
  shows "convex hull S =
immler@69619
  2252
    {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> S) \<and>
immler@69619
  2253
                (sum u {1..k} = 1) \<and> (\<Sum>i = 1..k. u i *\<^sub>R x i) = y}"
immler@69619
  2254
    (is "?xyz = ?hull")
immler@69619
  2255
proof (rule hull_unique [OF _ convexI])
immler@69619
  2256
  show "S \<subseteq> ?hull" 
immler@69619
  2257
    by (clarsimp, rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI, auto)
immler@69619
  2258
next
immler@69619
  2259
  fix T
immler@69619
  2260
  assume "S \<subseteq> T" "convex T"
immler@69619
  2261
  then show "?hull \<subseteq> T"
immler@69619
  2262
    by (blast intro: convex_sum)
immler@69619
  2263
next
immler@69619
  2264
  fix x y u v
immler@69619
  2265
  assume uv: "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
immler@69619
  2266
  assume xy: "x \<in> ?hull" "y \<in> ?hull"
immler@69619
  2267
  from xy obtain k1 u1 x1 where
immler@69619
  2268
    x [rule_format]: "\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> S" 
immler@69619
  2269
                      "sum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x"
immler@69619
  2270
    by auto
immler@69619
  2271
  from xy obtain k2 u2 x2 where
immler@69619
  2272
    y [rule_format]: "\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> S" 
immler@69619
  2273
                     "sum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y"
immler@69619
  2274
    by auto
immler@69619
  2275
  have *: "\<And>P (x::'a) y s t i. (if P i then s else t) *\<^sub>R (if P i then x else y) = (if P i then s *\<^sub>R x else t *\<^sub>R y)"
immler@69619
  2276
          "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
immler@69619
  2277
    by auto
immler@69619
  2278
  have inj: "inj_on (\<lambda>i. i + k1) {1..k2}"
immler@69619
  2279
    unfolding inj_on_def by auto
immler@69619
  2280
  let ?uu = "\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)"
immler@69619
  2281
  let ?xx = "\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)"
immler@69619
  2282
  show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull"
immler@69619
  2283
  proof (intro CollectI exI conjI ballI)
immler@69619
  2284
    show "0 \<le> ?uu i" "?xx i \<in> S" if "i \<in> {1..k1+k2}" for i
immler@69619
  2285
      using that by (auto simp add: le_diff_conv uv(1) x(1) uv(2) y(1))
immler@69619
  2286
    show "(\<Sum>i = 1..k1 + k2. ?uu i) = 1"  "(\<Sum>i = 1..k1 + k2. ?uu i *\<^sub>R ?xx i) = u *\<^sub>R x + v *\<^sub>R y"
immler@69619
  2287
      unfolding * sum.If_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]]
immler@69619
  2288
        sum.reindex[OF inj] Collect_mem_eq o_def
immler@69619
  2289
      unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] sum_distrib_left[symmetric]
immler@69619
  2290
      by (simp_all add: sum_distrib_left[symmetric]  x(2,3) y(2,3) uv(3))
immler@69619
  2291
  qed 
immler@69619
  2292
qed
immler@69619
  2293
immler@69619
  2294
lemma convex_hull_finite:
immler@69619
  2295
  fixes S :: "'a::real_vector set"
immler@69619
  2296
  assumes "finite S"
immler@69619
  2297
  shows "convex hull S = {y. \<exists>u. (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y}"
immler@69619
  2298
  (is "?HULL = _")
immler@69619
  2299
proof (rule hull_unique [OF _ convexI]; clarify)
immler@69619
  2300
  fix x
immler@69619
  2301
  assume "x \<in> S"
immler@69619
  2302
  then show "\<exists>u. (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> (\<Sum>x\<in>S. u x *\<^sub>R x) = x"
immler@69619
  2303
    by (rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) (auto simp: sum.delta'[OF assms] sum_delta''[OF assms])
immler@69619
  2304
next
immler@69619
  2305
  fix u v :: real
immler@69619
  2306
  assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"