(* Title: HOL/Analysis/Convex_Euclidean_Space.thy Author: L C Paulson, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Bogdan Grechuk, University of Edinburgh Author: Armin Heller, TU Muenchen Author: Johannes Hoelzl, TU Muenchen *) section ‹Convex sets, functions and related things› theory Convex_Euclidean_Space imports Connected "HOL-Library.Set_Algebras" begin lemma swap_continuous: (*move to Topological_Spaces?*) assumes "continuous_on (cbox (a,c) (b,d)) (λ(x,y). f x y)" shows "continuous_on (cbox (c,a) (d,b)) (λ(x, y). f y x)" proof - have "(λ(x, y). f y x) = (λ(x, y). f x y) ∘ prod.swap" by auto then show ?thesis apply (rule ssubst) apply (rule continuous_on_compose) apply (simp add: split_def) apply (rule continuous_intros | simp add: assms)+ done qed lemma substdbasis_expansion_unique: assumes d: "d ⊆ Basis" shows "(∑i∈d. f i *⇩_{R}i) = (x::'a::euclidean_space) ⟷ (∀i∈Basis. (i ∈ d ⟶ f i = x ∙ i) ∧ (i ∉ d ⟶ x ∙ i = 0))" proof - have *: "⋀x a b P. x * (if P then a else b) = (if P then x * a else x * b)" by auto have **: "finite d" by (auto intro: finite_subset[OF assms]) have ***: "⋀i. i ∈ Basis ⟹ (∑i∈d. f i *⇩_{R}i) ∙ i = (∑x∈d. if x = i then f x else 0)" using d by (auto intro!: sum.cong simp: inner_Basis inner_sum_left) show ?thesis unfolding euclidean_eq_iff[where 'a='a] by (auto simp: sum.delta[OF **] ***) qed lemma independent_substdbasis: "d ⊆ Basis ⟹ independent d" by (rule independent_mono[OF independent_Basis]) lemma dim_cball: assumes "e > 0" shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)" proof - { fix x :: "'n::euclidean_space" define y where "y = (e / norm x) *⇩_{R}x" then have "y ∈ cball 0 e" using assms by auto moreover have *: "x = (norm x / e) *⇩_{R}y" using y_def assms by simp moreover from * have "x = (norm x/e) *⇩_{R}y" by auto ultimately have "x ∈ span (cball 0 e)" using span_scale[of y "cball 0 e" "norm x/e"] span_superset[of "cball 0 e"] by (simp add: span_base) } then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)" by auto then show ?thesis using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp: dim_UNIV) qed lemma sum_not_0: "sum f A ≠ 0 ⟹ ∃a ∈ A. f a ≠ 0" by (rule ccontr) auto lemma subset_translation_eq [simp]: fixes a :: "'a::real_vector" shows "(+) a ` s ⊆ (+) a ` t ⟷ s ⊆ t" by auto lemma translate_inj_on: fixes A :: "'a::ab_group_add set" shows "inj_on (λx. a + x) A" unfolding inj_on_def by auto lemma translation_assoc: fixes a b :: "'a::ab_group_add" shows "(λx. b + x) ` ((λx. a + x) ` S) = (λx. (a + b) + x) ` S" by auto lemma translation_invert: fixes a :: "'a::ab_group_add" assumes "(λx. a + x) ` A = (λx. a + x) ` B" shows "A = B" proof - have "(λx. -a + x) ` ((λx. a + x) ` A) = (λx. - a + x) ` ((λx. a + x) ` B)" using assms by auto then show ?thesis using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto qed lemma translation_galois: fixes a :: "'a::ab_group_add" shows "T = ((λx. a + x) ` S) ⟷ S = ((λx. (- a) + x) ` T)" using translation_assoc[of "-a" a S] apply auto using translation_assoc[of a "-a" T] apply auto done lemma translation_inverse_subset: assumes "((λx. - a + x) ` V) ≤ (S :: 'n::ab_group_add set)" shows "V ≤ ((λx. a + x) ` S)" proof - { fix x assume "x ∈ V" then have "x-a ∈ S" using assms by auto then have "x ∈ {a + v |v. v ∈ S}" apply auto apply (rule exI[of _ "x-a"], simp) done then have "x ∈ ((λx. a+x) ` S)" by auto } then show ?thesis by auto qed subsection ‹Convexity› definition%important convex :: "'a::real_vector set ⇒ bool" where "convex s ⟷ (∀x∈s. ∀y∈s. ∀u≥0. ∀v≥0. u + v = 1 ⟶ u *⇩_{R}x + v *⇩_{R}y ∈ s)" lemma convexI: assumes "⋀x y u v. x ∈ s ⟹ y ∈ s ⟹ 0 ≤ u ⟹ 0 ≤ v ⟹ u + v = 1 ⟹ u *⇩_{R}x + v *⇩_{R}y ∈ s" shows "convex s" using assms unfolding convex_def by fast lemma convexD: assumes "convex s" and "x ∈ s" and "y ∈ s" and "0 ≤ u" and "0 ≤ v" and "u + v = 1" shows "u *⇩_{R}x + v *⇩_{R}y ∈ s" using assms unfolding convex_def by fast lemma convex_alt: "convex s ⟷ (∀x∈s. ∀y∈s. ∀u. 0 ≤ u ∧ u ≤ 1 ⟶ ((1 - u) *⇩_{R}x + u *⇩_{R}y) ∈ s)" (is "_ ⟷ ?alt") proof show "convex s" if alt: ?alt proof - { fix x y and u v :: real assume mem: "x ∈ s" "y ∈ s" assume "0 ≤ u" "0 ≤ v" moreover assume "u + v = 1" then have "u = 1 - v" by auto ultimately have "u *⇩_{R}x + v *⇩_{R}y ∈ s" using alt [rule_format, OF mem] by auto } then show ?thesis unfolding convex_def by auto qed show ?alt if "convex s" using that by (auto simp: convex_def) qed lemma convexD_alt: assumes "convex s" "a ∈ s" "b ∈ s" "0 ≤ u" "u ≤ 1" shows "((1 - u) *⇩_{R}a + u *⇩_{R}b) ∈ s" using assms unfolding convex_alt by auto lemma mem_convex_alt: assumes "convex S" "x ∈ S" "y ∈ S" "u ≥ 0" "v ≥ 0" "u + v > 0" shows "((u/(u+v)) *⇩_{R}x + (v/(u+v)) *⇩_{R}y) ∈ S" apply (rule convexD) using assms apply (simp_all add: zero_le_divide_iff add_divide_distrib [symmetric]) done lemma convex_empty[intro,simp]: "convex {}" unfolding convex_def by simp lemma convex_singleton[intro,simp]: "convex {a}" unfolding convex_def by (auto simp: scaleR_left_distrib[symmetric]) lemma convex_UNIV[intro,simp]: "convex UNIV" unfolding convex_def by auto lemma convex_Inter: "(⋀s. s∈f ⟹ convex s) ⟹ convex(⋂f)" unfolding convex_def by auto lemma convex_Int: "convex s ⟹ convex t ⟹ convex (s ∩ t)" unfolding convex_def by auto lemma convex_INT: "(⋀i. i ∈ A ⟹ convex (B i)) ⟹ convex (⋂i∈A. B i)" unfolding convex_def by auto lemma convex_Times: "convex s ⟹ convex t ⟹ convex (s × t)" unfolding convex_def by auto lemma convex_halfspace_le: "convex {x. inner a x ≤ b}" unfolding convex_def by (auto simp: inner_add intro!: convex_bound_le) lemma convex_halfspace_ge: "convex {x. inner a x ≥ b}" proof - have *: "{x. inner a x ≥ b} = {x. inner (-a) x ≤ -b}" by auto show ?thesis unfolding * using convex_halfspace_le[of "-a" "-b"] by auto qed lemma convex_halfspace_abs_le: "convex {x. ¦inner a x¦ ≤ b}" proof - have *: "{x. ¦inner a x¦ ≤ b} = {x. inner a x ≤ b} ∩ {x. -b ≤ inner a x}" by auto show ?thesis unfolding * by (simp add: convex_Int convex_halfspace_ge convex_halfspace_le) qed lemma convex_hyperplane: "convex {x. inner a x = b}" proof - have *: "{x. inner a x = b} = {x. inner a x ≤ b} ∩ {x. inner a x ≥ b}" by auto show ?thesis using convex_halfspace_le convex_halfspace_ge by (auto intro!: convex_Int simp: *) qed lemma convex_halfspace_lt: "convex {x. inner a x < b}" unfolding convex_def by (auto simp: convex_bound_lt inner_add) lemma convex_halfspace_gt: "convex {x. inner a x > b}" using convex_halfspace_lt[of "-a" "-b"] by auto lemma convex_halfspace_Re_ge: "convex {x. Re x ≥ b}" using convex_halfspace_ge[of b "1::complex"] by simp lemma convex_halfspace_Re_le: "convex {x. Re x ≤ b}" using convex_halfspace_le[of "1::complex" b] by simp lemma convex_halfspace_Im_ge: "convex {x. Im x ≥ b}" using convex_halfspace_ge[of b 𝗂] by simp lemma convex_halfspace_Im_le: "convex {x. Im x ≤ b}" using convex_halfspace_le[of 𝗂 b] by simp lemma convex_halfspace_Re_gt: "convex {x. Re x > b}" using convex_halfspace_gt[of b "1::complex"] by simp lemma convex_halfspace_Re_lt: "convex {x. Re x < b}" using convex_halfspace_lt[of "1::complex" b] by simp lemma convex_halfspace_Im_gt: "convex {x. Im x > b}" using convex_halfspace_gt[of b 𝗂] by simp lemma convex_halfspace_Im_lt: "convex {x. Im x < b}" using convex_halfspace_lt[of 𝗂 b] by simp lemma convex_real_interval [iff]: fixes a b :: "real" shows "convex {a..}" and "convex {..b}" and "convex {a<..}" and "convex {..<b}" and "convex {a..b}" and "convex {a<..b}" and "convex {a..<b}" and "convex {a<..<b}" proof - have "{a..} = {x. a ≤ inner 1 x}" by auto then show 1: "convex {a..}" by (simp only: convex_halfspace_ge) have "{..b} = {x. inner 1 x ≤ b}" by auto then show 2: "convex {..b}" by (simp only: convex_halfspace_le) have "{a<..} = {x. a < inner 1 x}" by auto then show 3: "convex {a<..}" by (simp only: convex_halfspace_gt) have "{..<b} = {x. inner 1 x < b}" by auto then show 4: "convex {..<b}" by (simp only: convex_halfspace_lt) have "{a..b} = {a..} ∩ {..b}" by auto then show "convex {a..b}" by (simp only: convex_Int 1 2) have "{a<..b} = {a<..} ∩ {..b}" by auto then show "convex {a<..b}" by (simp only: convex_Int 3 2) have "{a..<b} = {a..} ∩ {..<b}" by auto then show "convex {a..<b}" by (simp only: convex_Int 1 4) have "{a<..<b} = {a<..} ∩ {..<b}" by auto then show "convex {a<..<b}" by (simp only: convex_Int 3 4) qed lemma convex_Reals: "convex ℝ" by (simp add: convex_def scaleR_conv_of_real) subsection%unimportant ‹Explicit expressions for convexity in terms of arbitrary sums› lemma convex_sum: fixes C :: "'a::real_vector set" assumes "finite s" and "convex C" and "(∑ i ∈ s. a i) = 1" assumes "⋀i. i ∈ s ⟹ a i ≥ 0" and "⋀i. i ∈ s ⟹ y i ∈ C" shows "(∑ j ∈ s. a j *⇩_{R}y j) ∈ C" using assms(1,3,4,5) proof (induct arbitrary: a set: finite) case empty then show ?case by simp next case (insert i s) note IH = this(3) have "a i + sum a s = 1" and "0 ≤ a i" and "∀j∈s. 0 ≤ a j" and "y i ∈ C" and "∀j∈s. y j ∈ C" using insert.hyps(1,2) insert.prems by simp_all then have "0 ≤ sum a s" by (simp add: sum_nonneg) have "a i *⇩_{R}y i + (∑j∈s. a j *⇩_{R}y j) ∈ C" proof (cases "sum a s = 0") case True with ‹a i + sum a s = 1› have "a i = 1" by simp from sum_nonneg_0 [OF ‹finite s› _ True] ‹∀j∈s. 0 ≤ a j› have "∀j∈s. a j = 0" by simp show ?thesis using ‹a i = 1› and ‹∀j∈s. a j = 0› and ‹y i ∈ C› by simp next case False with ‹0 ≤ sum a s› have "0 < sum a s" by simp then have "(∑j∈s. (a j / sum a s) *⇩_{R}y j) ∈ C" using ‹∀j∈s. 0 ≤ a j› and ‹∀j∈s. y j ∈ C› by (simp add: IH sum_divide_distrib [symmetric]) from ‹convex C› and ‹y i ∈ C› and this and ‹0 ≤ a i› and ‹0 ≤ sum a s› and ‹a i + sum a s = 1› have "a i *⇩_{R}y i + sum a s *⇩_{R}(∑j∈s. (a j / sum a s) *⇩_{R}y j) ∈ C" by (rule convexD) then show ?thesis by (simp add: scaleR_sum_right False) qed then show ?case using ‹finite s› and ‹i ∉ s› by simp qed lemma convex: "convex s ⟷ (∀(k::nat) u x. (∀i. 1≤i ∧ i≤k ⟶ 0 ≤ u i ∧ x i ∈s) ∧ (sum u {1..k} = 1) ⟶ sum (λi. u i *⇩_{R}x i) {1..k} ∈ s)" proof safe fix k :: nat fix u :: "nat ⇒ real" fix x assume "convex s" "∀i. 1 ≤ i ∧ i ≤ k ⟶ 0 ≤ u i ∧ x i ∈ s" "sum u {1..k} = 1" with convex_sum[of "{1 .. k}" s] show "(∑j∈{1 .. k}. u j *⇩_{R}x j) ∈ s" by auto next assume *: "∀k u x. (∀ i :: nat. 1 ≤ i ∧ i ≤ k ⟶ 0 ≤ u i ∧ x i ∈ s) ∧ sum u {1..k} = 1 ⟶ (∑i = 1..k. u i *⇩_{R}(x i :: 'a)) ∈ s" { fix μ :: real fix x y :: 'a assume xy: "x ∈ s" "y ∈ s" assume mu: "μ ≥ 0" "μ ≤ 1" let ?u = "λi. if (i :: nat) = 1 then μ else 1 - μ" let ?x = "λi. if (i :: nat) = 1 then x else y" have "{1 :: nat .. 2} ∩ - {x. x = 1} = {2}" by auto then have card: "card ({1 :: nat .. 2} ∩ - {x. x = 1}) = 1" by simp then have "sum ?u {1 .. 2} = 1" using sum.If_cases[of "{(1 :: nat) .. 2}" "λ x. x = 1" "λ x. μ" "λ x. 1 - μ"] by auto with *[rule_format, of "2" ?u ?x] have s: "(∑j ∈ {1..2}. ?u j *⇩_{R}?x j) ∈ s" using mu xy by auto have grarr: "(∑j ∈ {Suc (Suc 0)..2}. ?u j *⇩_{R}?x j) = (1 - μ) *⇩_{R}y" using sum_head_Suc[of "Suc (Suc 0)" 2 "λ j. (1 - μ) *⇩_{R}y"] by auto from sum_head_Suc[of "Suc 0" 2 "λ j. ?u j *⇩_{R}?x j", simplified this] have "(∑j ∈ {1..2}. ?u j *⇩_{R}?x j) = μ *⇩_{R}x + (1 - μ) *⇩_{R}y" by auto then have "(1 - μ) *⇩_{R}y + μ *⇩_{R}x ∈ s" using s by (auto simp: add.commute) } then show "convex s" unfolding convex_alt by auto qed lemma convex_explicit: fixes s :: "'a::real_vector set" shows "convex s ⟷ (∀t u. finite t ∧ t ⊆ s ∧ (∀x∈t. 0 ≤ u x) ∧ sum u t = 1 ⟶ sum (λx. u x *⇩_{R}x) t ∈ s)" proof safe fix t fix u :: "'a ⇒ real" assume "convex s" and "finite t" and "t ⊆ s" "∀x∈t. 0 ≤ u x" "sum u t = 1" then show "(∑x∈t. u x *⇩_{R}x) ∈ s" using convex_sum[of t s u "λ x. x"] by auto next assume *: "∀t. ∀ u. finite t ∧ t ⊆ s ∧ (∀x∈t. 0 ≤ u x) ∧ sum u t = 1 ⟶ (∑x∈t. u x *⇩_{R}x) ∈ s" show "convex s" unfolding convex_alt proof safe fix x y fix μ :: real assume **: "x ∈ s" "y ∈ s" "0 ≤ μ" "μ ≤ 1" show "(1 - μ) *⇩_{R}x + μ *⇩_{R}y ∈ s" proof (cases "x = y") case False then show ?thesis using *[rule_format, of "{x, y}" "λ z. if z = x then 1 - μ else μ"] ** by auto next case True then show ?thesis using *[rule_format, of "{x, y}" "λ z. 1"] ** by (auto simp: field_simps real_vector.scale_left_diff_distrib) qed qed qed lemma convex_finite: assumes "finite s" shows "convex s ⟷ (∀u. (∀x∈s. 0 ≤ u x) ∧ sum u s = 1 ⟶ sum (λx. u x *⇩_{R}x) s ∈ s)" unfolding convex_explicit apply safe subgoal for u by (erule allE [where x=s], erule allE [where x=u]) auto subgoal for t u proof - have if_distrib_arg: "⋀P f g x. (if P then f else g) x = (if P then f x else g x)" by simp assume sum: "∀u. (∀x∈s. 0 ≤ u x) ∧ sum u s = 1 ⟶ (∑x∈s. u x *⇩_{R}x) ∈ s" assume *: "∀x∈t. 0 ≤ u x" "sum u t = 1" assume "t ⊆ s" then have "s ∩ t = t" by auto with sum[THEN spec[where x="λx. if x∈t then u x else 0"]] * show "(∑x∈t. u x *⇩_{R}x) ∈ s" by (auto simp: assms sum.If_cases if_distrib if_distrib_arg) qed done subsection ‹Functions that are convex on a set› definition%important convex_on :: "'a::real_vector set ⇒ ('a ⇒ real) ⇒ bool" where "convex_on s f ⟷ (∀x∈s. ∀y∈s. ∀u≥0. ∀v≥0. u + v = 1 ⟶ f (u *⇩_{R}x + v *⇩_{R}y) ≤ u * f x + v * f y)" lemma convex_onI [intro?]: assumes "⋀t x y. t > 0 ⟹ t < 1 ⟹ x ∈ A ⟹ y ∈ A ⟹ f ((1 - t) *⇩_{R}x + t *⇩_{R}y) ≤ (1 - t) * f x + t * f y" shows "convex_on A f" unfolding convex_on_def proof clarify fix x y fix u v :: real assume A: "x ∈ A" "y ∈ A" "u ≥ 0" "v ≥ 0" "u + v = 1" from A(5) have [simp]: "v = 1 - u" by (simp add: algebra_simps) from A(1-4) show "f (u *⇩_{R}x + v *⇩_{R}y) ≤ u * f x + v * f y" using assms[of u y x] by (cases "u = 0 ∨ u = 1") (auto simp: algebra_simps) qed lemma convex_on_linorderI [intro?]: fixes A :: "('a::{linorder,real_vector}) set" assumes "⋀t x y. t > 0 ⟹ t < 1 ⟹ x ∈ A ⟹ y ∈ A ⟹ x < y ⟹ f ((1 - t) *⇩_{R}x + t *⇩_{R}y) ≤ (1 - t) * f x + t * f y" shows "convex_on A f" proof fix x y fix t :: real assume A: "x ∈ A" "y ∈ A" "t > 0" "t < 1" with assms [of t x y] assms [of "1 - t" y x] show "f ((1 - t) *⇩_{R}x + t *⇩_{R}y) ≤ (1 - t) * f x + t * f y" by (cases x y rule: linorder_cases) (auto simp: algebra_simps) qed lemma convex_onD: assumes "convex_on A f" shows "⋀t x y. t ≥ 0 ⟹ t ≤ 1 ⟹ x ∈ A ⟹ y ∈ A ⟹ f ((1 - t) *⇩_{R}x + t *⇩_{R}y) ≤ (1 - t) * f x + t * f y" using assms by (auto simp: convex_on_def) lemma convex_onD_Icc: assumes "convex_on {x..y} f" "x ≤ (y :: _ :: {real_vector,preorder})" shows "⋀t. t ≥ 0 ⟹ t ≤ 1 ⟹ f ((1 - t) *⇩_{R}x + t *⇩_{R}y) ≤ (1 - t) * f x + t * f y" using assms(2) by (intro convex_onD [OF assms(1)]) simp_all lemma convex_on_subset: "convex_on t f ⟹ s ⊆ t ⟹ convex_on s f" unfolding convex_on_def by auto lemma convex_on_add [intro]: assumes "convex_on s f" and "convex_on s g" shows "convex_on s (λx. f x + g x)" proof - { fix x y assume "x ∈ s" "y ∈ s" moreover fix u v :: real assume "0 ≤ u" "0 ≤ v" "u + v = 1" ultimately have "f (u *⇩_{R}x + v *⇩_{R}y) + g (u *⇩_{R}x + v *⇩_{R}y) ≤ (u * f x + v * f y) + (u * g x + v * g y)" using assms unfolding convex_on_def by (auto simp: add_mono) then have "f (u *⇩_{R}x + v *⇩_{R}y) + g (u *⇩_{R}x + v *⇩_{R}y) ≤ u * (f x + g x) + v * (f y + g y)" by (simp add: field_simps) } then show ?thesis unfolding convex_on_def by auto qed lemma convex_on_cmul [intro]: fixes c :: real assumes "0 ≤ c" and "convex_on s f" shows "convex_on s (λx. c * f x)" proof - have *: "u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" for u c fx v fy :: real by (simp add: field_simps) show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)] unfolding convex_on_def and * by auto qed lemma convex_lower: assumes "convex_on s f" and "x ∈ s" and "y ∈ s" and "0 ≤ u" and "0 ≤ v" and "u + v = 1" shows "f (u *⇩_{R}x + v *⇩_{R}y) ≤ max (f x) (f y)" proof - let ?m = "max (f x) (f y)" have "u * f x + v * f y ≤ u * max (f x) (f y) + v * max (f x) (f y)" using assms(4,5) by (auto simp: mult_left_mono add_mono) also have "… = max (f x) (f y)" using assms(6) by (simp add: distrib_right [symmetric]) finally show ?thesis using assms unfolding convex_on_def by fastforce qed lemma convex_on_dist [intro]: fixes s :: "'a::real_normed_vector set" shows "convex_on s (λx. dist a x)" proof (auto simp: convex_on_def dist_norm) fix x y assume "x ∈ s" "y ∈ s" fix u v :: real assume "0 ≤ u" assume "0 ≤ v" assume "u + v = 1" have "a = u *⇩_{R}a + v *⇩_{R}a" unfolding scaleR_left_distrib[symmetric] and ‹u + v = 1› by simp then have *: "a - (u *⇩_{R}x + v *⇩_{R}y) = (u *⇩_{R}(a - x)) + (v *⇩_{R}(a - y))" by (auto simp: algebra_simps) show "norm (a - (u *⇩_{R}x + v *⇩_{R}y)) ≤ u * norm (a - x) + v * norm (a - y)" unfolding * using norm_triangle_ineq[of "u *⇩_{R}(a - x)" "v *⇩_{R}(a - y)"] using ‹0 ≤ u› ‹0 ≤ v› by auto qed subsection%unimportant ‹Arithmetic operations on sets preserve convexity› lemma convex_linear_image: assumes "linear f" and "convex s" shows "convex (f ` s)" proof - interpret f: linear f by fact from ‹convex s› show "convex (f ` s)" by (simp add: convex_def f.scaleR [symmetric] f.add [symmetric]) qed lemma convex_linear_vimage: assumes "linear f" and "convex s" shows "convex (f -` s)" proof - interpret f: linear f by fact from ‹convex s› show "convex (f -` s)" by (simp add: convex_def f.add f.scaleR) qed lemma convex_scaling: assumes "convex s" shows "convex ((λx. c *⇩_{R}x) ` s)" proof - have "linear (λx. c *⇩_{R}x)" by (simp add: linearI scaleR_add_right) then show ?thesis using ‹convex s› by (rule convex_linear_image) qed lemma convex_scaled: assumes "convex S" shows "convex ((λx. x *⇩_{R}c) ` S)" proof - have "linear (λx. x *⇩_{R}c)" by (simp add: linearI scaleR_add_left) then show ?thesis using ‹convex S› by (rule convex_linear_image) qed lemma convex_negations: assumes "convex S" shows "convex ((λx. - x) ` S)" proof - have "linear (λx. - x)" by (simp add: linearI) then show ?thesis using ‹convex S› by (rule convex_linear_image) qed lemma convex_sums: assumes "convex S" and "convex T" shows "convex (⋃x∈ S. ⋃y ∈ T. {x + y})" proof - have "linear (λ(x, y). x + y)" by (auto intro: linearI simp: scaleR_add_right) with assms have "convex ((λ(x, y). x + y) ` (S × T))" by (intro convex_linear_image convex_Times) also have "((λ(x, y). x + y) ` (S × T)) = (⋃x∈ S. ⋃y ∈ T. {x + y})" by auto finally show ?thesis . qed lemma convex_differences: assumes "convex S" "convex T" shows "convex (⋃x∈ S. ⋃y ∈ T. {x - y})" proof - have "{x - y| x y. x ∈ S ∧ y ∈ T} = {x + y |x y. x ∈ S ∧ y ∈ uminus ` T}" by (auto simp: diff_conv_add_uminus simp del: add_uminus_conv_diff) then show ?thesis using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto qed lemma convex_translation: assumes "convex S" shows "convex ((λx. a + x) ` S)" proof - have "(⋃ x∈ {a}. ⋃y ∈ S. {x + y}) = (λx. a + x) ` S" by auto then show ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed lemma convex_affinity: assumes "convex S" shows "convex ((λx. a + c *⇩_{R}x) ` S)" proof - have "(λx. a + c *⇩_{R}x) ` S = (+) a ` ( *⇩_{R}) c ` S" by auto then show ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed lemma pos_is_convex: "convex {0 :: real <..}" unfolding convex_alt proof safe fix y x μ :: real assume *: "y > 0" "x > 0" "μ ≥ 0" "μ ≤ 1" { assume "μ = 0" then have "μ *⇩_{R}x + (1 - μ) *⇩_{R}y = y" by simp then have "μ *⇩_{R}x + (1 - μ) *⇩_{R}y > 0" using * by simp } moreover { assume "μ = 1" then have "μ *⇩_{R}x + (1 - μ) *⇩_{R}y > 0" using * by simp } moreover { assume "μ ≠ 1" "μ ≠ 0" then have "μ > 0" "(1 - μ) > 0" using * by auto then have "μ *⇩_{R}x + (1 - μ) *⇩_{R}y > 0" using * by (auto simp: add_pos_pos) } ultimately show "(1 - μ) *⇩_{R}y + μ *⇩_{R}x > 0" by fastforce qed lemma convex_on_sum: fixes a :: "'a ⇒ real" and y :: "'a ⇒ 'b::real_vector" and f :: "'b ⇒ real" assumes "finite s" "s ≠ {}" and "convex_on C f" and "convex C" and "(∑ i ∈ s. a i) = 1" and "⋀i. i ∈ s ⟹ a i ≥ 0" and "⋀i. i ∈ s ⟹ y i ∈ C" shows "f (∑ i ∈ s. a i *⇩_{R}y i) ≤ (∑ i ∈ s. a i * f (y i))" using assms proof (induct s arbitrary: a rule: finite_ne_induct) case (singleton i) then have ai: "a i = 1" by auto then show ?case by auto next case (insert i s) then have "convex_on C f" by simp from this[unfolded convex_on_def, rule_format] have conv: "⋀x y μ. x ∈ C ⟹ y ∈ C ⟹ 0 ≤ μ ⟹ μ ≤ 1 ⟹ f (μ *⇩_{R}x + (1 - μ) *⇩_{R}y) ≤ μ * f x + (1 - μ) * f y" by simp show ?case proof (cases "a i = 1") case True then have "(∑ j ∈ s. a j) = 0" using insert by auto then have "⋀j. j ∈ s ⟹ a j = 0" using insert by (fastforce simp: sum_nonneg_eq_0_iff) then show ?thesis using insert by auto next case False from insert have yai: "y i ∈ C" "a i ≥ 0" by auto have fis: "finite (insert i s)" using insert by auto then have ai1: "a i ≤ 1" using sum_nonneg_leq_bound[of "insert i s" a] insert by simp then have "a i < 1" using False by auto then have i0: "1 - a i > 0" by auto let ?a = "λj. a j / (1 - a i)" have a_nonneg: "?a j ≥ 0" if "j ∈ s" for j using i0 insert that by fastforce have "(∑ j ∈ insert i s. a j) = 1" using insert by auto then have "(∑ j ∈ s. a j) = 1 - a i" using sum.insert insert by fastforce then have "(∑ j ∈ s. a j) / (1 - a i) = 1" using i0 by auto then have a1: "(∑ j ∈ s. ?a j) = 1" unfolding sum_divide_distrib by simp have "convex C" using insert by auto then have asum: "(∑ j ∈ s. ?a j *⇩_{R}y j) ∈ C" using insert convex_sum [OF ‹finite s› ‹convex C› a1 a_nonneg] by auto have asum_le: "f (∑ j ∈ s. ?a j *⇩_{R}y j) ≤ (∑ j ∈ s. ?a j * f (y j))" using a_nonneg a1 insert by blast have "f (∑ j ∈ insert i s. a j *⇩_{R}y j) = f ((∑ j ∈ s. a j *⇩_{R}y j) + a i *⇩_{R}y i)" using sum.insert[of s i "λ j. a j *⇩_{R}y j", OF ‹finite s› ‹i ∉ s›] insert by (auto simp only: add.commute) also have "… = f (((1 - a i) * inverse (1 - a i)) *⇩_{R}(∑ j ∈ s. a j *⇩_{R}y j) + a i *⇩_{R}y i)" using i0 by auto also have "… = f ((1 - a i) *⇩_{R}(∑ j ∈ s. (a j * inverse (1 - a i)) *⇩_{R}y j) + a i *⇩_{R}y i)" using scaleR_right.sum[of "inverse (1 - a i)" "λ j. a j *⇩_{R}y j" s, symmetric] by (auto simp: algebra_simps) also have "… = f ((1 - a i) *⇩_{R}(∑ j ∈ s. ?a j *⇩_{R}y j) + a i *⇩_{R}y i)" by (auto simp: divide_inverse) also have "… ≤ (1 - a i) *⇩_{R}f ((∑ j ∈ s. ?a j *⇩_{R}y j)) + a i * f (y i)" using conv[of "y i" "(∑ j ∈ s. ?a j *⇩_{R}y j)" "a i", OF yai(1) asum yai(2) ai1] by (auto simp: add.commute) also have "… ≤ (1 - a i) * (∑ j ∈ s. ?a j * f (y j)) + a i * f (y i)" using add_right_mono [OF mult_left_mono [of _ _ "1 - a i", OF asum_le less_imp_le[OF i0]], of "a i * f (y i)"] by simp also have "… = (∑ j ∈ s. (1 - a i) * ?a j * f (y j)) + a i * f (y i)" unfolding sum_distrib_left[of "1 - a i" "λ j. ?a j * f (y j)"] using i0 by auto also have "… = (∑ j ∈ s. a j * f (y j)) + a i * f (y i)" using i0 by auto also have "… = (∑ j ∈ insert i s. a j * f (y j))" using insert by auto finally show ?thesis by simp qed qed lemma convex_on_alt: fixes C :: "'a::real_vector set" assumes "convex C" shows "convex_on C f ⟷ (∀x ∈ C. ∀ y ∈ C. ∀ μ :: real. μ ≥ 0 ∧ μ ≤ 1 ⟶ f (μ *⇩_{R}x + (1 - μ) *⇩_{R}y) ≤ μ * f x + (1 - μ) * f y)" proof safe fix x y fix μ :: real assume *: "convex_on C f" "x ∈ C" "y ∈ C" "0 ≤ μ" "μ ≤ 1" from this[unfolded convex_on_def, rule_format] have "0 ≤ u ⟹ 0 ≤ v ⟹ u + v = 1 ⟹ f (u *⇩_{R}x + v *⇩_{R}y) ≤ u * f x + v * f y" for u v by auto from this [of "μ" "1 - μ", simplified] * show "f (μ *⇩_{R}x + (1 - μ) *⇩_{R}y) ≤ μ * f x + (1 - μ) * f y" by auto next assume *: "∀x∈C. ∀y∈C. ∀μ. 0 ≤ μ ∧ μ ≤ 1 ⟶ f (μ *⇩_{R}x + (1 - μ) *⇩_{R}y) ≤ μ * f x + (1 - μ) * f y" { fix x y fix u v :: real assume **: "x ∈ C" "y ∈ C" "u ≥ 0" "v ≥ 0" "u + v = 1" then have[simp]: "1 - u = v" by auto from *[rule_format, of x y u] have "f (u *⇩_{R}x + v *⇩_{R}y) ≤ u * f x + v * f y" using ** by auto } then show "convex_on C f" unfolding convex_on_def by auto qed lemma convex_on_diff: fixes f :: "real ⇒ real" assumes f: "convex_on I f" and I: "x ∈ I" "y ∈ I" and t: "x < t" "t < y" shows "(f x - f t) / (x - t) ≤ (f x - f y) / (x - y)" and "(f x - f y) / (x - y) ≤ (f t - f y) / (t - y)" proof - define a where "a ≡ (t - y) / (x - y)" with t have "0 ≤ a" "0 ≤ 1 - a" by (auto simp: field_simps) with f ‹x ∈ I› ‹y ∈ I› have cvx: "f (a * x + (1 - a) * y) ≤ a * f x + (1 - a) * f y" by (auto simp: convex_on_def) have "a * x + (1 - a) * y = a * (x - y) + y" by (simp add: field_simps) also have "… = t" unfolding a_def using ‹x < t› ‹t < y› by simp finally have "f t ≤ a * f x + (1 - a) * f y" using cvx by simp also have "… = a * (f x - f y) + f y" by (simp add: field_simps) finally have "f t - f y ≤ a * (f x - f y)" by simp with t show "(f x - f t) / (x - t) ≤ (f x - f y) / (x - y)" by (simp add: le_divide_eq divide_le_eq field_simps a_def) with t show "(f x - f y) / (x - y) ≤ (f t - f y) / (t - y)" by (simp add: le_divide_eq divide_le_eq field_simps) qed lemma pos_convex_function: fixes f :: "real ⇒ real" assumes "convex C" and leq: "⋀x y. x ∈ C ⟹ y ∈ C ⟹ f' x * (y - x) ≤ f y - f x" shows "convex_on C f" unfolding convex_on_alt[OF assms(1)] using assms proof safe fix x y μ :: real let ?x = "μ *⇩_{R}x + (1 - μ) *⇩_{R}y" assume *: "convex C" "x ∈ C" "y ∈ C" "μ ≥ 0" "μ ≤ 1" then have "1 - μ ≥ 0" by auto then have xpos: "?x ∈ C" using * unfolding convex_alt by fastforce have geq: "μ * (f x - f ?x) + (1 - μ) * (f y - f ?x) ≥ μ * f' ?x * (x - ?x) + (1 - μ) * f' ?x * (y - ?x)" using add_mono [OF mult_left_mono [OF leq [OF xpos *(2)] ‹μ ≥ 0›] mult_left_mono [OF leq [OF xpos *(3)] ‹1 - μ ≥ 0›]] by auto then have "μ * f x + (1 - μ) * f y - f ?x ≥ 0" by (auto simp: field_simps) then show "f (μ *⇩_{R}x + (1 - μ) *⇩_{R}y) ≤ μ * f x + (1 - μ) * f y" using convex_on_alt by auto qed lemma atMostAtLeast_subset_convex: fixes C :: "real set" assumes "convex C" and "x ∈ C" "y ∈ C" "x < y" shows "{x .. y} ⊆ C" proof safe fix z assume z: "z ∈ {x .. y}" have less: "z ∈ C" if *: "x < z" "z < y" proof - let ?μ = "(y - z) / (y - x)" have "0 ≤ ?μ" "?μ ≤ 1" using assms * by (auto simp: field_simps) then have comb: "?μ * x + (1 - ?μ) * y ∈ C" using assms iffD1[OF convex_alt, rule_format, of C y x ?μ] by (simp add: algebra_simps) have "?μ * x + (1 - ?μ) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y" by (auto simp: field_simps) also have "… = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)" using assms by (simp only: add_divide_distrib) (auto simp: field_simps) also have "… = z" using assms by (auto simp: field_simps) finally show ?thesis using comb by auto qed show "z ∈ C" using z less assms by (auto simp: le_less) qed lemma f''_imp_f': fixes f :: "real ⇒ real" assumes "convex C" and f': "⋀x. x ∈ C ⟹ DERIV f x :> (f' x)" and f'': "⋀x. x ∈ C ⟹ DERIV f' x :> (f'' x)" and pos: "⋀x. x ∈ C ⟹ f'' x ≥ 0" and x: "x ∈ C" and y: "y ∈ C" shows "f' x * (y - x) ≤ f y - f x" using assms proof - have less_imp: "f y - f x ≥ f' x * (y - x)" "f' y * (x - y) ≤ f x - f y" if *: "x ∈ C" "y ∈ C" "y > x" for x y :: real proof - from * have ge: "y - x > 0" "y - x ≥ 0" by auto from * have le: "x - y < 0" "x - y ≤ 0" by auto then obtain z1 where z1: "z1 > x" "z1 < y" "f y - f x = (y - x) * f' z1" using subsetD[OF atMostAtLeast_subset_convex[OF ‹convex C› ‹x ∈ C› ‹y ∈ C› ‹x < y›], THEN f', THEN MVT2[OF ‹x < y›, rule_format, unfolded atLeastAtMost_iff[symmetric]]] by auto then have "z1 ∈ C" using atMostAtLeast_subset_convex ‹convex C› ‹x ∈ C› ‹y ∈ C› ‹x < y› by fastforce from z1 have z1': "f x - f y = (x - y) * f' z1" by (simp add: field_simps) obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2" using subsetD[OF atMostAtLeast_subset_convex[OF ‹convex C› ‹x ∈ C› ‹z1 ∈ C› ‹x < z1›], THEN f'', THEN MVT2[OF ‹x < z1›, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 by auto obtain z3 where z3: "z3 > z1" "z3 < y" "f' y - f' z1 = (y - z1) * f'' z3" using subsetD[OF atMostAtLeast_subset_convex[OF ‹convex C› ‹z1 ∈ C› ‹y ∈ C› ‹z1 < y›], THEN f'', THEN MVT2[OF ‹z1 < y›, rule_format, unfolded atLeastAtMost_iff[symmetric]]] z1 by auto have "f' y - (f x - f y) / (x - y) = f' y - f' z1" using * z1' by auto also have "… = (y - z1) * f'' z3" using z3 by auto finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp have A': "y - z1 ≥ 0" using z1 by auto have "z3 ∈ C" using z3 * atMostAtLeast_subset_convex ‹convex C› ‹x ∈ C› ‹z1 ∈ C› ‹x < z1› by fastforce then have B': "f'' z3 ≥ 0" using assms by auto from A' B' have "(y - z1) * f'' z3 ≥ 0" by auto from cool' this have "f' y - (f x - f y) / (x - y) ≥ 0" by auto from mult_right_mono_neg[OF this le(2)] have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) ≤ 0 * (x - y)" by (simp add: algebra_simps) then have "f' y * (x - y) - (f x - f y) ≤ 0" using le by auto then have res: "f' y * (x - y) ≤ f x - f y" by auto have "(f y - f x) / (y - x) - f' x = f' z1 - f' x" using * z1 by auto also have "… = (z1 - x) * f'' z2" using z2 by auto finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp have A: "z1 - x ≥ 0" using z1 by auto have "z2 ∈ C" using z2 z1 * atMostAtLeast_subset_convex ‹convex C› ‹z1 ∈ C› ‹y ∈ C› ‹z1 < y› by fastforce then have B: "f'' z2 ≥ 0" using assms by auto from A B have "(z1 - x) * f'' z2 ≥ 0" by auto with cool have "(f y - f x) / (y - x) - f' x ≥ 0" by auto from mult_right_mono[OF this ge(2)] have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) ≥ 0 * (y - x)" by (simp add: algebra_simps) then have "f y - f x - f' x * (y - x) ≥ 0" using ge by auto then show "f y - f x ≥ f' x * (y - x)" "f' y * (x - y) ≤ f x - f y" using res by auto qed show ?thesis proof (cases "x = y") case True with x y show ?thesis by auto next case False with less_imp x y show ?thesis by (auto simp: neq_iff) qed qed lemma f''_ge0_imp_convex: fixes f :: "real ⇒ real" assumes conv: "convex C" and f': "⋀x. x ∈ C ⟹ DERIV f x :> (f' x)" and f'': "⋀x. x ∈ C ⟹ DERIV f' x :> (f'' x)" and pos: "⋀x. x ∈ C ⟹ f'' x ≥ 0" shows "convex_on C f" using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastforce lemma minus_log_convex: fixes b :: real assumes "b > 1" shows "convex_on {0 <..} (λ x. - log b x)" proof - have "⋀z. z > 0 ⟹ DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto then have f': "⋀z. z > 0 ⟹ DERIV (λ z. - log b z) z :> - 1 / (ln b * z)" by (auto simp: DERIV_minus) have "⋀z::real. z > 0 ⟹ DERIV inverse z :> - (inverse z ^ Suc (Suc 0))" using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto from this[THEN DERIV_cmult, of _ "- 1 / ln b"] have "⋀z::real. z > 0 ⟹ DERIV (λ z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))" by auto then have f''0: "⋀z::real. z > 0 ⟹ DERIV (λ z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)" unfolding inverse_eq_divide by (auto simp: mult.assoc) have f''_ge0: "⋀z::real. z > 0 ⟹ 1 / (ln b * z * z) ≥ 0" using ‹b > 1› by (auto intro!: less_imp_le) from f''_ge0_imp_convex[OF pos_is_convex, unfolded greaterThan_iff, OF f' f''0 f''_ge0] show ?thesis by auto qed subsection%unimportant ‹Convexity of real functions› lemma convex_on_realI: assumes "connected A" and "⋀x. x ∈ A ⟹ (f has_real_derivative f' x) (at x)" and "⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≤ y ⟹ f' x ≤ f' y" shows "convex_on A f" proof (rule convex_on_linorderI) fix t x y :: real assume t: "t > 0" "t < 1" assume xy: "x ∈ A" "y ∈ A" "x < y" define z where "z = (1 - t) * x + t * y" with ‹connected A› and xy have ivl: "{x..y} ⊆ A" using connected_contains_Icc by blast from xy t have xz: "z > x" by (simp add: z_def algebra_simps) have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps) also from xy t have "… > 0" by (intro mult_pos_pos) simp_all finally have yz: "z < y" by simp from assms xz yz ivl t have "∃ξ. ξ > x ∧ ξ < z ∧ f z - f x = (z - x) * f' ξ" by (intro MVT2) (auto intro!: assms(2)) then obtain ξ where ξ: "ξ > x" "ξ < z" "f' ξ = (f z - f x) / (z - x)" by auto from assms xz yz ivl t have "∃η. η > z ∧ η < y ∧ f y - f z = (y - z) * f' η" by (intro MVT2) (auto intro!: assms(2)) then obtain η where η: "η > z" "η < y" "f' η = (f y - f z) / (y - z)" by auto from η(3) have "(f y - f z) / (y - z) = f' η" .. also from ξ η ivl have "ξ ∈ A" "η ∈ A" by auto with ξ η have "f' η ≥ f' ξ" by (intro assms(3)) auto also from ξ(3) have "f' ξ = (f z - f x) / (z - x)" . finally have "(f y - f z) * (z - x) ≥ (f z - f x) * (y - z)" using xz yz by (simp add: field_simps) also have "z - x = t * (y - x)" by (simp add: z_def algebra_simps) also have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps) finally have "(f y - f z) * t ≥ (f z - f x) * (1 - t)" using xy by simp then show "(1 - t) * f x + t * f y ≥ f ((1 - t) *⇩_{R}x + t *⇩_{R}y)" by (simp add: z_def algebra_simps) qed lemma convex_on_inverse: assumes "A ⊆ {0<..}" shows "convex_on A (inverse :: real ⇒ real)" proof (rule convex_on_subset[OF _ assms], intro convex_on_realI[of _ _ "λx. -inverse (x^2)"]) fix u v :: real assume "u ∈ {0<..}" "v ∈ {0<..}" "u ≤ v" with assms show "-inverse (u^2) ≤ -inverse (v^2)" by (intro le_imp_neg_le le_imp_inverse_le power_mono) (simp_all) qed (insert assms, auto intro!: derivative_eq_intros simp: divide_simps power2_eq_square) lemma convex_onD_Icc': assumes "convex_on {x..y} f" "c ∈ {x..y}" defines "d ≡ y - x" shows "f c ≤ (f y - f x) / d * (c - x) + f x" proof (cases x y rule: linorder_cases) case less then have d: "d > 0" by (simp add: d_def) from assms(2) less have A: "0 ≤ (c - x) / d" "(c - x) / d ≤ 1" by (simp_all add: d_def divide_simps) have "f c = f (x + (c - x) * 1)" by simp also from less have "1 = ((y - x) / d)" by (simp add: d_def) also from d have "x + (c - x) * … = (1 - (c - x) / d) *⇩_{R}x + ((c - x) / d) *⇩_{R}y" by (simp add: field_simps) also have "f … ≤ (1 - (c - x) / d) * f x + (c - x) / d * f y" using assms less by (intro convex_onD_Icc) simp_all also from d have "… = (f y - f x) / d * (c - x) + f x" by (simp add: field_simps) finally show ?thesis . qed (insert assms(2), simp_all) lemma convex_onD_Icc'': assumes "convex_on {x..y} f" "c ∈ {x..y}" defines "d ≡ y - x" shows "f c ≤ (f x - f y) / d * (y - c) + f y" proof (cases x y rule: linorder_cases) case less then have d: "d > 0" by (simp add: d_def) from assms(2) less have A: "0 ≤ (y - c) / d" "(y - c) / d ≤ 1" by (simp_all add: d_def divide_simps) have "f c = f (y - (y - c) * 1)" by simp also from less have "1 = ((y - x) / d)" by (simp add: d_def) also from d have "y - (y - c) * … = (1 - (1 - (y - c) / d)) *⇩_{R}x + (1 - (y - c) / d) *⇩_{R}y" by (simp add: field_simps) also have "f … ≤ (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y" using assms less by (intro convex_onD_Icc) (simp_all add: field_simps) also from d have "… = (f x - f y) / d * (y - c) + f y" by (simp add: field_simps) finally show ?thesis . qed (insert assms(2), simp_all) lemma convex_supp_sum: assumes "convex S" and 1: "supp_sum u I = 1" and "⋀i. i ∈ I ⟹ 0 ≤ u i ∧ (u i = 0 ∨ f i ∈ S)" shows "supp_sum (λi. u i *⇩_{R}f i) I ∈ S" proof - have fin: "finite {i ∈ I. u i ≠ 0}" using 1 sum.infinite by (force simp: supp_sum_def support_on_def) then have eq: "supp_sum (λi. u i *⇩_{R}f i) I = sum (λi. u i *⇩_{R}f i) {i ∈ I. u i ≠ 0}" by (force intro: sum.mono_neutral_left simp: supp_sum_def support_on_def) show ?thesis apply (simp add: eq) apply (rule convex_sum [OF fin ‹convex S›]) using 1 assms apply (auto simp: supp_sum_def support_on_def) done qed lemma convex_translation_eq [simp]: "convex ((λx. a + x) ` s) ⟷ convex s" by (metis convex_translation translation_galois) lemma convex_linear_image_eq [simp]: fixes f :: "'a::real_vector ⇒ 'b::real_vector" shows "⟦linear f; inj f⟧ ⟹ convex (f ` s) ⟷ convex s" by (metis (no_types) convex_linear_image convex_linear_vimage inj_vimage_image_eq) lemma closure_bounded_linear_image_subset: assumes f: "bounded_linear f" shows "f ` closure S ⊆ closure (f ` S)" using linear_continuous_on [OF f] closed_closure closure_subset by (rule image_closure_subset) lemma closure_linear_image_subset: fixes f :: "'m::euclidean_space ⇒ 'n::real_normed_vector" assumes "linear f" shows "f ` (closure S) ⊆ closure (f ` S)" using assms unfolding linear_conv_bounded_linear by (rule closure_bounded_linear_image_subset) lemma closed_injective_linear_image: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes S: "closed S" and f: "linear f" "inj f" shows "closed (f ` S)" proof - obtain g where g: "linear g" "g ∘ f = id" using linear_injective_left_inverse [OF f] by blast then have confg: "continuous_on (range f) g" using linear_continuous_on linear_conv_bounded_linear by blast have [simp]: "g ` f ` S = S" using g by (simp add: image_comp) have cgf: "closed (g ` f ` S)" by (simp add: ‹g ∘ f = id› S image_comp) have [simp]: "(range f ∩ g -` S) = f ` S" using g unfolding o_def id_def image_def by auto metis+ show ?thesis proof (rule closedin_closed_trans [of "range f"]) show "closedin (subtopology euclidean (range f)) (f ` S)" using continuous_closedin_preimage [OF confg cgf] by simp show "closed (range f)" apply (rule closed_injective_image_subspace) using f apply (auto simp: linear_linear linear_injective_0) done qed qed lemma closed_injective_linear_image_eq: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes f: "linear f" "inj f" shows "(closed(image f s) ⟷ closed s)" by (metis closed_injective_linear_image closure_eq closure_linear_image_subset closure_subset_eq f(1) f(2) inj_image_subset_iff) lemma closure_injective_linear_image: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" shows "⟦linear f; inj f⟧ ⟹ f ` (closure S) = closure (f ` S)" apply (rule subset_antisym) apply (simp add: closure_linear_image_subset) by (simp add: closure_minimal closed_injective_linear_image closure_subset image_mono) lemma closure_bounded_linear_image: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" shows "⟦linear f; bounded S⟧ ⟹ f ` (closure S) = closure (f ` S)" apply (rule subset_antisym, simp add: closure_linear_image_subset) apply (rule closure_minimal, simp add: closure_subset image_mono) by (meson bounded_closure closed_closure compact_continuous_image compact_eq_bounded_closed linear_continuous_on linear_conv_bounded_linear) lemma closure_scaleR: fixes S :: "'a::real_normed_vector set" shows "(( *⇩_{R}) c) ` (closure S) = closure ((( *⇩_{R}) c) ` S)" proof show "(( *⇩_{R}) c) ` (closure S) ⊆ closure ((( *⇩_{R}) c) ` S)" using bounded_linear_scaleR_right by (rule closure_bounded_linear_image_subset) show "closure ((( *⇩_{R}) c) ` S) ⊆ (( *⇩_{R}) c) ` (closure S)" by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure) qed lemma fst_linear: "linear fst" unfolding linear_iff by (simp add: algebra_simps) lemma snd_linear: "linear snd" unfolding linear_iff by (simp add: algebra_simps) lemma fst_snd_linear: "linear (λ(x,y). x + y)" unfolding linear_iff by (simp add: algebra_simps) lemma vector_choose_size: assumes "0 ≤ c" obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c" proof - obtain a::'a where "a ≠ 0" using UNIV_not_singleton UNIV_eq_I set_zero singletonI by fastforce then show ?thesis by (rule_tac x="scaleR (c / norm a) a" in that) (simp add: assms) qed lemma vector_choose_dist: assumes "0 ≤ c" obtains y :: "'a::{real_normed_vector, perfect_space}" where "dist x y = c" by (metis add_diff_cancel_left' assms dist_commute dist_norm vector_choose_size) lemma sphere_eq_empty [simp]: fixes a :: "'a::{real_normed_vector, perfect_space}" shows "sphere a r = {} ⟷ r < 0" by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist) lemma sum_delta_notmem: assumes "x ∉ s" shows "sum (λy. if (y = x) then P x else Q y) s = sum Q s" and "sum (λy. if (x = y) then P x else Q y) s = sum Q s" and "sum (λy. if (y = x) then P y else Q y) s = sum Q s" and "sum (λy. if (x = y) then P y else Q y) s = sum Q s" apply (rule_tac [!] sum.cong) using assms apply auto done lemma sum_delta'': fixes s::"'a::real_vector set" assumes "finite s" shows "(∑x∈s. (if y = x then f x else 0) *⇩_{R}x) = (if y∈s then (f y) *⇩_{R}y else 0)" proof - have *: "⋀x y. (if y = x then f x else (0::real)) *⇩_{R}x = (if x=y then (f x) *⇩_{R}x else 0)" by auto show ?thesis unfolding * using sum.delta[OF assms, of y "λx. f x *⇩_{R}x"] by auto qed lemma if_smult: "(if P then x else (y::real)) *⇩_{R}v = (if P then x *⇩_{R}v else y *⇩_{R}v)" by (fact if_distrib) lemma dist_triangle_eq: fixes x y z :: "'a::real_inner" shows "dist x z = dist x y + dist y z ⟷ norm (x - y) *⇩_{R}(y - z) = norm (y - z) *⇩_{R}(x - y)" proof - have *: "x - y + (y - z) = x - z" by auto show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *] by (auto simp:norm_minus_commute) qed subsection ‹Affine set and affine hull› definition%important affine :: "'a::real_vector set ⇒ bool" where "affine s ⟷ (∀x∈s. ∀y∈s. ∀u v. u + v = 1 ⟶ u *⇩_{R}x + v *⇩_{R}y ∈ s)" lemma affine_alt: "affine s ⟷ (∀x∈s. ∀y∈s. ∀u::real. (1 - u) *⇩_{R}x + u *⇩_{R}y ∈ s)" unfolding affine_def by (metis eq_diff_eq') lemma affine_empty [iff]: "affine {}" unfolding affine_def by auto lemma affine_sing [iff]: "affine {x}" unfolding affine_alt by (auto simp: scaleR_left_distrib [symmetric]) lemma affine_UNIV [iff]: "affine UNIV" unfolding affine_def by auto lemma affine_Inter [intro]: "(⋀s. s∈f ⟹ affine s) ⟹ affine (⋂f)" unfolding affine_def by auto lemma affine_Int[intro]: "affine s ⟹ affine t ⟹ affine (s ∩ t)" unfolding affine_def by auto lemma affine_scaling: "affine s ⟹ affine (image (λx. c *⇩_{R}x) s)" apply (clarsimp simp add: affine_def) apply (rule_tac x="u *⇩_{R}x + v *⇩_{R}y" in image_eqI) apply (auto simp: algebra_simps) done lemma affine_affine_hull [simp]: "affine(affine hull s)" unfolding hull_def using affine_Inter[of "{t. affine t ∧ s ⊆ t}"] by auto lemma affine_hull_eq[simp]: "(affine hull s = s) ⟷ affine s" by (metis affine_affine_hull hull_same) lemma affine_hyperplane: "affine {x. a ∙ x = b}" by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral) subsubsection%unimportant ‹Some explicit formulations (from Lars Schewe)› lemma affine: fixes V::"'a::real_vector set" shows "affine V ⟷ (∀S u. finite S ∧ S ≠ {} ∧ S ⊆ V ∧ sum u S = 1 ⟶ (∑x∈S. u x *⇩_{R}x) ∈ V)" proof - have "u *⇩_{R}x + v *⇩_{R}y ∈ V" if "x ∈ V" "y ∈ V" "u + v = (1::real)" and *: "⋀S u. ⟦finite S; S ≠ {}; S ⊆ V; sum u S = 1⟧ ⟹ (∑x∈S. u x *⇩_{R}x) ∈ V" for x y u v proof (cases "x = y") case True then show ?thesis using that by (metis scaleR_add_left scaleR_one) next case False then show ?thesis using that *[of "{x,y}" "λw. if w = x then u else v"] by auto qed moreover have "(∑x∈S. u x *⇩_{R}x) ∈ V" if *: "⋀x y u v. ⟦x∈V; y∈V; u + v = 1⟧ ⟹ u *⇩_{R}x + v *⇩_{R}y ∈ V" and "finite S" "S ≠ {}" "S ⊆ V" "sum u S = 1" for S u proof - define n where "n = card S" consider "card S = 0" | "card S = 1" | "card S = 2" | "card S > 2" by linarith then show "(∑x∈S. u x *⇩_{R}x) ∈ V" proof cases assume "card S = 1" then obtain a where "S={a}" by (auto simp: card_Suc_eq) then show ?thesis using that by simp next assume "card S = 2" then obtain a b where "S = {a, b}" by (metis Suc_1 card_1_singletonE card_Suc_eq) then show ?thesis using *[of a b] that by (auto simp: sum_clauses(2)) next assume "card S > 2" then show ?thesis using that n_def proof (induct n arbitrary: u S) case 0 then show ?case by auto next case (Suc n u S) have "sum u S = card S" if "¬ (∃x∈S. u x ≠ 1)" using that unfolding card_eq_sum by auto with Suc.prems obtain x where "x ∈ S" and x: "u x ≠ 1" by force have c: "card (S - {x}) = card S - 1" by (simp add: Suc.prems(3) ‹x ∈ S›) have "sum u (S - {x}) = 1 - u x" by (simp add: Suc.prems sum_diff1_ring ‹x ∈ S›) with x have eq1: "inverse (1 - u x) * sum u (S - {x}) = 1" by auto have inV: "(∑y∈S - {x}. (inverse (1 - u x) * u y) *⇩_{R}y) ∈ V" proof (cases "card (S - {x}) > 2") case True then have S: "S - {x} ≠ {}" "card (S - {x}) = n" using Suc.prems c by force+ show ?thesis proof (rule Suc.hyps) show "(∑a∈S - {x}. inverse (1 - u x) * u a) = 1" by (auto simp: eq1 sum_distrib_left[symmetric]) qed (use S Suc.prems True in auto) next case False then have "card (S - {x}) = Suc (Suc 0)" using Suc.prems c by auto then obtain a b where ab: "(S - {x}) = {a, b}" "a≠b" unfolding card_Suc_eq by auto then show ?thesis using eq1 ‹S ⊆ V› by (auto simp: sum_distrib_left distrib_left intro!: Suc.prems(2)[of a b]) qed have "u x + (1 - u x) = 1 ⟹ u x *⇩_{R}x + (1 - u x) *⇩_{R}((∑y∈S - {x}. u y *⇩_{R}y) /⇩_{R}(1 - u x)) ∈ V" by (rule Suc.prems) (use ‹x ∈ S› Suc.prems inV in ‹auto simp: scaleR_right.sum›) moreover have "(∑a∈S. u a *⇩_{R}a) = u x *⇩_{R}x + (∑a∈S - {x}. u a *⇩_{R}a)" by (meson Suc.prems(3) sum.remove ‹x ∈ S›) ultimately show "(∑x∈S. u x *⇩_{R}x) ∈ V" by (simp add: x) qed qed (use ‹S≠{}› ‹finite S› in auto) qed ultimately show ?thesis unfolding affine_def by meson qed lemma affine_hull_explicit: "affine hull p = {y. ∃S u. finite S ∧ S ≠ {} ∧ S ⊆ p ∧ sum u S = 1 ∧ sum (λv. u v *⇩_{R}v) S = y}" (is "_ = ?rhs") proof (rule hull_unique) show "p ⊆ ?rhs" proof (intro subsetI CollectI exI conjI) show "⋀x. sum (λz. 1) {x} = 1" by auto qed auto show "?rhs ⊆ T" if "p ⊆ T" "affine T" for T using that unfolding affine by blast show "affine ?rhs" unfolding affine_def proof clarify fix u v :: real and sx ux sy uy assume uv: "u + v = 1" and x: "finite sx" "sx ≠ {}" "sx ⊆ p" "sum ux sx = (1::real)" and y: "finite sy" "sy ≠ {}" "sy ⊆ p" "sum uy sy = (1::real)" have **: "(sx ∪ sy) ∩ sx = sx" "(sx ∪ sy) ∩ sy = sy" by auto show "∃S w. finite S ∧ S ≠ {} ∧ S ⊆ p ∧ sum w S = 1 ∧ (∑v∈S. w v *⇩_{R}v) = u *⇩_{R}(∑v∈sx. ux v *⇩_{R}v) + v *⇩_{R}(∑v∈sy. uy v *⇩_{R}v)" proof (intro exI conjI) show "finite (sx ∪ sy)" using x y by auto show "sum (λi. (if i∈sx then u * ux i else 0) + (if i∈sy then v * uy i else 0)) (sx ∪ sy) = 1" using x y uv by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] sum_distrib_left [symmetric] **) have "(∑i∈sx ∪ sy. ((if i ∈ sx then u * ux i else 0) + (if i ∈ sy then v * uy i else 0)) *⇩_{R}i) = (∑i∈sx. (u * ux i) *⇩_{R}i) + (∑i∈sy. (v * uy i) *⇩_{R}i)" using x y unfolding scaleR_left_distrib scaleR_zero_left if_smult by (simp add: sum_Un sum.distrib sum.inter_restrict[symmetric] **) also have "… = u *⇩_{R}(∑v∈sx. ux v *⇩_{R}v) + v *⇩_{R}(∑v∈sy. uy v *⇩_{R}v)" unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by blast finally show "(∑i∈sx ∪ sy. ((if i ∈ sx then u * ux i else 0) + (if i ∈ sy then v * uy i else 0)) *⇩_{R}i) = u *⇩_{R}(∑v∈sx. ux v *⇩_{R}v) + v *⇩_{R}(∑v∈sy. uy v *⇩_{R}v)" . qed (use x y in auto) qed qed lemma affine_hull_finite: assumes "finite S" shows "affine hull S = {y. ∃u. sum u S = 1 ∧ sum (λv. u v *⇩_{R}v) S = y}" proof - have *: "∃h. sum h S = 1 ∧ (∑v∈S. h v *⇩_{R}v) = x" if "F ⊆ S" "finite F" "F ≠ {}" and sum: "sum u F = 1" and x: "(∑v∈F. u v *⇩_{R}v) = x" for x F u proof - have "S ∩ F = F" using that by auto show ?thesis proof (intro exI conjI) show "(∑x∈S. if x ∈ F then u x else 0) = 1" by (metis (mono_tags, lifting) ‹S ∩ F = F› assms sum.inter_restrict sum) show "(∑v∈S. (if v ∈ F then u v else 0) *⇩_{R}v) = x" by (simp add: if_smult cong: if_cong) (metis (no_types) ‹S ∩ F = F› assms sum.inter_restrict x) qed qed show ?thesis unfolding affine_hull_explicit using assms by (fastforce dest: *) qed subsubsection%unimportant ‹Stepping theorems and hence small special cases› lemma affine_hull_empty[simp]: "affine hull {} = {}" by simp lemma affine_hull_finite_step: fixes y :: "'a::real_vector" shows "finite S ⟹ (∃u. sum u (insert a S) = w ∧ sum (λx. u x *⇩_{R}x) (insert a S) = y) ⟷ (∃v u. sum u S = w - v ∧ sum (λx. u x *⇩_{R}x) S = y - v *⇩_{R}a)" (is "_ ⟹ ?lhs = ?rhs") proof - assume fin: "finite S" show "?lhs = ?rhs" proof assume ?lhs then obtain u where u: "sum u (insert a S) = w ∧ (∑x∈insert a S. u x *⇩_{R}x) = y" by auto show ?rhs proof (cases "a ∈ S") case True then show ?thesis using u by (simp add: insert_absorb) (metis diff_zero real_vector.scale_zero_left) next case False show ?thesis by (rule exI [where x="u a"]) (use u fin False in auto) qed next assume ?rhs then obtain v u where vu: "sum u S = w - v" "(∑x∈S. u x *⇩_{R}x) = y - v *⇩_{R}a" by auto have *: "⋀x M. (if x = a then v else M) *⇩_{R}x = (if x = a then v *⇩_{R}x else M *⇩_{R}x)" by auto show ?lhs proof (cases "a ∈ S") case True show ?thesis by (rule exI [where x="λx. (if x=a then v else 0) + u x"]) (simp add: True scaleR_left_distrib sum.distrib sum_clauses fin vu * cong: if_cong) next case False then show ?thesis apply (rule_tac x="λx. if x=a then v else u x" in exI) apply (simp add: vu sum_clauses(2)[OF fin] *) by (simp add: sum_delta_notmem(3) vu) qed qed qed lemma affine_hull_2: fixes a b :: "'a::real_vector" shows "affine hull {a,b} = {u *⇩_{R}a + v *⇩_{R}b| u v. (u + v = 1)}" (is "?lhs = ?rhs") proof - have *: "⋀x y z. z = x - y ⟷ y + z = (x::real)" "⋀x y z. z = x - y ⟷ y + z = (x::'a)" by auto have "?lhs = {y. ∃u. sum u {a, b} = 1 ∧ (∑v∈{a, b}. u v *⇩_{R}v) = y}" using affine_hull_finite[of "{a,b}"] by auto also have "… = {y. ∃v u. u b = 1 - v ∧ u b *⇩_{R}b = y - v *⇩_{R}a}" by (simp add: affine_hull_finite_step[of "{b}" a]) also have "… = ?rhs" unfolding * by auto finally show ?thesis by auto qed lemma affine_hull_3: fixes a b c :: "'a::real_vector" shows "affine hull {a,b,c} = { u *⇩_{R}a + v *⇩_{R}b + w *⇩_{R}c| u v w. u + v + w = 1}" proof - have *: "⋀x y z. z = x - y ⟷ y + z = (x::real)" "⋀x y z. z = x - y ⟷ y + z = (x::'a)" by auto show ?thesis apply (simp add: affine_hull_finite affine_hull_finite_step) unfolding * apply safe apply (metis add.assoc) apply (rule_tac x=u in exI, force) done qed lemma mem_affine: assumes "affine S" "x ∈ S" "y ∈ S" "u + v = 1" shows "u *⇩_{R}x + v *⇩_{R}y ∈ S" using assms affine_def[of S] by auto lemma mem_affine_3: assumes "affine S" "x ∈ S" "y ∈ S" "z ∈ S" "u + v + w = 1" shows "u *⇩_{R}x + v *⇩_{R}y + w *⇩_{R}z ∈ S" proof - have "u *⇩_{R}x + v *⇩_{R}y + w *⇩_{R}z ∈ affine hull {x, y, z}" using affine_hull_3[of x y z] assms by auto moreover have "affine hull {x, y, z} ⊆ affine hull S" using hull_mono[of "{x, y, z}" "S"] assms by auto moreover have "affine hull S = S" using assms affine_hull_eq[of S] by auto ultimately show ?thesis by auto qed lemma mem_affine_3_minus: assumes "affine S" "x ∈ S" "y ∈ S" "z ∈ S" shows "x + v *⇩_{R}(y-z) ∈ S" using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps) corollary mem_affine_3_minus2: "⟦affine S; x ∈ S; y ∈ S; z ∈ S⟧ ⟹ x - v *⇩_{R}(y-z) ∈ S" by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left) subsubsection%unimportant ‹Some relations between affine hull and subspaces› lemma affine_hull_insert_subset_span: "affine hull (insert a S) ⊆ {a + v| v . v ∈ span {x - a | x . x ∈ S}}" proof - have "∃v T u. x = a + v ∧ (finite T ∧ T ⊆ {x - a |x. x ∈ S} ∧ (∑v∈T. u v *⇩_{R}v) = v)" if "finite F" "F ≠ {}" "F ⊆ insert a S" "sum u F = 1" "(∑v∈F. u v *⇩_{R}v) = x" for x F u proof - have *: "(λx. x - a) ` (F - {a}) ⊆ {x - a |x. x ∈ S}" using that by auto show ?thesis proof (intro exI conjI) show "finite ((λx. x - a) ` (F - {a}))" by (simp add: that(1)) show "(∑v∈(λx. x - a) ` (F - {a}). u(v+a) *⇩_{R}v) = x-a" by (simp add: sum.reindex[unfolded inj_on_def] algebra_simps sum_subtractf scaleR_left.sum[symmetric] sum_diff1 that) qed (use ‹F ⊆ insert a S› in auto) qed then show ?thesis unfolding affine_hull_explicit span_explicit by blast qed lemma affine_hull_insert_span: assumes "a ∉ S" shows "affine hull (insert a S) = {a + v | v . v ∈ span {x - a | x. x ∈ S}}" proof - have *: "∃G u. finite G ∧ G ≠ {} ∧ G ⊆ insert a S ∧ sum u G = 1 ∧ (∑v∈G. u v *⇩_{R}v) = y" if "v ∈ span {x - a |x. x ∈ S}" "y = a + v" for y v proof - from that obtain T u where u: "finite T" "T ⊆ {x - a |x. x ∈ S}" "a + (∑v∈T. u v *⇩_{R}v) = y" unfolding span_explicit by auto define F where "F = (λx. x + a) ` T" have F: "finite F" "F ⊆ S" "(∑v∈F. u (v - a) *⇩_{R}(v - a)) = y - a" unfolding F_def using u by (auto simp: sum.reindex[unfolded inj_on_def]) have *: "F ∩ {a} = {}" "F ∩ - {a} = F" using F assms by auto show "∃G u. finite G ∧ G ≠ {} ∧ G ⊆ insert a S ∧ sum u G = 1 ∧ (∑v∈G. u v *⇩_{R}v) = y" apply (rule_tac x = "insert a F" in exI) apply (rule_tac x = "λx. if x=a then 1 - sum (λx. u (x - a)) F else u (x - a)" in exI) using assms F apply (auto simp: sum_clauses sum.If_cases if_smult sum_subtractf scaleR_left.sum algebra_simps *) done qed show ?thesis by (intro subset_antisym affine_hull_insert_subset_span) (auto simp: affine_hull_explicit dest!: *) qed lemma affine_hull_span: assumes "a ∈ S" shows "affine hull S = {a + v | v. v ∈ span {x - a | x. x ∈ S - {a}}}" using affine_hull_insert_span[of a "S - {a}", unfolded insert_Diff[OF assms]] by auto subsubsection%unimportant ‹Parallel affine sets› definition affine_parallel :: "'a::real_vector set ⇒ 'a::real_vector set ⇒ bool" where "affine_parallel S T ⟷ (∃a. T = (λx. a + x) ` S)" lemma affine_parallel_expl_aux: fixes S T :: "'a::real_vector set" assumes "⋀x. x ∈ S ⟷ a + x ∈ T" shows "T = (λx. a + x) ` S" proof - have "x ∈ ((λx. a + x) ` S)" if "x ∈ T" for x using that by (simp add: image_iff) (metis add.commute diff_add_cancel assms) moreover have "T ≥ (λx. a + x) ` S" using assms by auto ultimately show ?thesis by auto qed lemma affine_parallel_expl: "affine_parallel S T ⟷ (∃a. ∀x. x ∈ S ⟷ a + x ∈ T)" unfolding affine_parallel_def using affine_parallel_expl_aux[of S _ T] by auto lemma affine_parallel_reflex: "affine_parallel S S" unfolding affine_parallel_def using image_add_0 by blast lemma affine_parallel_commut: assumes "affine_parallel A B" shows "affine_parallel B A" proof - from assms obtain a where B: "B = (λx. a + x) ` A" unfolding affine_parallel_def by auto have [simp]: "(λx. x - a) = plus (- a)" by (simp add: fun_eq_iff) from B show ?thesis using translation_galois [of B a A] unfolding affine_parallel_def by auto qed lemma affine_parallel_assoc: assumes "affine_parallel A B" and "affine_parallel B C" shows "affine_parallel A C" proof - from assms obtain ab where "B = (λx. ab + x) ` A" unfolding affine_parallel_def by auto moreover from assms obtain bc where "C = (λx. bc + x) ` B" unfolding affine_parallel_def by auto ultimately show ?thesis using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto qed lemma affine_translation_aux: fixes a :: "'a::real_vector" assumes "affine ((λx. a + x) ` S)" shows "affine S" proof - { fix x y u v assume xy: "x ∈ S" "y ∈ S" "(u :: real) + v = 1" then have "(a + x) ∈ ((λx. a + x) ` S)" "(a + y) ∈ ((λx. a + x) ` S)" by auto then have h1: "u *⇩_{R}(a + x) + v *⇩_{R}(a + y) ∈ (λx. a + x) ` S" using xy assms unfolding affine_def by auto have "u *⇩_{R}(a + x) + v *⇩_{R}(a + y) = (u + v) *⇩_{R}a + (u *⇩_{R}x + v *⇩_{R}y)" by (simp add: algebra_simps) also have "… = a + (u *⇩_{R}x + v *⇩_{R}y)" using ‹u + v = 1› by auto ultimately have "a + (u *⇩_{R}x + v *⇩_{R}y) ∈ (λx. a + x) ` S" using h1 by auto then have "u *⇩_{R}x + v *⇩_{R}y ∈ S" by auto } then show ?thesis unfolding affine_def by auto qed lemma affine_translation: fixes a :: "'a::real_vector" shows "affine S ⟷ affine ((λx. a + x) ` S)" proof - have "affine S ⟹ affine ((λx. a + x) ` S)" using affine_translation_aux[of "-a" "((λx. a + x) ` S)"] using translation_assoc[of "-a" a S] by auto then show ?thesis using affine_translation_aux by auto qed lemma parallel_is_affine: fixes S T :: "'a::real_vector set" assumes "affine S" "affine_parallel S T" shows "affine T" proof - from assms obtain a where "T = (λx. a + x) ` S" unfolding affine_parallel_def by auto then show ?thesis using affine_translation assms by auto qed lemma subspace_imp_affine: "subspace s ⟹ affine s" unfolding subspace_def affine_def by auto subsubsection%unimportant ‹Subspace parallel to an affine set› lemma subspace_affine: "subspace S ⟷ affine S ∧ 0 ∈ S" proof - have h0: "subspace S ⟹ affine S ∧ 0 ∈ S" using subspace_imp_affine[of S] subspace_0 by auto { assume assm: "affine S ∧ 0 ∈ S" { fix c :: real fix x assume x: "x ∈ S" have "c *⇩_{R}x = (1-c) *⇩_{R}0 + c *⇩_{R}x" by auto moreover have "(1 - c) *⇩_{R}0 + c *⇩_{R}x ∈ S" using affine_alt[of S] assm x by auto ultimately have "c *⇩_{R}x ∈ S" by auto } then have h1: "∀c. ∀x ∈ S. c *⇩_{R}x ∈ S" by auto { fix x y assume xy: "x ∈ S" "y ∈ S" define u where "u = (1 :: real)/2" have "(1/2) *⇩_{R}(x+y) = (1/2) *⇩_{R}(x+y)" by auto moreover have "(1/2) *⇩_{R}(x+y)=(1/2) *⇩_{R}x + (1-(1/2)) *⇩_{R}y" by (simp add: algebra_simps) moreover have "(1 - u) *⇩_{R}x + u *⇩_{R}y ∈ S" using affine_alt[of S] assm xy by auto ultimately have "(1/2) *⇩_{R}(x+y) ∈ S" using u_def by auto moreover have "x + y = 2 *⇩_{R}((1/2) *⇩_{R}(x+y))" by auto ultimately have "x + y ∈ S" using h1[rule_format, of "(1/2) *⇩_{R}(x+y)" "2"] by auto } then have "∀x ∈ S. ∀y ∈ S. x + y ∈ S" by auto then have "subspace S" using h1 assm unfolding subspace_def by auto } then show ?thesis using h0 by metis qed lemma affine_diffs_subspace: assumes "affine S" "a ∈ S" shows "subspace ((λx. (-a)+x) ` S)" proof - have [simp]: "(λx. x - a) = plus (- a)" by (simp add: fun_eq_iff) have "affine ((λx. (-a)+x) ` S)" using affine_translation assms by auto moreover have "0 ∈ ((λx. (-a)+x) ` S)" using assms exI[of "(λx. x∈S ∧ -a+x = 0)" a] by auto ultimately show ?thesis using subspace_affine by auto qed lemma parallel_subspace_explicit: assumes "affine S" and "a ∈ S" assumes "L ≡ {y. ∃x ∈ S. (-a) + x = y}" shows "subspace L ∧ affine_parallel S L" proof - from assms have "L = plus (- a) ` S" by auto then have par: "affine_parallel S L" unfolding affine_parallel_def .. then have "affine L" using assms parallel_is_affine by auto moreover have "0 ∈ L" using assms by auto ultimately show ?thesis using subspace_affine par by auto qed lemma parallel_subspace_aux: assumes "subspace A" and "subspace B" and "affine_parallel A B" shows "A ⊇ B" proof - from assms obtain a where a: "∀x. x ∈ A ⟷ a + x ∈ B" using affine_parallel_expl[of A B] by auto then have "-a ∈ A" using assms subspace_0[of B] by auto then have "a ∈ A" using assms subspace_neg[of A "-a"] by auto then show ?thesis using assms a unfolding subspace_def by auto qed lemma parallel_subspace: assumes "subspace A" and "subspace B" and "affine_parallel A B" shows "A = B" proof show "A ⊇ B" using assms parallel_subspace_aux by auto show "A ⊆ B" using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto qed lemma affine_parallel_subspace: assumes "affine S" "S ≠ {}" shows "∃!L. subspace L ∧ affine_parallel S L" proof - have ex: "∃L. subspace L ∧ affine_parallel S L" using assms parallel_subspace_explicit by auto { fix L1 L2 assume ass: "subspace L1 ∧ affine_parallel S L1" "subspace L2 ∧ affine_parallel S L2" then have "affine_parallel L1 L2" using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto then have "L1 = L2" using ass parallel_subspace by auto } then show ?thesis using ex by auto qed subsection ‹Cones› definition%important cone :: "'a::real_vector set ⇒ bool" where "cone s ⟷ (∀x∈s. ∀c≥0. c *⇩_{R}x ∈ s)" lemma cone_empty[intro, simp]: "cone {}" unfolding cone_def by auto lemma cone_univ[intro, simp]: "cone UNIV" unfolding cone_def by auto lemma cone_Inter[intro]: "∀s∈f. cone s ⟹ cone (⋂f)" unfolding cone_def by auto lemma subspace_imp_cone: "subspace S ⟹ cone S" by (simp add: cone_def subspace_scale) subsubsection ‹Conic hull› lemma cone_cone_hull: "cone (cone hull s)" unfolding hull_def by auto lemma cone_hull_eq: "cone hull s = s ⟷ cone s" apply (rule hull_eq) using cone_Inter unfolding subset_eq apply auto done lemma mem_cone: assumes "cone S" "x ∈ S" "c ≥ 0" shows "c *⇩_{R}x ∈ S" using assms cone_def[of S] by auto lemma cone_contains_0: assumes "cone S" shows "S ≠ {} ⟷ 0 ∈ S" proof - { assume "S ≠ {}" then obtain a where "a ∈ S" by auto then have "0 ∈ S" using assms mem_cone[of S a 0] by auto } then show ?thesis by auto qed lemma cone_0: "cone {0}" unfolding cone_def by auto lemma cone_Union[intro]: "(∀s∈f. cone s) ⟶ cone (⋃f)" unfolding cone_def by blast lemma cone_iff: assumes "S ≠ {}" shows "cone S ⟷ 0 ∈ S ∧ (∀c. c > 0 ⟶ (( *⇩_{R}) c) ` S = S)" proof - { assume "cone S" { fix c :: real assume "c > 0" { fix x assume "x ∈ S" then have "x ∈ (( *⇩_{R}) c) ` S" unfolding image_def using ‹cone S› ‹c>0› mem_cone[of S x "1/c"] exI[of "(λt. t ∈ S ∧ x = c *⇩_{R}t)" "(1 / c) *⇩_{R}x"] by auto } moreover { fix x assume "x ∈ (( *⇩_{R}) c) ` S" then have "x ∈ S" using ‹cone S› ‹c > 0› unfolding cone_def image_def ‹c > 0› by auto } ultimately have "(( *⇩_{R}) c) ` S = S" by auto } then have "0 ∈ S ∧ (∀c. c > 0 ⟶ (( *⇩_{R}) c) ` S = S)" using ‹cone S› cone_contains_0[of S] assms by auto } moreover { assume a: "0 ∈ S ∧ (∀c. c > 0 ⟶ (( *⇩_{R}) c) ` S = S)" { fix x assume "x ∈ S" fix c1 :: real assume "c1 ≥ 0" then have "c1 = 0 ∨ c1 > 0" by auto then have "c1 *⇩_{R}x ∈ S" using a ‹x ∈ S› by auto } then have "cone S" unfolding cone_def by auto } ultimately show ?thesis by blast qed lemma cone_hull_empty: "cone hull {} = {}" by (metis cone_empty cone_hull_eq) lemma cone_hull_empty_iff: "S = {} ⟷ cone hull S = {}" by (metis bot_least cone_hull_empty hull_subset xtrans(5)) lemma cone_hull_contains_0: "S ≠ {} ⟷ 0 ∈ cone hull S" using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S] by auto lemma mem_cone_hull: assumes "x ∈ S" "c ≥ 0" shows "c *⇩_{R}x ∈ cone hull S" by (metis assms cone_cone_hull hull_inc mem_cone) proposition cone_hull_expl: "cone hull S = {c *⇩_{R}x | c x. c ≥ 0 ∧ x ∈ S}" (is "?lhs = ?rhs") proof - { fix x assume "x ∈ ?rhs" then obtain cx :: real and xx where x: "x = cx *⇩_{R}xx" "cx ≥ 0" "xx ∈ S" by auto fix c :: real assume c: "c ≥ 0" then have "c *⇩_{R}x = (c * cx) *⇩_{R}xx" using x by (simp add: algebra_simps) moreover have "c * cx ≥ 0" using c x by auto ultimately have "c *⇩_{R}x ∈ ?rhs" using x by auto } then have "cone ?rhs" unfolding cone_def by auto then have "?rhs ∈ Collect cone" unfolding mem_Collect_eq by auto { fix x assume "x ∈ S" then have "1 *⇩_{R}x ∈ ?rhs" apply auto apply (rule_tac x = 1 in exI, auto) done then have "x ∈ ?rhs" by auto } then have "S ⊆ ?rhs" by auto then have "?lhs ⊆ ?rhs" using ‹?rhs ∈ Collect cone› hull_minimal[of S "?rhs" "cone"] by auto moreover { fix x assume "x ∈ ?rhs" then obtain cx :: real and xx where x: "x = cx *⇩_{R}xx" "cx ≥ 0" "xx ∈ S" by auto then have "xx ∈ cone hull S" using hull_subset[of S] by auto then have "x ∈ ?lhs" using x cone_cone_hull[of S] cone_def[of "cone hull S"] by auto } ultimately show ?thesis by auto qed lemma cone_closure: fixes S :: "'a::real_normed_vector set" assumes "cone S" shows "cone (closure S)" proof (cases "S = {}") case True then show ?thesis by auto next case False then have "0 ∈ S ∧ (∀c. c > 0 ⟶ ( *⇩_{R}) c ` S = S)" using cone_iff[of S] assms by auto then have "0 ∈ closure S ∧ (∀c. c > 0 ⟶ ( *⇩_{R}) c ` closure S = closure S)" using closure_subset by (auto simp: closure_scaleR) then show ?thesis using False cone_iff[of "closure S"] by auto qed subsection ‹Affine dependence and consequential theorems (from Lars Schewe)› definition%important affine_dependent :: "'a::real_vector set ⇒ bool" where "affine_dependent s ⟷ (∃x∈s. x ∈ affine hull (s - {x}))" lemma affine_dependent_subset: "⟦affine_dependent s; s ⊆ t⟧ ⟹ affine_dependent t" apply (simp add: affine_dependent_def Bex_def) apply (blast dest: hull_mono [OF Diff_mono [OF _ subset_refl]]) done lemma affine_independent_subset: shows "⟦~ affine_dependent t; s ⊆ t⟧ ⟹ ~ affine_dependent s" by (metis affine_dependent_subset) lemma affine_independent_Diff: "~ affine_dependent s ⟹ ~ affine_dependent(s - t)" by (meson Diff_subset affine_dependent_subset) proposition affine_dependent_explicit: "affine_dependent p ⟷ (∃S u. finite S ∧ S ⊆ p ∧ sum u S = 0 ∧ (∃v∈S. u v ≠ 0) ∧ sum (λv. u v *⇩_{R}v) S = 0)" proof - have "∃S u. finite S ∧ S ⊆ p ∧ sum u S = 0 ∧ (∃v∈S. u v ≠ 0) ∧ (∑w∈S. u w *⇩_{R}w) = 0" if "(∑w∈S. u w *⇩_{R}w) = x" "x ∈ p" "finite S" "S ≠ {}" "S ⊆ p - {x}" "sum u S = 1" for x S u proof (intro exI conjI) have "x ∉ S" using that by auto then show "(∑v ∈ insert x S. if v = x then - 1 else u v) = 0" using that by (simp add: sum_delta_notmem) show "(∑w ∈ insert x S. (if w = x then - 1 else u w) *⇩_{R}w) = 0" using that ‹x ∉ S› by (simp add: if_smult sum_delta_notmem cong: if_cong) qed (use that in auto) moreover have "∃x∈p. ∃S u. finite S ∧ S ≠ {} ∧ S ⊆ p - {x} ∧ sum u S = 1 ∧ (∑v∈S. u v *⇩_{R}v) = x" if "(∑v∈S. u v *⇩_{R}v) = 0" "finite S" "S ⊆ p" "sum u S = 0" "v ∈ S" "u v ≠ 0" for S u v proof (intro bexI exI conjI) have "S ≠ {v}" using that by auto then show "S - {v} ≠ {}" using that by auto show "(∑x ∈ S - {v}. - (1 / u v) * u x) = 1" unfolding sum_distrib_left[symmetric] sum_diff1[OF ‹finite S›] by (simp add: that) show "(∑x∈S - {v}. (- (1 / u v) * u x) *⇩_{R}x) = v" unfolding sum_distrib_left [symmetric] scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] sum_diff1[OF ‹finite S›] using that by auto show "S - {v} ⊆ p - {v}" using that by auto qed (use that in auto) ultimately show ?thesis unfolding affine_dependent_def affine_hull_explicit by auto qed lemma affine_dependent_explicit_finite: fixes S :: "'a::real_vector set" assumes "finite S" shows "affine_dependent S ⟷ (∃u. sum u S = 0 ∧ (∃v∈S. u v ≠ 0) ∧ sum (λv. u v *⇩_{R}v) S = 0)" (is "?lhs = ?rhs") proof have *: "⋀vt u v. (if vt then u v else 0) *⇩_{R}v = (if vt then (u v) *⇩_{R}v else 0::'a)" by auto assume ?lhs then obtain t u v where "finite t" "t ⊆ S" "sum u t = 0" "v∈t" "u v ≠ 0" "(∑v∈t. u v *⇩_{R}v) = 0" unfolding affine_dependent_explicit by auto then show ?rhs apply (rule_tac x="λx. if x∈t then u x else 0" in exI) apply (auto simp: * sum.inter_restrict[OF assms, symmetric] Int_absorb1[OF ‹t⊆S›]) done next assume ?rhs then obtain u v where "sum u S = 0" "v∈S" "u v ≠ 0" "(∑v∈S. u v *⇩_{R}v) = 0" by auto then show ?lhs unfolding affine_dependent_explicit using assms by auto qed subsection%unimportant ‹Connectedness of convex sets› lemma connectedD: "connected S ⟹ open A ⟹ open B ⟹ S ⊆ A ∪ B ⟹ A ∩ B ∩ S = {} ⟹ A ∩ S = {} ∨ B ∩ S = {}" by (rule Topological_Spaces.topological_space_class.connectedD) lemma convex_connected: fixes S :: "'a::real_normed_vector set" assumes "convex S" shows "connected S" proof (rule connectedI) fix A B assume "open A" "open B" "A ∩ B ∩ S = {}" "S ⊆ A ∪ B" moreover assume "A ∩ S ≠ {}" "B ∩ S ≠ {}" then obtain a b where a: "a ∈ A" "a ∈ S" and b: "b ∈ B" "b ∈ S" by auto define f where [abs_def]: "f u = u *⇩_{R}a + (1 - u) *⇩_{R}b" for u then have "continuous_on {0 .. 1} f" by (auto intro!: continuous_intros) then have "connected (f ` {0 .. 1})" by (auto intro!: connected_continuous_image) note connectedD[OF this, of A B] moreover have "a ∈ A ∩ f ` {0 .. 1}" using a by (auto intro!: image_eqI[of _ _ 1] simp: f_def) moreover have "b ∈ B ∩ f ` {0 .. 1}" using b by (auto intro!: image_eqI[of _ _ 0] simp: f_def) moreover have "f ` {0 .. 1} ⊆ S" using ‹convex S› a b unfolding convex_def f_def by auto ultimately show False by auto qed corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)" by (simp add: convex_connected) corollary component_complement_connected: fixes S :: "'a::real_normed_vector set" assumes "connected S" "C ∈ components (-S)" shows "connected(-C)" using component_diff_connected [of S UNIV] assms by (auto simp: Compl_eq_Diff_UNIV) proposition clopen: fixes S :: "'a :: real_normed_vector set" shows "closed S ∧ open S ⟷ S = {} ∨ S = UNIV" by (force intro!: connected_UNIV [unfolded connected_clopen, rule_format]) corollary compact_open: fixes S :: "'a :: euclidean_space set" shows "compact S ∧ open S ⟷ S = {}" by (auto simp: compact_eq_bounded_closed clopen) corollary finite_imp_not_open: fixes S :: "'a::{real_normed_vector, perfect_space} set" shows "⟦finite S; open S⟧ ⟹ S={}" using clopen [of S] finite_imp_closed not_bounded_UNIV by blast corollary empty_interior_finite: fixes S :: "'a::{real_normed_vector, perfect_space} set" shows "finite S ⟹ interior S = {}" by (metis interior_subset finite_subset open_interior [of S] finite_imp_not_open) text ‹Balls, being convex, are connected.› lemma convex_prod: assumes "⋀i. i ∈ Basis ⟹ convex {x. P i x}" shows "convex {x. ∀i∈Basis. P i (x∙i)}" using assms unfolding convex_def by (auto simp: inner_add_left) lemma convex_positive_orthant: "convex {x::'a::euclidean_space. (∀i∈Basis. 0 ≤ x∙i)}" by (rule convex_prod) (simp add: atLeast_def[symmetric] convex_real_interval) lemma convex_local_global_minimum: fixes s :: "'a::real_normed_vector set" assumes "e > 0" and "convex_on s f" and "ball x e ⊆ s" and "∀y∈ball x e. f x ≤ f y" shows "∀y∈s. f x ≤ f y" proof (rule ccontr) have "x ∈ s" using assms(1,3) by auto assume "¬ ?thesis" then obtain y where "y∈s" and y: "f x > f y" by auto then have xy: "0 < dist x y" by auto then obtain u where "0 < u" "u ≤ 1" and u: "u < e / dist x y" using field_lbound_gt_zero[of 1 "e / dist x y"] xy ‹e>0› by auto then have "f ((1-u) *⇩_{R}x + u *⇩_{R}y) ≤ (1-u) * f x + u * f y" using ‹x∈s› ‹y∈s› using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto moreover have *: "x - ((1 - u) *⇩_{R}x + u *⇩_{R}y) = u *⇩_{R}(x - y)" by (simp add: algebra_simps) have "(1 - u) *⇩_{R}x + u *⇩_{R}y ∈ ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF ‹0<u›] unfolding dist_norm[symmetric] using u unfolding pos_less_divide_eq[OF xy] by auto then have "f x ≤ f ((1 - u) *⇩_{R}x + u *⇩_{R}y)" using assms(4) by auto ultimately show False using mult_strict_left_mono[OF y ‹u>0›] unfolding left_diff_distrib by auto qed lemma convex_ball [iff]: fixes x :: "'a::real_normed_vector" shows "convex (ball x e)" proof (auto simp: convex_def) fix y z assume yz: "dist x y < e" "dist x z < e" fix u v :: real assume uv: "0 ≤ u" "0 ≤ v" "u + v = 1" have "dist x (u *⇩_{R}y + v *⇩_{R}z) ≤ u * dist x y + v * dist x z" using uv yz using convex_on_dist [of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto then show "dist x (u *⇩_{R}y + v *⇩_{R}z) < e" using convex_bound_lt[OF yz uv] by auto qed lemma convex_cball [iff]: fixes x :: "'a::real_normed_vector" shows "convex (cball x e)" proof - { fix y z assume yz: "dist x y ≤ e" "dist x z ≤ e" fix u v :: real assume uv: "0 ≤ u" "0 ≤ v" "u + v = 1" have "dist x (u *⇩_{R}y + v *⇩_{R}z) ≤ u * dist x y + v * dist x z" using uv yz using convex_on_dist [of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto then have "dist x (u *⇩_{R}y + v *⇩_{R}z) ≤ e" using convex_bound_le[OF yz uv] by auto } then show ?thesis by (auto simp: convex_def Ball_def) qed lemma connected_ball [iff]: fixes x :: "'a::real_normed_vector" shows "connected (ball x e)" using convex_connected convex_ball by auto lemma connected_cball [iff]: fixes x :: "'a::real_normed_vector" shows "connected (cball x e)" using convex_connected convex_cball by auto subsection ‹Convex hull› lemma convex_convex_hull [iff]: "convex (convex hull s)" unfolding hull_def using convex_Inter[of "{t. convex t ∧ s ⊆ t}"] by auto lemma convex_hull_subset: "s ⊆ convex hull t ⟹ convex hull s ⊆ convex hull t" by (simp add: convex_convex_hull subset_hull) lemma convex_hull_eq: "convex hull s = s ⟷ convex s" by (metis convex_convex_hull hull_same) lemma bounded_convex_hull: fixes s :: "'a::real_normed_vector set" assumes "bounded s" shows "bounded (convex hull s)" proof - from assms obtain B where B: "∀x∈s. norm x ≤ B" unfolding bounded_iff by auto show ?thesis apply (rule bounded_subset[OF bounded_cball, of _ 0 B]) unfolding subset_hull[of convex, OF convex_cball] unfolding subset_eq mem_cball dist_norm using B apply auto done qed lemma finite_imp_bounded_convex_hull: fixes s :: "'a::real_normed_vector set" shows "finite s ⟹ bounded (convex hull s)" using bounded_convex_hull finite_imp_bounded by auto subsubsection%unimportant ‹Convex hull is "preserved" by a linear function› lemma convex_hull_linear_image: assumes f: "linear f" shows "f ` (convex hull s) = convex hull (f ` s)" proof show "convex hull (f ` s) ⊆ f ` (convex hull s)" by (intro hull_minimal image_mono hull_subset convex_linear_image assms convex_convex_hull) show "f ` (convex hull s) ⊆ convex hull (f ` s)" proof (unfold image_subset_iff_subset_vimage, rule hull_minimal) show "s ⊆ f -` (convex hull (f ` s))" by (fast intro: hull_inc) show "convex (f -` (convex hull (f ` s)))" by (intro convex_linear_vimage [OF f] convex_convex_hull) qed qed lemma in_convex_hull_linear_image: assumes "linear f" and "x ∈ convex hull s" shows "f x ∈ convex hull (f ` s)" using convex_hull_linear_image[OF assms(1)] assms(2) by auto lemma convex_hull_Times: "convex hull (s × t) = (convex hull s) × (convex hull t)" proof show "convex hull (s × t) ⊆ (convex hull s) × (convex hull t)" by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull) have "(x, y) ∈ convex hull (s × t)" if x: "x ∈ convex hull s" and y: "y ∈ convex hull t" for x y proof (rule hull_induct [OF x], rule hull_induct [OF y]) fix x y assume "x ∈ s" and "y ∈ t" then show "(x, y) ∈ convex hull (s × t)" by (simp add: hull_inc) next fix x let ?S = "((λy. (0, y)) -` (λp. (- x, 0) + p) ` (convex hull s × t))" have "convex ?S" by (intro convex_linear_vimage convex_translation convex_convex_hull, simp add: linear_iff) also have "?S = {y. (x, y) ∈ convex hull (s × t)}" by (auto simp: image_def Bex_def) finally show "convex {y. (x, y) ∈ convex hull (s × t)}" . next show "convex {x. (x, y) ∈ convex hull s × t}" proof - fix y let ?S = "((λx. (x, 0)) -` (λp. (0, - y) + p) ` (convex hull s × t))" have "convex ?S" by (intro convex_linear_vimage convex_translation convex_convex_hull, simp add: linear_iff) also have "?S = {x. (x, y) ∈ convex hull (s × t)}" by (auto simp: image_def Bex_def) finally show "convex {x. (x, y) ∈ convex hull (s × t)}" . qed qed then show "(convex hull s) × (convex hull t) ⊆ convex hull (s × t)" unfolding subset_eq split_paired_Ball_Sigma by blast qed subsubsection%unimportant ‹Stepping theorems for convex hulls of finite sets› lemma convex_hull_empty[simp]: "convex hull {} = {}" by (rule hull_unique) auto lemma convex_hull_singleton[simp]: "convex hull {a} = {a}" by (rule hull_unique) auto lemma convex_hull_insert: fixes S :: "'a::real_vector set" assumes "S ≠ {}" shows "convex hull (insert a S) = {x. ∃u≥0. ∃v≥0. ∃b. (u + v = 1) ∧ b ∈ (convex hull S) ∧ (x = u *⇩_{R}a + v *⇩_{R}b)}" (is "_ = ?hull") proof (intro equalityI hull_minimal subsetI) fix x assume "x ∈ insert a S" then have "∃u≥0. ∃v≥0. u + v = 1 ∧ (∃b. b ∈ convex hull S ∧ x = u *⇩_{R}a + v *⇩_{R}b)" unfolding insert_iff proof assume "x = a" then show ?thesis by (rule_tac x=1 in exI) (use assms hull_subset in fastforce) next assume "x ∈ S" with hull_subset[of S convex] show ?thesis by force qed then show "x ∈ ?hull" by simp next fix x assume "x ∈ ?hull" then obtain u v b where obt: "u≥0" "v≥0" "u + v = 1" "b ∈ convex hull S" "x = u *⇩_{R}a + v *⇩_{R}b" by auto have "a ∈ convex hull insert a S" "b ∈ convex hull insert a S" using hull_mono[of S "insert a S" convex] hull_mono[of "{a}" "insert a S" convex] and obt(4) by auto then show "x ∈ convex hull insert a S" unfolding obt(5) using obt(1-3) by (rule convexD [OF convex_convex_hull]) next show "convex ?hull" proof (rule convexI) fix x y u v assume as: "(0::real) ≤ u" "0 ≤ v" "u + v = 1" and x: "x ∈ ?hull" and y: "y ∈ ?hull" from x obtain u1 v1 b1 where obt1: "u1≥0" "v1≥0" "u1 + v1 = 1" "b1 ∈ convex hull S" and xeq: "x = u1 *⇩_{R}a + v1 *⇩_{R}b1" by auto from y obtain u2 v2 b2 where obt2: "u2≥0" "v2≥0" "u2 + v2 = 1" "b2 ∈ convex hull S" and yeq: "y = u2 *⇩_{R}a + v2 *⇩_{R}b2" by auto have *: "⋀(x::'a) s1 s2. x - s1 *⇩_{R}x - s2 *⇩_{R}x = ((1::real) - (s1 + s2)) *⇩_{R}x" by (auto simp: algebra_simps) have "∃b ∈ convex hull S. u *⇩_{R}x + v *⇩_{R}y = (u * u1) *⇩_{R}a + (v * u2) *⇩_{R}a + (b - (u * u1) *⇩_{R}b - (v * u2) *⇩_{R}b)" proof (cases "u * v1 + v * v2 = 0") case True have *: "⋀(x::'a) s1 s2. x - s1 *⇩_{R}x - s2 *⇩_{R}x = ((1::real) - (s1 + s2)) *⇩_{R}x" by (auto simp: algebra_simps) have eq0: "u * v1 = 0" "v * v2 = 0" using True mult_nonneg_nonneg[OF ‹u≥0› ‹v1≥0›] mult_nonneg_nonneg[OF ‹v≥0› ‹v2≥0›] by arith+ then have "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto then show ?thesis using "*" eq0 as obt1(4) xeq yeq by auto next case False have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" using as(3) obt1(3) obt2(3) by (auto simp: field_simps) also have "… = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp: field_simps) also have "… = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto let ?b = "((u * v1) / (u * v1 + v * v2)) *⇩_{R}b1 + ((v * v2) / (u * v1 + v * v2)) *⇩_{R}b2" have zeroes: "0 ≤ u * v1 + v * v2" "0 ≤ u * v1" "0 ≤ u * v1 + v * v2" "0 ≤ v * v2" using as(1,2) obt1(1,2) obt2(1,2) by auto show ?thesis proof show "u *⇩_{R}x + v *⇩_{R}y = (u * u1) *⇩_{R}a + (v * u2) *⇩_{R}a + (?b - (u * u1) *⇩_{R}?b - (v * u2) *⇩_{R}?b)" unfolding xeq yeq * ** using False by (auto simp: scaleR_left_distrib scaleR_right_distrib) show "?b ∈ convex hull S" using False zeroes obt1(4) obt2(4) by (auto simp: convexD [OF convex_convex_hull] scaleR_left_distrib scaleR_right_distrib add_divide_distrib[symmetric] zero_le_divide_iff) qed qed then obtain b where b: "b ∈ convex hull S" "u *⇩_{R}x + v *⇩_{R}y = (u * u1) *⇩_{R}a + (v * u2) *⇩_{R}a + (b - (u * u1) *⇩_{R}b - (v * u2) *⇩_{R}b)" .. have u1: "u1 ≤ 1" unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto have u2: "u2 ≤ 1" unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto have "u1 * u + u2 * v ≤ max u1 u2 * u + max u1 u2 * v" proof (rule add_mono) show "u1 * u ≤ max u1 u2 * u" "u2 * v ≤ max u1 u2 * v" by (simp_all add: as mult_right_mono) qed also have "… ≤ 1" unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto finally have le1: "u1 * u + u2 * v ≤ 1" . show "u *⇩_{R}x + v *⇩_{R}y ∈ ?hull" proof (intro CollectI exI conjI) show "0 ≤ u * u1 + v * u2" by (simp add: as(1) as(2) obt1(1) obt2(1)) show "0 ≤ 1 - u * u1 - v * u2" by (simp add: le1 diff_diff_add mult.commute) qed (use b in ‹auto simp: algebra_simps›) qed qed lemma convex_hull_insert_alt: "convex hull (insert a S) = (if S = {} then {a} else {(1 - u) *⇩_{R}a + u *⇩_{R}x |x u. 0 ≤ u ∧ u ≤ 1 ∧ x ∈ convex hull S})" apply (auto simp: convex_hull_insert) using diff_eq_eq apply fastforce by (metis add.group_left_neutral add_le_imp_le_diff diff_add_cancel) subsubsection%unimportant ‹Explicit expression for convex hull› proposition convex_hull_indexed: fixes S :: "'a::real_vector set" shows "convex hull S = {y. ∃k u x. (∀i∈{1::nat .. k}. 0 ≤ u i ∧ x i ∈ S) ∧ (sum u {1..k} = 1) ∧ (∑i = 1..k. u i *⇩_{R}x i) = y}" (is "?xyz = ?hull") proof (rule hull_unique [OF _ convexI]) show "S ⊆ ?hull" by (clarsimp, rule_tac x=1 in exI, rule_tac x="λx. 1" in exI, auto) next fix T assume "S ⊆ T" "convex T" then show "?hull ⊆ T" by (blast intro: convex_sum) next fix x y u v assume uv: "0 ≤ u" "0 ≤ v" "u + v = (1::real)" assume xy: "x ∈ ?hull" "y ∈ ?hull" from xy obtain k1 u1 x1 where x [rule_format]: "∀i∈{1::nat..k1}. 0≤u1 i ∧ x1 i ∈ S" "sum u1 {Suc 0..k1} = 1" "(∑i = Suc 0..k1. u1 i *⇩_{R}x1 i) = x" by auto from xy obtain k2 u2 x2 where y [rule_format]: "∀i∈{1::nat..k2}. 0≤u2 i ∧ x2 i ∈ S" "sum u2 {Suc 0..k2} = 1" "(∑i = Suc 0..k2. u2 i *⇩_{R}x2 i) = y" by auto have *: "⋀P (x::'a) y s t i. (if P i then s else t) *⇩_{R}(if P i then x else y) = (if P i then s *⇩_{R}x else t *⇩_{R}y)" "{1..k1 + k2} ∩ {1..k1} = {1..k1}" "{1..k1 + k2} ∩ - {1..k1} = (λi. i + k1) ` {1..k2}" by auto have inj: "inj_on (λi. i + k1) {1..k2}" unfolding inj_on_def by auto let ?uu = "λi. if i ∈ {1..k1} then u * u1 i else v * u2 (i - k1)" let ?xx = "λi. if i ∈ {1..k1} then x1 i else x2 (i - k1)" show "u *⇩_{R}x + v *⇩_{R}y ∈ ?hull" proof (intro CollectI exI conjI ballI) show "0 ≤ ?uu i" "?xx i ∈ S" if "i ∈ {1..k1+k2}" for i using that by (auto simp add: le_diff_conv uv(1) x(1) uv(2) y(1)) show "(∑i = 1..k1 + k2. ?uu i) = 1" "(∑i = 1..k1 + k2. ?uu i *⇩_{R}?xx i) = u *⇩_{R}x + v *⇩_{R}y" unfolding * sum.If_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] sum.reindex[OF inj] Collect_mem_eq o_def unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] sum_distrib_left[symmetric] by (simp_all add: sum_distrib_left[symmetric] x(2,3) y(2,3) uv(3)) qed qed lemma convex_hull_finite: fixes S :: "'a::real_vector set" assumes "finite S" shows "convex hull S = {y. ∃u. (∀x∈S. 0 ≤ u x) ∧ sum u S = 1 ∧ sum (λx. u x *⇩_{R}x) S = y}" (is "?HULL = _") proof (rule hull_unique [OF _ convexI]; clarify) fix x assume "x ∈ S" then show "∃u. (∀x∈S. 0 ≤ u x) ∧ sum u S = 1 ∧ (∑x∈S. u x *⇩_{R}x) = x" by (rule_tac x="λy. if x=y then 1 else 0" in exI) (auto simp: sum.delta'[OF assms] sum_delta''[OF assms]) next fix u v :: real assume uv: "0 ≤ u" "0 ≤ v" "u + v = 1" fix ux assume ux [rule_format]: "∀x∈S. 0 ≤ ux x" "sum ux S = (1::real)" fix uy assume uy [rule_format]: "∀x∈S. 0 ≤ uy x" "sum uy S = (1::real)" have "0 ≤ u * ux x + v * uy x" if "x∈S" for x by (simp add: that uv ux(1) uy(1)) moreover have "(∑x∈S. u * ux x + v * uy x) = 1" unfolding sum.distrib and sum_distrib_left[symmetric] ux(2) uy(2) using uv(3) by auto moreover have "(∑x∈S. (u * ux x + v * uy x) *⇩_{R}x) = u *⇩_{R}(∑x∈S. ux x *⇩_{R}x) + v *⇩_{R}(∑x∈S. uy x *⇩_{R}x)" unfolding scaleR_left_distrib sum.distrib scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] by auto ultimately show "∃uc. (∀x∈S. 0 ≤ uc x) ∧ sum uc S = 1 ∧ (∑x∈S. uc x *⇩_{R}x) = u *⇩_{R}(∑x∈S. ux x *⇩_{R}x) + v *⇩_{R}(∑x∈S. uy x *⇩_{R}x)" by (rule_tac x="λx. u * ux x + v * uy x" in exI, auto) qed (use assms in ‹auto simp: convex_explicit›) subsubsection%unimportant ‹Another formulation from Lars Schewe› lemma convex_hull_explicit: fixes p :: "'a::real_vector set" shows "convex hull p = {y. ∃S u. finite S ∧ S ⊆ p ∧ (∀x∈S. 0 ≤ u x) ∧ sum u S = 1 ∧ sum (λv. u v *⇩_{R}v) S = y}" (is "?lhs = ?rhs") proof - { fix x assume "x∈?lhs" then obtain k u y where obt: "∀i∈{1::nat..k}. 0 ≤ u i ∧ y i ∈ p" "sum u {1..k} = 1" "(∑i = 1..k. u i *⇩_{R}y i) = x" unfolding convex_hull_indexed by auto have fin: "finite {1..k}" by auto have fin': "⋀v. finite {i ∈ {1..k}. y i = v}" by auto { fix j assume "j∈{1..k}" then have "y j ∈ p" "0 ≤ sum u {i. Suc 0 ≤ i ∧ i ≤ k ∧ y i = y j}" using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp apply (rule sum_nonneg) using obt(1) apply auto done } moreover have "(∑v∈y ` {1..k}. sum u {i ∈ {1..k}. y i = v}) = 1" unfolding sum_image_gen[OF fin, symmetric] using obt(2) by auto moreover have "(∑v∈y ` {1..k}. sum u {i ∈ {1..k}. y i = v} *⇩_{R}v) = x" using sum_image_gen[OF fin, of "λi. u i *⇩_{R}y i" y, symmetric] unfolding scaleR_left.sum using obt(3) by auto ultimately have "∃S u. finite S ∧ S ⊆ p ∧ (∀x∈S. 0 ≤ u x) ∧ sum u S = 1 ∧ (∑v∈S. u v *⇩_{R}v) = x" apply (rule_tac x="y ` {1..k}" in exI) apply (rule_tac x="λv. sum u {i∈{1..k}. y i = v}" in exI, auto) done then have "x∈?rhs" by auto } moreover { fix y assume "y∈?rhs" then obtain S u where obt: "finite S" "S ⊆ p" "∀x∈S. 0 ≤ u x" "sum u S = 1" "(∑v∈S. u v *⇩_{R}v) = y" by auto obtain f where f: "inj_on f {1..card S}" "f ` {1..card S} = S" using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto { fix i :: nat assume "i∈{1..card S}" then have "f i ∈ S" using f(2) by blast then have "0 ≤ u (f i)" "f i ∈ p" using obt(2,3) by auto } moreover have *: "finite {1..card S}" by auto { fix y assume "y∈S" then obtain i where "i∈{1..card S}" "f i = y" using f using image_iff[of y f "{1..card S}"] by auto then have "{x. Suc 0 ≤ x ∧ x ≤ card S ∧ f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] by (metis One_nat_def atLeastAtMost_iff) then have "card {x. Suc 0 ≤ x ∧ x ≤ card S ∧ f x = y} = 1" by auto then have "(∑x∈{x ∈ {1..card S}. f x = y}. u (f x)) = u y" "(∑x∈{x ∈ {1..card S}. f x = y}. u (f x) *⇩_{R}f x) = u y *⇩_{R}y" by (auto simp: sum_constant_scaleR) } then have "(∑x = 1..card S. u (f x)) = 1" "(∑i = 1..card S. u (f i) *⇩_{R}f i) = y" unfolding sum_image_gen[OF *(1), of "λx. u (f x) *⇩_{R}f x" f] and sum_image_gen[OF *(1), of "λx. u (f x)" f] unfolding f using sum.cong [of S S "λy. (∑x∈{x ∈ {1..card S}. f x = y}. u (f x) *⇩_{R}f x)" "λv. u v *⇩_{R}v"] using sum.cong [of S S "λy. (∑x∈{x ∈ {1..card S}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto ultimately have "∃k u x. (∀i∈{1..k}. 0 ≤ u i ∧ x i ∈ p) ∧ sum u {1..k} = 1 ∧ (∑i::nat = 1..k. u i *⇩_{R}x i) = y" apply (rule_tac x="card S" in exI) apply (rule_tac x="u ∘ f" in exI) apply (rule_tac x=f in exI, fastforce) done then have "y ∈ ?lhs" unfolding convex_hull_indexed by auto } ultimately show ?thesis unfolding set_eq_iff by blast qed subsubsection%unimportant ‹A stepping theorem for that expansion› lemma convex_hull_finite_step: fixes S :: "'a::real_vector set" assumes "finite S" shows "(∃u. (∀x∈insert a S. 0 ≤ u x) ∧ sum u (insert a S) = w ∧ sum (λx. u x *⇩_{R}x) (insert a S) = y) ⟷ (∃v≥0. ∃u. (∀x∈S. 0 ≤ u x) ∧ sum u S = w - v ∧ sum (λx. u x *⇩_{R}x) S = y - v *⇩_{R}a)" (is "?lhs = ?rhs") proof (rule, case_tac[!] "a∈S") assume "a ∈ S" then have *: "insert a S = S" by auto assume ?lhs then show ?rhs unfolding * by (rule_tac x=0 in exI, auto) next assume ?lhs then obtain u where u: "∀x∈insert a S. 0 ≤ u x" "sum u (insert a S) = w" "(∑x∈insert a S. u x *⇩_{R}x) = y" by auto assume "a ∉ S" then show ?rhs apply (rule_tac x="u a" in exI) using u(1)[THEN bspec[where x=a]] apply simp apply (rule_tac x=u in exI) using u[unfolded sum_clauses(2)[OF assms]] and ‹a∉S› apply auto done next assume "a ∈ S" then have *: "insert a S = S" by auto have fin: "finite (insert a S)" using assms by auto assume ?rhs then obtain v u where uv: "v≥0" "∀x∈S. 0 ≤ u x" "sum u S = w - v" "(∑x∈S. u x *⇩_{R}x) = y - v *⇩_{R}a" by auto show ?lhs apply (rule_tac x = "λx. (if a = x then v else 0) + u x" in exI) unfolding scaleR_left_distrib and sum.distrib and sum_delta''[OF fin] and sum.delta'[OF fin] unfolding sum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and ‹a∈S› apply auto done next assume ?rhs then obtain v u where uv: "v≥0" "∀x∈S. 0 ≤ u x" "sum u S = w - v" "(∑x∈S. u x *⇩_{R}x) = y - v *⇩_{R}a" by auto moreover assume "a ∉ S" moreover have "(∑x∈S. if a = x then v else u x) = sum u S" "(∑x∈S. (if a = x then v else u x) *⇩_{R}x) = (∑x∈S. u x *⇩_{R}x)" using ‹a ∉ S› by (auto simp: intro!: sum.cong) ultimately show ?lhs by (rule_tac x="λx. if a = x then v else u x" in exI) (auto simp: sum_clauses(2)[OF assms]) qed subsubsection%unimportant ‹Hence some special cases› lemma convex_hull_2: "convex hull {a,b} = {u *⇩_{R}a + v *⇩_{R}b | u v. 0 ≤ u ∧ 0 ≤ v ∧ u + v = 1}" proof - have *: "⋀u. (∀x∈{a, b}. 0 ≤ u x) ⟷ 0 ≤ u a ∧ 0 ≤ u b" by auto have **: "finite {b}" by auto show ?thesis apply (simp add: convex_hull_finite) unfolding convex_hull_finite_step[OF **, of a 1, unfolded * conj_assoc] apply auto apply (rule_tac x=v in exI) apply (rule_tac x="1 - v" in exI, simp) apply (rule_tac x=u in exI, simp) apply (rule_tac x="λx. v" in exI, simp) done qed lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *⇩_{R}(b - a) | u. 0 ≤ u ∧ u ≤ 1}" unfolding convex_hull_2 proof (rule Collect_cong) have *: "⋀x y ::real. x + y = 1 ⟷ x = 1 - y" by auto fix x show "(∃v u. x = v *⇩_{R}a + u *⇩_{R}b ∧ 0 ≤ v ∧ 0 ≤ u ∧ v + u = 1) ⟷ (∃u. x = a + u *⇩_{R}(b - a) ∧ 0 ≤ u ∧ u ≤ 1)" unfolding * apply auto apply (rule_tac[!] x=u in exI) apply (auto simp: algebra_simps) done qed lemma convex_hull_3: "convex hull {a,b,c} = { u *⇩_{R}a + v *⇩_{R}b + w *⇩_{R}c | u v w. 0 ≤ u ∧ 0 ≤ v ∧ 0 ≤ w ∧ u + v + w = 1}" proof - have fin: "finite {a,b,c}" "finite {b,c}" "finite {c}" by auto have *: "⋀x y z ::real. x + y + z = 1 ⟷ x = 1 - y - z" by (auto simp: field_simps) show ?thesis unfolding convex_hull_finite[OF fin(1)] and convex_hull_finite_step[OF fin(2)] and * unfolding convex_hull_finite_step[OF fin(3)] apply (rule Collect_cong, simp) apply auto apply (rule_tac x=va in exI) apply (rule_tac x="u c" in exI, simp) apply (rule_tac x="1 - v - w" in exI, simp) apply (rule_tac x=v in exI, simp) apply (rule_tac x="λx. w" in exI, simp) done qed lemma convex_hull_3_alt: "convex hull {a,b,c} = {a + u *⇩_{R}(b - a) + v *⇩_{R}(c - a) | u v. 0 ≤ u ∧ 0 ≤ v ∧ u + v ≤ 1}" proof - have *: "⋀x y z ::real. x + y + z = 1 ⟷ x = 1 - y - z" by auto show ?thesis unfolding convex_hull_3 apply (auto simp: *) apply (rule_tac x=v in exI) apply (rule_tac x=w in exI) apply (simp add: algebra_simps) apply (rule_tac x=u in exI) apply (rule_tac x=v in exI) apply (simp add: algebra_simps) done qed subsection%unimportant ‹Relations among closure notions and corresponding hulls› lemma affine_imp_convex: "affine s ⟹ convex s" unfolding affine_def convex_def by auto lemma convex_affine_hull [simp]: "convex (affine hull S)" by (simp add: affine_imp_convex) lemma subspace_imp_convex: "subspace s ⟹ convex s" using subspace_imp_affine affine_imp_convex by auto lemma affine_hull_subset_span: "(affine hull s) ⊆ (span s)" by (metis hull_minimal span_superset subspace_imp_affine subspace_span) lemma convex_hull_subset_span: "(convex hull s) ⊆ (span s)" by (metis hull_minimal span_superset subspace_imp_convex subspace_span) lemma convex_hull_subset_affine_hull: "(convex hull s) ⊆ (affine hull s)" by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset) lemma affine_dependent_imp_dependent: "affine_dependent s ⟹ dependent s" unfolding affine_dependent_def dependent_def using affine_hull_subset_span by auto lemma dependent_imp_affine_dependent: assumes "dependent {x - a| x . x ∈ s}" and "a ∉ s" shows "affine_dependent (insert a s)" proof - from assms(1)[unfolded dependent_explicit] obtain S u v where obt: "finite S" "S ⊆ {x - a |x. x ∈ s}" "v∈S" "u v ≠ 0" "(∑v∈S. u v *⇩_{R}v) = 0" by auto define t where "t = (λx. x + a) ` S" have inj: "inj_on (λx. x + a) S" unfolding inj_on_def by auto have "0 ∉ S" using obt(2) assms(2) unfolding subset_eq by auto have fin: "finite t" and "t ⊆ s" unfolding t_def using obt(1,2) by auto then have "finite (insert a t)" and "insert a t ⊆ insert a s" by auto moreover have *: "⋀P Q. (∑x∈t. (if x = a then P x else Q x)) = (∑x∈t. Q x)" apply (rule sum.cong) using ‹a∉s› ‹t⊆s› apply auto done have "(∑x∈insert a t. if x = a then - (∑x∈t. u (x - a)) else u (x - a)) = 0" unfolding sum_clauses(2)[OF fin] * using ‹a∉s› ‹t⊆s› by auto moreover have "∃v∈insert a t. (if v = a then - (∑x∈t. u (x - a)) else u (v - a)) ≠ 0" using obt(3,4) ‹0∉S› by (rule_tac x="v + a" in bexI) (auto simp: t_def) moreover have *: "⋀P Q. (∑x∈t. (if x = a then P x else Q x) *⇩_{R}x) = (∑x∈t. Q x *⇩_{R}x)" using ‹a∉s› ‹t⊆s› by (auto intro!: sum.cong) have "(∑x∈t. u (x - a)) *⇩_{R}a = (∑v∈t. u (v - a) *⇩_{R}v)" unfolding scaleR_left.sum unfolding t_def and sum.reindex[OF inj] and o_def using obt(5) by (auto simp: sum.distrib scaleR_right_distrib) then have "(∑v∈insert a t. (if v = a then - (∑x∈t. u (x - a)) else u (v - a)) *⇩_{R}v) = 0" unfolding sum_clauses(2)[OF fin] using ‹a∉s› ‹t⊆s› by (auto simp: *) ultimately show ?thesis unfolding affine_dependent_explicit apply (rule_tac x="insert a t" in exI, auto) done qed lemma convex_cone: "convex s ∧ cone s ⟷ (∀x∈s. ∀y∈s. (x + y) ∈ s) ∧ (∀x∈s. ∀c≥0. (c *⇩_{R}x) ∈ s)" (is "?lhs = ?rhs") proof - { fix x y assume "x∈s" "y∈s" and ?lhs then have "2 *⇩_{R}x ∈s" "2 *⇩_{R}y ∈ s" unfolding cone_def by auto then have "x + y ∈ s" using ‹?lhs›[unfolded convex_def, THEN conjunct1] apply (erule_tac x="2*⇩_{R}x" in ballE) apply (erule_tac x="2*⇩_{R}y" in ballE) apply (erule_tac x="1/2" in allE, simp) apply (erule_tac x="1/2" in allE, auto) done } then show ?thesis unfolding convex_def cone_def by blast qed lemma affine_dependent_biggerset: fixes s :: "'a::euclidean_space set" assumes "finite s" "card s ≥ DIM('a) + 2" shows "affine_dependent s" proof - have "s ≠ {}" using assms by auto then obtain a where "a∈s" by auto have *: "{x - a |x. x ∈ s - {a}} = (λx. x - a) ` (s - {a})" by auto have "card {x - a |x. x ∈ s - {a}} = card (s - {a})" unfolding * by (simp add: card_image inj_on_def) also have "… > DIM('a)" using assms(2) unfolding card_Diff_singleton[OF assms(1) ‹a∈s›] by auto finally show ?thesis apply (subst insert_Diff[OF ‹a∈s›, symmetric]) apply (rule dependent_imp_affine_dependent) apply (rule dependent_biggerset, auto) done qed lemma affine_dependent_biggerset_general: assumes "finite (S :: 'a::euclidean_space set)" and "card S ≥ dim S + 2" shows "affine_dependent S" proof - from assms(2) have "S ≠ {}" by auto then obtain a where "a∈S" by auto have *: "{x - a |x. x ∈ S - {a}} = (λx. x - a) ` (S - {a})" by auto have **: "card {x - a |x. x ∈ S - {a}} = card (S - {a})" by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def) have "dim {x - a |x. x ∈ S - {a}} ≤ dim S" using ‹a∈S› by (auto simp: span_base span_diff intro: subset_le_dim) also have "… < dim S + 1" by auto also have "… ≤ card (S - {a})" using assms using card_Diff_singleton[OF assms(1) ‹a∈S›] by auto finally show ?thesis apply (subst insert_Diff[OF ‹a∈S›, symmetric]) apply (rule dependent_imp_affine_dependent) apply (rule dependent_biggerset_general) unfolding ** apply auto done qed subsection%unimportant ‹Some Properties of Affine Dependent Sets› lemma affine_independent_0 [simp]: "¬ affine_dependent {}" by (simp add: affine_dependent_def) lemma affine_independent_1 [simp]: "¬ affine_dependent {a}" by (simp add: affine_dependent_def) lemma affine_independent_2 [simp]: "¬ affine_dependent {a,b}" by (simp add: affine_dependent_def insert_Diff_if hull_same) lemma affine_hull_translation: "affine hull ((λx. a + x) ` S) = (λx. a + x) ` (affine hull S)" proof - have "affine ((λx. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by blast moreover have "(λx. a + x) ` S ⊆ (λx. a + x) ` (affine hull S)" using hull_subset[of S] by auto ultimately have h1: "affine hull ((λx. a + x) ` S) ⊆ (λx. a + x) ` (affine hull S)" by (metis hull_minimal) have "affine((λx. -a + x) ` (affine hull ((λx. a + x) ` S)))" using affine_translation affine_affine_hull by blast moreover have "(λx. -a + x) ` (λx. a + x) ` S ⊆ (λx. -a + x) ` (affine hull ((λx. a + x) ` S))" using hull_subset[of "(λx. a + x) ` S"] by auto moreover have "S = (λx. -a + x) ` (λx. a + x) ` S" using translation_assoc[of "-a" a] by auto ultimately have "(λx. -a + x) ` (affine hull ((λx. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal) then have "affine hull ((λx. a + x) ` S) >= (λx. a + x) ` (affine hull S)" by auto then show ?thesis using h1 by auto qed lemma affine_dependent_translation: assumes "affine_dependent S" shows "affine_dependent ((λx. a + x) ` S)" proof - obtain x where x: "x ∈ S ∧ x ∈ affine hull (S - {x})" using assms affine_dependent_def by auto have "(+) a ` (S - {x}) = (+) a ` S - {a + x}" by auto then have "a + x ∈ affine hull ((λx. a + x) ` S - {a + x})" using affine_hull_translation[of a "S - {x}"] x by auto moreover have "a + x ∈ (λx. a + x) ` S" using x by auto ultimately show ?thesis unfolding affine_dependent_def by auto qed lemma affine_dependent_translation_eq: "affine_dependent S ⟷ affine_dependent ((λx. a + x) ` S)" proof - { assume "affine_dependent ((λx. a + x) ` S)" then have "affine_dependent S" using affine_dependent_translation[of "((λx. a + x) ` S)" "-a"] translation_assoc[of "-a" a] by auto } then show ?thesis using affine_dependent_translation by auto qed lemma affine_hull_0_dependent: assumes "0 ∈ affine hull S" shows "dependent S" proof - obtain s u where s_u: "finite s ∧ s ≠ {} ∧ s ⊆ S ∧ sum u s = 1 ∧ (∑v∈s. u v *⇩_{R}v) = 0" using assms affine_hull_explicit[of S] by auto then have "∃v∈s. u v ≠ 0" using sum_not_0[of "u" "s"] by auto then have "finite s ∧ s ⊆ S ∧ (∃v∈s. u v ≠ 0 ∧ (∑v∈s. u v *⇩_{R}v) = 0)" using s_u by auto then show ?thesis unfolding dependent_explicit[of S] by auto qed lemma affine_dependent_imp_dependent2: assumes "affine_dependent (insert 0 S)" shows "dependent S" proof - obtain x where x: "x ∈ insert 0 S ∧ x ∈ affine hull (insert 0 S - {x})" using affine_dependent_def[of "(insert 0 S)"] assms by blast then have "x ∈ span (insert 0 S - {x})" using affine_hull_subset_span by auto moreover have "span (insert 0 S - {x}) = span (S - {x})" using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto ultimately have "x ∈ span (S - {x})" by auto then have "x ≠ 0 ⟹ dependent S" using x dependent_def by auto moreover { assume "x = 0" then have "0 ∈ affine hull S" using x hull_mono[of "S - {0}" S] by auto then have "dependent S" using affine_hull_0_dependent by auto } ultimately show ?thesis by auto qed lemma affine_dependent_iff_dependent: assumes "a ∉ S" shows "affine_dependent (insert a S) ⟷ dependent ((λx. -a + x) ` S)" proof - have "((+) (- a) ` S) = {x - a| x . x ∈ S}" by auto then show ?thesis using affine_dependent_translation_eq[of "(insert a S)" "-a"] affine_dependent_imp_dependent2 assms dependent_imp_affine_dependent[of a S] by (auto simp del: uminus_add_conv_diff) qed lemma affine_dependent_iff_dependent2: assumes "a ∈ S" shows "affine_dependent S ⟷ dependent ((λx. -a + x) ` (S-{a}))" proof - have "insert a (S - {a}) = S" using assms by auto then show ?thesis using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto qed lemma affine_hull_insert_span_gen: "affine hull (insert a s) = (λx. a + x) ` span ((λx. - a + x) ` s)" proof - have h1: "{x - a |x. x ∈ s} = ((λx. -a+x) ` s)" by auto { assume "a ∉ s" then have ?thesis using affine_hull_insert_span[of a s] h1 by auto } moreover { assume a1: "a ∈ s" have "∃x. x ∈ s ∧ -a+x=0" apply (rule exI[of _ a]) using a1 apply auto done then have "insert 0 ((λx. -a+x) ` (s - {a})) = (λx. -a+x) ` s" by auto then have "span ((λx. -a+x) ` (s - {a}))=span ((λx. -a+x) ` s)" using span_insert_0[of "(+) (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff) moreover have "{x - a |x. x ∈ (s - {a})} = ((λx. -a+x) ` (s - {a}))" by auto moreover have "insert a (s - {a}) = insert a s" by auto ultimately have ?thesis using affine_hull_insert_span[of "a" "s-{a}"] by auto } ultimately show ?thesis by auto qed lemma affine_hull_span2: assumes "a ∈ s" shows "affine hull s = (λx. a+x) ` span ((λx. -a+x) ` (s-{a}))" using affine_hull_insert_span_gen[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto lemma affine_hull_span_gen: assumes "a ∈ affine hull s" shows "affine hull s = (λx. a+x) ` span ((λx. -a+x) ` s)" proof - have "affine hull (insert a s) = affine hull s" using hull_redundant[of a affine s] assms by auto then show ?thesis using affine_hull_insert_span_gen[of a "s"] by auto qed lemma affine_hull_span_0: assumes "0 ∈ affine hull S" shows "affine hull S = span S" using affine_hull_span_gen[of "0" S] assms by auto lemma extend_to_affine_basis_nonempty: fixes S V :: "'n::euclidean_space set" assumes "¬ affine_dependent S" "S ⊆ V" "S ≠ {}" shows "∃T. ¬ affine_dependent T ∧ S ⊆ T ∧ T ⊆ V ∧ affine hull T = affine hull V" proof - obtain a where a: "a ∈ S" using assms by auto then have h0: "independent ((λx. -a + x) ` (S-{a}))" using affine_dependent_iff_dependent2 assms by auto obtain B where B: "(λx. -a+x) ` (S - {a}) ⊆ B ∧ B ⊆ (λx. -a+x) ` V ∧ independent B ∧ (λx. -a+x) ` V ⊆ span B" using assms by (blast intro: maximal_independent_subset_extend[OF _ h0, of "(λx. -a + x) ` V"]) define T where "T = (λx. a+x) ` insert 0 B" then have "T = insert a ((λx. a+x) ` B)" by auto then have "affine hull T = (λx. a+x) ` span B" using affine_hull_insert_span_gen[of a "((λx. a+x) ` B)"] translation_assoc[of "-a" a B] by auto then have "V ⊆ affine hull T" using B assms translation_inverse_subset[of a V "span B"] by auto moreover have "T ⊆ V" using T_def B a assms by auto ultimately have "affine hull T = affine hull V" by (metis Int_absorb1 Int_absorb2 hull_hull hull_mono) moreover have "S ⊆ T" using T_def B translation_inverse_subset[of a "S-{a}" B] by auto moreover have "¬ affine_dependent T" using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B by auto ultimately show ?thesis using ‹T ⊆ V› by auto qed lemma affine_basis_exists: fixes V :: "'n::euclidean_space set" shows "∃B. B ⊆ V ∧ ¬ affine_dependent B ∧ affine hull V = affine hull B" proof (cases "V = {}") case True then show ?thesis using affine_independent_0 by auto next case False then obtain x where "x ∈ V" by auto then show ?thesis using affine_dependent_def[of "{x}"] extend_to_affine_basis_nonempty[of "{x}" V] by auto qed proposition extend_to_affine_basis: fixes S V :: "'n::euclidean_space set" assumes "¬ affine_dependent S" "S ⊆ V" obtains T where "¬ affine_dependent T" "S ⊆ T" "T ⊆ V" "affine hull T = affine hull V" proof (cases "S = {}") case True then show ?thesis using affine_basis_exists by (metis empty_subsetI that) next case False then show ?thesis by (metis assms extend_to_affine_basis_nonempty that) qed subsection ‹Affine Dimension of a Set› definition%important aff_dim :: "('a::euclidean_space) set ⇒ int" where "aff_dim V = (SOME d :: int. ∃B. affine hull B = affine hull V ∧ ¬ affine_dependent B ∧ of_nat (card B) = d + 1)" lemma aff_dim_basis_exists: fixes V :: "('n::euclidean_space) set" shows "∃B. affine hull B = affine hull V ∧ ¬ affine_dependent B ∧ of_nat (card B) = aff_dim V + 1" proof - obtain B where "¬ affine_dependent B ∧ affine hull B = affine hull V" using affine_basis_exists[of V] by auto then show ?thesis unfolding aff_dim_def some_eq_ex[of "λd. ∃B. affine hull B = affine hull V ∧ ¬ affine_dependent B ∧ of_nat (card B) = d + 1"] apply auto apply (rule exI[of _ "int (card B) - (1 :: int)"]) apply (rule exI[of _ "B"], auto) done qed lemma affine_hull_nonempty: "S ≠ {} ⟷ affine hull S ≠ {}" proof - have "S = {} ⟹ affine hull S = {}" using affine_hull_empty by auto moreover have "affine hull S = {} ⟹ S = {}" unfolding hull_def by auto ultimately show ?thesis by blast qed lemma aff_dim_parallel_subspace_aux: fixes B :: "'n::euclidean_space set" assumes "¬ affine_dependent B" "a ∈ B" shows "finite B ∧ ((card B) - 1 = dim (span ((λx. -a+x) ` (B-{a}))))" proof - have "independent ((λx. -a + x) ` (B-{a}))" using affine_dependent_iff_dependent2 assms by auto then have fin: "dim (span ((λx. -a+x) ` (B-{a}))) = card ((λx. -a + x) ` (B-{a}))" "finite ((λx. -a + x) ` (B - {a}))" using indep_card_eq_dim_span[of "(λx. -a+x) ` (B-{a})"] by auto show ?thesis proof (cases "(λx. -a + x) ` (B - {a}) = {}") case True have "B = insert a ((λx. a + x) ` (λx. -a + x) ` (B - {a}))" using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto then have "B = {a}" using True by auto then show ?thesis using assms fin by auto next case False then have "card ((λx. -a + x) ` (B - {a})) > 0" using fin by auto moreover have h1: "card ((λx. -a + x) ` (B-{a})) = card (B-{a})" by (rule card_image) (use translate_inj_on in blast) ultimately have "card (B-{a}) > 0" by auto then have *: "finite (B - {a})" using card_gt_0_iff[of "(B - {a})"] by auto then have "card (B - {a}) = card B - 1" using card_Diff_singleton assms by auto with * show ?thesis using fin h1 by auto qed qed lemma aff_dim_parallel_subspace: fixes V L :: "'n::euclidean_space set" assumes "V ≠ {}" and "subspace L" and "affine_parallel (affine hull V) L" shows "aff_dim V = int (dim L)" proof - obtain B where B: "affine hull B = affine hull V ∧ ¬ affine_dependent B ∧ int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto then have "B ≠ {}" using assms B affine_hull_nonempty[of V] affine_hull_nonempty[of B] by auto then obtain a where a: "a ∈ B" by auto define Lb where "Lb = span ((λx. -a+x) ` (B-{a}))" moreover have "affine_parallel (affine hull B) Lb" using Lb_def B assms affine_hull_span2[of a B] a affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto moreover have "subspace Lb" using Lb_def subspace_span by auto moreover have "affine hull B ≠ {}" using assms B affine_hull_nonempty[of V] by auto ultimately have "L = Lb" using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B by auto then have "dim L = dim Lb" by auto moreover have "card B - 1 = dim Lb" and "finite B" using Lb_def aff_dim_parallel_subspace_aux a B by auto ultimately show ?thesis using B ‹B ≠ {}› card_gt_0_iff[of B] by auto qed lemma aff_independent_finite: fixes B :: "'n::euclidean_space set" assumes "¬ affine_dependent B" shows "finite B" proof - { assume "B ≠ {}" then obtain a where "a ∈ B" by auto then have ?thesis using aff_dim_parallel_subspace_aux assms by auto } then show ?thesis by auto qed lemmas independent_finite = independent_imp_finite lemma span_substd_basis: assumes d: "d ⊆ Basis" shows "span d = {x. ∀i∈Basis. i ∉ d ⟶ x∙i = 0}" (is "_ = ?B") proof - have "d ⊆ ?B" using d by (auto simp: inner_Basis) moreover have s: "subspace ?B" using subspace_substandard[of "λi. i ∉ d"] . ultimately have "span d ⊆ ?B" using span_mono[of d "?B"] span_eq_iff[of "?B"] by blast moreover have *: "card d ≤ dim (span d)" using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms] span_superset[of d] by auto moreover from * have "dim ?B ≤ dim (span d)" using dim_substandard[OF assms] by auto ultimately show ?thesis using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto qed lemma basis_to_substdbasis_subspace_isomorphism: fixes B :: "'a::euclidean_space set" assumes "independent B" shows "∃f d::'a set. card d = card B ∧ linear f ∧ f ` B = d ∧ f ` span B = {x. ∀i∈Basis. i ∉ d ⟶ x ∙ i = 0} ∧ inj_on f (span B) ∧ d ⊆ Basis" proof - have B: "card B = dim B" using dim_unique[of B B "card B"] assms span_superset[of B] by auto have "dim B ≤ card (Basis :: 'a set)" using dim_subset_UNIV[of B] by simp from ex_card[OF this] obtain d :: "'a set" where d: "d ⊆ Basis" and t: "card d = dim B" by auto let ?t = "{x::'a::euclidean_space. ∀i∈Basis. i ∉ d ⟶ x∙i = 0}" have "∃f. linear f ∧ f ` B = d ∧ f ` span B = ?t ∧ inj_on f (span B)" proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_superset) show "d ⊆ {x. ∀i∈Basis. i ∉ d ⟶ x ∙ i = 0}" using d inner_not_same_Basis by blast qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms) with t ‹card B = dim B› d show ?thesis by auto qed lemma aff_dim_empty: fixes S :: "'n::euclidean_space set" shows "S = {} ⟷ aff_dim S = -1" proof - obtain B where *: "affine hull B = affine hull S" and "¬ affine_dependent B" and "int (card B) = aff_dim S + 1" using aff_dim_basis_exists by auto moreover from * have "S = {} ⟷ B = {}" using affine_hull_nonempty[of B] affine_hull_nonempty[of S] by auto ultimately show ?thesis using aff_independent_finite[of B] card_gt_0_iff[of B] by auto qed lemma aff_dim_empty_eq [simp]: "aff_dim ({}::'a::euclidean_space set) = -1" by (simp add: aff_dim_empty [symmetric]) lemma aff_dim_affine_hull [simp]: "aff_dim (affine hull S) = aff_dim S" unfolding aff_dim_def using hull_hull[of _ S] by auto lemma aff_dim_affine_hull2: assumes "affine hull S = affine hull T" shows "aff_dim S = aff_dim T" unfolding aff_dim_def using assms by auto lemma aff_dim_unique: fixes B V :: "'n::euclidean_space set" assumes "affine hull B = affine hull V ∧ ¬ affine_dependent B" shows "of_nat (card B) = aff_dim V + 1" proof (cases "B = {}") case True then have "V = {}" using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms by auto then have "aff_dim V = (-1::int)" using aff_dim_empty by auto then show ?thesis using ‹B = {}› by auto next case False then obtain a where a: "a ∈ B" by auto define Lb where "Lb = span ((λx. -a+x) ` (B-{a}))" have "affine_parallel (affine hull B) Lb" using Lb_def affine_hull_span2[of a B] a affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto moreover have "subspace Lb" using Lb_def subspace_span by auto ultimately have "aff_dim B = int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] ‹B ≠ {}› by auto moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a assms by auto ultimately have "of_nat (card B) = aff_dim B + 1" using ‹B ≠ {}› card_gt_0_iff[of B] by auto then show ?thesis using aff_dim_affine_hull2 assms by auto qed lemma aff_dim_affine_independent: fixes B :: "'n::euclidean_space set" assumes "¬ affine_dependent B" shows "of_nat (card B) = aff_dim B + 1" using aff_dim_unique[of B B] assms by auto lemma affine_independent_iff_card: fixes s :: "'a::euclidean_space set" shows "~ affine_dependent s ⟷ finite s ∧ aff_dim s = int(card s) - 1" apply (rule iffI) apply (simp add: aff_dim_affine_independent aff_independent_finite) by (metis affine_basis_exists [of s] aff_dim_unique card_subset_eq diff_add_cancel of_nat_eq_iff) lemma aff_dim_sing [simp]: fixes a :: "'n::euclidean_space" shows "aff_dim {a} = 0" using aff_dim_affine_independent[of "{a}"] affine_independent_1 by auto lemma aff_dim_2 [simp]: "aff_dim {a,b} = (if a = b then 0 else 1)" proof (clarsimp) assume "a ≠ b" then have "aff_dim{a,b} = card{a,b} - 1" using affine_independent_2 [of a b] aff_dim_affine_independent by fastforce also have "… = 1" using ‹a ≠ b› by simp finally show "aff_dim {a, b} = 1" . qed lemma aff_dim_inner_basis_exists: fixes V :: "('n::euclidean_space) set" shows "∃B. B ⊆ V ∧ affine hull B = affine hull V ∧ ¬ affine_dependent B ∧ of_nat (card B) = aff_dim V + 1" proof - obtain B where B: "¬ affine_dependent B" "B ⊆ V" "affine hull B = affine hull V" using affine_basis_exists[of V] by auto then have "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto with B show ?thesis by auto qed lemma aff_dim_le_card: fixes V :: "'n::euclidean_space set" assumes "finite V" shows "aff_dim V ≤ of_nat (card V) - 1" proof - obtain B where B: "B ⊆ V" "of_nat (card B) = aff_dim V + 1" using aff_dim_inner_basis_exists[of V] by auto then have "card B ≤ card V" using assms card_mono by auto with B show ?thesis by auto qed lemma aff_dim_parallel_eq: fixes S T :: "'n::euclidean_space set" assumes "affine_parallel (affine hull S) (affine hull T)" shows "aff_dim S = aff_dim T" proof - { assume "T ≠ {}" "S ≠ {}" then obtain L where L: "subspace L ∧ affine_parallel (affine hull T) L" using affine_parallel_subspace[of "affine hull T"] affine_affine_hull[of T] affine_hull_nonempty by auto then have "aff_dim T = int (dim L)" using aff_dim_parallel_subspace ‹T ≠ {}› by auto moreover have *: "subspace L ∧ affine_parallel (affine hull S) L" using L affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto moreover from * have "aff_dim S = int (dim L)" using aff_dim_parallel_subspace ‹S ≠ {}› by auto ultimately have ?thesis by auto } moreover { assume "S = {}" then have "S = {}" and "T = {}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto then have ?thesis using aff_dim_empty by auto } moreover { assume "T = {}" then have "S = {}" and "T = {}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto then have ?thesis using aff_dim_empty by auto } ultimately show ?thesis by blast qed lemma aff_dim_translation_eq: fixes a :: "'n::euclidean_space" shows "aff_dim ((λx. a + x) ` S) = aff_dim S" proof - have "affine_parallel (affine hull S) (affine hull ((λx. a + x) ` S))" unfolding affine_parallel_def apply (rule exI[of _ "a"]) using affine_hull_translation[of a S] apply auto done then show ?thesis using aff_dim_parallel_eq[of S "(λx. a + x) ` S"] by auto qed lemma aff_dim_affine: fixes S L :: "'n::euclidean_space set" assumes "S ≠ {}" and "affine S" and "subspace L" and "affine_parallel S L" shows "aff_dim S = int (dim L)" proof - have *: "affine hull S = S" using assms affine_hull_eq[of S] by auto then have "affine_parallel (affine hull S) L" using assms by (simp add: *) then show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast qed lemma dim_affine_hull: fixes S :: "'n::euclidean_space set" shows "dim (affine hull S) = dim S" proof - have "dim (affine hull S) ≥ dim S" using dim_subset by auto moreover have "dim (span S) ≥ dim (affine hull S)" using dim_subset affine_hull_subset_span by blast moreover have "dim (span S) = dim S" using dim_span by auto ultimately show ?thesis by auto qed lemma aff_dim_subspace: fixes S :: "'n::euclidean_space set" assumes "subspace S" shows "aff_dim S = int (dim S)" proof (cases "S={}") case True with assms show ?thesis by (simp add: subspace_affine) next case False with aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] subspace_affine show ?thesis by auto qed lemma aff_dim_zero: fixes S :: "'n::euclidean_space set" assumes "0 ∈ affine hull S" shows "aff_dim S = int (dim S)" proof - have "subspace (affine hull S)" using subspace_affine[of "affine hull S"] affine_affine_hull assms by auto then have "aff_dim (affine hull S) = int (dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto then show ?thesis using aff_dim_affine_hull[of S] dim_affine_hull[of S] by auto qed lemma aff_dim_eq_dim: fixes S :: "'n::euclidean_space set" assumes "a ∈ affine hull S" shows "aff_dim S = int (dim ((λx. -a+x) ` S))" proof - have "0 ∈ affine hull ((λx. -a+x) ` S)" unfolding Convex_Euclidean_Space.affine_hull_translation using assms by (simp add: ab_group_add_class.ab_left_minus image_iff) with aff_dim_zero show ?thesis by (metis aff_dim_translation_eq) qed lemma aff_dim_UNIV [simp]: "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))" using aff_dim_subspace[of "(UNIV :: 'n::euclidean_space set)"] dim_UNIV[where 'a="'n::euclidean_space"] by auto lemma aff_dim_geq: fixes V :: "'n::euclidean_space set" shows "aff_dim V ≥ -1" proof - obtain B where "affine hull B = affine hull V" and "¬ affine_dependent B" and "int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto then show ?thesis by auto qed lemma aff_dim_negative_iff [simp]: fixes S :: "'n::euclidean_space set" shows "aff_dim S < 0 ⟷S = {}" by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq) lemma aff_lowdim_subset_hyperplane: fixes S :: "'a::euclidean_space set" assumes "aff_dim S < DIM('a)" obtains a b where "a ≠ 0" "S ⊆ {x. a ∙ x = b}" proof (cases "S={}") case True moreover have "(SOME b. b ∈ Basis) ≠ 0" by (metis norm_some_Basis norm_zero zero_neq_one) ultimately show ?thesis using that by blast next case False then obtain c S' where "c ∉ S'" "S = insert c S'" by (meson equals0I mk_disjoint_insert) have "dim ((+) (-c) ` S) < DIM('a)" by (metis ‹S = insert c S'› aff_dim_eq_dim assms hull_inc insertI1 of_nat_less_imp_less) then obtain a where "a ≠ 0" "span ((+) (-c) ` S) ⊆ {x. a ∙ x = 0}" using lowdim_subset_hyperplane by blast moreover have "a ∙ w = a ∙ c" if "span ((+) (- c) ` S) ⊆ {x. a ∙ x = 0}" "w ∈ S" for w proof - have "w-c ∈ span ((+) (- c) ` S)" by (simp add: span_base ‹w ∈ S›) with that have "w-c ∈ {x. a ∙ x = 0}" by blast then show ?thesis by (auto simp: algebra_simps) qed ultimately have "S ⊆ {x. a ∙ x = a ∙ c}" by blast then show ?thesis by (rule that[OF ‹a ≠ 0›]) qed lemma affine_independent_card_dim_diffs: fixes S :: "'a :: euclidean_space set" assumes "~ affine_dependent S" "a ∈ S" shows "card S = dim {x - a|x. x ∈ S} + 1" proof - have 1: "{b - a|b. b ∈ (S - {a})} ⊆ {x - a|x. x ∈ S}" by auto have 2: "x - a ∈ span {b - a |b. b ∈ S - {a}}" if "x ∈ S" for x proof (cases "x = a") case True then show ?thesis by (simp add: span_clauses) next case False then show ?thesis using assms by (blast intro: span_base that) qed have "¬ affine_dependent (insert a S)" by (simp add: assms insert_absorb) then have 3: "independent {b - a |b. b ∈ S - {a}}" using dependent_imp_affine_dependent by fastforce have "{b - a |b. b ∈ S - {a}} = (λb. b-a) ` (S - {a})" by blast then have "card {b - a |b. b ∈ S - {a}} = card ((λb. b-a) ` (S - {a}))" by simp also have "… = card (S - {a})" by (metis (no_types, lifting) card_image diff_add_cancel inj_onI) also have "… = card S - 1" by (simp add: aff_independent_finite assms) finally have 4: "card {b - a |b. b ∈ S - {a}} = card S - 1" . have "finite S" by (meson assms aff_independent_finite) with ‹a ∈ S› have "card S ≠ 0" by auto moreover have "dim {x - a |x. x ∈ S} = card S - 1" using 2 by (blast intro: dim_unique [OF 1 _ 3 4]) ultimately show ?thesis by auto qed lemma independent_card_le_aff_dim: fixes B :: "'n::euclidean_space set" assumes "B ⊆ V" assumes "¬ affine_dependent B" shows "int (card B) ≤ aff_dim V + 1" proof - obtain T where T: "¬ affine_dependent T ∧ B ⊆ T ∧ T ⊆ V ∧ affine hull T = affine hull V" by (metis assms extend_to_affine_basis[of B V]) then have "of_nat (card T) = aff_dim V + 1" using aff_dim_unique by auto then show ?thesis using T card_mono[of T B] aff_independent_finite[of T] by auto qed lemma aff_dim_subset: fixes S T :: "'n::euclidean_space set" assumes "S ⊆ T" shows "aff_dim S ≤ aff_dim T" proof - obtain B where B: "¬ affine_dependent B" "B ⊆ S" "affine hull B = affine hull S" "of_nat (card B) = aff_dim S + 1" using aff_dim_inner_basis_exists[of S] by auto then have "int (card B) ≤ aff_dim T + 1" using assms independent_card_le_aff_dim[of B T] by auto with B show ?thesis by auto qed lemma aff_dim_le_DIM: fixes S :: "'n::euclidean_space set" shows "aff_dim S ≤ int (DIM('n))" proof - have "aff_dim (UNIV :: 'n::euclidean_space set) = int(DIM('n))" using aff_dim_UNIV by auto then show "aff_dim (S:: 'n::euclidean_space set) ≤ int(DIM('n))" using aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto qed lemma affine_dim_equal: fixes S :: "'n::euclidean_space set" assumes "affine S" "affine T" "S ≠ {}" "S ⊆ T" "aff_dim S = aff_dim T" shows "S = T" proof - obtain a where "a ∈ S" using assms by auto then have "a ∈ T" using assms by auto define LS where "LS = {y. ∃x ∈ S. (-a) + x = y}" then have ls: "subspace LS" "affine_parallel S LS" using assms parallel_subspace_explicit[of S a LS] ‹a ∈ S› by auto then have h1: "int(dim LS) = aff_dim S" using assms aff_dim_affine[of S LS] by auto have "T ≠ {}" using assms by auto define LT where "LT = {y. ∃x ∈ T. (-a) + x = y}" then have lt: "subspace LT ∧ affine_parallel T LT" using assms parallel_subspace_explicit[of T a LT] ‹a ∈ T› by auto then have "int(dim LT) = aff_dim T" using assms aff_dim_affine[of T LT] ‹T ≠ {}› by auto then have "dim LS = dim LT" using h1 assms by auto moreover have "LS ≤ LT" using LS_def LT_def assms by auto ultimately have "LS = LT" using subspace_dim_equal[of LS LT] ls lt by auto moreover have "S = {x. ∃y ∈ LS. a+y=x}" using LS_def by auto moreover have "T = {x. ∃y ∈ LT. a+y=x}" using LT_def by auto ultimately show ?thesis by auto qed lemma aff_dim_eq_0: fixes S :: "'a::euclidean_space set" shows "aff_dim S = 0 ⟷ (∃a. S = {a})" proof (cases "S = {}") case True then show ?thesis by auto next case False then obtain a where "a ∈ S" by auto show ?thesis proof safe assume 0: "aff_dim S = 0" have "~ {a,b} ⊆ S" if "b ≠ a" for b by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that) then show "∃a. S = {a}" using ‹a ∈ S› by blast qed auto qed lemma affine_hull_UNIV: fixes S :: "'n::euclidean_space set" assumes "aff_dim S = int(DIM('n))" shows "affine hull S = (UNIV :: ('n::euclidean_space) set)" proof - have "S ≠ {}" using assms aff_dim_empty[of S] by auto have h0: "S ⊆ affine hull S" using hull_subset[of S _] by auto have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S" using aff_dim_UNIV assms by auto then have h2: "aff_dim (affine hull S) ≤ aff_dim (UNIV :: ('n::euclidean_space) set)" using aff_dim_le_DIM[of "affine hull S"] assms h0 by auto have h3: "aff_dim S ≤ aff_dim (affine hull S)" using h0 aff_dim_subset[of S "affine hull S"] assms by auto then have h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)" using h0 h1 h2 by auto then show ?thesis using affine_dim_equal[of "affine hull S" "(UNIV :: ('n::euclidean_space) set)"] affine_affine_hull[of S] affine_UNIV assms h4 h0 ‹S ≠ {}› by auto qed lemma disjoint_affine_hull: fixes s :: "'n::euclidean_space set" assumes "~ affine_dependent s" "t ⊆ s" "u ⊆ s" "t ∩ u = {}" shows "(affine hull t) ∩ (affine hull u) = {}" proof - have "finite s" using assms by (simp add: aff_independent_finite) then have "finite t" "finite u" using assms finite_subset by blast+ { fix y assume yt: "y ∈ affine hull t" and yu: "y ∈ affine hull u" then obtain a b where a1 [simp]: "sum a t = 1" and [simp]: "sum (λv. a v *⇩_{R}v) t = y" and [simp]: "sum b u = 1" "sum (λv. b v *⇩_{R}v) u = y" by (auto simp: affine_hull_finite ‹finite t› ‹finite u›) define c where "c x = (if x ∈ t then a x else if x ∈ u then -(b x) else 0)" for x have [simp]: "s ∩ t = t" "s ∩ - t ∩ u = u" using assms by auto have "sum c s = 0" by (simp add: c_def comm_monoid_add_class.sum.If_cases ‹finite s› sum_negf) moreover have "~ (∀v∈s. c v = 0)" by (metis (no_types) IntD1 ‹s ∩ t = t› a1 c_def sum_not_0 zero_neq_one) moreover have "(∑v∈s. c v *⇩_{R}v) = 0" by (simp add: c_def if_smult sum_negf comm_monoid_add_class.sum.If_cases ‹finite s›) ultimately have False using assms ‹finite s› by (auto simp: affine_dependent_explicit) } then show ?thesis by blast qed lemma aff_dim_convex_hull: fixes S :: "'n::euclidean_space set" shows "aff_dim (convex hull S) = aff_dim S" using aff_dim_affine_hull[of S] convex_hull_subset_affine_hull[of S] hull_subset[of S "convex"] aff_dim_subset[of S "convex hull S"] aff_dim_subset[of "convex hull S" "affine hull S"] by auto lemma aff_dim_cball: fixes a :: "'n::euclidean_space" assumes "e > 0" shows "aff_dim (cball a e) = int (DIM('n))" proof - have "(λx. a + x) ` (cball 0 e) ⊆ cball a e" unfolding cball_def dist_norm by auto then have "aff_dim (cball (0 :: 'n::euclidean_space) e) ≤ aff_dim (cball a e)" using aff_dim_translation_eq[of a "cball 0 e"] aff_dim_subset[of "(+) a ` cball 0 e" "cball a e"] by auto moreover have "aff_dim (cball (0 :: 'n::euclidean_space) e) = int (DIM('n))" using hull_inc[of "(0 :: 'n::euclidean_space)" "cball 0 e"] centre_in_cball[of "(0 :: 'n::euclidean_space)"] assms by (simp add: dim_cball[of e] aff_dim_zero[of "cball 0 e"]) ultimately show ?thesis using aff_dim_le_DIM[of "cball a e"] by auto qed lemma aff_dim_open: fixes S :: "'n::euclidean_space set" assumes "open S" and "S ≠ {}" shows "aff_dim S = int (DIM('n))" proof - obtain x where "x ∈ S" using assms by auto then obtain e where e: "e > 0" "cball x e ⊆ S" using open_contains_cball[of S] assms by auto then have "aff_dim (cball x e) ≤ aff_dim S" using aff_dim_subset by auto with e show ?thesis using aff_dim_cball[of e x] aff_dim_le_DIM[of S] by auto qed lemma low_dim_interior: fixes S :: "'n::euclidean_space set" assumes "¬ aff_dim S = int (DIM('n))" shows "interior S = {}" proof - have "aff_dim(interior S) ≤ aff_dim S" using interior_subset aff_dim_subset[of "interior S" S] by auto then show ?thesis using aff_dim_open[of "interior S"] aff_dim_le_DIM[of S] assms by auto qed corollary empty_interior_lowdim: fixes S :: "'n::euclidean_space set" shows "dim S < DIM ('n) ⟹ interior S = {}" by (metis low_dim_interior affine_hull_UNIV dim_affine_hull less_not_refl dim_UNIV) corollary aff_dim_nonempty_interior: fixes S :: "'a::euclidean_space set" shows "interior S ≠ {} ⟹ aff_dim S = DIM('a)" by (metis low_dim_interior) subsection ‹Caratheodory's theorem› lemma convex_hull_caratheodory_aff_dim: fixes p :: "('a::euclidean_space) set" shows "convex hull p = {y. ∃s u. finite s ∧ s ⊆ p ∧ card s ≤ aff_dim p + 1 ∧ (∀x∈s. 0 ≤ u x) ∧ sum u s = 1 ∧ sum (λv. u v *⇩_{R}v) s = y}" unfolding convex_hull_explicit set_eq_iff mem_Collect_eq proof (intro allI iffI) fix y let ?P = "λn. ∃s u. finite s ∧ card s = n ∧ s ⊆ p ∧ (∀x∈s. 0 ≤ u x) ∧ sum u s = 1 ∧ (∑v∈s. u v *⇩_{R}v) = y" assume "∃s u. finite s ∧ s ⊆ p ∧ (∀x∈s. 0 ≤ u x) ∧ sum u s = 1 ∧ (∑v∈s. u v *⇩_{R}v) = y" then obtain N where "?P N" by auto then have "∃n≤N. (∀k<n. ¬ ?P k) ∧ ?P n" apply (rule_tac ex_least_nat_le, auto) done then obtain n where "?P n" and smallest: "∀k<n. ¬ ?P k" by blast then obtain s u where obt: "finite s" "card s = n" "s⊆p" "∀x∈s. 0 ≤ u x" "sum u s = 1" "(∑v∈s. u v *⇩_{R}v) = y" by auto have "card s ≤ aff_dim p + 1" proof (rule ccontr, simp only: not_le) assume "aff_dim p + 1 < card s" then have "affine_dependent s" using affine_dependent_biggerset[OF obt(1)] independent_card_le_aff_dim not_less obt(3) by blast then obtain w v where wv: "sum w s = 0" "v∈s" "w v ≠ 0" "(∑v∈s. w v *⇩_{R}v) = 0" using affine_dependent_explicit_finite[OF obt(1)] by auto define i where "i = (λv. (u v) / (- w v)) ` {v∈s. w v < 0}" define t where "t = Min i" have "∃x∈s. w x < 0" proof (rule ccontr, simp add: not_less) assume as:"∀x∈s. 0 ≤ w x" then have "sum w (s - {v}) ≥ 0" apply (rule_tac sum_nonneg