src/HOL/Library/Convex.thy
 author hoelzl Mon May 03 14:35:10 2010 +0200 (2010-05-03) changeset 36623 d26348b667f2 child 36648 43b66dcd9266 permissions -rw-r--r--
Moved Convex theory to library.
 hoelzl@36623 ` 1` ```theory Convex ``` hoelzl@36623 ` 2` ```imports Product_Vector ``` hoelzl@36623 ` 3` ```begin ``` hoelzl@36623 ` 4` hoelzl@36623 ` 5` ```subsection {* Convexity. *} ``` hoelzl@36623 ` 6` hoelzl@36623 ` 7` ```definition ``` hoelzl@36623 ` 8` ``` convex :: "'a::real_vector set \ bool" where ``` hoelzl@36623 ` 9` ``` "convex s \ (\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s)" ``` hoelzl@36623 ` 10` hoelzl@36623 ` 11` ```lemma convex_alt: ``` hoelzl@36623 ` 12` ``` "convex s \ (\x\s. \y\s. \u. 0 \ u \ u \ 1 \ ((1 - u) *\<^sub>R x + u *\<^sub>R y) \ s)" ``` hoelzl@36623 ` 13` ``` (is "_ \ ?alt") ``` hoelzl@36623 ` 14` ```proof ``` hoelzl@36623 ` 15` ``` assume alt[rule_format]: ?alt ``` hoelzl@36623 ` 16` ``` { fix x y and u v :: real assume mem: "x \ s" "y \ s" ``` hoelzl@36623 ` 17` ``` assume "0 \ u" "0 \ v" "u + v = 1" ``` hoelzl@36623 ` 18` ``` moreover hence "u = 1 - v" by auto ``` hoelzl@36623 ` 19` ``` ultimately have "u *\<^sub>R x + v *\<^sub>R y \ s" using alt[OF mem] by auto } ``` hoelzl@36623 ` 20` ``` thus "convex s" unfolding convex_def by auto ``` hoelzl@36623 ` 21` ```qed (auto simp: convex_def) ``` hoelzl@36623 ` 22` hoelzl@36623 ` 23` ```lemma mem_convex: ``` hoelzl@36623 ` 24` ``` assumes "convex s" "a \ s" "b \ s" "0 \ u" "u \ 1" ``` hoelzl@36623 ` 25` ``` shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \ s" ``` hoelzl@36623 ` 26` ``` using assms unfolding convex_alt by auto ``` hoelzl@36623 ` 27` hoelzl@36623 ` 28` ```lemma convex_empty[intro]: "convex {}" ``` hoelzl@36623 ` 29` ``` unfolding convex_def by simp ``` hoelzl@36623 ` 30` hoelzl@36623 ` 31` ```lemma convex_singleton[intro]: "convex {a}" ``` hoelzl@36623 ` 32` ``` unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric]) ``` hoelzl@36623 ` 33` hoelzl@36623 ` 34` ```lemma convex_UNIV[intro]: "convex UNIV" ``` hoelzl@36623 ` 35` ``` unfolding convex_def by auto ``` hoelzl@36623 ` 36` hoelzl@36623 ` 37` ```lemma convex_Inter: "(\s\f. convex s) ==> convex(\ f)" ``` hoelzl@36623 ` 38` ``` unfolding convex_def by auto ``` hoelzl@36623 ` 39` hoelzl@36623 ` 40` ```lemma convex_Int: "convex s \ convex t \ convex (s \ t)" ``` hoelzl@36623 ` 41` ``` unfolding convex_def by auto ``` hoelzl@36623 ` 42` hoelzl@36623 ` 43` ```lemma convex_halfspace_le: "convex {x. inner a x \ b}" ``` hoelzl@36623 ` 44` ``` unfolding convex_def ``` hoelzl@36623 ` 45` ``` by (auto simp: inner_add inner_scaleR intro!: convex_bound_le) ``` hoelzl@36623 ` 46` hoelzl@36623 ` 47` ```lemma convex_halfspace_ge: "convex {x. inner a x \ b}" ``` hoelzl@36623 ` 48` ```proof - ``` hoelzl@36623 ` 49` ``` have *:"{x. inner a x \ b} = {x. inner (-a) x \ -b}" by auto ``` hoelzl@36623 ` 50` ``` show ?thesis unfolding * using convex_halfspace_le[of "-a" "-b"] by auto ``` hoelzl@36623 ` 51` ```qed ``` hoelzl@36623 ` 52` hoelzl@36623 ` 53` ```lemma convex_hyperplane: "convex {x. inner a x = b}" ``` hoelzl@36623 ` 54` ```proof- ``` hoelzl@36623 ` 55` ``` have *:"{x. inner a x = b} = {x. inner a x \ b} \ {x. inner a x \ b}" by auto ``` hoelzl@36623 ` 56` ``` show ?thesis using convex_halfspace_le convex_halfspace_ge ``` hoelzl@36623 ` 57` ``` by (auto intro!: convex_Int simp: *) ``` hoelzl@36623 ` 58` ```qed ``` hoelzl@36623 ` 59` hoelzl@36623 ` 60` ```lemma convex_halfspace_lt: "convex {x. inner a x < b}" ``` hoelzl@36623 ` 61` ``` unfolding convex_def ``` hoelzl@36623 ` 62` ``` by (auto simp: convex_bound_lt inner_add) ``` hoelzl@36623 ` 63` hoelzl@36623 ` 64` ```lemma convex_halfspace_gt: "convex {x. inner a x > b}" ``` hoelzl@36623 ` 65` ``` using convex_halfspace_lt[of "-a" "-b"] by auto ``` hoelzl@36623 ` 66` hoelzl@36623 ` 67` ```lemma convex_real_interval: ``` hoelzl@36623 ` 68` ``` fixes a b :: "real" ``` hoelzl@36623 ` 69` ``` shows "convex {a..}" and "convex {..b}" ``` hoelzl@36623 ` 70` ``` and "convex {a<..}" and "convex {.. inner 1 x}" by auto ``` hoelzl@36623 ` 75` ``` thus 1: "convex {a..}" by (simp only: convex_halfspace_ge) ``` hoelzl@36623 ` 76` ``` have "{..b} = {x. inner 1 x \ b}" by auto ``` hoelzl@36623 ` 77` ``` thus 2: "convex {..b}" by (simp only: convex_halfspace_le) ``` hoelzl@36623 ` 78` ``` have "{a<..} = {x. a < inner 1 x}" by auto ``` hoelzl@36623 ` 79` ``` thus 3: "convex {a<..}" by (simp only: convex_halfspace_gt) ``` hoelzl@36623 ` 80` ``` have "{.. {..b}" by auto ``` hoelzl@36623 ` 83` ``` thus "convex {a..b}" by (simp only: convex_Int 1 2) ``` hoelzl@36623 ` 84` ``` have "{a<..b} = {a<..} \ {..b}" by auto ``` hoelzl@36623 ` 85` ``` thus "convex {a<..b}" by (simp only: convex_Int 3 2) ``` hoelzl@36623 ` 86` ``` have "{a.. {.. {.. i \ s. a i) = 1" ``` hoelzl@36623 ` 97` ``` assumes "\ i. i \ s \ a i \ 0" and "\ i. i \ s \ y i \ C" ``` hoelzl@36623 ` 98` ``` shows "(\ j \ s. a j *\<^sub>R y j) \ C" ``` hoelzl@36623 ` 99` ```using assms ``` hoelzl@36623 ` 100` ```proof (induct s arbitrary:a rule:finite_induct) ``` hoelzl@36623 ` 101` ``` case empty thus ?case by auto ``` hoelzl@36623 ` 102` ```next ``` hoelzl@36623 ` 103` ``` case (insert i s) note asms = this ``` hoelzl@36623 ` 104` ``` { assume "a i = 1" ``` hoelzl@36623 ` 105` ``` hence "(\ j \ s. a j) = 0" ``` hoelzl@36623 ` 106` ``` using asms by auto ``` hoelzl@36623 ` 107` ``` hence "\ j. j \ s \ a j = 0" ``` hoelzl@36623 ` 108` ``` using setsum_nonneg_0[where 'b=real] asms by fastsimp ``` hoelzl@36623 ` 109` ``` hence ?case using asms by auto } ``` hoelzl@36623 ` 110` ``` moreover ``` hoelzl@36623 ` 111` ``` { assume asm: "a i \ 1" ``` hoelzl@36623 ` 112` ``` from asms have yai: "y i \ C" "a i \ 0" by auto ``` hoelzl@36623 ` 113` ``` have fis: "finite (insert i s)" using asms by auto ``` hoelzl@36623 ` 114` ``` hence ai1: "a i \ 1" using setsum_nonneg_leq_bound[of "insert i s" a 1] asms by simp ``` hoelzl@36623 ` 115` ``` hence "a i < 1" using asm by auto ``` hoelzl@36623 ` 116` ``` hence i0: "1 - a i > 0" by auto ``` hoelzl@36623 ` 117` ``` let "?a j" = "a j / (1 - a i)" ``` hoelzl@36623 ` 118` ``` { fix j assume "j \ s" ``` hoelzl@36623 ` 119` ``` hence "?a j \ 0" ``` hoelzl@36623 ` 120` ``` using i0 asms divide_nonneg_pos ``` hoelzl@36623 ` 121` ``` by fastsimp } note a_nonneg = this ``` hoelzl@36623 ` 122` ``` have "(\ j \ insert i s. a j) = 1" using asms by auto ``` hoelzl@36623 ` 123` ``` hence "(\ j \ s. a j) = 1 - a i" using setsum.insert asms by fastsimp ``` hoelzl@36623 ` 124` ``` hence "(\ j \ s. a j) / (1 - a i) = 1" using i0 by auto ``` hoelzl@36623 ` 125` ``` hence a1: "(\ j \ s. ?a j) = 1" unfolding divide.setsum by simp ``` hoelzl@36623 ` 126` ``` from this asms ``` hoelzl@36623 ` 127` ``` have "(\j\s. ?a j *\<^sub>R y j) \ C" using a_nonneg by fastsimp ``` hoelzl@36623 ` 128` ``` hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\ j \ s. ?a j *\<^sub>R y j) \ C" ``` hoelzl@36623 ` 129` ``` using asms[unfolded convex_def, rule_format] yai ai1 by auto ``` hoelzl@36623 ` 130` ``` hence "a i *\<^sub>R y i + (\ j \ s. (1 - a i) *\<^sub>R (?a j *\<^sub>R y j)) \ C" ``` hoelzl@36623 ` 131` ``` using scaleR_right.setsum[of "(1 - a i)" "\ j. ?a j *\<^sub>R y j" s] by auto ``` hoelzl@36623 ` 132` ``` hence "a i *\<^sub>R y i + (\ j \ s. a j *\<^sub>R y j) \ C" using i0 by auto ``` hoelzl@36623 ` 133` ``` hence ?case using setsum.insert asms by auto } ``` hoelzl@36623 ` 134` ``` ultimately show ?case by auto ``` hoelzl@36623 ` 135` ```qed ``` hoelzl@36623 ` 136` hoelzl@36623 ` 137` ```lemma convex: ``` hoelzl@36623 ` 138` ``` shows "convex s \ (\(k::nat) u x. (\i. 1\i \ i\k \ 0 \ u i \ x i \s) \ (setsum u {1..k} = 1) ``` hoelzl@36623 ` 139` ``` \ setsum (\i. u i *\<^sub>R x i) {1..k} \ s)" ``` hoelzl@36623 ` 140` ```proof safe ``` hoelzl@36623 ` 141` ``` fix k :: nat fix u :: "nat \ real" fix x ``` hoelzl@36623 ` 142` ``` assume "convex s" ``` hoelzl@36623 ` 143` ``` "\i. 1 \ i \ i \ k \ 0 \ u i \ x i \ s" ``` hoelzl@36623 ` 144` ``` "setsum u {1..k} = 1" ``` hoelzl@36623 ` 145` ``` from this convex_setsum[of "{1 .. k}" s] ``` hoelzl@36623 ` 146` ``` show "(\j\{1 .. k}. u j *\<^sub>R x j) \ s" by auto ``` hoelzl@36623 ` 147` ```next ``` hoelzl@36623 ` 148` ``` assume asm: "\k u x. (\ i :: nat. 1 \ i \ i \ k \ 0 \ u i \ x i \ s) \ setsum u {1..k} = 1 ``` hoelzl@36623 ` 149` ``` \ (\i = 1..k. u i *\<^sub>R (x i :: 'a)) \ s" ``` hoelzl@36623 ` 150` ``` { fix \ :: real fix x y :: 'a assume xy: "x \ s" "y \ s" assume mu: "\ \ 0" "\ \ 1" ``` hoelzl@36623 ` 151` ``` let "?u i" = "if (i :: nat) = 1 then \ else 1 - \" ``` hoelzl@36623 ` 152` ``` let "?x i" = "if (i :: nat) = 1 then x else y" ``` hoelzl@36623 ` 153` ``` have "{1 :: nat .. 2} \ - {x. x = 1} = {2}" by auto ``` hoelzl@36623 ` 154` ``` hence card: "card ({1 :: nat .. 2} \ - {x. x = 1}) = 1" by simp ``` hoelzl@36623 ` 155` ``` hence "setsum ?u {1 .. 2} = 1" ``` hoelzl@36623 ` 156` ``` using setsum_cases[of "{(1 :: nat) .. 2}" "\ x. x = 1" "\ x. \" "\ x. 1 - \"] ``` hoelzl@36623 ` 157` ``` by auto ``` hoelzl@36623 ` 158` ``` from this asm[rule_format, of "2" ?u ?x] ``` hoelzl@36623 ` 159` ``` have s: "(\j \ {1..2}. ?u j *\<^sub>R ?x j) \ s" ``` hoelzl@36623 ` 160` ``` using mu xy by auto ``` hoelzl@36623 ` 161` ``` have grarr: "(\j \ {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \) *\<^sub>R y" ``` hoelzl@36623 ` 162` ``` using setsum_head_Suc[of "Suc (Suc 0)" 2 "\ j. (1 - \) *\<^sub>R y"] by auto ``` hoelzl@36623 ` 163` ``` from setsum_head_Suc[of "Suc 0" 2 "\ j. ?u j *\<^sub>R ?x j", simplified this] ``` hoelzl@36623 ` 164` ``` have "(\j \ {1..2}. ?u j *\<^sub>R ?x j) = \ *\<^sub>R x + (1 - \) *\<^sub>R y" by auto ``` hoelzl@36623 ` 165` ``` hence "(1 - \) *\<^sub>R y + \ *\<^sub>R x \ s" using s by (auto simp:add_commute) } ``` hoelzl@36623 ` 166` ``` thus "convex s" unfolding convex_alt by auto ``` hoelzl@36623 ` 167` ```qed ``` hoelzl@36623 ` 168` hoelzl@36623 ` 169` hoelzl@36623 ` 170` ```lemma convex_explicit: ``` hoelzl@36623 ` 171` ``` fixes s :: "'a::real_vector set" ``` hoelzl@36623 ` 172` ``` shows "convex s \ ``` hoelzl@36623 ` 173` ``` (\t u. finite t \ t \ s \ (\x\t. 0 \ u x) \ setsum u t = 1 \ setsum (\x. u x *\<^sub>R x) t \ s)" ``` hoelzl@36623 ` 174` ```proof safe ``` hoelzl@36623 ` 175` ``` fix t fix u :: "'a \ real" ``` hoelzl@36623 ` 176` ``` assume "convex s" "finite t" ``` hoelzl@36623 ` 177` ``` "t \ s" "\x\t. 0 \ u x" "setsum u t = 1" ``` hoelzl@36623 ` 178` ``` thus "(\x\t. u x *\<^sub>R x) \ s" ``` hoelzl@36623 ` 179` ``` using convex_setsum[of t s u "\ x. x"] by auto ``` hoelzl@36623 ` 180` ```next ``` hoelzl@36623 ` 181` ``` assume asm0: "\t. \ u. finite t \ t \ s \ (\x\t. 0 \ u x) ``` hoelzl@36623 ` 182` ``` \ setsum u t = 1 \ (\x\t. u x *\<^sub>R x) \ s" ``` hoelzl@36623 ` 183` ``` show "convex s" ``` hoelzl@36623 ` 184` ``` unfolding convex_alt ``` hoelzl@36623 ` 185` ``` proof safe ``` hoelzl@36623 ` 186` ``` fix x y fix \ :: real ``` hoelzl@36623 ` 187` ``` assume asm: "x \ s" "y \ s" "0 \ \" "\ \ 1" ``` hoelzl@36623 ` 188` ``` { assume "x \ y" ``` hoelzl@36623 ` 189` ``` hence "(1 - \) *\<^sub>R x + \ *\<^sub>R y \ s" ``` hoelzl@36623 ` 190` ``` using asm0[rule_format, of "{x, y}" "\ z. if z = x then 1 - \ else \"] ``` hoelzl@36623 ` 191` ``` asm by auto } ``` hoelzl@36623 ` 192` ``` moreover ``` hoelzl@36623 ` 193` ``` { assume "x = y" ``` hoelzl@36623 ` 194` ``` hence "(1 - \) *\<^sub>R x + \ *\<^sub>R y \ s" ``` hoelzl@36623 ` 195` ``` using asm0[rule_format, of "{x, y}" "\ z. 1"] ``` hoelzl@36623 ` 196` ``` asm by (auto simp:field_simps real_vector.scale_left_diff_distrib) } ``` hoelzl@36623 ` 197` ``` ultimately show "(1 - \) *\<^sub>R x + \ *\<^sub>R y \ s" by blast ``` hoelzl@36623 ` 198` ``` qed ``` hoelzl@36623 ` 199` ```qed ``` hoelzl@36623 ` 200` hoelzl@36623 ` 201` ```lemma convex_finite: assumes "finite s" ``` hoelzl@36623 ` 202` ``` shows "convex s \ (\u. (\x\s. 0 \ u x) \ setsum u s = 1 ``` hoelzl@36623 ` 203` ``` \ setsum (\x. u x *\<^sub>R x) s \ s)" ``` hoelzl@36623 ` 204` ``` unfolding convex_explicit ``` hoelzl@36623 ` 205` ```proof (safe elim!: conjE) ``` hoelzl@36623 ` 206` ``` fix t u assume sum: "\u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) \ s" ``` hoelzl@36623 ` 207` ``` and as: "finite t" "t \ s" "\x\t. 0 \ u x" "setsum u t = (1::real)" ``` hoelzl@36623 ` 208` ``` have *:"s \ t = t" using as(2) by auto ``` hoelzl@36623 ` 209` ``` 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 ``` hoelzl@36623 ` 210` ``` show "(\x\t. u x *\<^sub>R x) \ s" ``` hoelzl@36623 ` 211` ``` using sum[THEN spec[where x="\x. if x\t then u x else 0"]] as * ``` hoelzl@36623 ` 212` ``` by (auto simp: assms setsum_cases if_distrib if_distrib_arg) ``` hoelzl@36623 ` 213` ```qed (erule_tac x=s in allE, erule_tac x=u in allE, auto) ``` hoelzl@36623 ` 214` hoelzl@36623 ` 215` ```definition ``` hoelzl@36623 ` 216` ``` convex_on :: "'a::real_vector set \ ('a \ real) \ bool" where ``` hoelzl@36623 ` 217` ``` "convex_on s f \ ``` hoelzl@36623 ` 218` ``` (\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)" ``` hoelzl@36623 ` 219` hoelzl@36623 ` 220` ```lemma convex_on_subset: "convex_on t f \ s \ t \ convex_on s f" ``` hoelzl@36623 ` 221` ``` unfolding convex_on_def by auto ``` hoelzl@36623 ` 222` hoelzl@36623 ` 223` ```lemma convex_add[intro]: ``` hoelzl@36623 ` 224` ``` assumes "convex_on s f" "convex_on s g" ``` hoelzl@36623 ` 225` ``` shows "convex_on s (\x. f x + g x)" ``` hoelzl@36623 ` 226` ```proof- ``` hoelzl@36623 ` 227` ``` { fix x y assume "x\s" "y\s" moreover ``` hoelzl@36623 ` 228` ``` fix u v ::real assume "0 \ u" "0 \ v" "u + v = 1" ``` hoelzl@36623 ` 229` ``` 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)" ``` hoelzl@36623 ` 230` ``` using assms unfolding convex_on_def by (auto simp add:add_mono) ``` hoelzl@36623 ` 231` ``` 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) } ``` hoelzl@36623 ` 232` ``` thus ?thesis unfolding convex_on_def by auto ``` hoelzl@36623 ` 233` ```qed ``` hoelzl@36623 ` 234` hoelzl@36623 ` 235` ```lemma convex_cmul[intro]: ``` hoelzl@36623 ` 236` ``` assumes "0 \ (c::real)" "convex_on s f" ``` hoelzl@36623 ` 237` ``` shows "convex_on s (\x. c * f x)" ``` hoelzl@36623 ` 238` ```proof- ``` hoelzl@36623 ` 239` ``` have *:"\u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps) ``` hoelzl@36623 ` 240` ``` show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto ``` hoelzl@36623 ` 241` ```qed ``` hoelzl@36623 ` 242` hoelzl@36623 ` 243` ```lemma convex_lower: ``` hoelzl@36623 ` 244` ``` assumes "convex_on s f" "x\s" "y \ s" "0 \ u" "0 \ v" "u + v = 1" ``` hoelzl@36623 ` 245` ``` shows "f (u *\<^sub>R x + v *\<^sub>R y) \ max (f x) (f y)" ``` hoelzl@36623 ` 246` ```proof- ``` hoelzl@36623 ` 247` ``` let ?m = "max (f x) (f y)" ``` hoelzl@36623 ` 248` ``` have "u * f x + v * f y \ u * max (f x) (f y) + v * max (f x) (f y)" ``` hoelzl@36623 ` 249` ``` using assms(4,5) by(auto simp add: mult_mono1 add_mono) ``` hoelzl@36623 ` 250` ``` also have "\ = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto ``` hoelzl@36623 ` 251` ``` finally show ?thesis ``` hoelzl@36623 ` 252` ``` using assms unfolding convex_on_def by fastsimp ``` hoelzl@36623 ` 253` ```qed ``` hoelzl@36623 ` 254` hoelzl@36623 ` 255` ```lemma convex_distance[intro]: ``` hoelzl@36623 ` 256` ``` fixes s :: "'a::real_normed_vector set" ``` hoelzl@36623 ` 257` ``` shows "convex_on s (\x. dist a x)" ``` hoelzl@36623 ` 258` ```proof(auto simp add: convex_on_def dist_norm) ``` hoelzl@36623 ` 259` ``` fix x y assume "x\s" "y\s" ``` hoelzl@36623 ` 260` ``` fix u v ::real assume "0 \ u" "0 \ v" "u + v = 1" ``` hoelzl@36623 ` 261` ``` have "a = u *\<^sub>R a + v *\<^sub>R a" unfolding scaleR_left_distrib[THEN sym] and `u+v=1` by simp ``` hoelzl@36623 ` 262` ``` hence *:"a - (u *\<^sub>R x + v *\<^sub>R y) = (u *\<^sub>R (a - x)) + (v *\<^sub>R (a - y))" ``` hoelzl@36623 ` 263` ``` by (auto simp add: algebra_simps) ``` hoelzl@36623 ` 264` ``` show "norm (a - (u *\<^sub>R x + v *\<^sub>R y)) \ u * norm (a - x) + v * norm (a - y)" ``` hoelzl@36623 ` 265` ``` unfolding * using norm_triangle_ineq[of "u *\<^sub>R (a - x)" "v *\<^sub>R (a - y)"] ``` hoelzl@36623 ` 266` ``` using `0 \ u` `0 \ v` by auto ``` hoelzl@36623 ` 267` ```qed ``` hoelzl@36623 ` 268` hoelzl@36623 ` 269` ```subsection {* Arithmetic operations on sets preserve convexity. *} ``` hoelzl@36623 ` 270` ```lemma convex_scaling: ``` hoelzl@36623 ` 271` ``` assumes "convex s" ``` hoelzl@36623 ` 272` ``` shows"convex ((\x. c *\<^sub>R x) ` s)" ``` hoelzl@36623 ` 273` ```using assms unfolding convex_def image_iff ``` hoelzl@36623 ` 274` ```proof safe ``` hoelzl@36623 ` 275` ``` fix x xa y xb :: "'a::real_vector" fix u v :: real ``` hoelzl@36623 ` 276` ``` assume asm: "\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" ``` hoelzl@36623 ` 277` ``` "xa \ s" "xb \ s" "0 \ u" "0 \ v" "u + v = 1" ``` hoelzl@36623 ` 278` ``` show "\x\s. u *\<^sub>R c *\<^sub>R xa + v *\<^sub>R c *\<^sub>R xb = c *\<^sub>R x" ``` hoelzl@36623 ` 279` ``` using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by (auto simp add: algebra_simps) ``` hoelzl@36623 ` 280` ```qed ``` hoelzl@36623 ` 281` hoelzl@36623 ` 282` ```lemma convex_negations: "convex s \ convex ((\x. -x)` s)" ``` hoelzl@36623 ` 283` ```using assms unfolding convex_def image_iff ``` hoelzl@36623 ` 284` ```proof safe ``` hoelzl@36623 ` 285` ``` fix x xa y xb :: "'a::real_vector" fix u v :: real ``` hoelzl@36623 ` 286` ``` assume asm: "\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" ``` hoelzl@36623 ` 287` ``` "xa \ s" "xb \ s" "0 \ u" "0 \ v" "u + v = 1" ``` hoelzl@36623 ` 288` ``` show "\x\s. u *\<^sub>R - xa + v *\<^sub>R - xb = - x" ``` hoelzl@36623 ` 289` ``` using bexI[of _ "u *\<^sub>R xa +v *\<^sub>R xb"] asm by auto ``` hoelzl@36623 ` 290` ```qed ``` hoelzl@36623 ` 291` hoelzl@36623 ` 292` ```lemma convex_sums: ``` hoelzl@36623 ` 293` ``` assumes "convex s" "convex t" ``` hoelzl@36623 ` 294` ``` shows "convex {x + y| x y. x \ s \ y \ t}" ``` hoelzl@36623 ` 295` ```using assms unfolding convex_def image_iff ``` hoelzl@36623 ` 296` ```proof safe ``` hoelzl@36623 ` 297` ``` fix xa xb ya yb assume xy:"xa\s" "xb\s" "ya\t" "yb\t" ``` hoelzl@36623 ` 298` ``` fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" ``` hoelzl@36623 ` 299` ``` show "\x y. u *\<^sub>R (xa + ya) + v *\<^sub>R (xb + yb) = x + y \ x \ s \ y \ t" ``` hoelzl@36623 ` 300` ``` using exI[of _ "u *\<^sub>R xa + v *\<^sub>R xb"] exI[of _ "u *\<^sub>R ya + v *\<^sub>R yb"] ``` hoelzl@36623 ` 301` ``` assms[unfolded convex_def] uv xy by (auto simp add:scaleR_right_distrib) ``` hoelzl@36623 ` 302` ```qed ``` hoelzl@36623 ` 303` hoelzl@36623 ` 304` ```lemma convex_differences: ``` hoelzl@36623 ` 305` ``` assumes "convex s" "convex t" ``` hoelzl@36623 ` 306` ``` shows "convex {x - y| x y. x \ s \ y \ t}" ``` hoelzl@36623 ` 307` ```proof - ``` hoelzl@36623 ` 308` ``` have "{x - y| x y. x \ s \ y \ t} = {x + y |x y. x \ s \ y \ uminus ` t}" ``` hoelzl@36623 ` 309` ``` proof safe ``` hoelzl@36623 ` 310` ``` fix x x' y assume "x' \ s" "y \ t" ``` hoelzl@36623 ` 311` ``` thus "\x y'. x' - y = x + y' \ x \ s \ y' \ uminus ` t" ``` hoelzl@36623 ` 312` ``` using exI[of _ x'] exI[of _ "-y"] by auto ``` hoelzl@36623 ` 313` ``` next ``` hoelzl@36623 ` 314` ``` fix x x' y y' assume "x' \ s" "y' \ t" ``` hoelzl@36623 ` 315` ``` thus "\x y. x' + - y' = x - y \ x \ s \ y \ t" ``` hoelzl@36623 ` 316` ``` using exI[of _ x'] exI[of _ y'] by auto ``` hoelzl@36623 ` 317` ``` qed ``` hoelzl@36623 ` 318` ``` thus ?thesis using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto ``` hoelzl@36623 ` 319` ```qed ``` hoelzl@36623 ` 320` hoelzl@36623 ` 321` ```lemma convex_translation: assumes "convex s" shows "convex ((\x. a + x) ` s)" ``` hoelzl@36623 ` 322` ```proof- have "{a + y |y. y \ s} = (\x. a + x) ` s" by auto ``` hoelzl@36623 ` 323` ``` thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed ``` hoelzl@36623 ` 324` hoelzl@36623 ` 325` ```lemma convex_affinity: assumes "convex s" shows "convex ((\x. a + c *\<^sub>R x) ` s)" ``` hoelzl@36623 ` 326` ```proof- have "(\x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto ``` hoelzl@36623 ` 327` ``` thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed ``` hoelzl@36623 ` 328` hoelzl@36623 ` 329` ```lemma convex_linear_image: ``` hoelzl@36623 ` 330` ``` assumes c:"convex s" and l:"bounded_linear f" ``` hoelzl@36623 ` 331` ``` shows "convex(f ` s)" ``` hoelzl@36623 ` 332` ```proof(auto simp add: convex_def) ``` hoelzl@36623 ` 333` ``` interpret f: bounded_linear f by fact ``` hoelzl@36623 ` 334` ``` fix x y assume xy:"x \ s" "y \ s" ``` hoelzl@36623 ` 335` ``` fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" ``` hoelzl@36623 ` 336` ``` show "u *\<^sub>R f x + v *\<^sub>R f y \ f ` s" unfolding image_iff ``` hoelzl@36623 ` 337` ``` using bexI[of _ "u *\<^sub>R x + v *\<^sub>R y"] f.add f.scaleR ``` hoelzl@36623 ` 338` ``` c[unfolded convex_def] xy uv by auto ``` hoelzl@36623 ` 339` ```qed ``` hoelzl@36623 ` 340` hoelzl@36623 ` 341` hoelzl@36623 ` 342` ```lemma pos_is_convex: ``` hoelzl@36623 ` 343` ``` shows "convex {0 :: real <..}" ``` hoelzl@36623 ` 344` ```unfolding convex_alt ``` hoelzl@36623 ` 345` ```proof safe ``` hoelzl@36623 ` 346` ``` fix y x \ :: real ``` hoelzl@36623 ` 347` ``` assume asms: "y > 0" "x > 0" "\ \ 0" "\ \ 1" ``` hoelzl@36623 ` 348` ``` { assume "\ = 0" ``` hoelzl@36623 ` 349` ``` hence "\ *\<^sub>R x + (1 - \) *\<^sub>R y = y" by simp ``` hoelzl@36623 ` 350` ``` hence "\ *\<^sub>R x + (1 - \) *\<^sub>R y > 0" using asms by simp } ``` hoelzl@36623 ` 351` ``` moreover ``` hoelzl@36623 ` 352` ``` { assume "\ = 1" ``` hoelzl@36623 ` 353` ``` hence "\ *\<^sub>R x + (1 - \) *\<^sub>R y > 0" using asms by simp } ``` hoelzl@36623 ` 354` ``` moreover ``` hoelzl@36623 ` 355` ``` { assume "\ \ 1" "\ \ 0" ``` hoelzl@36623 ` 356` ``` hence "\ > 0" "(1 - \) > 0" using asms by auto ``` hoelzl@36623 ` 357` ``` hence "\ *\<^sub>R x + (1 - \) *\<^sub>R y > 0" using asms ``` hoelzl@36623 ` 358` ``` using add_nonneg_pos[of "\ *\<^sub>R x" "(1 - \) *\<^sub>R y"] ``` hoelzl@36623 ` 359` ``` real_mult_order by auto fastsimp } ``` hoelzl@36623 ` 360` ``` ultimately show "(1 - \) *\<^sub>R y + \ *\<^sub>R x > 0" using assms by fastsimp ``` hoelzl@36623 ` 361` ```qed ``` hoelzl@36623 ` 362` hoelzl@36623 ` 363` ```lemma convex_on_setsum: ``` hoelzl@36623 ` 364` ``` fixes a :: "'a \ real" ``` hoelzl@36623 ` 365` ``` fixes y :: "'a \ 'b::real_vector" ``` hoelzl@36623 ` 366` ``` fixes f :: "'b \ real" ``` hoelzl@36623 ` 367` ``` assumes "finite s" "s \ {}" ``` hoelzl@36623 ` 368` ``` assumes "convex_on C f" ``` hoelzl@36623 ` 369` ``` assumes "convex C" ``` hoelzl@36623 ` 370` ``` assumes "(\ i \ s. a i) = 1" ``` hoelzl@36623 ` 371` ``` assumes "\ i. i \ s \ a i \ 0" ``` hoelzl@36623 ` 372` ``` assumes "\ i. i \ s \ y i \ C" ``` hoelzl@36623 ` 373` ``` shows "f (\ i \ s. a i *\<^sub>R y i) \ (\ i \ s. a i * f (y i))" ``` hoelzl@36623 ` 374` ```using assms ``` hoelzl@36623 ` 375` ```proof (induct s arbitrary:a rule:finite_ne_induct) ``` hoelzl@36623 ` 376` ``` case (singleton i) ``` hoelzl@36623 ` 377` ``` hence ai: "a i = 1" by auto ``` hoelzl@36623 ` 378` ``` thus ?case by auto ``` hoelzl@36623 ` 379` ```next ``` hoelzl@36623 ` 380` ``` case (insert i s) note asms = this ``` hoelzl@36623 ` 381` ``` hence "convex_on C f" by simp ``` hoelzl@36623 ` 382` ``` from this[unfolded convex_on_def, rule_format] ``` hoelzl@36623 ` 383` ``` have conv: "\ x y \. \x \ C; y \ C; 0 \ \; \ \ 1\ ``` hoelzl@36623 ` 384` ``` \ f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" ``` hoelzl@36623 ` 385` ``` by simp ``` hoelzl@36623 ` 386` ``` { assume "a i = 1" ``` hoelzl@36623 ` 387` ``` hence "(\ j \ s. a j) = 0" ``` hoelzl@36623 ` 388` ``` using asms by auto ``` hoelzl@36623 ` 389` ``` hence "\ j. j \ s \ a j = 0" ``` hoelzl@36623 ` 390` ``` using setsum_nonneg_0[where 'b=real] asms by fastsimp ``` hoelzl@36623 ` 391` ``` hence ?case using asms by auto } ``` hoelzl@36623 ` 392` ``` moreover ``` hoelzl@36623 ` 393` ``` { assume asm: "a i \ 1" ``` hoelzl@36623 ` 394` ``` from asms have yai: "y i \ C" "a i \ 0" by auto ``` hoelzl@36623 ` 395` ``` have fis: "finite (insert i s)" using asms by auto ``` hoelzl@36623 ` 396` ``` hence ai1: "a i \ 1" using setsum_nonneg_leq_bound[of "insert i s" a] asms by simp ``` hoelzl@36623 ` 397` ``` hence "a i < 1" using asm by auto ``` hoelzl@36623 ` 398` ``` hence i0: "1 - a i > 0" by auto ``` hoelzl@36623 ` 399` ``` let "?a j" = "a j / (1 - a i)" ``` hoelzl@36623 ` 400` ``` { fix j assume "j \ s" ``` hoelzl@36623 ` 401` ``` hence "?a j \ 0" ``` hoelzl@36623 ` 402` ``` using i0 asms divide_nonneg_pos ``` hoelzl@36623 ` 403` ``` by fastsimp } note a_nonneg = this ``` hoelzl@36623 ` 404` ``` have "(\ j \ insert i s. a j) = 1" using asms by auto ``` hoelzl@36623 ` 405` ``` hence "(\ j \ s. a j) = 1 - a i" using setsum.insert asms by fastsimp ``` hoelzl@36623 ` 406` ``` hence "(\ j \ s. a j) / (1 - a i) = 1" using i0 by auto ``` hoelzl@36623 ` 407` ``` hence a1: "(\ j \ s. ?a j) = 1" unfolding divide.setsum by simp ``` hoelzl@36623 ` 408` ``` have "convex C" using asms by auto ``` hoelzl@36623 ` 409` ``` hence asum: "(\ j \ s. ?a j *\<^sub>R y j) \ C" ``` hoelzl@36623 ` 410` ``` using asms convex_setsum[OF `finite s` ``` hoelzl@36623 ` 411` ``` `convex C` a1 a_nonneg] by auto ``` hoelzl@36623 ` 412` ``` have asum_le: "f (\ j \ s. ?a j *\<^sub>R y j) \ (\ j \ s. ?a j * f (y j))" ``` hoelzl@36623 ` 413` ``` using a_nonneg a1 asms by blast ``` hoelzl@36623 ` 414` ``` 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)" ``` hoelzl@36623 ` 415` ``` using setsum.insert[of s i "\ j. a j *\<^sub>R y j", OF `finite s` `i \ s`] asms ``` hoelzl@36623 ` 416` ``` by (auto simp only:add_commute) ``` hoelzl@36623 ` 417` ``` 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)" ``` hoelzl@36623 ` 418` ``` using i0 by auto ``` hoelzl@36623 ` 419` ``` 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)" ``` hoelzl@36623 ` 420` ``` using scaleR_right.setsum[of "inverse (1 - a i)" "\ j. a j *\<^sub>R y j" s, symmetric] by (auto simp:algebra_simps) ``` hoelzl@36623 ` 421` ``` also have "\ = f ((1 - a i) *\<^sub>R (\ j \ s. ?a j *\<^sub>R y j) + a i *\<^sub>R y i)" ``` hoelzl@36623 ` 422` ``` by (auto simp:real_divide_def) ``` hoelzl@36623 ` 423` ``` also have "\ \ (1 - a i) *\<^sub>R f ((\ j \ s. ?a j *\<^sub>R y j)) + a i * f (y i)" ``` hoelzl@36623 ` 424` ``` using conv[of "y i" "(\ j \ s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1] ``` hoelzl@36623 ` 425` ``` by (auto simp add:add_commute) ``` hoelzl@36623 ` 426` ``` also have "\ \ (1 - a i) * (\ j \ s. ?a j * f (y j)) + a i * f (y i)" ``` hoelzl@36623 ` 427` ``` using add_right_mono[OF mult_left_mono[of _ _ "1 - a i", ``` hoelzl@36623 ` 428` ``` OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp ``` hoelzl@36623 ` 429` ``` also have "\ = (\ j \ s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)" ``` hoelzl@36623 ` 430` ``` unfolding mult_right.setsum[of "1 - a i" "\ j. ?a j * f (y j)"] using i0 by auto ``` hoelzl@36623 ` 431` ``` also have "\ = (\ j \ s. a j * f (y j)) + a i * f (y i)" using i0 by auto ``` hoelzl@36623 ` 432` ``` also have "\ = (\ j \ insert i s. a j * f (y j))" using asms by auto ``` hoelzl@36623 ` 433` ``` finally have "f (\ j \ insert i s. a j *\<^sub>R y j) \ (\ j \ insert i s. a j * f (y j))" ``` hoelzl@36623 ` 434` ``` by simp } ``` hoelzl@36623 ` 435` ``` ultimately show ?case by auto ``` hoelzl@36623 ` 436` ```qed ``` hoelzl@36623 ` 437` hoelzl@36623 ` 438` ```lemma convex_on_alt: ``` hoelzl@36623 ` 439` ``` fixes C :: "'a::real_vector set" ``` hoelzl@36623 ` 440` ``` assumes "convex C" ``` hoelzl@36623 ` 441` ``` shows "convex_on C f = ``` hoelzl@36623 ` 442` ``` (\ x \ C. \ y \ C. \ \ :: real. \ \ 0 \ \ \ 1 ``` hoelzl@36623 ` 443` ``` \ f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y)" ``` hoelzl@36623 ` 444` ```proof safe ``` hoelzl@36623 ` 445` ``` fix x y fix \ :: real ``` hoelzl@36623 ` 446` ``` assume asms: "convex_on C f" "x \ C" "y \ C" "0 \ \" "\ \ 1" ``` hoelzl@36623 ` 447` ``` from this[unfolded convex_on_def, rule_format] ``` hoelzl@36623 ` 448` ``` 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 ``` hoelzl@36623 ` 449` ``` from this[of "\" "1 - \", simplified] asms ``` hoelzl@36623 ` 450` ``` show "f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) ``` hoelzl@36623 ` 451` ``` \ \ * f x + (1 - \) * f y" by auto ``` hoelzl@36623 ` 452` ```next ``` hoelzl@36623 ` 453` ``` assume asm: "\x\C. \y\C. \\. 0 \ \ \ \ \ 1 \ f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" ``` hoelzl@36623 ` 454` ``` {fix x y fix u v :: real ``` hoelzl@36623 ` 455` ``` assume lasm: "x \ C" "y \ C" "u \ 0" "v \ 0" "u + v = 1" ``` hoelzl@36623 ` 456` ``` hence[simp]: "1 - u = v" by auto ``` hoelzl@36623 ` 457` ``` from asm[rule_format, of x y u] ``` hoelzl@36623 ` 458` ``` have "f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y" using lasm by auto } ``` hoelzl@36623 ` 459` ``` thus "convex_on C f" unfolding convex_on_def by auto ``` hoelzl@36623 ` 460` ```qed ``` hoelzl@36623 ` 461` hoelzl@36623 ` 462` hoelzl@36623 ` 463` ```lemma pos_convex_function: ``` hoelzl@36623 ` 464` ``` fixes f :: "real \ real" ``` hoelzl@36623 ` 465` ``` assumes "convex C" ``` hoelzl@36623 ` 466` ``` assumes leq: "\ x y. \x \ C ; y \ C\ \ f' x * (y - x) \ f y - f x" ``` hoelzl@36623 ` 467` ``` shows "convex_on C f" ``` hoelzl@36623 ` 468` ```unfolding convex_on_alt[OF assms(1)] ``` hoelzl@36623 ` 469` ```using assms ``` hoelzl@36623 ` 470` ```proof safe ``` hoelzl@36623 ` 471` ``` fix x y \ :: real ``` hoelzl@36623 ` 472` ``` let ?x = "\ *\<^sub>R x + (1 - \) *\<^sub>R y" ``` hoelzl@36623 ` 473` ``` assume asm: "convex C" "x \ C" "y \ C" "\ \ 0" "\ \ 1" ``` hoelzl@36623 ` 474` ``` hence "1 - \ \ 0" by auto ``` hoelzl@36623 ` 475` ``` hence xpos: "?x \ C" using asm unfolding convex_alt by fastsimp ``` hoelzl@36623 ` 476` ``` have geq: "\ * (f x - f ?x) + (1 - \) * (f y - f ?x) ``` hoelzl@36623 ` 477` ``` \ \ * f' ?x * (x - ?x) + (1 - \) * f' ?x * (y - ?x)" ``` hoelzl@36623 ` 478` ``` using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\ \ 0`] ``` hoelzl@36623 ` 479` ``` mult_mono1[OF leq[OF xpos asm(3)] `1 - \ \ 0`]] by auto ``` hoelzl@36623 ` 480` ``` hence "\ * f x + (1 - \) * f y - f ?x \ 0" ``` hoelzl@36623 ` 481` ``` by (auto simp add:field_simps) ``` hoelzl@36623 ` 482` ``` thus "f (\ *\<^sub>R x + (1 - \) *\<^sub>R y) \ \ * f x + (1 - \) * f y" ``` hoelzl@36623 ` 483` ``` using convex_on_alt by auto ``` hoelzl@36623 ` 484` ```qed ``` hoelzl@36623 ` 485` hoelzl@36623 ` 486` ```lemma atMostAtLeast_subset_convex: ``` hoelzl@36623 ` 487` ``` fixes C :: "real set" ``` hoelzl@36623 ` 488` ``` assumes "convex C" ``` hoelzl@36623 ` 489` ``` assumes "x \ C" "y \ C" "x < y" ``` hoelzl@36623 ` 490` ``` shows "{x .. y} \ C" ``` hoelzl@36623 ` 491` ```proof safe ``` hoelzl@36623 ` 492` ``` fix z assume zasm: "z \ {x .. y}" ``` hoelzl@36623 ` 493` ``` { assume asm: "x < z" "z < y" ``` hoelzl@36623 ` 494` ``` let "?\" = "(y - z) / (y - x)" ``` hoelzl@36623 ` 495` ``` have "0 \ ?\" "?\ \ 1" using assms asm by (auto simp add:field_simps) ``` hoelzl@36623 ` 496` ``` hence comb: "?\ * x + (1 - ?\) * y \ C" ``` hoelzl@36623 ` 497` ``` using assms iffD1[OF convex_alt, rule_format, of C y x ?\] by (simp add:algebra_simps) ``` hoelzl@36623 ` 498` ``` have "?\ * x + (1 - ?\) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y" ``` hoelzl@36623 ` 499` ``` by (auto simp add:field_simps) ``` hoelzl@36623 ` 500` ``` also have "\ = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)" ``` hoelzl@36623 ` 501` ``` using assms unfolding add_divide_distrib by (auto simp:field_simps) ``` hoelzl@36623 ` 502` ``` also have "\ = z" ``` hoelzl@36623 ` 503` ``` using assms by (auto simp:field_simps) ``` hoelzl@36623 ` 504` ``` finally have "z \ C" ``` hoelzl@36623 ` 505` ``` using comb by auto } note less = this ``` hoelzl@36623 ` 506` ``` show "z \ C" using zasm less assms ``` hoelzl@36623 ` 507` ``` unfolding atLeastAtMost_iff le_less by auto ``` hoelzl@36623 ` 508` ```qed ``` hoelzl@36623 ` 509` hoelzl@36623 ` 510` ```lemma f''_imp_f': ``` hoelzl@36623 ` 511` ``` fixes f :: "real \ real" ``` hoelzl@36623 ` 512` ``` assumes "convex C" ``` hoelzl@36623 ` 513` ``` assumes f': "\ x. x \ C \ DERIV f x :> (f' x)" ``` hoelzl@36623 ` 514` ``` assumes f'': "\ x. x \ C \ DERIV f' x :> (f'' x)" ``` hoelzl@36623 ` 515` ``` assumes pos: "\ x. x \ C \ f'' x \ 0" ``` hoelzl@36623 ` 516` ``` assumes "x \ C" "y \ C" ``` hoelzl@36623 ` 517` ``` shows "f' x * (y - x) \ f y - f x" ``` hoelzl@36623 ` 518` ```using assms ``` hoelzl@36623 ` 519` ```proof - ``` hoelzl@36623 ` 520` ``` { fix x y :: real assume asm: "x \ C" "y \ C" "y > x" ``` hoelzl@36623 ` 521` ``` hence ge: "y - x > 0" "y - x \ 0" by auto ``` hoelzl@36623 ` 522` ``` from asm have le: "x - y < 0" "x - y \ 0" by auto ``` hoelzl@36623 ` 523` ``` then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1" ``` hoelzl@36623 ` 524` ``` using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `x \ C` `y \ C` `x < y`], ``` hoelzl@36623 ` 525` ``` THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] ``` hoelzl@36623 ` 526` ``` by auto ``` hoelzl@36623 ` 527` ``` hence "z1 \ C" using atMostAtLeast_subset_convex ``` hoelzl@36623 ` 528` ``` `convex C` `x \ C` `y \ C` `x < y` by fastsimp ``` hoelzl@36623 ` 529` ``` from z1 have z1': "f x - f y = (x - y) * f' z1" ``` hoelzl@36623 ` 530` ``` by (simp add:field_simps) ``` hoelzl@36623 ` 531` ``` obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2" ``` hoelzl@36623 ` 532` ``` using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `x \ C` `z1 \ C` `x < z1`], ``` hoelzl@36623 ` 533` ``` THEN f'', THEN MVT2[OF `x < z1`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 ``` hoelzl@36623 ` 534` ``` by auto ``` hoelzl@36623 ` 535` ``` obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3" ``` hoelzl@36623 ` 536` ``` using subsetD[OF atMostAtLeast_subset_convex[OF `convex C` `z1 \ C` `y \ C` `z1 < y`], ``` hoelzl@36623 ` 537` ``` THEN f'', THEN MVT2[OF `z1 < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 ``` hoelzl@36623 ` 538` ``` by auto ``` hoelzl@36623 ` 539` ``` have "f' y - (f x - f y) / (x - y) = f' y - f' z1" ``` hoelzl@36623 ` 540` ``` using asm z1' by auto ``` hoelzl@36623 ` 541` ``` also have "\ = (y - z1) * f'' z3" using z3 by auto ``` hoelzl@36623 ` 542` ``` finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp ``` hoelzl@36623 ` 543` ``` have A': "y - z1 \ 0" using z1 by auto ``` hoelzl@36623 ` 544` ``` have "z3 \ C" using z3 asm atMostAtLeast_subset_convex ``` hoelzl@36623 ` 545` ``` `convex C` `x \ C` `z1 \ C` `x < z1` by fastsimp ``` hoelzl@36623 ` 546` ``` hence B': "f'' z3 \ 0" using assms by auto ``` hoelzl@36623 ` 547` ``` from A' B' have "(y - z1) * f'' z3 \ 0" using mult_nonneg_nonneg by auto ``` hoelzl@36623 ` 548` ``` from cool' this have "f' y - (f x - f y) / (x - y) \ 0" by auto ``` hoelzl@36623 ` 549` ``` from mult_right_mono_neg[OF this le(2)] ``` hoelzl@36623 ` 550` ``` have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \ 0 * (x - y)" ``` hoelzl@36623 ` 551` ``` unfolding diff_def using real_add_mult_distrib by auto ``` hoelzl@36623 ` 552` ``` hence "f' y * (x - y) - (f x - f y) \ 0" using le by auto ``` hoelzl@36623 ` 553` ``` hence res: "f' y * (x - y) \ f x - f y" by auto ``` hoelzl@36623 ` 554` ``` have "(f y - f x) / (y - x) - f' x = f' z1 - f' x" ``` hoelzl@36623 ` 555` ``` using asm z1 by auto ``` hoelzl@36623 ` 556` ``` also have "\ = (z1 - x) * f'' z2" using z2 by auto ``` hoelzl@36623 ` 557` ``` finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp ``` hoelzl@36623 ` 558` ``` have A: "z1 - x \ 0" using z1 by auto ``` hoelzl@36623 ` 559` ``` have "z2 \ C" using z2 z1 asm atMostAtLeast_subset_convex ``` hoelzl@36623 ` 560` ``` `convex C` `z1 \ C` `y \ C` `z1 < y` by fastsimp ``` hoelzl@36623 ` 561` ``` hence B: "f'' z2 \ 0" using assms by auto ``` hoelzl@36623 ` 562` ``` from A B have "(z1 - x) * f'' z2 \ 0" using mult_nonneg_nonneg by auto ``` hoelzl@36623 ` 563` ``` from cool this have "(f y - f x) / (y - x) - f' x \ 0" by auto ``` hoelzl@36623 ` 564` ``` from mult_right_mono[OF this ge(2)] ``` hoelzl@36623 ` 565` ``` have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \ 0 * (y - x)" ``` hoelzl@36623 ` 566` ``` unfolding diff_def using real_add_mult_distrib by auto ``` hoelzl@36623 ` 567` ``` hence "f y - f x - f' x * (y - x) \ 0" using ge by auto ``` hoelzl@36623 ` 568` ``` hence "f y - f x \ f' x * (y - x)" "f' y * (x - y) \ f x - f y" ``` hoelzl@36623 ` 569` ``` using res by auto } note less_imp = this ``` hoelzl@36623 ` 570` ``` { fix x y :: real assume "x \ C" "y \ C" "x \ y" ``` hoelzl@36623 ` 571` ``` hence"f y - f x \ f' x * (y - x)" ``` hoelzl@36623 ` 572` ``` unfolding neq_iff using less_imp by auto } note neq_imp = this ``` hoelzl@36623 ` 573` ``` moreover ``` hoelzl@36623 ` 574` ``` { fix x y :: real assume asm: "x \ C" "y \ C" "x = y" ``` hoelzl@36623 ` 575` ``` hence "f y - f x \ f' x * (y - x)" by auto } ``` hoelzl@36623 ` 576` ``` ultimately show ?thesis using assms by blast ``` hoelzl@36623 ` 577` ```qed ``` hoelzl@36623 ` 578` hoelzl@36623 ` 579` ```lemma f''_ge0_imp_convex: ``` hoelzl@36623 ` 580` ``` fixes f :: "real \ real" ``` hoelzl@36623 ` 581` ``` assumes conv: "convex C" ``` hoelzl@36623 ` 582` ``` assumes f': "\ x. x \ C \ DERIV f x :> (f' x)" ``` hoelzl@36623 ` 583` ``` assumes f'': "\ x. x \ C \ DERIV f' x :> (f'' x)" ``` hoelzl@36623 ` 584` ``` assumes pos: "\ x. x \ C \ f'' x \ 0" ``` hoelzl@36623 ` 585` ``` shows "convex_on C f" ``` hoelzl@36623 ` 586` ```using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp ``` hoelzl@36623 ` 587` hoelzl@36623 ` 588` ```lemma minus_log_convex: ``` hoelzl@36623 ` 589` ``` fixes b :: real ``` hoelzl@36623 ` 590` ``` assumes "b > 1" ``` hoelzl@36623 ` 591` ``` shows "convex_on {0 <..} (\ x. - log b x)" ``` hoelzl@36623 ` 592` ```proof - ``` hoelzl@36623 ` 593` ``` have "\ z. z > 0 \ DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto ``` hoelzl@36623 ` 594` ``` hence f': "\ z. z > 0 \ DERIV (\ z. - log b z) z :> - 1 / (ln b * z)" ``` hoelzl@36623 ` 595` ``` using DERIV_minus by auto ``` hoelzl@36623 ` 596` ``` have "\ z :: real. z > 0 \ DERIV inverse z :> - (inverse z ^ Suc (Suc 0))" ``` hoelzl@36623 ` 597` ``` using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto ``` hoelzl@36623 ` 598` ``` from this[THEN DERIV_cmult, of _ "- 1 / ln b"] ``` hoelzl@36623 ` 599` ``` have "\ z :: real. z > 0 \ DERIV (\ z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))" ``` hoelzl@36623 ` 600` ``` by auto ``` hoelzl@36623 ` 601` ``` hence f''0: "\ z :: real. z > 0 \ DERIV (\ z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)" ``` hoelzl@36623 ` 602` ``` unfolding inverse_eq_divide by (auto simp add:real_mult_assoc) ``` hoelzl@36623 ` 603` ``` have f''_ge0: "\ z :: real. z > 0 \ 1 / (ln b * z * z) \ 0" ``` hoelzl@36623 ` 604` ``` using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order) ``` hoelzl@36623 ` 605` ``` from f''_ge0_imp_convex[OF pos_is_convex, ``` hoelzl@36623 ` 606` ``` unfolded greaterThan_iff, OF f' f''0 f''_ge0] ``` hoelzl@36623 ` 607` ``` show ?thesis by auto ``` hoelzl@36623 ` 608` ```qed ``` hoelzl@36623 ` 609` hoelzl@36623 ` 610` ```end ```