section ‹Convex Hulls› text ‹We define the notion of convex hull of a set or list of vectors and derive basic properties thereof.› theory Convex_Hull imports Cone begin context gram_schmidt begin definition "convex_lincomb c Vs b = (nonneg_lincomb c Vs b ∧ sum c Vs = 1)" definition "convex_lincomb_list c Vs b = (nonneg_lincomb_list c Vs b ∧ sum c {0..<length Vs} = 1)" definition "convex_hull Vs = {x. ∃ Ws c. finite Ws ∧ Ws ⊆ Vs ∧ convex_lincomb c Ws x}" lemma convex_hull_carrier[intro]: "Vs ⊆ carrier_vec n ⟹ convex_hull Vs ⊆ carrier_vec n" unfolding convex_hull_def convex_lincomb_def nonneg_lincomb_def by auto lemma convex_hull_mono: "Vs ⊆ Ws ⟹ convex_hull Vs ⊆ convex_hull Ws" unfolding convex_hull_def by auto lemma convex_lincomb_empty[simp]: "¬ (convex_lincomb c {} x)" unfolding convex_lincomb_def by simp lemma set_in_convex_hull: assumes "A ⊆ carrier_vec n" shows "A ⊆ convex_hull A" proof fix a assume "a ∈ A" hence acarr: "a ∈ carrier_vec n" using assms by auto hence "convex_lincomb (λ x. 1) {a} a " unfolding convex_lincomb_def by (auto simp: nonneg_lincomb_def lincomb_def) then show "a ∈ convex_hull A" using ‹a ∈ A› unfolding convex_hull_def by auto qed lemma convex_hull_empty[simp]: "convex_hull {} = {}" "A ⊆ carrier_vec n ⟹ convex_hull A = {} ⟷ A = {}" proof - show "convex_hull {} = {}" unfolding convex_hull_def by auto then show "A ⊆ carrier_vec n ⟹ convex_hull A = {} ⟷ A = {}" using set_in_convex_hull[of A] by auto qed lemma convex_hull_bound: assumes XBnd: "X ⊆ Bounded_vec Bnd" and X: "X ⊆ carrier_vec n" shows "convex_hull X ⊆ Bounded_vec Bnd" proof fix x assume "x ∈ convex_hull X" from this[unfolded convex_hull_def] obtain Y c where fin: "finite Y" and YX: "Y ⊆ X" and cx: "convex_lincomb c Y x" by auto from cx[unfolded convex_lincomb_def nonneg_lincomb_def] have x: "x = lincomb c Y" and sum: "sum c Y = 1" and c0: "⋀ y. y ∈ Y ⟹ c y ≥ 0" by auto from YX X XBnd have Y: "Y ⊆ carrier_vec n" and YBnd: "Y ⊆ Bounded_vec Bnd" by auto from x Y have dim: "dim_vec x = n" by auto show "x ∈ Bounded_vec Bnd" unfolding Bounded_vec_def mem_Collect_eq dim proof (intro allI impI) fix i assume i: "i < n" have "abs (x $ i) = abs (∑x∈Y. c x * x $ i)" unfolding x by (subst lincomb_index[OF i Y], auto) also have "… ≤ (∑x∈Y. abs (c x * x $ i))" by auto also have "… = (∑x∈Y. abs (c x) * abs (x $ i))" by (simp add: abs_mult) also have "… ≤ (∑x∈Y. abs (c x) * Bnd)" by (intro sum_mono mult_left_mono, insert YBnd[unfolded Bounded_vec_def] i Y, force+) also have "… = (∑x∈Y. abs (c x)) * Bnd" by (simp add: sum_distrib_right) also have "(∑x∈Y. abs (c x)) = (∑x∈Y. c x)" by (rule sum.cong, insert c0, auto) also have "… = 1" by fact finally show "¦x $ i¦ ≤ Bnd" by auto qed qed definition "convex_hull_list Vs = {x. ∃ c. convex_lincomb_list c Vs x}" lemma lincomb_list_elem: "set Vs ⊆ carrier_vec n ⟹ lincomb_list (λ j. if i=j then 1 else 0) Vs = (if i < length Vs then Vs ! i else 0⇩_{v}n)" proof (induction Vs rule: rev_induct) case (snoc x Vs) have x: "x ∈ carrier_vec n" and Vs: "set Vs ⊆ carrier_vec n" using snoc.prems by auto let ?f = "λ j. if i = j then 1 else 0" have "lincomb_list ?f (Vs @ [x]) = lincomb_list ?f Vs + ?f (length Vs) ⋅⇩_{v}x" using x Vs by simp also have "… = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0⇩_{v}n)" (is ?goal) using less_linear[of i "length Vs"] proof (elim disjE) assume i: "i < length Vs" have "lincomb_list (λj. if i = j then 1 else 0) Vs = Vs ! i" using snoc.IH[OF Vs] i by auto moreover have "(if i = length Vs then 1 else 0) ⋅⇩_{v}x = 0⇩_{v}n" using i x by auto moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0⇩_{v}n) = Vs ! i" using i append_Cons_nth_left by fastforce ultimately show ?goal using Vs i lincomb_list_carrier M.r_zero by metis next assume i: "i = length Vs" have "lincomb_list (λj. if i = j then 1 else 0) Vs = 0⇩_{v}n" using snoc.IH[OF Vs] i by auto moreover have "(if i = length Vs then 1 else 0) ⋅⇩_{v}x = x" using i x by auto moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0⇩_{v}n) = x" using i append_Cons_nth_left by simp ultimately show ?goal using x by simp next assume i: "i > length Vs" have "lincomb_list (λj. if i = j then 1 else 0) Vs = 0⇩_{v}n" using snoc.IH[OF Vs] i by auto moreover have "(if i = length Vs then 1 else 0) ⋅⇩_{v}x = 0⇩_{v}n" using i x by auto moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0⇩_{v}n) = 0⇩_{v}n" using i by simp ultimately show ?goal by simp qed finally show ?case by auto qed simp lemma set_in_convex_hull_list: fixes Vs :: "'a vec list" assumes "set Vs ⊆ carrier_vec n" shows "set Vs ⊆ convex_hull_list Vs" proof fix x assume "x ∈ set Vs" then obtain i where i: "i < length Vs" and x: "x = Vs ! i" using set_conv_nth[of Vs] by auto let ?f = "λ j. if i = j then 1 else 0 :: 'a" have "lincomb_list ?f Vs = x" using i x lincomb_list_elem[OF assms] by auto moreover have "∀ j < length Vs. ?f j ≥ 0" by auto moreover have "sum ?f {0..<length Vs} = 1" using i by simp ultimately show "x ∈ convex_hull_list Vs" unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def by auto qed lemma convex_hull_list_combination: assumes Vs: "set Vs ⊆ carrier_vec n" and x: "x ∈ convex_hull_list Vs" and y: "y ∈ convex_hull_list Vs" and l0: "0 ≤ l" and l1: "l ≤ 1" shows "l ⋅⇩_{v}x + (1 - l) ⋅⇩_{v}y ∈ convex_hull_list Vs" proof - from x obtain cx where x: "lincomb_list cx Vs = x" and cx0: "∀ i < length Vs. cx i ≥ 0" and cx1: "sum cx {0..<length Vs} = 1" unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def by auto from y obtain cy where y: "lincomb_list cy Vs = y" and cy0: "∀ i < length Vs. cy i ≥ 0" and cy1: "sum cy {0..<length Vs} = 1" unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def by auto let ?c = "λ i. l * cx i + (1 - l) * cy i" have "set Vs ⊆ carrier_vec n ⟹ lincomb_list ?c Vs = l ⋅⇩_{v}lincomb_list cx Vs + (1 - l) ⋅⇩_{v}lincomb_list cy Vs" proof (induction Vs rule: rev_induct) case (snoc v Vs) have v: "v ∈ carrier_vec n" and Vs: "set Vs ⊆ carrier_vec n" using snoc.prems by auto have "lincomb_list ?c (Vs @ [v]) = lincomb_list ?c Vs + ?c (length Vs) ⋅⇩_{v}v" using snoc.prems by auto also have "lincomb_list ?c Vs = l ⋅⇩_{v}lincomb_list cx Vs + (1 - l) ⋅⇩_{v}lincomb_list cy Vs" by (rule snoc.IH[OF Vs]) also have "?c (length Vs) ⋅⇩_{v}v = l ⋅⇩_{v}(cx (length Vs) ⋅⇩_{v}v) + (1 - l) ⋅⇩_{v}(cy (length Vs) ⋅⇩_{v}v)" using add_smult_distrib_vec smult_smult_assoc by metis also have "l ⋅⇩_{v}lincomb_list cx Vs + (1 - l) ⋅⇩_{v}lincomb_list cy Vs + … = l ⋅⇩_{v}(lincomb_list cx Vs + cx (length Vs) ⋅⇩_{v}v) + (1 - l) ⋅⇩_{v}(lincomb_list cy Vs + cy (length Vs) ⋅⇩_{v}v)" using lincomb_list_carrier[OF Vs] v by (simp add: M.add.m_assoc M.add.m_lcomm smult_r_distr) finally show ?case using Vs v by simp qed simp hence "lincomb_list ?c Vs = l ⋅⇩_{v}x + (1 - l) ⋅⇩_{v}y" using Vs x y by simp moreover have "∀ i < length Vs. ?c i ≥ 0" using cx0 cy0 l0 l1 by simp moreover have "sum ?c {0..<length Vs} = 1" proof(simp add: sum.distrib) have "(∑i = 0..<length Vs. (1 - l) * cy i) = (1 - l) * sum cy {0..<length Vs}" using sum_distrib_left by metis moreover have "(∑i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}" using sum_distrib_left by metis ultimately show "(∑i = 0..<length Vs. l * cx i) + (∑i = 0..<length Vs. (1 - l) * cy i) = 1" using cx1 cy1 by simp qed ultimately show ?thesis unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def by auto qed lemma convex_hull_list_mono: assumes "set Ws ⊆ carrier_vec n" shows "set Vs ⊆ set Ws ⟹ convex_hull_list Vs ⊆ convex_hull_list Ws" proof (standard, induction Vs) case Nil from Nil(2) show ?case unfolding convex_hull_list_def convex_lincomb_list_def by auto next case (Cons v Vs) have v: "v ∈ set Ws" and Vs: "set Vs ⊆ set Ws" using Cons.prems(1) by auto hence v1: "v ∈ convex_hull_list Ws" using set_in_convex_hull_list[OF assms] by auto from Cons.prems(2) obtain c where x: "lincomb_list c (v # Vs) = x" and c0: "∀ i < length Vs + 1. c i ≥ 0" and c1: "sum c {0..<length Vs + 1} = 1" unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def by auto have x: "x = c 0 ⋅⇩_{v}v + lincomb_list (c ∘ Suc) Vs" using Vs v assms x by auto show ?case proof (cases) assume P: "c 0 = 1" hence "sum (c ∘ Suc) {0..<length Vs} = 0" using sum.atLeast0_lessThan_Suc_shift c1 by (metis One_nat_def R.show_r_zero add.right_neutral add_Suc_right) moreover have "⋀ i. i ∈ {0..<length Vs} ⟹ (c ∘ Suc) i ≥ 0" using c0 by simp ultimately have "∀ i ∈ {0..<length Vs}. (c ∘ Suc) i = 0" using sum_nonneg_eq_0_iff by blast hence "⋀ i. i < length Vs ⟹ (c ∘ Suc) i ⋅⇩_{v}Vs ! i = 0⇩_{v}n" using Vs assms by (simp add: subset_code(1)) hence "lincomb_list (c ∘ Suc) Vs = 0⇩_{v}n" using lincomb_list_eq_0 by simp hence "x = v" using P x v assms by auto thus ?case using v1 by auto next assume P: "c 0 ≠ 1" have c1: "c 0 + sum (c ∘ Suc) {0..<length Vs} = 1" using sum.atLeast0_lessThan_Suc_shift[of c] c1 by simp have "sum (c ∘ Suc) {0..<length Vs} ≥ 0" by (rule sum_nonneg, insert c0, simp) hence "c 0 < 1" using P c1 by auto let ?c' = "λ i. 1 / (1 - c 0) * (c ∘ Suc) i" have "sum ?c' {0..<length Vs} = 1 / (1 - c 0) * sum (c ∘ Suc) {0..<length Vs}" using c1 P sum_distrib_left by metis hence "sum ?c' {0..<length Vs} = 1" using P c1 by simp moreover have "∀ i < length Vs. ?c' i ≥ 0" using c0 ‹c 0 < 1› by simp ultimately have c': "lincomb_list ?c' Vs ∈ convex_hull_list Ws" using Cons.IH[OF Vs] convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def by blast have "lincomb_list ?c' Vs = 1 / (1 - c 0) ⋅⇩_{v}lincomb_list (c ∘ Suc) Vs" by(rule lincomb_list_smult, insert Vs assms, auto) hence "(1 - c 0) ⋅⇩_{v}lincomb_list ?c' Vs = lincomb_list (c ∘ Suc) Vs" using P by auto hence "x = c 0 ⋅⇩_{v}v + (1 - c 0) ⋅⇩_{v}lincomb_list ?c' Vs" using x by auto thus "x ∈ convex_hull_list Ws" using convex_hull_list_combination[OF assms v1 c'] c0 ‹c 0 < 1› by simp qed qed lemma convex_hull_list_eq_set: "set Vs ⊆ carrier_vec n ⟹ set Vs = set Ws ⟹ convex_hull_list Vs = convex_hull_list Ws" using convex_hull_list_mono by blast lemma find_indices_empty: "(find_indices x Vs = []) = (x ∉ set Vs)" proof (induction Vs rule: rev_induct) case (snoc v Vs) show ?case proof assume "find_indices x (Vs @ [v]) = []" hence "x ≠ v ∧ find_indices x Vs = []" by auto thus "x ∉ set (Vs @ [v])" using snoc by simp next assume "x ∉ set (Vs @ [v])" hence "x ≠ v ∧ find_indices x Vs = []" using snoc by auto thus "find_indices x (Vs @ [v]) = []" by simp qed qed simp lemma distinct_list_find_indices: shows "⟦ i < length Vs; Vs ! i = x; distinct Vs ⟧ ⟹ find_indices x Vs = [i]" proof (induction Vs rule: rev_induct) case (snoc v Vs) have dist: "distinct Vs" and xVs: "v ∉ set Vs" using snoc.prems(3) by(simp_all) show ?case proof (cases) assume i: "i = length Vs" hence "x = v" using snoc.prems(2) by auto thus ?case using xVs find_indices_empty i by fastforce next assume "i ≠ length Vs" hence i: "i < length Vs" using snoc.prems(1) by simp hence Vsi: "Vs ! i = x" using snoc.prems(2) append_Cons_nth_left by fastforce hence "x ≠ v" using snoc.prems(3) i by auto thus ?case using snoc.IH[OF i Vsi dist] by simp qed qed auto lemma finite_convex_hull_iff_convex_hull_list: assumes Vs: "Vs ⊆ carrier_vec n" and id': "Vs = set Vsl'" shows "convex_hull Vs = convex_hull_list Vsl'" proof - have fin: "finite Vs" unfolding id' by auto from finite_distinct_list fin obtain Vsl where id: "Vs = set Vsl" and dist: "distinct Vsl" by auto from Vs id have Vsl: "set Vsl ⊆ carrier_vec n" by auto { fix c :: "nat ⇒ 'a" have "distinct Vsl ⟹(∑x∈set Vsl. sum_list (map c (find_indices x Vsl))) = sum c {0..<length Vsl}" proof (induction Vsl rule: rev_induct) case (snoc v Vsl) let ?coef = "λ x. sum_list (map c (find_indices x (Vsl @ [v])))" let ?coef' = "λ x. sum_list (map c (find_indices x Vsl))" have dist: "distinct Vsl" using snoc.prems by simp have "sum ?coef (set (Vsl @ [v])) = sum_list (map ?coef (Vsl @ [v]))" by (rule sum.distinct_set_conv_list[OF snoc.prems, of ?coef]) also have "… = sum_list (map ?coef Vsl) + ?coef v" by simp also have "sum_list (map ?coef Vsl) = sum ?coef (set Vsl)" using sum.distinct_set_conv_list[OF dist, of ?coef] by auto also have "… = sum ?coef' (set Vsl)" proof (intro R.finsum_restrict[of ?coef] restrict_ext, standard) fix x assume "x ∈ set Vsl" then obtain i where i: "i < length Vsl" and x: "x = Vsl ! i" using in_set_conv_nth[of x Vsl] by blast hence "(Vsl @ [v]) ! i = x" by (simp add: append_Cons_nth_left) hence "?coef x = c i" using distinct_list_find_indices[OF _ _ snoc.prems] i by fastforce also have "c i = ?coef' x" using distinct_list_find_indices[OF i _ dist] x by simp finally show "?coef x = ?coef' x" by auto qed also have "… = sum c {0..<length Vsl}" by (rule snoc.IH[OF dist]) also have "?coef v = c (length Vsl)" using distinct_list_find_indices[OF _ _ snoc.prems, of "length Vsl" v] nth_append_length by simp finally show ?case using sum.atLeast0_lessThan_Suc by simp qed simp } note sum_sumlist = this { fix b assume "b ∈ convex_hull_list Vsl" then obtain c where b: "lincomb_list c Vsl = b" and c: "(∀ i < length Vsl. c i ≥ 0)" and c1: "sum c {0..<length Vsl} = 1" unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def by auto have "convex_lincomb (mk_coeff Vsl c) Vs b" unfolding b[symmetric] convex_lincomb_def nonneg_lincomb_def apply (subst lincomb_list_as_lincomb[OF Vsl]) by (insert c c1, auto simp: id mk_coeff_def dist sum_sumlist intro!: sum_list_nonneg) hence "b ∈ convex_hull Vs" unfolding convex_hull_def convex_lincomb_def using fin by blast } moreover { fix b assume "b ∈ convex_hull Vs" then obtain c Ws where Ws: "Ws ⊆ Vs" and b: "lincomb c Ws = b" and c: "c ` Ws ⊆ {x. x ≥ 0}" and c1: "sum c Ws = 1" unfolding convex_hull_def convex_lincomb_def nonneg_lincomb_def by auto let ?d = "λ x. if x ∈ Ws then c x else 0" have "lincomb ?d Vs = lincomb c Ws + lincomb (λ x. 0) (Vs - Ws)" using lincomb_union2[OF _ _ Diff_disjoint[of Ws Vs], of c "λ x. 0"] fin Vs Diff_partition[OF Ws] by metis also have "lincomb (λ x. 0) (Vs - Ws) = 0⇩_{v}n" using lincomb_zero[of "Vs - Ws" "λ x. 0"] Vs by auto finally have "lincomb ?d Vs = b" using b lincomb_closed Vs Ws by auto moreover have "?d ` Vs ⊆ {t. t ≥ 0}" using c by auto moreover have "sum ?d Vs = 1" using c1 R.extend_sum[OF fin Ws] by auto ultimately have "∃ c. convex_lincomb c Vs b" unfolding convex_lincomb_def nonneg_lincomb_def by blast } moreover { fix b assume "∃ c. convex_lincomb c Vs b" then obtain c where b: "lincomb c Vs = b" and c: "c ` Vs ⊆ {x. x ≥ 0}" and c1: "sum c Vs = 1" unfolding convex_lincomb_def nonneg_lincomb_def by auto from lincomb_as_lincomb_list_distinct[OF Vsl dist, of c] have b: "lincomb_list (λi. c (Vsl ! i)) Vsl = b" unfolding b[symmetric] id by simp have "1 = sum c (set Vsl)" using c1 id by auto also have "… = sum_list (map c Vsl)" by(rule sum.distinct_set_conv_list[OF dist]) also have "… = sum ((!) (map c Vsl)) {0..<length Vsl}" using sum_list_sum_nth length_map by metis also have "… = sum (λ i. c (Vsl ! i)) {0..<length Vsl}" by simp finally have sum_1: "(∑i = 0..<length Vsl. c (Vsl ! i)) = 1" by simp have "∃ c. convex_lincomb_list c Vsl b" unfolding convex_lincomb_list_def nonneg_lincomb_list_def by (intro exI[of _ "λi. c (Vsl ! i)"] conjI b sum_1) (insert c, force simp: set_conv_nth id) hence "b ∈ convex_hull_list Vsl" unfolding convex_hull_list_def by auto } ultimately have "convex_hull Vs = convex_hull_list Vsl" by auto also have "convex_hull_list Vsl = convex_hull_list Vsl'" using convex_hull_list_eq_set[OF Vsl, of Vsl'] id id' by simp finally show ?thesis by simp qed definition "convex S = (convex_hull S = S)" lemma convex_convex_hull: "convex S ⟹ convex_hull S = S" unfolding convex_def by auto lemma convex_hull_convex_hull_listD: assumes A: "A ⊆ carrier_vec n" and x: "x ∈ convex_hull A" shows "∃ as. set as ⊆ A ∧ x ∈ convex_hull_list as" proof - from x[unfolded convex_hull_def] obtain X c where finX: "finite X" and XA: "X ⊆ A" and "convex_lincomb c X x" by auto hence x: "x ∈ convex_hull X" unfolding convex_hull_def by auto from finite_list[OF finX] obtain xs where X: "X = set xs" by auto from finite_convex_hull_iff_convex_hull_list[OF _ this] x XA A have x: "x ∈ convex_hull_list xs" by auto thus ?thesis using XA unfolding X by auto qed lemma convex_hull_convex_sum: assumes A: "A ⊆ carrier_vec n" and x: "x ∈ convex_hull A" and y: "y ∈ convex_hull A" and a: "0 ≤ a" "a ≤ 1" shows "a ⋅⇩_{v}x + (1 - a) ⋅⇩_{v}y ∈ convex_hull A" proof - from convex_hull_convex_hull_listD[OF A x] obtain xs where xs: "set xs ⊆ A" and x: "x ∈ convex_hull_list xs" by auto from convex_hull_convex_hull_listD[OF A y] obtain ys where ys: "set ys ⊆ A" and y: "y ∈ convex_hull_list ys" by auto have fin: "finite (set (xs @ ys))" by auto have sub: "set (xs @ ys) ⊆ A" using xs ys by auto from convex_hull_list_mono[of "xs @ ys" xs] x sub A have x: "x ∈ convex_hull_list (xs @ ys)" by auto from convex_hull_list_mono[of "xs @ ys" ys] y sub A have y: "y ∈ convex_hull_list (xs @ ys)" by auto from convex_hull_list_combination[OF _ x y a] have "a ⋅⇩_{v}x + (1 - a) ⋅⇩_{v}y ∈ convex_hull_list (xs @ ys)" using sub A by auto from finite_convex_hull_iff_convex_hull_list[of _ "xs @ ys"] this sub A have "a ⋅⇩_{v}x + (1 - a) ⋅⇩_{v}y ∈ convex_hull (set (xs @ ys))" by auto with convex_hull_mono[OF sub] show "a ⋅⇩_{v}x + (1 - a) ⋅⇩_{v}y ∈ convex_hull A" by auto qed lemma convexI: assumes S: "S ⊆ carrier_vec n" and step: "⋀ a x y. x ∈ S ⟹ y ∈ S ⟹ 0 ≤ a ⟹ a ≤ 1 ⟹ a ⋅⇩_{v}x + (1 - a) ⋅⇩_{v}y ∈ S" shows "convex S" unfolding convex_def proof (standard, standard) fix z assume "z ∈ convex_hull S" from this[unfolded convex_hull_def] obtain W c where "finite W" and WS: "W ⊆ S" and "convex_lincomb c W z" by auto then show "z ∈ S" proof (induct W arbitrary: c z) case empty thus ?case unfolding convex_lincomb_def by auto next case (insert w W c z) have "convex_lincomb c (insert w W) z" by fact hence zl: "z = lincomb c (insert w W)" and nonneg: "⋀ w. w ∈ W ⟹ 0 ≤ c w" and cw: "c w ≥ 0" and sum: "sum c (insert w W) = 1" unfolding convex_lincomb_def nonneg_lincomb_def by auto have zl: "z = c w ⋅⇩_{v}w + lincomb c W" unfolding zl by (rule lincomb_insert2, insert insert S, auto) have sum: "c w + sum c W = 1" unfolding sum[symmetric] by (subst sum.insert, insert insert, auto) have W: "W ⊆ carrier_vec n" and w: "w ∈ carrier_vec n" using S insert by auto show ?case proof (cases "sum c W = 0") case True with nonneg have c0: "⋀ w. w ∈ W ⟹ c w = 0" using insert(1) sum_nonneg_eq_0_iff by auto with sum have cw: "c w = 1" by auto have lin0: "lincomb c W = 0⇩_{v}n" by (intro lincomb_zero W, insert c0, auto) have "z = w" unfolding zl cw lin0 using w by simp with insert(4) show ?thesis by simp next case False have "sum c W ≥ 0" using nonneg by (metis sum_nonneg) with False have pos: "sum c W > 0" by auto define b where "b = (λ w. inverse (sum c W) * c w)" have "convex_lincomb b W (lincomb b W)" unfolding convex_lincomb_def nonneg_lincomb_def b_def proof (intro conjI refl) show "(λw. inverse (sum c W) * c w) ` W ⊆ Collect ((≤) 0)" using nonneg pos by auto show "(∑w∈W. inverse (sum c W) * c w) = 1" unfolding sum_distrib_left[symmetric] using False by auto qed from insert(3)[OF _ this] insert have IH: "lincomb b W ∈ S" by auto have lin: "lincomb c W = sum c W ⋅⇩_{v}lincomb b W" unfolding b_def by (subst lincomb_smult[symmetric, OF W], rule lincomb_cong[OF _ W], insert False, auto) from sum cw pos have sum: "sum c W = 1 - c w" and cw1: "c w ≤ 1" by auto show ?thesis unfolding zl lin unfolding sum by (rule step[OF _ IH cw cw1], insert insert, auto) qed qed next show "S ⊆ convex_hull S" using S by (rule set_in_convex_hull) qed lemma convex_hulls_are_convex: assumes "A ⊆ carrier_vec n" shows "convex (convex_hull A)" by (intro convexI convex_hull_convex_sum convex_hull_carrier assms) lemma convex_hull_sum: assumes A: "A ⊆ carrier_vec n" and B: "B ⊆ carrier_vec n" shows "convex_hull (A + B) = convex_hull A + convex_hull B" proof note cA = convex_hull_carrier[OF A] note cB = convex_hull_carrier[OF B] have "convex (convex_hull A + convex_hull B)" proof (intro convexI sum_carrier_vec convex_hull_carrier A B) fix a :: 'a and x1 x2 assume "x1 ∈ convex_hull A + convex_hull B" "x2 ∈ convex_hull A + convex_hull B" then obtain y1 y2 z1 z2 where x12: "x1 = y1 + z1" "x2 = y2 + z2" and y12: "y1 ∈ convex_hull A" "y2 ∈ convex_hull A" and z12: "z1 ∈ convex_hull B" "z2 ∈ convex_hull B" unfolding set_plus_def by auto from y12 z12 cA cB have carr: "y1 ∈ carrier_vec n" "y2 ∈ carrier_vec n" "z1 ∈ carrier_vec n" "z2 ∈ carrier_vec n" by auto assume a: "0 ≤ a" "a ≤ 1" have A: "a ⋅⇩_{v}y1 + (1 - a) ⋅⇩_{v}y2 ∈ convex_hull A" using y12 a A by (metis convex_hull_convex_sum) have B: "a ⋅⇩_{v}z1 + (1 - a) ⋅⇩_{v}z2 ∈ convex_hull B" using z12 a B by (metis convex_hull_convex_sum) have "a ⋅⇩_{v}x1 + (1 - a) ⋅⇩_{v}x2 = (a ⋅⇩_{v}y1 + a ⋅⇩_{v}z1) + ((1 - a) ⋅⇩_{v}y2 + (1 - a) ⋅⇩_{v}z2)" unfolding x12 using carr by (auto simp: smult_add_distrib_vec) also have "… = (a ⋅⇩_{v}y1 + (1 - a) ⋅⇩_{v}y2) + (a ⋅⇩_{v}z1 + (1 - a) ⋅⇩_{v}z2)" using carr by (intro eq_vecI, auto) finally show "a ⋅⇩_{v}x1 + (1 - a) ⋅⇩_{v}x2 ∈ convex_hull A + convex_hull B" using A B by auto qed from convex_convex_hull[OF this] have id: "convex_hull (convex_hull A + convex_hull B) = convex_hull A + convex_hull B" . show "convex_hull (A + B) ⊆ convex_hull A + convex_hull B" by (subst id[symmetric], rule convex_hull_mono[OF set_plus_mono2]; intro set_in_convex_hull A B) show "convex_hull A + convex_hull B ⊆ convex_hull (A + B)" proof fix x assume "x ∈ convex_hull A + convex_hull B" then obtain y z where x: "x = y + z" and y: "y ∈ convex_hull A" and z: "z ∈ convex_hull B" by (auto simp: set_plus_def) from convex_hull_convex_hull_listD[OF A y] obtain ys where ysA: "set ys ⊆ A" and y: "y ∈ convex_hull_list ys" by auto from convex_hull_convex_hull_listD[OF B z] obtain zs where zsB: "set zs ⊆ B" and z: "z ∈ convex_hull_list zs" by auto from y[unfolded convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def] obtain c where yid: "y = lincomb_list c ys" and conv_c: "(∀i<length ys. 0 ≤ c i) ∧ sum c {0..<length ys} = 1" by auto from z[unfolded convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def] obtain d where zid: "z = lincomb_list d zs" and conv_d: "(∀i<length zs. 0 ≤ d i) ∧ sum d {0..<length zs} = 1" by auto from ysA A have ys: "set ys ⊆ carrier_vec n" by auto from zsB B have zs: "set zs ⊆ carrier_vec n" by auto have [intro, simp]: "lincomb_list x ys ∈ carrier_vec n" for x using lincomb_list_carrier[OF ys] . have [intro, simp]: "lincomb_list x zs ∈ carrier_vec n" for x using lincomb_list_carrier[OF zs] . have dim[simp]: "dim_vec (lincomb_list d zs) = n" by auto from yid have y: "y ∈ carrier_vec n" by auto from zid have z: "z ∈ carrier_vec n" by auto { fix x assume "x ∈ set (map ((+) y) zs)" then obtain z where "x = y + z" and "z ∈ set zs" by auto then obtain j where j: "j < length zs" and x: "x = y + zs ! j" unfolding set_conv_nth by auto hence mem: "zs ! j ∈ set zs" by auto hence zsj: "zs ! j ∈ carrier_vec n" using zs by auto let ?list = "(map (λ y. y + zs ! j) ys)" let ?set = "set ?list" have set: "?set ⊆ carrier_vec n" using ys A zsj by auto have lin_map: "lincomb_list c ?list ∈ carrier_vec n" by (intro lincomb_list_carrier[OF set]) have "y + (zs ! j) = lincomb_list c ?list" unfolding yid using zsj lin_map lincomb_list_index[OF _ set] lincomb_list_index[OF _ ys] by (intro eq_vecI, auto simp: field_simps sum_distrib_right[symmetric] conv_c) hence "convex_lincomb_list c ?list (y + (zs ! j))" unfolding convex_lincomb_list_def nonneg_lincomb_list_def using conv_c by auto hence "y + (zs ! j) ∈ convex_hull_list ?list" unfolding convex_hull_list_def by auto with finite_convex_hull_iff_convex_hull_list[OF set refl] have "(y + zs ! j) ∈ convex_hull ?set" by auto also have "… ⊆ convex_hull (A + B)" by (rule convex_hull_mono, insert mem ys ysA zsB, force simp: set_plus_def) finally have "x ∈ convex_hull (A + B)" unfolding x . } note step1 = this { let ?list = "map ((+) y) zs" let ?set = "set ?list" have set: "?set ⊆ carrier_vec n" using zs B y by auto have lin_map: "lincomb_list d ?list ∈ carrier_vec n" by (intro lincomb_list_carrier[OF set]) have [simp]: "i < n ⟹ (∑j = 0..<length zs. d j * (y + zs ! j) $ i) = (∑j = 0..<length zs. d j * (y $ i + zs ! j $ i))" for i by (rule sum.cong, insert zs[unfolded set_conv_nth] y, auto) have "y + z = lincomb_list d ?list" unfolding zid using y zs lin_map lincomb_list_index[OF _ set] lincomb_list_index[OF _ zs] set lincomb_list_carrier[OF zs, of d] zs[unfolded set_conv_nth] by (intro eq_vecI, auto simp: field_simps sum_distrib_right[symmetric] conv_d) hence "convex_lincomb_list d ?list x" unfolding x unfolding convex_lincomb_list_def nonneg_lincomb_list_def using conv_d by auto hence "x ∈ convex_hull_list ?list" unfolding convex_hull_list_def by auto with finite_convex_hull_iff_convex_hull_list[OF set refl] have "x ∈ convex_hull ?set" by auto also have "… ⊆ convex_hull (convex_hull (A + B))" by (rule convex_hull_mono, insert step1, auto) also have "… = convex_hull (A + B)" by (rule convex_convex_hull[OF convex_hulls_are_convex], intro sum_carrier_vec A B) finally show "x ∈ convex_hull (A + B)" . } qed qed lemma convex_hull_in_cone: "convex_hull C ⊆ cone C" unfolding convex_hull_def cone_def convex_lincomb_def finite_cone_def by auto lemma convex_cone: assumes C: "C ⊆ carrier_vec n" shows "convex (cone C)" unfolding convex_def using convex_hull_in_cone set_in_convex_hull[OF cone_carrier[OF C]] cone_cone[OF C] by blast end end