src/HOL/Analysis/Convex.thy
author haftmann
Mon Jan 14 18:35:03 2019 +0000 (4 months ago)
changeset 69661 a03a63b81f44
parent 69619 3f7d8e05e0f2
child 69675 880ab0f27ddf
permissions -rw-r--r--
tuned proofs
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:
haftmann@69661
   616
  "convex ((+) a ` S)" if "convex S"
immler@69619
   617
proof -
haftmann@69661
   618
  have "(\<Union> x\<in> {a}. \<Union>y \<in> S. {x + y}) = (+) a ` S"
immler@69619
   619
    by auto
immler@69619
   620
  then show ?thesis
haftmann@69661
   621
    using convex_sums [OF convex_singleton [of a] that] by auto
immler@69619
   622
qed
immler@69619
   623
haftmann@69661
   624
lemma convex_translation_subtract:
haftmann@69661
   625
  "convex ((\<lambda>b. b - a) ` S)" if "convex S"
haftmann@69661
   626
  using convex_translation [of S "- a"] that by (simp cong: image_cong_simp)
haftmann@69661
   627
immler@69619
   628
lemma convex_affinity:
immler@69619
   629
  assumes "convex S"
immler@69619
   630
  shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` S)"
immler@69619
   631
proof -
immler@69619
   632
  have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` (*\<^sub>R) c ` S"
immler@69619
   633
    by auto
immler@69619
   634
  then show ?thesis
immler@69619
   635
    using convex_translation[OF convex_scaling[OF assms], of a c] by auto
immler@69619
   636
qed
immler@69619
   637
immler@69619
   638
lemma pos_is_convex: "convex {0 :: real <..}"
immler@69619
   639
  unfolding convex_alt
immler@69619
   640
proof safe
immler@69619
   641
  fix y x \<mu> :: real
immler@69619
   642
  assume *: "y > 0" "x > 0" "\<mu> \<ge> 0" "\<mu> \<le> 1"
immler@69619
   643
  {
immler@69619
   644
    assume "\<mu> = 0"
immler@69619
   645
    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y = y"
immler@69619
   646
      by simp
immler@69619
   647
    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
immler@69619
   648
      using * by simp
immler@69619
   649
  }
immler@69619
   650
  moreover
immler@69619
   651
  {
immler@69619
   652
    assume "\<mu> = 1"
immler@69619
   653
    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
immler@69619
   654
      using * by simp
immler@69619
   655
  }
immler@69619
   656
  moreover
immler@69619
   657
  {
immler@69619
   658
    assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
immler@69619
   659
    then have "\<mu> > 0" "(1 - \<mu>) > 0"
immler@69619
   660
      using * by auto
immler@69619
   661
    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
immler@69619
   662
      using * by (auto simp: add_pos_pos)
immler@69619
   663
  }
immler@69619
   664
  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0"
immler@69619
   665
    by fastforce
immler@69619
   666
qed
immler@69619
   667
immler@69619
   668
lemma convex_on_sum:
immler@69619
   669
  fixes a :: "'a \<Rightarrow> real"
immler@69619
   670
    and y :: "'a \<Rightarrow> 'b::real_vector"
immler@69619
   671
    and f :: "'b \<Rightarrow> real"
immler@69619
   672
  assumes "finite s" "s \<noteq> {}"
immler@69619
   673
    and "convex_on C f"
immler@69619
   674
    and "convex C"
immler@69619
   675
    and "(\<Sum> i \<in> s. a i) = 1"
immler@69619
   676
    and "\<And>i. i \<in> s \<Longrightarrow> a i \<ge> 0"
immler@69619
   677
    and "\<And>i. i \<in> s \<Longrightarrow> y i \<in> C"
immler@69619
   678
  shows "f (\<Sum> i \<in> s. a i *\<^sub>R y i) \<le> (\<Sum> i \<in> s. a i * f (y i))"
immler@69619
   679
  using assms
immler@69619
   680
proof (induct s arbitrary: a rule: finite_ne_induct)
immler@69619
   681
  case (singleton i)
immler@69619
   682
  then have ai: "a i = 1"
immler@69619
   683
    by auto
immler@69619
   684
  then show ?case
immler@69619
   685
    by auto
immler@69619
   686
next
immler@69619
   687
  case (insert i s)
immler@69619
   688
  then have "convex_on C f"
immler@69619
   689
    by simp
immler@69619
   690
  from this[unfolded convex_on_def, rule_format]
immler@69619
   691
  have conv: "\<And>x y \<mu>. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> 0 \<le> \<mu> \<Longrightarrow> \<mu> \<le> 1 \<Longrightarrow>
immler@69619
   692
      f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
immler@69619
   693
    by simp
immler@69619
   694
  show ?case
immler@69619
   695
  proof (cases "a i = 1")
immler@69619
   696
    case True
immler@69619
   697
    then have "(\<Sum> j \<in> s. a j) = 0"
immler@69619
   698
      using insert by auto
immler@69619
   699
    then have "\<And>j. j \<in> s \<Longrightarrow> a j = 0"
immler@69619
   700
      using insert by (fastforce simp: sum_nonneg_eq_0_iff)
immler@69619
   701
    then show ?thesis
immler@69619
   702
      using insert by auto
immler@69619
   703
  next
immler@69619
   704
    case False
immler@69619
   705
    from insert have yai: "y i \<in> C" "a i \<ge> 0"
immler@69619
   706
      by auto
immler@69619
   707
    have fis: "finite (insert i s)"
immler@69619
   708
      using insert by auto
immler@69619
   709
    then have ai1: "a i \<le> 1"
immler@69619
   710
      using sum_nonneg_leq_bound[of "insert i s" a] insert by simp
immler@69619
   711
    then have "a i < 1"
immler@69619
   712
      using False by auto
immler@69619
   713
    then have i0: "1 - a i > 0"
immler@69619
   714
      by auto
immler@69619
   715
    let ?a = "\<lambda>j. a j / (1 - a i)"
immler@69619
   716
    have a_nonneg: "?a j \<ge> 0" if "j \<in> s" for j
immler@69619
   717
      using i0 insert that by fastforce
immler@69619
   718
    have "(\<Sum> j \<in> insert i s. a j) = 1"
immler@69619
   719
      using insert by auto
immler@69619
   720
    then have "(\<Sum> j \<in> s. a j) = 1 - a i"
immler@69619
   721
      using sum.insert insert by fastforce
immler@69619
   722
    then have "(\<Sum> j \<in> s. a j) / (1 - a i) = 1"
immler@69619
   723
      using i0 by auto
immler@69619
   724
    then have a1: "(\<Sum> j \<in> s. ?a j) = 1"
immler@69619
   725
      unfolding sum_divide_distrib by simp
immler@69619
   726
    have "convex C" using insert by auto
immler@69619
   727
    then have asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
immler@69619
   728
      using insert convex_sum [OF \<open>finite s\<close> \<open>convex C\<close> a1 a_nonneg] by auto
immler@69619
   729
    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
   730
      using a_nonneg a1 insert by blast
immler@69619
   731
    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
   732
      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
   733
      by (auto simp only: add.commute)
immler@69619
   734
    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
   735
      using i0 by auto
immler@69619
   736
    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
   737
      using scaleR_right.sum[of "inverse (1 - a i)" "\<lambda> j. a j *\<^sub>R y j" s, symmetric]
immler@69619
   738
      by (auto simp: algebra_simps)
immler@69619
   739
    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
   740
      by (auto simp: divide_inverse)
immler@69619
   741
    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
   742
      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
   743
      by (auto simp: add.commute)
immler@69619
   744
    also have "\<dots> \<le> (1 - a i) * (\<Sum> j \<in> s. ?a j * f (y j)) + a i * f (y i)"
immler@69619
   745
      using add_right_mono [OF mult_left_mono [of _ _ "1 - a i",
immler@69619
   746
            OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"]
immler@69619
   747
      by simp
immler@69619
   748
    also have "\<dots> = (\<Sum> j \<in> s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)"
immler@69619
   749
      unfolding sum_distrib_left[of "1 - a i" "\<lambda> j. ?a j * f (y j)"]
immler@69619
   750
      using i0 by auto
immler@69619
   751
    also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)"
immler@69619
   752
      using i0 by auto
immler@69619
   753
    also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))"
immler@69619
   754
      using insert by auto
immler@69619
   755
    finally show ?thesis
immler@69619
   756
      by simp
immler@69619
   757
  qed
immler@69619
   758
qed
immler@69619
   759
immler@69619
   760
lemma convex_on_alt:
immler@69619
   761
  fixes C :: "'a::real_vector set"
immler@69619
   762
  assumes "convex C"
immler@69619
   763
  shows "convex_on C f \<longleftrightarrow>
immler@69619
   764
    (\<forall>x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1 \<longrightarrow>
immler@69619
   765
      f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y)"
immler@69619
   766
proof safe
immler@69619
   767
  fix x y
immler@69619
   768
  fix \<mu> :: real
immler@69619
   769
  assume *: "convex_on C f" "x \<in> C" "y \<in> C" "0 \<le> \<mu>" "\<mu> \<le> 1"
immler@69619
   770
  from this[unfolded convex_on_def, rule_format]
immler@69619
   771
  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
   772
    by auto
immler@69619
   773
  from this [of "\<mu>" "1 - \<mu>", simplified] *
immler@69619
   774
  show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
immler@69619
   775
    by auto
immler@69619
   776
next
immler@69619
   777
  assume *: "\<forall>x\<in>C. \<forall>y\<in>C. \<forall>\<mu>. 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow>
immler@69619
   778
    f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
immler@69619
   779
  {
immler@69619
   780
    fix x y
immler@69619
   781
    fix u v :: real
immler@69619
   782
    assume **: "x \<in> C" "y \<in> C" "u \<ge> 0" "v \<ge> 0" "u + v = 1"
immler@69619
   783
    then have[simp]: "1 - u = v" by auto
immler@69619
   784
    from *[rule_format, of x y u]
immler@69619
   785
    have "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y"
immler@69619
   786
      using ** by auto
immler@69619
   787
  }
immler@69619
   788
  then show "convex_on C f"
immler@69619
   789
    unfolding convex_on_def by auto
immler@69619
   790
qed
immler@69619
   791
immler@69619
   792
lemma convex_on_diff:
immler@69619
   793
  fixes f :: "real \<Rightarrow> real"
immler@69619
   794
  assumes f: "convex_on I f"
immler@69619
   795
    and I: "x \<in> I" "y \<in> I"
immler@69619
   796
    and t: "x < t" "t < y"
immler@69619
   797
  shows "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
immler@69619
   798
    and "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
immler@69619
   799
proof -
immler@69619
   800
  define a where "a \<equiv> (t - y) / (x - y)"
immler@69619
   801
  with t have "0 \<le> a" "0 \<le> 1 - a"
immler@69619
   802
    by (auto simp: field_simps)
immler@69619
   803
  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
   804
    by (auto simp: convex_on_def)
immler@69619
   805
  have "a * x + (1 - a) * y = a * (x - y) + y"
immler@69619
   806
    by (simp add: field_simps)
immler@69619
   807
  also have "\<dots> = t"
immler@69619
   808
    unfolding a_def using \<open>x < t\<close> \<open>t < y\<close> by simp
immler@69619
   809
  finally have "f t \<le> a * f x + (1 - a) * f y"
immler@69619
   810
    using cvx by simp
immler@69619
   811
  also have "\<dots> = a * (f x - f y) + f y"
immler@69619
   812
    by (simp add: field_simps)
immler@69619
   813
  finally have "f t - f y \<le> a * (f x - f y)"
immler@69619
   814
    by simp
immler@69619
   815
  with t show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
immler@69619
   816
    by (simp add: le_divide_eq divide_le_eq field_simps a_def)
immler@69619
   817
  with t show "(f x - f y) / (x - y) \<le> (f t - f y) / (t - y)"
immler@69619
   818
    by (simp add: le_divide_eq divide_le_eq field_simps)
immler@69619
   819
qed
immler@69619
   820
immler@69619
   821
lemma pos_convex_function:
immler@69619
   822
  fixes f :: "real \<Rightarrow> real"
immler@69619
   823
  assumes "convex C"
immler@69619
   824
    and leq: "\<And>x y. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> f' x * (y - x) \<le> f y - f x"
immler@69619
   825
  shows "convex_on C f"
immler@69619
   826
  unfolding convex_on_alt[OF assms(1)]
immler@69619
   827
  using assms
immler@69619
   828
proof safe
immler@69619
   829
  fix x y \<mu> :: real
immler@69619
   830
  let ?x = "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
immler@69619
   831
  assume *: "convex C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
immler@69619
   832
  then have "1 - \<mu> \<ge> 0" by auto
immler@69619
   833
  then have xpos: "?x \<in> C"
immler@69619
   834
    using * unfolding convex_alt by fastforce
immler@69619
   835
  have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x) \<ge>
immler@69619
   836
      \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
immler@69619
   837
    using add_mono [OF mult_left_mono [OF leq [OF xpos *(2)] \<open>\<mu> \<ge> 0\<close>]
immler@69619
   838
        mult_left_mono [OF leq [OF xpos *(3)] \<open>1 - \<mu> \<ge> 0\<close>]]
immler@69619
   839
    by auto
immler@69619
   840
  then have "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
immler@69619
   841
    by (auto simp: field_simps)
immler@69619
   842
  then show "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
immler@69619
   843
    using convex_on_alt by auto
immler@69619
   844
qed
immler@69619
   845
immler@69619
   846
lemma atMostAtLeast_subset_convex:
immler@69619
   847
  fixes C :: "real set"
immler@69619
   848
  assumes "convex C"
immler@69619
   849
    and "x \<in> C" "y \<in> C" "x < y"
immler@69619
   850
  shows "{x .. y} \<subseteq> C"
immler@69619
   851
proof safe
immler@69619
   852
  fix z assume z: "z \<in> {x .. y}"
immler@69619
   853
  have less: "z \<in> C" if *: "x < z" "z < y"
immler@69619
   854
  proof -
immler@69619
   855
    let ?\<mu> = "(y - z) / (y - x)"
immler@69619
   856
    have "0 \<le> ?\<mu>" "?\<mu> \<le> 1"
immler@69619
   857
      using assms * by (auto simp: field_simps)
immler@69619
   858
    then have comb: "?\<mu> * x + (1 - ?\<mu>) * y \<in> C"
immler@69619
   859
      using assms iffD1[OF convex_alt, rule_format, of C y x ?\<mu>]
immler@69619
   860
      by (simp add: algebra_simps)
immler@69619
   861
    have "?\<mu> * x + (1 - ?\<mu>) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"
immler@69619
   862
      by (auto simp: field_simps)
immler@69619
   863
    also have "\<dots> = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"
immler@69619
   864
      using assms by (simp only: add_divide_distrib) (auto simp: field_simps)
immler@69619
   865
    also have "\<dots> = z"
immler@69619
   866
      using assms by (auto simp: field_simps)
immler@69619
   867
    finally show ?thesis
immler@69619
   868
      using comb by auto
immler@69619
   869
  qed
immler@69619
   870
  show "z \<in> C"
immler@69619
   871
    using z less assms by (auto simp: le_less)
immler@69619
   872
qed
immler@69619
   873
immler@69619
   874
lemma f''_imp_f':
immler@69619
   875
  fixes f :: "real \<Rightarrow> real"
immler@69619
   876
  assumes "convex C"
immler@69619
   877
    and f': "\<And>x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
immler@69619
   878
    and f'': "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
immler@69619
   879
    and pos: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
immler@69619
   880
    and x: "x \<in> C"
immler@69619
   881
    and y: "y \<in> C"
immler@69619
   882
  shows "f' x * (y - x) \<le> f y - f x"
immler@69619
   883
  using assms
immler@69619
   884
proof -
immler@69619
   885
  have less_imp: "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
immler@69619
   886
    if *: "x \<in> C" "y \<in> C" "y > x" for x y :: real
immler@69619
   887
  proof -
immler@69619
   888
    from * have ge: "y - x > 0" "y - x \<ge> 0"
immler@69619
   889
      by auto
immler@69619
   890
    from * have le: "x - y < 0" "x - y \<le> 0"
immler@69619
   891
      by auto
immler@69619
   892
    then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1"
immler@69619
   893
      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
   894
          THEN f', THEN MVT2[OF \<open>x < y\<close>, rule_format, unfolded atLeastAtMost_iff[symmetric]]]
immler@69619
   895
      by auto
immler@69619
   896
    then have "z1 \<in> C"
immler@69619
   897
      using atMostAtLeast_subset_convex \<open>convex C\<close> \<open>x \<in> C\<close> \<open>y \<in> C\<close> \<open>x < y\<close>
immler@69619
   898
      by fastforce
immler@69619
   899
    from z1 have z1': "f x - f y = (x - y) * f' z1"
immler@69619
   900
      by (simp add: field_simps)
immler@69619
   901
    obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2"
immler@69619
   902
      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
   903
          THEN f'', THEN MVT2[OF \<open>x < z1\<close>, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
immler@69619
   904
      by auto
immler@69619
   905
    obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3"
immler@69619
   906
      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
   907
          THEN f'', THEN MVT2[OF \<open>z1 < y\<close>, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1
immler@69619
   908
      by auto
immler@69619
   909
    have "f' y - (f x - f y) / (x - y) = f' y - f' z1"
immler@69619
   910
      using * z1' by auto
immler@69619
   911
    also have "\<dots> = (y - z1) * f'' z3"
immler@69619
   912
      using z3 by auto
immler@69619
   913
    finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3"
immler@69619
   914
      by simp
immler@69619
   915
    have A': "y - z1 \<ge> 0"
immler@69619
   916
      using z1 by auto
immler@69619
   917
    have "z3 \<in> C"
immler@69619
   918
      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
   919
      by fastforce
immler@69619
   920
    then have B': "f'' z3 \<ge> 0"
immler@69619
   921
      using assms by auto
immler@69619
   922
    from A' B' have "(y - z1) * f'' z3 \<ge> 0"
immler@69619
   923
      by auto
immler@69619
   924
    from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0"
immler@69619
   925
      by auto
immler@69619
   926
    from mult_right_mono_neg[OF this le(2)]
immler@69619
   927
    have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
immler@69619
   928
      by (simp add: algebra_simps)
immler@69619
   929
    then have "f' y * (x - y) - (f x - f y) \<le> 0"
immler@69619
   930
      using le by auto
immler@69619
   931
    then have res: "f' y * (x - y) \<le> f x - f y"
immler@69619
   932
      by auto
immler@69619
   933
    have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
immler@69619
   934
      using * z1 by auto
immler@69619
   935
    also have "\<dots> = (z1 - x) * f'' z2"
immler@69619
   936
      using z2 by auto
immler@69619
   937
    finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2"
immler@69619
   938
      by simp
immler@69619
   939
    have A: "z1 - x \<ge> 0"
immler@69619
   940
      using z1 by auto
immler@69619
   941
    have "z2 \<in> C"
immler@69619
   942
      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
   943
      by fastforce
immler@69619
   944
    then have B: "f'' z2 \<ge> 0"
immler@69619
   945
      using assms by auto
immler@69619
   946
    from A B have "(z1 - x) * f'' z2 \<ge> 0"
immler@69619
   947
      by auto
immler@69619
   948
    with cool have "(f y - f x) / (y - x) - f' x \<ge> 0"
immler@69619
   949
      by auto
immler@69619
   950
    from mult_right_mono[OF this ge(2)]
immler@69619
   951
    have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
immler@69619
   952
      by (simp add: algebra_simps)
immler@69619
   953
    then have "f y - f x - f' x * (y - x) \<ge> 0"
immler@69619
   954
      using ge by auto
immler@69619
   955
    then show "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
immler@69619
   956
      using res by auto
immler@69619
   957
  qed
immler@69619
   958
  show ?thesis
immler@69619
   959
  proof (cases "x = y")
immler@69619
   960
    case True
immler@69619
   961
    with x y show ?thesis by auto
immler@69619
   962
  next
immler@69619
   963
    case False
immler@69619
   964
    with less_imp x y show ?thesis
immler@69619
   965
      by (auto simp: neq_iff)
immler@69619
   966
  qed
immler@69619
   967
qed
immler@69619
   968
immler@69619
   969
lemma f''_ge0_imp_convex:
immler@69619
   970
  fixes f :: "real \<Rightarrow> real"
immler@69619
   971
  assumes conv: "convex C"
immler@69619
   972
    and f': "\<And>x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)"
immler@69619
   973
    and f'': "\<And>x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
immler@69619
   974
    and pos: "\<And>x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
immler@69619
   975
  shows "convex_on C f"
immler@69619
   976
  using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function
immler@69619
   977
  by fastforce
immler@69619
   978
immler@69619
   979
lemma minus_log_convex:
immler@69619
   980
  fixes b :: real
immler@69619
   981
  assumes "b > 1"
immler@69619
   982
  shows "convex_on {0 <..} (\<lambda> x. - log b x)"
immler@69619
   983
proof -
immler@69619
   984
  have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)"
immler@69619
   985
    using DERIV_log by auto
immler@69619
   986
  then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
immler@69619
   987
    by (auto simp: DERIV_minus)
immler@69619
   988
  have "\<And>z::real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
immler@69619
   989
    using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
immler@69619
   990
  from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
immler@69619
   991
  have "\<And>z::real. z > 0 \<Longrightarrow>
immler@69619
   992
    DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
immler@69619
   993
    by auto
immler@69619
   994
  then have f''0: "\<And>z::real. z > 0 \<Longrightarrow>
immler@69619
   995
    DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
immler@69619
   996
    unfolding inverse_eq_divide by (auto simp: mult.assoc)
immler@69619
   997
  have f''_ge0: "\<And>z::real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
immler@69619
   998
    using \<open>b > 1\<close> by (auto intro!: less_imp_le)
immler@69619
   999
  from f''_ge0_imp_convex[OF pos_is_convex, unfolded greaterThan_iff, OF f' f''0 f''_ge0]
immler@69619
  1000
  show ?thesis
immler@69619
  1001
    by auto
immler@69619
  1002
qed
immler@69619
  1003
immler@69619
  1004
immler@69619
  1005
subsection%unimportant \<open>Convexity of real functions\<close>
immler@69619
  1006
immler@69619
  1007
lemma convex_on_realI:
immler@69619
  1008
  assumes "connected A"
immler@69619
  1009
    and "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
immler@69619
  1010
    and "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f' x \<le> f' y"
immler@69619
  1011
  shows "convex_on A f"
immler@69619
  1012
proof (rule convex_on_linorderI)
immler@69619
  1013
  fix t x y :: real
immler@69619
  1014
  assume t: "t > 0" "t < 1"
immler@69619
  1015
  assume xy: "x \<in> A" "y \<in> A" "x < y"
immler@69619
  1016
  define z where "z = (1 - t) * x + t * y"
immler@69619
  1017
  with \<open>connected A\<close> and xy have ivl: "{x..y} \<subseteq> A"
immler@69619
  1018
    using connected_contains_Icc by blast
immler@69619
  1019
immler@69619
  1020
  from xy t have xz: "z > x"
immler@69619
  1021
    by (simp add: z_def algebra_simps)
immler@69619
  1022
  have "y - z = (1 - t) * (y - x)"
immler@69619
  1023
    by (simp add: z_def algebra_simps)
immler@69619
  1024
  also from xy t have "\<dots> > 0"
immler@69619
  1025
    by (intro mult_pos_pos) simp_all
immler@69619
  1026
  finally have yz: "z < y"
immler@69619
  1027
    by simp
immler@69619
  1028
immler@69619
  1029
  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
  1030
    by (intro MVT2) (auto intro!: assms(2))
immler@69619
  1031
  then obtain \<xi> where \<xi>: "\<xi> > x" "\<xi> < z" "f' \<xi> = (f z - f x) / (z - x)"
immler@69619
  1032
    by auto
immler@69619
  1033
  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
  1034
    by (intro MVT2) (auto intro!: assms(2))
immler@69619
  1035
  then obtain \<eta> where \<eta>: "\<eta> > z" "\<eta> < y" "f' \<eta> = (f y - f z) / (y - z)"
immler@69619
  1036
    by auto
immler@69619
  1037
immler@69619
  1038
  from \<eta>(3) have "(f y - f z) / (y - z) = f' \<eta>" ..
immler@69619
  1039
  also from \<xi> \<eta> ivl have "\<xi> \<in> A" "\<eta> \<in> A"
immler@69619
  1040
    by auto
immler@69619
  1041
  with \<xi> \<eta> have "f' \<eta> \<ge> f' \<xi>"
immler@69619
  1042
    by (intro assms(3)) auto
immler@69619
  1043
  also from \<xi>(3) have "f' \<xi> = (f z - f x) / (z - x)" .
immler@69619
  1044
  finally have "(f y - f z) * (z - x) \<ge> (f z - f x) * (y - z)"
immler@69619
  1045
    using xz yz by (simp add: field_simps)
immler@69619
  1046
  also have "z - x = t * (y - x)"
immler@69619
  1047
    by (simp add: z_def algebra_simps)
immler@69619
  1048
  also have "y - z = (1 - t) * (y - x)"
immler@69619
  1049
    by (simp add: z_def algebra_simps)
immler@69619
  1050
  finally have "(f y - f z) * t \<ge> (f z - f x) * (1 - t)"
immler@69619
  1051
    using xy by simp
immler@69619
  1052
  then show "(1 - t) * f x + t * f y \<ge> f ((1 - t) *\<^sub>R x + t *\<^sub>R y)"
immler@69619
  1053
    by (simp add: z_def algebra_simps)
immler@69619
  1054
qed
immler@69619
  1055
immler@69619
  1056
lemma convex_on_inverse:
immler@69619
  1057
  assumes "A \<subseteq> {0<..}"
immler@69619
  1058
  shows "convex_on A (inverse :: real \<Rightarrow> real)"
immler@69619
  1059
proof (rule convex_on_subset[OF _ assms], intro convex_on_realI[of _ _ "\<lambda>x. -inverse (x^2)"])
immler@69619
  1060
  fix u v :: real
immler@69619
  1061
  assume "u \<in> {0<..}" "v \<in> {0<..}" "u \<le> v"
immler@69619
  1062
  with assms show "-inverse (u^2) \<le> -inverse (v^2)"
immler@69619
  1063
    by (intro le_imp_neg_le le_imp_inverse_le power_mono) (simp_all)
immler@69619
  1064
qed (insert assms, auto intro!: derivative_eq_intros simp: divide_simps power2_eq_square)
immler@69619
  1065
immler@69619
  1066
lemma convex_onD_Icc':
immler@69619
  1067
  assumes "convex_on {x..y} f" "c \<in> {x..y}"
immler@69619
  1068
  defines "d \<equiv> y - x"
immler@69619
  1069
  shows "f c \<le> (f y - f x) / d * (c - x) + f x"
immler@69619
  1070
proof (cases x y rule: linorder_cases)
immler@69619
  1071
  case less
immler@69619
  1072
  then have d: "d > 0"
immler@69619
  1073
    by (simp add: d_def)
immler@69619
  1074
  from assms(2) less have A: "0 \<le> (c - x) / d" "(c - x) / d \<le> 1"
immler@69619
  1075
    by (simp_all add: d_def divide_simps)
immler@69619
  1076
  have "f c = f (x + (c - x) * 1)"
immler@69619
  1077
    by simp
immler@69619
  1078
  also from less have "1 = ((y - x) / d)"
immler@69619
  1079
    by (simp add: d_def)
immler@69619
  1080
  also from d have "x + (c - x) * \<dots> = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y"
immler@69619
  1081
    by (simp add: field_simps)
immler@69619
  1082
  also have "f \<dots> \<le> (1 - (c - x) / d) * f x + (c - x) / d * f y"
immler@69619
  1083
    using assms less by (intro convex_onD_Icc) simp_all
immler@69619
  1084
  also from d have "\<dots> = (f y - f x) / d * (c - x) + f x"
immler@69619
  1085
    by (simp add: field_simps)
immler@69619
  1086
  finally show ?thesis .
immler@69619
  1087
qed (insert assms(2), simp_all)
immler@69619
  1088
immler@69619
  1089
lemma convex_onD_Icc'':
immler@69619
  1090
  assumes "convex_on {x..y} f" "c \<in> {x..y}"
immler@69619
  1091
  defines "d \<equiv> y - x"
immler@69619
  1092
  shows "f c \<le> (f x - f y) / d * (y - c) + f y"
immler@69619
  1093
proof (cases x y rule: linorder_cases)
immler@69619
  1094
  case less
immler@69619
  1095
  then have d: "d > 0"
immler@69619
  1096
    by (simp add: d_def)
immler@69619
  1097
  from assms(2) less have A: "0 \<le> (y - c) / d" "(y - c) / d \<le> 1"
immler@69619
  1098
    by (simp_all add: d_def divide_simps)
immler@69619
  1099
  have "f c = f (y - (y - c) * 1)"
immler@69619
  1100
    by simp
immler@69619
  1101
  also from less have "1 = ((y - x) / d)"
immler@69619
  1102
    by (simp add: d_def)
immler@69619
  1103
  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
  1104
    by (simp add: field_simps)
immler@69619
  1105
  also have "f \<dots> \<le> (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y"
immler@69619
  1106
    using assms less by (intro convex_onD_Icc) (simp_all add: field_simps)
immler@69619
  1107
  also from d have "\<dots> = (f x - f y) / d * (y - c) + f y"
immler@69619
  1108
    by (simp add: field_simps)
immler@69619
  1109
  finally show ?thesis .
immler@69619
  1110
qed (insert assms(2), simp_all)
immler@69619
  1111
haftmann@69661
  1112
lemma convex_translation_eq [simp]:
haftmann@69661
  1113
  "convex ((+) a ` s) \<longleftrightarrow> convex s"
immler@69619
  1114
  by (metis convex_translation translation_galois)
immler@69619
  1115
haftmann@69661
  1116
lemma convex_translation_subtract_eq [simp]:
haftmann@69661
  1117
  "convex ((\<lambda>b. b - a) ` s) \<longleftrightarrow> convex s"
haftmann@69661
  1118
  using convex_translation_eq [of "- a"] by (simp cong: image_cong_simp)
haftmann@69661
  1119
immler@69619
  1120
lemma convex_linear_image_eq [simp]:
immler@69619
  1121
    fixes f :: "'a::real_vector \<Rightarrow> 'b::real_vector"
immler@69619
  1122
    shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> convex (f ` s) \<longleftrightarrow> convex s"
immler@69619
  1123
    by (metis (no_types) convex_linear_image convex_linear_vimage inj_vimage_image_eq)
immler@69619
  1124
immler@69619
  1125
lemma fst_linear: "linear fst"
immler@69619
  1126
  unfolding linear_iff by (simp add: algebra_simps)
immler@69619
  1127
immler@69619
  1128
lemma snd_linear: "linear snd"
immler@69619
  1129
  unfolding linear_iff by (simp add: algebra_simps)
immler@69619
  1130
immler@69619
  1131
lemma fst_snd_linear: "linear (\<lambda>(x,y). x + y)"
immler@69619
  1132
  unfolding linear_iff by (simp add: algebra_simps)
immler@69619
  1133
immler@69619
  1134
lemma vector_choose_size:
immler@69619
  1135
  assumes "0 \<le> c"
immler@69619
  1136
  obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c"
immler@69619
  1137
proof -
immler@69619
  1138
  obtain a::'a where "a \<noteq> 0"
immler@69619
  1139
    using UNIV_not_singleton UNIV_eq_I set_zero singletonI by fastforce
immler@69619
  1140
  then show ?thesis
immler@69619
  1141
    by (rule_tac x="scaleR (c / norm a) a" in that) (simp add: assms)
immler@69619
  1142
qed
immler@69619
  1143
immler@69619
  1144
lemma vector_choose_dist:
immler@69619
  1145
  assumes "0 \<le> c"
immler@69619
  1146
  obtains y :: "'a::{real_normed_vector, perfect_space}" where "dist x y = c"
immler@69619
  1147
by (metis add_diff_cancel_left' assms dist_commute dist_norm vector_choose_size)
immler@69619
  1148
immler@69619
  1149
lemma sum_delta_notmem:
immler@69619
  1150
  assumes "x \<notin> s"
immler@69619
  1151
  shows "sum (\<lambda>y. if (y = x) then P x else Q y) s = sum Q s"
immler@69619
  1152
    and "sum (\<lambda>y. if (x = y) then P x else Q y) s = sum Q s"
immler@69619
  1153
    and "sum (\<lambda>y. if (y = x) then P y else Q y) s = sum Q s"
immler@69619
  1154
    and "sum (\<lambda>y. if (x = y) then P y else Q y) s = sum Q s"
immler@69619
  1155
  apply (rule_tac [!] sum.cong)
immler@69619
  1156
  using assms
immler@69619
  1157
  apply auto
immler@69619
  1158
  done
immler@69619
  1159
immler@69619
  1160
lemma sum_delta'':
immler@69619
  1161
  fixes s::"'a::real_vector set"
immler@69619
  1162
  assumes "finite s"
immler@69619
  1163
  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
  1164
proof -
immler@69619
  1165
  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
  1166
    by auto
immler@69619
  1167
  show ?thesis
immler@69619
  1168
    unfolding * using sum.delta[OF assms, of y "\<lambda>x. f x *\<^sub>R x"] by auto
immler@69619
  1169
qed
immler@69619
  1170
immler@69619
  1171
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
  1172
  by (fact if_distrib)
immler@69619
  1173
immler@69619
  1174
lemma dist_triangle_eq:
immler@69619
  1175
  fixes x y z :: "'a::real_inner"
immler@69619
  1176
  shows "dist x z = dist x y + dist y z \<longleftrightarrow>
immler@69619
  1177
    norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
immler@69619
  1178
proof -
immler@69619
  1179
  have *: "x - y + (y - z) = x - z" by auto
immler@69619
  1180
  show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *]
immler@69619
  1181
    by (auto simp:norm_minus_commute)
immler@69619
  1182
qed
immler@69619
  1183
immler@69619
  1184
immler@69619
  1185
subsection \<open>Affine set and affine hull\<close>
immler@69619
  1186
immler@69619
  1187
definition%important affine :: "'a::real_vector set \<Rightarrow> bool"
immler@69619
  1188
  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
  1189
immler@69619
  1190
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
  1191
  unfolding affine_def by (metis eq_diff_eq')
immler@69619
  1192
immler@69619
  1193
lemma affine_empty [iff]: "affine {}"
immler@69619
  1194
  unfolding affine_def by auto
immler@69619
  1195
immler@69619
  1196
lemma affine_sing [iff]: "affine {x}"
immler@69619
  1197
  unfolding affine_alt by (auto simp: scaleR_left_distrib [symmetric])
immler@69619
  1198
immler@69619
  1199
lemma affine_UNIV [iff]: "affine UNIV"
immler@69619
  1200
  unfolding affine_def by auto
immler@69619
  1201
immler@69619
  1202
lemma affine_Inter [intro]: "(\<And>s. s\<in>f \<Longrightarrow> affine s) \<Longrightarrow> affine (\<Inter>f)"
immler@69619
  1203
  unfolding affine_def by auto
immler@69619
  1204
immler@69619
  1205
lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
immler@69619
  1206
  unfolding affine_def by auto
immler@69619
  1207
immler@69619
  1208
lemma affine_scaling: "affine s \<Longrightarrow> affine (image (\<lambda>x. c *\<^sub>R x) s)"
immler@69619
  1209
  apply (clarsimp simp add: affine_def)
immler@69619
  1210
  apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI)
immler@69619
  1211
  apply (auto simp: algebra_simps)
immler@69619
  1212
  done
immler@69619
  1213
immler@69619
  1214
lemma affine_affine_hull [simp]: "affine(affine hull s)"
immler@69619
  1215
  unfolding hull_def
immler@69619
  1216
  using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] by auto
immler@69619
  1217
immler@69619
  1218
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
immler@69619
  1219
  by (metis affine_affine_hull hull_same)
immler@69619
  1220
immler@69619
  1221
lemma affine_hyperplane: "affine {x. a \<bullet> x = b}"
immler@69619
  1222
  by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)
immler@69619
  1223
immler@69619
  1224
immler@69619
  1225
subsubsection%unimportant \<open>Some explicit formulations\<close>
immler@69619
  1226
immler@69619
  1227
text "Formalized by Lars Schewe."
immler@69619
  1228
immler@69619
  1229
lemma affine:
immler@69619
  1230
  fixes V::"'a::real_vector set"
immler@69619
  1231
  shows "affine V \<longleftrightarrow>
immler@69619
  1232
         (\<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
  1233
proof -
immler@69619
  1234
  have "u *\<^sub>R x + v *\<^sub>R y \<in> V" if "x \<in> V" "y \<in> V" "u + v = (1::real)"
immler@69619
  1235
    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
  1236
  proof (cases "x = y")
immler@69619
  1237
    case True
immler@69619
  1238
    then show ?thesis
immler@69619
  1239
      using that by (metis scaleR_add_left scaleR_one)
immler@69619
  1240
  next
immler@69619
  1241
    case False
immler@69619
  1242
    then show ?thesis
immler@69619
  1243
      using that *[of "{x,y}" "\<lambda>w. if w = x then u else v"] by auto
immler@69619
  1244
  qed
immler@69619
  1245
  moreover have "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V"
immler@69619
  1246
                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
  1247
                  and "finite S" "S \<noteq> {}" "S \<subseteq> V" "sum u S = 1" for S u
immler@69619
  1248
  proof -
immler@69619
  1249
    define n where "n = card S"
immler@69619
  1250
    consider "card S = 0" | "card S = 1" | "card S = 2" | "card S > 2" by linarith
immler@69619
  1251
    then show "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V"
immler@69619
  1252
    proof cases
immler@69619
  1253
      assume "card S = 1"
immler@69619
  1254
      then obtain a where "S={a}"
immler@69619
  1255
        by (auto simp: card_Suc_eq)
immler@69619
  1256
      then show ?thesis
immler@69619
  1257
        using that by simp
immler@69619
  1258
    next
immler@69619
  1259
      assume "card S = 2"
immler@69619
  1260
      then obtain a b where "S = {a, b}"
immler@69619
  1261
        by (metis Suc_1 card_1_singletonE card_Suc_eq)
immler@69619
  1262
      then show ?thesis
immler@69619
  1263
        using *[of a b] that
immler@69619
  1264
        by (auto simp: sum_clauses(2))
immler@69619
  1265
    next
immler@69619
  1266
      assume "card S > 2"
immler@69619
  1267
      then show ?thesis using that n_def
immler@69619
  1268
      proof (induct n arbitrary: u S)
immler@69619
  1269
        case 0
immler@69619
  1270
        then show ?case by auto
immler@69619
  1271
      next
immler@69619
  1272
        case (Suc n u S)
immler@69619
  1273
        have "sum u S = card S" if "\<not> (\<exists>x\<in>S. u x \<noteq> 1)"
immler@69619
  1274
          using that unfolding card_eq_sum by auto
immler@69619
  1275
        with Suc.prems obtain x where "x \<in> S" and x: "u x \<noteq> 1" by force
immler@69619
  1276
        have c: "card (S - {x}) = card S - 1"
immler@69619
  1277
          by (simp add: Suc.prems(3) \<open>x \<in> S\<close>)
immler@69619
  1278
        have "sum u (S - {x}) = 1 - u x"
immler@69619
  1279
          by (simp add: Suc.prems sum_diff1_ring \<open>x \<in> S\<close>)
immler@69619
  1280
        with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1"
immler@69619
  1281
          by auto
immler@69619
  1282
        have inV: "(\<Sum>y\<in>S - {x}. (inverse (1 - u x) * u y) *\<^sub>R y) \<in> V"
immler@69619
  1283
        proof (cases "card (S - {x}) > 2")
immler@69619
  1284
          case True
immler@69619
  1285
          then have S: "S - {x} \<noteq> {}" "card (S - {x}) = n"
immler@69619
  1286
            using Suc.prems c by force+
immler@69619
  1287
          show ?thesis
immler@69619
  1288
          proof (rule Suc.hyps)
immler@69619
  1289
            show "(\<Sum>a\<in>S - {x}. inverse (1 - u x) * u a) = 1"
immler@69619
  1290
              by (auto simp: eq1 sum_distrib_left[symmetric])
immler@69619
  1291
          qed (use S Suc.prems True in auto)
immler@69619
  1292
        next
immler@69619
  1293
          case False
immler@69619
  1294
          then have "card (S - {x}) = Suc (Suc 0)"
immler@69619
  1295
            using Suc.prems c by auto
immler@69619
  1296
          then obtain a b where ab: "(S - {x}) = {a, b}" "a\<noteq>b"
immler@69619
  1297
            unfolding card_Suc_eq by auto
immler@69619
  1298
          then show ?thesis
immler@69619
  1299
            using eq1 \<open>S \<subseteq> V\<close>
immler@69619
  1300
            by (auto simp: sum_distrib_left distrib_left intro!: Suc.prems(2)[of a b])
immler@69619
  1301
        qed
immler@69619
  1302
        have "u x + (1 - u x) = 1 \<Longrightarrow>
immler@69619
  1303
          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
  1304
          by (rule Suc.prems) (use \<open>x \<in> S\<close> Suc.prems inV in \<open>auto simp: scaleR_right.sum\<close>)
immler@69619
  1305
        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
  1306
          by (meson Suc.prems(3) sum.remove \<open>x \<in> S\<close>)
immler@69619
  1307
        ultimately show "(\<Sum>x\<in>S. u x *\<^sub>R x) \<in> V"
immler@69619
  1308
          by (simp add: x)
immler@69619
  1309
      qed
immler@69619
  1310
    qed (use \<open>S\<noteq>{}\<close> \<open>finite S\<close> in auto)
immler@69619
  1311
  qed
immler@69619
  1312
  ultimately show ?thesis
immler@69619
  1313
    unfolding affine_def by meson
immler@69619
  1314
qed
immler@69619
  1315
immler@69619
  1316
immler@69619
  1317
lemma affine_hull_explicit:
immler@69619
  1318
  "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
  1319
  (is "_ = ?rhs")
immler@69619
  1320
proof (rule hull_unique)
immler@69619
  1321
  show "p \<subseteq> ?rhs"
immler@69619
  1322
  proof (intro subsetI CollectI exI conjI)
immler@69619
  1323
    show "\<And>x. sum (\<lambda>z. 1) {x} = 1"
immler@69619
  1324
      by auto
immler@69619
  1325
  qed auto
immler@69619
  1326
  show "?rhs \<subseteq> T" if "p \<subseteq> T" "affine T" for T
immler@69619
  1327
    using that unfolding affine by blast
immler@69619
  1328
  show "affine ?rhs"
immler@69619
  1329
    unfolding affine_def
immler@69619
  1330
  proof clarify
immler@69619
  1331
    fix u v :: real and sx ux sy uy
immler@69619
  1332
    assume uv: "u + v = 1"
immler@69619
  1333
      and x: "finite sx" "sx \<noteq> {}" "sx \<subseteq> p" "sum ux sx = (1::real)"
immler@69619
  1334
      and y: "finite sy" "sy \<noteq> {}" "sy \<subseteq> p" "sum uy sy = (1::real)" 
immler@69619
  1335
    have **: "(sx \<union> sy) \<inter> sx = sx" "(sx \<union> sy) \<inter> sy = sy"
immler@69619
  1336
      by auto
immler@69619
  1337
    show "\<exists>S w. finite S \<and> S \<noteq> {} \<and> S \<subseteq> p \<and>
immler@69619
  1338
        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
  1339
    proof (intro exI conjI)
immler@69619
  1340
      show "finite (sx \<union> sy)"
immler@69619
  1341
        using x y by auto
immler@69619
  1342
      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
  1343
        using x y uv
immler@69619
  1344
        by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] sum_distrib_left [symmetric] **)
immler@69619
  1345
      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
  1346
          = (\<Sum>i\<in>sx. (u * ux i) *\<^sub>R i) + (\<Sum>i\<in>sy. (v * uy i) *\<^sub>R i)"
immler@69619
  1347
        using x y
immler@69619
  1348
        unfolding scaleR_left_distrib scaleR_zero_left if_smult
immler@69619
  1349
        by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric]  **)
immler@69619
  1350
      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
  1351
        unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by blast
immler@69619
  1352
      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
  1353
                  = 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
  1354
    qed (use x y in auto)
immler@69619
  1355
  qed
immler@69619
  1356
qed
immler@69619
  1357
immler@69619
  1358
lemma affine_hull_finite:
immler@69619
  1359
  assumes "finite S"
immler@69619
  1360
  shows "affine hull S = {y. \<exists>u. sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
immler@69619
  1361
proof -
immler@69619
  1362
  have *: "\<exists>h. sum h S = 1 \<and> (\<Sum>v\<in>S. h v *\<^sub>R v) = x" 
immler@69619
  1363
    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
  1364
  proof -
immler@69619
  1365
    have "S \<inter> F = F"
immler@69619
  1366
      using that by auto
immler@69619
  1367
    show ?thesis
immler@69619
  1368
    proof (intro exI conjI)
immler@69619
  1369
      show "(\<Sum>x\<in>S. if x \<in> F then u x else 0) = 1"
immler@69619
  1370
        by (metis (mono_tags, lifting) \<open>S \<inter> F = F\<close> assms sum.inter_restrict sum)
immler@69619
  1371
      show "(\<Sum>v\<in>S. (if v \<in> F then u v else 0) *\<^sub>R v) = x"
immler@69619
  1372
        by (simp add: if_smult cong: if_cong) (metis (no_types) \<open>S \<inter> F = F\<close> assms sum.inter_restrict x)
immler@69619
  1373
    qed
immler@69619
  1374
  qed
immler@69619
  1375
  show ?thesis
immler@69619
  1376
    unfolding affine_hull_explicit using assms
immler@69619
  1377
    by (fastforce dest: *)
immler@69619
  1378
qed
immler@69619
  1379
immler@69619
  1380
immler@69619
  1381
subsubsection%unimportant \<open>Stepping theorems and hence small special cases\<close>
immler@69619
  1382
immler@69619
  1383
lemma affine_hull_empty[simp]: "affine hull {} = {}"
immler@69619
  1384
  by simp
immler@69619
  1385
immler@69619
  1386
lemma affine_hull_finite_step:
immler@69619
  1387
  fixes y :: "'a::real_vector"
immler@69619
  1388
  shows "finite S \<Longrightarrow>
immler@69619
  1389
      (\<exists>u. sum u (insert a S) = w \<and> sum (\<lambda>x. u x *\<^sub>R x) (insert a S) = y) \<longleftrightarrow>
immler@69619
  1390
      (\<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
  1391
proof -
immler@69619
  1392
  assume fin: "finite S"
immler@69619
  1393
  show "?lhs = ?rhs"
immler@69619
  1394
  proof
immler@69619
  1395
    assume ?lhs
immler@69619
  1396
    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
  1397
      by auto
immler@69619
  1398
    show ?rhs
immler@69619
  1399
    proof (cases "a \<in> S")
immler@69619
  1400
      case True
immler@69619
  1401
      then show ?thesis
immler@69619
  1402
        using u by (simp add: insert_absorb) (metis diff_zero real_vector.scale_zero_left)
immler@69619
  1403
    next
immler@69619
  1404
      case False
immler@69619
  1405
      show ?thesis
immler@69619
  1406
        by (rule exI [where x="u a"]) (use u fin False in auto)
immler@69619
  1407
    qed
immler@69619
  1408
  next
immler@69619
  1409
    assume ?rhs
immler@69619
  1410
    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
  1411
      by auto
immler@69619
  1412
    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
  1413
      by auto
immler@69619
  1414
    show ?lhs
immler@69619
  1415
    proof (cases "a \<in> S")
immler@69619
  1416
      case True
immler@69619
  1417
      show ?thesis
immler@69619
  1418
        by (rule exI [where x="\<lambda>x. (if x=a then v else 0) + u x"])
immler@69619
  1419
           (simp add: True scaleR_left_distrib sum.distrib sum_clauses fin vu * cong: if_cong)
immler@69619
  1420
    next
immler@69619
  1421
      case False
immler@69619
  1422
      then show ?thesis
immler@69619
  1423
        apply (rule_tac x="\<lambda>x. if x=a then v else u x" in exI) 
immler@69619
  1424
        apply (simp add: vu sum_clauses(2)[OF fin] *)
immler@69619
  1425
        by (simp add: sum_delta_notmem(3) vu)
immler@69619
  1426
    qed
immler@69619
  1427
  qed
immler@69619
  1428
qed
immler@69619
  1429
immler@69619
  1430
lemma affine_hull_2:
immler@69619
  1431
  fixes a b :: "'a::real_vector"
immler@69619
  1432
  shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}"
immler@69619
  1433
  (is "?lhs = ?rhs")
immler@69619
  1434
proof -
immler@69619
  1435
  have *:
immler@69619
  1436
    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
immler@69619
  1437
    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
immler@69619
  1438
  have "?lhs = {y. \<exists>u. sum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}"
immler@69619
  1439
    using affine_hull_finite[of "{a,b}"] by auto
immler@69619
  1440
  also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}"
immler@69619
  1441
    by (simp add: affine_hull_finite_step[of "{b}" a])
immler@69619
  1442
  also have "\<dots> = ?rhs" unfolding * by auto
immler@69619
  1443
  finally show ?thesis by auto
immler@69619
  1444
qed
immler@69619
  1445
immler@69619
  1446
lemma affine_hull_3:
immler@69619
  1447
  fixes a b c :: "'a::real_vector"
immler@69619
  1448
  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
  1449
proof -
immler@69619
  1450
  have *:
immler@69619
  1451
    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
immler@69619
  1452
    "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
immler@69619
  1453
  show ?thesis
immler@69619
  1454
    apply (simp add: affine_hull_finite affine_hull_finite_step)
immler@69619
  1455
    unfolding *
immler@69619
  1456
    apply safe
immler@69619
  1457
     apply (metis add.assoc)
immler@69619
  1458
    apply (rule_tac x=u in exI, force)
immler@69619
  1459
    done
immler@69619
  1460
qed
immler@69619
  1461
immler@69619
  1462
lemma mem_affine:
immler@69619
  1463
  assumes "affine S" "x \<in> S" "y \<in> S" "u + v = 1"
immler@69619
  1464
  shows "u *\<^sub>R x + v *\<^sub>R y \<in> S"
immler@69619
  1465
  using assms affine_def[of S] by auto
immler@69619
  1466
immler@69619
  1467
lemma mem_affine_3:
immler@69619
  1468
  assumes "affine S" "x \<in> S" "y \<in> S" "z \<in> S" "u + v + w = 1"
immler@69619
  1469
  shows "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \<in> S"
immler@69619
  1470
proof -
immler@69619
  1471
  have "u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z \<in> affine hull {x, y, z}"
immler@69619
  1472
    using affine_hull_3[of x y z] assms by auto
immler@69619
  1473
  moreover
immler@69619
  1474
  have "affine hull {x, y, z} \<subseteq> affine hull S"
immler@69619
  1475
    using hull_mono[of "{x, y, z}" "S"] assms by auto
immler@69619
  1476
  moreover
immler@69619
  1477
  have "affine hull S = S"
immler@69619
  1478
    using assms affine_hull_eq[of S] by auto
immler@69619
  1479
  ultimately show ?thesis by auto
immler@69619
  1480
qed
immler@69619
  1481
immler@69619
  1482
lemma mem_affine_3_minus:
immler@69619
  1483
  assumes "affine S" "x \<in> S" "y \<in> S" "z \<in> S"
immler@69619
  1484
  shows "x + v *\<^sub>R (y-z) \<in> S"
immler@69619
  1485
  using mem_affine_3[of S x y z 1 v "-v"] assms
immler@69619
  1486
  by (simp add: algebra_simps)
immler@69619
  1487
immler@69619
  1488
corollary mem_affine_3_minus2:
immler@69619
  1489
    "\<lbrakk>affine S; x \<in> S; y \<in> S; z \<in> S\<rbrakk> \<Longrightarrow> x - v *\<^sub>R (y-z) \<in> S"
immler@69619
  1490
  by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left)
immler@69619
  1491
immler@69619
  1492
immler@69619
  1493
subsubsection%unimportant \<open>Some relations between affine hull and subspaces\<close>
immler@69619
  1494
immler@69619
  1495
lemma affine_hull_insert_subset_span:
immler@69619
  1496
  "affine hull (insert a S) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> S}}"
immler@69619
  1497
proof -
immler@69619
  1498
  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
  1499
    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
  1500
    for x F u
immler@69619
  1501
  proof -
immler@69619
  1502
    have *: "(\<lambda>x. x - a) ` (F - {a}) \<subseteq> {x - a |x. x \<in> S}"
immler@69619
  1503
      using that by auto
immler@69619
  1504
    show ?thesis
immler@69619
  1505
    proof (intro exI conjI)
immler@69619
  1506
      show "finite ((\<lambda>x. x - a) ` (F - {a}))"
immler@69619
  1507
        by (simp add: that(1))
immler@69619
  1508
      show "(\<Sum>v\<in>(\<lambda>x. x - a) ` (F - {a}). u(v+a) *\<^sub>R v) = x-a"
immler@69619
  1509
        by (simp add: sum.reindex[unfolded inj_on_def] algebra_simps
immler@69619
  1510
            sum_subtractf scaleR_left.sum[symmetric] sum_diff1 that)
immler@69619
  1511
    qed (use \<open>F \<subseteq> insert a S\<close> in auto)
immler@69619
  1512
  qed
immler@69619
  1513
  then show ?thesis
immler@69619
  1514
    unfolding affine_hull_explicit span_explicit by blast
immler@69619
  1515
qed
immler@69619
  1516
immler@69619
  1517
lemma affine_hull_insert_span:
immler@69619
  1518
  assumes "a \<notin> S"
immler@69619
  1519
  shows "affine hull (insert a S) = {a + v | v . v \<in> span {x - a | x.  x \<in> S}}"
immler@69619
  1520
proof -
immler@69619
  1521
  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
  1522
    if "v \<in> span {x - a |x. x \<in> S}" "y = a + v" for y v
immler@69619
  1523
  proof -
immler@69619
  1524
    from that
immler@69619
  1525
    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
  1526
      unfolding span_explicit by auto
immler@69619
  1527
    define F where "F = (\<lambda>x. x + a) ` T"
immler@69619
  1528
    have F: "finite F" "F \<subseteq> S" "(\<Sum>v\<in>F. u (v - a) *\<^sub>R (v - a)) = y - a"
immler@69619
  1529
      unfolding F_def using u by (auto simp: sum.reindex[unfolded inj_on_def])
immler@69619
  1530
    have *: "F \<inter> {a} = {}" "F \<inter> - {a} = F"
immler@69619
  1531
      using F assms by auto
immler@69619
  1532
    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
  1533
      apply (rule_tac x = "insert a F" in exI)
immler@69619
  1534
      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
  1535
      using assms F
immler@69619
  1536
      apply (auto simp:  sum_clauses sum.If_cases if_smult sum_subtractf scaleR_left.sum algebra_simps *)
immler@69619
  1537
      done
immler@69619
  1538
  qed
immler@69619
  1539
  show ?thesis
immler@69619
  1540
    by (intro subset_antisym affine_hull_insert_subset_span) (auto simp: affine_hull_explicit dest!: *)
immler@69619
  1541
qed
immler@69619
  1542
immler@69619
  1543
lemma affine_hull_span:
immler@69619
  1544
  assumes "a \<in> S"
immler@69619
  1545
  shows "affine hull S = {a + v | v. v \<in> span {x - a | x. x \<in> S - {a}}}"
immler@69619
  1546
  using affine_hull_insert_span[of a "S - {a}", unfolded insert_Diff[OF assms]] by auto
immler@69619
  1547
immler@69619
  1548
immler@69619
  1549
subsubsection%unimportant \<open>Parallel affine sets\<close>
immler@69619
  1550
immler@69619
  1551
definition affine_parallel :: "'a::real_vector set \<Rightarrow> 'a::real_vector set \<Rightarrow> bool"
immler@69619
  1552
  where "affine_parallel S T \<longleftrightarrow> (\<exists>a. T = (\<lambda>x. a + x) ` S)"
immler@69619
  1553
immler@69619
  1554
lemma affine_parallel_expl_aux:
immler@69619
  1555
  fixes S T :: "'a::real_vector set"
immler@69619
  1556
  assumes "\<And>x. x \<in> S \<longleftrightarrow> a + x \<in> T"
immler@69619
  1557
  shows "T = (\<lambda>x. a + x) ` S"
immler@69619
  1558
proof -
immler@69619
  1559
  have "x \<in> ((\<lambda>x. a + x) ` S)" if "x \<in> T" for x
immler@69619
  1560
    using that
immler@69619
  1561
    by (simp add: image_iff) (metis add.commute diff_add_cancel assms)
immler@69619
  1562
  moreover have "T \<ge> (\<lambda>x. a + x) ` S"
immler@69619
  1563
    using assms by auto
immler@69619
  1564
  ultimately show ?thesis by auto
immler@69619
  1565
qed
immler@69619
  1566
immler@69619
  1567
lemma affine_parallel_expl: "affine_parallel S T \<longleftrightarrow> (\<exists>a. \<forall>x. x \<in> S \<longleftrightarrow> a + x \<in> T)"
immler@69619
  1568
  unfolding affine_parallel_def
immler@69619
  1569
  using affine_parallel_expl_aux[of S _ T] by auto
immler@69619
  1570
immler@69619
  1571
lemma affine_parallel_reflex: "affine_parallel S S"
immler@69619
  1572
  unfolding affine_parallel_def
immler@69619
  1573
  using image_add_0 by blast
immler@69619
  1574
immler@69619
  1575
lemma affine_parallel_commut:
immler@69619
  1576
  assumes "affine_parallel A B"
immler@69619
  1577
  shows "affine_parallel B A"
immler@69619
  1578
proof -
immler@69619
  1579
  from assms obtain a where B: "B = (\<lambda>x. a + x) ` A"
immler@69619
  1580
    unfolding affine_parallel_def by auto
immler@69619
  1581
  have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
immler@69619
  1582
  from B show ?thesis
immler@69619
  1583
    using translation_galois [of B a A]
immler@69619
  1584
    unfolding affine_parallel_def by auto
immler@69619
  1585
qed
immler@69619
  1586
immler@69619
  1587
lemma affine_parallel_assoc:
immler@69619
  1588
  assumes "affine_parallel A B"
immler@69619
  1589
    and "affine_parallel B C"
immler@69619
  1590
  shows "affine_parallel A C"
immler@69619
  1591
proof -
immler@69619
  1592
  from assms obtain ab where "B = (\<lambda>x. ab + x) ` A"
immler@69619
  1593
    unfolding affine_parallel_def by auto
immler@69619
  1594
  moreover
immler@69619
  1595
  from assms obtain bc where "C = (\<lambda>x. bc + x) ` B"
immler@69619
  1596
    unfolding affine_parallel_def by auto
immler@69619
  1597
  ultimately show ?thesis
immler@69619
  1598
    using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto
immler@69619
  1599
qed
immler@69619
  1600
immler@69619
  1601
lemma affine_translation_aux:
immler@69619
  1602
  fixes a :: "'a::real_vector"
immler@69619
  1603
  assumes "affine ((\<lambda>x. a + x) ` S)"
immler@69619
  1604
  shows "affine S"
immler@69619
  1605
proof -
immler@69619
  1606
  {
immler@69619
  1607
    fix x y u v
immler@69619
  1608
    assume xy: "x \<in> S" "y \<in> S" "(u :: real) + v = 1"
immler@69619
  1609
    then have "(a + x) \<in> ((\<lambda>x. a + x) ` S)" "(a + y) \<in> ((\<lambda>x. a + x) ` S)"
immler@69619
  1610
      by auto
immler@69619
  1611
    then have h1: "u *\<^sub>R  (a + x) + v *\<^sub>R (a + y) \<in> (\<lambda>x. a + x) ` S"
immler@69619
  1612
      using xy assms unfolding affine_def by auto
immler@69619
  1613
    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
  1614
      by (simp add: algebra_simps)
immler@69619
  1615
    also have "\<dots> = a + (u *\<^sub>R x + v *\<^sub>R y)"
immler@69619
  1616
      using \<open>u + v = 1\<close> by auto
immler@69619
  1617
    ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) \<in> (\<lambda>x. a + x) ` S"
immler@69619
  1618
      using h1 by auto
immler@69619
  1619
    then have "u *\<^sub>R x + v *\<^sub>R y \<in> S" by auto
immler@69619
  1620
  }
immler@69619
  1621
  then show ?thesis unfolding affine_def by auto
immler@69619
  1622
qed
immler@69619
  1623
immler@69619
  1624
lemma affine_translation:
haftmann@69661
  1625
  "affine S \<longleftrightarrow> affine ((+) a ` S)" for a :: "'a::real_vector"
haftmann@69661
  1626
proof
haftmann@69661
  1627
  show "affine ((+) a ` S)" if "affine S"
haftmann@69661
  1628
    using that translation_assoc [of "- a" a S]
haftmann@69661
  1629
    by (auto intro: affine_translation_aux [of "- a" "((+) a ` S)"])
haftmann@69661
  1630
  show "affine S" if "affine ((+) a ` S)"
haftmann@69661
  1631
    using that by (rule affine_translation_aux)
immler@69619
  1632
qed
immler@69619
  1633
immler@69619
  1634
lemma parallel_is_affine:
immler@69619
  1635
  fixes S T :: "'a::real_vector set"
immler@69619
  1636
  assumes "affine S" "affine_parallel S T"
immler@69619
  1637
  shows "affine T"
immler@69619
  1638
proof -
immler@69619
  1639
  from assms obtain a where "T = (\<lambda>x. a + x) ` S"
immler@69619
  1640
    unfolding affine_parallel_def by auto
immler@69619
  1641
  then show ?thesis
immler@69619
  1642
    using affine_translation assms by auto
immler@69619
  1643
qed
immler@69619
  1644
immler@69619
  1645
lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
immler@69619
  1646
  unfolding subspace_def affine_def by auto
immler@69619
  1647
immler@69619
  1648
immler@69619
  1649
subsubsection%unimportant \<open>Subspace parallel to an affine set\<close>
immler@69619
  1650
immler@69619
  1651
lemma subspace_affine: "subspace S \<longleftrightarrow> affine S \<and> 0 \<in> S"
immler@69619
  1652
proof -
immler@69619
  1653
  have h0: "subspace S \<Longrightarrow> affine S \<and> 0 \<in> S"
immler@69619
  1654
    using subspace_imp_affine[of S] subspace_0 by auto
immler@69619
  1655
  {
immler@69619
  1656
    assume assm: "affine S \<and> 0 \<in> S"
immler@69619
  1657
    {
immler@69619
  1658
      fix c :: real
immler@69619
  1659
      fix x
immler@69619
  1660
      assume x: "x \<in> S"
immler@69619
  1661
      have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto
immler@69619
  1662
      moreover
immler@69619
  1663
      have "(1 - c) *\<^sub>R 0 + c *\<^sub>R x \<in> S"
immler@69619
  1664
        using affine_alt[of S] assm x by auto
immler@69619
  1665
      ultimately have "c *\<^sub>R x \<in> S" by auto
immler@69619
  1666
    }
immler@69619
  1667
    then have h1: "\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S" by auto
immler@69619
  1668
immler@69619
  1669
    {
immler@69619
  1670
      fix x y
immler@69619
  1671
      assume xy: "x \<in> S" "y \<in> S"
immler@69619
  1672
      define u where "u = (1 :: real)/2"
immler@69619
  1673
      have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)"
immler@69619
  1674
        by auto
immler@69619
  1675
      moreover
immler@69619
  1676
      have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y"
immler@69619
  1677
        by (simp add: algebra_simps)
immler@69619
  1678
      moreover
immler@69619
  1679
      have "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> S"
immler@69619
  1680
        using affine_alt[of S] assm xy by auto
immler@69619
  1681
      ultimately
immler@69619
  1682
      have "(1/2) *\<^sub>R (x+y) \<in> S"
immler@69619
  1683
        using u_def by auto
immler@69619
  1684
      moreover
immler@69619
  1685
      have "x + y = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))"
immler@69619
  1686
        by auto
immler@69619
  1687
      ultimately
immler@69619
  1688
      have "x + y \<in> S"
immler@69619
  1689
        using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
immler@69619
  1690
    }
immler@69619
  1691
    then have "\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S"
immler@69619
  1692
      by auto
immler@69619
  1693
    then have "subspace S"
immler@69619
  1694
      using h1 assm unfolding subspace_def by auto
immler@69619
  1695
  }
immler@69619
  1696
  then show ?thesis using h0 by metis
immler@69619
  1697
qed
immler@69619
  1698
immler@69619
  1699
lemma affine_diffs_subspace:
immler@69619
  1700
  assumes "affine S" "a \<in> S"
immler@69619
  1701
  shows "subspace ((\<lambda>x. (-a)+x) ` S)"
immler@69619
  1702
proof -
immler@69619
  1703
  have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
immler@69619
  1704
  have "affine ((\<lambda>x. (-a)+x) ` S)"
immler@69619
  1705
    using  affine_translation assms by auto
immler@69619
  1706
  moreover have "0 \<in> ((\<lambda>x. (-a)+x) ` S)"
immler@69619
  1707
    using assms exI[of "(\<lambda>x. x\<in>S \<and> -a+x = 0)" a] by auto
immler@69619
  1708
  ultimately show ?thesis using subspace_affine by auto
immler@69619
  1709
qed
immler@69619
  1710
haftmann@69661
  1711
lemma affine_diffs_subspace_subtract:
haftmann@69661
  1712
  "subspace ((\<lambda>x. x - a) ` S)" if "affine S" "a \<in> S"
haftmann@69661
  1713
  using that affine_diffs_subspace [of _ a] by simp
haftmann@69661
  1714
immler@69619
  1715
lemma parallel_subspace_explicit:
immler@69619
  1716
  assumes "affine S"
immler@69619
  1717
    and "a \<in> S"
immler@69619
  1718
  assumes "L \<equiv> {y. \<exists>x \<in> S. (-a) + x = y}"
immler@69619
  1719
  shows "subspace L \<and> affine_parallel S L"
immler@69619
  1720
proof -
immler@69619
  1721
  from assms have "L = plus (- a) ` S" by auto
immler@69619
  1722
  then have par: "affine_parallel S L"
immler@69619
  1723
    unfolding affine_parallel_def ..
immler@69619
  1724
  then have "affine L" using assms parallel_is_affine by auto
immler@69619
  1725
  moreover have "0 \<in> L"
immler@69619
  1726
    using assms by auto
immler@69619
  1727
  ultimately show ?thesis
immler@69619
  1728
    using subspace_affine par by auto
immler@69619
  1729
qed
immler@69619
  1730
immler@69619
  1731
lemma parallel_subspace_aux:
immler@69619
  1732
  assumes "subspace A"
immler@69619
  1733
    and "subspace B"
immler@69619
  1734
    and "affine_parallel A B"
immler@69619
  1735
  shows "A \<supseteq> B"
immler@69619
  1736
proof -
immler@69619
  1737
  from assms obtain a where a: "\<forall>x. x \<in> A \<longleftrightarrow> a + x \<in> B"
immler@69619
  1738
    using affine_parallel_expl[of A B] by auto
immler@69619
  1739
  then have "-a \<in> A"
immler@69619
  1740
    using assms subspace_0[of B] by auto
immler@69619
  1741
  then have "a \<in> A"
immler@69619
  1742
    using assms subspace_neg[of A "-a"] by auto
immler@69619
  1743
  then show ?thesis
immler@69619
  1744
    using assms a unfolding subspace_def by auto
immler@69619
  1745
qed
immler@69619
  1746
immler@69619
  1747
lemma parallel_subspace:
immler@69619
  1748
  assumes "subspace A"
immler@69619
  1749
    and "subspace B"
immler@69619
  1750
    and "affine_parallel A B"
immler@69619
  1751
  shows "A = B"
immler@69619
  1752
proof
immler@69619
  1753
  show "A \<supseteq> B"
immler@69619
  1754
    using assms parallel_subspace_aux by auto
immler@69619
  1755
  show "A \<subseteq> B"
immler@69619
  1756
    using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto
immler@69619
  1757
qed
immler@69619
  1758
immler@69619
  1759
lemma affine_parallel_subspace:
immler@69619
  1760
  assumes "affine S" "S \<noteq> {}"
immler@69619
  1761
  shows "\<exists>!L. subspace L \<and> affine_parallel S L"
immler@69619
  1762
proof -
immler@69619
  1763
  have ex: "\<exists>L. subspace L \<and> affine_parallel S L"
immler@69619
  1764
    using assms parallel_subspace_explicit by auto
immler@69619
  1765
  {
immler@69619
  1766
    fix L1 L2
immler@69619
  1767
    assume ass: "subspace L1 \<and> affine_parallel S L1" "subspace L2 \<and> affine_parallel S L2"
immler@69619
  1768
    then have "affine_parallel L1 L2"
immler@69619
  1769
      using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto
immler@69619
  1770
    then have "L1 = L2"
immler@69619
  1771
      using ass parallel_subspace by auto
immler@69619
  1772
  }
immler@69619
  1773
  then show ?thesis using ex by auto
immler@69619
  1774
qed
immler@69619
  1775
immler@69619
  1776
immler@69619
  1777
subsection \<open>Cones\<close>
immler@69619
  1778
immler@69619
  1779
definition%important cone :: "'a::real_vector set \<Rightarrow> bool"
immler@69619
  1780
  where "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. c *\<^sub>R x \<in> s)"
immler@69619
  1781
immler@69619
  1782
lemma cone_empty[intro, simp]: "cone {}"
immler@69619
  1783
  unfolding cone_def by auto
immler@69619
  1784
immler@69619
  1785
lemma cone_univ[intro, simp]: "cone UNIV"
immler@69619
  1786
  unfolding cone_def by auto
immler@69619
  1787
immler@69619
  1788
lemma cone_Inter[intro]: "\<forall>s\<in>f. cone s \<Longrightarrow> cone (\<Inter>f)"
immler@69619
  1789
  unfolding cone_def by auto
immler@69619
  1790
immler@69619
  1791
lemma subspace_imp_cone: "subspace S \<Longrightarrow> cone S"
immler@69619
  1792
  by (simp add: cone_def subspace_scale)
immler@69619
  1793
immler@69619
  1794
immler@69619
  1795
subsubsection \<open>Conic hull\<close>
immler@69619
  1796
immler@69619
  1797
lemma cone_cone_hull: "cone (cone hull s)"
immler@69619
  1798
  unfolding hull_def by auto
immler@69619
  1799
immler@69619
  1800
lemma cone_hull_eq: "cone hull s = s \<longleftrightarrow> cone s"
immler@69619
  1801
  apply (rule hull_eq)
immler@69619
  1802
  using cone_Inter
immler@69619
  1803
  unfolding subset_eq
immler@69619
  1804
  apply auto
immler@69619
  1805
  done
immler@69619
  1806
immler@69619
  1807
lemma mem_cone:
immler@69619
  1808
  assumes "cone S" "x \<in> S" "c \<ge> 0"
immler@69619
  1809
  shows "c *\<^sub>R x \<in> S"
immler@69619
  1810
  using assms cone_def[of S] by auto
immler@69619
  1811
immler@69619
  1812
lemma cone_contains_0:
immler@69619
  1813
  assumes "cone S"
immler@69619
  1814
  shows "S \<noteq> {} \<longleftrightarrow> 0 \<in> S"
immler@69619
  1815
proof -
immler@69619
  1816
  {
immler@69619
  1817
    assume "S \<noteq> {}"
immler@69619
  1818
    then obtain a where "a \<in> S" by auto
immler@69619
  1819
    then have "0 \<in> S"
immler@69619
  1820
      using assms mem_cone[of S a 0] by auto
immler@69619
  1821
  }
immler@69619
  1822
  then show ?thesis by auto
immler@69619
  1823
qed
immler@69619
  1824
immler@69619
  1825
lemma cone_0: "cone {0}"
immler@69619
  1826
  unfolding cone_def by auto
immler@69619
  1827
immler@69619
  1828
lemma cone_Union[intro]: "(\<forall>s\<in>f. cone s) \<longrightarrow> cone (\<Union>f)"
immler@69619
  1829
  unfolding cone_def by blast
immler@69619
  1830
immler@69619
  1831
lemma cone_iff:
immler@69619
  1832
  assumes "S \<noteq> {}"
immler@69619
  1833
  shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
immler@69619
  1834
proof -
immler@69619
  1835
  {
immler@69619
  1836
    assume "cone S"
immler@69619
  1837
    {
immler@69619
  1838
      fix c :: real
immler@69619
  1839
      assume "c > 0"
immler@69619
  1840
      {
immler@69619
  1841
        fix x
immler@69619
  1842
        assume "x \<in> S"
immler@69619
  1843
        then have "x \<in> ((*\<^sub>R) c) ` S"
immler@69619
  1844
          unfolding image_def
immler@69619
  1845
          using \<open>cone S\<close> \<open>c>0\<close> mem_cone[of S x "1/c"]
immler@69619
  1846
            exI[of "(\<lambda>t. t \<in> S \<and> x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"]
immler@69619
  1847
          by auto
immler@69619
  1848
      }
immler@69619
  1849
      moreover
immler@69619
  1850
      {
immler@69619
  1851
        fix x
immler@69619
  1852
        assume "x \<in> ((*\<^sub>R) c) ` S"
immler@69619
  1853
        then have "x \<in> S"
immler@69619
  1854
          using \<open>cone S\<close> \<open>c > 0\<close>
immler@69619
  1855
          unfolding cone_def image_def \<open>c > 0\<close> by auto
immler@69619
  1856
      }
immler@69619
  1857
      ultimately have "((*\<^sub>R) c) ` S = S" by auto
immler@69619
  1858
    }
immler@69619
  1859
    then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
immler@69619
  1860
      using \<open>cone S\<close> cone_contains_0[of S] assms by auto
immler@69619
  1861
  }
immler@69619
  1862
  moreover
immler@69619
  1863
  {
immler@69619
  1864
    assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ((*\<^sub>R) c) ` S = S)"
immler@69619
  1865
    {
immler@69619
  1866
      fix x
immler@69619
  1867
      assume "x \<in> S"
immler@69619
  1868
      fix c1 :: real
immler@69619
  1869
      assume "c1 \<ge> 0"
immler@69619
  1870
      then have "c1 = 0 \<or> c1 > 0" by auto
immler@69619
  1871
      then have "c1 *\<^sub>R x \<in> S" using a \<open>x \<in> S\<close> by auto
immler@69619
  1872
    }
immler@69619
  1873
    then have "cone S" unfolding cone_def by auto
immler@69619
  1874
  }
immler@69619
  1875
  ultimately show ?thesis by blast
immler@69619
  1876
qed
immler@69619
  1877
immler@69619
  1878
lemma cone_hull_empty: "cone hull {} = {}"
immler@69619
  1879
  by (metis cone_empty cone_hull_eq)
immler@69619
  1880
immler@69619
  1881
lemma cone_hull_empty_iff: "S = {} \<longleftrightarrow> cone hull S = {}"
immler@69619
  1882
  by (metis bot_least cone_hull_empty hull_subset xtrans(5))
immler@69619
  1883
immler@69619
  1884
lemma cone_hull_contains_0: "S \<noteq> {} \<longleftrightarrow> 0 \<in> cone hull S"
immler@69619
  1885
  using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S]
immler@69619
  1886
  by auto
immler@69619
  1887
immler@69619
  1888
lemma mem_cone_hull:
immler@69619
  1889
  assumes "x \<in> S" "c \<ge> 0"
immler@69619
  1890
  shows "c *\<^sub>R x \<in> cone hull S"
immler@69619
  1891
  by (metis assms cone_cone_hull hull_inc mem_cone)
immler@69619
  1892
immler@69619
  1893
proposition cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
immler@69619
  1894
  (is "?lhs = ?rhs")
immler@69619
  1895
proof -
immler@69619
  1896
  {
immler@69619
  1897
    fix x
immler@69619
  1898
    assume "x \<in> ?rhs"
immler@69619
  1899
    then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S"
immler@69619
  1900
      by auto
immler@69619
  1901
    fix c :: real
immler@69619
  1902
    assume c: "c \<ge> 0"
immler@69619
  1903
    then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx"
immler@69619
  1904
      using x by (simp add: algebra_simps)
immler@69619
  1905
    moreover
immler@69619
  1906
    have "c * cx \<ge> 0" using c x by auto
immler@69619
  1907
    ultimately
immler@69619
  1908
    have "c *\<^sub>R x \<in> ?rhs" using x by auto
immler@69619
  1909
  }
immler@69619
  1910
  then have "cone ?rhs"
immler@69619
  1911
    unfolding cone_def by auto
immler@69619
  1912
  then have "?rhs \<in> Collect cone"
immler@69619
  1913
    unfolding mem_Collect_eq by auto
immler@69619
  1914
  {
immler@69619
  1915
    fix x
immler@69619
  1916
    assume "x \<in> S"
immler@69619
  1917
    then have "1 *\<^sub>R x \<in> ?rhs"
immler@69619
  1918
      apply auto
immler@69619
  1919
      apply (rule_tac x = 1 in exI, auto)
immler@69619
  1920
      done
immler@69619
  1921
    then have "x \<in> ?rhs" by auto
immler@69619
  1922
  }
immler@69619
  1923
  then have "S \<subseteq> ?rhs" by auto
immler@69619
  1924
  then have "?lhs \<subseteq> ?rhs"
immler@69619
  1925
    using \<open>?rhs \<in> Collect cone\<close> hull_minimal[of S "?rhs" "cone"] by auto
immler@69619
  1926
  moreover
immler@69619
  1927
  {
immler@69619
  1928
    fix x
immler@69619
  1929
    assume "x \<in> ?rhs"
immler@69619
  1930
    then obtain cx :: real and xx where x: "x = cx *\<^sub>R xx" "cx \<ge> 0" "xx \<in> S"
immler@69619
  1931
      by auto
immler@69619
  1932
    then have "xx \<in> cone hull S"
immler@69619
  1933
      using hull_subset[of S] by auto
immler@69619
  1934
    then have "x \<in> ?lhs"
immler@69619
  1935
      using x cone_cone_hull[of S] cone_def[of "cone hull S"] by auto
immler@69619
  1936
  }
immler@69619
  1937
  ultimately show ?thesis by auto
immler@69619
  1938
qed
immler@69619
  1939
immler@69619
  1940
immler@69619
  1941
subsection \<open>Affine dependence and consequential theorems\<close>
immler@69619
  1942
immler@69619
  1943
text "Formalized by Lars Schewe."
immler@69619
  1944
immler@69619
  1945
definition%important affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
immler@69619
  1946
  where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
immler@69619
  1947
immler@69619
  1948
lemma affine_dependent_subset:
immler@69619
  1949
   "\<lbrakk>affine_dependent s; s \<subseteq> t\<rbrakk> \<Longrightarrow> affine_dependent t"
immler@69619
  1950
apply (simp add: affine_dependent_def Bex_def)
immler@69619
  1951
apply (blast dest: hull_mono [OF Diff_mono [OF _ subset_refl]])
immler@69619
  1952
done
immler@69619
  1953
immler@69619
  1954
lemma affine_independent_subset:
immler@69619
  1955
  shows "\<lbrakk>\<not> affine_dependent t; s \<subseteq> t\<rbrakk> \<Longrightarrow> \<not> affine_dependent s"
immler@69619
  1956
by (metis affine_dependent_subset)
immler@69619
  1957
immler@69619
  1958
lemma affine_independent_Diff:
immler@69619
  1959
   "\<not> affine_dependent s \<Longrightarrow> \<not> affine_dependent(s - t)"
immler@69619
  1960
by (meson Diff_subset affine_dependent_subset)
immler@69619
  1961
immler@69619
  1962
proposition affine_dependent_explicit:
immler@69619
  1963
  "affine_dependent p \<longleftrightarrow>
immler@69619
  1964
    (\<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
  1965
proof -
immler@69619
  1966
  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
  1967
    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
  1968
  proof (intro exI conjI)
immler@69619
  1969
    have "x \<notin> S" 
immler@69619
  1970
      using that by auto
immler@69619
  1971
    then show "(\<Sum>v \<in> insert x S. if v = x then - 1 else u v) = 0"
immler@69619
  1972
      using that by (simp add: sum_delta_notmem)
immler@69619
  1973
    show "(\<Sum>w \<in> insert x S. (if w = x then - 1 else u w) *\<^sub>R w) = 0"
immler@69619
  1974
      using that \<open>x \<notin> S\<close> by (simp add: if_smult sum_delta_notmem cong: if_cong)
immler@69619
  1975
  qed (use that in auto)
immler@69619
  1976
  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
  1977
    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
  1978
  proof (intro bexI exI conjI)
immler@69619
  1979
    have "S \<noteq> {v}"
immler@69619
  1980
      using that by auto
immler@69619
  1981
    then show "S - {v} \<noteq> {}"
immler@69619
  1982
      using that by auto
immler@69619
  1983
    show "(\<Sum>x \<in> S - {v}. - (1 / u v) * u x) = 1"
immler@69619
  1984
      unfolding sum_distrib_left[symmetric] sum_diff1[OF \<open>finite S\<close>] by (simp add: that)
immler@69619
  1985
    show "(\<Sum>x\<in>S - {v}. (- (1 / u v) * u x) *\<^sub>R x) = v"
immler@69619
  1986
      unfolding sum_distrib_left [symmetric] scaleR_scaleR[symmetric]
immler@69619
  1987
                scaleR_right.sum [symmetric] sum_diff1[OF \<open>finite S\<close>] 
immler@69619
  1988
      using that by auto
immler@69619
  1989
    show "S - {v} \<subseteq> p - {v}"
immler@69619
  1990
      using that by auto
immler@69619
  1991
  qed (use that in auto)
immler@69619
  1992
  ultimately show ?thesis
immler@69619
  1993
    unfolding affine_dependent_def affine_hull_explicit by auto
immler@69619
  1994
qed
immler@69619
  1995
immler@69619
  1996
lemma affine_dependent_explicit_finite:
immler@69619
  1997
  fixes S :: "'a::real_vector set"
immler@69619
  1998
  assumes "finite S"
immler@69619
  1999
  shows "affine_dependent S \<longleftrightarrow>
immler@69619
  2000
    (\<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
  2001
  (is "?lhs = ?rhs")
immler@69619
  2002
proof
immler@69619
  2003
  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
  2004
    by auto
immler@69619
  2005
  assume ?lhs
immler@69619
  2006
  then obtain t u v where
immler@69619
  2007
    "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
  2008
    unfolding affine_dependent_explicit by auto
immler@69619
  2009
  then show ?rhs
immler@69619
  2010
    apply (rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
immler@69619
  2011
    apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF \<open>t\<subseteq>S\<close>])
immler@69619
  2012
    done
immler@69619
  2013
next
immler@69619
  2014
  assume ?rhs
immler@69619
  2015
  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
  2016
    by auto
immler@69619
  2017
  then show ?lhs unfolding affine_dependent_explicit
immler@69619
  2018
    using assms by auto
immler@69619
  2019
qed
immler@69619
  2020
immler@69619
  2021
immler@69619
  2022
subsection%unimportant \<open>Connectedness of convex sets\<close>
immler@69619
  2023
immler@69619
  2024
lemma connectedD:
immler@69619
  2025
  "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
  2026
  by (rule Topological_Spaces.topological_space_class.connectedD)
immler@69619
  2027
immler@69619
  2028
lemma convex_connected:
immler@69619
  2029
  fixes S :: "'a::real_normed_vector set"
immler@69619
  2030
  assumes "convex S"
immler@69619
  2031
  shows "connected S"
immler@69619
  2032
proof (rule connectedI)
immler@69619
  2033
  fix A B
immler@69619
  2034
  assume "open A" "open B" "A \<inter> B \<inter> S = {}" "S \<subseteq> A \<union> B"
immler@69619
  2035
  moreover
immler@69619
  2036
  assume "A \<inter> S \<noteq> {}" "B \<inter> S \<noteq> {}"
immler@69619
  2037
  then obtain a b where a: "a \<in> A" "a \<in> S" and b: "b \<in> B" "b \<in> S" by auto
immler@69619
  2038
  define f where [abs_def]: "f u = u *\<^sub>R a + (1 - u) *\<^sub>R b" for u
immler@69619
  2039
  then have "continuous_on {0 .. 1} f"
immler@69619
  2040
    by (auto intro!: continuous_intros)
immler@69619
  2041
  then have "connected (f ` {0 .. 1})"
immler@69619
  2042
    by (auto intro!: connected_continuous_image)
immler@69619
  2043
  note connectedD[OF this, of A B]
immler@69619
  2044
  moreover have "a \<in> A \<inter> f ` {0 .. 1}"
immler@69619
  2045
    using a by (auto intro!: image_eqI[of _ _ 1] simp: f_def)
immler@69619
  2046
  moreover have "b \<in> B \<inter> f ` {0 .. 1}"
immler@69619
  2047
    using b by (auto intro!: image_eqI[of _ _ 0] simp: f_def)
immler@69619
  2048
  moreover have "f ` {0 .. 1} \<subseteq> S"
immler@69619
  2049
    using \<open>convex S\<close> a b unfolding convex_def f_def by auto
immler@69619
  2050
  ultimately show False by auto
immler@69619
  2051
qed
immler@69619
  2052
immler@69619
  2053
corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
immler@69619
  2054
  by (simp add: convex_connected)
immler@69619
  2055
immler@69619
  2056
lemma convex_prod:
immler@69619
  2057
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> convex {x. P i x}"
immler@69619
  2058
  shows "convex {x. \<forall>i\<in>Basis. P i (x\<bullet>i)}"
immler@69619
  2059
  using assms unfolding convex_def
immler@69619
  2060
  by (auto simp: inner_add_left)
immler@69619
  2061
immler@69619
  2062
lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (\<forall>i\<in>Basis. 0 \<le> x\<bullet>i)}"
immler@69619
  2063
  by (rule convex_prod) (simp add: atLeast_def[symmetric] convex_real_interval)
immler@69619
  2064
immler@69619
  2065
subsection \<open>Convex hull\<close>
immler@69619
  2066
immler@69619
  2067
lemma convex_convex_hull [iff]: "convex (convex hull s)"
immler@69619
  2068
  unfolding hull_def
immler@69619
  2069
  using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"]
immler@69619
  2070
  by auto
immler@69619
  2071
immler@69619
  2072
lemma convex_hull_subset:
immler@69619
  2073
    "s \<subseteq> convex hull t \<Longrightarrow> convex hull s \<subseteq> convex hull t"
immler@69619
  2074
  by (simp add: convex_convex_hull subset_hull)
immler@69619
  2075
immler@69619
  2076
lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
immler@69619
  2077
  by (metis convex_convex_hull hull_same)
immler@69619
  2078
immler@69619
  2079
subsubsection%unimportant \<open>Convex hull is "preserved" by a linear function\<close>
immler@69619
  2080
immler@69619
  2081
lemma convex_hull_linear_image:
immler@69619
  2082
  assumes f: "linear f"
immler@69619
  2083
  shows "f ` (convex hull s) = convex hull (f ` s)"
immler@69619
  2084
proof
immler@69619
  2085
  show "convex hull (f ` s) \<subseteq> f ` (convex hull s)"
immler@69619
  2086
    by (intro hull_minimal image_mono hull_subset convex_linear_image assms convex_convex_hull)
immler@69619
  2087
  show "f ` (convex hull s) \<subseteq> convex hull (f ` s)"
immler@69619
  2088
  proof (unfold image_subset_iff_subset_vimage, rule hull_minimal)
immler@69619
  2089
    show "s \<subseteq> f -` (convex hull (f ` s))"
immler@69619
  2090
      by (fast intro: hull_inc)
immler@69619
  2091
    show "convex (f -` (convex hull (f ` s)))"
immler@69619
  2092
      by (intro convex_linear_vimage [OF f] convex_convex_hull)
immler@69619
  2093
  qed
immler@69619
  2094
qed
immler@69619
  2095
immler@69619
  2096
lemma in_convex_hull_linear_image:
immler@69619
  2097
  assumes "linear f"
immler@69619
  2098
    and "x \<in> convex hull s"
immler@69619
  2099
  shows "f x \<in> convex hull (f ` s)"
immler@69619
  2100
  using convex_hull_linear_image[OF assms(1)] assms(2) by auto
immler@69619
  2101
immler@69619
  2102
lemma convex_hull_Times:
immler@69619
  2103
  "convex hull (s \<times> t) = (convex hull s) \<times> (convex hull t)"
immler@69619
  2104
proof
immler@69619
  2105
  show "convex hull (s \<times> t) \<subseteq> (convex hull s) \<times> (convex hull t)"
immler@69619
  2106
    by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull)
immler@69619
  2107
  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
  2108
  proof (rule hull_induct [OF x], rule hull_induct [OF y])
immler@69619
  2109
    fix x y assume "x \<in> s" and "y \<in> t"
immler@69619
  2110
    then show "(x, y) \<in> convex hull (s \<times> t)"
immler@69619
  2111
      by (simp add: hull_inc)
immler@69619
  2112
  next
immler@69619
  2113
    fix x let ?S = "((\<lambda>y. (0, y)) -` (\<lambda>p. (- x, 0) + p) ` (convex hull s \<times> t))"
immler@69619
  2114
    have "convex ?S"
immler@69619
  2115
      by (intro convex_linear_vimage convex_translation convex_convex_hull,
immler@69619
  2116
        simp add: linear_iff)
immler@69619
  2117
    also have "?S = {y. (x, y) \<in> convex hull (s \<times> t)}"
immler@69619
  2118
      by (auto simp: image_def Bex_def)
immler@69619
  2119
    finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
immler@69619
  2120
  next
immler@69619
  2121
    show "convex {x. (x, y) \<in> convex hull s \<times> t}"
immler@69619
  2122
    proof -
immler@69619
  2123
      fix y let ?S = "((\<lambda>x. (x, 0)) -` (\<lambda>p. (0, - y) + p) ` (convex hull s \<times> t))"
immler@69619
  2124
      have "convex ?S"
immler@69619
  2125
      by (intro convex_linear_vimage convex_translation convex_convex_hull,
immler@69619
  2126
        simp add: linear_iff)
immler@69619
  2127
      also have "?S = {x. (x, y) \<in> convex hull (s \<times> t)}"
immler@69619
  2128
        by (auto simp: image_def Bex_def)
immler@69619
  2129
      finally show "convex {x. (x, y) \<in> convex hull (s \<times> t)}" .
immler@69619
  2130
    qed
immler@69619
  2131
  qed
immler@69619
  2132
  then show "(convex hull s) \<times> (convex hull t) \<subseteq> convex hull (s \<times> t)"
immler@69619
  2133
    unfolding subset_eq split_paired_Ball_Sigma by blast
immler@69619
  2134
qed
immler@69619
  2135
immler@69619
  2136
immler@69619
  2137
subsubsection%unimportant \<open>Stepping theorems for convex hulls of finite sets\<close>
immler@69619
  2138
immler@69619
  2139
lemma convex_hull_empty[simp]: "convex hull {} = {}"
immler@69619
  2140
  by (rule hull_unique) auto
immler@69619
  2141
immler@69619
  2142
lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
immler@69619
  2143
  by (rule hull_unique) auto
immler@69619
  2144
immler@69619
  2145
lemma convex_hull_insert:
immler@69619
  2146
  fixes S :: "'a::real_vector set"
immler@69619
  2147
  assumes "S \<noteq> {}"
immler@69619
  2148
  shows "convex hull (insert a S) =
immler@69619
  2149
         {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
  2150
  (is "_ = ?hull")
immler@69619
  2151
proof (intro equalityI hull_minimal subsetI)
immler@69619
  2152
  fix x
immler@69619
  2153
  assume "x \<in> insert a S"
immler@69619
  2154
  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
  2155
  unfolding insert_iff
immler@69619
  2156
  proof
immler@69619
  2157
    assume "x = a"
immler@69619
  2158
    then show ?thesis
immler@69619
  2159
      by (rule_tac x=1 in exI) (use assms hull_subset in fastforce)
immler@69619
  2160
  next
immler@69619
  2161
    assume "x \<in> S"
immler@69619
  2162
    with hull_subset[of S convex] show ?thesis
immler@69619
  2163
      by force
immler@69619
  2164
  qed
immler@69619
  2165
  then show "x \<in> ?hull"
immler@69619
  2166
    by simp
immler@69619
  2167
next
immler@69619
  2168
  fix x
immler@69619
  2169
  assume "x \<in> ?hull"
immler@69619
  2170
  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
  2171
    by auto
immler@69619
  2172
  have "a \<in> convex hull insert a S" "b \<in> convex hull insert a S"
immler@69619
  2173
    using hull_mono[of S "insert a S" convex] hull_mono[of "{a}" "insert a S" convex] and obt(4)
immler@69619
  2174
    by auto
immler@69619
  2175
  then show "x \<in> convex hull insert a S"
immler@69619
  2176
    unfolding obt(5) using obt(1-3)
immler@69619
  2177
    by (rule convexD [OF convex_convex_hull])
immler@69619
  2178
next
immler@69619
  2179
  show "convex ?hull"
immler@69619
  2180
  proof (rule convexI)
immler@69619
  2181
    fix x y u v
immler@69619
  2182
    assume as: "(0::real) \<le> u" "0 \<le> v" "u + v = 1" and x: "x \<in> ?hull" and y: "y \<in> ?hull"
immler@69619
  2183
    from x obtain u1 v1 b1 where
immler@69619
  2184
      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
  2185
      by auto
immler@69619
  2186
    from y obtain u2 v2 b2 where
immler@69619
  2187
      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
  2188
      by auto
immler@69619
  2189
    have *: "\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
immler@69619
  2190
      by (auto simp: algebra_simps)
immler@69619
  2191
    have "\<exists>b \<in> convex hull S. u *\<^sub>R x + v *\<^sub>R y =
immler@69619
  2192
      (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"
immler@69619
  2193
    proof (cases "u * v1 + v * v2 = 0")
immler@69619
  2194
      case True
immler@69619
  2195
      have *: "\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x"
immler@69619
  2196
        by (auto simp: algebra_simps)
immler@69619
  2197
      have eq0: "u * v1 = 0" "v * v2 = 0"
immler@69619
  2198
        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
  2199
        by arith+
immler@69619
  2200
      then have "u * u1 + v * u2 = 1"
immler@69619
  2201
        using as(3) obt1(3) obt2(3) by auto
immler@69619
  2202
      then show ?thesis
immler@69619
  2203
        using "*" eq0 as obt1(4) xeq yeq by auto
immler@69619
  2204
    next
immler@69619
  2205
      case False
immler@69619
  2206
      have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)"
immler@69619
  2207
        using as(3) obt1(3) obt2(3) by (auto simp: field_simps)
immler@69619
  2208
      also have "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)"
immler@69619
  2209
        using as(3) obt1(3) obt2(3) by (auto simp: field_simps)
immler@69619
  2210
      also have "\<dots> = u * v1 + v * v2"
immler@69619
  2211
        by simp
immler@69619
  2212
      finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
immler@69619
  2213
      let ?b = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2"
immler@69619
  2214
      have zeroes: "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2"
immler@69619
  2215
        using as(1,2) obt1(1,2) obt2(1,2) by auto
immler@69619
  2216
      show ?thesis
immler@69619
  2217
      proof
immler@69619
  2218
        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
  2219
          unfolding xeq yeq * **
immler@69619
  2220
          using False by (auto simp: scaleR_left_distrib scaleR_right_distrib)
immler@69619
  2221
        show "?b \<in> convex hull S"
immler@69619
  2222
          using False zeroes obt1(4) obt2(4)
immler@69619
  2223
          by (auto simp: convexD [OF convex_convex_hull] scaleR_left_distrib scaleR_right_distrib  add_divide_distrib[symmetric]  zero_le_divide_iff)
immler@69619
  2224
      qed
immler@69619
  2225
    qed
immler@69619
  2226
    then obtain b where b: "b \<in> convex hull S" 
immler@69619
  2227
       "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
  2228
immler@69619
  2229
    have u1: "u1 \<le> 1"
immler@69619
  2230
      unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto
immler@69619
  2231
    have u2: "u2 \<le> 1"
immler@69619
  2232
      unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
immler@69619
  2233
    have "u1 * u + u2 * v \<le> max u1 u2 * u + max u1 u2 * v"
immler@69619
  2234
    proof (rule add_mono)
immler@69619
  2235
      show "u1 * u \<le> max u1 u2 * u" "u2 * v \<le> max u1 u2 * v"
immler@69619
  2236
        by (simp_all add: as mult_right_mono)
immler@69619
  2237
    qed
immler@69619
  2238
    also have "\<dots> \<le> 1"
immler@69619
  2239
      unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
immler@69619
  2240
    finally have le1: "u1 * u + u2 * v \<le> 1" .    
immler@69619
  2241
    show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull"
immler@69619
  2242
    proof (intro CollectI exI conjI)
immler@69619
  2243
      show "0 \<le> u * u1 + v * u2"
immler@69619
  2244
        by (simp add: as(1) as(2) obt1(1) obt2(1))
immler@69619
  2245
      show "0 \<le> 1 - u * u1 - v * u2"
immler@69619
  2246
        by (simp add: le1 diff_diff_add mult.commute)
immler@69619
  2247
    qed (use b in \<open>auto simp: algebra_simps\<close>)
immler@69619
  2248
  qed
immler@69619
  2249
qed
immler@69619
  2250
immler@69619
  2251
lemma convex_hull_insert_alt:
immler@69619
  2252
   "convex hull (insert a S) =
immler@69619
  2253
     (if S = {} then {a}
immler@69619
  2254
      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
  2255
  apply (auto simp: convex_hull_insert)
immler@69619
  2256
  using diff_eq_eq apply fastforce
immler@69619
  2257
  by (metis add.group_left_neutral add_le_imp_le_diff diff_add_cancel)
immler@69619
  2258
immler@69619
  2259
subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
immler@69619
  2260
immler@69619
  2261
proposition convex_hull_indexed:
immler@69619
  2262
  fixes S :: "'a::real_vector set"
immler@69619
  2263
  shows "convex hull S =
immler@69619
  2264
    {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> S) \<and>
immler@69619
  2265
                (sum u {1..k} = 1) \<and> (\<Sum>i = 1..k. u i *\<^sub>R x i) = y}"
immler@69619
  2266
    (is "?xyz = ?hull")
immler@69619
  2267
proof (rule hull_unique [OF _ convexI])
immler@69619
  2268
  show "S \<subseteq> ?hull" 
immler@69619
  2269
    by (clarsimp, rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI, auto)
immler@69619
  2270
next
immler@69619
  2271
  fix T
immler@69619
  2272
  assume "S \<subseteq> T" "convex T"
immler@69619
  2273
  then show "?hull \<subseteq> T"
immler@69619
  2274
    by (blast intro: convex_sum)
immler@69619
  2275
next
immler@69619
  2276
  fix x y u v
immler@69619
  2277
  assume uv: "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
immler@69619
  2278
  assume xy: "x \<in> ?hull" "y \<in> ?hull"
immler@69619
  2279
  from xy obtain k1 u1 x1 where
immler@69619
  2280
    x [rule_format]: "\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> S" 
immler@69619
  2281
                      "sum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x"
immler@69619
  2282
    by auto
immler@69619
  2283
  from xy obtain k2 u2 x2 where
immler@69619
  2284
    y [rule_format]: "\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> S" 
immler@69619
  2285
                     "sum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y"
immler@69619
  2286
    by auto
immler@69619
  2287
  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
  2288
          "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
immler@69619
  2289
    by auto
immler@69619
  2290
  have inj: "inj_on (\<lambda>i. i + k1) {1..k2}"
immler@69619
  2291
    unfolding inj_on_def by auto
immler@69619
  2292
  let ?uu = "\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)"
immler@69619
  2293
  let ?xx = "\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)"
immler@69619
  2294
  show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull"
immler@69619
  2295
  proof (intro CollectI exI conjI ballI)
immler@69619
  2296
    show "0 \<le> ?uu i" "?xx i \<in> S" if "i \<in> {1..k1+k2}" for i
immler@69619
  2297
      using that by (auto simp add: le_diff_conv uv(1) x(1) uv(2) y(1))
immler@69619
  2298
    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
  2299
      unfolding * sum.If_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]]
immler@69619
  2300
        sum.reindex[OF inj] Collect_mem_eq o_def
immler@69619
  2301
      unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] sum_distrib_left[symmetric]
immler@69619
  2302
      by (simp_all add: sum_distrib_left[symmetric]  x(2,3) y(2,3) uv(3))
immler@69619
  2303
  qed 
immler@69619
  2304
qed
immler@69619
  2305
immler@69619
  2306
lemma convex_hull_finite:
immler@69619
  2307
  fixes S :: "'a::real_vector set"
immler@69619
  2308
  assumes "finite S"
immler@69619
  2309
  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}"
imm