Farkas' lemma over a linearly ordered field

[UPSTREAM] A finite system of linear inequalities A *ᵥ x ≤ b over a linearly ordered field either has a solution or admits a certificate of infeasibility, a nonnegative combination y of its rows with y ᵥ* A = 0 and y ⬝ᵥ b < 0. Gordan's alternative follows: either a nonnegative combination of the rows of M is positive in every column, or a probability vector x has M *ᵥ x ≤ 0.

Main statements

• Matrix.farkas: Farkas' lemma for A *ᵥ x ≤ b.
• Matrix.gordan: Gordan's alternative.

Implementation notes

The proof is Fourier–Motzkin elimination. Eliminating the last variable multiplies the system on the left by the nonnegative matrix fmMatrix A, whose rows keep each row of A with a zero last coefficient and combine each row with a positive last coefficient with each row with a negative one, so that the last column of fmMatrix A * A vanishes. A solution of the eliminated system extends to the original one by placing the last variable between the bounds that the original rows impose, and a certificate y for the eliminated system gives the certificate y ᵥ* fmMatrix A for the original. Gordan's alternative states the simplex conditions explicitly, since the file defining stdSimplex imports topology.

theorem Matrix.farkas {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {ι : Type u_2} {σ : Type u_3} [Fintype ι] [Fintype σ] (A : Matrix ι σ K) (b : ι → K) : (∃ (x : σ → K), A.mulVec x ≤ b) ∨ ∃ (y : ι → K), 0 ≤ y ∧ vecMul y A = 0 ∧ y ⬝ᵥ b < 0

Farkas' lemma. A finite system of linear inequalities A *ᵥ x ≤ b over a linearly ordered field has a solution, or a nonnegative combination y of its rows has y ᵥ* A = 0 and y ⬝ᵥ b < 0.

theorem Matrix.gordan {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {ι : Type u_2} {σ : Type u_3} [Fintype ι] [Fintype σ] (M : Matrix ι σ K) : (∃ (y : ι → K), 0 ≤ y ∧ ∀ (j : σ), 0 < vecMul y M j) ∨ ∃ (x : σ → K), 0 ≤ x ∧ ∑ j : σ, x j = 1 ∧ M.mulVec x ≤ 0

Gordan's alternative. Either a nonnegative combination of the rows of M is positive in every column, or a probability vector x has M *ᵥ x ≤ 0.