author | huffman |
Fri, 13 Sep 2013 11:16:13 -0700 | |
changeset 53620 | 3c7f5e7926dc |
parent 53596 | d29d63460d84 |
child 53676 | 476ef9b468d2 |
permissions | -rw-r--r-- |
36648 | 1 |
(* Title: HOL/Library/Convex.thy |
2 |
Author: Armin Heller, TU Muenchen |
|
3 |
Author: Johannes Hoelzl, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* Convexity in real vector spaces *} |
|
7 |
||
36623 | 8 |
theory Convex |
9 |
imports Product_Vector |
|
10 |
begin |
|
11 |
||
12 |
subsection {* Convexity. *} |
|
13 |
||
49609 | 14 |
definition convex :: "'a::real_vector set \<Rightarrow> bool" |
15 |
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)" |
|
36623 | 16 |
|
17 |
lemma convex_alt: |
|
18 |
"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)" |
|
19 |
(is "_ \<longleftrightarrow> ?alt") |
|
20 |
proof |
|
21 |
assume alt[rule_format]: ?alt |
|
22 |
{ fix x y and u v :: real assume mem: "x \<in> s" "y \<in> s" |
|
49609 | 23 |
assume "0 \<le> u" "0 \<le> v" |
24 |
moreover assume "u + v = 1" then have "u = 1 - v" by auto |
|
36623 | 25 |
ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> s" using alt[OF mem] by auto } |
49609 | 26 |
then show "convex s" unfolding convex_def by auto |
36623 | 27 |
qed (auto simp: convex_def) |
28 |
||
29 |
lemma mem_convex: |
|
30 |
assumes "convex s" "a \<in> s" "b \<in> s" "0 \<le> u" "u \<le> 1" |
|
31 |
shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s" |
|
32 |
using assms unfolding convex_alt by auto |
|
33 |
||
34 |
lemma convex_empty[intro]: "convex {}" |
|
35 |
unfolding convex_def by simp |
|
36 |
||
37 |
lemma convex_singleton[intro]: "convex {a}" |
|
38 |
unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric]) |
|
39 |
||
40 |
lemma convex_UNIV[intro]: "convex UNIV" |
|
41 |
unfolding convex_def by auto |
|
42 |
||
43 |
lemma convex_Inter: "(\<forall>s\<in>f. convex s) ==> convex(\<Inter> f)" |
|
44 |
unfolding convex_def by auto |
|
45 |
||
46 |
lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)" |
|
47 |
unfolding convex_def by auto |
|
48 |
||
53596 | 49 |
lemma convex_INT: "\<forall>i\<in>A. convex (B i) \<Longrightarrow> convex (\<Inter>i\<in>A. B i)" |
50 |
unfolding convex_def by auto |
|
51 |
||
52 |
lemma convex_Times: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<times> t)" |
|
53 |
unfolding convex_def by auto |
|
54 |
||
36623 | 55 |
lemma convex_halfspace_le: "convex {x. inner a x \<le> b}" |
56 |
unfolding convex_def |
|
44142 | 57 |
by (auto simp: inner_add intro!: convex_bound_le) |
36623 | 58 |
|
59 |
lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}" |
|
60 |
proof - |
|
49609 | 61 |
have *: "{x. inner a x \<ge> b} = {x. inner (-a) x \<le> -b}" by auto |
36623 | 62 |
show ?thesis unfolding * using convex_halfspace_le[of "-a" "-b"] by auto |
63 |
qed |
|
64 |
||
65 |
lemma convex_hyperplane: "convex {x. inner a x = b}" |
|
49609 | 66 |
proof - |
67 |
have *: "{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}" by auto |
|
36623 | 68 |
show ?thesis using convex_halfspace_le convex_halfspace_ge |
69 |
by (auto intro!: convex_Int simp: *) |
|
70 |
qed |
|
71 |
||
72 |
lemma convex_halfspace_lt: "convex {x. inner a x < b}" |
|
73 |
unfolding convex_def |
|
74 |
by (auto simp: convex_bound_lt inner_add) |
|
75 |
||
76 |
lemma convex_halfspace_gt: "convex {x. inner a x > b}" |
|
77 |
using convex_halfspace_lt[of "-a" "-b"] by auto |
|
78 |
||
79 |
lemma convex_real_interval: |
|
80 |
fixes a b :: "real" |
|
81 |
shows "convex {a..}" and "convex {..b}" |
|
49609 | 82 |
and "convex {a<..}" and "convex {..<b}" |
83 |
and "convex {a..b}" and "convex {a<..b}" |
|
84 |
and "convex {a..<b}" and "convex {a<..<b}" |
|
36623 | 85 |
proof - |
86 |
have "{a..} = {x. a \<le> inner 1 x}" by auto |
|
49609 | 87 |
then show 1: "convex {a..}" by (simp only: convex_halfspace_ge) |
36623 | 88 |
have "{..b} = {x. inner 1 x \<le> b}" by auto |
49609 | 89 |
then show 2: "convex {..b}" by (simp only: convex_halfspace_le) |
36623 | 90 |
have "{a<..} = {x. a < inner 1 x}" by auto |
49609 | 91 |
then show 3: "convex {a<..}" by (simp only: convex_halfspace_gt) |
36623 | 92 |
have "{..<b} = {x. inner 1 x < b}" by auto |
49609 | 93 |
then show 4: "convex {..<b}" by (simp only: convex_halfspace_lt) |
36623 | 94 |
have "{a..b} = {a..} \<inter> {..b}" by auto |
49609 | 95 |
then show "convex {a..b}" by (simp only: convex_Int 1 2) |
36623 | 96 |
have "{a<..b} = {a<..} \<inter> {..b}" by auto |
49609 | 97 |
then show "convex {a<..b}" by (simp only: convex_Int 3 2) |
36623 | 98 |
have "{a..<b} = {a..} \<inter> {..<b}" by auto |
49609 | 99 |
then show "convex {a..<b}" by (simp only: convex_Int 1 4) |
36623 | 100 |
have "{a<..<b} = {a<..} \<inter> {..<b}" by auto |
49609 | 101 |
then show "convex {a<..<b}" by (simp only: convex_Int 3 4) |
36623 | 102 |
qed |
103 |
||
49609 | 104 |
|
36623 | 105 |
subsection {* Explicit expressions for convexity in terms of arbitrary sums. *} |
106 |
||
107 |
lemma convex_setsum: |
|
108 |
fixes C :: "'a::real_vector set" |
|
109 |
assumes "finite s" and "convex C" and "(\<Sum> i \<in> s. a i) = 1" |
|
49609 | 110 |
assumes "\<And>i. i \<in> s \<Longrightarrow> a i \<ge> 0" and "\<And>i. i \<in> s \<Longrightarrow> y i \<in> C" |
36623 | 111 |
shows "(\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C" |
49609 | 112 |
using assms |
113 |
proof (induct s arbitrary:a rule: finite_induct) |
|
114 |
case empty |
|
115 |
then show ?case by auto |
|
36623 | 116 |
next |
117 |
case (insert i s) note asms = this |
|
118 |
{ assume "a i = 1" |
|
49609 | 119 |
then have "(\<Sum> j \<in> s. a j) = 0" |
36623 | 120 |
using asms by auto |
49609 | 121 |
then have "\<And>j. j \<in> s \<Longrightarrow> a j = 0" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44282
diff
changeset
|
122 |
using setsum_nonneg_0[where 'b=real] asms by fastforce |
49609 | 123 |
then have ?case using asms by auto } |
36623 | 124 |
moreover |
125 |
{ assume asm: "a i \<noteq> 1" |
|
126 |
from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto |
|
127 |
have fis: "finite (insert i s)" using asms by auto |
|
49609 | 128 |
then have ai1: "a i \<le> 1" using setsum_nonneg_leq_bound[of "insert i s" a 1] asms by simp |
129 |
then have "a i < 1" using asm by auto |
|
130 |
then have i0: "1 - a i > 0" by auto |
|
131 |
let ?a = "\<lambda>j. a j / (1 - a i)" |
|
36623 | 132 |
{ fix j assume "j \<in> s" |
49609 | 133 |
then have "?a j \<ge> 0" |
36623 | 134 |
using i0 asms divide_nonneg_pos |
49609 | 135 |
by fastforce |
136 |
} note a_nonneg = this |
|
36623 | 137 |
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto |
49609 | 138 |
then have "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastforce |
139 |
then have "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto |
|
140 |
then have a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp |
|
141 |
with asms have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastforce |
|
142 |
then have "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C" |
|
36623 | 143 |
using asms[unfolded convex_def, rule_format] yai ai1 by auto |
49609 | 144 |
then have "a i *\<^sub>R y i + (\<Sum> j \<in> s. (1 - a i) *\<^sub>R (?a j *\<^sub>R y j)) \<in> C" |
36623 | 145 |
using scaleR_right.setsum[of "(1 - a i)" "\<lambda> j. ?a j *\<^sub>R y j" s] by auto |
49609 | 146 |
then have "a i *\<^sub>R y i + (\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C" using i0 by auto |
147 |
then have ?case using setsum.insert asms by auto |
|
148 |
} |
|
36623 | 149 |
ultimately show ?case by auto |
150 |
qed |
|
151 |
||
152 |
lemma convex: |
|
49609 | 153 |
"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> (setsum u {1..k} = 1) |
154 |
\<longrightarrow> setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} \<in> s)" |
|
36623 | 155 |
proof safe |
49609 | 156 |
fix k :: nat |
157 |
fix u :: "nat \<Rightarrow> real" |
|
158 |
fix x |
|
36623 | 159 |
assume "convex s" |
160 |
"\<forall>i. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s" |
|
161 |
"setsum u {1..k} = 1" |
|
162 |
from this convex_setsum[of "{1 .. k}" s] |
|
163 |
show "(\<Sum>j\<in>{1 .. k}. u j *\<^sub>R x j) \<in> s" by auto |
|
164 |
next |
|
165 |
assume asm: "\<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> setsum u {1..k} = 1 |
|
166 |
\<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R (x i :: 'a)) \<in> s" |
|
49609 | 167 |
{ fix \<mu> :: real |
168 |
fix x y :: 'a |
|
169 |
assume xy: "x \<in> s" "y \<in> s" |
|
170 |
assume mu: "\<mu> \<ge> 0" "\<mu> \<le> 1" |
|
171 |
let ?u = "\<lambda>i. if (i :: nat) = 1 then \<mu> else 1 - \<mu>" |
|
172 |
let ?x = "\<lambda>i. if (i :: nat) = 1 then x else y" |
|
36623 | 173 |
have "{1 :: nat .. 2} \<inter> - {x. x = 1} = {2}" by auto |
49609 | 174 |
then have card: "card ({1 :: nat .. 2} \<inter> - {x. x = 1}) = 1" by simp |
175 |
then have "setsum ?u {1 .. 2} = 1" |
|
36623 | 176 |
using setsum_cases[of "{(1 :: nat) .. 2}" "\<lambda> x. x = 1" "\<lambda> x. \<mu>" "\<lambda> x. 1 - \<mu>"] |
177 |
by auto |
|
49609 | 178 |
with asm[rule_format, of "2" ?u ?x] have s: "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) \<in> s" |
36623 | 179 |
using mu xy by auto |
180 |
have grarr: "(\<Sum>j \<in> {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \<mu>) *\<^sub>R y" |
|
181 |
using setsum_head_Suc[of "Suc (Suc 0)" 2 "\<lambda> j. (1 - \<mu>) *\<^sub>R y"] by auto |
|
182 |
from setsum_head_Suc[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this] |
|
183 |
have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y" by auto |
|
49609 | 184 |
then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s" using s by (auto simp:add_commute) |
185 |
} |
|
186 |
then show "convex s" unfolding convex_alt by auto |
|
36623 | 187 |
qed |
188 |
||
189 |
||
190 |
lemma convex_explicit: |
|
191 |
fixes s :: "'a::real_vector set" |
|
192 |
shows "convex s \<longleftrightarrow> |
|
49609 | 193 |
(\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) t \<in> s)" |
36623 | 194 |
proof safe |
49609 | 195 |
fix t |
196 |
fix u :: "'a \<Rightarrow> real" |
|
36623 | 197 |
assume "convex s" "finite t" |
198 |
"t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" |
|
49609 | 199 |
then show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" |
36623 | 200 |
using convex_setsum[of t s u "\<lambda> x. x"] by auto |
201 |
next |
|
202 |
assume asm0: "\<forall>t. \<forall> u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) |
|
203 |
\<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" |
|
204 |
show "convex s" |
|
205 |
unfolding convex_alt |
|
206 |
proof safe |
|
49609 | 207 |
fix x y |
208 |
fix \<mu> :: real |
|
36623 | 209 |
assume asm: "x \<in> s" "y \<in> s" "0 \<le> \<mu>" "\<mu> \<le> 1" |
210 |
{ assume "x \<noteq> y" |
|
49609 | 211 |
then have "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s" |
36623 | 212 |
using asm0[rule_format, of "{x, y}" "\<lambda> z. if z = x then 1 - \<mu> else \<mu>"] |
213 |
asm by auto } |
|
214 |
moreover |
|
215 |
{ assume "x = y" |
|
49609 | 216 |
then have "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s" |
36623 | 217 |
using asm0[rule_format, of "{x, y}" "\<lambda> z. 1"] |
218 |
asm by (auto simp:field_simps real_vector.scale_left_diff_distrib) } |
|
219 |
ultimately show "(1 - \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s" by blast |
|
220 |
qed |
|
221 |
qed |
|
222 |
||
49609 | 223 |
lemma convex_finite: |
224 |
assumes "finite s" |
|
36623 | 225 |
shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 |
226 |
\<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)" |
|
227 |
unfolding convex_explicit |
|
49609 | 228 |
proof safe |
229 |
fix t u |
|
230 |
assume sum: "\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> s" |
|
36623 | 231 |
and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)" |
49609 | 232 |
have *: "s \<inter> t = t" using as(2) by auto |
233 |
have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)" |
|
234 |
by simp |
|
36623 | 235 |
show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" |
236 |
using sum[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]] as * |
|
237 |
by (auto simp: assms setsum_cases if_distrib if_distrib_arg) |
|
238 |
qed (erule_tac x=s in allE, erule_tac x=u in allE, auto) |
|
239 |
||
49609 | 240 |
definition convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" |
241 |
where "convex_on s f \<longleftrightarrow> |
|
242 |
(\<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)" |
|
36623 | 243 |
|
244 |
lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f" |
|
245 |
unfolding convex_on_def by auto |
|
246 |
||
53620
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
247 |
lemma convex_on_add [intro]: |
36623 | 248 |
assumes "convex_on s f" "convex_on s g" |
249 |
shows "convex_on s (\<lambda>x. f x + g x)" |
|
49609 | 250 |
proof - |
251 |
{ fix x y |
|
252 |
assume "x\<in>s" "y\<in>s" |
|
253 |
moreover |
|
254 |
fix u v :: real |
|
255 |
assume "0 \<le> u" "0 \<le> v" "u + v = 1" |
|
256 |
ultimately |
|
257 |
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)" |
|
258 |
using assms unfolding convex_on_def by (auto simp add: add_mono) |
|
259 |
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)" |
|
260 |
by (simp add: field_simps) |
|
261 |
} |
|
262 |
then show ?thesis unfolding convex_on_def by auto |
|
36623 | 263 |
qed |
264 |
||
53620
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
265 |
lemma convex_on_cmul [intro]: |
36623 | 266 |
assumes "0 \<le> (c::real)" "convex_on s f" |
267 |
shows "convex_on s (\<lambda>x. c * f x)" |
|
268 |
proof- |
|
49609 | 269 |
have *: "\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" |
270 |
by (simp add: field_simps) |
|
271 |
show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)] |
|
272 |
unfolding convex_on_def and * by auto |
|
36623 | 273 |
qed |
274 |
||
275 |
lemma convex_lower: |
|
276 |
assumes "convex_on s f" "x\<in>s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1" |
|
277 |
shows "f (u *\<^sub>R x + v *\<^sub>R y) \<le> max (f x) (f y)" |
|
278 |
proof- |
|
279 |
let ?m = "max (f x) (f y)" |
|
280 |
have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)" |
|
38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
36778
diff
changeset
|
281 |
using assms(4,5) by (auto simp add: mult_left_mono add_mono) |
49609 | 282 |
also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[symmetric] by auto |
36623 | 283 |
finally show ?thesis |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44282
diff
changeset
|
284 |
using assms unfolding convex_on_def by fastforce |
36623 | 285 |
qed |
286 |
||
53620
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
287 |
lemma convex_on_dist [intro]: |
36623 | 288 |
fixes s :: "'a::real_normed_vector set" |
289 |
shows "convex_on s (\<lambda>x. dist a x)" |
|
49609 | 290 |
proof (auto simp add: convex_on_def dist_norm) |
291 |
fix x y |
|
292 |
assume "x\<in>s" "y\<in>s" |
|
293 |
fix u v :: real |
|
294 |
assume "0 \<le> u" "0 \<le> v" "u + v = 1" |
|
295 |
have "a = u *\<^sub>R a + v *\<^sub>R a" |
|
296 |
unfolding scaleR_left_distrib[symmetric] and `u+v=1` by simp |
|
297 |
then have *: "a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))" |
|
36623 | 298 |
by (auto simp add: algebra_simps) |
299 |
show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a - x) + v * norm (a - y)" |
|
300 |
unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"] |
|
301 |
using `0 \<le> u` `0 \<le> v` by auto |
|
302 |
qed |
|
303 |
||
49609 | 304 |
|
36623 | 305 |
subsection {* Arithmetic operations on sets preserve convexity. *} |
49609 | 306 |
|
53620
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
307 |
lemma convex_linear_image: |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
308 |
assumes "linear f" and "convex s" shows "convex (f ` s)" |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
309 |
proof - |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
310 |
interpret f: linear f by fact |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
311 |
from `convex s` show "convex (f ` s)" |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
312 |
by (simp add: convex_def f.scaleR [symmetric] f.add [symmetric]) |
36623 | 313 |
qed |
314 |
||
53620
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
315 |
lemma convex_linear_vimage: |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
316 |
assumes "linear f" and "convex s" shows "convex (f -` s)" |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
317 |
proof - |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
318 |
interpret f: linear f by fact |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
319 |
from `convex s` show "convex (f -` s)" |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
320 |
by (simp add: convex_def f.add f.scaleR) |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
321 |
qed |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
322 |
|
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
323 |
lemma convex_scaling: |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
324 |
assumes "convex s" shows "convex ((\<lambda>x. c *\<^sub>R x) ` s)" |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
325 |
proof - |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
326 |
have "linear (\<lambda>x. c *\<^sub>R x)" by (simp add: linearI scaleR_add_right) |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
327 |
then show ?thesis using `convex s` by (rule convex_linear_image) |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
328 |
qed |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
329 |
|
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
330 |
lemma convex_negations: |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
331 |
assumes "convex s" shows "convex ((\<lambda>x. - x) ` s)" |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
332 |
proof - |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets
huffman
parents:
53596
diff
changeset
|
333 |
have "linear (\<lambda>x. - x)" by (simp add: linearI) |
3c7f5e7926dc
generalized and simplified proofs of several theorems about convex sets |