(* Title: HOL/Library/Convex.thy Author: Armin Heller, TU Muenchen Author: Johannes Hoelzl, TU Muenchen *) header {* Convexity in real vector spaces *} theory Convex imports Product_Vector begin subsection {* Convexity. *} definition convex :: "'a::real_vector set \ bool" where "convex s \ (\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s)" lemma convex_alt: "convex s \ (\x\s. \y\s. \u. 0 \ u \ u \ 1 \ ((1 - u) *\<^sub>R x + u *\<^sub>R y) \ s)" (is "_ \ ?alt") proof assume alt[rule_format]: ?alt { fix x y and u v :: real assume mem: "x \ s" "y \ s" assume "0 \ u" "0 \ v" "u + v = 1" moreover hence "u = 1 - v" by auto ultimately have "u *\<^sub>R x + v *\<^sub>R y \ s" using alt[OF mem] by auto } thus "convex s" unfolding convex_def by auto qed (auto simp: convex_def) lemma mem_convex: assumes "convex s" "a \ s" "b \ s" "0 \ u" "u \ 1" shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \ s" using assms unfolding convex_alt by auto lemma convex_empty[intro]: "convex {}" unfolding convex_def by simp lemma convex_singleton[intro]: "convex {a}" unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric]) lemma convex_UNIV[intro]: "convex UNIV" unfolding convex_def by auto lemma convex_Inter: "(\s\f. convex s) ==> convex(\ f)" unfolding convex_def by auto lemma convex_Int: "convex s \ convex t \ convex (s \ t)" unfolding convex_def by auto lemma convex_halfspace_le: "convex {x. inner a x \ b}" unfolding convex_def by (auto simp: inner_add inner_scaleR intro!: convex_bound_le) lemma convex_halfspace_ge: "convex {x. inner a x \ b}" proof - have *:"{x. inner a x \ b} = {x. inner (-a) x \ -b}" by auto show ?thesis unfolding * using convex_halfspace_le[of "-a" "-b"] by auto qed lemma convex_hyperplane: "convex {x. inner a x = b}" proof- have *:"{x. inner a x = b} = {x. inner a x \ b} \ {x. inner a x \ b}" by auto show ?thesis using convex_halfspace_le convex_halfspace_ge by (auto intro!: convex_Int simp: *) qed lemma convex_halfspace_lt: "convex {x. inner a x < b}" unfolding convex_def by (auto simp: convex_bound_lt inner_add) lemma convex_halfspace_gt: "convex {x. inner a x > b}" using convex_halfspace_lt[of "-a" "-b"] by auto lemma convex_real_interval: fixes a b :: "real" shows "convex {a..}" and "convex {..b}" and "convex {a<..}" and "convex {.. inner 1 x}" by auto thus 1: "convex {a..}" by (simp only: convex_halfspace_ge) have "{..b} = {x. inner 1 x \ b}" by auto thus 2: "convex {..b}" by (simp only: convex_halfspace_le) have "{a<..} = {x. a < inner 1 x}" by auto thus 3: "convex {a<..}" by (simp only: convex_halfspace_gt) have "{.. {..b}" by auto thus "convex {a..b}" by (simp only: convex_Int 1 2) have "{a<..b} = {a<..} \ {..b}" by auto thus "convex {a<..b}" by (simp only: convex_Int 3 2) have "{a.. {.. {.. i \ s. a i) = 1" assumes "\ i. i \ s \ a i \ 0" and "\ i. i \ s \ y i \ C" shows "(\ j \ s. a j *\<^sub>R y j) \ C" using assms proof (induct s arbitrary:a rule:finite_induct) case empty thus ?case by auto next case (insert i s) note asms = this { assume "a i = 1" hence "(\ j \ s. a j) = 0" using asms by auto hence "\ j. j \ s \ a j = 0" using setsum_nonneg_0[where 'b=real] asms by fastsimp hence ?case using asms by auto } moreover { assume asm: "a i \ 1" from asms have yai: "y i \ C" "a i \ 0" by auto have fis: "finite (insert i s)" using asms by auto hence ai1: "a i \ 1" using setsum_nonneg_leq_bound[of "insert i s" a 1] asms by simp hence "a i < 1" using asm by auto hence i0: "1 - a i > 0" by auto let "?a j" = "a j / (1 - a i)" { fix j assume "j \ s" hence "?a j \ 0" using i0 asms divide_nonneg_pos by fastsimp } note a_nonneg = this have "(\ j \ insert i s. a j) = 1" using asms by auto hence "(\ j \ s. a j) = 1 - a i" using setsum.insert asms by fastsimp hence "(\ j \ s. a j) / (1 - a i) = 1" using i0 by auto hence a1: "(\ j \ s. ?a j) = 1" unfolding divide.setsum by simp from this asms have "(\j\s. ?a j *\<^sub>R y j) \ C" using a_nonneg by fastsimp hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\ j \ s. ?a j *\<^sub>R y j) \ C" using asms[unfolded convex_def, rule_format] yai ai1 by auto hence "a i *\<^sub>R y i + (\ j \ s. (1 - a i) *\<^sub>R (?a j *\<^sub>R y j)) \ C" using scaleR_right.setsum[of "(1 - a i)" "\ j. ?a j *\<^sub>R y j" s] by auto hence "a i *\<^sub>R y i + (\ j \ s. a j *\<^sub>R y j) \ C" using i0 by auto hence ?case using setsum.insert asms by auto } ultimately show ?case by auto qed lemma convex: shows "convex s \ (\(k::nat) u x. (\i. 1\i \ i\k \ 0 \ u i \ x i \s) \ (setsum u {1..k} = 1) \ setsum (\i. u i *\<^sub>R x i) {1..k} \ s)" proof safe fix k :: nat fix u :: "nat \ real" fix x assume "convex s" "\i. 1 \ i \ i \ k \ 0 \ u i \ x i \ s" "setsum u {1..k} = 1" from this convex_setsum[of "{1 .. k}" s] show "(\j\{1 .. k}. u j *\<^sub>R x j) \ s" by auto next assume asm: "\k u x. (\ i :: nat. 1 \ i \ i \ k \ 0 \ u i \ x i \ s) \ setsum u {1..k} = 1 \ (\i = 1..k. u i *\<^sub>R (x i :: 'a)) \ s" { fix \ :: real fix x y :: 'a assume xy: "x \ s" "y \ s" assume mu: "\ \ 0" "\ \ 1" let "?u i" = "if (i :: nat) = 1 then \ else 1 - \" let "?x i" = "if (i :: nat) = 1 then x else y" have "{1 :: nat .. 2} \ - {x. x = 1} = {2}" by auto hence card: "card ({1 :: nat .. 2} \ - {x. x = 1}) = 1" by simp hence "setsum ?u {1 .. 2} = 1" using setsum_cases[of "{(1 :: nat) .. 2}" "\ x. x = 1" "\ x. \" "\ x. 1 - \"] by auto from this asm[rule_format, of "2" ?u ?x] have s: "(\j \ {1..2}. ?u j *\<^sub>R ?x j) \ s" using mu xy by auto have grarr: "(\j \ {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \) *\<^sub>R y" using setsum_head_Suc[of "Suc (Suc 0)" 2 "\ j. (1 - \) *\<^sub>R y"] by auto from setsum_head_Suc[of "Suc 0" 2 "\ j. ?u j *\<^sub>R ?x j", simplified this] have "(\j \ {1..2}. ?u j *\<^sub>R ?x j) = \ *\<^sub>R x + (1 - \) *\<^sub>R y" by auto hence "(1 - \) *\<^sub>R y + \ *\<^sub>R x \ s" using s by (auto simp:add_commute) } thus "convex s" unfolding convex_alt by auto qed lemma convex_explicit: fixes s :: "'a::real_vector set" shows "convex s \ (\t u. finite t \ t \ s \ (\x\t. 0 \ u x) \ setsum u t = 1 \ setsum (\x. u x *\<^sub>R x) t \ s)" proof safe fix t fix u :: "'a \ real" assume "convex s" "finite t" "t \ s" "\x\t. 0 \ u x" "setsum u t = 1" thus "(\x\t. u x *\<^sub>R x) \ s" using convex_setsum[of t s u "\ x. x"] by auto next assume asm0: "\t. \ u. finite t \ t \ s \ (\x\t. 0 \ u x) \ setsum u t = 1 \ (\x\t. u x *\<^sub>R x) \ s" show "convex s" unfolding convex_alt proof safe fix x y fix \ :: real assume asm: "x \ s" "y \ s" "0 \ \" "\ \ 1" { assume "x \ y" hence "(1 - \) *\<^sub>R x + \ *\<^sub>R y \ s" using asm0[rule_format, of "{x, y}" "\ z. if z = x then 1 - \ else \"] asm by auto } moreover { assume "x = y" hence "(1 - \) *\<^sub>R x + \ *\<^sub>R y \ s" using asm0[rule_format, of "{x, y}" "\ z. 1"] asm by (auto simp:field_simps real_vector.scale_left_diff_distrib) } ultimately show "(1 - \) *\<^sub>R x + \ *\<^sub>R y \ s" by blast qed qed lemma convex_finite: assumes "finite s" shows "convex s \ (\u. (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\x. u x *\<^sub>R x) s \ s)" unfolding convex_explicit proof (safe elim!: conjE) fix t u assume sum: "\u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) \ s" and as: "finite t" "t \ s" "\x\t. 0 \ u x" "setsum u t = (1::real)" have *:"s \ t = t" using as(2) by auto have if_distrib_arg: "\P f g x. (if P then f else g) x = (if P then f x else g x)" by simp show "(\x\t. u x *\<^sub>R x) \ s" using sum[THEN spec[where x="\x. if x\t then u x else 0"]] as * by (auto simp: assms setsum_cases if_distrib if_distrib_arg) qed (erule_tac x=s in allE, erule_tac x=u in allE, auto) definition convex_on :: "'a::real_vector set \ ('a \ real) \ bool" where "convex_on s f \ (\x\s. \y\s. \u\0. \v\0. u + v = 1 \ f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y)" lemma convex_on_subset: "convex_on t f \ s \ t \ convex_on s f" unfolding convex_on_def by auto lemma convex_add[intro]: assumes "convex_on s f" "convex_on s g" shows "convex_on s (\x. f x + g x)" proof- { fix x y assume "x\s" "y\s" moreover fix u v ::real assume "0 \ u" "0 \ v" "u + v = 1" ultimately have "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \ (u * f x + v * f y) + (u * g x + v * g y)" using assms unfolding convex_on_def by (auto simp add:add_mono) hence "f (u *\<^sub>R x + v *\<^sub>R y) + g (u *\<^sub>R x + v *\<^sub>R y) \ u * (f x + g x) + v * (f y + g y)" by (simp add: field_simps) } thus ?thesis unfolding convex_on_def by auto qed lemma convex_cmul[intro]: assumes "0 \ (c::real)" "convex_on s f" shows "convex_on s (\x. c * f x)" proof- have *:"\u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps) show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto qed lemma convex_lower: assumes "convex_on s f" "x\s" "y \ s" "0 \ u" "0 \ v" "u + v = 1" shows "f (u *\<^sub>R x + v *\<^sub>R y) \ max (f x) (f y)" proof- let ?m = "max (f x) (f y)" have "u * f x + v * f y \ u * max (f x) (f y) + v * max (f x) (f y)" using assms(4,5) by(auto simp add: mult_mono1 add_mono) also have "\ = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto finally show ?thesis using assms unfolding convex_on_def by fastsimp qed lemma convex_distance[intro]: fixes s :: "'a::real_normed_vector set" shows "convex_on s (\x. dist a x)" proof(auto simp add: convex_on_def dist_norm) fix x y assume "x\s" "y\s" fix u v ::real assume "0 \ u" "0 \ v" "u + v = 1" have "a = u *\<^sub>R a + v *\<^sub>R a" unfolding scaleR_left_distrib[THEN sym] and `u+v=1` by simp hence *:"a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))" by (auto simp add: algebra_simps) show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \ u * norm (a - x) + v * norm (a - y)" unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"] using `0 \ u` `0 \ v` by auto qed subsection {* Arithmetic operations on sets preserve convexity. *} lemma convex_scaling: assumes "convex s" shows"convex ((\x. c *\<^sub>R x) ` s)" using assms unfolding convex_def image_iff proof safe fix x xa y xb :: "'a::real_vector" fix u v :: real assume asm: "\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" "xa \ s" "xb \ s" "0 \ u" "0 \ v" "u + v = 1" show "\x\s. u *\<^sub>R c *\<^sub>R xa + v *\<^sub>R c *\<^sub>R xb = c *\<^sub>R x" using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by (auto simp add: algebra_simps) qed lemma convex_negations: "convex s \ convex ((\x. -x)` s)" using assms unfolding convex_def image_iff proof safe fix x xa y xb :: "'a::real_vector" fix u v :: real assume asm: "\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" "xa \ s" "xb \ s" "0 \ u" "0 \ v" "u + v = 1" show "\x\s. u *\<^sub>R - xa + v *\<^sub>R - xb = - x" using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by auto qed lemma convex_sums: assumes "convex s" "convex t" shows "convex {x + y| x y. x \ s \ y \ t}" using assms unfolding convex_def image_iff proof safe fix xa xb ya yb assume xy:"xa\s" "xb\s" "ya\t" "yb\t" fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" show "\x y. u *\<^sub>R (xa + ya) + v *\<^sub>R (xb + yb) = x + y \ x \ s \ y \ t" using exI[of _ "u *\<^sub>R xa + v *\<^sub>R xb"] exI[of _ "u *\<^sub>R ya + v *\<^sub>R yb"] assms[unfolded convex_def] uv xy by (auto simp add:scaleR_right_distrib) qed lemma convex_differences: assumes "convex s" "convex t" shows "convex {x - y| x y. x \ s \ y \ t}" proof - have "{x - y| x y. x \ s \ y \ t} = {x + y |x y. x \ s \ y \ uminus ` t}" proof safe fix x x' y assume "x' \ s" "y \ t" thus "\x y'. x' - y = x + y' \ x \ s \ y' \ uminus ` t" using exI[of _ x'] exI[of _ "-y"] by auto next fix x x' y y' assume "x' \ s" "y' \ t" thus "\x y. x' + - y' = x - y \ x \ s \ y \ t" using exI[of _ x'] exI[of _ y'] by auto qed thus ?thesis using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto qed lemma convex_translation: assumes "convex s" shows "convex ((\x. a + x) ` s)" proof- have "{a + y |y. y \ s} = (\x. a + x) ` s" by auto thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed lemma convex_affinity: assumes "convex s" shows "convex ((\x. a + c *\<^sub>R x) ` s)" proof- have "(\x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed lemma convex_linear_image: assumes c:"convex s" and l:"bounded_linear f" shows "convex(f ` s)" proof(auto simp add: convex_def) interpret f: bounded_linear f by fact fix x y assume xy:"x \ s" "y \ s" fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" show "u *\<^sub>R f x + v *\<^sub>R f y \ f ` s" unfolding image_iff using bexI[of _ "u *\<^sub>R x + v *\<^sub>R y"] f.add f.scaleR c[unfolded convex_def] xy uv by auto qed lemma pos_is_convex: shows "convex {0 :: real <..}" unfolding convex_alt proof safe fix y x \ :: real assume asms: "y > 0" "x > 0" "\ \ 0" "\ \ 1" { assume "\ = 0" hence "\ *\<^sub>R x + (1 - \) *\<^sub>R y = y" by simp hence "\ *\<^sub>R x + (1 - \) *\<^sub>R y > 0" using asms by simp } moreover { assume "\ = 1" hence "\ *\<^sub>R x + (1 - \) *\<^sub>R y > 0" using asms by simp } moreover { assume "\ \ 1" "\ \ 0" hence "\ > 0" "(1 - \) > 0" using asms by auto hence "\ *\<^sub>R x + (1 - \) *\<^sub>R y > 0" using asms using add_nonneg_pos[of "\ *\<^sub>R x" "(1 - \) *\<^sub>R y"] real_mult_order by auto fastsimp } ultimately show "(1 - \) *\<^sub>R y + \ *\<^sub>R x > 0" using assms by fastsimp qed lemma convex_on_setsum: fixes a :: "'a \ real" fixes y :: "'a \ 'b::real_vector" fixes f :: "'b \ real" assumes "finite s" "s \ {}" assumes "convex_on C f" assumes "convex C" assumes "(\ i \ s. a i) = 1" assumes "\ i. i \ s \ a i \ 0" assumes "\ i. i \ s \ y i \ C" shows "f (\ i \ s. a i *\<^sub>R y i) \ (\ i \ s. a i * f (y i))" using assms proof (induct s arbitrary:a rule:finite_ne_induct) case (singleton i) hence ai: "a i = 1" by auto thus ?case by auto next case (insert i s) note asms = this hence "convex_on C f" by simp from this[unfolded convex_on_def, rule_format] have conv: "\ x y \. \x \ C; y \ C; 0 \ \; \ \ 1\ \ f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" by simp { assume "a i = 1" hence "(\ j \ s. a j) = 0" using asms by auto hence "\ j. j \ s \ a j = 0" using setsum_nonneg_0[where 'b=real] asms by fastsimp hence ?case using asms by auto } moreover { assume asm: "a i \ 1" from asms have yai: "y i \ C" "a i \ 0" by auto have fis: "finite (insert i s)" using asms by auto hence ai1: "a i \ 1" using setsum_nonneg_leq_bound[of "insert i s" a] asms by simp hence "a i < 1" using asm by auto hence i0: "1 - a i > 0" by auto let "?a j" = "a j / (1 - a i)" { fix j assume "j \ s" hence "?a j \ 0" using i0 asms divide_nonneg_pos by fastsimp } note a_nonneg = this have "(\ j \ insert i s. a j) = 1" using asms by auto hence "(\ j \ s. a j) = 1 - a i" using setsum.insert asms by fastsimp hence "(\ j \ s. a j) / (1 - a i) = 1" using i0 by auto hence a1: "(\ j \ s. ?a j) = 1" unfolding divide.setsum by simp have "convex C" using asms by auto hence asum: "(\ j \ s. ?a j *\<^sub>R y j) \ C" using asms convex_setsum[OF `finite s` `convex C` a1 a_nonneg] by auto have asum_le: "f (\ j \ s. ?a j *\<^sub>R y j) \ (\ j \ s. ?a j * f (y j))" using a_nonneg a1 asms by blast have "f (\ j \ insert i s. a j *\<^sub>R y j) = f ((\ j \ s. a j *\<^sub>R y j) + a i *\<^sub>R y i)" using setsum.insert[of s i "\ j. a j *\<^sub>R y j", OF `finite s` `i \ s`] asms by (auto simp only:add_commute) also have "\ = f (((1 - a i) * inverse (1 - a i)) *\<^sub>R (\ j \ s. a j *\<^sub>R y j) + a i *\<^sub>R y i)" using i0 by auto also have "\ = f ((1 - a i) *\<^sub>R (\ j \ s. (a j * inverse (1 - a i)) *\<^sub>R y j) + a i *\<^sub>R y i)" using scaleR_right.setsum[of "inverse (1 - a i)" "\ j. a j *\<^sub>R y j" s, symmetric] by (auto simp:algebra_simps) also have "\ = f ((1 - a i) *\<^sub>R (\ j \ s. ?a j *\<^sub>R y j) + a i *\<^sub>R y i)" by (auto simp:real_divide_def) also have "\ \ (1 - a i) *\<^sub>R f ((\ j \ s. ?a j *\<^sub>R y j)) + a i * f (y i)" using conv[of "y i" "(\ j \ s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1] by (auto simp add:add_commute) also have "\ \ (1 - a i) * (\ j \ s. ?a j * f (y j)) + a i * f (y i)" using add_right_mono[OF mult_left_mono[of _ _ "1 - a i", OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp also have "\ = (\ j \ s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)" unfolding mult_right.setsum[of "1 - a i" "\ j. ?a j * f (y j)"] using i0 by auto also have "\ = (\ j \ s. a j * f (y j)) + a i * f (y i)" using i0 by auto also have "\ = (\ j \ insert i s. a j * f (y j))" using asms by auto finally have "f (\ j \ insert i s. a j *\<^sub>R y j) \ (\ j \ insert i s. a j * f (y j))" by simp } ultimately show ?case by auto qed lemma convex_on_alt: fixes C :: "'a::real_vector set" assumes "convex C" shows "convex_on C f = (\ x \ C. \ y \ C. \ \ :: real. \ \ 0 \ \ \ 1 \ f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y)" proof safe fix x y fix \ :: real assume asms: "convex_on C f" "x \ C" "y \ C" "0 \ \" "\ \ 1" from this[unfolded convex_on_def, rule_format] have "\ u v. \0 \ u; 0 \ v; u + v = 1\ \ f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y" by auto from this[of "\" "1 - \", simplified] asms show "f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" by auto next assume asm: "\x\C. \y\C. \\. 0 \ \ \ \ \ 1 \ f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" {fix x y fix u v :: real assume lasm: "x \ C" "y \ C" "u \ 0" "v \ 0" "u + v = 1" hence[simp]: "1 - u = v" by auto from asm[rule_format, of x y u] have "f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y" using lasm by auto } thus "convex_on C f" unfolding convex_on_def by auto qed lemma pos_convex_function: fixes f :: "real \ real" assumes "convex C" assumes leq: "\ x y. \x \ C ; y \ C\ \ f' x * (y - x) \ f y - f x" shows "convex_on C f" unfolding convex_on_alt[OF assms(1)] using assms proof safe fix x y \ :: real let ?x = "\ *\<^sub>R x + (1 - \) *\<^sub>R y" assume asm: "convex C" "x \ C" "y \ C" "\ \ 0" "\ \ 1" hence "1 - \ \ 0" by auto hence xpos: "?x \ C" using asm unfolding convex_alt by fastsimp have geq: "\ * (f x - f ?x) + (1 - \) * (f y - f ?x) \ \ * f' ?x * (x - ?x) + (1 - \) * f' ?x * (y - ?x)" using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\ \ 0`] mult_mono1[OF leq[OF xpos asm(3)] `1 - \ \ 0`]] by auto hence "\ * f x + (1 - \) * f y - f ?x \ 0" by (auto simp add:field_simps) thus "f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" using convex_on_alt by auto qed lemma atMostAtLeast_subset_convex: fixes C :: "real set" assumes "convex C" assumes "x \ C" "y \ C" "x < y" shows "{x .. y} \ C" proof safe fix z assume zasm: "z \ {x .. y}" { assume asm: "x < z" "z < y" let "?\" = "(y - z) / (y - x)" have "0 \ ?\" "?\ \ 1" using assms asm by (auto simp add:field_simps) hence comb: "?\ * x + (1 - ?\) * y \ C" using assms iffD1[OF convex_alt, rule_format, of C y x ?\] by (simp add:algebra_simps) have "?\ * x + (1 - ?\) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y" by (auto simp add:field_simps) also have "\ = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)" using assms unfolding add_divide_distrib by (auto simp:field_simps) also have "\ = z" using assms by (auto simp:field_simps) finally have "z \ C" using comb by auto } note less = this show "z \ C" using zasm less assms unfolding atLeastAtMost_iff le_less by auto qed lemma f''_imp_f': fixes f :: "real \ real" assumes "convex C" assumes f': "\ x. x \ C \ DERIV f x :> (f' x)" assumes f'': "\ x. x \ C \ DERIV f' x :> (f'' x)" assumes pos: "\ x. x \ C \ f'' x \ 0" assumes "x \ C" "y \ C" shows "f' x * (y - x) \ f y - f x" using assms proof - { fix x y :: real assume asm: "x \ C" "y \ C" "y > x" hence ge: "y - x > 0" "y - x \ 0" by auto from asm have le: "x - y < 0" "x - y \ 0" by auto then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1" using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `x \ C` `y \ C` `x < y`], THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] by auto hence "z1 \ C" using atMostAtLeast_subset_convex `convex C` `x \ C` `y \ C` `x < y` by fastsimp from z1 have z1': "f x - f y = (x - y) * f' z1" by (simp add:field_simps) obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2" using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `x \ C` `z1 \ C` `x < z1`], THEN f'', THEN MVT2[OF `x < z1`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 by auto obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3" using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `z1 \ C` `y \ C` `z1 < y`], THEN f'', THEN MVT2[OF `z1 < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 by auto have "f' y - (f x - f y) / (x - y) = f' y - f' z1" using asm z1' by auto also have "\ = (y - z1) * f'' z3" using z3 by auto finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp have A': "y - z1 \ 0" using z1 by auto have "z3 \ C" using z3 asm atMostAtLeast_subset_convex `convex C` `x \ C` `z1 \ C` `x < z1` by fastsimp hence B': "f'' z3 \ 0" using assms by auto from A' B' have "(y - z1) * f'' z3 \ 0" using mult_nonneg_nonneg by auto from cool' this have "f' y - (f x - f y) / (x - y) \ 0" by auto from mult_right_mono_neg[OF this le(2)] have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \ 0 * (x - y)" unfolding diff_def using real_add_mult_distrib by auto hence "f' y * (x - y) - (f x - f y) \ 0" using le by auto hence res: "f' y * (x - y) \ f x - f y" by auto have "(f y - f x) / (y - x) - f' x = f' z1 - f' x" using asm z1 by auto also have "\ = (z1 - x) * f'' z2" using z2 by auto finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp have A: "z1 - x \ 0" using z1 by auto have "z2 \ C" using z2 z1 asm atMostAtLeast_subset_convex `convex C` `z1 \ C` `y \ C` `z1 < y` by fastsimp hence B: "f'' z2 \ 0" using assms by auto from A B have "(z1 - x) * f'' z2 \ 0" using mult_nonneg_nonneg by auto from cool this have "(f y - f x) / (y - x) - f' x \ 0" by auto from mult_right_mono[OF this ge(2)] have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \ 0 * (y - x)" unfolding diff_def using real_add_mult_distrib by auto hence "f y - f x - f' x * (y - x) \ 0" using ge by auto hence "f y - f x \ f' x * (y - x)" "f' y * (x - y) \ f x - f y" using res by auto } note less_imp = this { fix x y :: real assume "x \ C" "y \ C" "x \ y" hence"f y - f x \ f' x * (y - x)" unfolding neq_iff using less_imp by auto } note neq_imp = this moreover { fix x y :: real assume asm: "x \ C" "y \ C" "x = y" hence "f y - f x \ f' x * (y - x)" by auto } ultimately show ?thesis using assms by blast qed lemma f''_ge0_imp_convex: fixes f :: "real \ real" assumes conv: "convex C" assumes f': "\ x. x \ C \ DERIV f x :> (f' x)" assumes f'': "\ x. x \ C \ DERIV f' x :> (f'' x)" assumes pos: "\ x. x \ C \ f'' x \ 0" shows "convex_on C f" using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp lemma minus_log_convex: fixes b :: real assumes "b > 1" shows "convex_on {0 <..} (\ x. - log b x)" proof - have "\ z. z > 0 \ DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto hence f': "\ z. z > 0 \ DERIV (\ z. - log b z) z :> - 1 / (ln b * z)" using DERIV_minus by auto have "\ z :: real. z > 0 \ DERIV inverse z :> - (inverse z ^ Suc (Suc 0))" using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto from this[THEN DERIV_cmult, of _ "- 1 / ln b"] have "\ z :: real. z > 0 \ DERIV (\ z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))" by auto hence f''0: "\ z :: real. z > 0 \ DERIV (\ z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)" unfolding inverse_eq_divide by (auto simp add:real_mult_assoc) have f''_ge0: "\ z :: real. z > 0 \ 1 / (ln b * z * z) \ 0" using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order) from f''_ge0_imp_convex[OF pos_is_convex, unfolded greaterThan_iff, OF f' f''0 f''_ge0] show ?thesis by auto qed end