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