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