section ‹Cones› text ‹We define the notions like cone, polyhedral cone, etc. and prove some basic facts about them.› theory Cone imports Basis_Extension Missing_VS_Connect Integral_Bounded_Vectors begin context gram_schmidt begin definition "nonneg_lincomb c Vs b = (lincomb c Vs = b ∧ c ` Vs ⊆ {x. x ≥ 0})" definition "nonneg_lincomb_list c Vs b = (lincomb_list c Vs = b ∧ (∀ i < length Vs. c i ≥ 0))" definition finite_cone :: "'a vec set ⇒ 'a vec set" where "finite_cone Vs = ({ b. ∃ c. nonneg_lincomb c (if finite Vs then Vs else {}) b})" definition cone :: "'a vec set ⇒ 'a vec set" where "cone Vs = ({ x. ∃ Ws. finite Ws ∧ Ws ⊆ Vs ∧ x ∈ finite_cone Ws})" definition cone_list :: "'a vec list ⇒ 'a vec set" where "cone_list Vs = {b. ∃c. nonneg_lincomb_list c Vs b}" lemma finite_cone_iff_cone_list: assumes Vs: "Vs ⊆ carrier_vec n" and id: "Vs = set Vsl" shows "finite_cone Vs = cone_list Vsl" proof - have fin: "finite Vs" unfolding id by auto from Vs id have Vsl: "set Vsl ⊆ carrier_vec n" by auto { fix c b assume b: "lincomb c Vs = b" and c: "c ` Vs ⊆ {x. x ≥ 0}" from lincomb_as_lincomb_list[OF Vsl, of c] have b: "lincomb_list (λi. if ∃j<i. Vsl ! i = Vsl ! j then 0 else c (Vsl ! i)) Vsl = b" unfolding b[symmetric] id by simp have "∃ c. nonneg_lincomb_list c Vsl b" unfolding nonneg_lincomb_list_def apply (intro exI conjI, rule b) by (insert c, auto simp: set_conv_nth id) } moreover { fix c b assume b: "lincomb_list c Vsl = b" and c: "(∀ i < length Vsl. c i ≥ 0)" have "nonneg_lincomb (mk_coeff Vsl c) Vs b" unfolding b[symmetric] nonneg_lincomb_def apply (subst lincomb_list_as_lincomb[OF Vsl]) by (insert c, auto simp: id mk_coeff_def intro!: sum_list_nonneg) hence "∃ c. nonneg_lincomb c Vs b" by blast } ultimately show ?thesis unfolding finite_cone_def cone_list_def nonneg_lincomb_def nonneg_lincomb_list_def using fin by auto qed lemma cone_alt_def: assumes Vs: "Vs ⊆ carrier_vec n" shows "cone Vs = ({ x. ∃ Ws. set Ws ⊆ Vs ∧ x ∈ cone_list Ws})" unfolding cone_def proof (intro Collect_cong iffI) fix x assume "∃Ws. finite Ws ∧ Ws ⊆ Vs ∧ x ∈ finite_cone Ws" then obtain Ws where *: "finite Ws" "Ws ⊆ Vs" "x ∈ finite_cone Ws" by auto from finite_list[OF *(1)] obtain Wsl where id: "Ws = set Wsl" by auto from finite_cone_iff_cone_list[OF _ this] *(2-3) Vs have "x ∈ cone_list Wsl" by auto with *(2) id show "∃Wsl. set Wsl ⊆ Vs ∧ x ∈ cone_list Wsl" by blast next fix x assume "∃Wsl. set Wsl ⊆ Vs ∧ x ∈ cone_list Wsl" then obtain Wsl where "set Wsl ⊆ Vs" "x ∈ cone_list Wsl" by auto thus "∃Ws. finite Ws ∧ Ws ⊆ Vs ∧ x ∈ finite_cone Ws" using Vs by (intro exI[of _ "set Wsl"], subst finite_cone_iff_cone_list, auto) qed lemma cone_mono: "Vs ⊆ Ws ⟹ cone Vs ⊆ cone Ws" unfolding cone_def by blast lemma finite_cone_mono: assumes fin: "finite Ws" and Ws: "Ws ⊆ carrier_vec n" and sub: "Vs ⊆ Ws" shows "finite_cone Vs ⊆ finite_cone Ws" proof fix b assume "b ∈ finite_cone Vs" then obtain c where b: "b = lincomb c Vs" and c: "c ` Vs ⊆ {x. x ≥ 0}" unfolding finite_cone_def nonneg_lincomb_def using finite_subset[OF sub fin] by auto define d where "d = (λ v. if v ∈ Vs then c v else 0)" from c have d: "d ` Ws ⊆ {x. x ≥ 0}" unfolding d_def by auto have "lincomb d Ws = lincomb d (Ws - Vs) + lincomb d Vs" by (rule lincomb_vec_diff_add[OF Ws sub fin], auto) also have "lincomb d Vs = lincomb c Vs" by (rule lincomb_cong, insert Ws sub, auto simp: d_def) also have "lincomb d (Ws - Vs) = 0⇩_{v}n" by (rule lincomb_zero, insert Ws sub, auto simp: d_def) also have "0⇩_{v}n + lincomb c Vs = lincomb c Vs" using Ws sub by auto also have "… = b" unfolding b by simp finally have "b = lincomb d Ws" by auto then show "b ∈ finite_cone Ws" using d fin unfolding finite_cone_def nonneg_lincomb_def by auto qed lemma finite_cone_carrier: "A ⊆ carrier_vec n ⟹ finite_cone A ⊆ carrier_vec n" unfolding finite_cone_def nonneg_lincomb_def by auto lemma cone_carrier: "A ⊆ carrier_vec n ⟹ cone A ⊆ carrier_vec n" using finite_cone_carrier unfolding cone_def by blast lemma cone_iff_finite_cone: assumes A: "A ⊆ carrier_vec n" and fin: "finite A" shows "cone A = finite_cone A" proof show "finite_cone A ⊆ cone A" unfolding cone_def using fin by auto show "cone A ⊆ finite_cone A" unfolding cone_def using fin finite_cone_mono[OF fin A] by auto qed lemma set_in_finite_cone: assumes Vs: "Vs ⊆ carrier_vec n" and fin: "finite Vs" shows "Vs ⊆ finite_cone Vs" proof fix x assume x: "x ∈ Vs" show "x ∈ finite_cone Vs" unfolding finite_cone_def proof let ?c = "λ y. if x = y then 1 else 0 :: 'a" have Vsx: "Vs - {x} ⊆ carrier_vec n" using Vs by auto have "lincomb ?c Vs = x + lincomb ?c (Vs - {x})" using lincomb_del2 x Vs fin by auto also have "lincomb ?c (Vs - {x}) = 0⇩_{v}n" using lincomb_zero Vsx by auto also have "x + 0⇩_{v}n = x " using M.r_zero Vs x by auto finally have "lincomb ?c Vs = x" by auto moreover have "?c ` Vs ⊆ {z. z ≥ 0}" by auto ultimately show "∃c. nonneg_lincomb c (if finite Vs then Vs else {}) x" unfolding nonneg_lincomb_def using fin by auto qed qed lemma set_in_cone: assumes Vs: "Vs ⊆ carrier_vec n" shows "Vs ⊆ cone Vs" proof fix x assume x: "x ∈ Vs" show "x ∈ cone Vs" unfolding cone_def proof (intro CollectI exI) have "x ∈ carrier_vec n" using Vs x by auto then have "x ∈ finite_cone {x}" using set_in_finite_cone by auto then show "finite {x} ∧ {x} ⊆ Vs ∧ x ∈ finite_cone {x}" using x by auto qed qed lemma zero_in_finite_cone: assumes Vs: "Vs ⊆ carrier_vec n" shows "0⇩_{v}n ∈ finite_cone Vs" proof - let ?Vs = "(if finite Vs then Vs else {})" have "lincomb (λ x. 0 :: 'a) ?Vs = 0⇩_{v}n" using lincomb_zero Vs by auto moreover have "(λ x. 0 :: 'a) ` ?Vs ⊆ {y. y ≥ 0}" by auto ultimately show ?thesis unfolding finite_cone_def nonneg_lincomb_def by blast qed lemma lincomb_in_finite_cone: assumes "x = lincomb l W" and "finite W" and "∀i ∈ W . l i ≥ 0" and "W ⊆ carrier_vec n" shows "x ∈ finite_cone W" using cone_iff_finite_cone assms unfolding finite_cone_def nonneg_lincomb_def by auto lemma lincomb_in_cone: assumes "x = lincomb l W" and "finite W" and "∀i ∈ W . l i ≥ 0" and "W ⊆ carrier_vec n" shows "x ∈ cone W" using cone_iff_finite_cone assms unfolding finite_cone_def nonneg_lincomb_def by auto lemma zero_in_cone: "0⇩_{v}n ∈ cone Vs" proof - have "finite {}" by auto moreover have "{} ⊆ cone Vs" by auto moreover have "0⇩_{v}n ∈ finite_cone {}" using zero_in_finite_cone by auto ultimately show ?thesis unfolding cone_def by blast qed lemma cone_smult: assumes a: "a ≥ 0" and Vs: "Vs ⊆ carrier_vec n" and x: "x ∈ cone Vs" shows "a ⋅⇩_{v}x ∈ cone Vs" proof - from x Vs obtain Ws c where Ws: "Ws ⊆ Vs" and fin: "finite Ws" and "nonneg_lincomb c Ws x" unfolding cone_def finite_cone_def by auto then have "nonneg_lincomb (λ w. a * c w) Ws (a ⋅⇩_{v}x)" unfolding nonneg_lincomb_def using a lincomb_distrib Vs by auto then show ?thesis using Ws fin unfolding cone_def finite_cone_def by auto qed lemma finite_cone_empty[simp]: "finite_cone {} = {0⇩_{v}n}" by (auto simp: finite_cone_def nonneg_lincomb_def) lemma cone_empty[simp]: "cone {} = {0⇩_{v}n}" unfolding cone_def by simp lemma cone_elem_sum: assumes Vs: "Vs ⊆ carrier_vec n" and x: "x ∈ cone Vs" and y: "y ∈ cone Vs" shows "x + y ∈ cone Vs" proof - obtain Xs where Xs: "Xs ⊆ Vs" and fin_Xs: "finite Xs" and Xs_cone: "x ∈ finite_cone Xs" using Vs x unfolding cone_def by auto obtain Ys where Ys: "Ys ⊆ Vs" and fin_Ys: "finite Ys" and Ys_cone: "y ∈ finite_cone Ys" using Vs y unfolding cone_def by auto have "x ∈ finite_cone (Xs ∪ Ys)" and "y ∈ finite_cone (Xs ∪ Ys)" using finite_cone_mono fin_Xs fin_Ys Xs Ys Vs Xs_cone Ys_cone by (blast, blast) then obtain cx cy where "nonneg_lincomb cx (Xs ∪ Ys) x" and "nonneg_lincomb cy (Xs ∪ Ys) y" unfolding finite_cone_def using fin_Xs fin_Ys by auto hence "nonneg_lincomb (λ v. cx v + cy v) (Xs ∪ Ys) (x + y)" unfolding nonneg_lincomb_def using lincomb_sum[of "Xs ∪ Ys" cx cy] fin_Xs fin_Ys Xs Ys Vs by fastforce hence "x + y ∈ finite_cone (Xs ∪ Ys)" unfolding finite_cone_def using fin_Xs fin_Ys by auto thus ?thesis unfolding cone_def using fin_Xs fin_Ys Xs Ys by auto qed lemma cone_cone: assumes Vs: "Vs ⊆ carrier_vec n" shows "cone (cone Vs) = cone Vs" proof show "cone Vs ⊆ cone (cone Vs)" by (rule set_in_cone[OF cone_carrier[OF Vs]]) next show "cone (cone Vs) ⊆ cone Vs" proof fix x assume x: "x ∈ cone (cone Vs)" then obtain Ws c where Ws: "set Ws ⊆ cone Vs" and c: "nonneg_lincomb_list c Ws x" using cone_alt_def Vs cone_carrier unfolding cone_list_def by auto have "set Ws ⊆ cone Vs ⟹ nonneg_lincomb_list c Ws x ⟹ x ∈ cone Vs" proof (induction Ws arbitrary: x c) case Nil hence "x = 0⇩_{v}n" unfolding nonneg_lincomb_list_def by auto thus "x ∈ cone Vs" using zero_in_cone by auto next case (Cons a Ws) have "a ∈ cone Vs" using Cons.prems(1) by auto moreover have "c 0 ≥ 0" using Cons.prems(2) unfolding nonneg_lincomb_list_def by fastforce ultimately have "c 0 ⋅⇩_{v}a ∈ cone Vs" using cone_smult Vs by auto moreover have "lincomb_list (c ∘ Suc) Ws ∈ cone Vs" using Cons unfolding nonneg_lincomb_list_def by fastforce moreover have "x = c 0 ⋅⇩_{v}a + lincomb_list (c ∘ Suc) Ws" using Cons.prems(2) unfolding nonneg_lincomb_list_def by auto ultimately show "x ∈ cone Vs" using cone_elem_sum Vs by auto qed thus "x ∈ cone Vs" using Ws c by auto qed qed lemma cone_smult_basis: assumes Vs: "Vs ⊆ carrier_vec n" and l: "l ` Vs ⊆ {x. x > 0}" shows "cone {l v ⋅⇩_{v}v | v . v ∈ Vs} = cone Vs" proof have "{l v ⋅⇩_{v}v |v. v ∈ Vs} ⊆ cone Vs" proof fix x assume "x ∈ {l v ⋅⇩_{v}v | v. v ∈ Vs}" then obtain v where "v ∈ Vs" and "x = l v ⋅⇩_{v}v" by auto thus "x ∈ cone Vs" using set_in_cone[OF Vs] cone_smult[OF _ Vs, of "l v" v] l by fastforce qed thus "cone {l v ⋅⇩_{v}v | v. v ∈ Vs} ⊆ cone Vs" using cone_mono cone_cone[OF Vs] by blast next have lVs: "{l v ⋅⇩_{v}v | v. v ∈ Vs} ⊆ carrier_vec n" using Vs by auto have "Vs ⊆ cone {l v ⋅⇩_{v}v | v. v ∈ Vs}" proof fix v assume v: "v ∈ Vs" hence "l v ⋅⇩_{v}v ∈ cone {l v ⋅⇩_{v}v | v. v ∈ Vs}" using set_in_cone[OF lVs] by auto moreover have "1 / l v > 0" using l v by auto ultimately have "(1 / l v) ⋅⇩_{v}(l v ⋅⇩_{v}v) ∈ cone {l v ⋅⇩_{v}v | v. v ∈ Vs}" using cone_smult[OF _ lVs] by auto also have "(1 / l v) ⋅⇩_{v}(l v ⋅⇩_{v}v) = v" using l v by(auto simp add: smult_smult_assoc) finally show "v ∈ cone {l v ⋅⇩_{v}v | v. v ∈ Vs}" by auto qed thus "cone Vs ⊆ cone {l v ⋅⇩_{v}v | v. v ∈ Vs}" using cone_mono cone_cone[OF lVs] by blast qed lemma cone_add_cone: assumes C: "C ⊆ carrier_vec n" shows "cone C + cone C = cone C" proof note CC = cone_carrier[OF C] have "cone C = cone C + {0⇩_{v}n}" by (subst add_0_right_vecset[OF CC], simp) also have "… ⊆ cone C + cone C" by (rule set_plus_mono2, insert zero_in_cone, auto) finally show "cone C ⊆ cone C + cone C" by auto from cone_elem_sum[OF C] show "cone C + cone C ⊆ cone C" by (auto elim!: set_plus_elim) qed lemma orthogonal_cone: assumes X: "X ⊆ carrier_vec n" and W: "W ⊆ carrier_vec n" and finX: "finite X" and spanLW: "span (set Ls ∪ W) = carrier_vec n" and ortho: "⋀ w x. w ∈ W ⟹ x ∈ set Ls ⟹ w ∙ x = 0" and WWs: "W = set Ws" and spanL: "span (set Ls) = span X" and LX: "set Ls ⊆ X" and lin_Ls_Bs: "lin_indpt_list (Ls @ Bs)" and len_Ls_Bs: "length (Ls @ Bs) = n" shows "cone (X ∪ set Bs) ∩ {x ∈ carrier_vec n. ∀w∈W. w ∙ x = 0} = cone X" "⋀ x. ∀w∈W. w ∙ x = 0 ⟹ Z ⊆ X ⟹ B ⊆ set Bs ⟹ x = lincomb c (Z ∪ B) ⟹ x = lincomb c (Z - B)" proof - from WWs have finW: "finite W" by auto define Y where "Y = X ∪ set Bs" from lin_Ls_Bs[unfolded lin_indpt_list_def] have Ls: "set Ls ⊆ carrier_vec n" and Bs: "set Bs ⊆ carrier_vec n" and distLsBs: "distinct (Ls @ Bs)" and lin: "lin_indpt (set (Ls @ Bs))" by auto have LW: "set Ls ∩ W = {}" proof (rule ccontr) assume "¬ ?thesis" then obtain x where xX: "x ∈ set Ls" and xW: "x ∈ W" by auto from ortho[OF xW xX] have "x ∙ x = 0" by auto hence "sq_norm x = 0" by (auto simp: sq_norm_vec_as_cscalar_prod) with vs_zero_lin_dep[OF _ lin] xX Ls Bs show False by auto qed have Y: "Y ⊆ carrier_vec n" using X Bs unfolding Y_def by auto have CLB: "carrier_vec n = span (set (Ls @ Bs))" using lin_Ls_Bs len_Ls_Bs lin_indpt_list_length_eq_n by blast also have "… ⊆ span Y" by (rule span_is_monotone, insert LX, auto simp: Y_def) finally have span: "span Y = carrier_vec n" using Y by auto have finY: "finite Y" using finX finW unfolding Y_def by auto { fix x Z B d assume xX: "∀w∈W. w ∙ x = 0" and ZX: "Z ⊆ X" and B: "B ⊆ set Bs" and xd: "x = lincomb d (Z ∪ B)" from ZX B X Bs have ZB: "Z ∪ B ⊆ carrier_vec n" by auto with xd have x: "x ∈ carrier_vec n" by auto from xX W have w0: "w ∈ W ⟹ w ∙ x = 0" for w by auto from finite_in_span[OF _ _ x[folded spanLW]] Ls X W finW finX obtain c where xc: "x = lincomb c (set Ls ∪ W)" by auto have "x = lincomb c (set Ls ∪ W)" unfolding xc by auto also have "… = lincomb c (set Ls) + lincomb c W" by (rule lincomb_union, insert X LX W LW finW, auto) finally have xsum: "x = lincomb c (set Ls) + lincomb c W" . { fix w assume wW: "w ∈ W" with W have w: "w ∈ carrier_vec n" by auto from w0[OF wW, unfolded xsum] have "0 = w ∙ (lincomb c (set Ls) + lincomb c W)" by simp also have "… = w ∙ lincomb c (set Ls) + w ∙ lincomb c W" by (rule scalar_prod_add_distrib[OF w], insert Ls W, auto) also have "w ∙ lincomb c (set Ls) = 0" using ortho[OF wW] by (subst lincomb_scalar_prod_right[OF Ls w], auto) finally have "w ∙ lincomb c W = 0" by simp } hence "lincomb c W ∙ lincomb c W = 0" using W by (subst lincomb_scalar_prod_left, auto) hence "sq_norm (lincomb c W) = 0" by (auto simp: sq_norm_vec_as_cscalar_prod) hence 0: "lincomb c W = 0⇩_{v}n" using lincomb_closed[OF W, of c] by simp have xc: "x = lincomb c (set Ls)" unfolding xsum 0 using Ls by auto hence xL: "x ∈ span (set Ls)" by auto let ?X = "Z - B" have "lincomb d ?X ∈ span X" using finite_subset[OF _ finX, of ?X] X ZX by auto from finite_in_span[OF finite_set Ls this[folded spanL]] obtain e where ed: "lincomb e (set Ls) = lincomb d ?X" by auto from B finite_subset[OF B] have finB: "finite B" by auto from B Bs have BC: "B ⊆ carrier_vec n" by auto define f where "f = (λ x. if x ∈ set Bs then if x ∈ B then d x else 0 else if x ∈ set Ls then e x else undefined)" have "x = lincomb d (?X ∪ B)" unfolding xd by auto also have "… = lincomb d ?X + lincomb d B" by (rule lincomb_union[OF _ _ _ finite_subset[OF _ finX]], insert ZX X finB B Bs, auto) finally have xd: "x = lincomb d ?X + lincomb d B" . also have "… = lincomb e (set Ls) + lincomb d B" unfolding ed by auto also have "lincomb e (set Ls) = lincomb f (set Ls)" by (rule lincomb_cong[OF _ Ls], insert distLsBs, auto simp: f_def) also have "lincomb d B = lincomb f B" by (rule lincomb_cong[OF _ BC], insert B, auto simp: f_def) also have "lincomb f B = lincomb f (B ∪ (set Bs - B))" by (subst lincomb_clean, insert finB Bs B, auto simp: f_def) also have "B ∪ (set Bs - B) = set Bs" using B by auto finally have "x = lincomb f (set Ls) + lincomb f (set Bs)" by auto also have "lincomb f (set Ls) + lincomb f (set Bs) = lincomb f (set (Ls @ Bs))" by (subst lincomb_union[symmetric], insert Ls distLsBs Bs, auto) finally have "x = lincomb f (set (Ls @ Bs))" . hence f: "f ∈ set (Ls @ Bs) →⇩_{E}UNIV ∧ lincomb f (set (Ls @ Bs)) = x" by (auto simp: f_def split: if_splits) from finite_in_span[OF finite_set Ls xL] obtain g where xg: "x = lincomb g (set Ls)" by auto define h where "h = (λ x. if x ∈ set Bs then 0 else if x ∈ set Ls then g x else undefined)" have "x = lincomb h (set Ls)" unfolding xg by (rule lincomb_cong[OF _ Ls], insert distLsBs, auto simp: h_def) also have "… = lincomb h (set Ls) + 0⇩_{v}n" using Ls by auto also have "0⇩_{v}n = lincomb h (set Bs)" by (rule lincomb_zero[symmetric, OF Bs], auto simp: h_def) also have "lincomb h (set Ls) + lincomb h (set Bs) = lincomb h (set (Ls @ Bs))" by (subst lincomb_union[symmetric], insert Ls Bs distLsBs, auto) finally have "x = lincomb h (set (Ls @ Bs))" . hence h: "h ∈ set (Ls @ Bs) →⇩_{E}UNIV ∧ lincomb h (set (Ls @ Bs)) = x" by (auto simp: h_def split: if_splits) have basis: "basis (set (Ls @ Bs))" using lin_Ls_Bs[unfolded lin_indpt_list_def] len_Ls_Bs using CLB basis_def by blast from Ls Bs have "set (Ls @ Bs) ⊆ carrier_vec n" by auto from basis[unfolded basis_criterion[OF finite_set this], rule_format, OF x] f h have fh: "f = h" by auto hence "⋀ x. x ∈ set Bs ⟹ f x = 0" unfolding h_def by auto hence "⋀ x. x ∈ B ⟹ d x = 0" unfolding f_def using B by force thus "x = lincomb d ?X" unfolding xd by (subst (2) lincomb_zero, insert BC ZB X, auto intro!: M.r_zero) } note main = this have "cone Y ∩ {x ∈ carrier_vec n. ∀w∈W. w ∙ x = 0} = cone X" (is "?I = _") proof { fix x assume xX: "x ∈ cone X" with cone_carrier[OF X] have x: "x ∈ carrier_vec n" by auto have "X ⊆ Y" unfolding Y_def by auto from cone_mono[OF this] xX have xY: "x ∈ cone Y" by auto from cone_iff_finite_cone[OF X finX] xX have "x ∈ finite_cone X" by auto from this[unfolded finite_cone_def nonneg_lincomb_def] finX obtain c where "x = lincomb c X" by auto with finX X have "x ∈ span X" by auto with spanL have "x ∈ span (set Ls)" by auto from finite_in_span[OF _ Ls this] obtain c where xc: "x = lincomb c (set Ls)" by auto { fix w assume wW: "w ∈ W" hence w: "w ∈ carrier_vec n" using W by auto have "w ∙ x = 0" unfolding xc using ortho[OF wW] by (subst lincomb_scalar_prod_right[OF Ls w], auto) } with xY x have "x ∈ ?I" by blast } thus "cone X ⊆ ?I" by blast { fix x let ?X = "X - set Bs" assume "x ∈ ?I" with cone_carrier[OF Y] cone_iff_finite_cone[OF Y finY] have xY: "x ∈ finite_cone Y" and x: "x ∈ carrier_vec n" and w0: "⋀ w. w ∈ W ⟹ w ∙ x = 0" by auto from xY[unfolded finite_cone_def nonneg_lincomb_def] finY obtain d where xd: "x = lincomb d Y" and nonneg: "d ` Y ⊆ Collect ((≤) 0)" by auto from main[OF _ _ _ xd[unfolded Y_def]] w0 have "x = lincomb d ?X" by auto hence "nonneg_lincomb d ?X x" unfolding nonneg_lincomb_def using nonneg[unfolded Y_def] by auto hence "x ∈ finite_cone ?X" using finX unfolding finite_cone_def by auto hence "x ∈ cone X" using finite_subset[OF _ finX, of ?X] unfolding cone_def by blast } then show "?I ⊆ cone X" by auto qed thus "cone (X ∪ set Bs) ∩ {x ∈ carrier_vec n. ∀w∈W. w ∙ x = 0} = cone X" unfolding Y_def . qed definition "polyhedral_cone (A :: 'a mat) = { x . x ∈ carrier_vec n ∧ A *⇩_{v}x ≤ 0⇩_{v}(dim_row A)}" lemma polyhedral_cone_carrier: assumes "A ∈ carrier_mat nr n" shows "polyhedral_cone A ⊆ carrier_vec n" using assms unfolding polyhedral_cone_def by auto lemma cone_in_polyhedral_cone: assumes CA: "C ⊆ polyhedral_cone A" and A: "A ∈ carrier_mat nr n" shows "cone C ⊆ polyhedral_cone A" proof interpret nr: gram_schmidt nr "TYPE ('a)". from polyhedral_cone_carrier[OF A] assms(1) have C: "C ⊆ carrier_vec n" by auto fix x assume x: "x ∈ cone C" then have xn: "x ∈ carrier_vec n" using cone_carrier[OF C] by auto from x[unfolded cone_alt_def[OF C] cone_list_def nonneg_lincomb_list_def] obtain ll Ds where l0: "lincomb_list ll Ds = x" and l1: "∀i<length Ds. 0 ≤ ll i" and DsC: "set Ds ⊆ C" by auto from DsC C have Ds: "set Ds ⊆ carrier_vec n" by auto have "A *⇩_{v}x = A *⇩_{v}(lincomb_list ll Ds)" using l0 by auto also have "… = nr.lincomb_list ll (map (λ d. A *⇩_{v}d) Ds)" proof - have one: " ∀w∈set Ds. dim_vec w = n" using DsC C by auto have two: "∀w∈set (map ((*⇩_{v}) A) Ds). dim_vec w = nr" using A DsC C by auto show "A *⇩_{v}lincomb_list ll Ds = nr.lincomb_list ll (map ((*⇩_{v}) A) Ds)" unfolding lincomb_list_as_mat_mult[OF one] nr.lincomb_list_as_mat_mult[OF two] length_map proof (subst assoc_mult_mat_vec[symmetric, OF A], force+, rule arg_cong[of _ _ "λ x. x *⇩_{v}_"]) show "A * mat_of_cols n Ds = mat_of_cols nr (map ((*⇩_{v}) A) Ds)" unfolding mat_of_cols_def by (intro eq_matI, insert A Ds[unfolded set_conv_nth], (force intro!: arg_cong[of _ _ "λ x. row A _ ∙ x"])+) qed qed also have "… ≤ 0⇩_{v}nr" proof (intro lesseq_vecI[of _ nr]) have *: "set (map ((*⇩_{v}) A) Ds) ⊆ carrier_vec nr" using A Ds by auto show Carr: "nr.lincomb_list ll (map ((*⇩_{v}) A) Ds) ∈ carrier_vec nr" by (intro nr.lincomb_list_carrier[OF *]) fix i assume i: "i < nr" from CA[unfolded polyhedral_cone_def] A have l2: "x ∈ C ⟹ A *⇩_{v}x ≤ 0⇩_{v}nr" for x by auto show "nr.lincomb_list ll (map ((*⇩_{v}) A) Ds) $ i ≤ 0⇩_{v}nr $ i" unfolding subst nr.lincomb_list_index[OF i *] length_map index_zero_vec(1)[OF i] proof (intro sum_nonpos mult_nonneg_nonpos) fix j assume "j ∈ {0..<length Ds}" hence j: "j < length Ds" by auto from j show "0 ≤ ll j" using l1 by auto from j have "Ds ! j ∈ C" using DsC by auto from l2[OF this] have l2: "A *⇩_{v}Ds ! j ≤ 0⇩_{v}nr" by auto from lesseq_vecD[OF _ this i] i have "(A *⇩_{v}Ds ! j) $ i ≤ 0" by auto thus "map ((*⇩_{v}) A) Ds ! j $ i ≤ 0" using j i by auto qed qed auto finally show "x ∈ polyhedral_cone A" unfolding polyhedral_cone_def using A xn by auto qed lemma bounded_cone_is_zero: assumes Ccarr: "C ⊆ carrier_vec n" and bnd: "cone C ⊆ Bounded_vec bnd" shows "cone C = {0⇩_{v}n}" proof(rule ccontr) assume "¬ ?thesis" then obtain v where vC: "v ∈ cone C" and vnz: "v ≠ 0⇩_{v}n" using zero_in_cone assms by auto have vcarr: "v ∈ carrier_vec n" using vC Ccarr cone_carrier by blast from vnz vcarr obtain i where i_le_n: "i < dim_vec v" and vinz: "v $ i ≠ 0" by force define M where "M = (1 / (v $ i) * (bnd + 1))" have abs_ge_bnd: "abs (M * (v $ i)) > bnd" unfolding M_def by (simp add: vinz) have aMvC: "(abs M) ⋅⇩_{v}v ∈ cone C" using cone_smult[OF _ Ccarr vC] abs_ge_bnd by simp have "¬(abs (abs M * (v $ i)) ≤ bnd)" using abs_ge_bnd by simp hence "(abs M) ⋅⇩_{v}v ∉ Bounded_vec bnd" unfolding Bounded_vec_def using i_le_n aMvC by auto thus False using aMvC bnd by auto qed lemma cone_of_cols: fixes A :: "'a mat" and b :: "'a vec" assumes A: "A ∈ carrier_mat n nr" and b: "b ∈ carrier_vec n" shows "b ∈ cone (set (cols A)) ⟷ (∃ x. x ≥ 0⇩_{v}nr ∧ A *⇩_{v}x = b)" proof - let ?C = "set (cols A)" from A have C: "?C ⊆ carrier_vec n" and C': " ∀w∈set (cols A). dim_vec w = n" unfolding cols_def by auto have id: "finite ?C = True" "length (cols A) = nr" using A by auto have Aid: "mat_of_cols n (cols A) = A" using A unfolding mat_of_cols_def by (intro eq_matI, auto) show ?thesis unfolding cone_iff_finite_cone[OF C finite_set] finite_cone_iff_cone_list[OF C refl] unfolding cone_list_def nonneg_lincomb_list_def mem_Collect_eq id unfolding lincomb_list_as_mat_mult[OF C'] id Aid proof - { fix x assume "x≥0⇩_{v}nr" "A *⇩_{v}x = b" hence "∃c. A *⇩_{v}vec nr c = b ∧ (∀i<nr. 0 ≤ c i)" using A b by (intro exI[of _ "λ i. x $ i"], auto simp: less_eq_vec_def intro!: arg_cong[of _ _ "(*⇩_{v}) A"]) } moreover { fix c assume "A *⇩_{v}vec nr c = b" "(∀i<nr. 0 ≤ c i)" hence "∃ x. x≥0⇩_{v}nr ∧ A *⇩_{v}x = b" by (intro exI[of _ "vec nr c"], auto simp: less_eq_vec_def) } ultimately show "(∃c. A *⇩_{v}vec nr c = b ∧ (∀i<nr. 0 ≤ c i)) = (∃x≥0⇩_{v}nr. A *⇩_{v}x = b)" by blast qed qed end end