Documentation

EconCSLib.Math.LinearAlgebra.Farkas

EconCSLib.Math.LinearAlgebra.Farkas #

Formalises Farkas' Lemma [MFoGT, Section 2.8, Exercise 8] in its objective-bound (LP-style) form, over any linearly ordered field.

Given a finite-row system A x ≥ b with S = { x | A x ≥ b } nonempty, the following are equivalent:

  1. (Primal bound.) For every feasible x, the linear objective ⟨c, x⟩ ≥ d.
  2. (Dual certificate.) There exists u : I → 𝕜 with u ≥ 0, uᵀA = c, and ⟨u, b⟩ ≥ d.

Proof structure #

The (←) direction is the standard weighted-sum argument.

The (→) direction homogenises the problem: introduce a slack variable t and the augmented system

A x - b·t ≥ 0 (m rows) t ≥ 0 (1 row) -⟨c, x⟩ + d·t ≥ 1 (1 row, encodes ⟨c, x⟩ < d·t strictly)

Show this is infeasible by case-splitting on t = 0 (recession direction contradicts the primal bound via y ∈ S) vs t > 0 (rescale to a primal point with ⟨c, x⟩ < d, contradicts the primal bound). Apply the Theorem of the Alternative to obtain a Farkas certificate of the augmented system; extract the coefficient β on the strict-bound row, divide by it, and read off the desired u.

Blueprint #

Augmented system construction #

Row index I ⊕ Bool where:

Column index Fin (n+1) where j.castSucc is x_j and Fin.last n is t.

source
@[reducible, inline]
abbrev EconCSLib.LinearAlgebra.FarkasAugRow (I : Type u_3) :
Type u_3

Row index of the augmented Farkas system.

Equations
Instances For
    source
    def EconCSLib.LinearAlgebra.farkasAugA {𝕜 : Type u_1} [Field 𝕜] {I : Type u_2} {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (d : 𝕜) :
    FarkasAugRow I → Fin (n + 1) → 𝕜

    Augmented matrix A_aug : FarkasAugRow I → Fin (n+1) → 𝕜.

    Equations
    Instances For
      source
      def EconCSLib.LinearAlgebra.farkasAugB {𝕜 : Type u_1} [Field 𝕜] {I : Type u_2} (b : I → 𝕜) :
      FarkasAugRow I → 𝕜

      Augmented RHS b_aug : FarkasAugRow I → 𝕜.

      Equations
      Instances For

        Simp lemmas for farkasAugA and farkasAugB #

        source
        @[simp]
        theorem EconCSLib.LinearAlgebra.farkasAugA_inl_castSucc {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (d : 𝕜) (i : I) (j' : Fin n) :
        farkasAugA A b c d (Sum.inl i) j'.castSucc = A i j'
        source
        @[simp]
        theorem EconCSLib.LinearAlgebra.farkasAugA_inl_last {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (d : 𝕜) (i : I) :
        farkasAugA A b c d (Sum.inl i) (Fin.last n) = -b i
        source
        @[simp]
        theorem EconCSLib.LinearAlgebra.farkasAugA_inr_false_castSucc {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (d : 𝕜) (j' : Fin n) :
        farkasAugA A b c d (Sum.inr false) j'.castSucc = 0
        source
        @[simp]
        theorem EconCSLib.LinearAlgebra.farkasAugA_inr_false_last {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (d : 𝕜) :
        farkasAugA A b c d (Sum.inr false) (Fin.last n) = 1
        source
        @[simp]
        theorem EconCSLib.LinearAlgebra.farkasAugA_inr_true_castSucc {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (d : 𝕜) (j' : Fin n) :
        farkasAugA A b c d (Sum.inr true) j'.castSucc = -c j'
        source
        @[simp]
        theorem EconCSLib.LinearAlgebra.farkasAugA_inr_true_last {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (d : 𝕜) :
        farkasAugA A b c d (Sum.inr true) (Fin.last n) = d
        source
        @[simp]
        theorem EconCSLib.LinearAlgebra.farkasAugB_inl {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] (b : I → 𝕜) (i : I) :
        farkasAugB b (Sum.inl i) = 0
        source
        @[simp]
        theorem EconCSLib.LinearAlgebra.farkasAugB_inr_false {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] (b : I → 𝕜) :
        farkasAugB b (Sum.inr false) = 0
        source
        @[simp]
        theorem EconCSLib.LinearAlgebra.farkasAugB_inr_true {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] (b : I → 𝕜) :
        farkasAugB b (Sum.inr true) = 1

        Augmented row evaluation at (x, t) = (xt ∘ castSucc, xt (last n)) #

        Each row of the augmented system has a clean form in terms of the original matrix/vector data. We collect these as private lemmas.

        Farkas Lemma #

        source
        theorem EconCSLib.LinearAlgebra.farkas_lemma {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (d : 𝕜) (hS : IsFeasible A b) :
        (∀ (x : Fin n → 𝕜), (∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x j) → d ≤ ∑ j : Fin n, c j * x j) ↔ ∃ (u : I → 𝕜), (∀ (i : I), 0 ≤ u i) ∧ (∀ (j : Fin n), ∑ i : I, u i * A i j = c j) ∧ d ≤ ∑ i : I, u i * b i

        Farkas' Lemma (objective-bound form). For a finite linear system A x ≥ b with S = {x | A x ≥ b} nonempty, the primal bound "∀ x ∈ S, ⟨c, x⟩ ≥ d" is equivalent to the existence of a nonneg dual certificate u with uᵀA = c and ⟨u, b⟩ ≥ d.