author  huffman 
Wed, 10 Aug 2011 18:02:16 0700  
changeset 44142  8e27e0177518 
parent 43337  57a1c19f8e3b 
child 44282  f0de18b62d63 
permissions  rwrr 
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 

14 
definition 

15 
convex :: "'a::real_vector set \<Rightarrow> bool" where 

16 
"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)" 

17 

18 
lemma convex_alt: 

19 
"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)" 

20 
(is "_ \<longleftrightarrow> ?alt") 

21 
proof 

22 
assume alt[rule_format]: ?alt 

23 
{ fix x y and u v :: real assume mem: "x \<in> s" "y \<in> s" 

24 
assume "0 \<le> u" "0 \<le> v" "u + v = 1" 

25 
moreover hence "u = 1  v" by auto 

26 
ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> s" using alt[OF mem] by auto } 

27 
thus "convex s" unfolding convex_def by auto 

28 
qed (auto simp: convex_def) 

29 

30 
lemma mem_convex: 

31 
assumes "convex s" "a \<in> s" "b \<in> s" "0 \<le> u" "u \<le> 1" 

32 
shows "((1  u) *\<^sub>R a + u *\<^sub>R b) \<in> s" 

33 
using assms unfolding convex_alt by auto 

34 

35 
lemma convex_empty[intro]: "convex {}" 

36 
unfolding convex_def by simp 

37 

38 
lemma convex_singleton[intro]: "convex {a}" 

39 
unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric]) 

40 

41 
lemma convex_UNIV[intro]: "convex UNIV" 

42 
unfolding convex_def by auto 

43 

44 
lemma convex_Inter: "(\<forall>s\<in>f. convex s) ==> convex(\<Inter> f)" 

45 
unfolding convex_def by auto 

46 

47 
lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)" 

48 
unfolding convex_def by auto 

49 

50 
lemma convex_halfspace_le: "convex {x. inner a x \<le> b}" 

51 
unfolding convex_def 

44142  52 
by (auto simp: inner_add intro!: convex_bound_le) 
36623  53 

54 
lemma convex_halfspace_ge: "convex {x. inner a x \<ge> b}" 

55 
proof  

56 
have *:"{x. inner a x \<ge> b} = {x. inner (a) x \<le> b}" by auto 

57 
show ?thesis unfolding * using convex_halfspace_le[of "a" "b"] by auto 

58 
qed 

59 

60 
lemma convex_hyperplane: "convex {x. inner a x = b}" 

61 
proof 

62 
have *:"{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}" by auto 

63 
show ?thesis using convex_halfspace_le convex_halfspace_ge 

64 
by (auto intro!: convex_Int simp: *) 

65 
qed 

66 

67 
lemma convex_halfspace_lt: "convex {x. inner a x < b}" 

68 
unfolding convex_def 

69 
by (auto simp: convex_bound_lt inner_add) 

70 

71 
lemma convex_halfspace_gt: "convex {x. inner a x > b}" 

72 
using convex_halfspace_lt[of "a" "b"] by auto 

73 

74 
lemma convex_real_interval: 

75 
fixes a b :: "real" 

76 
shows "convex {a..}" and "convex {..b}" 

77 
and "convex {a<..}" and "convex {..<b}" 

78 
and "convex {a..b}" and "convex {a<..b}" 

79 
and "convex {a..<b}" and "convex {a<..<b}" 

80 
proof  

81 
have "{a..} = {x. a \<le> inner 1 x}" by auto 

82 
thus 1: "convex {a..}" by (simp only: convex_halfspace_ge) 

83 
have "{..b} = {x. inner 1 x \<le> b}" by auto 

84 
thus 2: "convex {..b}" by (simp only: convex_halfspace_le) 

85 
have "{a<..} = {x. a < inner 1 x}" by auto 

86 
thus 3: "convex {a<..}" by (simp only: convex_halfspace_gt) 

87 
have "{..<b} = {x. inner 1 x < b}" by auto 

88 
thus 4: "convex {..<b}" by (simp only: convex_halfspace_lt) 

89 
have "{a..b} = {a..} \<inter> {..b}" by auto 

90 
thus "convex {a..b}" by (simp only: convex_Int 1 2) 

91 
have "{a<..b} = {a<..} \<inter> {..b}" by auto 

92 
thus "convex {a<..b}" by (simp only: convex_Int 3 2) 

93 
have "{a..<b} = {a..} \<inter> {..<b}" by auto 

94 
thus "convex {a..<b}" by (simp only: convex_Int 1 4) 

95 
have "{a<..<b} = {a<..} \<inter> {..<b}" by auto 

96 
thus "convex {a<..<b}" by (simp only: convex_Int 3 4) 

97 
qed 

98 

99 
subsection {* Explicit expressions for convexity in terms of arbitrary sums. *} 

100 

101 
lemma convex_setsum: 

102 
fixes C :: "'a::real_vector set" 

103 
assumes "finite s" and "convex C" and "(\<Sum> i \<in> s. a i) = 1" 

104 
assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0" and "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C" 

105 
shows "(\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C" 

106 
using assms 

107 
proof (induct s arbitrary:a rule:finite_induct) 

108 
case empty thus ?case by auto 

109 
next 

110 
case (insert i s) note asms = this 

111 
{ assume "a i = 1" 

112 
hence "(\<Sum> j \<in> s. a j) = 0" 

113 
using asms by auto 

114 
hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0" 

115 
using setsum_nonneg_0[where 'b=real] asms by fastsimp 

116 
hence ?case using asms by auto } 

117 
moreover 

118 
{ assume asm: "a i \<noteq> 1" 

119 
from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto 

120 
have fis: "finite (insert i s)" using asms by auto 

121 
hence ai1: "a i \<le> 1" using setsum_nonneg_leq_bound[of "insert i s" a 1] asms by simp 

122 
hence "a i < 1" using asm by auto 

123 
hence i0: "1  a i > 0" by auto 

124 
let "?a j" = "a j / (1  a i)" 

125 
{ fix j assume "j \<in> s" 

126 
hence "?a j \<ge> 0" 

127 
using i0 asms divide_nonneg_pos 

128 
by fastsimp } note a_nonneg = this 

129 
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto 

130 
hence "(\<Sum> j \<in> s. a j) = 1  a i" using setsum.insert asms by fastsimp 

131 
hence "(\<Sum> j \<in> s. a j) / (1  a i) = 1" using i0 by auto 

132 
hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp 

133 
from this asms 

134 
have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp 

135 
hence "a i *\<^sub>R y i + (1  a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C" 

136 
using asms[unfolded convex_def, rule_format] yai ai1 by auto 

137 
hence "a i *\<^sub>R y i + (\<Sum> j \<in> s. (1  a i) *\<^sub>R (?a j *\<^sub>R y j)) \<in> C" 

138 
using scaleR_right.setsum[of "(1  a i)" "\<lambda> j. ?a j *\<^sub>R y j" s] by auto 

139 
hence "a i *\<^sub>R y i + (\<Sum> j \<in> s. a j *\<^sub>R y j) \<in> C" using i0 by auto 

140 
hence ?case using setsum.insert asms by auto } 

141 
ultimately show ?case by auto 

142 
qed 

143 

144 
lemma convex: 

145 
shows "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) 

146 
\<longrightarrow> setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} \<in> s)" 

147 
proof safe 

148 
fix k :: nat fix u :: "nat \<Rightarrow> real" fix x 

149 
assume "convex s" 

150 
"\<forall>i. 1 \<le> i \<and> i \<le> k \<longrightarrow> 0 \<le> u i \<and> x i \<in> s" 

151 
"setsum u {1..k} = 1" 

152 
from this convex_setsum[of "{1 .. k}" s] 

153 
show "(\<Sum>j\<in>{1 .. k}. u j *\<^sub>R x j) \<in> s" by auto 

154 
next 

155 
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 

156 
\<longrightarrow> (\<Sum>i = 1..k. u i *\<^sub>R (x i :: 'a)) \<in> s" 

157 
{ fix \<mu> :: real fix x y :: 'a assume xy: "x \<in> s" "y \<in> s" assume mu: "\<mu> \<ge> 0" "\<mu> \<le> 1" 

158 
let "?u i" = "if (i :: nat) = 1 then \<mu> else 1  \<mu>" 

159 
let "?x i" = "if (i :: nat) = 1 then x else y" 

160 
have "{1 :: nat .. 2} \<inter>  {x. x = 1} = {2}" by auto 

161 
hence card: "card ({1 :: nat .. 2} \<inter>  {x. x = 1}) = 1" by simp 

162 
hence "setsum ?u {1 .. 2} = 1" 

163 
using setsum_cases[of "{(1 :: nat) .. 2}" "\<lambda> x. x = 1" "\<lambda> x. \<mu>" "\<lambda> x. 1  \<mu>"] 

164 
by auto 

165 
from this asm[rule_format, of "2" ?u ?x] 

166 
have s: "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) \<in> s" 

167 
using mu xy by auto 

168 
have grarr: "(\<Sum>j \<in> {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1  \<mu>) *\<^sub>R y" 

169 
using setsum_head_Suc[of "Suc (Suc 0)" 2 "\<lambda> j. (1  \<mu>) *\<^sub>R y"] by auto 

170 
from setsum_head_Suc[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this] 

171 
have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y" by auto 

172 
hence "(1  \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s" using s by (auto simp:add_commute) } 

173 
thus "convex s" unfolding convex_alt by auto 

174 
qed 

175 

176 

177 
lemma convex_explicit: 

178 
fixes s :: "'a::real_vector set" 

179 
shows "convex s \<longleftrightarrow> 

180 
(\<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)" 

181 
proof safe 

182 
fix t fix u :: "'a \<Rightarrow> real" 

183 
assume "convex s" "finite t" 

184 
"t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" 

185 
thus "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" 

186 
using convex_setsum[of t s u "\<lambda> x. x"] by auto 

187 
next 

188 
assume asm0: "\<forall>t. \<forall> u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) 

189 
\<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" 

190 
show "convex s" 

191 
unfolding convex_alt 

192 
proof safe 

193 
fix x y fix \<mu> :: real 

194 
assume asm: "x \<in> s" "y \<in> s" "0 \<le> \<mu>" "\<mu> \<le> 1" 

195 
{ assume "x \<noteq> y" 

196 
hence "(1  \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s" 

197 
using asm0[rule_format, of "{x, y}" "\<lambda> z. if z = x then 1  \<mu> else \<mu>"] 

198 
asm by auto } 

199 
moreover 

200 
{ assume "x = y" 

201 
hence "(1  \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s" 

202 
using asm0[rule_format, of "{x, y}" "\<lambda> z. 1"] 

203 
asm by (auto simp:field_simps real_vector.scale_left_diff_distrib) } 

204 
ultimately show "(1  \<mu>) *\<^sub>R x + \<mu> *\<^sub>R y \<in> s" by blast 

205 
qed 

206 
qed 

207 

208 
lemma convex_finite: assumes "finite s" 

209 
shows "convex s \<longleftrightarrow> (\<forall>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 

210 
\<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) s \<in> s)" 

211 
unfolding convex_explicit 

44142  212 
proof (safe) 
36623  213 
fix t u 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" 
214 
and as: "finite t" "t \<subseteq> s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = (1::real)" 

215 
have *:"s \<inter> t = t" using as(2) by auto 

216 
have if_distrib_arg: "\<And>P f g x. (if P then f else g) x = (if P then f x else g x)" by simp 

217 
show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" 

218 
using sum[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]] as * 

219 
by (auto simp: assms setsum_cases if_distrib if_distrib_arg) 

220 
qed (erule_tac x=s in allE, erule_tac x=u in allE, auto) 

221 

222 
definition 

223 
convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" where 

224 
"convex_on s f \<longleftrightarrow> 

225 
(\<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)" 

226 

227 
lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f" 

228 
unfolding convex_on_def by auto 

229 

230 
lemma convex_add[intro]: 

231 
assumes "convex_on s f" "convex_on s g" 

232 
shows "convex_on s (\<lambda>x. f x + g x)" 

233 
proof 

234 
{ fix x y assume "x\<in>s" "y\<in>s" moreover 

235 
fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1" 

236 
ultimately 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)" 

237 
using assms unfolding convex_on_def by (auto simp add:add_mono) 

238 
hence "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)" by (simp add: field_simps) } 

239 
thus ?thesis unfolding convex_on_def by auto 

240 
qed 

241 

242 
lemma convex_cmul[intro]: 

243 
assumes "0 \<le> (c::real)" "convex_on s f" 

244 
shows "convex_on s (\<lambda>x. c * f x)" 

245 
proof 

246 
have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps) 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
36778
diff
changeset

247 
show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)] unfolding convex_on_def and * by auto 
36623  248 
qed 
249 

250 
lemma convex_lower: 

251 
assumes "convex_on s f" "x\<in>s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1" 

252 
shows "f (u *\<^sub>R x + v *\<^sub>R y) \<le> max (f x) (f y)" 

253 
proof 

254 
let ?m = "max (f x) (f y)" 

255 
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

256 
using assms(4,5) by (auto simp add: mult_left_mono add_mono) 
36623  257 
also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto 
258 
finally show ?thesis 

259 
using assms unfolding convex_on_def by fastsimp 

260 
qed 

261 

262 
lemma convex_distance[intro]: 

263 
fixes s :: "'a::real_normed_vector set" 

264 
shows "convex_on s (\<lambda>x. dist a x)" 

265 
proof(auto simp add: convex_on_def dist_norm) 

266 
fix x y assume "x\<in>s" "y\<in>s" 

267 
fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1" 

268 
have "a = u *\<^sub>R a + v *\<^sub>R a" unfolding scaleR_left_distrib[THEN sym] and `u+v=1` by simp 

269 
hence *:"a  (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a  x)) + (v *\<^sub>R (a  y))" 

270 
by (auto simp add: algebra_simps) 

271 
show "norm (a  (u *\<^sub>R x + v *\<^sub>R y)) \<le> u * norm (a  x) + v * norm (a  y)" 

272 
unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a  x)" "v *\<^sub>R (a  y)"] 

273 
using `0 \<le> u` `0 \<le> v` by auto 

274 
qed 

275 

276 
subsection {* Arithmetic operations on sets preserve convexity. *} 

277 
lemma convex_scaling: 

278 
assumes "convex s" 

279 
shows"convex ((\<lambda>x. c *\<^sub>R x) ` s)" 

280 
using assms unfolding convex_def image_iff 

281 
proof safe 

282 
fix x xa y xb :: "'a::real_vector" fix u v :: real 

283 
assume asm: "\<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" 

284 
"xa \<in> s" "xb \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1" 

285 
show "\<exists>x\<in>s. u *\<^sub>R c *\<^sub>R xa + v *\<^sub>R c *\<^sub>R xb = c *\<^sub>R x" 

286 
using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by (auto simp add: algebra_simps) 

287 
qed 

288 

289 
lemma convex_negations: "convex s \<Longrightarrow> convex ((\<lambda>x. x)` s)" 

290 
using assms unfolding convex_def image_iff 

291 
proof safe 

292 
fix x xa y xb :: "'a::real_vector" fix u v :: real 

293 
assume asm: "\<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" 

294 
"xa \<in> s" "xb \<in> s" "0 \<le> u" "0 \<le> v" "u + v = 1" 

295 
show "\<exists>x\<in>s. u *\<^sub>R  xa + v *\<^sub>R  xb =  x" 

296 
using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by auto 

297 
qed 

298 

299 
lemma convex_sums: 

300 
assumes "convex s" "convex t" 

301 
shows "convex {x + y x y. x \<in> s \<and> y \<in> t}" 

302 
using assms unfolding convex_def image_iff 

303 
proof safe 

304 
fix xa xb ya yb assume xy:"xa\<in>s" "xb\<in>s" "ya\<in>t" "yb\<in>t" 

305 
fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1" 

306 
show "\<exists>x y. u *\<^sub>R (xa + ya) + v *\<^sub>R (xb + yb) = x + y \<and> x \<in> s \<and> y \<in> t" 

307 
using exI[of _ "u *\<^sub>R xa + v *\<^sub>R xb"] exI[of _ "u *\<^sub>R ya + v *\<^sub>R yb"] 

308 
assms[unfolded convex_def] uv xy by (auto simp add:scaleR_right_distrib) 

309 
qed 

310 

311 
lemma convex_differences: 

312 
assumes "convex s" "convex t" 

313 
shows "convex {x  y x y. x \<in> s \<and> y \<in> t}" 

314 
proof  

315 
have "{x  y x y. x \<in> s \<and> y \<in> t} = {x + y x y. x \<in> s \<and> y \<in> uminus ` t}" 

316 
proof safe 

317 
fix x x' y assume "x' \<in> s" "y \<in> t" 

318 
thus "\<exists>x y'. x'  y = x + y' \<and> x \<in> s \<and> y' \<in> uminus ` t" 

319 
using exI[of _ x'] exI[of _ "y"] by auto 

320 
next 

321 
fix x x' y y' assume "x' \<in> s" "y' \<in> t" 

322 
thus "\<exists>x y. x' +  y' = x  y \<and> x \<in> s \<and> y \<in> t" 

323 
using exI[of _ x'] exI[of _ y'] by auto 

324 
qed 

325 
thus ?thesis using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto 

326 
qed 

327 

328 
lemma convex_translation: assumes "convex s" shows "convex ((\<lambda>x. a + x) ` s)" 

329 
proof have "{a + y y. y \<in> s} = (\<lambda>x. a + x) ` s" by auto 

330 
thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed 

331 

332 
lemma convex_affinity: assumes "convex s" shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)" 

333 
proof have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto 

334 
thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed 

335 

336 
lemma convex_linear_image: 

337 
assumes c:"convex s" and l:"bounded_linear f" 

338 
shows "convex(f ` s)" 

339 
proof(auto simp add: convex_def) 

340 
interpret f: bounded_linear f by fact 

341 
fix x y assume xy:"x \<in> s" "y \<in> s" 

342 
fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1" 

343 
show "u *\<^sub>R f x + v *\<^sub>R f y \<in> f ` s" unfolding image_iff 

344 
using bexI[of _ "u *\<^sub>R x + v *\<^sub>R y"] f.add f.scaleR 

345 
c[unfolded convex_def] xy uv by auto 

346 
qed 

347 

348 

349 
lemma pos_is_convex: 

350 
shows "convex {0 :: real <..}" 

351 
unfolding convex_alt 

352 
proof safe 

353 
fix y x \<mu> :: real 

354 
assume asms: "y > 0" "x > 0" "\<mu> \<ge> 0" "\<mu> \<le> 1" 

355 
{ assume "\<mu> = 0" 

356 
hence "\<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y = y" by simp 

357 
hence "\<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y > 0" using asms by simp } 

358 
moreover 

359 
{ assume "\<mu> = 1" 

360 
hence "\<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y > 0" using asms by simp } 

361 
moreover 

362 
{ assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0" 

363 
hence "\<mu> > 0" "(1  \<mu>) > 0" using asms by auto 

364 
hence "\<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y > 0" using asms 

36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
36648
diff
changeset

365 
by (auto simp add: add_pos_pos mult_pos_pos) } 
36623  366 
ultimately show "(1  \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastsimp 
367 
qed 

368 

369 
lemma convex_on_setsum: 

370 
fixes a :: "'a \<Rightarrow> real" 

371 
fixes y :: "'a \<Rightarrow> 'b::real_vector" 

372 
fixes f :: "'b \<Rightarrow> real" 

373 
assumes "finite s" "s \<noteq> {}" 

374 
assumes "convex_on C f" 

375 
assumes "convex C" 

376 
assumes "(\<Sum> i \<in> s. a i) = 1" 

377 
assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0" 

378 
assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> C" 

379 
shows "f (\<Sum> i \<in> s. a i *\<^sub>R y i) \<le> (\<Sum> i \<in> s. a i * f (y i))" 

380 
using assms 

381 
proof (induct s arbitrary:a rule:finite_ne_induct) 

382 
case (singleton i) 

383 
hence ai: "a i = 1" by auto 

384 
thus ?case by auto 

385 
next 

386 
case (insert i s) note asms = this 

387 
hence "convex_on C f" by simp 

388 
from this[unfolded convex_on_def, rule_format] 

389 
have conv: "\<And> x y \<mu>. \<lbrakk>x \<in> C; y \<in> C; 0 \<le> \<mu>; \<mu> \<le> 1\<rbrakk> 

390 
\<Longrightarrow> f (\<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1  \<mu>) * f y" 

391 
by simp 

392 
{ assume "a i = 1" 

393 
hence "(\<Sum> j \<in> s. a j) = 0" 

394 
using asms by auto 

395 
hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0" 

396 
using setsum_nonneg_0[where 'b=real] asms by fastsimp 

397 
hence ?case using asms by auto } 

398 
moreover 

399 
{ assume asm: "a i \<noteq> 1" 

400 
from asms have yai: "y i \<in> C" "a i \<ge> 0" by auto 

401 
have fis: "finite (insert i s)" using asms by auto 

402 
hence ai1: "a i \<le> 1" using setsum_nonneg_leq_bound[of "insert i s" a] asms by simp 

403 
hence "a i < 1" using asm by auto 

404 
hence i0: "1  a i > 0" by auto 

405 
let "?a j" = "a j / (1  a i)" 

406 
{ fix j assume "j \<in> s" 

407 
hence "?a j \<ge> 0" 

408 
using i0 asms divide_nonneg_pos 

409 
by fastsimp } note a_nonneg = this 

410 
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto 

411 
hence "(\<Sum> j \<in> s. a j) = 1  a i" using setsum.insert asms by fastsimp 

412 
hence "(\<Sum> j \<in> s. a j) / (1  a i) = 1" using i0 by auto 

413 
hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding divide.setsum by simp 

414 
have "convex C" using asms by auto 

415 
hence asum: "(\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C" 

416 
using asms convex_setsum[OF `finite s` 

417 
`convex C` a1 a_nonneg] by auto 

418 
have asum_le: "f (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<le> (\<Sum> j \<in> s. ?a j * f (y j))" 

419 
using a_nonneg a1 asms by blast 

420 
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)" 

421 
using setsum.insert[of s i "\<lambda> j. a j *\<^sub>R y j", OF `finite s` `i \<notin> s`] asms 

422 
by (auto simp only:add_commute) 

423 
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)" 

424 
using i0 by auto 

425 
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)" 

426 
using scaleR_right.setsum[of "inverse (1  a i)" "\<lambda> j. a j *\<^sub>R y j" s, symmetric] by (auto simp:algebra_simps) 

427 
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)" 

36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
36648
diff
changeset

428 
by (auto simp: divide_inverse) 
36623  429 
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)" 
430 
using conv[of "y i" "(\<Sum> j \<in> s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1] 

431 
by (auto simp add:add_commute) 

432 
also have "\<dots> \<le> (1  a i) * (\<Sum> j \<in> s. ?a j * f (y j)) + a i * f (y i)" 

433 
using add_right_mono[OF mult_left_mono[of _ _ "1  a i", 

434 
OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp 

435 
also have "\<dots> = (\<Sum> j \<in> s. (1  a i) * ?a j * f (y j)) + a i * f (y i)" 

436 
unfolding mult_right.setsum[of "1  a i" "\<lambda> j. ?a j * f (y j)"] using i0 by auto 

437 
also have "\<dots> = (\<Sum> j \<in> s. a j * f (y j)) + a i * f (y i)" using i0 by auto 

438 
also have "\<dots> = (\<Sum> j \<in> insert i s. a j * f (y j))" using asms by auto 

439 
finally have "f (\<Sum> j \<in> insert i s. a j *\<^sub>R y j) \<le> (\<Sum> j \<in> insert i s. a j * f (y j))" 

440 
by simp } 

441 
ultimately show ?case by auto 

442 
qed 

443 

444 
lemma convex_on_alt: 

445 
fixes C :: "'a::real_vector set" 

446 
assumes "convex C" 

447 
shows "convex_on C f = 

448 
(\<forall> x \<in> C. \<forall> y \<in> C. \<forall> \<mu> :: real. \<mu> \<ge> 0 \<and> \<mu> \<le> 1 

449 
\<longrightarrow> f (\<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1  \<mu>) * f y)" 

450 
proof safe 

451 
fix x y fix \<mu> :: real 

452 
assume asms: "convex_on C f" "x \<in> C" "y \<in> C" "0 \<le> \<mu>" "\<mu> \<le> 1" 

453 
from this[unfolded convex_on_def, rule_format] 

454 
have "\<And> u v. \<lbrakk>0 \<le> u; 0 \<le> v; u + v = 1\<rbrakk> \<Longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" by auto 

455 
from this[of "\<mu>" "1  \<mu>", simplified] asms 

456 
show "f (\<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y) 

457 
\<le> \<mu> * f x + (1  \<mu>) * f y" by auto 

458 
next 

459 
assume asm: "\<forall>x\<in>C. \<forall>y\<in>C. \<forall>\<mu>. 0 \<le> \<mu> \<and> \<mu> \<le> 1 \<longrightarrow> f (\<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1  \<mu>) * f y" 

460 
{fix x y fix u v :: real 

461 
assume lasm: "x \<in> C" "y \<in> C" "u \<ge> 0" "v \<ge> 0" "u + v = 1" 

462 
hence[simp]: "1  u = v" by auto 

463 
from asm[rule_format, of x y u] 

464 
have "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" using lasm by auto } 

465 
thus "convex_on C f" unfolding convex_on_def by auto 

466 
qed 

467 

43337  468 
lemma convex_on_diff: 
469 
fixes f :: "real \<Rightarrow> real" 

470 
assumes f: "convex_on I f" and I: "x\<in>I" "y\<in>I" and t: "x < t" "t < y" 

471 
shows "(f x  f t) / (x  t) \<le> (f x  f y) / (x  y)" "(f x  f y) / (x  y) \<le> (f t  f y) / (t  y)" 

472 
proof  

473 
def a \<equiv> "(t  y) / (x  y)" 

474 
with t have "0 \<le> a" "0 \<le> 1  a" by (auto simp: field_simps) 

475 
with f `x \<in> I` `y \<in> I` have cvx: "f (a * x + (1  a) * y) \<le> a * f x + (1  a) * f y" 

476 
by (auto simp: convex_on_def) 

477 
have "a * x + (1  a) * y = a * (x  y) + y" by (simp add: field_simps) 

478 
also have "\<dots> = t" unfolding a_def using `x < t` `t < y` by simp 

479 
finally have "f t \<le> a * f x + (1  a) * f y" using cvx by simp 

480 
also have "\<dots> = a * (f x  f y) + f y" by (simp add: field_simps) 

481 
finally have "f t  f y \<le> a * (f x  f y)" by simp 

482 
with t show "(f x  f t) / (x  t) \<le> (f x  f y) / (x  y)" 

44142  483 
by (simp add: le_divide_eq divide_le_eq field_simps a_def) 
43337  484 
with t show "(f x  f y) / (x  y) \<le> (f t  f y) / (t  y)" 
44142  485 
by (simp add: le_divide_eq divide_le_eq field_simps) 
43337  486 
qed 
36623  487 

488 
lemma pos_convex_function: 

489 
fixes f :: "real \<Rightarrow> real" 

490 
assumes "convex C" 

491 
assumes leq: "\<And> x y. \<lbrakk>x \<in> C ; y \<in> C\<rbrakk> \<Longrightarrow> f' x * (y  x) \<le> f y  f x" 

492 
shows "convex_on C f" 

493 
unfolding convex_on_alt[OF assms(1)] 

494 
using assms 

495 
proof safe 

496 
fix x y \<mu> :: real 

497 
let ?x = "\<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y" 

498 
assume asm: "convex C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1" 

499 
hence "1  \<mu> \<ge> 0" by auto 

500 
hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp 

501 
have geq: "\<mu> * (f x  f ?x) + (1  \<mu>) * (f y  f ?x) 

502 
\<ge> \<mu> * f' ?x * (x  ?x) + (1  \<mu>) * f' ?x * (y  ?x)" 

38642
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
36778
diff
changeset

503 
using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`] 
8fa437809c67
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
haftmann
parents:
36778
diff
changeset

504 
mult_left_mono[OF leq[OF xpos asm(3)] `1  \<mu> \<ge> 0`]] by auto 
36623  505 
hence "\<mu> * f x + (1  \<mu>) * f y  f ?x \<ge> 0" 
506 
by (auto simp add:field_simps) 

507 
thus "f (\<mu> *\<^sub>R x + (1  \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1  \<mu>) * f y" 

508 
using convex_on_alt by auto 

509 
qed 

510 

511 
lemma atMostAtLeast_subset_convex: 

512 
fixes C :: "real set" 

513 
assumes "convex C" 

514 
assumes "x \<in> C" "y \<in> C" "x < y" 

515 
shows "{x .. y} \<subseteq> C" 

516 
proof safe 

517 
fix z assume zasm: "z \<in> {x .. y}" 

518 
{ assume asm: "x < z" "z < y" 

519 
let "?\<mu>" = "(y  z) / (y  x)" 

520 
have "0 \<le> ?\<mu>" "?\<mu> \<le> 1" using assms asm by (auto simp add:field_simps) 

521 
hence comb: "?\<mu> * x + (1  ?\<mu>) * y \<in> C" 

522 
using assms iffD1[OF convex_alt, rule_format, of C y x ?\<mu>] by (simp add:algebra_simps) 

523 
have "?\<mu> * x + (1  ?\<mu>) * y = (y  z) * x / (y  x) + (1  (y  z) / (y  x)) * y" 

524 
by (auto simp add:field_simps) 

525 
also have "\<dots> = ((y  z) * x + (y  x  (y  z)) * y) / (y  x)" 

526 
using assms unfolding add_divide_distrib by (auto simp:field_simps) 

527 
also have "\<dots> = z" 

528 
using assms by (auto simp:field_simps) 

529 
finally have "z \<in> C" 

530 
using comb by auto } note less = this 

531 
show "z \<in> C" using zasm less assms 

532 
unfolding atLeastAtMost_iff le_less by auto 

533 
qed 

534 

535 
lemma f''_imp_f': 

536 
fixes f :: "real \<Rightarrow> real" 

537 
assumes "convex C" 

538 
assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)" 

539 
assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)" 

540 
assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0" 

541 
assumes "x \<in> C" "y \<in> C" 

542 
shows "f' x * (y  x) \<le> f y  f x" 

543 
using assms 

544 
proof  

545 
{ fix x y :: real assume asm: "x \<in> C" "y \<in> C" "y > x" 

546 
hence ge: "y  x > 0" "y  x \<ge> 0" by auto 

547 
from asm have le: "x  y < 0" "x  y \<le> 0" by auto 

548 
then obtain z1 where z1: "z1 > x" "z1 < y" "f y  f x = (y  x) * f' z1" 

549 
using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `x \<in> C` `y \<in> C` `x < y`], 

550 
THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] 

551 
by auto 

552 
hence "z1 \<in> C" using atMostAtLeast_subset_convex 

553 
`convex C` `x \<in> C` `y \<in> C` `x < y` by fastsimp 

554 
from z1 have z1': "f x  f y = (x  y) * f' z1" 

555 
by (simp add:field_simps) 

556 
obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1  f' x = (z1  x) * f'' z2" 

557 
using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `x \<in> C` `z1 \<in> C` `x < z1`], 

558 
THEN f'', THEN MVT2[OF `x < z1`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 

559 
by auto 

560 
obtain z3 where z3: "z3 > z1" "z3 < y" "f' y  f' z1 = (y  z1) * f'' z3" 

561 
using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `z1 \<in> C` `y \<in> C` `z1 < y`], 

562 
THEN f'', THEN MVT2[OF `z1 < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 

563 
by auto 

564 
have "f' y  (f x  f y) / (x  y) = f' y  f' z1" 

565 
using asm z1' by auto 

566 
also have "\<dots> = (y  z1) * f'' z3" using z3 by auto 

567 
finally have cool': "f' y  (f x  f y) / (x  y) = (y  z1) * f'' z3" by simp 

568 
have A': "y  z1 \<ge> 0" using z1 by auto 

569 
have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex 

570 
`convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastsimp 

571 
hence B': "f'' z3 \<ge> 0" using assms by auto 

572 
from A' B' have "(y  z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto 

573 
from cool' this have "f' y  (f x  f y) / (x  y) \<ge> 0" by auto 

574 
from mult_right_mono_neg[OF this le(2)] 

575 
have "f' y * (x  y)  (f x  f y) / (x  y) * (x  y) \<le> 0 * (x  y)" 

36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
36648
diff
changeset

576 
by (simp add: algebra_simps) 
36623  577 
hence "f' y * (x  y)  (f x  f y) \<le> 0" using le by auto 
578 
hence res: "f' y * (x  y) \<le> f x  f y" by auto 

579 
have "(f y  f x) / (y  x)  f' x = f' z1  f' x" 

580 
using asm z1 by auto 

581 
also have "\<dots> = (z1  x) * f'' z2" using z2 by auto 

582 
finally have cool: "(f y  f x) / (y  x)  f' x = (z1  x) * f'' z2" by simp 

583 
have A: "z1  x \<ge> 0" using z1 by auto 

584 
have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex 

585 
`convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastsimp 

586 
hence B: "f'' z2 \<ge> 0" using assms by auto 

587 
from A B have "(z1  x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto 

588 
from cool this have "(f y  f x) / (y  x)  f' x \<ge> 0" by auto 

589 
from mult_right_mono[OF this ge(2)] 

590 
have "(f y  f x) / (y  x) * (y  x)  f' x * (y  x) \<ge> 0 * (y  x)" 

36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
36648
diff
changeset

591 
by (simp add: algebra_simps) 
36623  592 
hence "f y  f x  f' x * (y  x) \<ge> 0" using ge by auto 
593 
hence "f y  f x \<ge> f' x * (y  x)" "f' y * (x  y) \<le> f x  f y" 

594 
using res by auto } note less_imp = this 

595 
{ fix x y :: real assume "x \<in> C" "y \<in> C" "x \<noteq> y" 

596 
hence"f y  f x \<ge> f' x * (y  x)" 

597 
unfolding neq_iff using less_imp by auto } note neq_imp = this 

598 
moreover 

599 
{ fix x y :: real assume asm: "x \<in> C" "y \<in> C" "x = y" 

600 
hence "f y  f x \<ge> f' x * (y  x)" by auto } 

601 
ultimately show ?thesis using assms by blast 

602 
qed 

603 

604 
lemma f''_ge0_imp_convex: 

605 
fixes f :: "real \<Rightarrow> real" 

606 
assumes conv: "convex C" 

607 
assumes f': "\<And> x. x \<in> C \<Longrightarrow> DERIV f x :> (f' x)" 

608 
assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)" 

609 
assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0" 

610 
shows "convex_on C f" 

611 
using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp 

612 

613 
lemma minus_log_convex: 

614 
fixes b :: real 

615 
assumes "b > 1" 

616 
shows "convex_on {0 <..} (\<lambda> x.  log b x)" 

617 
proof  

618 
have "\<And> z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto 

619 
hence f': "\<And> z. z > 0 \<Longrightarrow> DERIV (\<lambda> z.  log b z) z :>  1 / (ln b * z)" 

620 
using DERIV_minus by auto 

621 
have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV inverse z :>  (inverse z ^ Suc (Suc 0))" 

622 
using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto 

623 
from this[THEN DERIV_cmult, of _ " 1 / ln b"] 

624 
have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. ( 1 / ln b) * inverse z) z :> ( 1 / ln b) * ( (inverse z ^ Suc (Suc 0)))" 

625 
by auto 

626 
hence f''0: "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z.  1 / (ln b * z)) z :> 1 / (ln b * z * z)" 

36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
36648
diff
changeset

627 
unfolding inverse_eq_divide by (auto simp add: mult_assoc) 
36623  628 
have f''_ge0: "\<And> z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0" 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
36648
diff
changeset

629 
using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] mult_pos_pos) 
36623  630 
from f''_ge0_imp_convex[OF pos_is_convex, 
631 
unfolded greaterThan_iff, OF f' f''0 f''_ge0] 

632 
show ?thesis by auto 

633 
qed 

634 

635 
end 