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