LeanPool.Duality.FarkasBasic #

finishit is a helper tactic used by equalityFarkas to discharge the residual matrix-vector equality after the main Farkas-Bartl bijection: it unfolds the matrix products, swaps the order of summation, and closes the goal with ring.

Equations

tacticFinishit = Lean.ParserDescr.node `tacticFinishit 1024 (Lean.ParserDescr.nonReservedSymbol "finishit" false)

Instances For

source

theorem equalityFarkas {I : Type u_1} {J : Type u_2} {F : Type u_3} [Fintype I] [Fintype J] [Field F] [LinearOrder F] [IsStrictOrderedRing F] (A : Matrix I J F) (b : I → F) :

(∃ (x : J → F), 0 ≤ x ∧ A.mulVec x = b) ≠ ∃ (y : I → F), 0 ≤ A.transpose.mulVec y ∧ b ⬝ᵥ y < 0

A system of linear equalities over nonnegative variables has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities.

source

theorem basicLinearAlgebra_lt {I : Type u_1} {J : Type u_2} {F : Type u_3} [Fintype I] [Fintype J] [Field F] [LinearOrder F] [IsStrictOrderedRing F] (A : Matrix I J F) (b : I → F) :

(∃ (x : J → F), A.mulVec x = b) ≠ ∃ (y : I → F), A.transpose.mulVec y = 0 ∧ b ⬝ᵥ y < 0

A system of linear equalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the equalities.

source

theorem basicLinearAlgebra {I : Type u_1} {J : Type u_2} {F : Type u_3} [Fintype I] [Fintype J] [Field F] [LinearOrder F] [IsStrictOrderedRing F] (A : Matrix I J F) (b : I → F) :

(∃ (x : J → F), A.mulVec x = b) ≠ ∃ (y : I → F), A.transpose.mulVec y = 0 ∧ b ⬝ᵥ y ≠ 0

A system of linear equalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the equalities; midly reformulated.

source

theorem inequalityFarkas {I : Type u_1} {J : Type u_2} {F : Type u_3} [Fintype I] [Fintype J] [Field F] [LinearOrder F] [IsStrictOrderedRing F] (A : Matrix I J F) (b : I → F) :

(∃ (x : J → F), 0 ≤ x ∧ A.mulVec x ≤ b) ≠ ∃ (y : I → F), 0 ≤ y ∧ 0 ≤ A.transpose.mulVec y ∧ b ⬝ᵥ y < 0

A system of linear inequalities over nonnegative variables has a solution if and only if we cannot obtain a contradiction by taking a nonnegative linear combination of the inequalities.

source

theorem inequalityFarkas_neg {I : Type u_1} {J : Type u_2} {F : Type u_3} [Fintype I] [Fintype J] [Field F] [LinearOrder F] [IsStrictOrderedRing F] (A : Matrix I J F) (b : I → F) :

(∃ (x : J → F), 0 ≤ x ∧ A.mulVec x ≤ b) ≠ ∃ (y : I → F), 0 ≤ y ∧ (-A.transpose).mulVec y ≤ 0 ∧ b ⬝ᵥ y < 0

A system of linear inequalities over nonnegative variables has a solution if and only if we cannot obtain a contradiction by taking a nonnegative linear combination of the inequalities; midly reformulated.