section ‹The Fundamental Theorem of Linear Inequalities›
text ‹The theorem states that for a given set of vectors A and vector b, either
b is in the cone of a linear independent subset of A, or
there is a hyperplane that contains span(A,b)-1 linearly independent vectors of A
that separates A from b. We prove this theorem and derive some consequences, e.g.,
Caratheodory's theorem that b is the cone of A iff b is in the cone of a linear
independent subset of A.›
theory Fundamental_Theorem_Linear_Inequalities
imports
Cone
Normal_Vector
Dim_Span
begin
context gram_schmidt
begin
text ‹The mentions equivances A-D are:
▪ A: b is in the cone of vectors A,
▪ B: b is in the cone of a subset of linear independent of vectors A,
▪ C: there is no separating hyperplane of b and the vectors A,
which contains dim many linear independent vectors of A
▪ D: there is no separating hyperplane of b and the vectors A›
lemma fundamental_theorem_of_linear_inequalities_A_imp_D:
assumes A: "A ⊆ carrier_vec n"
and fin: "finite A"
and b: "b ∈ cone A"
shows "∄ c. c ∈ carrier_vec n ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0"
proof
assume "∃ c. c ∈ carrier_vec n ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0"
then obtain c where c: "c ∈ carrier_vec n"
and ai: "⋀ ai. ai ∈ A ⟹ c ∙ ai ≥ 0"
and cb: "c ∙ b < 0" by auto
from b[unfolded cone_def nonneg_lincomb_def finite_cone_def]
obtain l AA where bc: "b = lincomb l AA" and l: "l ` AA ⊆ {x. x ≥ 0}" and AA: "AA ⊆ A" by auto
from cone_carrier[OF A] b have b: "b ∈ carrier_vec n" by auto
have "0 ≤ (∑ai∈AA. l ai * (c ∙ ai))"
by (intro sum_nonneg mult_nonneg_nonneg, insert l ai AA, auto)
also have "… = (∑ai∈AA. l ai * (ai ∙ c))"
by (rule sum.cong, insert c A AA comm_scalar_prod, force+)
also have "… = (∑ai∈AA. ((l ai ⋅⇩v ai) ∙ c))"
by (rule sum.cong, insert smult_scalar_prod_distrib c A AA, auto)
also have "… = b ∙ c" unfolding bc lincomb_def
by (subst finsum_scalar_prod_sum[symmetric], insert c A AA, auto)
also have "… = c ∙ b" using comm_scalar_prod b c by auto
also have "… < 0" by fact
finally show False by simp
qed
text ‹The difficult direction is that C implies B. To this end we follow the
proof that at least one of B and the negation of C is satisfied.›
context
fixes a :: "nat ⇒ 'a vec"
and b :: "'a vec"
and m :: nat
assumes a: "a ` {0 ..< m} ⊆ carrier_vec n"
and inj_a: "inj_on a {0 ..< m}"
and b: "b ∈ carrier_vec n"
and full_span: "span (a ` {0 ..< m}) = carrier_vec n"
begin
private definition "goal = ((∃ I. I ⊆ {0 ..< m} ∧ card (a ` I) = n ∧ lin_indpt (a ` I) ∧ b ∈ finite_cone (a ` I))
∨ (∃ c I. I ⊆ {0 ..< m} ∧ c ∈ {normal_vector (a ` I), - normal_vector (a ` I)} ∧ Suc (card (a ` I)) = n
∧ lin_indpt (a ` I) ∧ (∀ i < m. c ∙ a i ≥ 0) ∧ c ∙ b < 0))"
private lemma card_a_I[simp]: "I ⊆ {0 ..< m} ⟹ card (a ` I) = card I"
by (smt inj_a card_image inj_on_image_eq_iff subset_image_inj subset_refl subset_trans)
private lemma in_a_I[simp]: "I ⊆ {0 ..< m} ⟹ i < m ⟹ (a i ∈ a ` I) = (i ∈ I)"
using inj_a
by (meson atLeastLessThan_iff image_eqI inj_on_image_mem_iff_alt zero_le)
private definition "valid_I = { I. card I = n ∧ lin_indpt (a ` I) ∧ I ⊆ {0 ..< m}}"
private definition cond where "cond I I' l c h k ≡
b = lincomb l (a ` I) ∧
h ∈ I ∧ l (a h) < 0 ∧ (∀ h'. h' ∈ I ⟶ h' < h ⟶ l (a h') ≥ 0) ∧
c ∈ carrier_vec n ∧ span (a ` (I - {h})) = { x. x ∈ carrier_vec n ∧ c ∙ x = 0} ∧ c ∙ b < 0 ∧
k < m ∧ c ∙ a k < 0 ∧ (∀ k'. k' < k ⟶ c ∙ a k' ≥ 0) ∧
I' = insert k (I - {h})"
private definition "step_rel = Restr { (I'', I). ∃ l c h k. cond I I'' l c h k } valid_I"
private lemma finite_step_rel: "finite step_rel"
proof (rule finite_subset)
show "step_rel ⊆ (Pow {0 ..< m} × Pow {0 ..< m})" unfolding step_rel_def valid_I_def by auto
qed auto
private lemma acyclic_imp_goal: "acyclic step_rel ⟹ goal"
proof (rule ccontr)
assume ngoal: "¬ goal"
{
fix I
assume I: "I ∈ valid_I"
hence Im: "I ⊆ {0..<m}" and
lin: "lin_indpt (a ` I)" and
cardI: "card I = n"
by (auto simp: valid_I_def)
let ?D = "(a ` I)"
have finD: "finite ?D" using Im infinite_super by blast
have carrD: "?D ⊆ carrier_vec n" using a Im by auto
have cardD: "card ?D = n" using cardI Im by simp
have spanD: "span ?D = carrier_vec n"
by (intro span_carrier_lin_indpt_card_n lin cardD carrD)
obtain lamb where b_is_lincomb: "b = lincomb lamb (a ` I)"
using finite_in_span[OF fin carrD, of b] using spanD b carrD fin_dim lin by auto
define h where "h = (LEAST h. h ∈ I ∧ lamb (a h) < 0)"
have "∃ I'. (I', I) ∈ step_rel"
proof (cases "∀i∈ I . lamb (a i) ≥ 0")
case cond1_T: True
have goal unfolding goal_def
by (intro disjI1 exI[of _ I] conjI lin cardI
lincomb_in_finite_cone[OF b_is_lincomb finD _ carrD], insert cardI Im cond1_T, auto)
with ngoal show ?thesis by auto
next
case cond1_F: False
hence "∃ h. h ∈ I ∧ lamb (a h) < 0" by fastforce
from LeastI_ex[OF this, folded h_def] have h: "h ∈ I" "lamb (a h) < 0" by auto
from not_less_Least[of _ "λ h. h ∈ I ∧ lamb (a h) < 0", folded h_def]
have h_least: "∀ k. k ∈ I ⟶ k < h ⟶ lamb (a k) ≥ 0" by fastforce
obtain I' where I'_def: "I' = I - {h}" by auto
obtain c where c_def: "c = pos_norm_vec (a ` I') (a h)" by auto
let ?D' = "a ` I'"
have I'm: "I' ⊆ {0..<m}" using Im I'_def by auto
have carrD': " ?D' ⊆ carrier_vec n" using a Im I'_def by auto
have finD': "finite (?D')" using Im I'_def subset_eq_atLeast0_lessThan_finite by auto
have D'subs: "?D' ⊆ ?D" using I'_def by auto
have linD': "lin_indpt (?D')" using lin I'_def Im D'subs subset_li_is_li by auto
have D'strictsubs: "?D = ?D' ∪ {a h}" using h I'_def by auto
have h_nin_I: "h ∉ I'" using h I'_def by auto
have ah_nin_D': "a h ∉ ?D'" using h inj_a Im h_nin_I by (subst in_a_I, auto simp: I'_def)
have cardD': "Suc (card (?D')) = n " using cardD ah_nin_D' D'strictsubs finD' by simp
have ah_carr: "a h ∈ carrier_vec n" using h a Im by auto
note pnv = pos_norm_vec[OF carrD' finD' linD' cardD' c_def]
have ah_nin_span: "a h ∉ span ?D'"
using D'strictsubs lin_dep_iff_in_span[OF carrD' linD' ah_carr ah_nin_D'] lin by auto
have cah_ge_zero:"c ∙ a h > 0" and "c ∈ carrier_vec n"
and cnorm: "span ?D' = {x ∈ carrier_vec n. x ∙ c = 0}"
using ah_carr ah_nin_span pnv by auto
have ccarr: "c ∈ carrier_vec n" by fact
have "b ∙ c = lincomb lamb (a ` I) ∙ c" using b_is_lincomb by auto
also have "… = (∑w∈ ?D. lamb w * (w ∙ c))"
using lincomb_scalar_prod_left[OF carrD, of c lamb] pos_norm_vec ccarr by blast
also have "… = lamb (a h) * (a h ∙ c) + (∑w∈ ?D'. lamb w * (w ∙ c))"
using sum.insert[OF finD' ah_nin_D', of lamb] D'strictsubs ah_nin_D' finD' by auto
also have "(∑w∈ ?D'. lamb w * (w ∙ c)) = 0"
apply (rule sum.neutral)
using span_mem[OF carrD', unfolded cnorm] by simp
also have "lamb (a h) * (a h ∙ c) + 0 < 0"
using cah_ge_zero h(2) comm_scalar_prod[OF ah_carr ccarr]
by (auto intro: mult_neg_pos)
finally have cb_le_zero: "c ∙ b < 0" using comm_scalar_prod[OF b ccarr] by auto
show ?thesis
proof (cases "∀i < m . c ∙ a i ≥ 0")
case cond2_T: True
have goal
unfolding goal_def
by (intro disjI2 exI[of _ c] exI[of _ I'] conjI cb_le_zero linD' cond2_T cardD' I'm pnv(4))
with ngoal show ?thesis by auto
next
case cond2_F: False
define k where "k = (LEAST k. k < m ∧ c ∙ a k < 0)"
let ?I'' = "insert k I'"
show ?thesis unfolding step_rel_def
proof (intro exI[of _ ?I''], standard, unfold mem_Collect_eq split, intro exI)
from LeastI_ex[OF ]
have "∃k. k < m ∧ c ∙ a k < 0" using cond2_F by fastforce
from LeastI_ex[OF this, folded k_def] have k: "k < m" "c ∙ a k < 0" by auto
show "cond I ?I'' lamb c h k" unfolding cond_def I'_def[symmetric] cnorm
proof(intro conjI cb_le_zero b_is_lincomb h ccarr h_least refl k)
show "{x ∈ carrier_vec n. x ∙ c = 0} = {x ∈ carrier_vec n. c ∙ x = 0}"
using comm_scalar_prod[OF ccarr] by auto
from not_less_Least[of _ "λ k. k < m ∧ c ∙ a k < 0", folded k_def]
have "∀k' < k . k' > m ∨ c ∙ a k' ≥ 0" using k(1) less_trans not_less by blast
then show "∀k' < k . c ∙ a k' ≥ 0" using k(1) by auto
qed
have "?I'' ∈ valid_I" unfolding valid_I_def
proof(standard, intro conjI)
from k a have ak_carr: "a k ∈ carrier_vec n" by auto
have ak_nin_span: "a k ∉ span ?D'" using k(2) cnorm comm_scalar_prod[OF ak_carr ccarr] by auto
hence ak_nin_D': "a k ∉ ?D'" using span_mem[OF carrD'] by auto
from lin_dep_iff_in_span[OF carrD' linD' ak_carr ak_nin_D']
show "lin_indpt (a ` ?I'')" using ak_nin_span by auto
show "?I'' ⊆ {0..<m}" using I'm k by auto
show "card (insert k I') = n" using cardD' ak_nin_D' finD'
by (metis ‹insert k I' ⊆ {0..<m}› card_a_I card_insert_disjoint image_insert)
qed
then show "(?I'', I) ∈ valid_I × valid_I" using I by auto
qed
qed
qed
} note step = this
{
from exists_lin_indpt_subset[OF a, unfolded full_span]
obtain A where lin: "lin_indpt A" and span: "span A = carrier_vec n" and Am: "A ⊆ a ` {0 ..<m}" by auto
from Am a have A: "A ⊆ carrier_vec n" by auto
from lin span A have card: "card A = n"
using basis_def dim_basis dim_is_n fin_dim_li_fin by auto
from A Am obtain I where A: "A = a ` I" and I: "I ⊆ {0 ..< m}" by (metis subset_imageE)
have "I ∈ valid_I" using I card lin unfolding valid_I_def A by auto
hence "∃ I. I ∈ valid_I" ..
}
note init = this
have step_valid: "(I',I) ∈ step_rel ⟹ I' ∈ valid_I" for I I' unfolding step_rel_def by auto
have "¬ (wf step_rel)"
proof
from init obtain I where I: "I ∈ valid_I" by auto
assume "wf step_rel"
from this[unfolded wf_eq_minimal, rule_format, OF I] step step_valid show False by blast
qed
with wf_iff_acyclic_if_finite[OF finite_step_rel]
have "¬ acyclic step_rel" by auto
thus "acyclic step_rel ⟹ False" by auto
qed
private lemma acyclic_step_rel: "acyclic step_rel"
proof (rule ccontr)
assume "¬ ?thesis"
hence "¬ acyclic (step_rel¯)" by auto
then obtain I where "(I, I) ∈ (step_rel^-1)^+" unfolding acyclic_def by blast
from this[unfolded trancl_power]
obtain len where "(I, I) ∈ (step_rel^-1) ^^ len" and len0: "len > 0" by blast
from this[unfolded relpow_fun_conv] obtain Is where
stepsIs: "⋀ i. i < len ⟹ (Is (Suc i), Is i) ∈ step_rel"
and IsI: "Is 0 = I" "Is len = I" by auto
{
fix i
assume "i ≤ len" hence "i - 1 < len" using len0 by auto
from stepsIs[unfolded step_rel_def, OF this]
have "Is i ∈ valid_I" by (cases i, auto)
} note Is_valid = this
from stepsIs[unfolded step_rel_def]
have "∀ i. ∃ l c h k. i < len ⟶ cond (Is i) (Is (Suc i)) l c h k" by auto
from choice[OF this] obtain ls where "∀ i. ∃ c h k. i < len ⟶ cond (Is i) (Is (Suc i)) (ls i) c h k" by auto
from choice[OF this] obtain cs where "∀ i. ∃ h k. i < len ⟶ cond (Is i) (Is (Suc i)) (ls i) (cs i) h k" by auto
from choice[OF this] obtain hs where "∀ i. ∃ k. i < len ⟶ cond (Is i) (Is (Suc i)) (ls i) (cs i) (hs i) k" by auto
from choice[OF this] obtain ks where
cond: "⋀ i. i < len ⟹ cond (Is i) (Is (Suc i)) (ls i) (cs i) (hs i) (ks i)" by auto
let ?R = "{hs i | i. i < len}"
define r where "r = Max ?R"
from cond[OF len0] have "hs 0 ∈ I" using IsI unfolding cond_def by auto
hence R0: "hs 0 ∈ ?R" using len0 by auto
have finR: "finite ?R" by auto
from Max_in[OF finR] R0
have rR: "r ∈ ?R" unfolding r_def[symmetric] by auto
then obtain p where rp: "r = hs p" and p: "p < len" by auto
from Max_ge[OF finR, folded r_def]
have rLarge: "i < len ⟹ hs i ≤ r" for i by auto
have exq: "∃q. ks q = r ∧ q < len"
proof (rule ccontr)
assume neg: "¬?thesis"
show False
proof(cases "r ∈ I")
case True
have 1: "j∈{Suc p..len} ⟹ r ∉ Is j" for j
proof(induction j rule: less_induct)
case (less j)
from less(2) have j_bounds: "j = Suc p ∨ j > Suc p" by auto
from less(2) have j_len: "j ≤ len" by auto
have pj_cond: "j = Suc p ⟹ cond (Is p) (Is j) (ls p) (cs p) (hs p) (ks p)" using cond p by blast
have r_neq_ksp: "r ≠ ks p" using p neg by auto
have "j = Suc p ⟹ Is j = insert (ks p) (Is p - {r})"
using rp cond pj_cond cond_def[of "Is p" "Is j" _ _ r] by blast
hence c1: "j = Suc p ⟹ r ∉ Is j" using r_neq_ksp by simp
have IH: "⋀t. t < j ⟹ t ∈ {Suc p..len} ⟹ r ∉ Is t" by fact
have r_neq_kspj: "j > Suc p ∧ j ≤ len ⟹ r ≠ ks (j-1)" using j_len neg IH by auto
have jsucj_cond: "j > Suc p ∧ j ≤ len ⟹ Is j = insert (ks (j-1)) (Is (j-1) - {hs (j-1)})"
using cond_def[of "Is (j-1)" "Is j"] cond
by (metis (no_types, lifting) Suc_less_eq2 diff_Suc_1 le_simps(3))
hence "j > Suc p ∧ j ≤ len ⟹ r ∉ insert (ks (j-1)) (Is (j-1))"
using IH r_neq_kspj by auto
hence "j > Suc p ∧ j ≤ len ⟹ r ∉ Is j" using jsucj_cond by simp
then show ?case using j_bounds j_len c1 by blast
qed
then show ?thesis using neg IsI(2) True p by auto
next
case False
have 2: "j∈{0..p} ⟹ r ∉ Is j" for j
proof(induction j rule: less_induct)
case(less j)
from less(2) have j_bound: "j ≤ p" by auto
have r_nin_Is0: "r ∉ Is 0" using IsI(1) False by simp
have IH: "⋀t. t < j ∧ t ∈ {0..p} ⟹ r ∉ Is t" using less.IH by blast
have j_neq_ksjpred: "j > 0 ⟹ r ≠ ks (j -1)" using neg j_bound p by auto
have Is_jpredj: "j > 0 ⟹ Is j = insert (ks (j-1)) (Is (j-1) - {hs (j-1)})"
using cond_def[of "Is (j-1)" "Is j" _ _ "hs (j-1)" "ks (j-1)"] cond
by (metis (full_types) One_nat_def Suc_pred diff_le_self j_bound le_less_trans p)
have "j > 0 ⟹ r ∉ insert (ks (j-1)) (Is (j-1))"
using j_neq_ksjpred IH j_bound by fastforce
hence "j > 0 ⟹ r ∉ Is j" using Is_jpredj by blast
then show ?case using j_bound r_nin_Is0 by blast
qed
have 3: "r ∈ Is p" using rp cond cond_def p by blast
then show ?thesis using 2 3 by auto
qed
qed
then obtain q where q1: "ks q = r" and q_len: "q < len" by blast
{
fix t i1 i2
assume "i1 < len" "i2 < len" "t < m"
assume "t∈ Is i1" "t∉ Is i2"
have "∃j < len. t = hs j"
proof (rule ccontr)
assume "¬ ?thesis"
hence hst: "⋀ j. j < len ⟹ hs j ≠ t" by auto
have main: "t ∉ Is (i + k) ⟹ i + k ≤ len ⟹ t ∉ Is k" for i k
proof (induct i)
case (Suc i)
hence i: "i + k < len" by auto
from cond[OF this, unfolded cond_def]
have "Is (Suc i + k) = insert (ks (i + k)) (Is (i + k) - {hs (i + k)})" by auto
from Suc(2)[unfolded this] hst[OF i] have "t ∉ Is (i + k)" by auto
from Suc(1)[OF this] i show ?case by auto
qed auto
from main[of i2 0] ‹i2 < len› ‹t ∉ Is i2› have "t ∉ Is 0" by auto
with IsI have "t ∉ Is len" by auto
with main[of "len - i1" i1] ‹i1 < len› have "t ∉ Is i1" by auto
with ‹t ∈ Is i1› show False by blast
qed
} note innotin = this
{
fix i
assume i: "i ∈ {Suc r..<m}"
{
assume i_in_Isp: "i ∈ Is p"
have "i ∈ Is q"
proof (rule ccontr)
have i_range: "i < m" using i by simp
assume "¬ ?thesis"
then have ex: "∃j < len. i = hs j"
using innotin[OF p q_len i_range i_in_Isp] by simp
then obtain j where j_hs: "i = hs j" by blast
have "i>r" using i by simp
then show False using j_hs p rLarge ex by force
qed
}
hence "(i ∈ Is p) ⟹ (i ∈ Is q)" by blast
} note bla = this
have blin: "b = lincomb (ls p) (a ` (Is p))" using cond_def p cond by blast
have carrDp: "(a ` (Is p)) ⊆ carrier_vec n " using Is_valid valid_I_def a p
by (smt image_subset_iff less_imp_le_nat mem_Collect_eq subsetD)
have carrcq: "cs q ∈ carrier_vec n" using cond cond_def q_len by simp
have ineq1: "(cs q) ∙ b < 0" using cond_def q_len cond by blast
let ?Isp_lt_r = "{x ∈ Is p . x < r}"
let ?Isp_gt_r = "{x ∈ Is p . x > r}"
have Is_disj: "?Isp_lt_r ∩ ?Isp_gt_r = {}" using Is_valid by auto
have "?Isp_lt_r ⊆ Is p" by simp
hence Isp_lt_0m: "?Isp_lt_r ⊆ {0..<m}" using valid_I_def Is_valid p less_imp_le_nat by blast
have "?Isp_gt_r ⊆ Is p" by simp
hence Isp_gt_0m: "?Isp_gt_r ⊆ {0..<m}" using valid_I_def Is_valid p less_imp_le_nat by blast
let ?Dp_lt = "a ` ?Isp_lt_r"
let ?Dp_ge = "a ` ?Isp_gt_r"
{
fix A B
assume Asub: "A ⊆ {0..<m} ∪ {0..<Suc r}"
assume Bsub: "B ⊆ {0..<m} ∪ {0..<Suc r}"
assume ABinters: "A ∩ B = {}"
have "r ∈ Is p" using rp p cond unfolding cond_def by simp
hence r_lt_m: "r < m" using p Is_valid[of p] unfolding valid_I_def by auto
hence 1: "A ⊆ {0..<m}" using Asub by auto
have 2: "B ⊆ {0..<m}" using r_lt_m Bsub by auto
have "a ` A ∩ a ` B = {}"
using inj_on_image_Int[OF inj_a 1 2] ABinters by auto
} note inja = this
have "(Is p ∩ {0..<r}) ∩ (Is p ∩ {r}) = {}" by auto
hence "a ` (Is p ∩ {0..<r} ∪ Is p ∩ {r}) = a ` (Is p ∩ {0..<r}) ∪ a ` (Is p ∩ {r})"
using inj_a by auto
moreover have "Is p ∩ {0..<r} ∪ Is p ∩ {r} ⊆ {0..<m} ∪ {0..<Suc r}" by auto
moreover have "Is p ∩ {Suc r..<m} ⊆ {0..<m} ∪ {0..<Suc r}" by auto
moreover have "(Is p ∩ {0..<r} ∪ Is p ∩ {r}) ∩ (Is p ∩ {Suc r..<m}) = {}" by auto
ultimately have one: "(a ` (Is p ∩ {0..<r}) ∪ a ` (Is p ∩ {r})) ∩ a ` (Is p ∩ {Suc r..<m}) = {}"
using inja[of "Is p ∩ {0..<r} ∪ Is p ∩ {r}" "Is p ∩ {Suc r..<m}"] by auto
have split: "Is p = Is p ∩ {0..<r} ∪ Is p ∩ {r} ∪ Is p ∩ {Suc r ..< m}"
using rp p Is_valid[of p] unfolding valid_I_def by auto
have gtr: "(∑w ∈ (a ` (Is p ∩ {Suc r ..< m})). ((ls p) w) * (cs q ∙ w)) = 0"
proof (rule sum.neutral, clarify)
fix w
assume w1: "w ∈ Is p" and w2: "w∈{Suc r..<m}"
have w_in_q: "w ∈ Is q" using bla[OF w2] w1 by blast
moreover have "hs q ≤ r" using rR rLarge using q_len by blast
ultimately have "w ≠ hs q" using w2 by simp
hence "w ∈ Is q -{hs q}" using w1 w_in_q by auto
moreover have "Is q - {hs q} ⊆ {0..<m}"
using q_len Is_valid[of q] unfolding valid_I_def by auto
ultimately have "a w ∈ span ( a ` (Is q - {hs q}))" using a by (intro span_mem, auto)
moreover have "cs q ∈ carrier_vec n ∧ span (a ` (Is q - {hs q})) =
{ x. x ∈ carrier_vec n ∧ cs q ∙ x = 0}"
using cond[of q] q_len unfolding cond_def by auto
ultimately have "(cs q) ∙ (a w) = 0" using a w2 by simp
then show "ls p (a w) * (cs q ∙ a w) = 0" by simp
qed
note pp = cond[OF p, unfolded cond_def rp[symmetric]]
note qq = cond[OF q_len, unfolded cond_def q1]
have "(cs q) ∙ b = (cs q) ∙ lincomb (ls p) (a ` (Is p))" using blin by auto
also have "… = (∑w ∈ (a ` (Is p)). ((ls p) w) * (cs q ∙ w))"
by (subst lincomb_scalar_prod_right[OF carrDp carrcq], simp)
also have "… = (∑w ∈ (a ` (Is p ∩ {0..<r}) ∪ a ` (Is p ∩ {r}) ∪ a ` (Is p ∩ {Suc r..<m})).
((ls p) w) * (cs q ∙ w))"
by (subst (1) split, rule sum.cong, auto)
also have "… = (∑w ∈ (a ` (Is p ∩ {0..<r})). ((ls p) w) * (cs q ∙ w))
+ (∑w ∈ (a ` (Is p ∩ {r})). ((ls p) w) * (cs q ∙ w))
+ (∑w ∈ (a ` (Is p ∩ {Suc r ..< m})). ((ls p) w) * (cs q ∙ w))"
apply (subst sum.union_disjoint[OF _ _ one])
apply (force+)[2]
apply (subst sum.union_disjoint)
apply (force+)[2]
apply (rule inja)
by auto
also have "… = (∑w ∈ (a ` (Is p ∩ {0..<r})). ((ls p) w) * (cs q ∙ w))
+ (∑w ∈ (a ` (Is p ∩ {r})). ((ls p) w) * (cs q ∙ w))"
using sum.neutral gtr by simp
also have "… > 0 + 0"
proof (intro add_le_less_mono sum_nonneg mult_nonneg_nonneg)
{
fix x
assume x: "x ∈ a ` (Is p ∩ {0..<r})"
show "0 ≤ ls p x" using pp x by auto
show "0 ≤ cs q ∙ x" using qq x by auto
}
have "r ∈ Is p" using pp by blast
hence "a ` (Is p ∩ {r}) = {a r}" by auto
hence id: "(∑w∈a ` (Is p ∩ {r}). ls p w * (cs q ∙ w)) = ls p (a r) * (cs q ∙ a r)"
by simp
show "0 < (∑w∈a ` (Is p ∩ {r}). ls p w * (cs q ∙ w))"
unfolding id
proof (rule mult_neg_neg)
show "ls p (a r) < 0" using pp by auto
show "cs q ∙ a r < 0" using qq by auto
qed
qed
finally have "cs q ∙ b > 0" by simp
moreover have "cs q ∙ b < 0" using qq by blast
ultimately show False by auto
qed
lemma fundamental_theorem_neg_C_or_B_in_context:
assumes W: "W = a ` {0 ..< m}"
shows "(∃ U. U ⊆ W ∧ card U = n ∧ lin_indpt U ∧ b ∈ finite_cone U) ∨
(∃c U. U ⊆ W ∧
c ∈ {normal_vector U, - normal_vector U} ∧
Suc (card U) = n ∧ lin_indpt U ∧ (∀w ∈ W. 0 ≤ c ∙ w) ∧ c ∙ b < 0)"
using acyclic_imp_goal[unfolded goal_def, OF acyclic_step_rel]
proof
assume "∃I. I⊆{0..<m} ∧ card (a ` I) = n ∧ lin_indpt (a ` I) ∧ b ∈ finite_cone (a ` I)"
thus ?thesis unfolding W by (intro disjI1, blast)
next
assume "∃c I. I ⊆ {0..<m} ∧
c ∈ {normal_vector (a ` I), - normal_vector (a ` I)} ∧
Suc (card (a ` I)) = n ∧ lin_indpt (a ` I) ∧ (∀i<m. 0 ≤ c ∙ a i) ∧ c ∙ b < 0"
then obtain c I where "I ⊆ {0..<m} ∧
c ∈ {normal_vector (a ` I), - normal_vector (a ` I)} ∧
Suc (card (a ` I)) = n ∧ lin_indpt (a ` I) ∧ (∀i<m. 0 ≤ c ∙ a i) ∧ c ∙ b < 0" by auto
thus ?thesis unfolding W
by (intro disjI2 exI[of _ c] exI[of _ "a ` I"], auto)
qed
end
lemma fundamental_theorem_of_linear_inequalities_C_imp_B_full_dim:
assumes A: "A ⊆ carrier_vec n"
and fin: "finite A"
and span: "span A = carrier_vec n"
and b: "b ∈ carrier_vec n"
and C: "∄ c B. B ⊆ A ∧ c ∈ {normal_vector B, - normal_vector B} ∧ Suc (card B) = n
∧ lin_indpt B ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0"
shows "∃ B ⊆ A. lin_indpt B ∧ card B = n ∧ b ∈ finite_cone B"
proof -
from finite_distinct_list[OF fin] obtain as where Aas: "A = set as" and dist: "distinct as" by auto
define m where "m = length as"
define a where "a = (λ i. as ! i)"
have inj: "inj_on a {0..< (m :: nat)}"
and id: "A = a ` {0..<m}"
unfolding m_def a_def Aas using inj_on_nth[OF dist] unfolding set_conv_nth
by auto
from fundamental_theorem_neg_C_or_B_in_context[OF _ inj b, folded id, OF A span refl] C
show ?thesis by blast
qed
lemma fundamental_theorem_of_linear_inequalities_full_dim: fixes A :: "'a vec set"
defines "HyperN ≡ {b. b ∈ carrier_vec n ∧ (∄ B c. B ⊆ A ∧ c ∈ {normal_vector B, - normal_vector B}
∧ Suc (card B) = n ∧ lin_indpt B ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0)}"
defines "HyperA ≡ {b. b ∈ carrier_vec n ∧ (∄ c. c ∈ carrier_vec n ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0)}"
defines "lin_indpt_cone ≡ ⋃ { finite_cone B | B. B ⊆ A ∧ card B = n ∧ lin_indpt B}"
assumes A: "A ⊆ carrier_vec n"
and fin: "finite A"
and span: "span A = carrier_vec n"
shows
"cone A = lin_indpt_cone"
"cone A = HyperN"
"cone A = HyperA"
proof -
have "lin_indpt_cone ⊆ cone A" unfolding lin_indpt_cone_def cone_def using fin finite_cone_mono A
by auto
moreover have "cone A ⊆ HyperA"
proof
fix c
assume cA: "c ∈ cone A"
from fundamental_theorem_of_linear_inequalities_A_imp_D[OF A fin this] cone_carrier[OF A] cA
show "c ∈ HyperA" unfolding HyperA_def by auto
qed
moreover have "HyperA ⊆ HyperN"
proof
fix c
assume "c ∈ HyperA"
hence False: "⋀ v. v ∈ carrier_vec n ⟹ (∀a⇩i∈A. 0 ≤ v ∙ a⇩i) ⟹ v ∙ c < 0 ⟹ False"
and c: "c ∈ carrier_vec n" unfolding HyperA_def by auto
show "c ∈ HyperN"
unfolding HyperN_def
proof (standard, intro conjI c notI, clarify, goal_cases)
case (1 W nv)
with A fin have fin: "finite W" and W: "W ⊆ carrier_vec n" by (auto intro: finite_subset)
show ?case using False[of nv] 1 normal_vector[OF fin _ _ W] by auto
qed
qed
moreover have "HyperN ⊆ lin_indpt_cone"
proof
fix b
assume "b ∈ HyperN"
from this[unfolded HyperN_def]
fundamental_theorem_of_linear_inequalities_C_imp_B_full_dim[OF A fin span, of b]
show "b ∈ lin_indpt_cone" unfolding lin_indpt_cone_def by auto
qed
ultimately show
"cone A = lin_indpt_cone"
"cone A = HyperN"
"cone A = HyperA"
by auto
qed
lemma fundamental_theorem_of_linear_inequalities_C_imp_B:
assumes A: "A ⊆ carrier_vec n"
and fin: "finite A"
and b: "b ∈ carrier_vec n"
and C: "∄ c A'. c ∈ carrier_vec n
∧ A' ⊆ A ∧ Suc (card A') = dim_span (insert b A)
∧ (∀ a ∈ A'. c ∙ a = 0)
∧ lin_indpt A' ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0"
shows "∃ B ⊆ A. lin_indpt B ∧ card B = dim_span A ∧ b ∈ finite_cone B"
proof -
from exists_lin_indpt_sublist[OF A] obtain A' where
lin: "lin_indpt_list A'" and span: "span (set A') = span A" and A'A: "set A' ⊆ A" by auto
hence linA': "lin_indpt (set A')" unfolding lin_indpt_list_def by auto
from A'A A have A': "set A' ⊆ carrier_vec n" by auto
have dim_spanA: "dim_span A = card (set A')"
by (rule sym, rule same_span_imp_card_eq_dim_span[OF A' A span linA'])
show ?thesis
proof (cases "b ∈ span A")
case False
with span have "b ∉ span (set A')" by auto
with lin have linAb: "lin_indpt_list (A' @ [b])" unfolding lin_indpt_list_def
using lin_dep_iff_in_span[OF A' _ b] span_mem[OF A', of b] b by auto
interpret gso: gram_schmidt_fs_lin_indpt n "A' @ [b]"
by (standard, insert linAb[unfolded lin_indpt_list_def], auto)
let ?m = "length A'"
define c where "c = - gso.gso ?m"
have c: "c ∈ carrier_vec n" using gso.gso_carrier[of ?m] unfolding c_def by auto
from gso.gso_times_self_is_norm[of ?m]
have "b ∙ gso.gso ?m = sq_norm (gso.gso ?m)" unfolding c_def using b c by auto
also have "… > 0" using gso.sq_norm_pos[of ?m] by auto
finally have cb: "c ∙ b < 0" using b c comm_scalar_prod[OF b c] unfolding c_def by auto
{
fix a
assume "a ∈ A"
hence "a ∈ span (set A')" unfolding span using span_mem[OF A] by auto
from finite_in_span[OF _ A' this]
obtain l where "a = lincomb l (set A')" by auto
hence "c ∙ a = c ∙ lincomb l (set A')" by simp
also have "… = 0"
by (subst lincomb_scalar_prod_right[OF A' c], rule sum.neutral, insert A', unfold set_conv_nth,
insert gso.gso_scalar_zero[of ?m] c, auto simp: c_def nth_append )
finally have "c ∙ a = 0" .
} note cA = this
have "∃ c A'. c ∈ carrier_vec n ∧ A' ⊆ A ∧ Suc (card A') = dim_span (insert b A)
∧ (∀ a ∈ A'. c ∙ a = 0) ∧ lin_indpt A' ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0"
proof (intro exI[of _ c] exI[of _ "set A'"] conjI A'A linA' cb c)
show "∀a∈set A'. c ∙ a = 0" "∀a⇩i∈A. 0 ≤ c ∙ a⇩i" using cA A'A by auto
have "dim_span (insert b A) = Suc (dim_span A)"
by (rule dim_span_insert[OF A b False])
also have "… = Suc (card (set A'))" unfolding dim_spanA ..
finally show "Suc (card (set A')) = dim_span (insert b A)" ..
qed
with C have False by blast
thus ?thesis ..
next
case bspan: True
define N where "N = normal_vectors A'"
from normal_vectors[OF lin, folded N_def]
have N: "set N ⊆ carrier_vec n" and
orthA'N: "⋀ w nv. w ∈ set A' ⟹ nv ∈ set N ⟹ nv ∙ w = 0" and
linAN: "lin_indpt_list (A' @ N)" and
lenAN: "length (A' @ N) = n" and
disj: "set A' ∩ set N = {}" by auto
from linAN lenAN have full_span': "span (set (A' @ N)) = carrier_vec n"
using lin_indpt_list_length_eq_n by blast
hence full_span'': "span (set A' ∪ set N) = carrier_vec n" by auto
from A N A' have AN: "A ∪ set N ⊆ carrier_vec n" and A'N: "set (A' @ N) ⊆ carrier_vec n" by auto
hence "span (A ∪ set N) ⊆ carrier_vec n" by (simp add: span_is_subset2)
with A'A span_is_monotone[of "set (A' @ N)" "A ∪ set N", unfolded full_span']
have full_span: "span (A ∪ set N) = carrier_vec n" unfolding set_append by fast
from fin have finAN: "finite (A ∪ set N)" by auto
note fundamental = fundamental_theorem_of_linear_inequalities_full_dim[OF AN finAN full_span]
show ?thesis
proof (cases "b ∈ cone (A ∪ set N)")
case True
from this[unfolded fundamental(1)] obtain C where CAN: "C ⊆ A ∪ set N" and cardC: "card C = n"
and linC: "lin_indpt C"
and bC: "b ∈ finite_cone C" by auto
have finC: "finite C" using finite_subset[OF CAN] fin by auto
from CAN A N have C: "C ⊆ carrier_vec n" by auto
from bC[unfolded finite_cone_def nonneg_lincomb_def] finC obtain c
where bC: "b = lincomb c C" and nonneg: "⋀ b. b ∈ C ⟹ c b ≥ 0" by auto
let ?C = "C - set N"
show ?thesis
proof (intro exI[of _ ?C] conjI)
from subset_li_is_li[OF linC] show "lin_indpt ?C" by auto
show CA: "?C ⊆ A" using CAN by auto
have bc: "b = lincomb c (?C ∪ (C ∩ set N))" unfolding bC
by (rule arg_cong[of _ _ "lincomb _"], auto)
have "b = lincomb c (?C - C ∩ set N)"
proof (rule orthogonal_cone(2)[OF A N fin full_span'' orthA'N refl span
A'A linAN lenAN _ CA _ bc])
show "∀w∈set N. w ∙ b = 0"
using ortho_span'[OF A' N _ bspan[folded span]] orthA'N by auto
qed auto
also have "?C - C ∩ set N = ?C" by auto
finally have "b = lincomb c ?C" .
with nonneg have "nonneg_lincomb c ?C b" unfolding nonneg_lincomb_def by auto
thus "b ∈ finite_cone ?C" unfolding finite_cone_def using finite_subset[OF CA fin] by auto
have Cid: "C ∩ set N ∪ ?C = C" by auto
have "length A' + length N = n" by fact
also have "… = card (C ∩ set N ∪ ?C) " using Cid cardC by auto
also have "… = card (C ∩ set N) + card ?C"
by (subst card_Un_disjoint, insert finC, auto)
also have "… ≤ length N + card ?C"
by (rule add_right_mono, rule order.trans, rule card_mono[OF finite_set[of N]],
auto intro: card_length)
also have "length A' = card (set A')" using lin[unfolded lin_indpt_list_def]
distinct_card[of A'] by auto
finally have le: "dim_span A ≤ card ?C" using dim_spanA by auto
have CA: "?C ⊆ span A" using CA C in_own_span[OF A] by auto
have linC: "lin_indpt ?C" using subset_li_is_li[OF linC] by auto
show "card ?C = dim_span A"
using card_le_dim_span[OF _ CA linC] le C by force
qed
next
case False
from False[unfolded fundamental(2)] b
obtain C c where
CAN: "C ⊆ A ∪ set N" and
cardC: "Suc (card C) = n" and
linC: "lin_indpt C" and
contains: "(∀a⇩i∈A ∪ set N. 0 ≤ c ∙ a⇩i)" and
cb: "c ∙ b < 0" and
nv: "c ∈ {normal_vector C, - normal_vector C}"
by auto
from CAN A N have C: "C ⊆ carrier_vec n" by auto
from cardC have cardCn: "card C < n" by auto
from finite_subset[OF CAN] fin have finC: "finite C" by auto
let ?C = "C - set N"
note nv' = normal_vector(1-4)[OF finC cardC linC C]
from nv' nv have c: "c ∈ carrier_vec n" by auto
have "∃ c A'. c ∈ carrier_vec n ∧ A' ⊆ A ∧ Suc (card A') = dim_span (insert b A)
∧ (∀ a ∈ A'. c ∙ a = 0) ∧ lin_indpt A' ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0"
proof (intro exI[of _ c] exI[of _ ?C] conjI cb c)
show CA: "?C ⊆ A" using CAN by auto
show "∀a⇩i∈A. 0 ≤ c ∙ a⇩i" using contains by auto
show lin': "lin_indpt ?C" using subset_li_is_li[OF linC] by auto
show sC0: "∀a∈ ?C. c ∙ a = 0" using nv' nv C by auto
have Cid: "C ∩ set N ∪ ?C = C" by auto
have "dim_span (set A') = card (set A')"
by (rule sym, rule same_span_imp_card_eq_dim_span[OF A' A' refl linA'])
also have "… = length A'"
using lin[unfolded lin_indpt_list_def] distinct_card[of A'] by auto
finally have dimA': "dim_span (set A') = length A'" .
from bspan have "span (insert b A) = span A" using b A using already_in_span by auto
from dim_span_cong[OF this[folded span]] dimA'
have dimbA: "dim_span (insert b A) = length A'" by simp
also have "… = Suc (card ?C)"
proof (rule ccontr)
assume neq: "length A' ≠ Suc (card ?C)"
have "length A' + length N = n" by fact
also have "… = Suc (card (C ∩ set N ∪ ?C))" using Cid cardC by auto
also have "… = Suc (card (C ∩ set N) + card ?C)"
by (subst card_Un_disjoint, insert finC, auto)
finally have id: "length A' + length N = Suc (card (C ∩ set N) + card ?C)" .
have le1: "card (C ∩ set N) ≤ length N"
by (metis Int_lower2 List.finite_set card_length card_mono inf.absorb_iff2 le_inf_iff)
from CA C A have CsA: "?C ⊆ span (set A')" unfolding span by (meson in_own_span order.trans)
from card_le_dim_span[OF _ this lin'] C
have le2: "card ?C ≤ length A'" unfolding dimA' by auto
from id le1 le2 neq
have id2: "card ?C = length A'" by linarith+
from card_eq_dim_span_imp_same_span[OF A' CsA lin' id2[folded dimA']]
have "span ?C = span A" unfolding span by auto
with bspan have "b ∈ span ?C" by auto
from orthocompl_span[OF _ _ c this] C sC0
have "c ∙ b = 0" by auto
with cb show False by simp
qed
finally show "Suc (card ?C) = dim_span (insert b A)" by simp
qed
with assms(4) have False by blast
thus ?thesis ..
qed
qed
qed
lemma fundamental_theorem_of_linear_inequalities: fixes A :: "'a vec set"
defines "HyperN ≡ {b. b ∈ carrier_vec n ∧ (∄ c B. c ∈ carrier_vec n ∧ B ⊆ A
∧ Suc (card B) = dim_span (insert b A) ∧ lin_indpt B
∧ (∀ a ∈ B. c ∙ a = 0)
∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0)}"
defines "HyperA ≡ {b. b ∈ carrier_vec n ∧ (∄ c. c ∈ carrier_vec n ∧ (∀ a⇩i ∈ A. c ∙ a⇩i ≥ 0) ∧ c ∙ b < 0)}"
defines "lin_indpt_cone ≡ ⋃ { finite_cone B | B. B ⊆ A ∧ card B = dim_span A ∧ lin_indpt B}"
assumes A: "A ⊆ carrier_vec n"
and fin: "finite A"
shows
"cone A = lin_indpt_cone"
"cone A = HyperN"
"cone A = HyperA"
proof -
have "lin_indpt_cone ⊆ cone A"
unfolding lin_indpt_cone_def cone_def using fin finite_cone_mono A by auto
moreover have "cone A ⊆ HyperA"
using fundamental_theorem_of_linear_inequalities_A_imp_D[OF A fin] cone_carrier[OF A]
unfolding HyperA_def by blast
moreover have "HyperA ⊆ HyperN" unfolding HyperA_def HyperN_def by blast
moreover have "HyperN ⊆ lin_indpt_cone"
proof
fix b
assume "b ∈ HyperN"
from this[unfolded HyperN_def]
fundamental_theorem_of_linear_inequalities_C_imp_B[OF A fin, of b]
show "b ∈ lin_indpt_cone" unfolding lin_indpt_cone_def by blast
qed
ultimately show
"cone A = lin_indpt_cone"
"cone A = HyperN"
"cone A = HyperA"
by auto
qed
corollary Caratheodory_theorem: assumes A: "A ⊆ carrier_vec n"
shows "cone A = ⋃ {finite_cone B |B. B ⊆ A ∧ lin_indpt B}"
proof
show "⋃ {finite_cone B |B. B ⊆ A ∧ lin_indpt B} ⊆ cone A" unfolding cone_def
using fin[OF fin_dim _ subset_trans[OF _ A]] by auto
{
fix a
assume "a ∈ cone A"
from this[unfolded cone_def] obtain B where
finB: "finite B" and BA: "B ⊆ A" and a: "a ∈ finite_cone B" by auto
from BA A have B: "B ⊆ carrier_vec n" by auto
hence "a ∈ cone B" using finB a by (simp add: cone_iff_finite_cone)
with fundamental_theorem_of_linear_inequalities(1)[OF B finB]
obtain C where CB: "C ⊆ B" and a: "a ∈ finite_cone C" and "lin_indpt C" by auto
with BA have "a ∈ ⋃ {finite_cone B |B. B ⊆ A ∧ lin_indpt B}" by auto
}
thus "⋃ {finite_cone B |B. B ⊆ A ∧ lin_indpt B} ⊇ cone A" by blast
qed
end
end