section ‹Weak and Strong Duality of Linear Programming› theory LP_Duality imports Linear_Inequalities.Farkas_Lemma Minimum_Maximum begin lemma weak_duality_theorem: fixes A :: "'a :: linordered_comm_semiring_strict mat" assumes A: "A ∈ carrier_mat nr nc" and b: "b ∈ carrier_vec nr" and c: "c ∈ carrier_vec nc" and x: "x ∈ carrier_vec nc" and Axb: "A *⇩_{v}x ≤ b" and y0: "y ≥ 0⇩_{v}nr" and yA: "A⇧^{T}*⇩_{v}y = c" shows "c ∙ x ≤ b ∙ y" proof - from y0 have y: "y ∈ carrier_vec nr" unfolding less_eq_vec_def by auto have "c ∙ x = (A⇧^{T}*⇩_{v}y) ∙ x" unfolding yA by simp also have "… = y ∙ (A *⇩_{v}x)" using x y A by (metis transpose_vec_mult_scalar) also have "… ≤ y ∙ b" unfolding scalar_prod_def using A b Axb y0 by (auto intro!: sum_mono mult_left_mono simp: less_eq_vec_def) also have "… = b ∙ y" using y b by (metis comm_scalar_prod) finally show ?thesis . qed corollary unbounded_primal_solutions: fixes A :: "'a :: linordered_idom mat" assumes A: "A ∈ carrier_mat nr nc" and b: "b ∈ carrier_vec nr" and c: "c ∈ carrier_vec nc" and unbounded: "∀ v. ∃ x ∈ carrier_vec nc. A *⇩_{v}x ≤ b ∧ c ∙ x ≥ v" shows "¬ (∃ y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c)" proof assume "(∃ y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c)" then obtain y where y: "y ≥ 0⇩_{v}nr" and Ayc: "A⇧^{T}*⇩_{v}y = c" by auto from unbounded[rule_format, of "b ∙ y + 1"] obtain x where x: "x ∈ carrier_vec nc" and Axb: "A *⇩_{v}x ≤ b" and le: "b ∙ y + 1 ≤ c ∙ x" by auto from weak_duality_theorem[OF A b c x Axb y Ayc] have "c ∙ x ≤ b ∙ y" by auto with le show False by auto qed corollary unbounded_dual_solutions: fixes A :: "'a :: linordered_idom mat" assumes A: "A ∈ carrier_mat nr nc" and b: "b ∈ carrier_vec nr" and c: "c ∈ carrier_vec nc" and unbounded: "∀ v. ∃ y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c ∧ b ∙ y ≤ v" shows "¬ (∃ x ∈ carrier_vec nc. A *⇩_{v}x ≤ b)" proof assume "∃ x ∈ carrier_vec nc. A *⇩_{v}x ≤ b" then obtain x where x: "x ∈ carrier_vec nc" and Axb: "A *⇩_{v}x ≤ b" by auto from unbounded[rule_format, of "c ∙ x - 1"] obtain y where y: "y≥0⇩_{v}nr" and Ayc: "A⇧^{T}*⇩_{v}y = c" and le: "b ∙ y ≤ c ∙ x - 1" by auto from weak_duality_theorem[OF A b c x Axb y Ayc] have "c ∙ x ≤ b ∙ y" by auto with le show False by auto qed text ‹A version of the strong duality theorem which demands that both primal and dual problem are solvable. At this point we do not use min- or max-operations› theorem strong_duality_theorem_both_sat: fixes A :: "'a :: trivial_conjugatable_linordered_field mat" assumes A: "A ∈ carrier_mat nr nc" and b: "b ∈ carrier_vec nr" and c: "c ∈ carrier_vec nc" and primal: "∃ x ∈ carrier_vec nc. A *⇩_{v}x ≤ b" and dual: "∃ y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c" shows "∃ x y. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b ∧ y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c ∧ c ∙ x = b ∙ y" proof - define M_up where "M_up = four_block_mat A (0⇩_{m}nr nr) (mat_of_row (- c)) (mat_of_row b)" define M_low where "M_low = four_block_mat (0⇩_{m}nc nc) (A⇧^{T}) (0⇩_{m}nc nc) (- (A⇧^{T}))" define M_last where "M_last = append_cols (0⇩_{m}nr nc) (- 1⇩_{m}nr :: 'a mat)" define M where "M = (M_up @⇩_{r}M_low) @⇩_{r}M_last" define bc where "bc = ((b @⇩_{v}0⇩_{v}1) @⇩_{v}(c @⇩_{v}-c)) @⇩_{v}(0⇩_{v}nr)" (* M = ( A 0) bc = ( b) (-c b) ( 0) ( 0 At) ( c) ( 0 -At) ( -c) ( 0 -I) ( 0) *) let ?nr = "((nr + 1) + (nc + nc)) + nr" let ?nc = "nc + nr" have M_up: "M_up ∈ carrier_mat (nr + 1) ?nc" unfolding M_up_def using A b c by auto have M_low: "M_low ∈ carrier_mat (nc + nc) ?nc" unfolding M_low_def using A by auto have M_last: "M_last ∈ carrier_mat nr ?nc" unfolding M_last_def by auto have M: "M ∈ carrier_mat ?nr ?nc" using carrier_append_rows[OF carrier_append_rows[OF M_up M_low] M_last] unfolding M_def by auto have bc: "bc ∈ carrier_vec ?nr" unfolding bc_def by (intro append_carrier_vec, insert b c, auto) have "(∃xy. xy ∈ carrier_vec ?nc ∧ M *⇩_{v}xy ≤ bc)" proof (subst gram_schmidt.Farkas_Lemma'[OF M bc], intro allI impI, elim conjE) fix ulv assume ulv0: "0⇩_{v}?nr ≤ ulv" and Mulv: "M⇧^{T}*⇩_{v}ulv = 0⇩_{v}?nc" from ulv0[unfolded less_eq_vec_def] have ulv: "ulv ∈ carrier_vec ?nr" by auto define u1 where "u1 = vec_first ulv ((nr + 1) + (nc + nc))" define u2 where "u2 = vec_first u1 (nr + 1)" define u3 where "u3 = vec_last u1 (nc + nc)" define t where "t = vec_last ulv nr" have ulvid: "ulv = u1 @⇩_{v}t" using ulv unfolding u1_def t_def by auto have t: "t ∈ carrier_vec nr" unfolding t_def by auto have u1: "u1 ∈ carrier_vec ((nr + 1) + (nc + nc))" unfolding u1_def by auto have u1id: "u1 = u2 @⇩_{v}u3" using u1 unfolding u2_def u3_def by auto have u2: "u2 ∈ carrier_vec (nr + 1)" unfolding u2_def by auto have u3: "u3 ∈ carrier_vec (nc + nc)" unfolding u3_def by auto define v where "v = vec_first u3 nc" define w where "w = vec_last u3 nc" have u3id: "u3 = v @⇩_{v}w" using u3 unfolding v_def w_def by auto have v: "v ∈ carrier_vec nc" unfolding v_def by auto have w: "w ∈ carrier_vec nc" unfolding w_def by auto define u where "u = vec_first u2 nr" define L where "L = vec_last u2 1" have u2id: "u2 = u @⇩_{v}L" using u2 unfolding u_def L_def by auto have u: "u ∈ carrier_vec nr" unfolding u_def by auto have L: "L ∈ carrier_vec 1" unfolding L_def by auto define vec1 where "vec1 = A⇧^{T}*⇩_{v}u + mat_of_col (- c) *⇩_{v}L" have vec1: "vec1 ∈ carrier_vec nc" unfolding vec1_def mat_of_col_def using A u c L by (meson add_carrier_vec mat_of_row_carrier(1) mult_mat_vec_carrier transpose_carrier_mat uminus_carrier_vec) define vec2 where "vec2 = A *⇩_{v}(v - w)" have vec2: "vec2 ∈ carrier_vec nr" unfolding vec2_def using A v w by auto define vec3 where "vec3 = mat_of_col b *⇩_{v}L" have vec3: "vec3 ∈ carrier_vec nr" using A b L unfolding mat_of_col_def vec3_def by (meson add_carrier_vec mat_of_row_carrier(1) mult_mat_vec_carrier transpose_carrier_mat uminus_carrier_vec) have Mt: "M⇧^{T}= (M_up⇧^{T}@⇩_{c}M_low⇧^{T}) @⇩_{c}M_last⇧^{T}" unfolding M_def append_cols_def by simp have "M⇧^{T}*⇩_{v}ulv = (M_up⇧^{T}@⇩_{c}M_low⇧^{T}) *⇩_{v}u1 + M_last⇧^{T}*⇩_{v}t" unfolding Mt ulvid by (subst mat_mult_append_cols[OF carrier_append_cols _ u1 t], insert M_up M_low M_last, auto) also have "M_last⇧^{T}= 0⇩_{m}nc nr @⇩_{r}- 1⇩_{m}nr" unfolding M_last_def unfolding append_cols_def by (simp, subst transpose_uminus, auto) also have "… *⇩_{v}t = 0⇩_{v}nc @⇩_{v}- t" by (subst mat_mult_append[OF _ _ t], insert t, auto) also have "(M_up⇧^{T}@⇩_{c}M_low⇧^{T}) *⇩_{v}u1 = (M_up⇧^{T}*⇩_{v}u2) + (M_low⇧^{T}*⇩_{v}u3)" unfolding u1id by (rule mat_mult_append_cols[OF _ _ u2 u3], insert M_up M_low, auto) also have "M_low⇧^{T}= four_block_mat (0⇩_{m}nc nc) (0⇩_{m}nc nc) A (- A)" unfolding M_low_def by (subst transpose_four_block_mat, insert A, auto) also have "… *⇩_{v}u3 = (0⇩_{m}nc nc *⇩_{v}v + 0⇩_{m}nc nc *⇩_{v}w) @⇩_{v}(A *⇩_{v}v + - A *⇩_{v}w)" unfolding u3id by (subst four_block_mat_mult_vec[OF _ _ A _ v w], insert A, auto) also have "0⇩_{m}nc nc *⇩_{v}v + 0⇩_{m}nc nc *⇩_{v}w = 0⇩_{v}nc" using v w by auto also have "A *⇩_{v}v + - A *⇩_{v}w = vec2" unfolding vec2_def using A v w by (metis (full_types) carrier_matD(2) carrier_vecD minus_add_uminus_vec mult_mat_vec_carrier mult_minus_distrib_mat_vec uminus_mult_mat_vec) also have "M_up⇧^{T}= four_block_mat A⇧^{T}(mat_of_col (- c)) (0⇩_{m}nr nr) (mat_of_col b)" unfolding M_up_def mat_of_col_def by (subst transpose_four_block_mat[OF A], insert b c, auto) also have "… *⇩_{v}u2 = vec1 @⇩_{v}vec3" unfolding u2id vec1_def vec3_def by (subst four_block_mat_mult_vec[OF _ _ _ _ u L], insert A b c u, auto) also have "(vec1 @⇩_{v}vec3) + (0⇩_{v}nc @⇩_{v}vec2) + (0⇩_{v}nc @⇩_{v}- t) = (vec1 @⇩_{v}(vec3 + vec2 - t))" apply (subst append_vec_add[of _ nc _ _ nr, OF vec1 _ vec3 vec2]) subgoal by force apply (subst append_vec_add[of _ nc _ _ nr]) subgoal using vec1 by auto subgoal by auto subgoal using vec2 vec3 by auto subgoal using t by auto subgoal using vec1 by auto done finally have "vec1 @⇩_{v}(vec3 + vec2 - t) = 0⇩_{v}?nc" unfolding Mulv by simp also have "… = 0⇩_{v}nc @⇩_{v}0⇩_{v}nr" by auto finally have "vec1 = 0⇩_{v}nc ∧ vec3 + vec2 - t = 0⇩_{v}nr" by (subst (asm) append_vec_eq[OF vec1], auto) hence 01: "vec1 = 0⇩_{v}nc" and 02: "vec3 + vec2 - t = 0⇩_{v}nr" by auto from 01 have "vec1 + mat_of_col c *⇩_{v}L = mat_of_col c *⇩_{v}L" using c L vec1 unfolding mat_of_col_def by auto also have "vec1 + mat_of_col c *⇩_{v}L = A⇧^{T}*⇩_{v}u" unfolding vec1_def using A u c L unfolding mat_of_col_def mat_of_row_uminus transpose_uminus by (subst uminus_mult_mat_vec, auto) finally have As: "A⇧^{T}*⇩_{v}u = mat_of_col c *⇩_{v}L" . from 02 have "(vec3 + vec2 - t) + t = 0⇩_{v}nr + t" by simp also have "(vec3 + vec2 - t) + t = vec2 + vec3" using vec3 vec2 t by auto finally have t23: "t = vec2 + vec3" using t by auto have id0: "0⇩_{v}?nr = ((0⇩_{v}nr @⇩_{v}0⇩_{v}1) @⇩_{v}(0⇩_{v}nc @⇩_{v}0⇩_{v}nc)) @⇩_{v}0⇩_{v}nr" by auto from ulv0[unfolded id0 ulvid u1id u2id u3id] have "0⇩_{v}nr ≤ u ∧ 0⇩_{v}1 ≤ L ∧ 0⇩_{v}nc ≤ v ∧ 0⇩_{v}nc ≤ w ∧ 0⇩_{v}nr ≤ t" apply (subst (asm) append_vec_le[of _ "(nr + 1) + (nc + nc)"]) subgoal by (intro append_carrier_vec, auto) subgoal by (intro append_carrier_vec u L v w) apply (subst (asm) append_vec_le[of _ "(nr + 1)"]) subgoal by (intro append_carrier_vec, auto) subgoal by (intro append_carrier_vec u L v w) apply (subst (asm) append_vec_le[OF _ u], force) apply (subst (asm) append_vec_le[OF _ v], force) by auto hence ineqs: "0⇩_{v}nr ≤ u" "0⇩_{v}1 ≤ L" "0⇩_{v}nc ≤ v" "0⇩_{v}nc ≤ w" "0⇩_{v}nr ≤ t" by auto have "ulv ∙ bc = u ∙ b + (v ∙ c + w ∙ (-c))" unfolding ulvid u1id u2id u3id bc_def apply (subst scalar_prod_append[OF _ t]) apply (rule append_carrier_vec[OF append_carrier_vec[OF u L] append_carrier_vec[OF v w]]) apply (rule append_carrier_vec[OF append_carrier_vec[OF b] append_carrier_vec]; use c in force) apply force apply (subst scalar_prod_append) apply (rule append_carrier_vec[OF u L]) apply (rule append_carrier_vec[OF v w]) subgoal by (rule append_carrier_vec, insert b, auto) subgoal by (rule append_carrier_vec, insert c, auto) apply (subst scalar_prod_append[OF u L b], force) apply (subst scalar_prod_append[OF v w c], use c in force) apply (insert L t, auto) done also have "v ∙ c + w ∙ (-c) = c ∙ v + (-c) ∙ w" by (subst (1 2) comm_scalar_prod, insert w c v, auto) also have "… = c ∙ v - (c ∙ w)" using c w by simp also have "… = c ∙ (v - w)" using c v w by (simp add: scalar_prod_minus_distrib) finally have ulvbc: "ulv ∙ bc = u ∙ b + c ∙ (v - w)" . define lam where "lam = L $ 0" from ineqs(2) L have lam0: "lam ≥ 0" unfolding less_eq_vec_def lam_def by auto have As: "A⇧^{T}*⇩_{v}u = lam ⋅⇩_{v}c" unfolding As using c L unfolding lam_def mat_of_col_def by (intro eq_vecI, auto simp: scalar_prod_def) have vec3: "vec3 = lam ⋅⇩_{v}b" unfolding vec3_def using b L unfolding lam_def mat_of_col_def by (intro eq_vecI, auto simp: scalar_prod_def) note preconds = lam0 ineqs(1,3-)[unfolded t23[unfolded vec2_def vec3]] As have "0 ≤ u ∙ b + c ∙ (v - w)" proof (cases "lam > 0") case True hence "u ∙ b = inverse lam * (lam * (b ∙ u))" using comm_scalar_prod[OF b u] by simp also have "… = inverse lam * ((lam ⋅⇩_{v}b) ∙ u)" using b u by simp also have "… ≥ inverse lam * (-(A *⇩_{v}(v - w)) ∙ u)" proof (intro mult_left_mono) show "0 ≤ inverse lam" using preconds by auto show "-(A *⇩_{v}(v - w)) ∙ u ≤ (lam ⋅⇩_{v}b) ∙ u" unfolding scalar_prod_def apply (rule sum_mono) subgoal for i using lesseq_vecD[OF _ preconds(2), of nr i] lesseq_vecD[OF _ preconds(5), of nr i] u v w b A by (intro mult_right_mono, auto) done qed also have "inverse lam * (-(A *⇩_{v}(v - w)) ∙ u) = - (inverse lam * ((A *⇩_{v}(v - w)) ∙ u))" by (subst scalar_prod_uminus_left, insert A u v w, auto) also have "(A *⇩_{v}(v - w)) ∙ u = (A⇧^{T}*⇩_{v}u) ∙ (v - w)" apply (subst transpose_vec_mult_scalar[OF A _ u]) subgoal using v w by force by (rule comm_scalar_prod[OF _ u], insert A v w, auto) also have "inverse lam * … = c ∙ (v - w)" unfolding preconds(6) using True by (subst scalar_prod_smult_left, insert c v w, auto) finally show ?thesis by simp next case False with preconds have lam: "lam = 0" by auto from primal obtain x0 where x0: "x0 ∈ carrier_vec nc" and Ax0b: "A *⇩_{v}x0 ≤ b" by auto from dual obtain y0 where y00: "y0 ≥ 0⇩_{v}nr" and Ay0c: "A⇧^{T}*⇩_{v}y0 = c" by auto from y00 have y0: "y0 ∈ carrier_vec nr" unfolding less_eq_vec_def by auto have Au: "A⇧^{T}*⇩_{v}u = 0⇩_{v}nc" unfolding preconds lam using c by auto have "0 = (A⇧^{T}*⇩_{v}u) ∙ x0" unfolding Au using x0 by auto also have "… = u ∙ (A *⇩_{v}x0)" by (rule transpose_vec_mult_scalar[OF A x0 u]) also have "… ≤ u ∙ b" unfolding scalar_prod_def apply (use A x0 b in simp) apply (intro sum_mono) subgoal for i using lesseq_vecD[OF _ preconds(2), of nr i] lesseq_vecD[OF _ Ax0b, of nr i] u v w b A x0 by (intro mult_left_mono, auto) done finally have ub: "0 ≤ u ∙ b" . have "c ∙ (v - w) = (A⇧^{T}*⇩_{v}y0) ∙ (v - w)" unfolding Ay0c by simp also have "… = y0 ∙ (A *⇩_{v}(v - w))" by (subst transpose_vec_mult_scalar[OF A _ y0], insert v w, auto) also have "… ≥ 0" unfolding scalar_prod_def apply (use A v w in simp) apply (intro sum_nonneg) subgoal for i using lesseq_vecD[OF _ y00, of nr i] lesseq_vecD[OF _ preconds(5)[unfolded lam], of nr i] A y0 v w b by (intro mult_nonneg_nonneg, auto) done finally show ?thesis using ub by auto qed thus "0 ≤ ulv ∙ bc" unfolding ulvbc . qed then obtain xy where xy: "xy ∈ carrier_vec ?nc" and le: "M *⇩_{v}xy ≤ bc" by auto define x where "x = vec_first xy nc" define y where "y = vec_last xy nr" have xyid: "xy = x @⇩_{v}y" using xy unfolding x_def y_def by auto have x: "x ∈ carrier_vec nc" unfolding x_def by auto have y: "y ∈ carrier_vec nr" unfolding y_def by auto have At: "A⇧^{T}∈ carrier_mat nc nr" using A by auto have Ax1: "A *⇩_{v}x @⇩_{v}vec 1 (λ_. b ∙ y - c ∙ x) ∈ carrier_vec (nr + 1)" using A x by fastforce have b0cc: "(b @⇩_{v}0⇩_{v}1) @⇩_{v}c @⇩_{v}- c ∈ carrier_vec ((nr + 1) + (nc + nc))" using b c by (intro append_carrier_vec, auto) have "M *⇩_{v}xy = (M_up *⇩_{v}xy @⇩_{v}M_low *⇩_{v}xy) @⇩_{v}(M_last *⇩_{v}xy)" unfolding M_def unfolding mat_mult_append[OF carrier_append_rows[OF M_up M_low] M_last xy] by (simp add: mat_mult_append[OF M_up M_low xy]) also have "M_low *⇩_{v}xy = (0⇩_{m}nc nc *⇩_{v}x + A⇧^{T}*⇩_{v}y) @⇩_{v}(0⇩_{m}nc nc *⇩_{v}x + - A⇧^{T}*⇩_{v}y)" unfolding M_low_def xyid by (rule four_block_mat_mult_vec[OF _ At _ _ x y], insert A, auto) also have "0⇩_{m}nc nc *⇩_{v}x + A⇧^{T}*⇩_{v}y = A⇧^{T}*⇩_{v}y" using A x y by auto also have "0⇩_{m}nc nc *⇩_{v}x + - A⇧^{T}*⇩_{v}y = - A⇧^{T}*⇩_{v}y" using A x y by auto also have "M_up *⇩_{v}xy = (A *⇩_{v}x + 0⇩_{m}nr nr *⇩_{v}y) @⇩_{v}(mat_of_row (- c) *⇩_{v}x + mat_of_row b *⇩_{v}y)" unfolding M_up_def xyid by (rule four_block_mat_mult_vec[OF A _ _ _ x y], insert b c, auto) also have "A *⇩_{v}x + 0⇩_{m}nr nr *⇩_{v}y = A *⇩_{v}x" using A x y by auto also have "mat_of_row (- c) *⇩_{v}x + mat_of_row b *⇩_{v}y = vec 1 (λ _. b ∙ y - c ∙ x)" unfolding mult_mat_vec_def using c x by (intro eq_vecI, auto) also have "M_last *⇩_{v}xy = - y" unfolding M_last_def xyid using x y by (subst mat_mult_append_cols[OF _ _ x y], auto) finally have "((A *⇩_{v}x @⇩_{v}vec 1 (λ_. b ∙ y - c ∙ x)) @⇩_{v}(A⇧^{T}*⇩_{v}y @⇩_{v}- A⇧^{T}*⇩_{v}y)) @⇩_{v}-y = M *⇩_{v}xy" .. also have "… ≤ bc" by fact also have "… = ((b @⇩_{v}0⇩_{v}1) @⇩_{v}(c @⇩_{v}-c)) @⇩_{v}0⇩_{v}nr" unfolding bc_def by auto finally have ineqs: "A *⇩_{v}x ≤ b ∧ vec 1 (λ_. b ∙ y - c ∙ x) ≤ 0⇩_{v}1 ∧ A⇧^{T}*⇩_{v}y ≤ c ∧ - A⇧^{T}*⇩_{v}y ≤ -c ∧ -y ≤ 0⇩_{v}nr" apply (subst (asm) append_vec_le[OF _ b0cc]) subgoal using A x y by (intro append_carrier_vec, auto) apply (subst (asm) append_vec_le[OF Ax1], use b in fastforce) apply (subst (asm) append_vec_le[OF _ b], use A x in force) apply (subst (asm) append_vec_le[OF _ c], use A y in force) by auto show ?thesis proof (intro exI conjI) from ineqs show Axb: "A *⇩_{v}x ≤ b" by auto from ineqs have "- A⇧^{T}*⇩_{v}y ≤ -c" "A⇧^{T}*⇩_{v}y ≤ c" by auto hence "A⇧^{T}*⇩_{v}y ≥ c" "A⇧^{T}*⇩_{v}y ≤ c" unfolding less_eq_vec_def using A y by auto then show Aty: "A⇧^{T}*⇩_{v}y = c" by simp from ineqs have "- y ≤ 0⇩_{v}nr" by simp then show y0: "0⇩_{v}nr ≤ y" unfolding less_eq_vec_def by auto from ineqs have "b ∙ y ≤ c ∙ x" unfolding less_eq_vec_def by auto with weak_duality_theorem[OF A b c x Axb y0 Aty] show "c ∙ x = b ∙ y" by auto qed (insert x) qed text ‹A version of the strong duality theorem which demands that the primal problem is solvable and the objective function is bounded.› theorem strong_duality_theorem_primal_sat_bounded: fixes bound :: "'a :: trivial_conjugatable_linordered_field" assumes A: "A ∈ carrier_mat nr nc" and b: "b ∈ carrier_vec nr" and c: "c ∈ carrier_vec nc" and sat: "∃ x ∈ carrier_vec nc. A *⇩_{v}x ≤ b" and bounded: "∀ x ∈ carrier_vec nc. A *⇩_{v}x ≤ b ⟶ c ∙ x ≤ bound" shows "∃ x y. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b ∧ y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c ∧ c ∙ x = b ∙ y" proof (rule strong_duality_theorem_both_sat[OF A b c sat]) show "∃y≥0⇩_{v}nr. A⇧^{T}*⇩_{v}y = c" proof (rule ccontr) assume "¬ ?thesis" hence "∃y. y ∈ carrier_vec nc ∧ 0⇩_{v}nr ≤ A *⇩_{v}y ∧ 0 > y ∙ c" by (subst (asm) gram_schmidt.Farkas_Lemma[OF _ c], insert A, auto) then obtain y where y: "y ∈ carrier_vec nc" and Ay0: "A *⇩_{v}y ≥ 0⇩_{v}nr" and yc0: "y ∙ c < 0" by auto from sat obtain x where x: "x ∈ carrier_vec nc" and Axb: "A *⇩_{v}x ≤ b" by auto define diff where "diff = bound + 1 - c ∙ x" from x Axb bounded have "c ∙ x < bound + 1" by auto hence diff: "diff > 0" unfolding diff_def by auto from yc0 have inv: "inverse (- (y ∙ c)) > 0" by auto define fact where "fact = diff * (inverse (- (y ∙ c)))" have fact: "fact > 0" unfolding fact_def using diff inv by (metis mult_pos_pos) define z where "z = x - fact ⋅⇩_{v}y" have "A *⇩_{v}z = A *⇩_{v}x - A *⇩_{v}(fact ⋅⇩_{v}y)" unfolding z_def using A x y by (meson mult_minus_distrib_mat_vec smult_carrier_vec) also have "… = A *⇩_{v}x - fact ⋅⇩_{v}(A *⇩_{v}y)" using A y by auto also have "… ≤ b" proof (intro lesseq_vecI[OF _ b]) show "A *⇩_{v}x - fact ⋅⇩_{v}(A *⇩_{v}y) ∈ carrier_vec nr" using A x y by auto fix i assume i: "i < nr" have "(A *⇩_{v}x - fact ⋅⇩_{v}(A *⇩_{v}y)) $ i = (A *⇩_{v}x) $ i - fact * (A *⇩_{v}y) $ i" using i A x y by auto also have "… ≤ b $ i - fact * (A *⇩_{v}y) $ i" using lesseq_vecD[OF b Axb i] by auto also have "… ≤ b $ i - 0 * 0" using lesseq_vecD[OF _ Ay0 i] fact A y i by (intro diff_left_mono mult_monom, auto) finally show "(A *⇩_{v}x - fact ⋅⇩_{v}(A *⇩_{v}y)) $ i ≤ b $ i" by simp qed finally have Azb: "A *⇩_{v}z ≤ b" . have z: "z ∈ carrier_vec nc" using x y unfolding z_def by auto have "c ∙ z = c ∙ x - fact * (c ∙ y)" unfolding z_def using c x y by (simp add: scalar_prod_minus_distrib) also have "… = c ∙ x + diff" unfolding comm_scalar_prod[OF c y] fact_def using yc0 by simp also have "… = bound + 1" unfolding diff_def by simp also have "… > c ∙ z" using bounded Azb z by auto finally show False by simp qed qed text ‹A version of the strong duality theorem which demands that the dual problem is solvable and the objective function is bounded.› theorem strong_duality_theorem_dual_sat_bounded: fixes bound :: "'a :: trivial_conjugatable_linordered_field" assumes A: "A ∈ carrier_mat nr nc" and b: "b ∈ carrier_vec nr" and c: "c ∈ carrier_vec nc" and sat: "∃ y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c" and bounded: "∀ y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c ⟶ bound ≤ b ∙ y" shows "∃ x y. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b ∧ y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c ∧ c ∙ x = b ∙ y" proof (rule strong_duality_theorem_both_sat[OF A b c _ sat]) show "∃x∈carrier_vec nc. A *⇩_{v}x ≤ b" proof (rule ccontr) assume "¬ ?thesis" hence "¬ (∃x. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b)" by auto then obtain y where y0: "y ≥ 0⇩_{v}nr" and Ay0: "A⇧^{T}*⇩_{v}y = 0⇩_{v}nc" and yb: "y ∙ b < 0" by (subst (asm) gram_schmidt.Farkas_Lemma'[OF A b], auto) from sat obtain x where x0: "x ≥ 0⇩_{v}nr" and Axc: "A⇧^{T}*⇩_{v}x = c" by auto define diff where "diff = b ∙ x - (bound - 1)" from x0 Axc bounded have "bound ≤ b ∙ x" by auto hence diff: "diff > 0" unfolding diff_def by auto define fact where "fact = - inverse (y ∙ b) * diff" have fact: "fact > 0" unfolding fact_def using diff yb by (auto intro: mult_neg_pos) define z where "z = x + fact ⋅⇩_{v}y" from x0 have x: "x ∈ carrier_vec nr" unfolding less_eq_vec_def by auto from y0 have y: "y ∈ carrier_vec nr" unfolding less_eq_vec_def by auto have "A⇧^{T}*⇩_{v}z = A⇧^{T}*⇩_{v}x + A⇧^{T}*⇩_{v}(fact ⋅⇩_{v}y)" unfolding z_def using A x y by (simp add: mult_add_distrib_mat_vec) also have "… = A⇧^{T}*⇩_{v}x + fact ⋅⇩_{v}(A⇧^{T}*⇩_{v}y)" using A y by auto also have "… = c" unfolding Ay0 Axc using c by auto finally have Azc: "A⇧^{T}*⇩_{v}z = c" . have z0: "z ≥ 0⇩_{v}nr" unfolding z_def by (intro lesseq_vecI[of _ nr], insert x y lesseq_vecD[OF _ x0, of nr] lesseq_vecD[OF _ y0, of nr] fact, auto intro!: add_nonneg_nonneg) from bounded Azc z0 have bz: "bound ≤ b ∙ z" by auto also have "… = b ∙ x + fact * (b ∙ y)" unfolding z_def using b x y by (simp add: scalar_prod_add_distrib) also have "… = diff + (bound - 1) + fact * (b ∙ y)" unfolding diff_def by auto also have "fact * (b ∙ y) = - diff" using yb unfolding fact_def comm_scalar_prod[OF y b] by auto finally show False by simp qed qed text ‹Now the previous three duality theorems are formulated via min/max.› corollary strong_duality_theorem_min_max: fixes A :: "'a :: trivial_conjugatable_linordered_field mat" assumes A: "A ∈ carrier_mat nr nc" and b: "b ∈ carrier_vec nr" and c: "c ∈ carrier_vec nc" and primal: "∃ x ∈ carrier_vec nc. A *⇩_{v}x ≤ b" and dual: "∃ y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c" shows "Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b} = Minimum {b ∙ y | y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c}" and "has_Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b}" and "has_Minimum {b ∙ y | y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c}" proof - let ?Prim = "{c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b}" let ?Dual = "{b ∙ y | y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c}" define Prim where "Prim = ?Prim" define Dual where "Dual = ?Dual" from strong_duality_theorem_both_sat[OF assms] obtain x y where x: "x ∈ carrier_vec nc" and Axb: "A *⇩_{v}x ≤ b" and y: "y ≥ 0⇩_{v}nr" and Ayc: "A⇧^{T}*⇩_{v}y = c" and eq: "c ∙ x = b ∙ y" by auto have cxP: "c ∙ x ∈ Prim" unfolding Prim_def using x Axb by auto have cxD: "c ∙ x ∈ Dual" unfolding eq Dual_def using y Ayc by auto { fix z assume "z ∈ Prim" from this[unfolded Prim_def] obtain x' where x': "x' ∈ carrier_vec nc" and Axb': "A *⇩_{v}x' ≤ b" and z: "z = c ∙ x'" by auto from weak_duality_theorem[OF A b c x' Axb' y Ayc, folded eq] have "z ≤ c ∙ x" unfolding z . } note cxMax = this have max: "Maximum Prim = c ∙ x" by (intro eqMaximumI cxP cxMax) show "has_Maximum ?Prim" unfolding Prim_def[symmetric] has_Maximum_def using cxP cxMax by auto { fix z assume "z ∈ Dual" from this[unfolded Dual_def] obtain y' where y': "y' ≥ 0⇩_{v}nr" and Ayc': "A⇧^{T}*⇩_{v}y' = c" and z: "z = b ∙ y'" by auto from weak_duality_theorem[OF A b c x Axb y' Ayc', folded z] have "c ∙ x ≤ z" . } note cxMin = this show "has_Minimum ?Dual" unfolding Dual_def[symmetric] has_Minimum_def using cxD cxMin by auto have min: "Minimum Dual = c ∙ x" by (intro eqMinimumI cxD cxMin) from min max show "Maximum ?Prim = Minimum ?Dual" unfolding Dual_def Prim_def by auto qed corollary strong_duality_theorem_primal_sat_bounded_min_max: fixes bound :: "'a :: trivial_conjugatable_linordered_field" assumes A: "A ∈ carrier_mat nr nc" and b: "b ∈ carrier_vec nr" and c: "c ∈ carrier_vec nc" and sat: "∃ x ∈ carrier_vec nc. A *⇩_{v}x ≤ b" and bounded: "∀ x ∈ carrier_vec nc. A *⇩_{v}x ≤ b ⟶ c ∙ x ≤ bound" shows "Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b} = Minimum {b ∙ y | y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c}" and "has_Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b}" and "has_Minimum {b ∙ y | y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c}" proof - let ?Prim = "{c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b}" let ?Dual = "{b ∙ y | y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c}" from strong_duality_theorem_primal_sat_bounded[OF assms] have "∃y≥0⇩_{v}nr. A⇧^{T}*⇩_{v}y = c" by blast from strong_duality_theorem_min_max[OF A b c sat this] show "Maximum ?Prim = Minimum ?Dual" "has_Maximum ?Prim" "has_Minimum ?Dual" by blast+ qed corollary strong_duality_theorem_dual_sat_bounded_min_max: fixes bound :: "'a :: trivial_conjugatable_linordered_field" assumes A: "A ∈ carrier_mat nr nc" and b: "b ∈ carrier_vec nr" and c: "c ∈ carrier_vec nc" and sat: "∃ y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c" and bounded: "∀ y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c ⟶ bound ≤ b ∙ y" shows "Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b} = Minimum {b ∙ y | y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c}" and "has_Maximum {c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b}" and "has_Minimum {b ∙ y | y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c}" proof - let ?Prim = "{c ∙ x | x. x ∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b}" let ?Dual = "{b ∙ y | y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = c}" from strong_duality_theorem_dual_sat_bounded[OF assms] have "∃ x ∈ carrier_vec nc. A *⇩_{v}x ≤ b" by blast from strong_duality_theorem_min_max[OF A b c this sat] show "Maximum ?Prim = Minimum ?Dual" "has_Maximum ?Prim" "has_Minimum ?Dual" by blast+ qed end